From acbfd8813d13a6bed9752c35f2576bd7376af392 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Thu, 22 Feb 2024 15:45:24 +0100 Subject: [PATCH] Fix strange bug --- engine/backends/coq/coq/coq_backend.ml | 10 +- engine/backends/coq/coq/dune | 2 +- engine/backends/coq/ssprove/dune | 3 +- .../backends/coq/ssprove/ssprove_backend.ml | 887 +++++++++--------- 4 files changed, 452 insertions(+), 450 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 1b08bafd5..53539d3c6 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -196,7 +196,8 @@ struct let rec ppat (p : pat) : C.AST.pat = match p.p with | PWild -> C.AST.WildPat - | PAscription { typ; pat; _ } -> C.AST.AscriptionPat (ppat pat, pty p.span typ) + | PAscription { typ; pat; _ } -> + C.AST.AscriptionPat (ppat pat, pty p.span typ) | PBinding { mut = Immutable; @@ -278,7 +279,7 @@ struct { f = { e = GlobalVar (`Projector (`TupleField _)); _ }; args = [ _ ]; - _ + _; } -> __TODO_term__ span "app global vcar projector tuple" | App { f = { e = GlobalVar x; _ }; args; _ } when Map.mem operators x -> @@ -323,7 +324,8 @@ struct C.AST.Match ( pexpr scrutinee, List.map - ~f:(fun { arm = { arm_pat; body; _ }; _ } -> (ppat arm_pat, pexpr body)) + ~f:(fun { arm = { arm_pat; body; _ }; _ } -> + (ppat arm_pat, pexpr body)) arms ) | Ascription _ -> __TODO_term__ span "asciption" | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> @@ -657,7 +659,7 @@ let string_of_item (item : item) : string = in List.map ~f:C.decl_to_string @@ Print.pitem item |> String.concat ~sep:"\n" -let string_of_items = +let string_of_items : AST.item list -> string = List.map ~f:string_of_item >> List.map ~f:String.strip >> List.filter ~f:(String.is_empty >> not) >> String.concat ~sep:"\n\n" diff --git a/engine/backends/coq/coq/dune b/engine/backends/coq/coq/dune index 5ed05cf13..65fa2807e 100644 --- a/engine/backends/coq/coq/dune +++ b/engine/backends/coq/coq/dune @@ -17,4 +17,4 @@ (env (_ (flags - (:standard -w +A)))) + (:standard -w +A -w "-4-40-42-44-45-48")))) diff --git a/engine/backends/coq/ssprove/dune b/engine/backends/coq/ssprove/dune index e1aa47a35..2acbd78d8 100644 --- a/engine/backends/coq/ssprove/dune +++ b/engine/backends/coq/ssprove/dune @@ -8,7 +8,6 @@ ppx_sexp_conv ppx_compare ppx_hash - visitors.ppx ppx_deriving.show ppx_deriving.eq ppx_inline @@ -18,4 +17,4 @@ (env (_ (flags - (:standard -w -A)))) + (:standard -w +A -w "-4-40-42-44-45-48")))) diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index e4165c1ee..96def3200 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -549,7 +549,7 @@ module Context = struct } end -let primitive_to_string (id : primitive_ident) : string = +let primitive_to_string (id : Ast.primitive_ident) : string = match id with | Deref -> "(TODO: Deref)" (* failwith "Deref" *) | Cast -> "cast_int (WS2 := _)" (* failwith "Cast" *) @@ -582,26 +582,26 @@ module TransformToInputLanguage (* : PHASE *) = ] [@ocamlformat "disable"] -let token_list (tokens : string) : string list list = - List.map ~f:(split_str ~on:"=") (split_str ~on:"," tokens) +(* let token_list (tokens : string) : string list list = *) +(* List.map ~f:(split_str ~on:"=") (split_str ~on:"," tokens) *) -let get_argument (s : string) (token_list : string list list) = - List.find_map - ~f:(function - | [ v; a ] when String.equal (String.strip v) s -> Some a | _ -> None) - token_list +(* let get_argument (s : string) (token_list : string list list) = *) +(* List.find_map *) +(* ~f:(function *) +(* | [ v; a ] when String.equal (String.strip v) s -> Some a | _ -> None) *) +(* token_list *) -let strip (x : string) = - String.strip - ?drop:(Some (function '\"' -> true | _ -> false)) - (String.strip x) +(* let strip (x : string) = *) +(* String.strip *) +(* ?drop:(Some (function '\"' -> true | _ -> false)) *) +(* (String.strip x) *) -let strip_or_error (err : string) (s : string option) span = - match s with - | Some x -> strip x - | None -> Error.unimplemented ~details:err span +(* let strip_or_error (err : string) (s : string option) span = *) +(* match s with *) +(* | Some x -> strip x *) +(* | None -> Error.unimplemented ~details:err span *) -let pconcrete_ident (id : concrete_ident) : string = +let pconcrete_ident (id : Ast.concrete_ident) : string = U.Concrete_ident_view.to_definition_name id let plocal_ident (e : Local_ident.t) : string = @@ -618,7 +618,7 @@ end) = struct open Ctx - let pglobal_ident (id : global_ident) : string = + let pglobal_ident (id : Ast.global_ident) : string = match id with | `Projector (`Concrete cid) | `Concrete cid -> pconcrete_ident cid | `Primitive p_id -> primitive_to_string p_id @@ -652,7 +652,7 @@ struct open TODOs - let pint_kind (k : int_kind) : SSP.AST.int_type = + let pint_kind (k : Ast.int_kind) : SSP.AST.int_type = { size = (match k.size with @@ -665,7 +665,7 @@ struct signed = Stdlib.(k.signedness == Signed); } - let pliteral (e : literal) = + let pliteral (e : Ast.literal) = match e with | String s -> SSP.AST.Const_string s | Char c -> SSP.AST.Const_char (Char.to_int c) @@ -674,7 +674,7 @@ struct | Bool b -> SSP.AST.Const_bool b let operators = - let c = Global_ident.of_name Value in + let c = Ast.Global_ident.of_name Value in [ (c Rust_primitives__hax__array_of_list, (3, [ ""; ".a["; "]<-"; "" ])); (c Core__ops__index__Index__index, (2, [ ""; ".a["; "]" ])); @@ -695,7 +695,7 @@ struct (c Core__ops__bit__Shl__shl, (2, [ ""; " shift_left "; "" ])); (c Core__ops__bit__Shr__shr, (2, [ ""; " shift_right "; "" ])); ] - |> Map.of_alist_exn (module Global_ident) + |> Map.of_alist_exn (module Ast.Global_ident) module LocalIdentOrLisIis = StaticAnalysis.MutableVariables.LocalIdentOrData (struct @@ -708,18 +708,18 @@ struct | TChar -> __TODO_ty__ span "char" | TInt k -> SSP.AST.Int (pint_kind k) | TStr -> SSP.AST.NameTy "chString" - | TApp { ident = `TupleType 0; args = [] } -> SSP.AST.Unit - | TApp { ident = `TupleType 1; args = [ GType ty ] } -> pty span ty - | TApp { ident = `TupleType n; args } when n >= 2 -> + | TApp { ident = `TupleType 0; args = []; _ } -> SSP.AST.Unit + | TApp { ident = `TupleType 1; args = [ GType ty ]; _ } -> pty span ty + | TApp { ident = `TupleType n; args; _ } when n >= 2 -> SSP.AST.Product (args_ty span args) - | TApp { ident; args } -> + | TApp { ident; args; _ } -> SSP.AST.AppTy (SSP.AST.NameTy (pglobal_ident ident), args_ty span args) | TArrow (inputs, output) -> List.fold_right ~init:(pty span output) ~f:(fun x y -> SSP.AST.Arrow (x, y)) (List.map ~f:(pty span) inputs) | TFloat _ -> __TODO_ty__ span "pty: Float" - | TArray { typ; length = { e = Literal (Int { value; _ }) } } -> + | TArray { typ; length = { e = Literal (Int { value; _ }); _ }; _ } -> SSP.AST.ArrayTy (pty span typ, value) | TArray { typ; length } -> SSP.AST.ArrayTy @@ -758,7 +758,7 @@ struct and ppat (p : pat) : SSP.AST.pat = match p.p with | PWild -> SSP.AST.WildPat - | PAscription { typ; pat } -> + | PAscription { typ; pat; _ } -> SSP.AST.AscriptionPat (ppat pat, pty p.span typ) | PBinding { @@ -766,6 +766,7 @@ struct mode = _; var; typ = _ (* we skip type annot here *); + _; } -> SSP.AST.Ident (plocal_ident var) | PBinding @@ -779,12 +780,12 @@ struct SSP.AST.Ident (plocal_ident var) (* TODO Mutable binding ! *) | POr { subpats } -> SSP.AST.DisjunctivePat (List.map ~f:ppat subpats) | PArray _ -> __TODO_pat__ p.span "Parray?" - | PConstruct { name = `TupleCons 0; args = [] } -> + | PConstruct { name = `TupleCons 0; args = []; _ } -> SSP.AST.WildPat (* UnitPat *) - | PConstruct { name = `TupleCons 1; args = [ _ ] } -> + | PConstruct { name = `TupleCons 1; args = [ _ ]; _ } -> __TODO_pat__ p.span "tuple 1" - | PConstruct { name = `TupleCons _n; args } -> - SSP.AST.TuplePat (List.map ~f:(fun { pat } -> ppat pat) args) + | PConstruct { name = `TupleCons _n; args; _ } -> + SSP.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) args) (* Record *) | PConstruct { is_record = true; _ } -> __TODO_pat__ p.span "record pattern" (* (\* SSP.AST.Ident (pglobal_ident name) *\) *) @@ -792,7 +793,7 @@ struct (* (\* SSP.AST.ConstructorPat (pglobal_ident name ^ "_case", [SSP.AST.Ident "temp"]) *\) *) (* (\* List.map ~f:(fun {field; pat} -> (pat, SSP.AST.App (SSP.AST.Var (pglobal_ident field), [SSP.AST.Var "temp"]))) args *\) *) (* Enum *) - | PConstruct { name; args; is_record = false } -> + | PConstruct { name; args; is_record = false; _ } -> SSP.AST.ConstructorPat ( pglobal_ident name, match args with @@ -855,13 +856,17 @@ struct ] ) | LocalVar local_ident -> SSP.AST.NameTerm (plocal_ident local_ident) | GlobalVar (`TupleCons 0) - | Construct { constructor = `TupleCons 0; fields = [] } -> + | Construct { constructor = `TupleCons 0; fields = []; _ } -> SSP.AST.App (SSP.AST.Var "ret_both", [ SSPExtraDefinitions.unit_term ]) | GlobalVar global_ident -> SSP.AST.Var (pglobal_ident global_ident) - | App { f = { e = GlobalVar (`Projector (`TupleField _)) }; args = [ _ ] } - -> + | App + { + f = { e = GlobalVar (`Projector (`TupleField _)); _ }; + args = [ _ ]; + _; + } -> __TODO_term__ span "app global vcar projector tuple" - | App { f = { e = GlobalVar x }; args } when Map.mem operators x -> + | App { f = { e = GlobalVar x; _ }; args; _ } when Map.mem operators x -> let arity, op = Map.find_exn operators x in if List.length args <> arity then failwith "Bad arity"; let args = @@ -872,7 +877,7 @@ struct SSP.AST.AppFormat (op, args) (* | App { f = { e = GlobalVar x }; args } -> *) (* __TODO_term__ span "GLOBAL APP?" *) - | App { f; args } -> + | App { f; args; _ } -> let base = (pexpr env false) f in let args = List.map ~f:(pexpr env false) args in SSP.AST.App (base, args) @@ -947,9 +952,11 @@ struct is_struct = true; _; }; + _; }; body; }; + _; }; ]; } -> @@ -968,7 +975,7 @@ struct SSPExtraDefinitions.matchb ( (pexpr env false) scrutinee, List.map - ~f:(fun { arm = { arm_pat; body } } -> + ~f:(fun { arm = { arm_pat; body }; _ } -> match arm_pat.p with | PConstruct { name; args; is_record = false; is_struct = false } -> ( @@ -1017,14 +1024,14 @@ struct SSP.AST.App ( SSP.AST.Var "prod_b", [ SSP.AST.Tuple (List.map ~f:(snd >> pexpr env false) fields) ] ) - | Construct { is_record = true; constructor; fields; base = None } -> + | Construct { is_record = true; constructor; fields; base = None; _ } -> SSP.AST.RecordConstructor ( "t_" ^ pglobal_ident constructor, List.map ~f:(fun (f, e) -> (pglobal_ident f, (pexpr env false) e)) fields ) - | Construct { is_record = true; constructor; fields; base = Some (x, _) } - -> + | Construct + { is_record = true; constructor; fields; base = Some (x, _); _ } -> SSP.AST.RecordUpdate ( pglobal_ident constructor, (pexpr env false) x, @@ -1041,14 +1048,14 @@ struct SSP.AST.App ( SSP.AST.Var (pglobal_ident constructor), List.map ~f:(snd >> pexpr env add_solve) fields ) - | Closure { params; body } -> + | Closure { params; body; _ } -> SSP.AST.Lambda ( List.map ~f:ppat params, (pexpr (extend_env_with_params env params) add_solve) body ) | MacroInvokation { macro; _ } -> Error.raise @@ { - kind = UnsupportedMacro { id = [%show: global_ident] macro }; + kind = UnsupportedMacro { id = [%show: Ast.global_ident] macro }; span = e.span; } | Assign _ -> @@ -1288,7 +1295,7 @@ struct (* List.fold ~init:false ~f:(||) (List.map ~f:(fun p -> is_mutable_pat p) args) *) false | PConstant _ -> false - | PBinding { mut = Mutable _ } -> true + | PBinding { mut = Mutable _; _ } -> true | PBinding _ -> false | POr _ -> (* List.fold ~init:false ~f:( || ) *) @@ -1297,7 +1304,7 @@ struct (* TODO? *) | _ -> . - let pgeneric_param_as_argument span : generic_param -> SSP.AST.argument = + let pgeneric_param_as_argument span : AST.generic_param -> SSP.AST.argument = function | { ident; kind; _ } -> SSP.AST.Implicit @@ -1308,9 +1315,7 @@ struct SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])" (pty span t) | GPType { default = None } -> SSP.AST.WildTy - | _ -> - Error.unimplemented - ~details:"SSProve: TODO: generic_params_argument" span ) + | _ -> . ) let pgeneric_constraints_as_argument span : generic_constraint -> SSP.AST.argument list = function @@ -1323,20 +1328,16 @@ struct List.map ~f:(function | GType typ -> pty span typ - | GConst { typ } -> + | GConst { typ; _ } -> SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])" (pty span typ) - | _ -> - Error.unimplemented - ~details:"SSProve: TODO: generic_params_constraint1" - span) + | _ -> .) args ) ); ] - | _ -> - Error.unimplemented ~details:"SSProve: TODO: generic_params_constraint2" - span + | _ -> . - let pgeneric (span : span) (generics : generics) : SSP.AST.argument list = + let pgeneric (span : Ast.span) (generics : AST.generics) : + SSP.AST.argument list = List.map ~f:(pgeneric_param_as_argument span) generics.params @ List.concat_map ~f:(pgeneric_constraints_as_argument span) @@ -1402,7 +1403,7 @@ struct in (size, ret_ty) - let rec pitem (e : item) : SSP.AST.decl list = + let rec pitem (e : AST.item) : SSP.AST.decl list = try pitem_unwrapped e with Diagnostics.SpanFreeError.Exn _kind -> [ SSP.AST.Unimplemented "item error backend" ] @@ -1460,7 +1461,7 @@ struct { name; generics; - variants = [ { name = _record_name; arguments } ]; + variants = [ { name = _record_name; arguments; _ } ]; is_struct = true; } -> [ @@ -1472,10 +1473,10 @@ struct (p_record_record span arguments) ); ] (* enum *) - | Type { name; generics; variants } -> + | Type { name; generics; variants; _ } -> (* Define all record types in enums (no anonymous records) *) List.filter_map variants - ~f:(fun { name = v_name; arguments; is_record } -> + ~f:(fun { name = v_name; arguments; is_record; _ } -> if is_record then Some (SSPExtraDefinitions.updatable_record @@ -1495,7 +1496,7 @@ struct ( pconcrete_ident name, pgeneric span generics, List.map variants - ~f:(fun { name = v_name; arguments; is_record } -> + ~f:(fun { name = v_name; arguments; is_record; _ } -> if is_record then SSP.AST.InductiveCase ( pconcrete_ident v_name, @@ -1942,8 +1943,8 @@ struct end module type S = sig - val pitem : item -> SSP.AST.decl list - val pgeneric : span -> generics -> SSP.AST.argument list + val pitem : AST.item -> SSP.AST.decl list + (* val pgeneric : Ast.span -> AST.generics -> SSP.AST.argument list *) end let make ctx = @@ -1954,8 +1955,8 @@ let make ctx = let decls_to_string (decls : SSP.AST.decl list) : string = String.concat ~sep:"\n" (List.map ~f:SSP.decl_to_string decls) -let print_item (analysis_data : StaticAnalysis.analysis_data) (item : item) : - SSP.AST.decl list = +let print_item (analysis_data : StaticAnalysis.analysis_data) (item : AST.item) + : SSP.AST.decl list = let (module Print) = make { @@ -1970,380 +1971,380 @@ let cleanup_item_strings = >> List.filter ~f:(String.is_empty >> not) >> String.concat ~sep:"\n\n" -module ConCert = struct - let translate_concert_annotations - (analysis_data : StaticAnalysis.analysis_data) (e : item) : - SSP.AST.decl list = - let (module Print) = - make - { - current_namespace = U.Concrete_ident_view.to_namespace e.ident; - analysis_data; - } - in - match e.v with - | Fn { name = f_name; generics; _ } -> - List.concat_map - ~f:(fun { kind; span } -> - match kind with - | Tool { path; tokens } -> ( - let token_list = token_list tokens in - match path with - | "hax::init" -> - let contract = - strip_or_error "contract argument missing" - (get_argument "contract" token_list) - e.span - in - [ - SSP.AST.Definition - ( "init_" ^ contract, - [ - SSP.AST.Explicit - (SSP.AST.Ident "chain", SSP.AST.NameTy "Chain"); - SSP.AST.Explicit - ( SSP.AST.Ident "ctx", - SSP.AST.NameTy "ContractCallContext" ); - SSP.AST.Explicit - ( SSP.AST.Ident "st", - SSP.AST.NameTy ("state_" ^ contract) ); - ], - SSP.AST.App - (SSP.AST.Var "ResultMonad.Ok", [ SSP.AST.Var "st" ]), - SSP.AST.AppTy - ( SSP.AST.NameTy "ResultMonad.result", - [ - SSP.AST.NameTy ("state_" ^ contract); - SSP.AST.NameTy "t_ParseError"; - ] ) ); - ] - | "hax::receive" -> - let contract = - strip_or_error "contract argument missing" - (get_argument "contract" token_list) - e.span - in - let name = - strip_or_error "name argument missing" - (get_argument "name" token_list) - e.span - in - let parameter = get_argument "parameter" token_list in - (* let logger = get_argument "logger" token_list in *) - (* let payable = get_argument "payable" token_list in *) - let param_instances, param_list, count, param_vars = - match parameter with - | Some x -> - ( [ - SSP.AST.ProgramInstance - ( "t_HasReceiveContext", - [], - SSP.AST.NameTy ("t_" ^ strip x), - [ - SSP.AST.NameTy ("t_" ^ strip x); - SSP.AST.Unit; - ], - SSP.AST.InstanceDecls - [ - SSP.AST.InlineDef - ( "f_get", - [ - SSP.AST.Implicit - ( SSP.AST.Ident "Ctx", - SSP.AST.WildTy ); - SSP.AST.Implicit - ( SSP.AST.Ident "L", - (SSP.AST.NameTy - "{fset Location}" - : SSP.AST.ty) ); - SSP.AST.Implicit - ( SSP.AST.Ident "I", - (SSP.AST.NameTy "Interface" - : SSP.AST.ty) ); - ], - SSP.AST.Var - "(solve_lift (@ret_both \ - (t_ParamType × t_Result Ctx \ - t_ParseError)) (tt, inr tt))", - SSP.AST.WildTy ); - ] ); - SSP.AST.ProgramInstance - ( "t_Sized", - [], - SSP.AST.NameTy ("t_" ^ strip x), - [ SSP.AST.NameTy ("t_" ^ strip x) ], - SSP.AST.TermDef - (SSP.AST.Lambda - ([ SSP.AST.Ident "x" ], SSP.AST.Var "x")) - ); - ], - [ - SSP.AST.Explicit - ( SSP.AST.Ident "ctx", - SSPExtraDefinitions.wrap_type_in_both "L0" - "I0" - (SSP.AST.NameTy ("t_" ^ strip x)) ); - ], - 1, - [ SSP.AST.Var "ctx" ] ) - | _ -> ([], [], 0, []) - in - param_instances - @ [ - SSP.AST.Definition - ( "receive_" ^ contract ^ "_" ^ name, - Print.pgeneric span generics - @ List.map - ~f:(fun x -> - SSP.AST.Implicit - ( SSP.AST.Ident x, - (SSP.AST.NameTy "{fset Location}" - : SSP.AST.ty) )) - (List.map - ~f:(fun i -> "L" ^ Int.to_string i) - (List.range 0 (count + 1))) - @ List.map - ~f:(fun x -> - SSP.AST.Implicit - ( SSP.AST.Ident x, - (SSP.AST.NameTy "Interface" : SSP.AST.ty) - )) - (List.map - ~f:(fun i -> "I" ^ Int.to_string i) - (List.range 0 (count + 1))) - @ param_list - @ [ - SSP.AST.Explicit - ( SSP.AST.Ident "st", - SSPExtraDefinitions.wrap_type_in_both - ("L" ^ Int.to_string count) - ("I" ^ Int.to_string count) - (SSP.AST.NameTy ("state_" ^ contract)) ); - (* TODO: L, I *) - ], - (* Arguments *) - SSP.AST.App - ( SSP.AST.Var (pconcrete_ident f_name) - (* contract *), - param_vars @ [ SSP.AST.Var "st" ] ), - SSPExtraDefinitions.wrap_type_in_both "_" "_" - (SSP.AST.NameTy - ("t_Result ((v_A × state_" ^ contract - ^ ")) (t_ParseError)")) ); - (* TODO: L , I *) - ] - | _ -> []) - | _ -> []) - e.attrs - | Type { name; variants = [ _ ]; is_struct = true; _ } -> - List.concat_map - ~f:(fun { kind; _ } -> - match kind with - | Tool { path; tokens } when String.equal path "hax::contract_state" - -> - let token_list = token_list tokens in - let contract = - strip_or_error "contract argument missing" - (get_argument "contract" token_list) - e.span - in - [ - SSP.AST.Definition - ( "state_" ^ contract, - [], - SSP.AST.Var (pconcrete_ident name), - SSP.AST.TypeTy ); - ] - | _ -> []) - e.attrs - | _ -> [] - - let concert_contract_type_decls (items : item list) : SSP.AST.decl list list = - let contract_items = - List.filter_map - ~f:(function - | { kind = Tool { path; tokens }; _ } - when String.equal path "hax::receive" -> - let token_list = token_list tokens in - let contract = - strip_or_error "contract argument missing" - (get_argument "contract" token_list) - (Span.dummy ()) - (* TODO: carry span information *) - in - let name = - strip_or_error "name argument missing" - (get_argument "name" token_list) - (Span.dummy ()) - (* TODO: carry span information *) - in - let parameter = get_argument "parameter" token_list in - Some (contract, parameter, name) - | _ -> None) - (List.concat_map ~f:(fun x -> x.attrs) items) - in - if List.is_empty contract_items then [] - else - let contract_map = - List.fold_left - ~init:(Map.empty (module String)) - ~f:(fun y (x_name, x_parameter, x_item) -> - Map.set y ~key:x_name - ~data: - (Option.value ~default:[] (Map.find y x_name) - @ [ (x_parameter, x_item) ])) - contract_items - in - List.map - ~f:(fun contract -> - let receive_functions : (_ * string) list = - Option.value ~default:[] (Map.find contract_map contract) - in - [ - SSP.AST.Inductive - ( "Msg_" ^ contract, - [], - List.map - ~f:(function - | Some param, x_item -> - SSP.AST.InductiveCase - ( "msg_" ^ contract ^ "_" ^ x_item, - SSP.AST.NameTy ("t_" ^ strip param) ) - | None, x_item -> - SSP.AST.BaseCase ("msg_" ^ contract ^ "_" ^ x_item)) - receive_functions ); - SSP.AST.ProgramInstance - ( "t_HasReceiveContext", - [], - SSP.AST.NameTy ("state_" ^ contract), - [ SSP.AST.NameTy ("state_" ^ contract); SSP.AST.Unit ], - SSP.AST.InstanceDecls - [ - SSP.AST.InlineDef - ( "f_get", - [ - SSP.AST.Explicit (SSP.AST.Ident "Ctx", SSP.AST.WildTy); - SSP.AST.Implicit - ( SSP.AST.Ident "L", - (SSP.AST.NameTy "{fset Location}" : SSP.AST.ty) ); - SSP.AST.Implicit - ( SSP.AST.Ident "I", - (SSP.AST.NameTy "Interface" : SSP.AST.ty) ); - ], - SSP.AST.Var - "(solve_lift (@ret_both (t_ParamType × t_Result Ctx \ - t_ParseError)) (tt, inr tt))", - SSP.AST.WildTy ); - ] ); - SSP.AST.ProgramInstance - ( "t_Sized", - [], - SSP.AST.NameTy ("state_" ^ contract), - [ SSP.AST.NameTy ("state_" ^ contract) ], - SSP.AST.TermDef - (SSP.AST.Lambda ([ SSP.AST.Ident "x" ], SSP.AST.Var "x")) ); - SSP.AST.ProgramInstance - ( "t_HasActions", - [], - SSP.AST.NameTy ("state_" ^ contract), - [ SSP.AST.NameTy ("state_" ^ contract) ], - SSP.AST.TermDef (SSP.AST.Var "Admitted") ); - SSP.AST.Equations - ( "receive_" ^ contract, - [ - SSP.AST.Explicit - (SSP.AST.Ident "chain", SSP.AST.NameTy "Chain"); - SSP.AST.Explicit - (SSP.AST.Ident "ctx", SSP.AST.NameTy "ContractCallContext"); - SSP.AST.Explicit - (SSP.AST.Ident "st", SSP.AST.NameTy ("state_" ^ contract)); - SSP.AST.Explicit - ( SSP.AST.Ident "msg", - SSP.AST.NameTy ("Datatypes.option Msg_" ^ contract) ); - ], - SSP.AST.Match - ( SSP.AST.Var "msg", - List.map - ~f:(function - | Some _param, x_item -> - ( SSP.AST.Ident - ("Some" ^ " " ^ "(" ^ "msg_" ^ contract ^ "_" - ^ x_item ^ " " ^ "val" ^ ")"), - SSP.AST.Var - ("match (is_pure (both_prog (receive_" - ^ contract ^ "_" ^ x_item - ^ " (ret_both val) (ret_both st)))) with\n\ - \ | inl x => ResultMonad.Ok ((fst x), \ - [])\n\ - \ | inr x => ResultMonad.Err x\n\ - \ end") ) - | None, x_item -> - ( SSP.AST.Ident - ("Some" ^ " " ^ "msg_" ^ contract ^ "_" ^ x_item), - SSP.AST.Var - ("match (is_pure (both_prog (receive_" - ^ contract ^ "_" ^ x_item - ^ " (ret_both st)))) with\n\ - \ | inl x => ResultMonad.Ok ((fst x), \ - [])\n\ - \ | inr x => ResultMonad.Err x\n\ - \ end") )) - receive_functions - @ [ (SSP.AST.WildPat, SSP.AST.Var "ResultMonad.Err tt") ] ), - SSP.AST.NameTy - ("ResultMonad.result (state_" ^ contract - ^ " * list ActionBody) t_ParseError") ); - SSP.AST.ProgramInstance - ( "Serializable", - [], - SSP.AST.NameTy ("state_" ^ contract), - [ SSP.AST.NameTy ("state_" ^ contract) ], - SSP.AST.InstanceDecls [] ); - SSP.AST.ProgramInstance - ( "Serializable", - [], - SSP.AST.NameTy ("Msg_" ^ contract), - [ SSP.AST.NameTy ("Msg_" ^ contract) ], - SSP.AST.TermDef - (SSP.AST.Var - ("Derive Serializable Msg_OVN_rect<" - ^ String.concat ~sep:"," - (List.map - ~f:(fun x -> "msg_" ^ contract ^ "_" ^ snd x) - receive_functions) - ^ ">")) ); - SSP.AST.Definition - ( "contract_" ^ contract, - [], - SSP.AST.App - ( SSP.AST.Var "build_contract", - [ - SSP.AST.Var ("init_" ^ contract); - SSP.AST.Var ("receive_" ^ contract); - ] ), - SSP.AST.AppTy - ( SSP.AST.NameTy "Contract", - [ - SSP.AST.NameTy ("state_" ^ contract); - SSP.AST.NameTy ("Msg_" ^ contract); - SSP.AST.NameTy ("state_" ^ contract); - SSP.AST.NameTy "t_ParseError"; - ] ) ); - ]) - (Map.keys contract_map) - - let concert_header = - [ - SSP.AST.Comment "Concert lib part"; - SSP.AST.Require (Some "ConCert.Utils", [ "Extras" ], None); - SSP.AST.Require (Some "ConCert.Utils", [ "Automation" ], None); - SSP.AST.Require (Some "ConCert.Execution", [ "Serializable" ], None); - SSP.AST.Require (Some "ConCert.Execution", [ "Blockchain" ], None); - SSP.AST.Require (Some "ConCert.Execution", [ "ContractCommon" ], None); - SSP.AST.Require (Some "ConCert.Execution", [ "Serializable" ], None); - SSP.AST.Require (None, [ "ConCertLib" ], None); - ] -end +(* module ConCert = struct *) +(* let translate_concert_annotations *) +(* (analysis_data : StaticAnalysis.analysis_data) (e : item) : *) +(* SSP.AST.decl list = *) +(* let (module Print) = *) +(* make *) +(* { *) +(* current_namespace = U.Concrete_ident_view.to_namespace e.ident; *) +(* analysis_data; *) +(* } *) +(* in *) +(* match e.v with *) +(* | Fn { name = f_name; generics; _ } -> *) +(* List.concat_map *) +(* ~f:(fun { kind; span } -> *) +(* match kind with *) +(* | Tool { path; tokens } -> ( *) +(* let token_list = token_list tokens in *) +(* match path with *) +(* | "hax::init" -> *) +(* let contract = *) +(* strip_or_error "contract argument missing" *) +(* (get_argument "contract" token_list) *) +(* e.span *) +(* in *) +(* [ *) +(* SSP.AST.Definition *) +(* ( "init_" ^ contract, *) +(* [ *) +(* SSP.AST.Explicit *) +(* (SSP.AST.Ident "chain", SSP.AST.NameTy "Chain"); *) +(* SSP.AST.Explicit *) +(* ( SSP.AST.Ident "ctx", *) +(* SSP.AST.NameTy "ContractCallContext" ); *) +(* SSP.AST.Explicit *) +(* ( SSP.AST.Ident "st", *) +(* SSP.AST.NameTy ("state_" ^ contract) ); *) +(* ], *) +(* SSP.AST.App *) +(* (SSP.AST.Var "ResultMonad.Ok", [ SSP.AST.Var "st" ]), *) +(* SSP.AST.AppTy *) +(* ( SSP.AST.NameTy "ResultMonad.result", *) +(* [ *) +(* SSP.AST.NameTy ("state_" ^ contract); *) +(* SSP.AST.NameTy "t_ParseError"; *) +(* ] ) ); *) +(* ] *) +(* | "hax::receive" -> *) +(* let contract = *) +(* strip_or_error "contract argument missing" *) +(* (get_argument "contract" token_list) *) +(* e.span *) +(* in *) +(* let name = *) +(* strip_or_error "name argument missing" *) +(* (get_argument "name" token_list) *) +(* e.span *) +(* in *) +(* let parameter = get_argument "parameter" token_list in *) +(* (\* let logger = get_argument "logger" token_list in *\) *) +(* (\* let payable = get_argument "payable" token_list in *\) *) +(* let param_instances, param_list, count, param_vars = *) +(* match parameter with *) +(* | Some x -> *) +(* ( [ *) +(* SSP.AST.ProgramInstance *) +(* ( "t_HasReceiveContext", *) +(* [], *) +(* SSP.AST.NameTy ("t_" ^ strip x), *) +(* [ *) +(* SSP.AST.NameTy ("t_" ^ strip x); *) +(* SSP.AST.Unit; *) +(* ], *) +(* SSP.AST.InstanceDecls *) +(* [ *) +(* SSP.AST.InlineDef *) +(* ( "f_get", *) +(* [ *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident "Ctx", *) +(* SSP.AST.WildTy ); *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident "L", *) +(* (SSP.AST.NameTy *) +(* "{fset Location}" *) +(* : SSP.AST.ty) ); *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident "I", *) +(* (SSP.AST.NameTy "Interface" *) +(* : SSP.AST.ty) ); *) +(* ], *) +(* SSP.AST.Var *) +(* "(solve_lift (@ret_both \ *) + (* (t_ParamType × t_Result Ctx \ *) + (* t_ParseError)) (tt, inr tt))", *) +(* SSP.AST.WildTy ); *) +(* ] ); *) +(* SSP.AST.ProgramInstance *) +(* ( "t_Sized", *) +(* [], *) +(* SSP.AST.NameTy ("t_" ^ strip x), *) +(* [ SSP.AST.NameTy ("t_" ^ strip x) ], *) +(* SSP.AST.TermDef *) +(* (SSP.AST.Lambda *) +(* ([ SSP.AST.Ident "x" ], SSP.AST.Var "x")) *) +(* ); *) +(* ], *) +(* [ *) +(* SSP.AST.Explicit *) +(* ( SSP.AST.Ident "ctx", *) +(* SSPExtraDefinitions.wrap_type_in_both "L0" *) +(* "I0" *) +(* (SSP.AST.NameTy ("t_" ^ strip x)) ); *) +(* ], *) +(* 1, *) +(* [ SSP.AST.Var "ctx" ] ) *) +(* | _ -> ([], [], 0, []) *) +(* in *) +(* param_instances *) +(* @ [ *) +(* SSP.AST.Definition *) +(* ( "receive_" ^ contract ^ "_" ^ name, *) +(* Print.pgeneric span generics *) +(* @ List.map *) +(* ~f:(fun x -> *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident x, *) +(* (SSP.AST.NameTy "{fset Location}" *) +(* : SSP.AST.ty) )) *) +(* (List.map *) +(* ~f:(fun i -> "L" ^ Int.to_string i) *) +(* (List.range 0 (count + 1))) *) +(* @ List.map *) +(* ~f:(fun x -> *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident x, *) +(* (SSP.AST.NameTy "Interface" : SSP.AST.ty) *) +(* )) *) +(* (List.map *) +(* ~f:(fun i -> "I" ^ Int.to_string i) *) +(* (List.range 0 (count + 1))) *) +(* @ param_list *) +(* @ [ *) +(* SSP.AST.Explicit *) +(* ( SSP.AST.Ident "st", *) +(* SSPExtraDefinitions.wrap_type_in_both *) +(* ("L" ^ Int.to_string count) *) +(* ("I" ^ Int.to_string count) *) +(* (SSP.AST.NameTy ("state_" ^ contract)) ); *) +(* (\* TODO: L, I *\) *) +(* ], *) +(* (\* Arguments *\) *) +(* SSP.AST.App *) +(* ( SSP.AST.Var (pconcrete_ident f_name) *) +(* (\* contract *\), *) +(* param_vars @ [ SSP.AST.Var "st" ] ), *) +(* SSPExtraDefinitions.wrap_type_in_both "_" "_" *) +(* (SSP.AST.NameTy *) +(* ("t_Result ((v_A × state_" ^ contract *) +(* ^ ")) (t_ParseError)")) ); *) +(* (\* TODO: L , I *\) *) +(* ] *) +(* | _ -> []) *) +(* | _ -> []) *) +(* e.attrs *) +(* | Type { name; variants = [ _ ]; is_struct = true; _ } -> *) +(* List.concat_map *) +(* ~f:(fun { kind; _ } -> *) +(* match kind with *) +(* | Tool { path; tokens } when String.equal path "hax::contract_state" *) +(* -> *) +(* let token_list = token_list tokens in *) +(* let contract = *) +(* strip_or_error "contract argument missing" *) +(* (get_argument "contract" token_list) *) +(* e.span *) +(* in *) +(* [ *) +(* SSP.AST.Definition *) +(* ( "state_" ^ contract, *) +(* [], *) +(* SSP.AST.Var (pconcrete_ident name), *) +(* SSP.AST.TypeTy ); *) +(* ] *) +(* | _ -> []) *) +(* e.attrs *) +(* | _ -> [] *) + +(* let concert_contract_type_decls (items : item list) : SSP.AST.decl list list = *) +(* let contract_items = *) +(* List.filter_map *) +(* ~f:(function *) +(* | { kind = Tool { path; tokens }; _ } *) +(* when String.equal path "hax::receive" -> *) +(* let token_list = token_list tokens in *) +(* let contract = *) +(* strip_or_error "contract argument missing" *) +(* (get_argument "contract" token_list) *) +(* (Span.dummy ()) *) +(* (\* TODO: carry span information *\) *) +(* in *) +(* let name = *) +(* strip_or_error "name argument missing" *) +(* (get_argument "name" token_list) *) +(* (Span.dummy ()) *) +(* (\* TODO: carry span information *\) *) +(* in *) +(* let parameter = get_argument "parameter" token_list in *) +(* Some (contract, parameter, name) *) +(* | _ -> None) *) +(* (List.concat_map ~f:(fun x -> x.attrs) items) *) +(* in *) +(* if List.is_empty contract_items then [] *) +(* else *) +(* let contract_map = *) +(* List.fold_left *) +(* ~init:(Map.empty (module String)) *) +(* ~f:(fun y (x_name, x_parameter, x_item) -> *) +(* Map.set y ~key:x_name *) +(* ~data: *) +(* (Option.value ~default:[] (Map.find y x_name) *) +(* @ [ (x_parameter, x_item) ])) *) +(* contract_items *) +(* in *) +(* List.map *) +(* ~f:(fun contract -> *) +(* let receive_functions : (_ * string) list = *) +(* Option.value ~default:[] (Map.find contract_map contract) *) +(* in *) +(* [ *) +(* SSP.AST.Inductive *) +(* ( "Msg_" ^ contract, *) +(* [], *) +(* List.map *) +(* ~f:(function *) +(* | Some param, x_item -> *) +(* SSP.AST.InductiveCase *) +(* ( "msg_" ^ contract ^ "_" ^ x_item, *) +(* SSP.AST.NameTy ("t_" ^ strip param) ) *) +(* | None, x_item -> *) +(* SSP.AST.BaseCase ("msg_" ^ contract ^ "_" ^ x_item)) *) +(* receive_functions ); *) +(* SSP.AST.ProgramInstance *) +(* ( "t_HasReceiveContext", *) +(* [], *) +(* SSP.AST.NameTy ("state_" ^ contract), *) +(* [ SSP.AST.NameTy ("state_" ^ contract); SSP.AST.Unit ], *) +(* SSP.AST.InstanceDecls *) +(* [ *) +(* SSP.AST.InlineDef *) +(* ( "f_get", *) +(* [ *) +(* SSP.AST.Explicit (SSP.AST.Ident "Ctx", SSP.AST.WildTy); *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident "L", *) +(* (SSP.AST.NameTy "{fset Location}" : SSP.AST.ty) ); *) +(* SSP.AST.Implicit *) +(* ( SSP.AST.Ident "I", *) +(* (SSP.AST.NameTy "Interface" : SSP.AST.ty) ); *) +(* ], *) +(* SSP.AST.Var *) +(* "(solve_lift (@ret_both (t_ParamType × t_Result Ctx \ *) + (* t_ParseError)) (tt, inr tt))", *) +(* SSP.AST.WildTy ); *) +(* ] ); *) +(* SSP.AST.ProgramInstance *) +(* ( "t_Sized", *) +(* [], *) +(* SSP.AST.NameTy ("state_" ^ contract), *) +(* [ SSP.AST.NameTy ("state_" ^ contract) ], *) +(* SSP.AST.TermDef *) +(* (SSP.AST.Lambda ([ SSP.AST.Ident "x" ], SSP.AST.Var "x")) ); *) +(* SSP.AST.ProgramInstance *) +(* ( "t_HasActions", *) +(* [], *) +(* SSP.AST.NameTy ("state_" ^ contract), *) +(* [ SSP.AST.NameTy ("state_" ^ contract) ], *) +(* SSP.AST.TermDef (SSP.AST.Var "Admitted") ); *) +(* SSP.AST.Equations *) +(* ( "receive_" ^ contract, *) +(* [ *) +(* SSP.AST.Explicit *) +(* (SSP.AST.Ident "chain", SSP.AST.NameTy "Chain"); *) +(* SSP.AST.Explicit *) +(* (SSP.AST.Ident "ctx", SSP.AST.NameTy "ContractCallContext"); *) +(* SSP.AST.Explicit *) +(* (SSP.AST.Ident "st", SSP.AST.NameTy ("state_" ^ contract)); *) +(* SSP.AST.Explicit *) +(* ( SSP.AST.Ident "msg", *) +(* SSP.AST.NameTy ("Datatypes.option Msg_" ^ contract) ); *) +(* ], *) +(* SSP.AST.Match *) +(* ( SSP.AST.Var "msg", *) +(* List.map *) +(* ~f:(function *) +(* | Some _param, x_item -> *) +(* ( SSP.AST.Ident *) +(* ("Some" ^ " " ^ "(" ^ "msg_" ^ contract ^ "_" *) +(* ^ x_item ^ " " ^ "val" ^ ")"), *) +(* SSP.AST.Var *) +(* ("match (is_pure (both_prog (receive_" *) +(* ^ contract ^ "_" ^ x_item *) +(* ^ " (ret_both val) (ret_both st)))) with\n\ *) + (* \ | inl x => ResultMonad.Ok ((fst x), \ *) + (* [])\n\ *) + (* \ | inr x => ResultMonad.Err x\n\ *) + (* \ end") ) *) +(* | None, x_item -> *) +(* ( SSP.AST.Ident *) +(* ("Some" ^ " " ^ "msg_" ^ contract ^ "_" ^ x_item), *) +(* SSP.AST.Var *) +(* ("match (is_pure (both_prog (receive_" *) +(* ^ contract ^ "_" ^ x_item *) +(* ^ " (ret_both st)))) with\n\ *) + (* \ | inl x => ResultMonad.Ok ((fst x), \ *) + (* [])\n\ *) + (* \ | inr x => ResultMonad.Err x\n\ *) + (* \ end") )) *) +(* receive_functions *) +(* @ [ (SSP.AST.WildPat, SSP.AST.Var "ResultMonad.Err tt") ] ), *) +(* SSP.AST.NameTy *) +(* ("ResultMonad.result (state_" ^ contract *) +(* ^ " * list ActionBody) t_ParseError") ); *) +(* SSP.AST.ProgramInstance *) +(* ( "Serializable", *) +(* [], *) +(* SSP.AST.NameTy ("state_" ^ contract), *) +(* [ SSP.AST.NameTy ("state_" ^ contract) ], *) +(* SSP.AST.InstanceDecls [] ); *) +(* SSP.AST.ProgramInstance *) +(* ( "Serializable", *) +(* [], *) +(* SSP.AST.NameTy ("Msg_" ^ contract), *) +(* [ SSP.AST.NameTy ("Msg_" ^ contract) ], *) +(* SSP.AST.TermDef *) +(* (SSP.AST.Var *) +(* ("Derive Serializable Msg_OVN_rect<" *) +(* ^ String.concat ~sep:"," *) +(* (List.map *) +(* ~f:(fun x -> "msg_" ^ contract ^ "_" ^ snd x) *) +(* receive_functions) *) +(* ^ ">")) ); *) +(* SSP.AST.Definition *) +(* ( "contract_" ^ contract, *) +(* [], *) +(* SSP.AST.App *) +(* ( SSP.AST.Var "build_contract", *) +(* [ *) +(* SSP.AST.Var ("init_" ^ contract); *) +(* SSP.AST.Var ("receive_" ^ contract); *) +(* ] ), *) +(* SSP.AST.AppTy *) +(* ( SSP.AST.NameTy "Contract", *) +(* [ *) +(* SSP.AST.NameTy ("state_" ^ contract); *) +(* SSP.AST.NameTy ("Msg_" ^ contract); *) +(* SSP.AST.NameTy ("state_" ^ contract); *) +(* SSP.AST.NameTy "t_ParseError"; *) +(* ] ) ); *) +(* ]) *) +(* (Map.keys contract_map) *) + +(* let concert_header = *) +(* [ *) +(* SSP.AST.Comment "Concert lib part"; *) +(* SSP.AST.Require (Some "ConCert.Utils", [ "Extras" ], None); *) +(* SSP.AST.Require (Some "ConCert.Utils", [ "Automation" ], None); *) +(* SSP.AST.Require (Some "ConCert.Execution", [ "Serializable" ], None); *) +(* SSP.AST.Require (Some "ConCert.Execution", [ "Blockchain" ], None); *) +(* SSP.AST.Require (Some "ConCert.Execution", [ "ContractCommon" ], None); *) +(* SSP.AST.Require (Some "ConCert.Execution", [ "Serializable" ], None); *) +(* SSP.AST.Require (None, [ "ConCertLib" ], None); *) +(* ] *) +(* end *) let process_annotation (x : 'a list) (f2 : ('b * ('a -> 'b)) list) : 'b list = List.concat_map @@ -2358,9 +2359,9 @@ let string_of_items (x, y) = (process_annotation x [ ([], print_item y); - ConCert.(concert_header, translate_concert_annotations y); + (* ConCert.(concert_header, translate_concert_annotations y); *) ] - @ ConCert.concert_contract_type_decls x)) + (* @ ConCert.concert_contract_type_decls x *))) (* TODO move into string_of_items, as SSP.AST decl *) let hardcoded_coq_headers =