Misc fixes in extraction (AU-COBRA#100)

* Add more beta-reductions to inlining; inline definitions in inductive types; cleaned up ERC20 extraction to CameLIGO; misc fixes in Liquidity pretty-printing; fixed deboxing of type aliases * Update extraction/theories/LPretty.v Co-authored-by: Jakob Botsch Nielsen <[email protected]> * Fix comments in Elm tests Co-authored-by: Jakob Botsch Nielsen <[email protected]>
4ever2 · Jun 29, 2021 · 1441332 · 1441332
1 parent 4c2dae8
commit 1441332
Show file tree

Hide file tree

Showing 13 changed files with 473 additions and 149 deletions.
diff --git a/execution/examples/EIP20Token.v b/execution/examples/EIP20Token.v
@@ -22,7 +22,6 @@ Import RecordSetNotations.
 
 Section EIP20Token.
   Context {BaseTypes : ChainBase}.
-  Set Primitive Projections.
   Set Nonrecursive Elimination Schemes.
 
   Definition TokenValue := N.

diff --git a/extraction/_CoqProject b/extraction/_CoqProject
@@ -14,6 +14,7 @@ theories/Annotations.v
 theories/CameLIGOExtract.v
 theories/CameLIGOPretty.v
 theories/Certifying.v
+theories/CertifyingBeta.v
 theories/CertifyingEta.v
 theories/CertifyingInlining.v
 theories/ClosedAux.v

diff --git a/extraction/examples/CameLIGOExtractionTests.v b/extraction/examples/CameLIGOExtractionTests.v
@@ -344,14 +344,17 @@ Section CrowdfundingExtraction.
 End CrowdfundingExtraction.
 
 Section EIP20TokenExtraction.
+
   Import EIP20Token.
   Import RecordSetNotations.
 
+  Open Scope Z_scope.
+
   Definition init (ctx : ContractCallContext) (setup : EIP20Token.Setup) : option EIP20Token.State :=
     Some {| total_supply := setup.(init_amount);
-            balances := FMap.add (EIP20Token.owner setup) (init_amount setup) FMap.empty;
-            allowances := FMap.empty |}.
-  Open Scope Z_scope.
+            balances := Common.AddressMap.add (EIP20Token.owner setup) (init_amount setup) Common.AddressMap.empty;
+            allowances := Common.AddressMap.empty |}.
+
   Definition receive_ (chain : Chain)
        (ctx : ContractCallContext)
        (state : EIP20Token.State)
@@ -363,89 +366,72 @@ Section EIP20TokenExtraction.
     end.
   Close Scope Z_scope.
 
-  (* A specialized version of FMap's partial alter, w.r.t. FMap Address N *)
-  Definition partial_alter_addr_nat : string :=
-       "let partial_alter_addr_nat (f : nat option -> nat option)" ++ nl
-    ++ "                           (k : address)" ++ nl
-    ++ "                           (m : (address,nat) map) : (address,nat) map =" ++ nl
-    ++ "  match Map.find_opt k m with" ++ nl
-    ++ "    Some v -> Map.update k (f v) m" ++ nl
-    ++ "  | None -> Map.update k (f (None : nat option)) m" ++ nl.
-
-  Definition option_map_state_acts : string :=
-       "let option_map_state_acts (f : state -> (state * operation list)) (o : state option) =" ++ nl
-    ++ "  match o with" ++ nl
-    ++ "    Some a -> Some (f a)" ++ nl
-    ++ "    | None -> (None : (state * operation list))".
-
-  Definition bind_option_state : string :=
-       "let bind_option_state (a, b, c : unit) (m : state option) (f : state -> state option) : state option =" ++ nl
-    ++ "match m with" ++ nl
-    ++ "    Some a -> f a" ++ nl
-    ++ "  | None -> (None : state option)".
-
-  Definition with_default_N : string :=
-       "let with_default_N (n : nat) (m : nat option) : n =" ++ nl
-    ++ "  match m with" ++ nl
-    ++ "    Some m -> m" ++ nl
-    ++ "  | None -> n".
-
   Definition LIGO_EIP20Token_MODULE : CameLIGOMod EIP20Token.Msg ContractCallContext EIP20Token.Setup EIP20Token.State ActionBody :=
   {| (* a name for the definition with the extracted code *)
       lmd_module_name := "cameLIGO_eip20token" ;
 
       (* definitions of operations on pairs and ints *)
-      lmd_prelude := CameLIGOPrelude;
+      lmd_prelude := CameLIGOPrelude ++ nl ++
+                     dummy_chain;
 
       (* initial storage *)
       lmd_init := init ;
 
+      (* NOTE: printed as local [let]-bound definitions in the init *)
       lmd_init_prelude := "";
 
+      (* TODO: maybe not needed, [lmd_prelude] should be enough *)
+      lmd_receive_prelude := "";
+
       (* the main functionality *)
-      lmd_receive_prelude := partial_alter_addr_nat ++ nl ++
-      option_map_state_acts ++ nl ++
-      bind_option_state ++ nl ++
-      with_default_N;
       lmd_receive := receive_ ;
 
       (* code for the entry point *)
       lmd_entry_point := CameLIGOPretty.printWrapper (PREFIX ++ "eip20token") "msg" "state" CameLIGO_contractCallContext ++ nl
                         ++ CameLIGOPretty.printMain |}.
 
   Definition TT_remap_eip20token : list (kername * string) :=
-  [
-    remap <%% @ContractCallContext %%> "(adress * (address * int))"
-  ; remap <%% eqb_addr %%> "eq_addr"
-  ; remap <%% @Extras.with_default %%> "with_default_N"
-  ; remap <%% @Monads.bind %%> "bind_option_state"
-  ; remap <%% Monads.Monad_option %%> "()"
-
-  ; remap <%% @stdpp.base.insert %%> "Map.add"
-  ; remap <%% @stdpp.base.lookup %%> "Map.find_opt"
-  ; remap <%% @stdpp.base.empty %%> "Map.empty"
-  ; remap <%% @stdpp.base.partial_alter %%> "partial_alter_addr_nat"
-  ; remap <%% @gmap.gmap_partial_alter %%> ""
-  ; remap <%% @fin_maps.map_insert %%> ""
-  ; remap <%% @gmap.gmap_empty %%> ""
-  ; remap <%% @gmap.gmap_lookup %%> ""
-  ; remap <%% @address_eqdec %%> ""
-  ; remap <%% @address_countable %%> ""
-  ; remap <%% option_map %%> "option_map_state_acts"
+    TT_remap_default ++ [
+    (* TODO: is it of a correct type? *)
+    remap <%% @ContractCallContext %%> "(address * (address * int))"
+  ; remap <%% @ctx_from %%> "fst" (* small hack, but valid since ContractCallContext is mapped to a tuple *)
+
+  ; remap <%% @ActionBody %%> "operation"
+
+  ; remap <%% @FMap %%> "map"
+  ; remap <%% @Common.AddressMap.add %%> "Map.add"
+  ; remap <%% @Common.AddressMap.find %%> "Map.find_opt"
+  ; remap <%% @Common.AddressMap.empty %%> "Map.empty"
   ].
 
+  Definition TT_inlines_eip20token : list kername :=
+    [
+      <%% Monads.Monad_option %%>
+    ; <%% @Monads.bind %%>
+    ; <%% @Monads.ret %%>
+    ; <%% bool_rect %%>
+    ; <%% bool_rec %%>
+    ; <%% option_map %%>
+    ; <%% @Extras.with_default %%>
+
+    ; <%% @setter_from_getter_State_balances %%>
+    ; <%% @setter_from_getter_State_total_supply %%>
+    ; <%% @setter_from_getter_State_allowances %%>
+    ; <%% @set_State_balances %%>
+    ; <%% @set_State_allowances%%>
+    ; <%% @Common.AddressMap.AddrMap %%>
+    ].
+
+
   Definition TT_rename_eip20token :=
     [ ("Z0" ,"0tez")
-    ; ("N0", "0n")
-    ; ("N1", "1n")
+    ; ("N0", "0")
+    ; ("N1", "1")
     ; ("nil", "[]")
-      (* monad hack *)
-    ; ("Monad_option", "()")
     ; ("tt", "()") ].
 
   Time MetaCoq Run
-  (CameLIGO_prepare_extraction PREFIX [] TT_remap_eip20token TT_rename_eip20token LIGO_EIP20Token_MODULE).
-
+  (CameLIGO_prepare_extraction PREFIX TT_inlines_eip20token TT_remap_eip20token TT_rename_eip20token LIGO_EIP20Token_MODULE).
 
   Time Definition cameLIGO_eip20token := Eval vm_compute in cameLIGO_eip20token_prepared.
 
@@ -461,6 +447,35 @@ Section TestExtractionPlayground.
   Import RecordSetNotations.
 
   Open Scope N_scope.
+
+  (* A specialized version of FMap's partial alter, w.r.t. FMap Address N *)
+  Definition partial_alter_addr_nat : string :=
+       "let partial_alter_addr_nat (f : nat option -> nat option)" ++ nl
+    ++ "                           (k : address)" ++ nl
+    ++ "                           (m : (address,nat) map) : (address,nat) map =" ++ nl
+    ++ "  match Map.find_opt k m with" ++ nl
+    ++ "    Some v -> Map.update k (f v) m" ++ nl
+    ++ "  | None -> Map.update k (f (None : nat option)) m" ++ nl.
+
+  Definition option_map_state_acts : string :=
+       "let option_map_state_acts (f : state -> (state * operation list)) (o : state option) =" ++ nl
+    ++ "  match o with" ++ nl
+    ++ "    Some a -> Some (f a)" ++ nl
+    ++ "    | None -> (None : (state * operation list))".
+
+  Definition bind_option_state : string :=
+       "let bind_option_state (a, b, c : unit) (m : state option) (f : state -> state option) : state option =" ++ nl
+    ++ "match m with" ++ nl
+    ++ "    Some a -> f a" ++ nl
+    ++ "  | None -> (None : state option)".
+
+  Definition with_default_N : string :=
+       "let with_default_N (n : nat) (m : nat option) : n =" ++ nl
+    ++ "  match m with" ++ nl
+    ++ "    Some m -> m" ++ nl
+++ "  | None -> n".
+
+
   Definition test_try_transfer (from : Address)
        (to : Address)
        (amount : TokenValue)

diff --git a/extraction/examples/ERC20LiquidityExtraction.v b/extraction/examples/ERC20LiquidityExtraction.v
@@ -98,10 +98,10 @@ Section EIP20TokenExtraction.
     match maybe_msg with
     | Some (transfer to_addr amountt) => without_actions (try_transfer sender to_addr amountt state)
     | Some (transfer_from from to_addr amountt) => without_actions (try_transfer_from sender from to_addr amountt state)
-    (* 'approve' endpoint not included in this test *)
+   | Some (approve delegate amount) => without_actions (try_approve sender delegate amount state)
     | _ => None
     end.
-  
+
   Definition receive_wrapper
              (params : params)
              (st : State) : option (list ActionBody × State) :=
@@ -139,9 +139,11 @@ Section EIP20TokenExtraction.
 
 
   Definition TT_remap_eip20token : list (kername * string) :=
-  TT_remap_default ++ [
+    TT_remap_default ++ [
+    (* FIXME: it seems like the context type is wrong *)
     remap <%% @ContractCallContext %%> "(address * (address * int))"
   ; remap <%% @ctx_from %%> "fst" (* small hack, but valid since ContractCallContext is mapped to a tuple *)
+  ; remap <%% gmap.gmap %%> "map"
   ; remap <%% @AddressMap.add %%> "Map.add"
   ; remap <%% @AddressMap.find %%> "Map.find"
   ; remap <%% @AddressMap.empty %%> "(Map [])"
@@ -169,14 +171,16 @@ Section EIP20TokenExtraction.
     ; <%% @setter_from_getter_State_allowances %%>
     ; <%% @set_State_balances %%>
     ; <%% @set_State_allowances%%>
+
+    ; <%% @Common.AddressMap.AddrMap %%>
     ].
 
   Time MetaCoq Run
       (t <- liquidity_extraction_specialize PREFIX TT_remap_eip20token TT_rename_eip20token TT_inlines_eip20token EIP20Token_MODULE ;;
       tmDefinition EIP20Token_MODULE.(lmd_module_name) t).
 
   Print liquidity_eip20token.
-
+  
   (** We redirect the extraction result for later processing and compiling with the Liquidity compiler *)
   Redirect "./examples/liquidity-extract/liquidity_eip20token.liq" Compute liquidity_eip20token.
 

diff --git a/extraction/examples/ElmExtractTests.v b/extraction/examples/ElmExtractTests.v
@@ -12,6 +12,7 @@ From Coq Require Import String.
 From MetaCoq.Template Require Import Ast.
 From MetaCoq.Template Require Import Kernames.
 From MetaCoq.Template Require Import Loader.
+From MetaCoq.Template Require Import TemplateMonad.
 From MetaCoq Require Import monad_utils.
 From MetaCoq Require Import utils.
 
@@ -370,3 +371,133 @@ Module ex_infix1.
 "  in";
 "  map2" $>. reflexivity. Qed.
 End ex_infix1.
+
+Module recursor_ex.
+
+  Program Definition test {A B : Type} (f : A -> B) (xs : list A) : list B :=
+    list_rect (fun x => list B) [] (fun x _ rec => f x :: rec) xs.
+
+  Lemma test_is_map : @test = @map.
+  Proof. reflexivity. Qed.
+
+  Print test.
+
+  MetaCoq Quote Recursively Definition ex := @test.
+
+  Compute general_extract ex [] [].
+End recursor_ex.
+
+Module type_scheme_ex.
+
+  Definition general_extract_tc (p : program) (ignore: list kername) (TT : list (kername * string)) : TemplateMonad string :=
+  entry <- match p.2 with
+           | tConst kn _ => ret kn
+           | tInd ind _ => ret (inductive_mind ind)
+           | _ => tmFail "Expected program to be a tConst or tInd"
+           end;;
+  res <- tmEval lazy (extract_template_env
+                       no_check_args
+                       p.1
+                       (KernameSet.singleton entry)
+                       (fun k => existsb (eq_kername k) ignore));;
+  match res with
+  | Ok Σ =>
+    tmPrint Σ;;
+    let TT_fun kn := option_map snd (List.find (fun '(kn',v) => eq_kername kn kn') TT) in
+    s <- tmEval lazy (finish_print (print_env Σ TT_fun));;
+    match s with
+    | Ok (_,s) => ret s
+    | Err s => tmFail s
+    end
+  | Err s => tmFail s
+  end.
+
+
+  (* A simple type abbreviation *)
+
+  Definition Arrow (A B : Type) := A -> B.
+
+  MetaCoq Quote Recursively Definition Arrow_syn := Arrow.
+
+  Example Arrow_test :
+    general_extract Arrow_syn [] [] = Ok "type alias Arrow a b = a -> b".
+  Proof. vm_compute. reflexivity. Qed.
+
+  Definition Triple (A B C : Type) := A * B * C.
+
+  MetaCoq Quote Recursively Definition Triple_syn := Triple.
+
+  MetaCoq Run (general_extract_tc Triple_syn [] []).
+
+  Example Triple_test :
+    general_extract Triple_syn [] [] = Ok <$
+"type Prod a b";
+"  = Pair a b";
+"";
+"type alias Triple a b c = Prod (Prod a b) c" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+  Module LetouzeyExample.
+  (* An example from Letouzey's thesis, Section 3.3.4 *)
+
+  Definition P (b : bool) : Set := if b then nat else bool.
+  Definition Sch3 : (bool -> Set) -> Set := fun X => X true -> X false.
+  Definition Sch3_applied := (fun X => X true -> X false) (fun b => if b then nat else bool).
+
+  MetaCoq Quote Recursively Definition Sch3_syn := Sch3.
+
+  Example Sch3_test :
+    general_extract Sch3_syn [] [] = Ok "type alias Sch3 x = x -> x".
+  Proof. vm_compute. reflexivity. Qed.
+
+  MetaCoq Quote Recursively Definition Sch3_applied_syn := Sch3_applied.
+
+  (* In this case, the application reduces to a type with no type parameters *)
+  Example Sch3_applied_test :
+    general_extract Sch3_applied_syn [] [] = Ok <$
+"type Bool";
+"  = True";
+"  | False";
+"";
+"type Nat";
+"  = O";
+"  | S Nat";
+"";
+"type alias Sch3_applied = Nat -> Bool" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+  End LetouzeyExample.
+
+
+  (* [Vec] is a common example of using a type scheme to abbreviate a type *)
+
+  Definition vec (A : Type) (n : nat) := {xs : list A | length xs = n}.
+
+  Program Definition singleton_vec (n : nat) : vec nat 1 := [n].
+  Next Obligation. easy. Qed.
+
+  MetaCoq Quote Recursively Definition singleton_vec_syn := singleton_vec.
+
+  MetaCoq Run (general_extract_tc singleton_vec_syn [] []).
+
+  Example singleton_vec_test:
+    general_extract singleton_vec_syn [] [] = Ok <$
+"type Nat";
+"  = O";
+"  | S Nat";
+"";
+"type Sig a";
+"  = Exist a";
+"";
+"type List a";
+"  = Nil";
+"  | Cons a (List a)";
+"";
+"type alias Vec a = Sig (List a)";
+"";
+"singleton_vec : Nat -> Vec Nat";
+"singleton_vec n =";
+"  Exist (Cons n Nil)" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+End type_scheme_ex.