Qcert.Translation.RuletocNRAEnv

Section RuletocNRAEnv.




  Context {fruntime:foreign_runtime}.


  Definition cnraenv_of_rule (r:rule) : cnraenv :=
    cnraenv_of_pat (rule_to_pattern r).

  Lemma cnraenv_of_rule_correct h c rps bind d :
    lift_failure (interp h c (rule_to_pattern rps) bind d) =
    cnraenv_eval h c (cnraenv_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 (cnraenv_eval h
                                      c
                            (cnraenv_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 (cnraenv_eval h (mkWorld world) (cnraenv_of_rule r) (drec nil) dunit).



  Definition cnraenv_of_aggregate (rules:rule→rule) (op:unaryOp) (secondMap:pat) (flatn:nat) : cnraenv :=
    cnraenv_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) =
    cnraenv_eval h c (cnraenv_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 (cnraenv_eval h c (cnraenv_of_aggregate rules op secondMap flatn) (drec bind) d).


  Definition translate_rule_to_cnraenv (r:rule) : cnraenv :=
    
    ANAppEnv (cnraenv_of_rule r) (ANConst (drec nil)).

End RuletocNRAEnv.