Module Qcert.LambdaNRA.Lang.LambdaNRA


Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Utils.
Require Import DataRuntime.

Section LambdaNRA.

  Context {fruntime:foreign_runtime}.

  Unset Elimination Schemes.

Lambda NRA AST
  Inductive lambda_nra : Set :=
  | LNRAVar : string -> lambda_nra
  | LNRATable : string -> lambda_nra
  | LNRAConst : data -> lambda_nra
  | LNRABinop : binary_op -> lambda_nra -> lambda_nra -> lambda_nra
  | LNRAUnop : unary_op -> lambda_nra -> lambda_nra
  | LNRAMap : lnra_lambda -> lambda_nra -> lambda_nra
  | LNRAMapProduct : lnra_lambda -> lambda_nra -> lambda_nra
  | LNRAProduct : lambda_nra -> lambda_nra -> lambda_nra
  | LNRAFilter : lnra_lambda -> lambda_nra -> lambda_nra
  with lnra_lambda : Set :=
  | LNRALambda : string -> lambda_nra -> lnra_lambda
  .

  Tactic Notation "lambda_nra_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "LNRAVar"%string
  | Case_aux c "LNRATable"%string
  | Case_aux c "LNRAConst"%string
  | Case_aux c "LNRABinop"%string
  | Case_aux c "LNRAUnop"%string
  | Case_aux c "LNRAMap"%string
  | Case_aux c "LNRAMapProduct"%string
  | Case_aux c "LNRAProduct"%string
  | Case_aux c "LNRAFilter"%string
  ].
  
  Set Elimination Schemes.

  Definition lambda_nra_rect
              (P : lambda_nra -> Type)
              (fvar : forall s : string, P (LNRAVar s))
              (ftable : forall t : string, P (LNRATable t))
              (fconst : forall d : data, P (LNRAConst d))
              (fbinop : forall (b : binary_op) (l0 l1: lambda_nra), P l0 -> P l1 -> P (LNRABinop b l0 l1))
              (funop : forall (u : unary_op) (l : lambda_nra), P l -> P (LNRAUnop u l))
              (fmap : forall (s:string) (l0 l1 : lambda_nra), P l0 -> P l1 -> P (LNRAMap (LNRALambda s l0) l1))
              (fmapconcat : forall (s:string) (l0 l1 : lambda_nra), P l0 -> P l1 -> P (LNRAMapProduct (LNRALambda s l0) l1))
              (fproduct : forall l : lambda_nra, P l -> forall l0 : lambda_nra, P l0 -> P (LNRAProduct l l0))
              (ffilter : forall (s:string) (l0 l1 : lambda_nra), P l0 -> P l1 -> P (LNRAFilter (LNRALambda s l0) l1)) :
    forall l, P l
    :=
      fix F (l : lambda_nra) : P l :=
        match l as l0 return (P l0) with
        | LNRAVar s => fvar s
        | LNRATable t => ftable t
        | LNRAConst d => fconst d
        | LNRABinop b l0 l1 => fbinop b l0 l1 (F l0) (F l1)
        | LNRAUnop u l0 => funop u l0 (F l0)
        | LNRAMap (LNRALambda s l0) l1 => fmap s l0 l1 (F l0) (F l1)
        | LNRAMapProduct (LNRALambda s l0) l1 => fmapconcat s l0 l1 (F l0) (F l1)
        | LNRAProduct l0 l1 => fproduct l0 (F l0) l1 (F l1)
        | LNRAFilter (LNRALambda s l0) l1 => ffilter s l0 l1 (F l0) (F l1)
        end.

  Definition lambda_nra_ind (P : lambda_nra -> Prop) := lambda_nra_rect P.
  Definition lambda_nra_rec (P:lambda_nra->Set) := lambda_nra_rect P.

Semantics of Lambda NRA

  Context (h:brand_relation_t).
  Section Semantics.
    Context (global_env:list (string*data)).

    Fixpoint lambda_nra_eval (env: bindings) (op:lambda_nra) : option data :=
      match op with
      | LNRAVar x => edot env x
      | LNRATable t => edot global_env t
      | LNRAConst d => Some (normalize_data h d)
      | LNRABinop b op1 op2 =>
        olift2 (fun d1 d2 => binary_op_eval h b d1 d2) (lambda_nra_eval env op1) (lambda_nra_eval env op2)
      | LNRAUnop u op1 =>
        olift (fun d1 => unary_op_eval h u d1) (lambda_nra_eval env op1)
      | LNRAMap lop1 op2 =>
        let aux_map d :=
            lift_oncoll (fun c1 => lift dcoll (lift_map (lnra_lambda_eval env lop1) c1)) d
        in olift aux_map (lambda_nra_eval env op2)
      | LNRAMapProduct lop1 op2 =>
        let aux_mapconcat d :=
            lift_oncoll (fun c1 => lift dcoll (omap_product (lnra_lambda_eval env lop1) c1)) d
        in olift aux_mapconcat (lambda_nra_eval env op2)
      | LNRAProduct op1 op2 =>
        let aux_product d :=
            lift_oncoll (fun c1 => lift dcoll (omap_product (fun _ => lambda_nra_eval env op2) c1)) d
        in olift aux_product (lambda_nra_eval env op1)
      | LNRAFilter lop1 op2 =>
        let pred x' :=
            match lnra_lambda_eval env lop1 x' with
            | Some (dbool b) => Some b
            | _ => None
            end
        in
        let aux_map d :=
            lift_oncoll (fun c1 => lift dcoll (lift_filter pred c1)) d
        in
        olift aux_map (lambda_nra_eval env op2)
      end
    with lnra_lambda_eval (env:bindings)
                          (lop:lnra_lambda) (d:data)
         : option data :=
           match lop with
           | LNRALambda x op =>
             (lambda_nra_eval (rec_sort (env++((x,d)::nil))) op)
           end.

    Lemma lnra_lambda_eval_lambda_eq env x lop d:
      lnra_lambda_eval env (LNRALambda x lop) d =
      (lambda_nra_eval (rec_sort (env++((x,d)::nil))) lop).
Proof.

    Lemma lambda_nra_eval_var_eq env s :
      lambda_nra_eval env (LNRAVar s) =
      edot env s.
Proof.

    Lemma lambda_nra_eval_table_eq env s :
      lambda_nra_eval env (LNRATable s) =
      edot global_env s.
Proof.

    Lemma lambda_nra_eval_const_eq env c :
      lambda_nra_eval env (LNRAConst c) =
      Some (normalize_data h c).
Proof.

    Lemma lambda_nra_eval_binary_op_eq env b op1 op2 :
      lambda_nra_eval env (LNRABinop b op1 op2) =
      olift2 (fun d1 d2 => binary_op_eval h b d1 d2) (lambda_nra_eval env op1) (lambda_nra_eval env op2).
Proof.

    Lemma lambda_nra_eval_unop_eq env u op1 :
      lambda_nra_eval env (LNRAUnop u op1) =
      olift (fun d1 => unary_op_eval h u d1) (lambda_nra_eval env op1).
Proof.

    Lemma lambda_nra_eval_map_eq env lop1 op2 :
      lambda_nra_eval env (LNRAMap lop1 op2) =
      let aux_map d :=
          lift_oncoll (fun c1 => lift dcoll (lift_map (lnra_lambda_eval env lop1) c1)) d
      in olift aux_map (lambda_nra_eval env op2).
Proof.

    Lemma lambda_nra_eval_map_concat_eq env lop1 op2 :
      lambda_nra_eval env (LNRAMapProduct lop1 op2) =
      let aux_mapconcat d :=
          lift_oncoll (fun c1 => lift dcoll (omap_product (lnra_lambda_eval env lop1) c1)) d
      in olift aux_mapconcat (lambda_nra_eval env op2).
Proof.

    Lemma lambda_nra_eval_product_eq env op1 op2 :
      lambda_nra_eval env (LNRAProduct op1 op2) =
      let aux_product d :=
          lift_oncoll (fun c1 => lift dcoll (omap_product (fun _ => lambda_nra_eval env op2) c1)) d
      in olift aux_product (lambda_nra_eval env op1).
Proof.

    Lemma lambda_nra_eval_filter_eq env lop1 op2 :
      lambda_nra_eval env (LNRAFilter lop1 op2) =
      let pred x' :=
          match lnra_lambda_eval env lop1 x' with
          | Some (dbool b) => Some b
          | _ => None
          end
      in
      let aux_map d :=
          lift_oncoll (fun c1 => lift dcoll (lift_filter pred c1)) d
      in
      olift aux_map (lambda_nra_eval env op2).
Proof.

    Lemma lambda_nra_eval_normalized {op:lambda_nra} {env:bindings} {o} :
      lambda_nra_eval env op= Some o ->
      Forall (fun x => data_normalized h (snd x)) env ->
      Forall (fun x => data_normalized h (snd x)) global_env ->
      data_normalized h o.
Proof.
  End Semantics.

  Section LambdaNRAScope.

    Fixpoint lambda_nra_free_vars (e:lambda_nra) :=
      match e with
      | LNRAConst d => nil
      | LNRAVar v => v :: nil
      | LNRATable t => nil
      | LNRABinop bop e1 e2 => lambda_nra_free_vars e1 ++ lambda_nra_free_vars e2
      | LNRAUnop uop e1 => lambda_nra_free_vars e1
      | LNRAMap (LNRALambda x e1) e2 =>
        (remove string_eqdec x (lambda_nra_free_vars e1)) ++ (lambda_nra_free_vars e2)
      | LNRAMapProduct (LNRALambda x e1) e2 =>
        (remove string_eqdec x (lambda_nra_free_vars e1)) ++ (lambda_nra_free_vars e2)
      | LNRAProduct e1 e2 =>
        (lambda_nra_free_vars e1) ++ (lambda_nra_free_vars e2)
      | LNRAFilter (LNRALambda x e1) e2 =>
        (remove string_eqdec x (lambda_nra_free_vars e1)) ++ (lambda_nra_free_vars e2)
      end.

    Fixpoint lambda_nra_subst (e:lambda_nra) (x:string) (e':lambda_nra) : lambda_nra :=
      match e with
      | LNRAConst d => LNRAConst d
      | LNRAVar y => if y == x then e' else LNRAVar y
      | LNRATable t => LNRATable t
      | LNRABinop bop e1 e2 => LNRABinop bop
                                   (lambda_nra_subst e1 x e')
                                   (lambda_nra_subst e2 x e')
      | LNRAUnop uop e1 => LNRAUnop uop (lambda_nra_subst e1 x e')
      | LNRAMap (LNRALambda y e1) e2 =>
        if (y == x)
        then LNRAMap (LNRALambda y e1) (lambda_nra_subst e2 x e')
        else LNRAMap (LNRALambda y (lambda_nra_subst e1 x e')) (lambda_nra_subst e2 x e')
      | LNRAMapProduct (LNRALambda y e1) e2 =>
        if (y == x)
        then LNRAMapProduct (LNRALambda y e1) (lambda_nra_subst e2 x e')
        else LNRAMapProduct (LNRALambda y (lambda_nra_subst e1 x e')) (lambda_nra_subst e2 x e')
      | LNRAProduct e1 e2 =>
        LNRAProduct (lambda_nra_subst e1 x e') (lambda_nra_subst e2 x e')
      | LNRAFilter (LNRALambda y e1) e2 =>
        if (y == x)
        then LNRAFilter (LNRALambda y e1) (lambda_nra_subst e2 x e')
        else LNRAFilter (LNRALambda y (lambda_nra_subst e1 x e')) (lambda_nra_subst e2 x e')
      end.

  End LambdaNRAScope.

  Local Hint Rewrite @lnra_lambda_eval_lambda_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_var_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_table_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_const_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_binary_op_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_unop_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_map_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_map_concat_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_product_eq : lambda_nra.
  Local Hint Rewrite @lambda_nra_eval_filter_eq : lambda_nra.

  Global Instance lambda_nra_eval_lookup_equiv_prop :
    Proper (eq ==> assoc_lookupr_equiv ==> eq ==> eq) lambda_nra_eval.
Proof.
    
  
  Section Top.
    Definition q_to_lambda (Q:lambda_nra -> lambda_nra) : lnra_lambda :=
      (LNRALambda "input" (Q (LNRAVar "input"))).

    Definition lnra_lambda_eval_top (Q:lambda_nra -> lambda_nra)
               (global_env:bindings) (input:data) : option data :=
      lnra_lambda_eval global_env nil (q_to_lambda Q) input.

    Definition lambda_nra_eval_top (q:lambda_nra) (env:bindings) : option data :=
      lambda_nra_eval (rec_sort env) nil q.
  End Top.

 
End LambdaNRA.

Global Hint Rewrite @lnra_lambda_eval_lambda_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_var_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_table_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_const_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_binary_op_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_unop_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_map_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_map_concat_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_product_eq : lambda_nra.
Global Hint Rewrite @lambda_nra_eval_filter_eq : lambda_nra.

Tactic Notation "lambda_nra_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "LNRAVar"%string
  | Case_aux c "LNRATable"%string
  | Case_aux c "LNRAConst"%string
  | Case_aux c "LNRABinop"%string
  | Case_aux c "LNRAUnop"%string
  | Case_aux c "LNRAMap"%string
  | Case_aux c "LNRAMapProduct"%string
  | Case_aux c "LNRAProduct"%string
  | Case_aux c "LNRAFilter"%string
  ].