Qcert.LambdaNRA.Lang.LambdaNRA



Section LambdaNRA.

  Context {fruntime:foreign_runtime}.


Lambda NRA AST
  Inductive lnra : Set :=
  | LNRAVar : string → lnra
  | LNRATable : string → lnra
  | LNRAConst : data → lnra
  | LNRABinop : binOp → lnra → lnra → lnra
  | LNRAUnop : unaryOp → lnra → lnra
  | LNRAMap : lnra_lambda → lnra → lnra
  | LNRAMapConcat : lnra_lambda → lnra → lnra
  | LNRAProduct : lnra → lnra → lnra
  | LNRAFilter : lnra_lambda → lnra → lnra
  with lnra_lambda : Set :=
  | LNRALambda : string → lnra → lnra_lambda
  .

  Tactic Notation "lnra_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 "LNRAMapConcat"%string
  | Case_aux c "LNRAProduct"%string
  | Case_aux c "LNRAFilter"%string
  ].


  Definition lnra_rect
              (P : lnra → Type)
              (fvar : ∀ s : string, P (LNRAVar s))
              (ftable : ∀ t : string, P (LNRATable t))
              (fconst : ∀ d : data, P (LNRAConst d))
              (fbinop : ∀ (b : binOp) (l : lnra), P l → ∀ l0 : lnra, P l0 → P (LNRABinop b l l0))
              (funop : ∀ (u : unaryOp) (l : lnra), P l → P (LNRAUnop u l))
              (fmap : ∀ (s:string) (l0 l1 : lnra), P l0 → P l1 → P (LNRAMap (LNRALambda s l0) l1))
              (fmapconcat : ∀ (s:string) (l0 l1 : lnra), P l0 → P l1 → P (LNRAMapConcat (LNRALambda s l0) l1))
              (fproduct : ∀ l : lnra, P l → ∀ l0 : lnra, P l0 → P (LNRAProduct l l0))
              (ffilter : ∀ (s:string) (l0 l1 : lnra), P l0 → P l1 → P (LNRAFilter (LNRALambda s l0) l1)) :
    ∀ l, P l
    :=
      fix F (l : lnra) : 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 (F l0) l1 (F l1)
        | LNRAUnop u l0 ⇒ funop u l0 (F l0)
        | LNRAMap (LNRALambda s l0) l1 ⇒ fmap s l0 l1 (F l0) (F l1)
        | LNRAMapConcat (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 lnra_ind (P : lnra → Prop) := lnra_rect P.
  Definition lnra_rec (P:lnra→Set) := lnra_rect P.

Semantics of Lambda NRA

  Context (h:brand_relation_t).
  Context (global_env:list (string×data)).

  Fixpoint lnra_eval (env: bindings) (op:lnra) : 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 ⇒ fun_of_binop h b d1 d2) (lnra_eval env op1) (lnra_eval env op2)
    | LNRAUnop u op1 ⇒
      olift (fun d1 ⇒ fun_of_unaryop h u d1) (lnra_eval env op1)
    | LNRAMap lop1 op2 ⇒
        let aux_map d :=
            lift_oncoll (fun c1 ⇒ lift dcoll (rmap (lnra_lambda_eval env lop1) c1)) d
        in olift aux_map (lnra_eval env op2)
    | LNRAMapConcat lop1 op2 ⇒
      let aux_mapconcat d :=
          lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (lnra_lambda_eval env lop1) c1)) d
      in olift aux_mapconcat (lnra_eval env op2)
    | LNRAProduct op1 op2 ⇒
      
      let aux_product d :=
          lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (fun _ ⇒ lnra_eval env op2) c1)) d
      in olift aux_product (lnra_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 (lnra_eval env op2)
    end
  with lnra_lambda_eval (env:bindings)
                        (lop:lnra_lambda) (d:data)
       : option data :=
    match lop with
    | LNRALambda x op ⇒
      (lnra_eval (env++((x,d)::nil)) op)
    end.

  Definition q_to_lambda (Q:lnra → lnra) :=
    (LNRALambda "input" (Q (LNRAVar "input"))).

  Definition eval_q (Q:lnra → lnra) (input:data) : option data :=
    lnra_lambda_eval nil (q_to_lambda Q) input.

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

  Lemma lnra_eval_map_eq env lop1 op2 :
    lnra_eval env (LNRAMap lop1 op2) =
        let aux_map d :=
            lift_oncoll (fun c1 ⇒ lift dcoll (rmap (lnra_lambda_eval env lop1) c1)) d
        in olift aux_map (lnra_eval env op2).

  Lemma lnra_eval_map_concat_eq env lop1 op2 :
    lnra_eval env (LNRAMapConcat lop1 op2) =
      let aux_mapconcat d :=
          lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (lnra_lambda_eval env lop1) c1)) d
      in olift aux_mapconcat (lnra_eval env op2).

  Lemma lnra_eval_product_eq env op1 op2 :
    lnra_eval env (LNRAProduct op1 op2) =
        let aux_product d :=
          lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (fun _ ⇒ lnra_eval env op2) c1)) d
        in olift aux_product (lnra_eval env op1).

  Lemma lnra_eval_filter_eq env lop1 op2 :
    lnra_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 (lnra_eval env op2).

  Lemma lnra_eval_normalized {op:lnra} {env:bindings} {o} :
    lnra_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.

  Section LambdaNRAScope.

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

    Fixpoint lnra_subst (e:lnra) (x:string) (e':lnra) : lnra :=
      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
                                   (lnra_subst e1 x e')
                                   (lnra_subst e2 x e')
      | LNRAUnop uop e1 ⇒ LNRAUnop uop (lnra_subst e1 x e')
      | LNRAMap (LNRALambda y e1) e2 ⇒
        if (y == x)
        then LNRAMap (LNRALambda y e1) (lnra_subst e2 x e')
        else LNRAMap (LNRALambda y (lnra_subst e1 x e')) (lnra_subst e2 x e')
      | LNRAMapConcat (LNRALambda y e1) e2 ⇒
        if (y == x)
        then LNRAMapConcat (LNRALambda y e1) (lnra_subst e2 x e')
        else LNRAMapConcat (LNRALambda y (lnra_subst e1 x e')) (lnra_subst e2 x e')
      | LNRAProduct e1 e2 ⇒
        LNRAProduct (lnra_subst e1 x e') (lnra_subst e2 x e')
      | LNRAFilter (LNRALambda y e1) e2 ⇒
        if (y == x)
        then LNRAFilter (LNRALambda y e1) (lnra_subst e2 x e')
        else LNRAFilter (LNRALambda y (lnra_subst e1 x e')) (lnra_subst e2 x e')
      end.

  End LambdaNRAScope.
End LambdaNRA.


Tactic Notation "lnra_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 "LNRAMapConcat"%string
  | Case_aux c "LNRAProduct"%string
  | Case_aux c "LNRAFilter"%string
  ].