Qcert.Translation.RuletoNRA

Section RuletoNRA.




  Context {fruntime:foreign_runtime}.


  Definition nra_of_rule (r:rule) : nra :=
    nra_of_pat (rule_to_pattern r).

  Lemma rule_trans_correct {h:list(string×string)} c rps bind d :
    lift_failure (interp h c (rule_to_pattern rps) bind d) =
    nra_eval h (nra_of_rule rps) (pat_context_data (drec (rec_sort c)) (drec bind) d).

  Lemma rule_parts_trans_correct_r {h:list(string×string)} c rps bind d :
      interp h c (rule_to_pattern rps) bind d =
      lift_pat_failure (nra_eval h
                            (nra_of_rule rps)
                            (pat_context_data (drec (rec_sort c)) (drec bind) d)).


  Definition lift_rule_failure (d : option data) :=
    match d with
      | Some (dcoll nil) ⇒ Some nil
      | Some (dcoll (l::nil)) ⇒ Some (l::nil)
      | _ ⇒ None
    end.

  Definition rule_trans (r:rule) : nra :=
    AUnop AFlatten
          (AMap (nra_of_rule r)
                (AUnop AColl (pat_context AID (AConst (drec nil))
                                          (AConst dunit)))).

  Lemma rule_trans_correct_r {h:list(string×string)} (r:rule) (world:list data) :
    eval_rule h r world =
    lift_rule_failure (nra_eval h (rule_trans r) (drec (mkWorld world))).



  Definition nra_of_aggregate (rules:rule→rule) (op:unaryOp) (secondMap:pat) (nflat:nat): nra :=
    nra_of_pat (aggregate rules op secondMap nflat).

  Lemma aggregate_trans_correct {h:list(string×string)} c rules op secondMap bind d nflat :
    lift_failure (interp h c (aggregate rules op secondMap nflat) bind d) =
    nra_eval h (nra_of_aggregate rules op secondMap nflat) (pat_context_data (drec (rec_sort c)) (drec bind) d).

  Lemma aggregate_trans_correct_r {h:list(string×string)} c rules op secondMap bind d nflat:
    interp h c (aggregate rules op secondMap nflat) bind d =
    lift_pat_failure (nra_eval h (nra_of_aggregate rules op secondMap nflat) (pat_context_data (drec (rec_sort c)) (drec bind) d)).

End RuletoNRA.