Misc fixes (AU-COBRA#239)

embedding/examples/FinMap.v

@@ -31,7 +31,7 @@ Definition global_to_tc := compose trans_minductive_entry trans_global_dec.
 (** We generate names for inductives and constants (prefixed with a module path) *)
 MetaCoq Run
         (mp_ <- tmCurrentModPath tt ;;
-          let mp := (PCUICTranslate.string_of_modpath mp_ ++ "@")%string in
+          let mp := (Utils.string_of_modpath mp_ ++ "@")%string in
           mkNames mp ["Maybe"; "Map"] "Acorn").
 
 (** And constructors (just names, no module path prefix) *)
@@ -70,7 +70,7 @@ MetaCoq Run
       (mkNames "" ["A"; "B"; "C"; "f"; "a";
                    "b"; "c"; "m"; "n"; "k";
                    "v"; "w"; "x"; "y"; "z";
-                   "lookup"; "add" ] "_coq").
+                   "lookup"; "add"] "_coq").
 
 Notation " ' x " := (eTy (tyVar x))
                     (in custom expr at level 1,

embedding/extraction/Liquidity.v

@@ -30,7 +30,7 @@ Record LiquidityModule :=
     init : expr;
     (* the [main] function must be of type
        message * storage -> option (list SimpleActionBody * storage) *)
-    main: string;
+    main : string;
     (* extra arguments to the main function for using in the wrapper;
        note that two mandatory arguments (MSG_ARG : message) and (STORAGE_ARG : storage)
        should not be the list *)
@@ -51,15 +51,15 @@ Fixpoint liquidifyTy (TT : env string) (ty : type) : string :=
   match ty with
   | tyInd nm =>
     (* ignore module path on printing *)
-    let (_, nm') := PCUICTranslate.kername_of_string nm in
+    let (_, nm') := Utils.kername_of_string nm in
     TCString.to_string (Extras.with_default nm' (option_map TCString.of_string (look TT nm)))
   | tyForall x b => "forall " ++ "'" ++ x ++ liquidifyTy TT b
   (* is it a product? *)
   | tyApp ty1 ty2 =>
     match ty1 with
       | (tyApp (tyInd ty_nm) A) =>
         (* ignore module path on printing *)
-        let (_, nm') := PCUICTranslate.kername_of_string ty_nm in
+        let (_, nm') := Utils.kername_of_string ty_nm in
         if TCString.to_string nm' =? "prod" then
           inParens (liquidifyTy TT A ++ " * " ++ liquidifyTy TT ty2)
         else inParens (liquidifyTy TT ty2 ++ " " ++ liquidifyTy TT ty1)
@@ -89,7 +89,7 @@ Definition liquidifyInductive (TT : env string) (gd : global_dec) : string :=
   match gd with
   | gdInd nm nparams ctors is_record =>
     (* ignore module path on printing *)
-    let (_, nm') := PCUICTranslate.kername_of_string nm in
+    let (_, nm') := Utils.kername_of_string nm in
     "type " ++ nm' ++ " = " ++
     if is_record then
       Extras.with_default "Not a Record!" (head (map (printRecord TT) ctors))
@@ -159,7 +159,7 @@ Definition isFalsePat (p : pat) :=
 (** We assume that before printing the Liquidity code
     [erase] has been applied to the expression *)
 
-Definition liquidify (TT TTty : env string ) : expr -> string :=
+Definition liquidify (TT TTty : env string) : expr -> string :=
   fix go (e : expr) : string :=
   match e with
   | eRel _ => "Error : indices are not supported"
@@ -182,7 +182,7 @@ Definition liquidify (TT TTty : env string ) : expr -> string :=
         else default_app
     | eConst cst =>
       (* ignore module path *)
-      let (_, cst') := PCUICTranslate.kername_of_string cst in
+      let (_, cst') := Utils.kername_of_string cst in
       (* is it a first projection? *)
       if cst' =? "fst" then go e2 ++ "." ++ inParens ("0")
       else
@@ -204,13 +204,13 @@ Definition liquidify (TT TTty : env string ) : expr -> string :=
           else ctor
   | eConst cst =>
     (* ignore module path *)
-    let (_, cst') := PCUICTranslate.kername_of_string cst in
+    let (_, cst') := Utils.kername_of_string cst in
     Extras.with_default cst' (option_map TCString.of_string (look TT cst))
   | eCase (ind,_) _ d bs =>
     match bs with
     | [b1; b2] => (* Handling if-then-else *)
       (* ignore module path *)
-      let (_, ind') := PCUICTranslate.kername_of_string ind in
+      let (_, ind') := Utils.kername_of_string ind in
       if (ind' =? "bool") then
         if (isTruePat (fst b1)) && (isFalsePat (fst b2)) then
           "if " ++ inParens (go d)
@@ -253,17 +253,17 @@ Definition LiquidityPrelude :=
     ++ newLine
     ++ "let[@inline] addTez (n : tez) (m : tez) = n + m"
     ++ newLine
-    ++ "let[@inline] andb (a : bool ) (b : bool ) = a & b"
+    ++ "let[@inline] andb (a : bool) (b : bool) = a & b"
     ++ newLine
-    ++ "let[@inline] eqTez (a : tez ) (b : tez ) = a = b"
+    ++ "let[@inline] eqTez (a : tez) (b : tez) = a = b"
     ++ newLine
-    ++ "let[@inline] lebN (a : nat ) (b : nat ) = a <= b"
+    ++ "let[@inline] lebN (a : nat) (b : nat) = a <= b"
     ++ newLine
-    ++ "let[@inline] ltbN (a : nat ) (b : nat ) = a < b"
+    ++ "let[@inline] ltbN (a : nat) (b : nat) = a < b"
     ++ newLine
-    ++ "let[@inline] lebTez (a : tez ) (b : tez ) = a<=b"
+    ++ "let[@inline] lebTez (a : tez) (b : tez) = a<=b"
     ++ newLine
-    ++ "let[@inline] ltbTez (a : tez ) (b : tez ) = a<b"
+    ++ "let[@inline] ltbTez (a : tez) (b : tez) = a<b"
     ++ newLine
     ++ "let[@inline] eqb_addr (a1 : address) (a2 : address) = a1 = a2"
     ++ newLine
@@ -282,8 +282,8 @@ Definition printWrapperBody (f_call : string) :=
     ++ "| None -> failwith ()".
 
 
-Definition printWrapper (TTty: env string) (msgTy : type) (storageTy : type)
-           (extra_args : list string) (contract : string): string :=
+Definition printWrapper (TTty : env string) (msgTy : type) (storageTy : type)
+           (extra_args : list string) (contract : string) : string :=
   let mainDomainType :=
       inParens (ofType MSG_ARG (liquidifyTy TTty msgTy))
                ++ inParens (ofType "st" (liquidifyTy TTty storageTy)) in
@@ -304,25 +304,25 @@ Definition print_glob TT TTty (def_clause : string) (def_name : string)
 Definition simpleCallCtx :=
   "(Current.time (), (Current.sender (), (Current.amount (), Current.balance ())))".
 
-Definition printLiqDef (TT TTty: env string) (def_name : string) (e : expr) :=
+Definition printLiqDef (TT TTty : env string) (def_name : string) (e : expr) :=
   print_glob TT TTty "let" def_name (to_glob_def (erase e)).
 
 
-Definition printLiqInit (TT TTty: env string) (def_name : string) (e : expr) :=
+Definition printLiqInit (TT TTty : env string) (def_name : string) (e : expr) :=
   let (args, body) := to_glob_def (erase e) in
   (** We expect that the last parameter of the [init] is _always_ the simple call context [CallCtx] *)
   let init_params := firstn (List.length args - 1) args in
   "let%init" ++ " " ++ "storage "
              ++ sep " " (map (fun p => inParens (ofType (fst p) (liquidifyTy TTty (snd p)))) init_params)
              ++ " = " ++ newLine
-             (* FIXME: this is currently a workaround, since [init] cannot refer to any global definition *)
-             ++ "let eqTez (a : tez ) (b : tez ) = a = b in"
+             (* TODO: this is currently a workaround, since [init] cannot refer to any global definition *)
+             ++ "let eqTez (a : tez) (b : tez) = a = b in"
              ++ newLine
              ++ printLiqDef TT TTty "f" e ++ newLine
              ++ "in" ++ newLine
              ++ printWrapperBody ("f " ++ sep " " (map fst init_params) ++ " " ++ simpleCallCtx).
 
-Definition liquidifyModule (TT TTty: env string) (module : LiquidityModule) :=
+Definition liquidifyModule (TT TTty : env string) (module : LiquidityModule) :=
   let dt := sep newLine (map (liquidifyInductive TTty) module.(datatypes)) in
   let st := liquidifyTy TTty module.(storage) in
   let fs := sep (newLine ++ newLine) (map (fun '(defName, body) => printLiqDef TT TTty defName body) module.(functions)) in

embedding/extraction/PreludeExt.v

@@ -26,10 +26,10 @@ Open Scope nat.
 (** ** Wrappers for some primitive types *)
 
 MetaCoq Run
-        ( mp_ <- tmCurrentModPath tt ;;
-          let mp := (PCUICTranslate.string_of_modpath mp_ ++ "@")%string in
+         (mp_ <- tmCurrentModPath tt ;;
+          let mp := (Utils.string_of_modpath mp_ ++ "@")%string in
           mkNames mp ["address"; "time"; "ContractAddr";
-                      "UserAddr"; "Time" ; "Money" ] "_coq").
+                      "UserAddr"; "Time" ; "Money"] "_coq").
 
 
 Definition address_ty :=
@@ -104,7 +104,7 @@ Notation "'acc_balance' st" :=
 Notation "'mkCallCtx' now sender sent_am bal " :=
   [| Pair time (address × (money × money)) {now}
           (Pair address (money × money) {sender}
-                (Pair money money {sent_am} {bal} )) |]
+                (Pair money money {sent_am} {bal})) |]
     (in custom expr at level 0).
 
 (** A simple representation of the call context *)
@@ -119,19 +119,19 @@ Definition sc_sent_amount (ctx : SimpleCallCtx) : Z := ctx.2.2.1.
 Definition sc_acc_balance (ctx : SimpleCallCtx) : Z := ctx.2.2.2.
 
 
-Definition is_contract (addr: address_coq) :=
+Definition is_contract (addr : address_coq) :=
   match addr with
   | ContractAddr_coq _ => true
   | UserAddr_coq _ => false
   end.
 
-Definition encode_addr (addr: address_coq) : nat + nat :=
+Definition encode_addr (addr : address_coq) : nat + nat :=
   match addr with
   | ContractAddr_coq x => inl x
   | UserAddr_coq x => inr x
   end.
 
-Definition decode_addr (addr: nat + nat) : address_coq :=
+Definition decode_addr (addr : nat + nat) : address_coq :=
   match addr with
   | inl x => ContractAddr_coq x
   | inr x => UserAddr_coq x
@@ -210,9 +210,9 @@ Module Maps.
 
 
   MetaCoq Run
-          ( mp_ <- tmCurrentModPath tt ;;
-            let mp := (PCUICTranslate.string_of_modpath mp_ ++ "@")%string in
-            mkNames mp ["addr_map" ] "_coq").
+           (mp_ <- tmCurrentModPath tt ;;
+            let mp := (Utils.string_of_modpath mp_ ++ "@")%string in
+            mkNames mp ["addr_map"] "_coq").
 
   Definition addr_map_acorn :=
     [\ data addr_map =
@@ -263,10 +263,10 @@ Module Maps.
     | cons (k,v) tl => mcons k v (of_list tl)
     end.
 
-  Lemma of_list_to_list m: of_list (to_list m) = m.
+  Lemma of_list_to_list m : of_list (to_list m) = m.
   Proof. induction m; simpl; congruence. Qed.
 
-  Lemma to_list_of_list l: to_list (of_list l) = l.
+  Lemma to_list_of_list l : to_list (of_list l) = l.
   Proof. induction l as [ | x l']; simpl; auto.
          destruct x. simpl; congruence. Qed.
 

embedding/extraction/SimpleBlockchainExt.v

@@ -25,8 +25,8 @@ Module AcornBlockchain.
   Definition Money := money.
 
   MetaCoq Run
-        ( mp_ <- tmCurrentModPath tt ;;
-          let mp := (PCUICTranslate.string_of_modpath mp_ ++ "@")%string in
+         (mp_ <- tmCurrentModPath tt ;;
+          let mp := (Utils.string_of_modpath mp_ ++ "@")%string in
           mkNames mp
                   ["SimpleChain" ; "Build_chain";
                   "SimpleContractCallContext" ; "Build_ctx" ;

embedding/theories/Ast.v

@@ -70,7 +70,7 @@ Definition expr_ind_case (P : expr -> Prop)
            (Hty : forall t : type, P (eTy t)) :
   forall e : expr, P e.
 Proof.
-  refine (fix ind (e : expr) := _ ).
+  refine (fix ind (e : expr) := _).
   destruct e.
   + apply Hrel.
   + apply Hvar.
@@ -140,7 +140,7 @@ Fixpoint lookup {A} (l : list (string * A)) key : option A :=
   | (key', v) :: xs => if eqb key' key then Some v else lookup xs key
   end.
 
-Fixpoint lookup_global ( Σ : global_env) (key : ename) : option global_dec :=
+Fixpoint lookup_global (Σ : global_env) (key : ename) : option global_dec :=
   match Σ with
   | [] => None
   | gdInd key' n v r :: xs => if eqb key' key then Some (gdInd key' n v r) else lookup_global xs key
@@ -218,8 +218,8 @@ Fixpoint indexify (l : list (ename * nat)) (e : expr) : expr :=
     | Some v => eRel v
     end
   | eLambda nm ty b =>
-    eLambda nm (indexify_type l ty) (indexify ((nm,0 ) :: bump_indices l 1) b)
-  | eTyLam nm b => eTyLam nm (indexify ((nm,0 ) :: bump_indices l 1) b)
+    eLambda nm (indexify_type l ty) (indexify ((nm,0) :: bump_indices l 1) b)
+  | eTyLam nm b => eTyLam nm (indexify ((nm,0) :: bump_indices l 1) b)
   | eLetIn nm e1 ty e2 =>
     eLetIn nm (indexify l e1) (indexify_type l ty) (indexify ((nm, 0) :: bump_indices l 1) e2)
   | eApp e1 e2 => eApp (indexify l e1) (indexify l e2)