Fix warnings (#198)

embedding/_CoqProject

@@ -1,4 +1,3 @@
--arg -w -arg -undeclared-scope
 -arg -w -arg -notation-overridden
 -arg -w -arg -non-reversible-notation
 

embedding/examples/Demo.v

@@ -1,4 +1,4 @@
-(** * Simple examples on how to use our framework  **)
+(** * Simple examples on how to use our framework **)
 From Coq Require Import String.
 From Coq Require Import Basics.
 From Coq Require Import List.
@@ -20,7 +20,7 @@ Import MCMonadNotation.
 Import BaseTypes.
 Import StdLib.
 
-Module MC:=MetaCoq.Template.Ast.
+Module MC := MetaCoq.Template.Ast.
 Import BasicAst.
 
 
@@ -34,7 +34,7 @@ Section MCDemo.
 
   (* Quote *)
   MetaCoq Quote Definition id_nat_syn := (fun x : nat => x).
-  Print id_nat_syn.
+  (* Print id_nat_syn. *)
   (* Ast.tLambda (nNamed "x")
      (Ast.tInd {| TC.inductive_mind := "nat"; TC.inductive_ind := 0 |}
         []) (Ast.tRel 0) : Ast.term *)
@@ -63,14 +63,14 @@ Definition negb_app_true :=
      |].
 
 
-Unset Printing Notations.
-
-Set Printing Notations.
-
 (* Execute the program using the interpreter *)
-Compute (expr_eval_n Σ 3 nil negb_app_true).
+Example eval_negb_app_true :
+  expr_eval_n Σ 3 nil negb_app_true = Ok (vConstr Bool "false" nil).
+Proof. reflexivity. Qed.
 
-Compute (expr_eval_i Σ 3 nil (indexify nil negb_app_true)).
+Example eval_negb_app_true' :
+  expr_eval_i Σ 3 nil (indexify nil negb_app_true) = Ok (vConstr Bool "false" nil).
+Proof. reflexivity. Qed.
 
 (* Make a Coq function from the AST of the program *)
 MetaCoq Unquote Definition coq_negb_app_true :=
@@ -80,7 +80,7 @@ MetaCoq Unquote Definition coq_negb_app_true :=
 Definition my_negb_syn :=
   [| \x : Bool => case x : Bool return Bool of
                    | True -> False
-                   | False -> True  |].
+                   | False -> True |].
 
 MetaCoq Unquote Definition my_negb :=
   (expr_to_tc Σ (indexify nil my_negb_syn)).
@@ -89,7 +89,17 @@ Lemma my_negb_coq_negb b :
   my_negb b = negb b.
 Proof. reflexivity. Qed.
 
-Compute (expr_eval_n Σ 3 nil my_negb_syn).
+Example eval_my_negb_syn :
+  expr_eval_n Σ 3 nil my_negb_syn = Ok
+         (vClos [] "x" cmLam [!Bool!]
+            [!Bool!]
+            (eCase (Bool, [])
+               [!Bool!] [|"x"|]
+               [({| pName := "true"; pVars := [] |},
+                [|$ "false" $ Bool|]);
+               ({| pName := "false"; pVars := [] |},
+               [|$ "true" $ Bool|])])).
+Proof. reflexivity. Qed.
 
 Example eval_my_negb_true :
   expr_eval_i Σ 4 nil (indexify nil [| {my_negb_syn} True |]) = Ok (vConstr Bool "false" nil).
@@ -145,14 +155,20 @@ Inductive blah :=
 
 Definition Σ' : global_env :=
   [gdInd "blah" 0 [("Bar", [(None,tyInd "blah"); (None,tyInd "blah")]); ("Baz", [])] false;
-     gdInd Nat  0 [("Z", []); ("Suc", [(None,tyInd Nat)])] false].
+      gdInd Nat 0 [("Z", []); ("Suc", [(None,tyInd Nat)])] false].
 
 Notation "'Bar'" := (eConstr "blah" "Bar") (in custom expr).
 Notation "'Baz'" := (eConstr "blah" "Baz") (in custom expr).
 
 Definition prog3 := [| Bar (Bar Baz Baz) Baz |].
 
-Compute (expr_eval_n Σ' 5 [] prog3).
+Example eval_prog3 :
+  expr_eval_n Σ' 5 [] prog3 = Ok
+         (vConstr "blah" "Bar"
+            [vConstr "blah" "Bar"
+               [vConstr "blah" "Baz" []; vConstr "blah" "Baz" []];
+            vConstr "blah" "Baz" []]).
+Proof. reflexivity. Qed.
 
 (* Examples of a fixpoint *)
 
@@ -180,7 +196,7 @@ MetaCoq Unquote Definition my_plus := (expr_to_tc Σ (indexify [] plus_syn)).
 
 Lemma my_plus_correct n m :
   my_plus n m = n + m.
-Proof. induction n;simpl;auto. Qed.
+Proof. induction n; simpl; auto. Qed.
 
 
 Definition two :=
@@ -190,8 +206,10 @@ Definition two :=
 Definition one_plus_one :=
   [| {plus_syn} 1 1 |].
 
-Compute (expr_eval_n Σ 10 [] [| {plus_syn} 1 1 |]).
-(* = Ok (vConstr "nat" "Suc" [vConstr "nat" "Suc" [vConstr "nat" "Z" []]])*)
+Example eval_one_plus_one :
+  expr_eval_n Σ 10 [] one_plus_one =
+  Ok (vConstr Nat "Suc" [vConstr Nat "Suc" [vConstr Nat "Z" []]]).
+Proof. reflexivity. Qed.
 
 Definition two_arg_fun_syn := [| \x : Nat => \y : Bool => x |].
 
@@ -202,11 +220,13 @@ Parameter bbb: bool.
 
 MetaCoq Quote Definition two_arg_fun_app_syn' := ((fun (x : nat) (_ : bool) => x) 1 bbb).
 
-Example one_plus_one_two : expr_eval_n Σ 10 [] one_plus_one = Ok two.
-Proof.  reflexivity. Qed.
+Example one_plus_one_two :
+  expr_eval_n Σ 10 [] one_plus_one = Ok two.
+Proof. reflexivity. Qed.
 
-Example one_plus_one_two_i : expr_eval_i Σ 10 [] (indexify [] one_plus_one) = Ok two.
-Proof.  reflexivity. Qed.
+Example one_plus_one_two_i :
+  expr_eval_i Σ 10 [] (indexify [] one_plus_one) = Ok two.
+Proof. reflexivity. Qed.
 
 
 Definition plus_syn' :=
@@ -222,17 +242,17 @@ MetaCoq Unquote Definition my_plus' :=
 
 Lemma my_plus'_0 : forall n, my_plus' 0 n = n.
 Proof.
-  induction n;simpl;easy.
+  induction n; simpl; easy.
 Qed.
 
 Lemma my_plus'_Sn : forall n m, my_plus' (S n) m = S (my_plus' n m).
 Proof.
-  induction m;simpl;easy.
+  induction m; simpl; easy.
 Qed.
 
 Lemma my_plus'_comm : forall n m, my_plus' n m = my_plus' m n.
 Proof.
-  induction n; intros m;simpl.
+  induction n; intros m; simpl.
   + rewrite my_plus'_0. reflexivity.
   + rewrite my_plus'_Sn. easy.
 Qed.
@@ -241,7 +261,7 @@ Qed.
 Lemma my_plus'_correct : forall n m, my_plus' n m = n + m.
 Proof.
   intros n m.
-  induction m;simpl;easy.
+  induction m; simpl; easy.
 Qed.
 
 
@@ -252,8 +272,24 @@ Definition id_rec :=
            | Suc z -> Suc ("plus" z))
    |].
 
-Compute (expr_eval_n Σ 20 [] [| {id_rec} (Suc (Suc (Suc 1))) |]).
-Compute (expr_eval_i Σ 20 [] (indexify [] [| {id_rec} (Suc (Suc (Suc 1))) |])).
+Example eval_id_rec :
+  expr_eval_n Σ 20 [] [| {id_rec} (Suc (Suc (Suc 1))) |] =
+  Ok (vConstr Nat "Suc"
+      [vConstr Nat "Suc"
+        [vConstr Nat "Suc"
+          [vConstr Nat "Suc"
+            [vConstr Nat "Z" []]]]]).
+Proof. reflexivity. Qed.
+
+Example eval_id_rec' :
+  expr_eval_i Σ 20 [] (indexify [] [| {id_rec} (Suc (Suc (Suc 1))) |]) =
+  Ok (vConstr Nat "Suc"
+      [vConstr Nat "Suc"
+        [vConstr Nat "Suc"
+          [vConstr Nat "Suc"
+            [vConstr Nat "Z" []]]]]).
+Proof. reflexivity. Qed.
+
 
 Example id_rec_named_and_indexed :
   let arg := [| Suc (Suc (Suc 1)) |] in
@@ -268,14 +304,77 @@ Example plus_named_and_indexed :
   expr_eval_i Σ 20 [] (indexify [] [| ({plus_syn} {two}) {three} |]).
 Proof. reflexivity. Qed.
 
-Compute (expr_eval_i Σ 10 [] (indexify [] [| {plus_syn} 1 |])).
+Example eval_plus_syn_one :
+  expr_eval_i Σ 10 [] (indexify [] [| {plus_syn} 1 |]) =
+  Ok (vClos
+      [("x",
+        vConstr Nat "Suc"
+          [vConstr Nat "Z" []]);
+      ("plus",
+      vClos [] "x" (cmFix "plus") [!Nat!]
+        (tyArr [!Nat!]
+            [!Nat!])
+        [|\ "y" : Nat =>
+          {eCase (Nat, [])
+              [!Nat!] (eRel 1)
+              [({| pName := "Z"; pVars := [] |}, eRel 0);
+              ({| pName := "Suc"; pVars := ["z"] |},
+              eApp [|$ "Suc" $ Nat|]
+                (eApp (eApp (eRel 3) (eRel 0)) (eRel 1)))]}|])] "y"
+      cmLam [!Nat!] [!Nat!]
+      (eCase (Nat, [])
+          [!Nat!] (eRel 1)
+          [({| pName := "Z"; pVars := [] |}, eRel 0);
+          ({| pName := "Suc"; pVars := ["z"] |},
+          eApp [|$ "Suc" $ Nat|]
+            (eApp (eApp (eRel 3) (eRel 0)) (eRel 1)))])).
+Proof. reflexivity. Qed.
 
-Compute (indexify [] [| {plus_syn}|]).
-Compute (expr_eval_n Σ 10 [] [| {plus_syn} 0 |]).
+Example eval_plus_syn :
+  indexify [] [| {plus_syn}|] =
+  [|fix "plus" ("x" : Nat)
+    : Nat -> Nat :=
+      \ "y" : Nat =>
+      {eCase (Nat, [])
+          [!Nat!] (eRel 1)
+          [({| pName := "Z"; pVars := [] |}, eRel 0);
+          ({| pName := "Suc"; pVars := ["z"] |},
+          eApp [|$ "Suc" $ Nat|]
+            (eApp (eApp (eRel 3) (eRel 0)) (eRel 1)))]}|].
+Proof. reflexivity. Qed.
+
+Example eval_plus_syn_zero :
+  expr_eval_n Σ 10 [] [| {plus_syn} 0 |] =
+  Ok (vClos
+      [("x", vConstr Nat "Z" []);
+      ("plus",
+      vClos [] "x" (cmFix "plus") [!Nat!]
+        (tyArr [!Nat!]
+            [!Nat!])
+        [|\ "y" : Nat =>
+          {eCase (Nat, [])
+              [!Nat!] [|"x"|]
+              [({| pName := "Z"; pVars := [] |}, [|"y"|]);
+              ({| pName := "Suc"; pVars := ["z"] |},
+              eApp [|$ "Suc" $ Nat|]
+                (eApp (eApp [|"plus"|] [|"z"|]) [|"y"|]))]}|])] "y"
+      cmLam [!Nat!] [!Nat!]
+      (eCase (Nat, [])
+          [!Nat!] [|"x"|]
+          [({| pName := "Z"; pVars := [] |}, [|"y"|]);
+          ({| pName := "Suc"; pVars := ["z"] |},
+          eApp [|$ "Suc" $ Nat|]
+            (eApp (eApp [|"plus"|] [|"z"|]) [|"y"|]))])).
+Proof. reflexivity. Qed.
 
 Definition fun_app := [| (\x : Nat => \y : Nat => y + x) Zero |].
 
-Compute (expr_eval_n Σ' 10 [] fun_app).
+Example eval_fun_app :
+  expr_eval_n Σ' 10 [] fun_app =
+  Ok (vClos [("x", vConstr Nat "Z" [])] "y" cmLam
+      [!Nat!] [!Nat!]
+      (eApp (eApp (eConst "Coq/Init/Nat@add") [|"y"|]) [|"x"|])).
+Proof. reflexivity. Qed.
 
 
 Inductive mybool :=
@@ -331,8 +430,8 @@ Import Template.Ast.
 Unset Primitive Projections.
 
 Definition State_syn :=
-  [\ record "State" := "mkState" { "balance" : Nat ; "day" : Nat }  \].
+  [\ record "State" := "mkState" { "balance" : Nat ; "day" : Nat } \].
 
 MetaCoq Unquote Inductive (global_to_tc State_syn).
 
-Print State.
+(* Print State. *)

embedding/examples/FinMap.v

@@ -33,7 +33,7 @@ MetaCoq Run
           mkNames mp ["Maybe"; "Map"] "Acorn").
 
 (** And constructors (just names, no module path prefix) *)
-MetaCoq Run (mkNames "" ["Nothing";"Just"; "MNil"; "MCons"] "Acorn").
+MetaCoq Run (mkNames "" ["Nothing"; "Just"; "MNil"; "MCons"] "Acorn").
 
 (** Now we can use [Maybe] as a name for a data type in our deep embedding. [Maybe] contains a string "MaybeAcorn" *)
 
@@ -44,15 +44,15 @@ MetaCoq Run (mkNames "" ["Nothing";"Just"; "MNil"; "MCons"] "Acorn").
 (** Now, we define an AST (a deep embedding) for [MaybeAcorn] data type. [MaybeAcorn] is the same as [option] of Coq and [Maybe] of Haskell. First, we define a new datatype without using notations *)
 
 Definition maybe_syn :=
-  gdInd Maybe 1 [(Nothing, []);  (Just, [(None,tyRel 0)])] false.
+  gdInd Maybe 1 [(Nothing, []); (Just, [(None,tyRel 0)])] false.
 
 MetaCoq Unquote Inductive (global_to_tc maybe_syn).
 
 (** Now, we define a type of finite maps using notations based on Custom Entries *)
 Definition map_syn :=
   [\ data Map # 2 =
        MNil [_]
-     | MCons [^1, ^0, (Map ^1 ^0), _]  \].
+     | MCons [^1, ^0, (Map ^1 ^0), _] \].
 
 MetaCoq Unquote Inductive (global_to_tc map_syn).
 
@@ -70,7 +70,7 @@ Notation " ' x " := (eTy (tyVar x))
 (** [if .. then .. else] is just a shortcut for [case] of a boolean expression *)
 Notation "'if' cond 'then' b1 'else' b2 : ty" :=
     (eCase (Bool,[]) ty cond
-           [(pConstr true_name [],b1);(pConstr false_name [],b2)])
+           [(pConstr true_name [],b1); (pConstr false_name [],b2)])
       (in custom expr at level 2,
           cond custom expr at level 4,
           ty custom type at level 4,
@@ -121,7 +121,7 @@ Module NatMap := FMapWeakList.Make Nat_as_OT.
 (** Conversion function from our type of finite maps to the one in the standard library *)
 Fixpoint from_amap {A} (m : MapAcorn nat A) : NatMap.Raw.t A :=
   match m with
-  | MNilAcorn  => []
+  | MNilAcorn => []
   | MConsAcorn k v m' => (k,v) :: from_amap m'
   end.
 
@@ -147,7 +147,7 @@ Section MapEval.
 
   (** Boolean equality of two natural numbers in Acorn *)
   Definition eqb_syn : expr :=
-    [| (fix "eqb" (n : Nat) : Nat ->  Bool :=
+    [| (fix "eqb" (n : Nat) : Nat -> Bool :=
            case n : Nat return Nat -> Bool of
            | Zero -> \m : Nat => (case m : Nat return Bool of
                    | Zero -> True
@@ -166,7 +166,7 @@ Section MapEval.
   Lemma nat_eqb_correct n m : nat_eqb n m = Nat.eqb n m.
   Proof.
     revert m.
-    induction n;intros m; now destruct m.
+    induction n; intros m; now destruct m.
   Qed.
 
   (** The syntactic representation of the following map [1 ~> 1; 0 ~> 0] *)