Commit cb9cf881 authored by Danil's avatar Danil

Extracting crowdfunding with certified extraction. Printing types for...

Extracting crowdfunding with certified extraction. Printing types for top-level Liquidity definitions.
parent 60db1f69
Pipeline #19450 failed with stage
in 11 minutes and 9 seconds
......@@ -69,6 +69,7 @@ extraction/examples/SimpleBlockchain.v
extraction/examples/crowdfunding_extract/CrowdfundingData.v
extraction/examples/crowdfunding_extract/Crowdfunding.v
extraction/examples/CounterCertifiedExtraction.v
extraction/examples/CrowdfundingCertifiedExtraction.v
extraction/examples/CounterDepCertifiedExtraction.v
extraction/examples/CounterRefinementTypes.v
extraction/examples/StackInterpreter.v
......
......@@ -91,6 +91,8 @@ Definition TT : env string :=
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
].
......
......@@ -67,6 +67,7 @@ Definition TT : env string :=
; remap <% Z.sub %> "subInt"
; remap <% Z.leb %> "leInt"
; remap <% Z %> "int"
; remap <% bool %> "bool"
; remap <% nat %> "address"
; ("left", "Left")
; ("right", "Right")
......@@ -74,6 +75,8 @@ Definition TT : env string :=
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
; local <% my_bool_dec %>
......
......@@ -69,13 +69,17 @@ Definition TT_rt : env string :=
; remap <% Z.leb %> "leInt"
; remap <% Z %> "int"
; remap <% nat %> "address"
; remap <% proj1_sig %> "(fun x -> x)"
; remap <% bool %> "bool"
; remap <% proj1_sig %> "(fun x -> x)" (* this is a safe, but ad-hoc optimisation*)
; remap <% non_neg %> "int" (* this is again an ad-hoc optimisation *)
; ("left", "Left")
; ("right", "Right")
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% my_bool_dec %>
].
......
Require Import String ZArith Basics.
From ConCert.Embedding Require Import Ast Notations CustomTactics
PCUICTranslate PCUICtoTemplate Utils MyEnv.
From ConCert.Extraction Require Import Certified LPretty.
From ConCert.Extraction.Examples Require Import Prelude CrowdfundingData Crowdfunding SimpleBlockchain.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import AcornBlockchain.
Import MonadNotation.
Open Scope Z.
Import CrowdfundingContract.
Import Validate.
Import Receive.
(** A translation table for various constants we want to rename *)
Definition TT : env string :=
[ (* types *)
remap <% Z %> "tez"
; remap <% address_coq %> "address"
; remap <% time_coq %> "timestamp"
; remap <% nat %> "nat"
; remap <% bool %> "bool"
; remap <% unit %> "unit"
; remap <% list %> "list"
; remap <% option %> "option"
; remap <% addr_map %> "(address,tez) map"
; remap <% SimpleActionBody %> "operation"
; remap <% Z.add %> "addTez"
; remap <% Z.eqb %> "eqTez"
; remap <% Z.leb %> "leTez"
; remap <% Z.ltb %> "ltTez"
; remap <% ltb_time %> "ltb_time"
; remap <% leb_time %> "leb_time"
; remap <% eqb_addr %> "eq_addr"
; remap <% andb %> "andb"
; remap <% negb %> "not"
; remap <% add_map %> "Map.add"
; remap <% lookup %> "Map.find"
; ("Z0" ,"0DUN")
; ("nil", "[]")
; ("tt", "()")
; local <% msg_coq %>
; local <% @fst %>
; local <% @snd %>
; local <% update_contribs %>
; local <% maybe_bind_unit %>
; local <% set_done %>
; local <% validate %>
].
Definition printWrapperAndMain :=
"let wrapper (msg : msg_coq)(st : ((timestamp * (tez * address)) * ((address,tez) map * bool))) = match receive msg st (Current.time (), (Current.sender (), (Current.amount (), Current.balance ()))) with
| Some v -> v| None -> failwith ()
let%entry main (msg : msg_coq)(st : ((timestamp * (tez * address)) * ((address,tez) map * bool))) = wrapper msg st".
Time Run TemplateProgram
(
(* storage_def <- tmQuoteConstant "storage" false ;; *)
(* storage_body <- opt_to_template storage_def.(cst_body) ;; *)
ind <- tmQuoteInductive "msg_coq" ;;
ind_liq <- print_one_ind_body TT ind.(ind_bodies);;
t1 <- toLiquidity TT update_contribs ;;
t2 <- toLiquidity TT maybe_bind_unit ;;
t3 <- toLiquidity TT set_done ;;
t4 <- toLiquidity TT validate ;;
t5 <- toLiquidity TT receive ;;
res <- tmEval lazy
(LiquidityPrelude
++ nl ++ nl
++ "type storage = ((timestamp * (tez * address)) * ((address,tez) map * bool))"
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ t4
++ nl ++ nl
++ t5
++ nl ++ nl
++ printWrapperAndMain ) ;;
tmDefinition "crowdfunding_extracted" res).
Print crowdfunding_extracted.
......@@ -20,6 +20,16 @@ Import MonadNotation.
Definition my_lookup (m : FMap string Z) (k : string) := FMap.find k m.
Quote Definition yy := (stdpp.gmap.gmap).
Quote Recursively Definition z := (FMap.find).
Run TemplateProgram
(let ind_name := "stdpp.gmap.gmap" in
gmap_ <- tmQuoteInductive ind_name ;;
t <- toLiquidityEnv [] ((ind_name, InductiveDecl gmap_) :: z.1) my_lookup;;
code <- tmEval lazy t;;
tmPrint code).
(* Quoting this runs forever *)
(* Quote Recursively Definition zz := (my_lookup). *)
......@@ -122,6 +132,7 @@ Definition TT : env string :=
; local <% andb %>
(* local types *)
; local <% storage %>
; local <% value %>
; local <% op %>
].
......
......@@ -36,24 +36,26 @@ Module CrowdfundingContract.
"tx_amount"; "bal"; "sender"; "sent_by"; "own"; "isdone" ;
"accs"; "now"; "newstate"; "newmap"; "cond" ] "").
Notation "'Result'" := [!"prod" ("list" "SimpleActionBody") {full_state_ty} !]
(in custom type at level 2).
(** ** AST of the validation function *)
Module Validate.
Import Notations.
Definition maybe_bind_unit_syn :=
[| \\"B" => \"o" : Maybe Unit => \"b" : Maybe '"B" =>
case "o" : Maybe Unit return Maybe '"B" of
[| \"o" : Maybe Unit => \"b" : Maybe Result =>
case "o" : Maybe Unit return Maybe Result of
| Just "_" -> "b"
| Nothing -> $Nothing$Maybe [: '"B" ] |].
| Nothing -> $Nothing$Maybe [: Result ] |].
Make Definition maybe_bind_unit :=
(expr_to_tc Σ' (indexify nil maybe_bind_unit_syn)).
Notation "a >> b : B" :=
[| {eConst "maybe_bind_unit"} [: {B} ] {a} {b}|]
Notation "a >> b" :=
[| {eConst "maybe_bind_unit"} {a} {b}|]
(in custom expr at level 0,
B custom type at level 1,
a custom expr,
b custom expr).
......@@ -110,9 +112,6 @@ Module CrowdfundingContract.
Definition actions_ty := [! "list" "SimpleActionBody" !].
Notation "'Result'" := [!"prod" ("list" "SimpleActionBody") {full_state_ty} !]
(in custom type at level 2).
Notation "'Transfer' a b" :=
[| {eConstr SActionBody "Act_transfer"} {b} {a} |]
(in custom expr at level 0,
......@@ -173,7 +172,7 @@ Module CrowdfundingContract.
case m : msg return Maybe Result of
| GetFunds ->
if (own ==a sender) && (deadline s <t now) && (goal s <= bal) then
(VALIDATE tx_amount) >> (#Just (#Pair [Transfer bal sender] (DONE s))) : Result
(VALIDATE tx_amount) >> (#Just (#Pair [Transfer bal sender] (DONE s)))
else #Nothing : Maybe Result
| Donate ->
if now <=t deadline s then
......@@ -189,7 +188,7 @@ Module CrowdfundingContract.
if (deadline s <t now) && (bal < goal s) && (~ done s) then
(case (findm sender accs) : Maybe money return Maybe Result of
| Just v -> let newmap : Map := madd sender 0z accs in
(VALIDATE tx_amount) >> (#Just (#Pair [Transfer v sender] (UPDATE_CONTRIBS s newmap))) : Result
(VALIDATE tx_amount) >> (#Just (#Pair [Transfer v sender] (UPDATE_CONTRIBS s newmap)))
| Nothing -> #Nothing)
else #Nothing : Maybe Result
|].
......@@ -246,10 +245,11 @@ Definition CFModule : LiquidityModule :=
(** A translation table for types *)
Definition TTty : env string :=
[("Coq.Numbers.BinNums.Z", "tez");
("time_coq", "timestamp");
("address_coq", "address");
("addr_map", "(address,tez) map");
("Coq.Init.Datatypes.nat", "nat")].
("time_coq", "timestamp");
("address_coq", "address");
("addr_map", "(address,tez) map");
("Coq.Init.Datatypes.nat", "nat");
("SimpleActionBody", "operation")].
(** A translation table for primitive binary operations *)
Definition TT : env string :=
......
......@@ -44,18 +44,24 @@ Program Definition erase_and_print_template_program {cf : checker_flags}
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error Σ' e ++ ", while checking " ++ id)
end.
Definition print_template_program (TT : env string)
(checked_t : EnvCheck (EAst.global_context × EAst.term))
Definition print_EnvCheck {A}
(f : E.global_context -> A -> string)
(checked_t : EnvCheck (E.global_context * A))
: string + string :=
match checked_t return string + string with
| CorrectDecl (Σ', t) =>
inl (LPretty.print_term Σ' [] TT [] true false t)
inl (f Σ' t)
| EnvError Σ' (AlreadyDeclared id) =>
inr ("Already declared: " ++ id)
| EnvError Σ' (IllFormedDecl id e) =>
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error Σ' e ++ ", while checking " ++ id)
end.
Definition print_template_program (TT : env string)
(checked_t : EnvCheck (EAst.global_context × EAst.term))
: string + string :=
print_EnvCheck (fun Σ t => LPretty.print_term Σ [] TT [] true false t) checked_t.
Program Definition check_applied (p : Ast.program)
: EnvCheck bool :=
let p := fix_program_universes p in
......@@ -111,8 +117,8 @@ Definition erase_print_deboxed_all_applied (TT : env string) (p : Ast.program) :
print_sum (print_template_program TT deboxed).
Program Definition erase_check_debox_all_print (TT : env string) (p : Ast.program)
: string :=
Program Definition erase_check_debox_all (TT : env string) (p : Ast.program)
: EnvCheck (EAst.global_context × (list E.aname * E.term)) :=
let p := fix_program_universes p in
let res : EnvCheck ((EAst.global_context × bool) × EAst.term):=
'(Σ,t) <- erase_template_program p ;;
......@@ -124,12 +130,34 @@ Program Definition erase_check_debox_all_print (TT : env string) (p : Ast.progra
let '(Σ,is_ok, t) := g in
if is_ok : bool then
let deboxed := debox_top_level (debox_all t) in
print_sum (print_template_program TT (CorrectDecl (Σ, deboxed)))
else "Not all constructors or constants are appropriately applied"
| EnvError Σ' err => print_sum (print_template_program TT (EnvError Σ' err))
CorrectDecl (Σ, Edecompose_lam deboxed)
else
let err_msg := "Not all constructors or constants are appropriately applied" in
EnvError (P.empty_ext [])
(IllFormedDecl err_msg (Msg err_msg))
| EnvError Σ' err => EnvError Σ' err
end.
Definition print_decl (decl_name : string) (TT : env string) (tys : list Ast.term)
(Σ : E.global_context) (decl_body : list E.aname * E.term) : string :=
let (args,body) := decl_body in
(* FIXME: this will produce wrong type annotations if the logical argument
appears between the normal arguments! We need to switch to erased types and filter out the boxes in types *)
let targs := combine args tys in
let printed_targs :=
map (fun '(x,ty) => parens false (string_of_name x.(E.binder_name) ++ " : " ++ print_liq_type TT ty)) targs in
let decl := decl_name ++ " " ++ concat " " printed_targs in
let ctx := map (fun x => E.Build_context_decl x.(E.binder_name) None) (rev args) in
"let " ++ decl ++ " = " ++ LPretty.print_term Σ [] TT ctx true false body.
Program Definition erase_check_debox_all_print (TT : env string) (decl_name : string)
(tys : list Ast.term) (p : Ast.program)
: string :=
let p := fix_program_universes p in
let deboxed := erase_check_debox_all TT p in
print_sum (print_EnvCheck (print_decl decl_name TT tys) deboxed).
Notation "'unfolded' d" :=
ltac:(let y := eval unfold d in d in exact y) (at level 100, only parsing).
......@@ -168,6 +196,15 @@ Definition toDefWithEnv {A} (p : A) :=
cbody <- opt_to_template cbody_o.(cst_body) ;;
ret (mkLiqDef nm cbody_o.(cst_type) cbody, t.1).
Definition toDef {A} (p : A) :=
t <- tmQuote p ;;
nm <- opt_to_template (to_name t) ;;
cbody_o <- tmQuoteConstant nm false ;;
cbody <- opt_to_template cbody_o.(cst_body) ;;
ret (mkLiqDef nm cbody_o.(cst_type) cbody).
Definition toLiquidityWithBoxes {A} (TT : env string) (p : A) :=
d_e <- toDefWithEnv p ;;
let '(liq_def, env) := d_e in
......@@ -175,13 +212,25 @@ Definition toLiquidityWithBoxes {A} (TT : env string) (p : A) :=
let liq_def_string := "let " ++ unqual_name liq_def.(ld_name) ++ " = " ++ liq_prog in
ret liq_def_string.
About decompose_prod.
Definition toLiquidity {A} (TT : env string) (p : A) :=
d_e <- toDefWithEnv p ;;
let '(liq_def, env) := d_e in
liq_prog <- tmEval lazy (erase_check_debox_all_print TT (env,liq_def.(ld_body))) ;;
let liq_def_string := "let " ++ unqual_name liq_def.(ld_name) ++ " = " ++ liq_prog in
ret liq_def_string.
let decl_name := unqual_name liq_def.(ld_name) in
(* FIXME: we should use erasure for types here *)
let '(_,tys,_) := decompose_prod liq_def.(ld_type) in
tmEval lazy
(erase_check_debox_all_print TT decl_name tys (env,liq_def.(ld_body))).
Definition toLiquidityEnv {A} (TT : env string) (Σ : TemplateEnvironment.global_env)(p : A) :=
d <- toDef p ;;
let decl_name := unqual_name d.(ld_name) in
(* FIXME: we should use erasure for types here *)
let '(_,tys,_) := decompose_prod d.(ld_type) in
tmEval lazy
(erase_check_debox_all_print TT decl_name tys (Σ,d.(ld_body))).
Definition print_one_ind_body (TT : env string) (oibs : list one_inductive_body) :=
match oibs with
......
......@@ -11,7 +11,9 @@ Another issue (mostly solved): constructors accept only one argument, so we have
Pattern-macthing: pattern-matching on pairs is not supported by Liquidity, so all the programs must use projections.
Records are currently not supported. Should be represented as iterated products. *)
Records are currently not supported. Should be represented as iterated products.
Printing polymoprhic definitions is not supported currently (due to the need of removing redundant types from the type scheme). But the machinery is there, just need to switch to erased types. *)
From Coq Require Import List Program String Ascii.
From ConCert Require Import MyEnv Ast.
......@@ -68,14 +70,11 @@ Section print_term.
let error := "Error (not_supported_type " ++ Pretty.print_term (Ast.empty_ext []) [] true t ++ ")" in
match t with
| Ast.tInd ind _ =>
match look TT ind.(inductive_mind) with
| Some nm => nm
| None => ind.(inductive_mind)
end
from_option (look TT ind.(inductive_mind)) ind.(inductive_mind)
| Ast.tApp (Ast.tInd ind _) [t1;t2] =>
(* a special case of products - infix *)
if (Ast.from_option (to_name <% prod %>) "" =? ind.(inductive_mind))%string then
print_liq_type TT t1 ++ " * " ++ print_liq_type TT t2
parens false (print_liq_type TT t1 ++ " * " ++ print_liq_type TT t2)
else error
| Ast.tApp (Ast.tInd ind i) args =>
(* the usual - postfix - case of an applied type constructor *)
......@@ -87,6 +86,7 @@ Section print_term.
let nm := from_option (look TT nm) nm in
let printed_args := map (print_liq_type TT) args in
(print_uncurried "" printed_args) ++ " " ++ nm
| Ast.tConst nm _ => from_option (look TT nm) nm
| _ => "Error (not_supported_type " ++ Pretty.print_term (Ast.empty_ext []) [] true t ++ ")"
end.
......@@ -125,8 +125,8 @@ Section print_term.
Definition print_def (f : context -> term -> string) (def : def term) :=
let (args, _) := Edecompose_lam (dbody def) in
let ctx := rev (map (vass binder_name) args) in
let sargs := concat " ," (map (fun x => string_of_name x.(binder_name)) args) in
string_of_name (dname def) ++ parens false sargs ++ " = "
let sargs := print_uncurried "" (map (fun x => string_of_name x.(binder_name)) args) in
string_of_name (dname def) ++ " " ++ sargs ++ " = "
++ nl ++ f ctx (lam_body (dbody def)).
Definition print_defs (print_term : list string -> context -> bool -> bool -> term -> string) (FT : list string) (Γ : context) (defs : mfixpoint term) :=
......@@ -274,6 +274,15 @@ Section print_term.
let print_parens := (Nat.ltb 1 (List.length pt.1)) in
print_uncurried ctor_nm (rev pt.1) ++ " -> " ++ pt.2.
Definition print_transfer (args : list string) :=
match args with
| [] => "MalformedTransfer()"
| [a1;a2] => "Contract.call " ++ a1 ++ " " ++ a2 ++ " "
++ "default" ++ " ()"
| _ => "MalformedTransfer(" ++ concat "," args ++ ")"
end.
(** ** The pretty-printer *)
(** [FT] - list of fixpoint names. Used to determine if uncurrying is needed for the applied variable (if it corresponds to a recursive call).
......@@ -316,10 +325,13 @@ Section print_term.
(* is it a pair ? *)
if (nm =? "pair") then print_uncurried "" apps
else
(* is it a cons ? *)
(* is it a cons ? *)
if (nm =? "cons") then
parens top (concat " :: " apps)
else parens top (print_uncurried nm apps)
else
(* is it a transfer *)
if (nm =? "Act_transfer") then print_transfer apps
else parens top (print_uncurried nm apps)
| None => parens (top || inapp) (print_term FT TT Γ false true f ++ " " ++ print_term FT TT Γ false false l)
end
| tConst c =>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment