Qcert.Translation.RuletoNRAEnv

Section RuletoNRAEnv.




  Context {fruntime:foreign_runtime}.


  Definition nraenv_of_rule (r:rule) : nraenv :=
    nraenv_of_pat (rule_to_pattern r).

  Lemma nraenv_of_rule_correct h c rps bind d :
    lift_failure (interp h c (rule_to_pattern rps) bind d) =
    nraenv_eval h c (nraenv_of_rule rps) (drec bind) d.

  Lemma rule_parts_envtrans_correct_r h c rps bind d :
      interp h c (rule_to_pattern rps) bind d =
      lift_pat_failure (nraenv_eval h
                                      c
                            (nraenv_of_rule rps)
                            (drec bind) d).

  Lemma rule_trans_correct_r (h:list (string×string)) (r:rule) (world:list data) :
    eval_rule h r world =
    lift_rule_failure (nraenv_eval h (mkWorld world) (nraenv_of_rule r) (drec nil) dunit).



  Definition nraenv_of_aggregate (rules:rule→rule) (op:unaryOp) (secondMap:pat) (flatn:nat) : nraenv :=
    nraenv_of_pat (aggregate rules op secondMap flatn).

  Lemma aggregate_envtrans_correct h c rules op secondMap bind d (flatn:nat) :
    lift_failure (interp h c (aggregate rules op secondMap flatn) bind d) =
    nraenv_eval h c (nraenv_of_aggregate rules op secondMap flatn) (drec bind) d.

  Lemma aggregate_envtrans_correct_r h c rules op secondMap bind d (flatn:nat) :
    interp h c (aggregate rules op secondMap flatn) bind d =
    lift_pat_failure (nraenv_eval h c (nraenv_of_aggregate rules op secondMap flatn) (drec bind) d).


  Definition translate_rule_to_nraenv (r:rule) : nraenv :=
    
    NRAEnvAppEnv (nraenv_of_rule r) (NRAEnvConst (drec nil)).

End RuletoNRAEnv.