Contents:
Library ConCert.Extraction.CameLIGOExtract
From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import ZArith_base.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require ResultMonad.
From ConCert.Extraction Require Import CameLIGOPretty.
From ConCert.Extraction Require Import Common.
From ConCert.Extraction Require Import SpecializeChainBase.
From MetaCoq.Erasure.Typed Require Import CertifyingInlining.
From MetaCoq.Erasure.Typed Require Import ResultMonad.
From MetaCoq.Erasure.Typed Require Import ExAst.
From MetaCoq.Erasure.Typed Require Import Optimize.
From MetaCoq.Erasure.Typed Require Import Extraction.
From MetaCoq.Erasure.Typed Require Import TypeAnnotations.
From MetaCoq.Erasure.Typed Require Import Annotations.
From MetaCoq.Erasure.Typed Require Import Utils.
From ConCert.Utils Require Import Env.
From MetaCoq.Utils Require Import monad_utils.
From MetaCoq.Utils Require Import MCSquash.
From MetaCoq.Utils Require Import MCPrelude.
From MetaCoq.Utils Require Import MCProd.
From MetaCoq.Common Require Import Kernames.
From MetaCoq.Template Require Import TemplateMonad.
Import MCMonadNotation ListNotations.
Record CameLIGOMod {Base : ChainBase} (msg ctx setup storage operation error : Type) :=
{ lmd_module_name : string ;
lmd_prelude : string ;
lmd_init : setup -> ConCert.Execution.ResultMonad.result storage error;
lmd_init_prelude : string ;
lmd_receive_prelude : string;
lmd_receive : Chain -> ctx -> storage -> option msg -> ConCert.Execution.ResultMonad.result (list operation * storage) error;
lmd_entry_point : string }.
Arguments lmd_module_name {_ _ _ _ _ _ _}.
Arguments lmd_prelude {_ _ _ _ _ _ _}.
Arguments lmd_init {_ _ _ _ _ _ _}.
Arguments lmd_init_prelude {_ _ _ _ _ _ _}.
Arguments lmd_receive {_ _ _ _ _ _ _}.
Arguments lmd_receive_prelude {_ _ _ _ _ _ _}.
Arguments lmd_entry_point {_ _ _ _ _ _ _}.
(* We override masks for *some* constants that have only logical parameters, like
@AddressMap.empty. Our optimization conservatively keeps one parameter
if all the parameters are logical. This is necessary because such definitions
might use something like false_rect and removing all the arguments will force
evaluating their bodies, which can lead to an exception or looping depending
on how the elimination from the empty types is implemented.
However, for AddressMap.empty is completely safe to remove all arguments,
since it's an abbreviation for a constructor. *)
Definition overridden_masks (kn : kername) : option bitmask :=
if eq_kername kn <%% @AddressMap.empty %%> then Some [true]
else None.
Definition cameligo_args :=
{| optimize_prop_discr := true;
extract_transforms := [Optimize.dearg_transform
overridden_masks
true
false (* cannot have partially applied ctors *)
true
true
true] |}.
Import PCUICAst PCUICTyping.
Import bytestring.
Definition annot_extract_env_cameligo
(Σ : PCUICEnvironment.global_env)
(wfΣ : ∥wf Σ∥)
(include : KernameSet.t)
(ignore : list kername) : result (∑ Σ, env_annots box_type Σ) string.
Proof.
(* set (extract_cameligo_params inline) as params. *)
set (fun kn => existsb (eq_kername kn) ignore) as to_ignore.
unshelve epose proof (annot_extract_pcuic_env cameligo_args Σ wfΣ include to_ignore _).
- subst; cbn; constructor; [|constructor].
apply annot_dearg_transform.
- destruct extract_pcuic_env.
* exact (Ok (t; X)).
* exact (Err e).
Defined.
Definition blah : Monad (fun A => result A string) := _.
Program Definition annot_extract_template_env_specalize
(e : Ast.Env.global_env)
(seeds : KernameSet.t)
(ignore : list kername) : result_string (∑ e, env_annots box_type e) :=
let e := TemplateToPCUIC.trans_global_env e in
e <- specialize_ChainBase_env (PCUICProgram.trans_env_env e) ;;
wfe <-check_wf_env_func extract_within_coq e;;
annot_extract_env_cameligo e wfe seeds ignore.
Definition CameLIGO_ignore_default {Base : ChainBase} :=
[
<%% prod %%>
; <%% @ChainBase %%>
; <%% axiomatized_ChainBase %%>
; <%% Amount %%>
; <%% @Address %%>
; <%% @address_eqdec %%>
; <%% @address_countable %%>
; <%% @ContractCallContext %%>
; <%% @SerializedValue %%>
; <%% @SerializedType %%>
; <%% chain_height %%>
; <%% current_slot %%>
; <%% finalized_height %%>
].
Open Scope string.
Definition TT_remap_default : list (kername * String.string) :=
[
(* types *)
remap <%% Z %%> "tez"
(* NOTE: subtracting two nats gives int, so we remap N to int
and use truncated subtraction *)
(* TODO: this doesn't look right. N should be nat in CameLIGO and Z should be
int. However, Z is also used as the type of currency, that could lead to clashes
in the extracted code. *)
; remap <%% N %%> "int"
; remap <%% nat %%> "nat"
; remap <%% bool %%> "bool"
; remap <%% unit %%> "unit"
; remap <%% list %%> "list"
; remap <%% @fst %%> "fst"
; remap <%% @snd %%> "snd"
; remap <%% option %%> "option"
; remap <%% ConCert.Execution.ResultMonad.result %%> "result"
; remap <%% gmap.gmap %%> "map"
; remap <%% positive %%> "nat"
; remap <%% Amount %%> "tez"
; remap <%% @Address %%> "address"
; remap <%% @ActionBody %%> "operation"
; remap <%% @ContractCallContext %%> CameLIGO_call_ctx_type_name
(* operations on numbers and currency tez *)
; remap <%% Nat.add %%> "addN"
; remap <%% Nat.leb %%> "lebN"
; remap <%% Nat.ltb %%> "ltbN"
; remap <%% Nat.mul %%> "multN"
; remap <%% Pos.add %%> "addN"
; remap <%% Pos.sub %%> "subN"
; remap <%% Pos.mul %%> "multN"
; remap <%% Pos.leb %%> "leN"
; remap <%% Pos.eqb %%> "eqN"
; remap <%% Z.add %%> "addTez"
(* TODO: subtraction of tez returns option in LIGO now We should
not use Z.sub directly, but a similar operation that returns
option Z instead. For now, it can be provided and remapped by
each contract, but ideally it should be in some central place. *)
(* ; remap <% Z.sub %> "subTez" *)
; remap <%% Z.mul %%> "multTez"
; remap <%% Z.div %%> "divTez"
; remap <%% Z.leb %%> "leTez"
; remap <%% Z.ltb %%> "ltTez"
; remap <%% Z.eqb %%> "eqTez"
; remap <%% Z.gtb %%> "gtbTez"
; remap <%% Z.even %%> "evenTez"
; remap <%% N.add %%> "addInt"
; remap <%% N.sub %%> "subIntTruncated"
; remap <%% N.leb %%> "leInt"
; remap <%% N.ltb %%> "ltInt"
; remap <%% N.eqb %%> "eqInt"
; remap <%% andb %%> "andb"
; remap <%% negb %%> "not"
; remap <%% orb %%> "orb"
(* address *)
; remap <%% @address_eqb %%> "eq_addr"
(* lists *)
; remap <%% @List.fold_left %%> "List.fold"
; remap <%% @List.map %%> "List.map"
; remap <%% @List.find %%> "List.find"
; remap <%% @List.length %%> "List.length"
; remap <%% @List.app %%> "List.append"
(* maps *)
; remap <%% @stdpp.base.insert %%> "Map.add"
; remap <%% @stdpp.base.lookup %%> "Map.find_opt"
; remap <%% @stdpp.base.empty %%> "Map.empty"
(* call context *)
; remap <%% @ctx_origin %%> "ctx_origin"
; remap <%% @ctx_from %%> "ctx_from"
; remap <%% @ctx_contract_address %%> "ctx_contract_address"
; remap <%% @ctx_contract_balance %%> "ctx_contract_balance"
; remap <%% @ctx_amount %%> "ctx_amount"
(* blockchain infrastructure *)
; remap <%% @ActionBody %%> "operation"
; remap <%% @Chain %%> "chain"
; remap <%% @chain_height %%> "chain_height"
; remap <%% @current_slot %%> "current_slot"
; remap <%% @finalized_height %%> "finalized_height"
].
Definition TT_rename_ctors_default : list (String.string * String.string) :=
[ ("nil", "[]")
; ("true", "true")
; ("false", "false")
; ("Some", "Some")
; ("None", "None")
; ("Ok", "Ok")
; ("Err", "Err")
; ("tt", "()")].
Definition wrap_in_delimiters s :=
Strings.String.concat Common.nl [""; s].
Definition is_empty {A} (xs : list A) :=
match xs with
| [] => true
| _ => false
end.
Section LigoExtract.
Context `{ChainBase}
`{CameLIGOPrintConfig}.
Open Scope list.
Notation "'bs_to_s' s" := (bytestring.String.to_string s) (at level 200).
Local Coercion bytestring.String.to_string : bytestring.String.t >-> String.string.
Definition printCameLIGODefs {msg ctx params storage operation error : Type}
(Σ : Ast.Env.global_env)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(init : kername)
(receive : kername)
(m : CameLIGOMod msg ctx params storage operation error)
: String.string + String.string :=
let init_prelude := m.(lmd_init_prelude) in
let entry_point := m.(lmd_entry_point) in
let seeds := KernameSet.union (KernameSet.singleton init) (KernameSet.singleton receive) in
let TT_defs := TT_defs ++ TT_remap_default in
let ignore := (map fst TT_defs ++ CameLIGO_ignore_default ++ extra_ignore)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
match annot_extract_template_env_specalize Σ seeds ignore with
| Ok (eΣ; annots) =>
(* dependencies should be printed before the dependent definitions *)
let ldef_list := List.rev (print_global_env TT eΣ annots) in
(* filtering empty strings corresponding to the ignored definitions *)
let not_empty_str := (negb ∘ (Strings.String.eqb "") ∘ snd) in
let ldef_ty_list := ldef_list
|> filter (fun d => match d with TyDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let ldef_const_list := ldef_list
|> filter (fun d => match d with ConstDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
(* look for init function *)
match bigprod_find (fun '(k, _, _) _ => eq_kername k init) annots with
| Some ((_, ExAst.ConstantDecl init_cst); annots) =>
match print_init TT build_call_ctx init_prelude eΣ init_cst annots with
| Some init_code =>
(* filtering out the definition of init and projecting the code *)
(* and place init prelude after type decls and before constant decls *)
let defs : list String.string :=
ldef_const_list |> filter (negb ∘ (eq_kername init) ∘ fst)
|> map snd
|> List.app (map snd ldef_ty_list) (* append the above after ty decls*)
in
let res : String.string :=
Strings.String.concat (Common.nl ++ Common.nl) (defs ++ (cons init_code nil)) in
(wrap_in_delimiters (Strings.String.concat (Common.nl ++ Common.nl) [m.(lmd_prelude); res; entry_point])) |> inl
| None => inr "Error: Empty body for init"
end
| Some _ => inr "Error: init must be a constant"
| None => inr "Error: No init found"
end
| Err e => inr (bs_to_s e)
end.
Definition unwrap_string_sum (s : String.string + String.string) : String.string :=
match s with
| inl v => v
| inr v => v
end.
Open Scope bs_scope.
From Coq Require Import List.
From Coq Require Import ZArith_base.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require ResultMonad.
From ConCert.Extraction Require Import CameLIGOPretty.
From ConCert.Extraction Require Import Common.
From ConCert.Extraction Require Import SpecializeChainBase.
From MetaCoq.Erasure.Typed Require Import CertifyingInlining.
From MetaCoq.Erasure.Typed Require Import ResultMonad.
From MetaCoq.Erasure.Typed Require Import ExAst.
From MetaCoq.Erasure.Typed Require Import Optimize.
From MetaCoq.Erasure.Typed Require Import Extraction.
From MetaCoq.Erasure.Typed Require Import TypeAnnotations.
From MetaCoq.Erasure.Typed Require Import Annotations.
From MetaCoq.Erasure.Typed Require Import Utils.
From ConCert.Utils Require Import Env.
From MetaCoq.Utils Require Import monad_utils.
From MetaCoq.Utils Require Import MCSquash.
From MetaCoq.Utils Require Import MCPrelude.
From MetaCoq.Utils Require Import MCProd.
From MetaCoq.Common Require Import Kernames.
From MetaCoq.Template Require Import TemplateMonad.
Import MCMonadNotation ListNotations.
Record CameLIGOMod {Base : ChainBase} (msg ctx setup storage operation error : Type) :=
{ lmd_module_name : string ;
lmd_prelude : string ;
lmd_init : setup -> ConCert.Execution.ResultMonad.result storage error;
lmd_init_prelude : string ;
lmd_receive_prelude : string;
lmd_receive : Chain -> ctx -> storage -> option msg -> ConCert.Execution.ResultMonad.result (list operation * storage) error;
lmd_entry_point : string }.
Arguments lmd_module_name {_ _ _ _ _ _ _}.
Arguments lmd_prelude {_ _ _ _ _ _ _}.
Arguments lmd_init {_ _ _ _ _ _ _}.
Arguments lmd_init_prelude {_ _ _ _ _ _ _}.
Arguments lmd_receive {_ _ _ _ _ _ _}.
Arguments lmd_receive_prelude {_ _ _ _ _ _ _}.
Arguments lmd_entry_point {_ _ _ _ _ _ _}.
(* We override masks for *some* constants that have only logical parameters, like
@AddressMap.empty. Our optimization conservatively keeps one parameter
if all the parameters are logical. This is necessary because such definitions
might use something like false_rect and removing all the arguments will force
evaluating their bodies, which can lead to an exception or looping depending
on how the elimination from the empty types is implemented.
However, for AddressMap.empty is completely safe to remove all arguments,
since it's an abbreviation for a constructor. *)
Definition overridden_masks (kn : kername) : option bitmask :=
if eq_kername kn <%% @AddressMap.empty %%> then Some [true]
else None.
Definition cameligo_args :=
{| optimize_prop_discr := true;
extract_transforms := [Optimize.dearg_transform
overridden_masks
true
false (* cannot have partially applied ctors *)
true
true
true] |}.
Import PCUICAst PCUICTyping.
Import bytestring.
Definition annot_extract_env_cameligo
(Σ : PCUICEnvironment.global_env)
(wfΣ : ∥wf Σ∥)
(include : KernameSet.t)
(ignore : list kername) : result (∑ Σ, env_annots box_type Σ) string.
Proof.
(* set (extract_cameligo_params inline) as params. *)
set (fun kn => existsb (eq_kername kn) ignore) as to_ignore.
unshelve epose proof (annot_extract_pcuic_env cameligo_args Σ wfΣ include to_ignore _).
- subst; cbn; constructor; [|constructor].
apply annot_dearg_transform.
- destruct extract_pcuic_env.
* exact (Ok (t; X)).
* exact (Err e).
Defined.
Definition blah : Monad (fun A => result A string) := _.
Program Definition annot_extract_template_env_specalize
(e : Ast.Env.global_env)
(seeds : KernameSet.t)
(ignore : list kername) : result_string (∑ e, env_annots box_type e) :=
let e := TemplateToPCUIC.trans_global_env e in
e <- specialize_ChainBase_env (PCUICProgram.trans_env_env e) ;;
wfe <-check_wf_env_func extract_within_coq e;;
annot_extract_env_cameligo e wfe seeds ignore.
Definition CameLIGO_ignore_default {Base : ChainBase} :=
[
<%% prod %%>
; <%% @ChainBase %%>
; <%% axiomatized_ChainBase %%>
; <%% Amount %%>
; <%% @Address %%>
; <%% @address_eqdec %%>
; <%% @address_countable %%>
; <%% @ContractCallContext %%>
; <%% @SerializedValue %%>
; <%% @SerializedType %%>
; <%% chain_height %%>
; <%% current_slot %%>
; <%% finalized_height %%>
].
Open Scope string.
Definition TT_remap_default : list (kername * String.string) :=
[
(* types *)
remap <%% Z %%> "tez"
(* NOTE: subtracting two nats gives int, so we remap N to int
and use truncated subtraction *)
(* TODO: this doesn't look right. N should be nat in CameLIGO and Z should be
int. However, Z is also used as the type of currency, that could lead to clashes
in the extracted code. *)
; remap <%% N %%> "int"
; remap <%% nat %%> "nat"
; remap <%% bool %%> "bool"
; remap <%% unit %%> "unit"
; remap <%% list %%> "list"
; remap <%% @fst %%> "fst"
; remap <%% @snd %%> "snd"
; remap <%% option %%> "option"
; remap <%% ConCert.Execution.ResultMonad.result %%> "result"
; remap <%% gmap.gmap %%> "map"
; remap <%% positive %%> "nat"
; remap <%% Amount %%> "tez"
; remap <%% @Address %%> "address"
; remap <%% @ActionBody %%> "operation"
; remap <%% @ContractCallContext %%> CameLIGO_call_ctx_type_name
(* operations on numbers and currency tez *)
; remap <%% Nat.add %%> "addN"
; remap <%% Nat.leb %%> "lebN"
; remap <%% Nat.ltb %%> "ltbN"
; remap <%% Nat.mul %%> "multN"
; remap <%% Pos.add %%> "addN"
; remap <%% Pos.sub %%> "subN"
; remap <%% Pos.mul %%> "multN"
; remap <%% Pos.leb %%> "leN"
; remap <%% Pos.eqb %%> "eqN"
; remap <%% Z.add %%> "addTez"
(* TODO: subtraction of tez returns option in LIGO now We should
not use Z.sub directly, but a similar operation that returns
option Z instead. For now, it can be provided and remapped by
each contract, but ideally it should be in some central place. *)
(* ; remap <% Z.sub %> "subTez" *)
; remap <%% Z.mul %%> "multTez"
; remap <%% Z.div %%> "divTez"
; remap <%% Z.leb %%> "leTez"
; remap <%% Z.ltb %%> "ltTez"
; remap <%% Z.eqb %%> "eqTez"
; remap <%% Z.gtb %%> "gtbTez"
; remap <%% Z.even %%> "evenTez"
; remap <%% N.add %%> "addInt"
; remap <%% N.sub %%> "subIntTruncated"
; remap <%% N.leb %%> "leInt"
; remap <%% N.ltb %%> "ltInt"
; remap <%% N.eqb %%> "eqInt"
; remap <%% andb %%> "andb"
; remap <%% negb %%> "not"
; remap <%% orb %%> "orb"
(* address *)
; remap <%% @address_eqb %%> "eq_addr"
(* lists *)
; remap <%% @List.fold_left %%> "List.fold"
; remap <%% @List.map %%> "List.map"
; remap <%% @List.find %%> "List.find"
; remap <%% @List.length %%> "List.length"
; remap <%% @List.app %%> "List.append"
(* maps *)
; remap <%% @stdpp.base.insert %%> "Map.add"
; remap <%% @stdpp.base.lookup %%> "Map.find_opt"
; remap <%% @stdpp.base.empty %%> "Map.empty"
(* call context *)
; remap <%% @ctx_origin %%> "ctx_origin"
; remap <%% @ctx_from %%> "ctx_from"
; remap <%% @ctx_contract_address %%> "ctx_contract_address"
; remap <%% @ctx_contract_balance %%> "ctx_contract_balance"
; remap <%% @ctx_amount %%> "ctx_amount"
(* blockchain infrastructure *)
; remap <%% @ActionBody %%> "operation"
; remap <%% @Chain %%> "chain"
; remap <%% @chain_height %%> "chain_height"
; remap <%% @current_slot %%> "current_slot"
; remap <%% @finalized_height %%> "finalized_height"
].
Definition TT_rename_ctors_default : list (String.string * String.string) :=
[ ("nil", "[]")
; ("true", "true")
; ("false", "false")
; ("Some", "Some")
; ("None", "None")
; ("Ok", "Ok")
; ("Err", "Err")
; ("tt", "()")].
Definition wrap_in_delimiters s :=
Strings.String.concat Common.nl [""; s].
Definition is_empty {A} (xs : list A) :=
match xs with
| [] => true
| _ => false
end.
Section LigoExtract.
Context `{ChainBase}
`{CameLIGOPrintConfig}.
Open Scope list.
Notation "'bs_to_s' s" := (bytestring.String.to_string s) (at level 200).
Local Coercion bytestring.String.to_string : bytestring.String.t >-> String.string.
Definition printCameLIGODefs {msg ctx params storage operation error : Type}
(Σ : Ast.Env.global_env)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(init : kername)
(receive : kername)
(m : CameLIGOMod msg ctx params storage operation error)
: String.string + String.string :=
let init_prelude := m.(lmd_init_prelude) in
let entry_point := m.(lmd_entry_point) in
let seeds := KernameSet.union (KernameSet.singleton init) (KernameSet.singleton receive) in
let TT_defs := TT_defs ++ TT_remap_default in
let ignore := (map fst TT_defs ++ CameLIGO_ignore_default ++ extra_ignore)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
match annot_extract_template_env_specalize Σ seeds ignore with
| Ok (eΣ; annots) =>
(* dependencies should be printed before the dependent definitions *)
let ldef_list := List.rev (print_global_env TT eΣ annots) in
(* filtering empty strings corresponding to the ignored definitions *)
let not_empty_str := (negb ∘ (Strings.String.eqb "") ∘ snd) in
let ldef_ty_list := ldef_list
|> filter (fun d => match d with TyDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let ldef_const_list := ldef_list
|> filter (fun d => match d with ConstDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
(* look for init function *)
match bigprod_find (fun '(k, _, _) _ => eq_kername k init) annots with
| Some ((_, ExAst.ConstantDecl init_cst); annots) =>
match print_init TT build_call_ctx init_prelude eΣ init_cst annots with
| Some init_code =>
(* filtering out the definition of init and projecting the code *)
(* and place init prelude after type decls and before constant decls *)
let defs : list String.string :=
ldef_const_list |> filter (negb ∘ (eq_kername init) ∘ fst)
|> map snd
|> List.app (map snd ldef_ty_list) (* append the above after ty decls*)
in
let res : String.string :=
Strings.String.concat (Common.nl ++ Common.nl) (defs ++ (cons init_code nil)) in
(wrap_in_delimiters (Strings.String.concat (Common.nl ++ Common.nl) [m.(lmd_prelude); res; entry_point])) |> inl
| None => inr "Error: Empty body for init"
end
| Some _ => inr "Error: init must be a constant"
| None => inr "Error: No init found"
end
| Err e => inr (bs_to_s e)
end.
Definition unwrap_string_sum (s : String.string + String.string) : String.string :=
match s with
| inl v => v
| inr v => v
end.
Open Scope bs_scope.
A flag that controls whether info about universes is preserved after quoting
Definition WITH_UNIVERSES := false.
Definition quote_and_preprocess {Base : ChainBase}
{msg ctx params storage operation error : Type}
(inline : list kername)
(m : CameLIGOMod msg ctx params storage operation error)
: TemplateMonad (Ast.Env.global_env * kername * kername) :=
(* we compute with projections before quoting to
avoid unnecessary dependencies to be quoted *)
init <- tmEval cbn m.(lmd_init);;
receive <-tmEval cbn m.(lmd_receive);;
'(Σ,_) <- tmQuoteRecTransp (init,receive) false ;;
init_nm <- extract_def_name m.(lmd_init);;
receive_nm <- extract_def_name m.(lmd_receive);;
decls <-
(if is_empty inline then ret (Ast.Env.declarations Σ)
else
let decls := Ast.Env.declarations Σ in
let to_inline kn := existsb (eq_kername kn) inline in
Σcert <- tmEval lazy (inline_globals to_inline decls) ;;
mpath <- tmCurrentModPath tt;;
Certifying.gen_defs_and_proofs decls Σcert mpath "_cert_pass"
(KernameSetProp.of_list [init_nm; receive_nm]);;
ret Σcert);;
Σret <- tmEval lazy (if WITH_UNIVERSES then
Ast.Env.mk_global_env (Ast.Env.universes Σ) decls (Ast.Env.retroknowledge Σ)
else
Ast.Env.mk_global_env (ContextSet.empty) decls (Ast.Env.retroknowledge Σ));;
ret (Σret, init_nm,receive_nm).
Definition quote_and_preprocess {Base : ChainBase}
{msg ctx params storage operation error : Type}
(inline : list kername)
(m : CameLIGOMod msg ctx params storage operation error)
: TemplateMonad (Ast.Env.global_env * kername * kername) :=
(* we compute with projections before quoting to
avoid unnecessary dependencies to be quoted *)
init <- tmEval cbn m.(lmd_init);;
receive <-tmEval cbn m.(lmd_receive);;
'(Σ,_) <- tmQuoteRecTransp (init,receive) false ;;
init_nm <- extract_def_name m.(lmd_init);;
receive_nm <- extract_def_name m.(lmd_receive);;
decls <-
(if is_empty inline then ret (Ast.Env.declarations Σ)
else
let decls := Ast.Env.declarations Σ in
let to_inline kn := existsb (eq_kername kn) inline in
Σcert <- tmEval lazy (inline_globals to_inline decls) ;;
mpath <- tmCurrentModPath tt;;
Certifying.gen_defs_and_proofs decls Σcert mpath "_cert_pass"
(KernameSetProp.of_list [init_nm; receive_nm]);;
ret Σcert);;
Σret <- tmEval lazy (if WITH_UNIVERSES then
Ast.Env.mk_global_env (Ast.Env.universes Σ) decls (Ast.Env.retroknowledge Σ)
else
Ast.Env.mk_global_env (ContextSet.empty) decls (Ast.Env.retroknowledge Σ));;
ret (Σret, init_nm,receive_nm).
Runs all the necessary steps in TemplateMonad and adds a definition
<module_name>_prepared to the Coq environment.
The definition consist of a call to erasure and pretty-printing for further
evaluation outside of TemplateMonad, using, e.g. Eval vm_compute in,
which is much faster than running the computations inside TemplateMonad.
Definition CameLIGO_prepare_extraction {msg ctx params storage operation error : Type}
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(m : CameLIGOMod msg ctx params storage operation error) :=
'(Σ, init_nm, receive_nm) <- quote_and_preprocess inline m;;
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
let res := unwrap_string_sum (printCameLIGODefs Σ TT_defs TT_ctors extra_ignore
build_call_ctx
init_nm receive_nm
m) in
tmDefinition (bytestring.String.of_string (m.(lmd_module_name) ^ "_prepared")) res.
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(m : CameLIGOMod msg ctx params storage operation error) :=
'(Σ, init_nm, receive_nm) <- quote_and_preprocess inline m;;
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
let res := unwrap_string_sum (printCameLIGODefs Σ TT_defs TT_ctors extra_ignore
build_call_ctx
init_nm receive_nm
m) in
tmDefinition (bytestring.String.of_string (m.(lmd_module_name) ^ "_prepared")) res.
Bundles together quoting, inlining, erasure and pretty-printing.
Convenient to use, but might be slow, because performance of tmEval lazy is not great.
Definition CameLIGO_extract {msg ctx params storage operation error : Type}
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(m : CameLIGOMod msg ctx params storage operation error)
: TemplateMonad String.string :=
'(Σ, init_nm, receive_nm) <- quote_and_preprocess inline m;;
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
p <- tmEval lazy
(printCameLIGODefs Σ TT_defs TT_ctors extra_ignore
build_call_ctx
init_nm receive_nm
m) ;;
match (p : String.string + String.string) with
| inl s =>
tmEval lazy
(wrap_in_delimiters (Strings.String.concat (Common.nl ++ Common.nl)
[m.(lmd_prelude); s; m.(lmd_entry_point)]))
| inr s => tmFail (bytestring.String.of_string s)
end.
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(extra_ignore : list kername)
(build_call_ctx : String.string)
(m : CameLIGOMod msg ctx params storage operation error)
: TemplateMonad String.string :=
'(Σ, init_nm, receive_nm) <- quote_and_preprocess inline m;;
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let TT :=
(TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
p <- tmEval lazy
(printCameLIGODefs Σ TT_defs TT_ctors extra_ignore
build_call_ctx
init_nm receive_nm
m) ;;
match (p : String.string + String.string) with
| inl s =>
tmEval lazy
(wrap_in_delimiters (Strings.String.concat (Common.nl ++ Common.nl)
[m.(lmd_prelude); s; m.(lmd_entry_point)]))
| inr s => tmFail (bytestring.String.of_string s)
end.
A simplified erasure/printing intended mostly for testing purposes
Definition simple_def_print `{ChainBase} TT_defs TT_ctors seeds (prelude harness : String.string) Σ
: String.string + String.string :=
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let ignore := (map fst TT_defs ++ CameLIGO_ignore_default)%list in
let TT := (TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
match annot_extract_template_env_specalize Σ seeds ignore with
| Ok annot_env =>
let '(eΣ; annots) := annot_env in
(* dependencies should be printed before the dependent definitions *)
let ldef_list := List.rev (print_global_env TT eΣ annots) in
(* filtering empty strings corresponding to the ignored definitions *)
let not_empty_str := (negb ∘ (Strings.String.eqb "") ∘ snd) in
let ldef_ty_list := ldef_list
|> filter (fun d => match d with TyDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let ldef_const_list := ldef_list
|> filter (fun d => match d with ConstDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let defs : list String.string :=
ldef_const_list |> map snd
|> List.app (map snd ldef_ty_list) in
Strings.String.concat (Common.nl ++ Common.nl) ((prelude :: defs ++ [harness]))%list |> inl
| Err e => inr (bs_to_s e)
end.
: String.string + String.string :=
let TT_defs := (TT_defs ++ TT_remap_default)%list in
let ignore := (map fst TT_defs ++ CameLIGO_ignore_default)%list in
let TT := (TT_ctors ++ map (fun '(kn,d) => (bs_to_s (string_of_kername kn), d)) TT_defs)%list in
match annot_extract_template_env_specalize Σ seeds ignore with
| Ok annot_env =>
let '(eΣ; annots) := annot_env in
(* dependencies should be printed before the dependent definitions *)
let ldef_list := List.rev (print_global_env TT eΣ annots) in
(* filtering empty strings corresponding to the ignored definitions *)
let not_empty_str := (negb ∘ (Strings.String.eqb "") ∘ snd) in
let ldef_ty_list := ldef_list
|> filter (fun d => match d with TyDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let ldef_const_list := ldef_list
|> filter (fun d => match d with ConstDecl _ => true | _ => false end)
|> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
|> filter not_empty_str in
let defs : list String.string :=
ldef_const_list |> map snd
|> List.app (map snd ldef_ty_list) in
Strings.String.concat (Common.nl ++ Common.nl) ((prelude :: defs ++ [harness]))%list |> inl
| Err e => inr (bs_to_s e)
end.
Quoting and inlining for a single definition.
Intended mostly for testing purposes
Definition quote_and_preprocess_one_def {A}
(inline : list kername)
(def : A)
: TemplateMonad (Ast.Env.global_env * kername) :=
'(Σ,_) <- tmQuoteRecTransp def false ;;
def_nm <- extract_def_name def;;
decls <-(if is_empty inline then ret (Ast.Env.declarations Σ)
else
let decls := Ast.Env.declarations Σ in
let to_inline kn := existsb (eq_kername kn) inline in
Σcert <- tmEval lazy (inline_globals to_inline decls) ;;
mpath <- tmCurrentModPath tt;;
Certifying.gen_defs_and_proofs decls Σcert mpath "_cert_pass"
(KernameSetProp.of_list [def_nm]);;
ret Σcert);;
Σret <- tmEval lazy (if WITH_UNIVERSES then
Ast.Env.mk_global_env (Ast.Env.universes Σ) decls (Ast.Env.retroknowledge Σ)
else
Ast.Env.mk_global_env (ContextSet.empty) decls (Ast.Env.retroknowledge Σ));;
ret (Σret, def_nm).
(inline : list kername)
(def : A)
: TemplateMonad (Ast.Env.global_env * kername) :=
'(Σ,_) <- tmQuoteRecTransp def false ;;
def_nm <- extract_def_name def;;
decls <-(if is_empty inline then ret (Ast.Env.declarations Σ)
else
let decls := Ast.Env.declarations Σ in
let to_inline kn := existsb (eq_kername kn) inline in
Σcert <- tmEval lazy (inline_globals to_inline decls) ;;
mpath <- tmCurrentModPath tt;;
Certifying.gen_defs_and_proofs decls Σcert mpath "_cert_pass"
(KernameSetProp.of_list [def_nm]);;
ret Σcert);;
Σret <- tmEval lazy (if WITH_UNIVERSES then
Ast.Env.mk_global_env (Ast.Env.universes Σ) decls (Ast.Env.retroknowledge Σ)
else
Ast.Env.mk_global_env (ContextSet.empty) decls (Ast.Env.retroknowledge Σ));;
ret (Σret, def_nm).
Extraction for testing purposes.
Simply prints the definitions and allows for appending a prelude and a
handwritten harness code to run the extracted definition.
The harness is just a piece of code with definitions
of storage, main, etc.
Definition CameLIGO_extract_single `{ChainBase} {A}
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(prelude : String.string)
(harness : String.string)
(def : A) : TemplateMonad String.string :=
'(Σ,def_nm) <- quote_and_preprocess_one_def inline def ;;
let seeds := KernameSetProp.of_list [def_nm] in
tmEval lazy (unwrap_string_sum (simple_def_print TT_defs TT_ctors (KernameSet.singleton def_nm) prelude harness Σ)).
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(prelude : String.string)
(harness : String.string)
(def : A) : TemplateMonad String.string :=
'(Σ,def_nm) <- quote_and_preprocess_one_def inline def ;;
let seeds := KernameSetProp.of_list [def_nm] in
tmEval lazy (unwrap_string_sum (simple_def_print TT_defs TT_ctors (KernameSet.singleton def_nm) prelude harness Σ)).
Similar to CameLIGO_prepare_extraction, but for a single definition
Definition CameLIGO_prepare_extraction_single `{ChainBase} {A}
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(prelude : String.string)
(harness : String.string)
(def : A) : TemplateMonad String.string :=
'(Σ,def_nm) <- quote_and_preprocess_one_def inline def ;;
let seeds := KernameSetProp.of_list [def_nm] in
tmDefinition (def_nm.2 ++ "_prepared") (unwrap_string_sum (simple_def_print TT_defs TT_ctors (KernameSet.singleton def_nm) prelude harness Σ)).
End LigoExtract.
(inline : list kername)
(TT_defs : list (kername * String.string))
(TT_ctors : env String.string)
(prelude : String.string)
(harness : String.string)
(def : A) : TemplateMonad String.string :=
'(Σ,def_nm) <- quote_and_preprocess_one_def inline def ;;
let seeds := KernameSetProp.of_list [def_nm] in
tmDefinition (def_nm.2 ++ "_prepared") (unwrap_string_sum (simple_def_print TT_defs TT_ctors (KernameSet.singleton def_nm) prelude harness Σ)).
End LigoExtract.