diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index 58a953e12..55ad9a281 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -148,6 +148,8 @@ pub enum Backend { Fstar(FStarOptions), /// Use the Coq backend Coq, + /// Use the SSProve backend + Ssprove, /// Use the EasyCrypt backend (warning: work in progress!) Easycrypt, /// Use the ProVerif backend (warning: work in progress!) @@ -159,6 +161,7 @@ impl fmt::Display for Backend { match self { Backend::Fstar(..) => write!(f, "fstar"), Backend::Coq => write!(f, "coq"), + Backend::Ssprove => write!(f, "ssprove"), Backend::Easycrypt => write!(f, "easycrypt"), Backend::ProVerif => write!(f, "proverif"), } diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 457485e0b..c90877015 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -70,13 +70,9 @@ module CoqLibrary : Library = struct let int_repr (x : string) (i : string) : string = "(@repr" ^ " " ^ "WORDSIZE" ^ x ^ " " ^ i ^ ")" - let let_stmt (var : string) (expr : string) (typ : string) (body : string) - (depth : int) : string = - "let" ^ " " ^ var ^ " " ^ ":=" ^ " (" ^ expr ^ ") " ^ ":" ^ " " ^ typ - ^ " " ^ "in" ^ newline_indent depth ^ body - - let let_mut_stmt = let_stmt - let tuple_prefix : string = "" + let type_str : string = "Type" + let bool_str : string = "bool" + let unit_str : string = "unit" end end @@ -112,15 +108,15 @@ struct match id with | `Projector (`Concrete cid) | `Concrete cid -> pconcrete_ident cid | `Primitive p_id -> primitive_to_string p_id - | `TupleType i -> "TODO (global ident) tuple type" - | `TupleCons i -> "TODO (global ident) tuple cons" - | `Projector (`TupleField (i, j)) | `TupleField (i, j) -> + | `TupleType _i -> "TODO (global ident) tuple type" + | `TupleCons _i -> "TODO (global ident) tuple cons" + | `Projector (`TupleField _) | `TupleField _ -> "TODO (global ident) tuple field" | _ -> . module TODOs_debug = struct let __TODO_pat__ _ s = C.AST.Ident (s ^ " todo(pat)") - let __TODO_ty__ _ s : C.AST.ty = C.AST.Name (s ^ " todo(ty)") + let __TODO_ty__ _ s : C.AST.ty = C.AST.NameTy (s ^ " todo(ty)") let __TODO_item__ _ s = C.AST.Unimplemented (s ^ " todo(item)") let __TODO_term__ _ s = C.AST.Const (C.AST.Const_string (s ^ " todo(term)")) end @@ -135,7 +131,7 @@ struct let __TODO_term__ span s = Error.unimplemented ~details:("[expr] node " ^ s) span - let __TODO_item__ span s = C.AST.Unimplemented (s ^ " todo(item)") + let __TODO_item__ _span s = C.AST.Unimplemented (s ^ " todo(item)") end open TODOs @@ -150,14 +146,14 @@ struct | S64 -> U64 | S128 -> U128 | SSize -> USize); - signed = k.signedness == Signed; + signed = (match k.signedness with Signed -> true | _ -> false); } - let rec pliteral span (e : literal) = + let pliteral span (e : literal) = match e with | String s -> C.AST.Const_string s | Char c -> C.AST.Const_char (Char.to_int c) - | Int { value; kind } -> C.AST.Const_int (value, pint_kind kind) + | Int { value; kind; _ } -> C.AST.Const_int (value, pint_kind kind) | Float _ -> Error.unimplemented ~details:"pliteral: Float" span | Bool b -> C.AST.Const_bool b @@ -167,22 +163,23 @@ struct | TChar -> __TODO_ty__ span "char" | TInt k -> C.AST.Int (pint_kind k) | TStr -> __TODO_ty__ span "str" - | TApp { ident = `TupleType 0 as ident; args = [] } -> C.AST.Unit + | TApp { ident = `TupleType 0; args = [] } -> C.AST.Unit | TApp { ident = `TupleType 1; args = [ GType ty ] } -> pty span ty | TApp { ident = `TupleType n; args } when n >= 2 -> C.AST.Product (args_ty span args) | TApp { ident; args } -> - C.AST.AppTy (pglobal_ident ident ^ "_t", args_ty span args) + C.AST.AppTy + (C.AST.NameTy (pglobal_ident ident ^ "_t"), args_ty span args) | TArrow (inputs, output) -> List.fold_right ~init:(pty span output) ~f:(fun x y -> C.AST.Arrow (x, y)) (List.map ~f:(pty span) inputs) | TFloat _ -> __TODO_ty__ span "pty: Float" - | TArray { typ; length } -> + | TArray { typ; _ } -> C.AST.ArrayTy (pty span typ, "TODO: Int.to_string length") | TSlice { ty; _ } -> C.AST.SliceTy (pty span ty) - | TParam i -> C.AST.Name i.name - | TAssociatedType s -> C.AST.Wild + | TParam i -> C.AST.NameTy i.name + | TAssociatedType _ -> C.AST.WildTy | TOpaque _ -> __TODO_ty__ span "pty: TAssociatedType/TOpaque" | _ -> . @@ -191,7 +188,7 @@ struct match args with | arg :: xs -> (match arg with - | GLifetime { lt; witness } -> __TODO_ty__ span "lifetime" + | GLifetime _ -> __TODO_ty__ span "lifetime" | GType x -> pty span x | GConst _ -> __TODO_ty__ span "const") :: args_ty span xs @@ -199,8 +196,9 @@ struct let rec ppat (p : pat) : C.AST.pat = match p.p with - | PWild -> C.AST.Wild - | PAscription { typ; pat } -> C.AST.AscriptionPat (ppat pat, pty p.span typ) + | PWild -> C.AST.WildPat + | PAscription { typ; pat; _ } -> + C.AST.AscriptionPat (ppat pat, pty p.span typ) | PBinding { mut = Immutable; @@ -211,19 +209,18 @@ struct } -> C.AST.Ident var.name | POr { subpats } -> C.AST.DisjunctivePat (List.map ~f:ppat subpats) - | PArray { args } -> __TODO_pat__ p.span "Parray?" - | PConstruct { name = `TupleCons 0; args = [] } -> C.AST.UnitPat - | PConstruct { name = `TupleCons 1; args = [ { pat } ] } -> + | PArray _ -> __TODO_pat__ p.span "Parray?" + | PConstruct { name = `TupleCons 0; args = []; _ } -> C.AST.UnitPat + | PConstruct { name = `TupleCons 1; args = [ _ ]; _ } -> __TODO_pat__ p.span "tuple 1" - | PConstruct { name = `TupleCons n; args } -> - C.AST.TuplePat (List.map ~f:(fun { pat } -> ppat pat) args) - | PConstruct { name; args; is_record = true } -> + | PConstruct { name = `TupleCons _n; args; _ } -> + C.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) args) + | PConstruct { name; args; is_record = true; _ } -> C.AST.RecordPat (pglobal_ident name, pfield_pats args) - | PConstruct { name; args; is_record = false } -> + | PConstruct { name; args; is_record = false; _ } -> C.AST.ConstructorPat (pglobal_ident name, List.map ~f:(fun p -> ppat p.pat) args) | PConstant { lit } -> C.AST.Lit (pliteral p.span lit) - | PDeref { subpat } -> __TODO_pat__ p.span "deref" | _ -> . and pfield_pats (args : field_pat list) : (string * C.AST.pat) list = @@ -274,26 +271,27 @@ struct let span = e.span in match e.e with | Literal l -> C.AST.Const (pliteral e.span l) - | LocalVar local_ident -> C.AST.Name local_ident.name + | LocalVar local_ident -> C.AST.NameTerm local_ident.name | GlobalVar (`TupleCons 0) - | Construct { constructor = `TupleCons 0; fields = [] } -> + | Construct { constructor = `TupleCons 0; fields = []; _ } -> C.AST.UnitTerm | GlobalVar global_ident -> C.AST.Var (pglobal_ident global_ident) | App { - f = { e = GlobalVar (`Projector (`TupleField (n, len))) }; - args = [ arg ]; + 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 Error.assertion_failure span "expr: function application: bad arity"; - let args = List.map ~f:pexpr args in + let args = List.map ~f:(fun x -> C.AST.Value (pexpr x, true, 0)) args in C.AST.AppFormat (op, args) (* | App { f = { e = GlobalVar x }; args } -> *) (* __TODO_term__ span "GLOBAL APP?" *) - | App { f; args } -> + | App { f; args; _ } -> let base = pexpr f in let args = List.map ~f:pexpr args in C.AST.App (base, args) @@ -303,46 +301,53 @@ struct pexpr then_, Option.value_map else_ ~default:(C.AST.Literal "()") ~f:pexpr ) | Array l -> C.AST.Array (List.map ~f:pexpr l) - | Let { lhs; rhs; body; monadic = Some monad } -> + | Let { lhs; rhs; body; monadic } -> C.AST.Let { pattern = ppat lhs; + mut = + (match lhs.p with + | PBinding { mut = Mutable _; _ } -> true + | _ -> false); value = pexpr rhs; body = pexpr body; value_typ = pty span lhs.typ; + monad_typ = + Option.map + ~f:(fun (m, _) -> + match m with + | MException typ -> C.AST.Exception (pty span typ) + | MResult typ -> C.AST.Result (pty span typ) + | MOption -> C.AST.Option) + monadic; } - | Let { lhs; rhs; body; monadic = None } -> - C.AST.Let - { - pattern = ppat lhs; - value = pexpr rhs; - body = pexpr body; - value_typ = pty span lhs.typ; - } - | EffectAction _ -> __TODO_term__ span "monadic action" | Match { scrutinee; arms } -> 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 { e; typ } -> __TODO_term__ span "asciption" - | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; base } -> + | Ascription _ -> __TODO_term__ span "asciption" + | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> pexpr e - | Construct { constructor = `TupleCons n; fields; base } -> + | Construct { constructor = `TupleCons _n; fields; _ } -> C.AST.Tuple (List.map ~f:(snd >> pexpr) fields) - | Construct { is_record = true; constructor; fields; base } -> + | Construct { is_record = true; constructor; fields; _ } -> + (* TODO: handle base *) C.AST.RecordConstructor - ( C.AST.Var (pglobal_ident constructor), + ( pglobal_ident constructor, List.map ~f:(fun (f, e) -> (pglobal_ident f, pexpr e)) fields ) - | Construct { is_record = false; constructor; fields = [ (f, e) ]; base } -> + | Construct { is_record = false; constructor; fields = [ (_f, e) ]; _ } -> C.AST.App (C.AST.Var (pglobal_ident constructor), [ pexpr e ]) - | Construct { constructor; fields; base } -> + | Construct { constructor; _ } -> + (* __TODO_term__ span "constructor" *) C.AST.Var - (pglobal_ident constructor ^ snd (C.ty_to_string (pty span e.typ))) - | Closure { params; body } -> + (pglobal_ident constructor + ^ C.ty_to_string_without_paren (pty span e.typ)) + | Closure { params; body; _ } -> C.AST.Lambda (List.map ~f:ppat params, pexpr body) - | MacroInvokation { macro; args; witness } -> + | MacroInvokation { macro; _ } -> Error.raise @@ { kind = UnsupportedMacro { id = [%show: global_ident] macro }; @@ -350,44 +355,57 @@ struct } | _ -> . + let pgeneric_param_as_argument span : generic_param -> C.AST.argument = + function + | { ident; kind = GPType { default }; _ } -> + C.AST.Explicit + ( C.AST.Ident ident.name, + match default with Some t -> pty span t | None -> C.AST.WildTy ) + | _ -> Error.unimplemented ~details:"Coq: TODO: generic_params" span + let rec pitem (e : item) : C.AST.decl list = try pitem_unwrapped e with Diagnostics.SpanFreeError.Exn _ -> [ C.AST.Unimplemented "item error backend" ] - and pgeneric_param span : generic_param -> _ = function - | { ident; kind = GPType _; _ } -> ident.name - | _ -> Error.unimplemented ~details:"Coq: TODO: generic_params" span - and pitem_unwrapped (e : item) : C.AST.decl list = let span = e.span in match e.v with - | Fn { name; generics; body; params } -> + | Fn { name; body; params; _ } -> [ C.AST.Definition ( pconcrete_ident name, List.map - ~f:(fun { pat; typ; typ_span } -> (ppat pat, pty span typ)) + ~f:(fun { pat; typ; _ } -> + C.AST.Explicit (ppat pat, pty span typ)) params, pexpr body, pty span body.typ ); ] - | TyAlias { name; generics; ty } -> - [ C.AST.Notation (pconcrete_ident name ^ "_t", pty span ty) ] + | TyAlias { name; ty; _ } -> + [ + C.AST.Notation + ( "'" ^ pconcrete_ident name ^ "_t" ^ "'", + C.AST.Type (pty span ty), + None ); + ] (* record *) | Type { name; generics; variants = [ v ]; is_struct = true } -> [ (* TODO: generics *) C.AST.Record ( U.Concrete_ident_view.to_definition_name name, - p_record_record span v.arguments ); + List.map ~f:(pgeneric_param_as_argument span) generics.params, + List.map + ~f:(fun (x, y) -> C.AST.Named (x, y)) + (p_record_record span v.arguments) ); ] (* enum *) - | Type { name; generics; variants } -> + | Type { name; generics; variants; _ } -> [ C.AST.Inductive ( U.Concrete_ident_view.to_definition_name name, - List.map ~f:(pgeneric_param span) generics.params, + List.map ~f:(pgeneric_param_as_argument span) generics.params, p_inductive span variants name ); ] (* TODO: this is never matched, now *) @@ -404,7 +422,7 @@ struct (* ( C.AST.Name (U.Concrete_ident_view.to_definition_name name), *) (* C.AST.Name (U.Concrete_ident_view.to_definition_name name) ) ); *) (* ] *) - | IMacroInvokation { macro; argument; span } -> ( + | IMacroInvokation { macro; argument; _ } -> ( let unsupported () = let id = [%show: concrete_ident] macro in Error.raise { kind = UnsupportedMacro { id }; span = e.span } @@ -419,17 +437,20 @@ struct in [ C.AST.Notation - ( o.type_name ^ "_t", - C.AST.NatMod - (o.type_of_canvas, o.bit_size_of_field, o.modulo_value) - ); + ( "'" ^ o.type_name ^ "_t" ^ "'", + C.AST.Type + (C.AST.NatMod + ( o.type_of_canvas, + o.bit_size_of_field, + o.modulo_value )), + None ); C.AST.Definition ( o.type_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.Name (o.type_name ^ "_t"), - C.AST.Name (o.type_name ^ "_t") ) ); + ( C.AST.NameTy (o.type_name ^ "_t"), + C.AST.NameTy (o.type_name ^ "_t") ) ); ] | "bytes" -> let open Hacspeclib_macro_parser in @@ -438,17 +459,19 @@ struct in [ C.AST.Notation - ( o.bytes_name ^ "_t", - C.AST.ArrayTy - ( C.AST.Int { size = C.AST.U8; signed = false }, - (* int_of_string *) o.size ) ); + ( "'" ^ o.bytes_name ^ "_t" ^ "'", + C.AST.Type + (C.AST.ArrayTy + ( C.AST.Int { size = C.AST.U8; signed = false }, + (* int_of_string *) o.size )), + None ); C.AST.Definition ( o.bytes_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.Name (o.bytes_name ^ "_t"), - C.AST.Name (o.bytes_name ^ "_t") ) ); + ( C.AST.NameTy (o.bytes_name ^ "_t"), + C.AST.NameTy (o.bytes_name ^ "_t") ) ); ] | "unsigned_public_integer" -> let open Hacspeclib_macro_parser in @@ -457,17 +480,19 @@ struct in [ C.AST.Notation - ( o.integer_name ^ "_t", - C.AST.ArrayTy - ( C.AST.Int { size = C.AST.U8; signed = false }, - Int.to_string ((o.bits + 7) / 8) ) ); + ( "'" ^ o.integer_name ^ "_t" ^ "'", + C.AST.Type + (C.AST.ArrayTy + ( C.AST.Int { size = C.AST.U8; signed = false }, + Int.to_string ((o.bits + 7) / 8) )), + None ); C.AST.Definition ( o.integer_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.Name (o.integer_name ^ "_t"), - C.AST.Name (o.integer_name ^ "_t") ) ); + ( C.AST.NameTy (o.integer_name ^ "_t"), + C.AST.NameTy (o.integer_name ^ "_t") ) ); ] | "public_bytes" -> let open Hacspeclib_macro_parser in @@ -480,14 +505,15 @@ struct (* int_of_string *) o.size ) in [ - C.AST.Notation (o.bytes_name ^ "_t", typ); + C.AST.Notation + ("'" ^ o.bytes_name ^ "_t" ^ "'", C.AST.Type typ, None); C.AST.Definition ( o.bytes_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.Name (o.bytes_name ^ "_t"), - C.AST.Name (o.bytes_name ^ "_t") ) ); + ( C.AST.NameTy (o.bytes_name ^ "_t"), + C.AST.NameTy (o.bytes_name ^ "_t") ) ); ] | "array" -> let open Hacspeclib_macro_parser in @@ -510,22 +536,24 @@ struct in [ C.AST.Notation - ( o.array_name ^ "_t", - C.AST.ArrayTy - ( C.AST.Int { size = typ; signed = false }, - (* int_of_string *) o.size ) ); + ( "'" ^ o.array_name ^ "_t" ^ "'", + C.AST.Type + (C.AST.ArrayTy + ( C.AST.Int { size = typ; signed = false }, + (* int_of_string *) o.size )), + None ); C.AST.Definition ( o.array_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.Name (o.array_name ^ "_t"), - C.AST.Name (o.array_name ^ "_t") ) ); + ( C.AST.NameTy (o.array_name ^ "_t"), + C.AST.NameTy (o.array_name ^ "_t") ) ); ] | _ -> unsupported ()) | _ -> unsupported ()) | Use { path; is_external; rename } -> - if is_external then [] else [ C.AST.Require (path, rename) ] + if is_external then [] else [ C.AST.Require (None, path, rename) ] | HaxError s -> [ __TODO_item__ span s ] | NotImplementedYet -> [ __TODO_item__ span "Not implemented yet?" ] | Alias _ -> [ __TODO_item__ span "Not implemented yet? alias" ] @@ -533,29 +561,25 @@ struct [ C.AST.Class ( U.Concrete_ident_view.to_definition_name name, + List.map + ~f:(pgeneric_param_as_argument span) + (match List.rev generics.params with + | _ :: xs -> List.rev xs + | _ -> []), List.map ~f:(fun x -> - ( U.Concrete_ident_view.to_definition_name x.ti_ident, - match x.ti_v with - | TIFn fn_ty -> pty span fn_ty - | _ -> __TODO_ty__ span "field_ty" )) - items, - List.fold_left ~init:[] - ~f:(fun a b -> - a - @ [ - (match b with - | { ident; kind = GPType _; _ } -> ident.name - | _ -> - Error.unimplemented - ~details:"Coq: TODO: generic_params" span); - ]) - generics.params ); + C.AST.Named + ( U.Concrete_ident_view.to_definition_name x.ti_ident, + match x.ti_v with + | TIFn fn_ty -> pty span fn_ty + | _ -> __TODO_ty__ span "field_ty" )) + items ); ] | Impl { generics; self_ty; of_trait = name, gen_vals; items } -> [ C.AST.Instance ( pglobal_ident name, + List.map ~f:(pgeneric_param_as_argument span) generics.params, pty span self_ty, args_ty span gen_vals, List.map @@ -564,8 +588,8 @@ struct | IIFn { body; params } -> ( U.Concrete_ident_view.to_definition_name x.ii_ident, List.map - ~f:(fun { pat; typ; typ_span } -> - (ppat pat, pty span typ)) + ~f:(fun { pat; typ; _ } -> + C.AST.Explicit (ppat pat, pty span typ)) params, pexpr body, pty span body.typ ) @@ -577,8 +601,8 @@ struct items ); ] - and p_inductive span variants parrent_name : C.AST.inductive_case list = - List.map variants ~f:(fun { name; arguments; is_record } -> + and p_inductive span variants _parrent_name : C.AST.inductive_case list = + List.map variants ~f:(fun { name; arguments; is_record; _ } -> if is_record then C.AST.InductiveCase ( U.Concrete_ident_view.to_definition_name name, @@ -588,7 +612,7 @@ struct let name = U.Concrete_ident_view.to_definition_name name in match arguments with | [] -> C.AST.BaseCase name - | [ (arg_name, arg_ty, _arg_attrs) ] -> + | [ (_arg_name, arg_ty, _arg_attrs) ] -> C.AST.InductiveCase (name, pty span arg_ty) | _ -> C.AST.InductiveCase @@ -613,21 +637,6 @@ struct (* :: p_inductive span xs parrent_name *) (* | _ -> [] *) - and p_record span variants parrent_name : (string * C.AST.ty) list = - match variants with - | { name; arguments = [ (arg_name, arg_ty, _arg_attrs) ] } :: xs -> - (U.Concrete_ident_view.to_definition_name arg_name, pty span arg_ty) - :: p_record span xs parrent_name - | { name; arguments = [] } :: xs -> - ("TODO FIELD?", __TODO_ty__ span "TODO") - :: p_record span xs parrent_name - | { name; arguments } :: xs -> - ( U.Concrete_ident_view.to_definition_name name, - C.AST.RecordTy (pconcrete_ident name, p_record_record span arguments) - ) - :: p_record span xs parrent_name - | _ -> [] - and p_record_record span arguments : (string * C.AST.ty) list = List.map ~f:(function @@ -651,7 +660,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" @@ -664,13 +673,13 @@ let hardcoded_coq_headers = Open Scope Z_scope.\n\ Open Scope bool_scope.\n" -let translate _ (bo : BackendOptions.t) (items : AST.item list) : +let translate _ (_bo : BackendOptions.t) (items : AST.item list) : Types.file list = U.group_items_by_namespace items |> Map.to_alist |> List.map ~f:(fun (ns, items) -> let mod_name = - String.concat ~sep:"." + String.concat ~sep:"_" (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) @@ -709,6 +718,6 @@ module TransformToInputLanguage = ] [@ocamlformat "disable"] -let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) : +let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) : AST.item list = TransformToInputLanguage.ditems items diff --git a/engine/backends/coq/coq/dune b/engine/backends/coq/coq/dune index 60156b294..131beb9c0 100644 --- a/engine/backends/coq/coq/dune +++ b/engine/backends/coq/coq/dune @@ -17,4 +17,4 @@ (env (_ (flags - (:standard -warn-error -A -warn-error +8)))) + (:standard -w -A)))) diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml index 1684abac5..1fd848982 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/engine/backends/coq/coq_ast.ml @@ -5,9 +5,9 @@ open Base module type Library = sig module Notation : sig val int_repr : string -> string -> string - val let_stmt : string -> string -> string -> string -> int -> string - val let_mut_stmt : string -> string -> string -> string -> int -> string - val tuple_prefix : string + val type_str : string + val bool_str : string + val unit_str : string end end @@ -21,18 +21,22 @@ functor type int_type = { size : int_size; signed : bool } type ty = - | Wild + | WildTy | Bool | Unit + | TypeTy | Int of int_type - | Name of string + | NameTy of string | RecordTy of string * (string * ty) list | Product of ty list + | Coproduct of ty list | Arrow of ty * ty | ArrayTy of ty * string (* int *) | SliceTy of ty - | AppTy of string * ty list + | AppTy of ty * ty list | NatMod of string * int * string + | Forall of string list * string list * ty + | Exists of string list * string list * ty type literal = | Const_string of string @@ -41,7 +45,7 @@ functor | Const_bool of bool type pat = - | Wild + | WildPat | UnitPat | Ident of string | Lit of literal @@ -51,42 +55,87 @@ functor | AscriptionPat of pat * ty | DisjunctivePat of pat list + type monad_type = Option | Result of ty | Exception of ty + type term = | UnitTerm - | Let of { pattern : pat; value : term; body : term; value_typ : ty } + | Let of let_args | If of term * term * term | Match of term * (pat * term) list | Const of literal | Literal of string - | AppFormat of string list * term list + | AppFormat of string list * notation_elements list | App of term * term list | Var of string - | Name of string - | RecordConstructor of term * (string * term) list + | NameTerm of string + | RecordConstructor of string * (string * term) list + | RecordUpdate of string * term * (string * term) list | Type of ty | Lambda of pat list * term | Tuple of term list | Array of term list + | TypedTerm of term * ty + + and notation_elements = + | Newline of int + | Typing of ty * bool * int + | Variable of pat * int + | Value of term * bool * int + + and let_args = { + pattern : pat; + mut : bool; + value : term; + body : term; + value_typ : ty; + monad_typ : monad_type option; + } (* TODO: I don't get why you've got InductiveCase VS BaseCase. Why not an inductive case (i.e. a variant, right?) is a name + a list of types? *) type inductive_case = InductiveCase of string * ty | BaseCase of string - type definition_type = string * (pat * ty) list * term * ty - type generics_type = string list + + type argument = + | Implicit of pat * ty + | Explicit of pat * ty + | Typeclass of string option * ty + + (* name, arguments, body, type *) + type definition_type = string * argument list * term * ty + type record_field = Named of string * ty | Coercion of string * ty + + type instance_decl = + | InlineDef of definition_type + | LetDef of definition_type + + type instance_decls = + | InstanceDecls of instance_decl list + | TermDef of term type decl = + | MultipleDecls of decl list | Unimplemented of string + | Comment of string | Definition of definition_type | ProgramDefinition of definition_type - | Notation of string * ty - | Record of string * (string * ty) list - | Inductive of string * generics_type * inductive_case list - | Class of string * (string * ty) list * generics_type - | Instance of string * ty * ty list * definition_type list - | Require of string list * string option + | Equations of definition_type + | EquationsQuestionmark of definition_type + | Notation of string * term * string option + | Record of string * argument list * record_field list + | Inductive of string * argument list * inductive_case list + | Class of string * argument list * record_field list + | Instance of + string * argument list * ty * ty list * definition_type list + | ProgramInstance of + string * argument list * ty * ty list * instance_decls + | Require of string option * string list * string option + | ModuleType of string * argument list * record_field list + | Module of string * string * argument list * record_field list + | Parameter of string * ty (* definition_type minus 'term' *) + | HintUnfold of string * ty option end let __TODO_pat__ s = AST.Ident (s ^ " todo(pat)") - let __TODO_ty__ s : AST.ty = AST.Name (s ^ " todo(ty)") + let __TODO_ty__ s : AST.ty = AST.NameTy (s ^ " todo(ty)") let __TODO_term__ s = AST.Const (AST.Const_string (s ^ " todo(term)")) let __TODO_item__ s = AST.Unimplemented (s ^ " todo(item)") @@ -99,176 +148,263 @@ functor | AST.U128 -> "128" | AST.USize -> "32" - let rec ty_to_string (x : AST.ty) : AST.decl list * string = + let rec ty_to_string (x : AST.ty) : string * bool = match x with - | AST.Wild -> ([], "_") - | AST.Bool -> ([], "bool") - | AST.Unit -> ([], "unit") - | AST.Int { size = AST.USize; signed } -> ([], "uint_size") - | AST.Int { size; signed } -> ([], "int" ^ int_size_to_string size) - | AST.Name s -> ([], s) - | AST.RecordTy (name, fields) -> ([ AST.Record (name, fields) ], name) - | AST.Product [] -> ([], "unit") + | AST.WildTy -> ("_", false) + | AST.Bool -> (Lib.Notation.bool_str, false) + | AST.Coproduct [] -> ("⊥", false) + | AST.Coproduct l -> + let ty_str = + String.concat + ~sep:(" " ^ "∐" ^ " ") + (List.map ~f:ty_to_string_without_paren l) + in + (ty_str, true) + | AST.Product [] | AST.Unit -> + (Lib.Notation.unit_str, false (* TODO: might need paren *)) + | AST.TypeTy -> (Lib.Notation.type_str, false (* TODO: might need paren *)) + | AST.Int { size = AST.USize; _ } -> ("uint_size", false) + | AST.Int { size; _ } -> ("int" ^ int_size_to_string size, false) + | AST.NameTy s -> (s, false) + | AST.RecordTy (name, _fields) -> + (* [ AST.Record (name, fields) ] *) (name, false) | AST.Product l -> - let p_decl, p_str = product_to_string l (" " ^ "×" ^ " ") in - (p_decl, "(" ^ p_str ^ ")") + let ty_str = + String.concat + ~sep:(" " ^ "×" ^ " ") + (List.map ~f:ty_to_string_without_paren l) + in + (ty_str, true) | AST.Arrow (a, b) -> - let a_ty_def, a_ty_str = ty_to_string a in - let b_ty_def, b_ty_str = ty_to_string b in - (a_ty_def @ b_ty_def, a_ty_str ^ " " ^ "->" ^ " " ^ b_ty_str) + let a_ty_str = ty_to_string_without_paren a in + let b_ty_str = ty_to_string_without_paren b in + (a_ty_str ^ " " ^ "->" ^ " " ^ b_ty_str, true) | AST.ArrayTy (t, l) -> - let ty_def, ty_str = ty_to_string t in - (ty_def, "nseq" ^ " " ^ ty_str ^ " " ^ (* Int.to_string *) l) + let ty_str = ty_to_string_with_paren t in + ("nseq" ^ " " ^ ty_str ^ " " ^ (* Int.to_string *) l, true) | AST.SliceTy t -> - let ty_def, ty_str = ty_to_string t in - (ty_def, "seq" ^ " " ^ ty_str) - | AST.AppTy (i, []) -> ([], i) - | AST.AppTy (i, [ y ]) -> - let ty_defs, ty_str = ty_to_string y in - (ty_defs, i ^ " " ^ ty_str) + let ty_str = ty_to_string_with_paren t in + ("seq" ^ " " ^ ty_str, true) + | AST.AppTy (i, []) -> ty_to_string i + (* | AST.AppTy (i, [ y ]) -> *) + (* let ty_defs, ty_str = ty_to_string y in *) + (* (ty_defs, i ^ " " ^ ty_str) *) | AST.AppTy (i, p) -> - let ty_def, ty_str = product_to_string p ") (" in - (ty_def, i ^ " " ^ "(" ^ ty_str ^ ")") - | AST.NatMod (t, i, s) -> - ( [ - AST.Notation - ( t, - AST.ArrayTy - (AST.Int { size = U8; signed = false }, Int.to_string i) ); - ], - "nat_mod 0x" ^ s ) + let ty_str = + String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren p) + in + (ty_to_string_without_paren i ^ " " ^ ty_str, true) + | AST.NatMod (_t, _i, s) -> + (* [ *) + (* AST.Notation *) + (* ( t, *) + (* AST.ArrayTy *) + (* (AST.Int { size = U8; signed = false }, Int.to_string i) ); *) + (* ] *) + ("nat_mod 0x" ^ s, true) + | AST.Forall ([], [], ty) -> ty_to_string ty + | AST.Forall (implicit_vars, [], ty) -> + ( "forall" ^ " " ^ "{" + ^ String.concat ~sep:" " implicit_vars + ^ "}" ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) + | AST.Forall ([], vars, ty) -> + ( "forall" ^ " " + ^ String.concat ~sep:" " vars + ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) + | AST.Forall (implicit_vars, vars, ty) -> + ( "forall" ^ " " ^ "{" + ^ String.concat ~sep:" " implicit_vars + ^ "}" ^ "," ^ " " + ^ String.concat ~sep:" " vars + ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) + | AST.Exists ([], [], ty) -> ty_to_string ty + | AST.Exists (implicit_vars, [], ty) -> + ( "exists" ^ " " ^ "{" + ^ String.concat ~sep:" " implicit_vars + ^ "}" ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) + | AST.Exists ([], vars, ty) -> + ( "exists" ^ " " + ^ String.concat ~sep:" " vars + ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) + | AST.Exists (implicit_vars, vars, ty) -> + ( "exists" ^ " " ^ "{" + ^ String.concat ~sep:" " implicit_vars + ^ "}" ^ "," ^ " " + ^ String.concat ~sep:" " vars + ^ "," ^ " " + ^ ty_to_string_without_paren ty, + true ) | _ -> . - and product_to_string (x : AST.ty list) (sep : string) : - AST.decl list * string = - match x with - | [ y ] -> ty_to_string y - | y :: ys -> - let ty_defs, ty_str = ty_to_string y in - let ys_defs, ys_str = product_to_string ys sep in - (ty_defs @ ys_defs, ty_str ^ sep ^ ys_str) - | [] -> ([], "") - (* and record_fields_to_string (x : (string * AST.ty) list) : AST.decl list * string = *) - (* match x with *) - (* | (name, ty) :: xs -> *) - (* let ty_def, ty_str = ty_to_string ty in *) - (* let xs_def, xs_str = record_fields_to_string xs in *) - (* ty_def @ xs_def, newline_indent 1 ^ name ^ ":" ^ " " ^ ty_str ^ ";" ^ xs_str *) - (* | _ -> [], "" *) + and ty_to_string_with_paren (x : AST.ty) : string = + let s, b = ty_to_string x in + if b then "(" ^ s ^ ")" else s + + and ty_to_string_without_paren (x : AST.ty) : string = + let s, _ = ty_to_string x in + s let literal_to_string (x : AST.literal) : string = match x with | Const_string s -> s | Const_char c -> Int.to_string c (* TODO *) - | Const_int (i, { size; signed }) -> + | Const_int (i, { size; _ }) -> Lib.Notation.int_repr (int_size_to_string size) i (* *) | Const_bool b -> Bool.to_string b let rec pat_to_string (x : AST.pat) (is_top_expr : bool) depth : string = match x with - | AST.Wild -> "_" + | AST.WildPat -> "_" | AST.UnitPat -> tick_if is_top_expr ^ "tt" | AST.Ident s -> s | AST.Lit l -> literal_to_string l | AST.ConstructorPat (name, args) -> name ^ " " ^ String.concat ~sep:" " - @@ List.map ~f:(fun pat -> pat_to_string pat true depth) args - | AST.RecordPat (name, args) -> + @@ List.map ~f:(fun pat -> pat_to_string pat false depth) args + | AST.RecordPat (_name, []) -> "(* Empty Record *)" (* TODO *) + | AST.RecordPat (_name, args) -> (* name ^ " " ^ *) "{|" - ^ record_pat_to_string args (depth + 1) + ^ String.concat ~sep:";" + (List.map + ~f:(fun (name, pat) -> + newline_indent (depth + 1) + ^ name ^ " " ^ ":=" ^ " " + ^ pat_to_string pat true (depth + 1)) + args) ^ newline_indent depth ^ "|}" + | AST.TuplePat [] -> "_" (* TODO: empty tuple pattern? *) + | AST.TuplePat [ v ] -> pat_to_string v is_top_expr (depth + 1) | AST.TuplePat vals -> - tick_if is_top_expr ^ "(" ^ tuple_pat_to_string vals (depth + 1) ^ ")" + tick_if is_top_expr ^ "(" + ^ String.concat ~sep:"," + (List.map ~f:(fun t -> pat_to_string t false (depth + 1)) vals) + ^ ")" | AST.AscriptionPat (p, ty) -> - pat_to_string p true depth (* TODO: Should this be true of false? *) + "(" ^ pat_to_string p true depth ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ ")" (* TODO: Should this be true of false? *) | AST.DisjunctivePat pats -> let f pat = pat_to_string pat true depth in String.concat ~sep:" | " @@ List.map ~f pats and tick_if is_top_expr = if is_top_expr then "'" else "" - and tuple_pat_to_string vals depth = - match vals with - | [ t ] -> pat_to_string t false depth - | t :: ts -> - pat_to_string t false depth ^ "," ^ tuple_pat_to_string ts depth - | [] -> "todo empty tuple pattern?" - - and record_pat_to_string args depth : string = - match args with - | (name, pat) :: xs -> - newline_indent depth ^ name ^ " " ^ ":=" ^ " " - ^ pat_to_string pat true depth - ^ ";" - ^ record_pat_to_string xs depth - | _ -> "" - let rec term_to_string (x : AST.term) depth : string * bool = match x with | AST.UnitTerm -> ("tt", false) - | AST.Let { pattern = pat; value = bind; value_typ = typ; body = term } -> - let _, ty_str = ty_to_string typ in + | AST.Let { pattern = pat; value = bind; value_typ = typ; body = term; _ } + -> (* TODO: propegate type definition *) - ( Lib.Notation.let_stmt - (pat_to_string pat true depth) - (term_to_string_without_paren bind (depth + 1)) - ty_str - (term_to_string_without_paren term depth) - depth, + let var_str = pat_to_string pat true depth in + let expr_str = term_to_string_without_paren bind (depth + 1) in + let typ_str = ty_to_string_without_paren typ in + let body_str = term_to_string_without_paren term depth in + ( "let" ^ " " ^ var_str ^ " " ^ ":=" ^ " " ^ expr_str ^ " " ^ ":" + ^ " " ^ typ_str ^ " " ^ "in" ^ newline_indent depth ^ body_str, true ) | AST.If (cond, then_, else_) -> - ( "if" - ^ newline_indent (depth + 1) + ( "if" ^ " " ^ term_to_string_without_paren cond (depth + 1) - ^ newline_indent depth ^ "then" - ^ newline_indent (depth + 1) + ^ newline_indent depth ^ "then" ^ " " ^ term_to_string_without_paren then_ (depth + 1) - ^ newline_indent depth ^ "else" - ^ newline_indent (depth + 1) + ^ newline_indent depth ^ "else" ^ " " ^ term_to_string_without_paren else_ (depth + 1), true ) | AST.Match (match_val, arms) -> ( "match" ^ " " ^ term_to_string_without_paren match_val (depth + 1) - ^ " " ^ "with" ^ newline_indent depth ^ arm_to_string arms depth - ^ "end", + ^ " " ^ "with" ^ newline_indent depth + ^ String.concat ~sep:(newline_indent depth) + (List.map + ~f:(fun (pat, body) -> + "|" ^ " " + ^ pat_to_string pat true depth + ^ " " ^ "=>" + ^ newline_indent (depth + 1) + ^ term_to_string_without_paren body (depth + 1)) + arms) + ^ newline_indent depth ^ "end", false ) | AST.Const c -> (literal_to_string c, false) | AST.Literal s -> (s, false) | AST.AppFormat (format, args) -> ( format_to_string format - (List.map ~f:(fun x -> term_to_string_with_paren x depth) args), + (List.map + ~f:(function + | AST.Newline n -> newline_indent (depth + n) + | AST.Typing (typ, true, _n) -> ty_to_string_with_paren typ + | AST.Typing (typ, false, _n) -> + ty_to_string_without_paren typ + | AST.Value (x, true, n) -> + term_to_string_with_paren x (depth + n) + | AST.Value (x, false, n) -> + term_to_string_without_paren x (depth + n) + | AST.Variable (p, n) -> pat_to_string p true (depth + n)) + args), true (* TODO? Notation does not always need paren *) ) | AST.App (f, args) -> let f_s, f_b = term_to_string f depth in - (f_s ^ args_to_string args depth, f_b || List.length args > 0) + (f_s ^ term_list_to_string args depth, f_b || List.length args > 0) | AST.Var s -> (s, false) - | AST.Name s -> (s, false) + | AST.NameTerm s -> (s, false) | AST.RecordConstructor (f, args) -> - ( "Build_" - ^ term_to_string_without_paren f depth - ^ " " - ^ record_args_to_string args depth, + ( "Build_" ^ f + ^ (if List.length args > 0 then " " else "") + ^ String.concat ~sep:" " + (List.map + ~f:(fun (n, t) -> + "(" ^ n ^ " " ^ ":=" ^ " " + ^ term_to_string_without_paren t depth + ^ ")") + args), + true ) + | AST.RecordUpdate (f, base, args) -> + ( "Build_" ^ f ^ "[" + ^ term_to_string_without_paren base depth + ^ "]" + ^ (if List.length args > 0 then " " else "") + ^ String.concat ~sep:" " + (List.map + ~f:(fun (n, t) -> + "(" ^ n ^ " " ^ ":=" ^ " " + ^ term_to_string_without_paren t depth + ^ ")") + args), true ) | AST.Type t -> - let _, ty_str = ty_to_string t in + let ty_str = ty_to_string_with_paren t in (* TODO: Make definitions? *) - (ty_str, true (* TODO? does this always need paren? *)) + (ty_str, false (* TODO? does this always need paren? *)) | AST.Lambda (params, body) -> - ( "fun" - ^ lambda_params_to_string params depth - ^ " " ^ "=>" + ( String.concat ~sep:" " + (List.map + ~f:(fun x -> + "fun" ^ " " ^ pat_to_string x true depth ^ " " ^ "=>") + params) ^ newline_indent (depth + 1) ^ term_to_string_without_paren body (depth + 1), true ) + | AST.Tuple [] -> ("tt (* Empty tuple *)", false) (* TODO: Empty tuple? *) | AST.Tuple vals -> - ( Lib.Notation.tuple_prefix ^ "(" - ^ tuple_term_to_string vals (depth + 1) + ( "(" + ^ String.concat ~sep:"," + (List.map + ~f:(fun t -> term_to_string_without_paren t (depth + 1)) + vals) ^ ")", false ) - (* List.fold_left ~init:(term_to_string_without_paren t (depth+1)) ~f:(fun x y -> "(" ^ x ^ "," ^ term_to_string_without_paren y (depth+1) ^ ")") ts, false *) | AST.Array (t :: ts) -> ( "array_from_list" ^ " " ^ "[" ^ List.fold_left @@ -281,23 +417,12 @@ functor ^ "]", true ) | AST.Array [] -> ("!TODO empty array!", false) + | AST.TypedTerm (e, t) -> + ( term_to_string_without_paren e depth + ^ " " ^ ":" ^ " " ^ ty_to_string_with_paren t, + true ) | _ -> . - and tuple_term_to_string vals depth : string = - match vals with - | [ t ] -> term_to_string_without_paren t depth - | t :: ts -> - term_to_string_without_paren t depth - ^ "," - ^ tuple_term_to_string ts depth - | [] -> "!TODO empty tuple!" - - and lambda_params_to_string (params : AST.pat list) depth : string = - match params with - | x :: xs -> - " " ^ pat_to_string x true depth ^ lambda_params_to_string xs depth - | [] -> "" - and term_to_string_with_paren (x : AST.term) depth : string = let s, b = term_to_string x depth in if b then "(" ^ s ^ ")" else s @@ -312,177 +437,327 @@ functor match args with x :: xs -> f ^ x ^ format_to_string fs xs | [] -> f) | [] -> failwith "incorrect formatting" - and record_args_to_string (args : (string * AST.term) list) depth : string = - match args with - | (i, t) :: xs -> - term_to_string_with_paren t depth ^ record_args_to_string xs depth - | _ -> "" - - and args_to_string (args : AST.term list) depth : string = - match args with - | x :: xs -> - " " ^ term_to_string_with_paren x depth ^ args_to_string xs depth - | _ -> "" - - and arm_to_string (x : (AST.pat * AST.term) list) depth : string = - match x with - | (pat, body) :: xs -> - "|" ^ " " - ^ pat_to_string pat true depth - ^ " " ^ "=>" ^ " " - ^ term_to_string_without_paren body (depth + 1) - ^ newline_indent depth ^ arm_to_string xs depth - | _ -> "" + and term_list_to_string (terms : AST.term list) depth : string = + (if List.is_empty terms then "" else " ") + ^ String.concat ~sep:" " + (List.map ~f:(fun t -> term_to_string_with_paren t depth) terms) let rec decl_to_string (x : AST.decl) : string = match x with + | AST.MultipleDecls decls -> + String.concat ~sep:"\n" (List.map ~f:decl_to_string decls) | AST.Unimplemented s -> "(*" ^ s ^ "*)" - | AST.Definition (name, params, term, ty) -> - let definitions, ty_str = ty_to_string ty in - decl_list_to_string definitions - ^ "Definition" ^ " " ^ name ^ " " ^ params_to_string params ^ ":" - ^ " " ^ ty_str ^ " " ^ ":=" ^ newline_indent 1 - ^ term_to_string_without_paren term 1 - ^ "." - | AST.ProgramDefinition (name, params, term, ty) -> - let definitions, ty_str = ty_to_string ty in - decl_list_to_string definitions - ^ "Program" ^ " " ^ "Definition" ^ " " ^ name ^ " " - ^ params_to_string params ^ ":" ^ " " ^ ty_str ^ " " ^ ":=" - ^ newline_indent 1 - ^ term_to_string_without_paren term 1 - ^ " " ^ ":" ^ " " ^ ty_str ^ "." ^ newline_indent 0 ^ "Fail" ^ " " - ^ "Next" ^ " " ^ "Obligation." - | AST.Notation (name, ty) -> - let definitions, ty_str = ty_to_string ty in - decl_list_to_string definitions - ^ "Notation" ^ " " ^ name ^ " " ^ ":=" ^ " " ^ "(" ^ ty_str ^ ")" + | AST.Comment s -> "(**" ^ " " ^ s ^ " " ^ "**)" + | AST.Definition (name, arguments, term, ty) -> + "Definition" ^ " " + ^ definition_value_to_string (name, arguments, term, ty) + | AST.ProgramDefinition (name, arguments, term, ty) -> + "Program" ^ " " ^ "Definition" ^ " " + ^ definition_value_to_string (name, arguments, term, ty) + ^ fail_next_obligation + | AST.Equations (name, arguments, term, ty) -> + "Equations" ^ " " + ^ definition_value_to_equation_definition (name, arguments, term, ty) + | AST.EquationsQuestionmark (name, arguments, term, ty) -> + "Equations?" ^ " " + ^ definition_value_to_equation_definition (name, arguments, term, ty) + | AST.Notation (notation, value, extra) -> + "Notation" ^ " " ^ "\"" ^ notation ^ "\"" ^ " " ^ ":=" ^ " " + ^ term_to_string_with_paren value 0 + ^ (match extra with None -> "" | Some x -> " " ^ "(" ^ x ^ ")") ^ "." - | AST.Record (name, variants) -> - let definitions, variants_str = + | AST.Record (name, arguments, variants) -> + let variants_str = variants_to_string variants (newline_indent 1) ";" in - decl_list_to_string definitions - ^ "Record" ^ " " ^ name ^ " " ^ ":" ^ " " ^ "Type" ^ " " ^ ":=" ^ "{" - ^ variants_str ^ newline_indent 0 ^ "}." - | AST.Inductive (name, generics, variants) -> - let name_generics = - name ^ List.fold_left ~init:"" ~f:(fun a b -> a ^ " " ^ b) generics - in - let definitions, variants_str = - inductive_case_to_string variants - (newline_indent 0 ^ "|" ^ " ") - name_generics + "Record" ^ " " ^ name + ^ params_to_string_typed arguments + ^ " " ^ ":" ^ " " ^ "Type" ^ " " ^ ":=" ^ " " ^ "{" ^ variants_str + ^ newline_indent 0 ^ "}." + | AST.Inductive (name, arguments, variants) -> + let name_arguments = name ^ params_to_string_typed arguments in + let variants_str = + String.concat ~sep:(newline_indent 0) + (List.map + ~f:(fun x -> + let mid_str = + match x with + | AST.BaseCase ty_name -> ty_name ^ " : " + | AST.InductiveCase (ty_name, ty) -> + let ty_str = ty_to_string_with_paren ty in + ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ " " ^ "->" ^ " " + in + ("|" ^ " ") ^ mid_str ^ name_arguments) + variants) in - let _, args_str = - if List.is_empty generics then ([], "") + let args_str = + if List.is_empty arguments then "" else inductive_case_args_to_string variants (newline_indent 0 ^ "Arguments" ^ " ") - (List.fold_left ~init:"" ~f:(fun a b -> a ^ " {_}") generics) + (List.fold_left ~init:"" ~f:(fun a _ -> a ^ " {_}") arguments) "." in - decl_list_to_string definitions - ^ "Inductive" ^ " " ^ name_generics ^ " " ^ ":" ^ " " ^ "Type" ^ " " - ^ ":=" ^ variants_str ^ "." ^ args_str - | AST.Class (name, trait_items, generics) -> - let field_defs, field_str = - List.fold_left ~init:([], "") + "Inductive" ^ " " ^ name_arguments ^ " " ^ ":" ^ " " ^ "Type" ^ " " + ^ ":=" ^ newline_indent 0 ^ variants_str ^ "." ^ args_str + | AST.Class (name, arguments, trait_items) -> + let field_str = + List.fold_left ~init:"" ~f:(fun x y -> - let definitions, ty_str = ty_to_string (snd y) in - ( definitions @ fst x, - snd x ^ newline_indent 1 ^ fst y ^ ":" ^ ty_str ^ " " ^ ";" )) + let field_name, sep, field_ty = + match y with + | Named (field_name, field_ty) -> (field_name, ":", field_ty) + | Coercion (field_name, field_ty) -> + (field_name, ":>", field_ty) + (* Should be "::" in newer versions of coq *) + in + let ty_str = ty_to_string_with_paren field_ty in + x ^ newline_indent 1 ^ field_name ^ " " ^ sep ^ " " ^ ty_str + ^ " " ^ ";") trait_items in - let name_generics = - name ^ List.fold_left ~init:"" ~f:(fun a b -> a ^ " " ^ b) generics - in - decl_list_to_string field_defs - ^ "Class" ^ " " ^ name_generics ^ " " ^ ":=" ^ " " ^ "{" ^ field_str - ^ newline_indent 0 ^ "}" ^ "." - | AST.Instance (name, self_ty, ty_list, impl_list) -> - let ty_list_defs, ty_list_str = - List.fold_left ~init:([], "") + "Class" ^ " " ^ name ^ " " ^ "(Self : " + ^ ty_to_string_with_paren AST.TypeTy + ^ ")" + ^ params_to_string_typed arguments + ^ " " ^ ":=" ^ " " ^ "{" ^ field_str ^ newline_indent 0 ^ "}" ^ "." + | AST.ModuleType (name, arguments, trait_items) -> + let field_str = + List.fold_left ~init:"" ~f:(fun x y -> - let definitions, ty_str = ty_to_string y in - (definitions @ fst x, snd x ^ ty_str ^ " ")) - ty_list + x ^ newline_indent 1 + ^ + match y with + | Named (field_name, field_ty) -> + decl_to_string (AST.Parameter (field_name, field_ty)) + | Coercion (field_name, field_ty) -> + decl_to_string + (AST.Module + (field_name, ty_to_string_with_paren field_ty, [], [])) + (* Should be "::" in newer versions of coq *)) + trait_items + in + let arguments_str = params_to_string_typed arguments in + "Module Type" ^ " " ^ name ^ arguments_str ^ "." ^ newline_indent 1 + ^ field_str ^ newline_indent 0 ^ "End" ^ " " ^ name ^ "." + | AST.Parameter (name, typ) -> + String.concat ~sep:" " [ name; ":"; ty_to_string_without_paren typ ] + | AST.Module (name, typ, arguments, _trait_items) -> + let arguments_str = params_to_string_typed arguments in + "Module" ^ " " ^ name ^ arguments_str ^ " " ^ ":" ^ " " ^ typ ^ "." + ^ " " ^ "End" ^ " " ^ name ^ "." + | AST.Instance (name, arguments, self_ty, ty_list, impl_list) -> + let ty_list_str = + String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren ty_list) in let impl_str = List.fold_left ~init:"" - ~f:(fun x y -> - let name, params, term, ty = y in - x ^ newline_indent 1 ^ name ^ " " ^ params_to_string params - ^ ":=" ^ " " + ~f:(fun x (name, arguments, term, _ty) -> + x ^ newline_indent 1 ^ name + ^ params_to_string_typed arguments + ^ " " ^ ":=" ^ " " ^ term_to_string_without_paren term 1 ^ ";") impl_list in - let ty_defs, ty_str = ty_to_string self_ty in - decl_list_to_string (ty_list_defs @ ty_defs) - ^ "Instance" ^ " " ^ ty_str ^ "_" ^ name ^ " " ^ ":" ^ " " ^ name - ^ " " ^ ty_list_str ^ ":=" ^ " " ^ "{" ^ impl_str ^ newline_indent 0 - ^ "}" ^ "." - | AST.Require ([], rename) -> "" - | AST.Require (import :: imports, rename) -> ( - "Require Import" ^ " " - ^ map_first_letter String.uppercase import - (* (List.fold_left ~init:import ~f:(fun x y -> x ^ "." ^ y) imports) *) - ^ "." - ^ match rename with Some s -> " (* " ^ "as " ^ s ^ " *)" | _ -> "") - - and decl_list_to_string (x : AST.decl list) : string = - List.fold_right ~init:"" - ~f:(fun x y -> decl_to_string x ^ newline_indent 0 ^ y) - x - - and params_to_string params : string = - match params with - | (pat, ty) :: xs -> - let _, ty_str = ty_to_string ty in - "(" ^ pat_to_string pat true 0 ^ " " ^ ":" ^ " " ^ ty_str ^ ")" ^ " " - ^ params_to_string xs (* TODO: Should pat_to_string have tick here? *) - | [] -> "" - - and inductive_case_to_string variants pre post : AST.decl list * string = - match variants with - | x :: xs -> - let ty_def, mid_str = - match x with - | AST.BaseCase ty_name -> ([], ty_name) - | AST.InductiveCase (ty_name, ty) -> - let ty_definitions, ty_str = ty_to_string ty in - ( ty_definitions, - ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ " " ^ "->" ^ " " ) + let ty_str = ty_to_string_without_paren self_ty in + "#[global] Instance" ^ " " ^ ty_str ^ "_" ^ name + ^ params_to_string_typed arguments + ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":=" ^ " " ^ "{" + ^ impl_str ^ newline_indent 0 ^ "}" ^ "." + | AST.ProgramInstance + (name, arguments, self_ty, ty_list, InstanceDecls impl_list) -> + let ty_list_str = + String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren ty_list) in - let variant_definitions, variants_str = - inductive_case_to_string xs pre post + let impl_str, impl_str_empty = + let fl = + List.filter_map + ~f:(function + | LetDef (name, arguments, term, ty) -> + Some + ("let" ^ " " ^ name ^ " " ^ ":=" ^ " " + ^ (if List.is_empty arguments then "" + else + "fun" ^ " " + ^ params_to_string_typed arguments + ^ " " ^ "=>" ^ " ") + ^ term_to_string_without_paren term 1 + ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ " " ^ "in") + | _ -> None) + impl_list + in + (String.concat ~sep:(newline_indent 1) fl, List.is_empty fl) in - (ty_def @ variant_definitions, pre ^ mid_str ^ post ^ variants_str) - | [] -> ([], "") - - and inductive_case_args_to_string variants pre mid post : - AST.decl list * string = - List.fold_left ~init:([], "") - ~f:(fun y x -> - let mid_str, ty_str = - match x with - | AST.BaseCase ty_name -> (ty_name, "") - | AST.InductiveCase (ty_name, ty) -> - let _, ty_str = ty_to_string ty in - (ty_name, " " ^ ty_str) + let arg_str = + String.concat + ~sep:(";" ^ newline_indent 1) + (List.map + ~f:(function + | LetDef (name, _arguments, _term, _ty) -> + name ^ " " ^ ":=" ^ " " ^ "(" ^ "@" ^ name ^ ")" + | InlineDef (name, arguments, term, ty) -> + name ^ " " ^ ":=" ^ " " ^ "(" + ^ (if List.is_empty arguments then "" + else + "fun" ^ " " + ^ params_to_string_typed arguments + ^ " " ^ "=>" ^ " ") + ^ term_to_string_without_paren term 1 + ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ ")") + impl_list) in - match y with - | variant_definitions, variants_str -> - ( variant_definitions, - pre ^ mid_str ^ mid ^ ty_str ^ post ^ variants_str )) - variants - - and variants_to_string variants pre post : AST.decl list * string = - List.fold_left ~init:([], "") - ~f:(fun (variant_definitions, variants_str) (ty_name, ty) -> - let ty_definitions, ty_str = ty_to_string ty in - ( ty_definitions @ variant_definitions, - pre ^ ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ post ^ variants_str )) - variants + let ty_str = ty_to_string_without_paren self_ty in + "#[global] Program Instance" ^ " " ^ ty_str ^ "_" ^ name + ^ params_to_string_typed arguments + ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":=" + ^ newline_indent 1 ^ impl_str + ^ (if impl_str_empty then "" else newline_indent 1) + ^ (match impl_list with + | [] -> "_" + | _ -> "{|" (* ^ name ^ " " ^ ty_list_str *) ^ " " ^ arg_str ^ "|}") + ^ "." ^ fail_next_obligation + | AST.ProgramInstance (name, arguments, self_ty, ty_list, TermDef term) -> + let ty_list_str = + String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren ty_list) + in + let ty_str = ty_to_string_without_paren self_ty in + "#[global] Program Instance" ^ " " ^ ty_str ^ "_" ^ name + ^ params_to_string_typed arguments + ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":=" + ^ newline_indent 1 + ^ term_to_string_without_paren term 1 + ^ "." ^ fail_next_obligation + | AST.Require (_, [], _rename) -> "" + | AST.Require (None, import :: imports, rename) -> + (* map_first_letter String.uppercase import *) + let import_name = + match rename with + | Some s -> s + | _ -> + List.fold_left + ~init:(map_first_letter String.uppercase import) + ~f:(fun x y -> x ^ "_" ^ map_first_letter String.uppercase y) + imports + in + "Require Import" ^ " " ^ import_name ^ "." ^ newline_indent 0 + ^ "Export" ^ " " ^ import_name ^ "." + | AST.Require (Some x, imports, rename) -> + "From" ^ " " ^ x ^ " " + ^ decl_to_string (AST.Require (None, imports, rename)) + | AST.HintUnfold (n, Some typ) -> + let ty_str = ty_to_string_without_paren typ in + "Hint Unfold" ^ " " ^ ty_str ^ "_" ^ n ^ "." + | AST.HintUnfold (n, None) -> "Hint Unfold" ^ " " ^ n ^ "." + + and definition_value_to_equation_definition + ((name, arguments, term, ty) : AST.definition_type) = + let ty_str = ty_to_string_without_paren ty in + definition_value_to_shell_string + (name, arguments, term, ty) + (name ^ " " + ^ params_to_string + (List.filter_map + ~f:(fun x -> + match x with Explicit (y, z) -> Some (y, z) | _ -> None) + arguments) + ^ " " ^ ":=" ^ newline_indent 2 + ^ term_to_string_without_paren term 2 + ^ " " ^ ":" ^ " " ^ ty_str) + ^ fail_next_obligation + + and definition_value_to_shell_string + ((name, arguments, _, ty) : AST.definition_type) (body : string) : + string = + let ty_str = ty_to_string_without_paren ty in + name + ^ params_to_string_typed arguments + ^ " " ^ ":" ^ " " ^ ty_str ^ " " ^ ":=" ^ newline_indent 1 ^ body ^ "." + + and definition_value_to_string + ((name, arguments, term, ty) : AST.definition_type) : string = + definition_value_to_shell_string + (name, arguments, term, ty) + (term_to_string_without_paren term 1) + + and fail_next_obligation : string = + newline_indent 0 ^ "Fail" ^ " " ^ "Next" ^ " " ^ "Obligation." + + and params_to_string_typed params : string = + if List.is_empty params then "" + else + " " + ^ String.concat ~sep:" " + (List.map + ~f:(fun param -> + match param with + | Implicit (pat, ty) -> + "{" ^ pat_to_string pat true 0 ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ "}" + | Explicit (pat, ty) -> + "(" ^ pat_to_string pat true 0 ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ ")" + | Typeclass (None, ty) -> + "`{" ^ " " ^ ty_to_string_without_paren ty ^ "}" + | Typeclass (Some name, ty) -> + "`{" ^ name ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ "}") + params) + + and params_to_string params : string = + String.concat ~sep:"" + (List.map + ~f:(fun (pat, _ty) -> + (* let ty_str = ty_to_string_without_paren ty in *) + pat_to_string pat true 0 ^ " ") + params) + + (* and inductive_case_to_string variants pre post : string = *) + (* match variants with *) + (* | x :: xs -> *) + (* let mid_str = *) + (* match x with *) + (* | AST.BaseCase ty_name -> ty_name *) + (* | AST.InductiveCase (ty_name, ty) -> *) + (* let ty_str = ty_to_string ty in *) + (* ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ " " ^ "->" ^ " " *) + (* in *) + (* let variants_str = inductive_case_to_string xs pre post in *) + (* pre ^ mid_str ^ post ^ variants_str *) + (* | [] -> "" *) + + and inductive_case_args_to_string variants pre mid post : string = + String.concat ~sep:"" + (List.map + ~f:(fun x -> + let mid_str, ty_str = + match x with + | AST.BaseCase ty_name -> (ty_name, "") + | AST.InductiveCase (ty_name, ty) -> + (ty_name, " " ^ ty_to_string_with_paren ty) + in + pre ^ mid_str ^ mid ^ ty_str ^ post) + variants) + + and variants_to_string variants pre post : string = + String.concat ~sep:"" + (List.map + ~f:(fun y -> + let ty_name, _sep, ty = + match y with + | Named (ty_name, ty) -> (ty_name, ":", ty) + | Coercion (ty_name, ty) -> (ty_name, ":>", ty) + (* Should be "::" in newer versions of coq *) + in + pre ^ ty_name ^ " " ^ ":" ^ " " + ^ ty_to_string_without_paren ty + ^ post) + variants) end diff --git a/engine/backends/coq/dune b/engine/backends/coq/dune index 8d70c0971..4fda5dfbe 100644 --- a/engine/backends/coq/dune +++ b/engine/backends/coq/dune @@ -14,7 +14,12 @@ ppx_functor_application ppx_matches))) +; (env +; (_ +; (flags +; (:standard -warn-error -A -warn-error +8)))) + (env (_ (flags - (:standard -warn-error -A -warn-error +8)))) + (:standard -w +A)))) diff --git a/engine/backends/coq/ssprove/dune b/engine/backends/coq/ssprove/dune new file mode 100644 index 000000000..ee0600b3e --- /dev/null +++ b/engine/backends/coq/ssprove/dune @@ -0,0 +1,20 @@ +(library + (name ssprove_backend) + (package hax-engine) + (libraries hax_engine base hacspeclib_macro_parser coq_ast) + (preprocess + (pps + ppx_yojson_conv + ppx_sexp_conv + ppx_compare + ppx_hash + ppx_deriving.show + ppx_deriving.eq + ppx_inline + ppx_functor_application + ppx_matches))) + +(env + (_ + (flags + (:standard -w -A)))) diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml new file mode 100644 index 000000000..e4f6cf087 --- /dev/null +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -0,0 +1,2414 @@ +open Hax_engine +open Utils +open Base +open Coq_ast + +include + Backend.Make + (struct + open Features + include Off + include On.Slice + include On.Monadic_binding + include On.Macro + include On.Construct_base + include On.Mutable_variable + include On.Loop + include On.For_loop + include On.While_loop + include On.For_index_loop + include On.State_passing_loop + end) + (struct + let backend = Diagnostics.Backend.SSProve + end) + +module SubtypeToInputLanguage + (FA : Features.T + with type mutable_reference = Features.Off.mutable_reference + and type continue = Features.Off.continue + and type break = Features.Off.break + and type mutable_pointer = Features.Off.mutable_pointer + and type mutable_variable = Features.On.mutable_variable + and type reference = Features.Off.reference + and type raw_pointer = Features.Off.raw_pointer + and type early_exit = Features.Off.early_exit + and type question_mark = Features.Off.question_mark + and type as_pattern = Features.Off.as_pattern + and type lifetime = Features.Off.lifetime + and type monadic_action = Features.Off.monadic_action + and type arbitrary_lhs = Features.Off.arbitrary_lhs + and type nontrivial_lhs = Features.Off.nontrivial_lhs + and type block = Features.Off.block) = +struct + module FB = InputLanguage + + include + Subtype.Make (FA) (FB) + (struct + module A = FA + module B = FB + include Features.SUBTYPE.Id + include Features.SUBTYPE.On.Monadic_binding + include Features.SUBTYPE.On.Construct_base + include Features.SUBTYPE.On.Slice + include Features.SUBTYPE.On.Macro + include Features.SUBTYPE.On.Loop + include Features.SUBTYPE.On.For_loop + include Features.SUBTYPE.On.While_loop + include Features.SUBTYPE.On.For_index_loop + include Features.SUBTYPE.On.State_passing_loop + end) + + let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend)) +end + +module AST = Ast.Make (InputLanguage) +module BackendOptions = Backend.UnitBackendOptions +open Ast +module CoqNamePolicy = Concrete_ident.DefaultNamePolicy +module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy) +open AST + +module SSProveLibrary : Library = struct + module Notation = struct + let int_repr (_x : string) (i : string) : string = i + let type_str : string = "choice_type" + let bool_str : string = "'bool" + let unit_str : string = "'unit" + end +end + +module SSP = Coq (SSProveLibrary) + +module SSPExtraDefinitions (* : ANALYSIS *) = struct + let wrap_type_in_both (l : string) (i : string) (a : SSP.AST.ty) = + SSP.AST.AppTy (SSP.AST.NameTy ("both" ^ " " ^ l ^ " " ^ i), [ a ]) + + let unit_term : SSP.AST.term = + SSP.AST.TypedTerm (SSP.AST.UnitTerm, SSP.AST.Unit) + + let rec variables_of_ssp_pat (p : SSP.AST.pat) : string list = + match p with + | RecordPat (_, npl) -> List.concat_map ~f:(snd >> variables_of_ssp_pat) npl + | ConstructorPat (_, pl) -> List.concat_map ~f:variables_of_ssp_pat pl + | TuplePat pl -> List.concat_map ~f:variables_of_ssp_pat pl + | AscriptionPat (p, _) -> variables_of_ssp_pat p + | Ident x -> [ x ] + | DisjunctivePat pl -> List.concat_map ~f:variables_of_ssp_pat pl + | WildPat | UnitPat | Lit _ -> [] + + let letb + ({ pattern; mut; value; body; value_typ; monad_typ } : SSP.AST.let_args) : + SSP.AST.term = + match monad_typ with + | Some (Exception _typ) -> + SSP.AST.AppFormat + ( [ + "letm[choice_typeMonad.result_bind_code "; + (*typ*) + "] "; + (*p*) + " := "; + (*expr*) + " in"; + ""; + (*body*) + ""; + ], + [ + SSP.AST.Typing (value_typ, true, 0); + SSP.AST.Variable (pattern, 0); + SSP.AST.Value (value, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (body, false, 0); + ] ) + | Some (Result _typ) -> + SSP.AST.AppFormat + ( [ + "letm[choice_typeMonad.result_bind_code "; + (*typ*) + "] "; + (*p*) + " := "; + (*expr*) + " in"; + ""; + (*body*) + ""; + ], + [ + SSP.AST.Typing (value_typ, true, 0); + SSP.AST.Variable (pattern, 0); + SSP.AST.Value (value, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (body, false, 0); + ] ) + | Some Option -> + SSP.AST.AppFormat + ( [ + "letm[choice_typeMonad.option_bind_code] "; + (*p*) + " := "; + (*expr*) + " in"; + ""; + (*body*) + ""; + ], + [ + SSP.AST.Variable (pattern, 0); + SSP.AST.Value (value, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (body, false, 0); + ] ) + | None -> + if mut then + SSP.AST.AppFormat + ( [ + "letb "; + (*p*) + " loc(" (*p_loc*); + ") := "; + (*expr*) + " in"; + ""; + (*body*) + ""; + ], + [ + SSP.AST.Variable (pattern, 0); + SSP.AST.Variable + ( (match + List.map + ~f:(fun x -> SSP.AST.Ident (x ^ "_loc")) + (variables_of_ssp_pat pattern) + with + | [] -> SSP.AST.WildPat + | [ x ] -> x + | xs -> SSP.AST.TuplePat xs), + 0 ); + SSP.AST.Value (value, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (body, false, 0); + ] ) + else + SSP.AST.AppFormat + ( [ "letb "; (*p*) " := "; (*expr*) " in"; ""; (*body*) "" ], + [ + SSP.AST.Variable (pattern, 0); + SSP.AST.Value (value, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (body, false, 0); + ] ) + + let rec pat_as_expr (p : SSP.AST.pat) : (SSP.AST.pat * SSP.AST.term) option = + match p with + | WildPat | UnitPat -> None + | Ident s -> Some (SSP.AST.Ident s, SSP.AST.Var s) + | Lit l -> Some (SSP.AST.Lit l, Const l) + | RecordPat (s, sps) -> + let v = + List.filter_map + ~f:(fun (s, ps) -> + Option.map ~f:(fun (p, t) -> ((s, p), (s, t))) (pat_as_expr ps)) + sps + in + Some + ( SSP.AST.RecordPat (s, List.map ~f:fst v), + SSP.AST.RecordConstructor (s, List.map ~f:snd v) ) + | ConstructorPat (_, ps) | TuplePat ps -> + let pt_list = List.filter_map ~f:pat_as_expr ps in + Some + ( TuplePat (List.map ~f:fst pt_list), + SSP.AST.Tuple (List.map ~f:snd pt_list) ) + | AscriptionPat (p, _) -> pat_as_expr p (* TypedTerm (, t) *) + | DisjunctivePat ps -> + let pt_list = List.filter_map ~f:pat_as_expr ps in + Some + ( TuplePat (List.map ~f:fst pt_list), + SSP.AST.Tuple (List.map ~f:snd pt_list) ) + + let ifb ((cond, then_, else_) : SSP.AST.term * SSP.AST.term * SSP.AST.term) : + SSP.AST.term = + SSP.AST.AppFormat + ( [ "ifb "; (*expr*) ""; "then "; ""; "else "; "" ], + [ + SSP.AST.Value (cond, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (then_, false, 0); + SSP.AST.Newline 0; + SSP.AST.Value (else_, false, 0); + ] ) + + let matchb ((expr, arms) : SSP.AST.term * (SSP.AST.pat * SSP.AST.term) list) : + SSP.AST.term = + SSP.AST.AppFormat + ( [ "matchb "; (*expr*) " with" ] + @ List.concat_map ~f:(fun _ -> [ "| "; " =>"; ""; "" ]) arms + @ [ "end" ], + [ SSP.AST.Value (expr, false, 0); SSP.AST.Newline 0 ] + @ List.concat_map + ~f:(fun (arm_pat, body) -> + [ + SSP.AST.Variable (arm_pat, 0); + SSP.AST.Newline 1; + SSP.AST.Value (body, false, 1); + SSP.AST.Newline 0; + ]) + arms ) + + let updatable_record + ((name, arguments, variants) : + string * SSP.AST.argument list * SSP.AST.record_field list) : + SSP.AST.decl = + let fields = + List.concat_map + ~f:(function + | SSP.AST.Named (x, y) -> [ (x, y) ] | SSP.AST.Coercion _ -> []) + variants + in + let implicit_LI = + [ + SSP.AST.Implicit (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ] + in + let ty_name = + "(" + ^ String.concat ~sep:" " + (name + :: List.filter_map + ~f:(fun x -> + match x with + | SSP.AST.Explicit (p, _t) -> + Some (SSP.pat_to_string p false 0) + | _ -> None) + arguments) + ^ ")" + in + SSP.AST.MultipleDecls + ([ + SSP.AST.Definition + ( name, + arguments, + SSP.AST.Type (SSP.AST.Product (List.map ~f:snd fields)), + SSP.AST.TypeTy ); + ] + @ List.mapi + ~f:(fun i (x, y) -> + SSP.AST.Equations + ( x, + implicit_LI + @ List.map + ~f:(function + | SSP.AST.Explicit (a, b) -> SSP.AST.Implicit (a, b) + | v -> v) + arguments + @ [ + SSP.AST.Explicit + ( SSP.AST.Ident "s", + wrap_type_in_both "L" "I" (SSP.AST.NameTy name) ); + ], + SSP.AST.App + ( SSP.AST.Var "bind_both", + [ + SSP.AST.Var "s"; + SSP.AST.Lambda + ( [ SSP.AST.Ident "x" ], + SSP.AST.App + ( SSP.AST.Var "solve_lift", + [ + SSP.AST.App + ( SSP.AST.Var "ret_both", + [ + SSP.AST.TypedTerm + ( List.fold_right ~init:(SSP.AST.Var "x") + ~f:(fun x y -> + SSP.AST.App (SSP.AST.Var x, [ y ])) + ((if Stdlib.(i != 0) then [ "snd" ] + else []) + @ List.init + (List.length fields - 1 - i) + ~f:(fun _ -> "fst")), + y ); + ] ); + ] ) ); + ] ), + wrap_type_in_both "L" "I" y )) + fields + @ [ + SSP.AST.Equations + ( "Build_" ^ name, + List.mapi + ~f:(fun i _ -> + SSP.AST.Implicit + ( SSP.AST.Ident ("L" ^ Int.to_string i), + SSP.AST.NameTy "{fset Location}" )) + fields + @ List.mapi + ~f:(fun i _ -> + SSP.AST.Implicit + ( SSP.AST.Ident ("I" ^ Int.to_string i), + SSP.AST.NameTy "Interface" )) + fields + @ List.map + ~f:(function + | SSP.AST.Explicit (a, b) -> SSP.AST.Implicit (a, b) + | v -> v) + arguments + @ List.mapi + ~f:(fun i (x, y) -> + SSP.AST.Implicit + ( SSP.AST.Ident x, + wrap_type_in_both + ("L" ^ Int.to_string i) + ("I" ^ Int.to_string i) + y )) + fields, + List.fold_left + ~init: + (SSP.AST.App + ( SSP.AST.Var "solve_lift", + [ + SSP.AST.App + ( SSP.AST.Var "ret_both", + [ + SSP.AST.TypedTerm + ( SSP.AST.Tuple + (List.map + ~f:(fst >> fun x -> SSP.AST.Var x) + fields), + SSP.AST.NameTy ty_name ); + ] ); + ] )) + ~f:(fun z (x, _y) -> + SSP.AST.App + ( SSP.AST.Var "bind_both", + [ SSP.AST.Var x; SSP.AST.Lambda ([ SSP.AST.Ident x ], z) ] + )) + fields, + let lis = + String.concat ~sep:":|:" + (List.map + ~f:(fun i -> "L" ^ Int.to_string i) + (List.range 0 (List.length fields))) + in + let lis = + match List.length fields with + | 0 -> "(fset [])" + | 1 -> lis + | _ -> "(" ^ lis ^ ")" + in + let iis = + String.concat ~sep:":|:" + (List.map + ~f:(fun i -> "I" ^ Int.to_string i) + (List.range 0 (List.length fields))) + in + let iis = + match List.length fields with + | 0 -> "(fset [])" + | 1 -> iis + | _ -> "(" ^ iis ^ ")" + in + SSP.AST.NameTy ("both" ^ " " ^ lis ^ " " ^ iis ^ " " ^ ty_name) ) + (* :: SSP.AST.Arguments ("Build_" ^ pconcrete_ident name,) *); + ] + @ List.mapi + ~f:(fun i (x, _y) -> + SSP.AST.Notation + ( "'Build_" ^ name ^ "'" ^ " " ^ "'['" ^ " " ^ "x" ^ " " ^ "']'" + ^ " " ^ "'('" ^ " " ^ "'" ^ x ^ "'" ^ " " ^ "':='" ^ " " ^ "y" + ^ " " ^ "')'", + SSP.AST.App + ( SSP.AST.Var ("Build_" ^ name), + List.mapi + ~f:(fun j (x, _y) -> + SSP.AST.AppFormat + ( [ x ^ " " ^ ":=" ^ " "; (*v*) "" ], + [ + SSP.AST.Value + ( (if Stdlib.(j == i) then SSP.AST.Var "y" + else + SSP.AST.App + (SSP.AST.Var x, [ SSP.AST.Var "x" ])), + false, + 0 ); + ] )) + fields ), + None )) + fields) + + let both_enum + ((name, arguments, cases) : + string * SSP.AST.argument list * SSP.AST.inductive_case list) : + SSP.AST.decl = + let implicit_LI = + [ + SSP.AST.Implicit (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ] + in + SSP.AST.MultipleDecls + ((* Type definition *) + SSP.AST.Definition + ( (* "t_" ^ *) name, + arguments, + SSP.AST.Type + (SSP.AST.Coproduct + (List.map + ~f:(function + | BaseCase _ -> SSP.AST.Unit + | InductiveCase (_, typ) -> typ) + cases)) + (* (SSP.AST.NameTy ("chFin (mkpos " ^ number_of_cases ^ ")")) *), + SSP.AST.TypeTy ) + :: (* Index names and constructors *) + List.concat_mapi cases ~f:(fun i c -> + let v_name, curr_typ = + match c with + | BaseCase v_name -> (v_name, []) + | InductiveCase (v_name, typ) -> (v_name, [ typ ]) + in + let injections inner_val = + List.fold_left ~init:inner_val + ~f:(fun y x -> SSP.AST.App (SSP.AST.Var x, [ y ])) + ((if Stdlib.(i != 0) then [ "inr" ] else []) + @ List.init (List.length cases - 1 - i) ~f:(fun _ -> "inl")) + in + let definition_body = + let inject_argument inner_val = + SSP.AST.App + ( SSP.AST.Var "solve_lift", + [ + SSP.AST.App + ( SSP.AST.Var "ret_both", + [ + SSP.AST.TypedTerm + (injections inner_val, SSP.AST.NameTy name); + ] ); + ] ) + in + match curr_typ with + | [] -> inject_argument unit_term + | _ -> + SSP.AST.App + ( SSP.AST.Var "bind_both", + [ + SSP.AST.Var "x"; + SSP.AST.Lambda + ( [ SSP.AST.Ident "x" ], + inject_argument (SSP.AST.Var "x") ); + ] ) + in + [ + (let arg, body = + match curr_typ with + | [] -> + ("", injections SSP.AST.UnitTerm) + (* TODO: Fix unit translation *) + | _ -> (" " ^ "x", injections (SSP.AST.Var "x")) + in + SSP.AST.Notation + ("'" ^ v_name ^ "_case" ^ "'" ^ arg, body, Some "at level 100")); + SSP.AST.Equations + ( v_name, + implicit_LI + @ List.map + ~f:(fun x -> + SSP.AST.Explicit + (SSP.AST.Ident "x", wrap_type_in_both "L" "I" x)) + curr_typ, + definition_body, + wrap_type_in_both "L" "I" (SSP.AST.NameTy name) ); + ])) +end + +module StaticAnalysis (* : ANALYSIS *) = struct + module FunctionDependency (* : ANALYSIS *) = + [%functor_application + Analyses.Function_dependency InputLanguage] + + module MutableVariables (* : ANALYSIS *) = + [%functor_application + Analyses.Mutable_variables InputLanguage] + + type analysis_data = { mut_var : MutableVariables.analysis_data } + + let analyse items = + let func_dep = FunctionDependency.analyse items in + let mut_var = + MutableVariables.analyse (func_dep : MutableVariables.pre_data) items + in + { mut_var } +end + +module Context = struct + type t = { + current_namespace : string * string list; + analysis_data : StaticAnalysis.analysis_data; + } +end + +let primitive_to_string (id : Ast.primitive_ident) : string = + match id with + | Deref -> "(TODO: Deref)" (* failwith "Deref" *) + | Cast -> "cast_int (WS2 := _)" (* failwith "Cast" *) + | LogicalOp op -> ( match op with And -> "andb" | Or -> "orb") + +open Phase_utils + +module TransformToInputLanguage (* : PHASE *) = + [%functor_application + Phases.Reject.RawOrMutPointer(Features.Rust) + |> Phases.And_mut_defsite + |> Phases.Reconstruct_for_loops + |> Phases.Direct_and_mut + |> Phases.Reject.Arbitrary_lhs + |> Phases.Drop_blocks + (* |> Phases.Reject.Continue *) + |> Phases.Drop_references + |> Phases.Trivialize_assign_lhs + |> Phases.Reconstruct_question_marks + |> Side_effect_utils.Hoist + (* |> Phases.Local_mutation *) + (* |> Phases.State_passing_loop *) + |> Phases.Reject.Continue + |> Phases.Cf_into_monads + |> Phases.Reject.EarlyExit + (* |> Phases.Functionalize_loops *) + |> Phases.Reject.As_pattern + |> SubtypeToInputLanguage + |> Identity + ] + [@ocamlformat "disable"] + +(* 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 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 pconcrete_ident (id : Ast.concrete_ident) : string = + U.Concrete_ident_view.to_definition_name id + +let plocal_ident (e : Local_ident.t) : string = + U.Concrete_ident_view.local_ident + (match String.chop_prefix ~prefix:"impl " e.name with + | Some name -> + let name = "impl_" ^ Int.to_string ([%hash: string] name) in + { e with name } + | _ -> e) + +module Make (Ctx : sig + val ctx : Context.t +end) = +struct + open Ctx + + 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 + | `TupleType _i -> "TODO (global ident) tuple type" + | `TupleCons _i -> "TODO (global ident) tuple cons" + | `Projector (`TupleField (_i, _j)) | `TupleField (_i, _j) -> + "TODO (global ident) tuple field" + | _ -> . + + (* module TODOs_debug = struct *) + (* let __TODO_pat__ _ s = SSP.AST.Ident (s ^ " todo(pat)") *) + (* let __TODO_ty__ _ s : SSP.AST.ty = SSP.AST.NameTy (s ^ " todo(ty)") *) + (* let __TODO_item__ _ s = SSP.AST.Unimplemented (s ^ " todo(item)") *) + + (* let __TODO_term__ _ s = *) + (* SSP.AST.Const (SSP.AST.Const_string (s ^ " todo(term)")) *) + (* end *) + + module TODOs = struct + let __TODO_ty__ span s : SSP.AST.ty = + Error.unimplemented ~details:("[ty] node " ^ s) span + + let __TODO_pat__ span s = + Error.unimplemented ~details:("[pat] node " ^ s) span + + let __TODO_term__ span s = + Error.unimplemented ~details:("[expr] node " ^ s) span + + let __TODO_item__ _span s = SSP.AST.Unimplemented (s ^ " todo(item)") + end + + open TODOs + + let pint_kind (k : Ast.int_kind) : SSP.AST.int_type = + { + size = + (match k.size with + | S8 -> U8 + | S16 -> U16 + | S32 -> U32 + | S64 -> U64 + | S128 -> U128 + | SSize -> USize); + signed = Stdlib.(k.signedness == Signed); + } + + 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) + | Int { value; kind; _ } -> SSP.AST.Const_int (value, pint_kind kind) + | Float _ -> failwith "Float: todo" + | Bool b -> SSP.AST.Const_bool b + + let operators = + 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["; "]" ])); + (c Core__ops__bit__BitXor__bitxor, (2, [ ""; " .^ "; "" ])); + (c Core__ops__bit__BitAnd__bitand, (2, [ ""; " .& "; "" ])); + (c Core__ops__bit__BitOr__bitor, (2, [ ""; " .| "; "" ])); + (c Core__ops__arith__Add__add, (2, [ ""; " .+ "; "" ])); + (c Core__ops__arith__Sub__sub, (2, [ ""; " .- "; "" ])); + (c Core__ops__arith__Mul__mul, (2, [ ""; " .* "; "" ])); + (c Core__ops__arith__Div__div, (2, [ ""; " ./ "; "" ])); + (c Core__cmp__PartialEq__eq, (2, [ ""; " =.? "; "" ])); + (c Core__cmp__PartialOrd__lt, (2, [ ""; " <.? "; "" ])); + (c Core__cmp__PartialOrd__le, (2, [ ""; " <=.? "; "" ])); + (c Core__cmp__PartialOrd__ge, (2, [ ""; " >=.? "; "" ])); + (c Core__cmp__PartialOrd__gt, (2, [ ""; " >.? "; "" ])); + (c Core__cmp__PartialEq__ne, (2, [ ""; " <> "; "" ])); + (c Core__ops__arith__Rem__rem, (2, [ ""; " .% "; "" ])); + (c Core__ops__bit__Shl__shl, (2, [ ""; " shift_left "; "" ])); + (c Core__ops__bit__Shr__shr, (2, [ ""; " shift_right "; "" ])); + ] + |> Map.of_alist_exn (module Ast.Global_ident) + + module LocalIdentOrLisIis = + StaticAnalysis.MutableVariables.LocalIdentOrData (struct + type ty = string list * string list [@@deriving compare, sexp] + end) + + let rec pty span (t : ty) : SSP.AST.ty = + match t with + | TBool -> SSP.AST.Bool + | 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 -> + SSP.AST.Product (args_ty span 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; _ }); _ }; _ } -> + SSP.AST.ArrayTy (pty span typ, value) + | TArray { typ; length } -> + SSP.AST.ArrayTy + ( pty span typ, + "(" ^ "is_pure" ^ " " ^ "(" + ^ SSP.term_to_string_with_paren + (pexpr (Map.empty (module Local_ident)) false length) + 0 + ^ ")" ^ ")" ) + (* TODO: check int.to_string is correct! *) + | TSlice { ty; _ } -> SSP.AST.SliceTy (pty span ty) + | TParam i -> SSP.AST.NameTy (plocal_ident i) + | TAssociatedType { item; _ } -> SSP.AST.NameTy (pconcrete_ident item) + | TOpaque _ -> __TODO_ty__ span "pty: TAssociatedType/TOpaque" + | _ -> . + + and args_ty span (args : generic_value list) : SSP.AST.ty list = + List.map + ~f:(function + | GLifetime _ -> __TODO_ty__ span "lifetime" + | GType typ -> pty span typ + | GConst { typ; _ } -> + SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])" + (pty span typ)) + args + (* match args with *) + (* | arg :: xs -> *) + (* (match arg with *) + (* | GLifetime { lt; witness } -> __TODO_ty__ span "lifetime" *) + (* | GType typ -> pty span typ *) + (* | GConst { typ; _ } -> *) + (* wrap_type_in_both "(fset [])" "(fset [])" (pty span typ)) *) + (* :: args_ty span xs *) + (* | [] -> [] *) + + and ppat (p : pat) : SSP.AST.pat = + match p.p with + | PWild -> SSP.AST.WildPat + | PAscription { typ; pat; _ } -> + SSP.AST.AscriptionPat (ppat pat, pty p.span typ) + | PBinding + { + mut = Immutable; + mode = _; + var; + typ = _ (* we skip type annot here *); + _; + } -> + SSP.AST.Ident (plocal_ident var) + | PBinding + { + mut = Mutable _; + mode = _; + var; + typ = _ (* we skip type annot here *); + _; + } -> + 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 = []; _ } -> + SSP.AST.WildPat (* UnitPat *) + | 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) + (* Record *) + | PConstruct { is_record = true; _ } -> __TODO_pat__ p.span "record pattern" + (* (\* SSP.AST.Ident (pglobal_ident name) *\) *) + (* SSP.AST.RecordPat (pglobal_ident name, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) args) *) + (* (\* 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; _ } -> + SSP.AST.ConstructorPat + ( pglobal_ident name, + match args with + | [] -> [] + | _ -> [ SSP.AST.TuplePat (List.map ~f:(fun p -> ppat p.pat) args) ] + ) + | PConstant { lit } -> SSP.AST.Lit (pliteral lit) + | _ -> . + + (* and analyse_fset (data : StaticAnalysis.MutableVariables.analysis_data) items = *) + (* (object *) + (* inherit [_] expr_reduce as super *) + (* inherit [_] U.Reducers.expr_list_monoid as m (\* TODO: Raname into list monoid *\) *) + (* method visit_t _ _ = m#zero *) + (* (\* method visit_mutability (_f : string -> _ -> _) (ctx : string) _ = m#zero *\) *) + (* method visit_mutability (f : string -> _ -> _) (ctx : string) mu = *) + (* match mu with Mutable wit -> f ctx wit | _ -> m#zero *) + + (* method! visit_PBinding env mut _ var _typ subpat = *) + (* m#plus *) + (* (match mut with *) + (* | Mutable _ -> *) + (* var.name *) + (* | Immutable -> *) + (* (\* Set.singleton (module U.TypedLocalIdent) (var, typ) *\) *) + (* "") *) + (* (Option.value_map subpat ~default:m#zero *) + (* ~f:(fst >> super#visit_pat env)) *) + + (* method! visit_global_ident (env : string) (x : Global_ident.t) = *) + (* match x with *) + (* | `Projector (`Concrete cid) | `Concrete cid -> *) + (* (match Map.find data (Uprint.Concrete_ident_view.to_definition_name cid) with *) + (* | Some (x,_) -> Set.of_list (module LocalIdent) x *) + (* | _ -> m#zero) *) + (* | _ -> m#zero *) + + (* method visit_expr (env : string) e = [(e, env)] (\* :: super#visit_expr f e *\) *) + (* end) *) + (* #visit_expr *) + (* "" *) + + and pexpr (env : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) + (add_solve : bool) (e : expr) : SSP.AST.term = + let span = e.span in + (match (add_solve, e.e) with + | ( true, + ( Construct { is_record = true; _ } + | If _ (* | Match _ *) | Literal _ + | Construct { constructor = `TupleCons _; _ } + | App _ | GlobalVar _ | LocalVar _ ) ) -> + fun x -> SSP.AST.App (SSP.AST.Var "solve_lift", [ x ]) + | _ -> fun x -> x) + (match e.e with + | Literal lit -> + SSP.AST.App + ( SSP.AST.Var "ret_both", + [ + SSP.AST.TypedTerm (SSP.AST.Const (pliteral lit), pty span e.typ); + ] ) + | LocalVar local_ident -> SSP.AST.NameTerm (plocal_ident local_ident) + | GlobalVar (`TupleCons 0) + | 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 = [ _ ]; + _; + } -> + __TODO_term__ span "app global vcar projector tuple" + | 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 = + List.map + ~f:(fun x -> SSP.AST.Value ((pexpr env false) x, true, 0)) + args + in + SSP.AST.AppFormat (op, args) + (* | App { f = { e = GlobalVar x }; args } -> *) + (* __TODO_term__ span "GLOBAL APP?" *) + | 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) + | If { cond; then_; else_ } -> + SSPExtraDefinitions.ifb + ( (pexpr env false) cond, + (pexpr env false) then_, + Option.value_map else_ ~default:(SSP.AST.Literal "()") + ~f:(pexpr env false) ) + | Array l -> SSP.AST.Array (List.map ~f:(pexpr env add_solve) l) + | Let { lhs; rhs; body; monadic } -> + let extra_set, _extra_env = + LocalIdentOrLisIis.analyse_expr ctx.analysis_data.mut_var env rhs + in + let new_env = + extend_env env + (Map.of_alist_exn + (module Local_ident) + (List.map + ~f:(fun v -> (v, extra_set)) + (Set.to_list (U.Reducers.variables_of_pat lhs)))) + in + let new_env = + match (monadic, is_mutable_pat lhs) with + | None, true -> + extend_env new_env + (Map.of_alist_exn + (module Local_ident) + (List.map + ~f:(fun v -> (v, [ LocalIdentOrLisIis.W.Identifier v ])) + (Set.to_list (U.Reducers.variables_of_pat lhs)))) + | _, _ -> new_env + in + SSPExtraDefinitions.letb + { + pattern = ppat lhs; + mut = is_mutable_pat lhs; + value = (pexpr env false) rhs; + body = (pexpr new_env add_solve) body; + value_typ = + (match monadic with + | Some (MException typ, _) -> pty span typ + | Some (MResult typ, _) -> pty span typ + | _ -> + SSP.AST.WildTy + (* TODO : What should the correct type be here? `lhs.span lhs.typ` *)); + monad_typ = + Option.map + ~f:(fun (m, _) -> + match m with + | MException typ -> SSP.AST.Exception (pty span typ) + | MResult typ -> SSP.AST.Result (pty span typ) + | MOption -> SSP.AST.Option) + monadic; + } + | EffectAction _ -> . (* __TODO_term__ span "monadic action" *) + | Match + { + scrutinee; + arms = + [ + { + arm = + { + arm_pat = + { + p = + PConstruct + { + args = [ { pat; _ } ]; + is_record = false; + is_struct = true; + _; + }; + _; + }; + body; + }; + _; + }; + ]; + } -> + (* Record match expressions *) + (* (pexpr env true) body *) + SSPExtraDefinitions.letb + { + pattern = ppat pat; + mut = false; + value = (pexpr env false) scrutinee; + body = (pexpr env true) body; + value_typ = pty pat.span pat.typ; + monad_typ = None; + } + | Match { scrutinee; arms } -> + SSPExtraDefinitions.matchb + ( (pexpr env false) scrutinee, + List.map + ~f:(fun { arm = { arm_pat; body }; _ } -> + match arm_pat.p with + | PConstruct + { name; args; is_record = false; is_struct = false } -> ( + let arg_tuple = + SSP.AST.TuplePat + (List.map ~f:(fun p -> ppat p.pat) args) + in + ( SSP.AST.ConstructorPat + ( pglobal_ident name ^ "_case", + match args with [] -> [] | _ -> [ arg_tuple ] ), + match + (args, SSPExtraDefinitions.pat_as_expr arg_tuple) + with + | _ :: _, Some (redefine_pat, redefine_expr) -> + SSPExtraDefinitions.letb + { + pattern = redefine_pat (* TODO *); + mut = false; + value = + SSP.AST.App + ( SSP.AST.Var "ret_both", + [ + SSP.AST.TypedTerm + ( redefine_expr, + SSP.AST.Product + (List.map + ~f:(fun x -> + pty arm_pat.span x.pat.typ) + args) ); + ] ); + body = (pexpr env true) body; + value_typ = + SSP.AST.Product + (List.map + ~f:(fun x -> pty arm_pat.span x.pat.typ) + args); + monad_typ = None; + } + | _, _ -> (pexpr env true) body )) + | _ -> (ppat arm_pat, (pexpr env true) body)) + arms ) + | Ascription _ -> __TODO_term__ span "asciption" + | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> + (pexpr env false) e + | Construct { constructor = `TupleCons _n; fields; _ } -> + 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; _ } -> + 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, _); _ } -> + SSP.AST.RecordUpdate + ( pglobal_ident constructor, + (pexpr env false) x, + List.map + ~f:(fun (f, e) -> (pglobal_ident f, (pexpr env false) e)) + fields ) + (* TODO: Is there only 1 field? *) + | Construct { constructor; fields = [ (_f, e) ]; _ } -> + SSP.AST.App + ( SSP.AST.Var (pglobal_ident constructor), + [ (pexpr env add_solve) e ] ) + | Construct { constructor; fields; _ } -> + (* __TODO_term__ span "constructor" *) + SSP.AST.App + ( SSP.AST.Var (pglobal_ident constructor), + List.map ~f:(snd >> pexpr env add_solve) fields ) + | 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: Ast.global_ident] macro }; + span = e.span; + } + | Assign _ -> + SSP.AST.Const (SSP.AST.Const_string ("assign" ^ " todo(term)")) + (* __TODO_term__ span "assign" *) + | Loop { body; kind; state = None; label; witness } -> + (pexpr env false) + { + e = + Loop + { + body; + kind; + state = + Some + { + init = + { + e = + Construct + { + is_record = false; + is_struct = false; + base = None; + constructor = `TupleCons 0; + fields = []; + }; + span = Span.dummy (); + typ = TApp { ident = `TupleType 0; args = [] }; + }; + bpat = + { + p = + PConstruct + { + name = `TupleCons 0; + args = []; + is_record = false; + is_struct = false; + }; + span = Span.dummy (); + typ = TApp { ident = `TupleType 0; args = [] }; + }; + witness = + Features.On.state_passing_loop + (* state_passing_loop *); + }; + label; + witness; + }; + typ = e.typ; + span = e.span; + } + | Loop + { + body; + kind = ForIndexLoop { start; end_; var; _ }; + state = Some { init; bpat; _ }; + _; + } -> + SSP.AST.App + ( SSP.AST.Var "foldi_both", + [ + (pexpr env false) start; + (pexpr env false) end_; + SSP.AST.Lambda + ( [ + (* SSP.AST.Ident "{L I _ _}"; *) + SSP.AST.Ident (plocal_ident var); + ], + SSP.AST.App + ( SSP.AST.Var "ssp", + [ + SSP.AST.Lambda + ( [ ppat bpat ], + both_type_expr + (extend_env env + (Map.of_alist_exn + (module Local_ident) + ([ + ( var, + [ + LocalIdentOrLisIis.W.Data + ( [ plocal_ident var ^ "?" ], + [ plocal_ident var ^ "?" ] ); + ] ); + ] + @ List.map + ~f:(fun v -> + ( v, + [ + LocalIdentOrLisIis.W.Data + ( [ plocal_ident v ^ "!" ], + [ plocal_ident v ^ "!" ] ); + ] )) + (vars_from_pat bpat)))) + true [] body ); + ] ) ); + (pexpr env false) init; + ] ) + | Loop + { + body; + kind = ForLoop { pat; it; _ }; + state = Some { init; bpat; _ }; + _; + } -> + let extra_set_init, _extra_env = + LocalIdentOrLisIis.analyse_expr ctx.analysis_data.mut_var env init + in + let new_env = + extend_env env + (Map.of_alist_exn + (module Local_ident) + (List.map + ~f:(fun v -> (v, extra_set_init)) + (Set.to_list (U.Reducers.variables_of_pat bpat)))) + in + let extra_set_iter, _extra_env = + LocalIdentOrLisIis.analyse_expr ctx.analysis_data.mut_var env it + in + let new_env = + extend_env new_env + (Map.of_alist_exn + (module Local_ident) + (List.map + ~f:(fun v -> (v, extra_set_iter)) + (Set.to_list (U.Reducers.variables_of_pat bpat)))) + in + SSP.AST.App + ( SSP.AST.Var "foldi_both_list", + [ + (pexpr env false) it; + SSP.AST.Lambda + ( [ (* SSP.AST.Ident "{L I _ _}"; *) ppat pat ], + SSP.AST.App + ( SSP.AST.Var "ssp", + [ + SSP.AST.Lambda + ( [ ppat bpat ], + both_type_expr new_env true + (extra_set_iter @ extra_set_init) + body ); + ] ) ); + (pexpr env false) init; + ] ) + | Loop _ -> + SSP.AST.Const (SSP.AST.Const_string ("other loop" ^ " todo(term)")) + (* __TODO_term__ span "other loop" *) + (* | Break { e; _ } -> *) + (* SSP.AST.Const (SSP.AST.Const_string ("break" ^ " todo(term)")) *) + (* (* __TODO_term__ span "break" *) *) + | _ -> .) + + and vars_from_pat : pat -> Local_ident.t list = + U.Reducers.variables_of_pat >> Set.to_list + + and env_from_param (params : pat list) : + LocalIdentOrLisIis.W.t list Map.M(Local_ident).t = + Map.of_alist_exn + (module Local_ident) + (List.concat_mapi + ~f:(fun i pat -> + List.map + ~f:(fun var -> + ( var, + [ + LocalIdentOrLisIis.W.Data + ( [ "L" ^ Int.to_string (i + 1) ], + [ "I" ^ Int.to_string (i + 1) ] ); + ] )) + (vars_from_pat pat)) + params) + + and extend_env (env : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) + (env_ext : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) : + LocalIdentOrLisIis.W.t list Map.M(Local_ident).t = + Map.merge_skewed env env_ext ~combine:(fun ~key:_ a b -> a @ b) + (* TODO: Just combine values? Should do this as sets! *) + + and extend_env_with_params + (env : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) + (params : pat list) : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t = + extend_env env (env_from_param params) + + and analyse_env_of_expr + (env : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) (e : expr) + extra_set = + let expr_env, new_env = + LocalIdentOrLisIis.analyse_expr ctx.analysis_data.mut_var env e + in + let expr_env = expr_env @ extra_set in + let identifiers = + List.filter_map + ~f:(function Identifier x -> Some x | Data _ -> None) + expr_env + in + let data = + List.filter_map + ~f:(function Identifier _ -> None | Data x -> Some x) + expr_env + in + let lis, iis = (List.concat *** List.concat) (List.unzip data) in + (identifiers, lis, iis, new_env) + + and both_type_expr (env : LocalIdentOrLisIis.W.t list Map.M(Local_ident).t) + (add_solve : bool) (extra_set : LocalIdentOrLisIis.W.t list) (e : expr) = + let identifiers, lis, iis, _new_env = analyse_env_of_expr env e extra_set in + let mvars_ext_fset_str = + "fset" ^ " " ^ "[" + ^ String.concat ~sep:";" + (List.map ~f:(fun x -> plocal_ident x ^ "_loc") identifiers) + ^ "]" + in + let lis_str = String.concat ~sep:":|:" (lis @ [ mvars_ext_fset_str ]) in + let iis_str = + if List.is_empty iis then "(fset [])" else String.concat ~sep:":|:" iis + in + SSP.AST.TypedTerm + ( (pexpr env add_solve) e, + SSPExtraDefinitions.wrap_type_in_both + ("(*" + ^ Int.to_string (List.length identifiers) + ^ "*)" ^ "(" ^ lis_str ^ ")") + ("(" ^ iis_str ^ ")") + (pty e.span e.typ) ) + + and is_mutable_pat (pat : pat) = + match pat.p with + | PWild -> false + | PAscription { pat; _ } -> is_mutable_pat pat + | PConstruct { name = `TupleCons _; args; _ } -> + List.fold ~init:false ~f:( || ) + (List.map ~f:(fun p -> is_mutable_pat p.pat) args) + | PConstruct _ -> false + | PArray _ -> + (* List.fold ~init:false ~f:(||) (List.map ~f:(fun p -> is_mutable_pat p) args) *) + false + | PConstant _ -> false + | PBinding { mut = Mutable _; _ } -> true + | PBinding _ -> false + | POr _ -> + (* List.fold ~init:false ~f:( || ) *) + (* (List.map ~f:(fun p -> is_mutable_pat p) subpats) *) + false + (* TODO? *) + | _ -> . + + let pgeneric_param_as_argument span : AST.generic_param -> SSP.AST.argument = + function + | { ident; kind; _ } -> + SSP.AST.Implicit + ( SSP.AST.Ident (plocal_ident ident), + match kind with + | GPType { default = Some t } -> pty span t + | GPConst { typ = t } -> + SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])" + (pty span t) + | GPType { default = None } -> SSP.AST.WildTy + | _ -> . ) + + let pgeneric_constraints_as_argument span : + generic_constraint -> SSP.AST.argument list = function + | GCType { bound = { trait; args }; _ } -> + [ + SSP.AST.Typeclass + ( None, + SSP.AST.AppTy + ( SSP.AST.NameTy (pconcrete_ident trait), + List.map + ~f:(function + | GType typ -> pty span typ + | GConst { typ; _ } -> + SSPExtraDefinitions.wrap_type_in_both "(fset [])" + "(fset [])" (pty span typ) + | _ -> .) + args ) ); + ] + | _ -> . + + 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) + generics.constraints + + let rec split_arrow_in_args (a : SSP.AST.ty) : SSP.AST.ty list * SSP.AST.ty = + match a with + | SSP.AST.Arrow (x, y) -> + let l, r = split_arrow_in_args y in + (x :: l, r) + | _ -> ([], a) + + let rec wrap_type_in_enumerator_helper (li : int -> string) + (ii : int -> string) (i : int) (a : SSP.AST.ty) = + let l, r = split_arrow_in_args a in + let size, t = + List.fold_left + ~f:(fun (yi, ys) x -> + let size, x_val = wrap_type_in_enumerator_helper li ii yi x in + ( size, + match ys with + | Some v -> Some (SSP.AST.Arrow (v, x_val)) + | None -> Some x_val )) + ~init:(i, None) l + in + match t with + | Some v -> + ( size, + SSP.AST.Arrow + (v, SSPExtraDefinitions.wrap_type_in_both (li i) (ii i) r) ) + | None -> (size + 1, SSPExtraDefinitions.wrap_type_in_both (li i) (ii i) r) + + let wrap_type_in_enumerator (li : int -> string) (ii : int -> string) + (a : SSP.AST.ty) (extra_L : string list) = + let size, v = wrap_type_in_enumerator_helper li ii 0 a in + (* Throw away anotation of last type, and replace with accumulation of all locations and imports *) + let xs, a = + match v with + | SSP.AST.Arrow (x, SSP.AST.AppTy (SSP.AST.NameTy _, [ a ])) -> ([ x ], a) + | SSP.AST.AppTy (SSP.AST.NameTy _, [ a ]) -> ([], a) + | _ -> + Error.unimplemented + ~details: + "SSProve: TODO: wrap_type_in_enumerator encountered an \ + unexpected type" + (Span.dummy ()) + in + let lis, iis = + List.unzip (List.map ~f:(fun i -> (li i, ii i)) (List.range 0 size)) + in + let lis = lis @ extra_L in + let ret_ty = + List.fold + ~init: + (SSPExtraDefinitions.wrap_type_in_both + (let lis_str = String.concat ~sep:" :|: " lis in + if List.length lis <= 1 then lis_str else "(" ^ lis_str ^ ")") + (let iis_str = String.concat ~sep:" :|: " iis in + if List.length iis <= 1 then iis_str else "(" ^ iis_str ^ ")") + a) + ~f:(fun y x -> SSP.AST.Arrow (x, y)) + xs + in + (size, ret_ty) + + 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" ] + + and pitem_unwrapped (e : AST.item) : SSP.AST.decl list = + let span = e.span in + let decls_from_item = + match e.v with + | Fn { name = f_name; generics; body; params } -> + loc_defs_from_name f_name + (List.map + ~f:(fun v -> + match v with + | SSP.AST.Explicit (a, b) -> SSP.AST.Implicit (a, b) + | _ -> v) + (pgeneric span generics)) + @ [ + (let args, ret_typ = + lift_definition_type_to_both f_name + (pgeneric span generics + @ List.map + ~f:(fun { pat; typ; _ } -> + SSP.AST.Explicit (ppat pat, pty span typ)) + params) + (pty span body.typ) [] + in + SSP.AST.Equations + ( pconcrete_ident f_name, + args, + (pexpr + (extend_env_with_params + (Map.empty (module Local_ident)) + (List.map ~f:(fun { pat; _ } -> pat) params)) + true) + body, + ret_typ )); + ] + | TyAlias { name; generics; ty } -> + let g = pgeneric span generics in + [ + (if List.is_empty g then + SSP.AST.Notation + ( "'" ^ pconcrete_ident name ^ "'", + SSP.AST.Type (pty span ty), + None ) + else + SSP.AST.Definition + ( pconcrete_ident name, + g, + SSP.AST.Type (pty span ty), + SSP.AST.TypeTy )); + ] + (* record *) + | Type + { + name; + generics; + variants = [ { name = _record_name; arguments; _ } ]; + is_struct = true; + } -> + [ + SSPExtraDefinitions.updatable_record + ( pconcrete_ident name, + pgeneric span generics, + List.map + ~f:(fun (x, y) -> SSP.AST.Named (x, y)) + (p_record_record span arguments) ); + ] + (* enum *) + | 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; _ } -> + if is_record then + Some + (SSPExtraDefinitions.updatable_record + ( (match + String.chop_prefix ~prefix:"C_" + (pconcrete_ident v_name) + with + | Some name -> "t_" ^ name + | _ -> failwith "Incorrect prefix of record name in enum"), + pgeneric span generics, + List.map + ~f:(fun (x, y) -> SSP.AST.Named (x, y)) + (p_record_record span arguments) )) + else None) + @ [ + SSPExtraDefinitions.both_enum + ( pconcrete_ident name, + pgeneric span generics, + List.map variants + ~f:(fun { name = v_name; arguments; is_record; _ } -> + if is_record then + SSP.AST.InductiveCase + ( pconcrete_ident v_name, + SSP.AST.RecordTy + ( (match + String.chop_prefix ~prefix:"C_" + (pconcrete_ident v_name) + with + | Some name -> "t_" ^ name + | _ -> + failwith + "Incorrect prefix of record name in enum"), + p_record_record span arguments ) ) + else + match arguments with + | [] -> SSP.AST.BaseCase (pconcrete_ident v_name) + | [ (_arg_name, arg_ty, _attr) ] -> + SSP.AST.InductiveCase + (* arg_name = ?? *) + (pconcrete_ident v_name, pty span arg_ty) + | _ -> + SSP.AST.InductiveCase + ( pconcrete_ident v_name, + SSP.AST.Product + (List.map + ~f:((fun (_x, y, _z) -> y) >> pty span) + arguments) )) ); + ] + | IMacroInvokation { macro; argument; _ } -> ( + let unsupported () = + let id = [%show: concrete_ident] macro in + Error.raise { kind = UnsupportedMacro { id }; span = e.span } + in + match U.Concrete_ident_view.to_view macro with + | { crate = "hacspec_lib"; path = _; definition = name } -> ( + match name with + | "public_nat_mod" -> + let open Hacspeclib_macro_parser in + let o : PublicNatMod.t = + PublicNatMod.parse argument |> Result.ok_or_failwith + in + [ + SSP.AST.Notation + ( "'" ^ "t_" ^ o.type_name ^ "'", + SSP.AST.Type + (SSP.AST.NatMod + ( o.type_of_canvas, + o.bit_size_of_field, + o.modulo_value )), + None ); + SSP.AST.Definition + ( o.type_name, + [ + SSP.AST.Implicit + (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit + (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ], + SSP.AST.Var "id", + SSP.AST.Arrow + ( SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.type_name)), + SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.type_name)) ) ); + ] + | "bytes" -> + let open Hacspeclib_macro_parser in + let o : Bytes.t = + Bytes.parse argument |> Result.ok_or_failwith + in + [ + SSP.AST.Notation + ( "'" ^ "t_" ^ o.bytes_name ^ "'", + SSP.AST.Type + (SSP.AST.ArrayTy + ( SSP.AST.Int { size = SSP.AST.U8; signed = false }, + (* int_of_string *) o.size )), + None ); + SSP.AST.Definition + ( o.bytes_name, + [ + SSP.AST.Implicit + (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit + (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ], + SSP.AST.Var "id", + SSP.AST.Arrow + ( SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.bytes_name)), + SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.bytes_name)) ) ); + ] + | "unsigned_public_integer" -> + let open Hacspeclib_macro_parser in + let o = + UnsignedPublicInteger.parse argument + |> Result.ok_or_failwith + in + [ + SSP.AST.Notation + ( "'" ^ "t_" ^ o.integer_name ^ "'", + SSP.AST.Type + (SSP.AST.ArrayTy + ( SSP.AST.Int { size = SSP.AST.U8; signed = false }, + Int.to_string ((o.bits + 7) / 8) )), + None ); + SSP.AST.Definition + ( o.integer_name, + [ + SSP.AST.Implicit + (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit + (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ], + SSP.AST.Var "id", + SSP.AST.Arrow + ( SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.integer_name)), + SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.integer_name)) ) ); + ] + | "public_bytes" -> + let open Hacspeclib_macro_parser in + let o : Bytes.t = + Bytes.parse argument |> Result.ok_or_failwith + in + let typ = + SSP.AST.ArrayTy + ( SSP.AST.Int { size = SSP.AST.U8; signed = false }, + (* int_of_string *) o.size ) + in + [ + SSP.AST.Notation + ("'" ^ "t_" ^ o.bytes_name ^ "'", SSP.AST.Type typ, None); + SSP.AST.Definition + ( o.bytes_name, + [ + SSP.AST.Implicit + (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit + (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ], + SSP.AST.Var "id", + SSP.AST.Arrow + ( SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.bytes_name)), + SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.bytes_name)) ) ); + ] + | "array" -> + let open Hacspeclib_macro_parser in + let o : Array.t = + Array.parse argument |> Result.ok_or_failwith + in + let typ = + match o.typ with + | "U128" -> SSP.AST.U128 + | "U64" -> SSP.AST.U64 + | "U32" -> SSP.AST.U32 + | "U16" -> SSP.AST.U16 + | "U8" -> SSP.AST.U8 + | _usize -> SSP.AST.U32 (* TODO: usize? *) + in + [ + SSP.AST.Notation + ( "'" ^ "t_" ^ o.array_name ^ "'", + SSP.AST.Type + (SSP.AST.ArrayTy + ( SSP.AST.Int { size = typ; signed = false }, + (* int_of_string *) o.size )), + None ); + SSP.AST.Definition + ( o.array_name, + [ + SSP.AST.Implicit + (SSP.AST.Ident "L", SSP.AST.NameTy "{fset Location}"); + SSP.AST.Implicit + (SSP.AST.Ident "I", SSP.AST.NameTy "Interface"); + ], + SSP.AST.Var "id", + SSP.AST.Arrow + ( SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.array_name)), + SSPExtraDefinitions.wrap_type_in_both "L" "I" + (SSP.AST.NameTy ("t_" ^ o.array_name)) ) ); + ] + | _ -> unsupported ()) + | _ -> unsupported ()) + | Use { path; is_external; rename } -> + let _ns_crate, _ns_path = ctx.current_namespace in + if is_external then [] + else + [ SSP.AST.Require (None, (* ns_crate:: ns_path @ *) path, rename) ] + | HaxError s -> [ __TODO_item__ span s ] + | NotImplementedYet -> [ __TODO_item__ span "Not implemented yet?" ] + | Alias _ -> [ __TODO_item__ span "Not implemented yet? alias" ] + | Trait { name; items; _ } -> + [ + SSP.AST.Class + ( pconcrete_ident name, + [], + (* pgeneric span generics, *) + List.concat_map + ~f:(fun x -> + match x.ti_v with + | TIFn fn_ty -> + let loc_name = pconcrete_ident x.ti_ident ^ "_loc" in + let include_extra_loc = + match fn_ty with TArrow _ -> true | _ -> false + in + let size, value = + wrap_type_in_enumerator + (fun (i : int) -> "L" ^ Int.to_string (i + 1)) + (fun (i : int) -> "I" ^ Int.to_string (i + 1)) + (pty x.ti_span fn_ty) + (if include_extra_loc then [ loc_name ] else []) + in + (if include_extra_loc then + [ + SSP.AST.Named + (loc_name, SSP.AST.NameTy "{fset Location}"); + ] + else []) + @ [ + SSP.AST.Named + ( pconcrete_ident x.ti_ident, + SSP.AST.Forall + ( List.map + ~f:(fun (i : int) -> + "L" ^ Int.to_string (i + 1)) + (List.range 0 size) + @ List.map + ~f:(fun (i : int) -> + "I" ^ Int.to_string (i + 1)) + (List.range 0 size), + [], + value ) ); + ] + | TIType trait_refs -> + SSP.AST.Named + (pconcrete_ident x.ti_ident, SSP.AST.TypeTy) + :: List.map + ~f:(fun tr -> + SSP.AST.Coercion + ( pconcrete_ident x.ti_ident ^ "_" + ^ pconcrete_ident tr.trait, + SSP.AST.AppTy + ( SSP.AST.NameTy (pconcrete_ident tr.trait), + [ + SSP.AST.NameTy + (pconcrete_ident x.ti_ident); + ] ) )) + trait_refs) + items ); + ] + @ List.concat_map + ~f:(fun x -> + match x.ti_v with + | TIFn (TArrow _) -> + [ + SSP.AST.HintUnfold + (pconcrete_ident x.ti_ident ^ "_loc", None); + ] + | _ -> []) + items + | Impl { generics; self_ty; of_trait = name, gen_vals; items } -> + List.concat_map + ~f:(fun x -> + loc_defs_from_name x.ii_ident + (List.map + ~f:(fun v -> + match v with + | SSP.AST.Explicit (a, b) -> SSP.AST.Implicit (a, b) + | _ -> v) + (pgeneric span generics))) + items + @ [ + SSP.AST.ProgramInstance + ( pglobal_ident name, + pgeneric span generics, + pty span self_ty, + args_ty span gen_vals, + SSP.AST.InstanceDecls + (List.concat_map + ~f:(fun x -> + match x.ii_v with + | IIFn { body; params } -> + let mvars_ext_fset_str = + "fset" ^ " " ^ "[" + ^ String.concat ~sep:";" + (List.map + ~f:(fun x -> plocal_ident x ^ "_loc") + (match + Map.find ctx.analysis_data.mut_var + (pconcrete_ident x.ii_ident) + with + | Some (l, _) -> l + | _ -> [])) + ^ "]" + in + [ + SSP.AST.InlineDef + ( pconcrete_ident x.ii_ident ^ "_loc", + [], + SSP.AST.NameTerm mvars_ext_fset_str, + SSP.AST.NameTy "{fset Location}" ); + (let args, ret_typ = + lift_definition_type_to_both x.ii_ident + (List.map + ~f:(fun { pat; typ; _ } -> + SSP.AST.Explicit + (ppat pat, pty span typ)) + params) + (pty span body.typ) + (match + Map.find ctx.analysis_data.mut_var + (pconcrete_ident x.ii_ident) + with + | Some (_ :: _, _) -> [] + | _ -> [ "fset []" ]) + in + SSP.AST.LetDef + ( pconcrete_ident x.ii_ident, + args, + (pexpr + (extend_env_with_params + (Map.empty (module Local_ident)) + (List.map + ~f:(fun { pat; _ } -> pat) + params)) + true) + body, + ret_typ )); + ] + | IIType ty -> + [ + SSP.AST.LetDef + ( pconcrete_ident x.ii_ident, + [], + SSP.AST.Type (pty span ty), + SSP.AST.TypeTy ); + ]) + items) ); + ] + @ [ SSP.AST.HintUnfold (pglobal_ident name, Some (pty span self_ty)) ] + in + decls_from_item + + and loc_defs_from_name (name : concrete_ident) generics : SSP.AST.decl list = + List.map + ~f:(fun ((x, x_ty), x_n) -> + (* x_ty should not be (totally) resolved! , infer from let not pbinding ?? *) + SSP.AST.Definition + ( plocal_ident x ^ "_loc", + generics, + SSP.AST.AppFormat + ( [ "("; ";"; "%nat)" ], + [ + SSP.AST.Typing (pty (Span.dummy ()) x_ty, false, 0); + SSP.AST.Value (SSP.AST.Literal (Int.to_string x_n), false, 0); + ] ), + SSP.AST.NameTy "Location" )) + (match Map.find ctx.analysis_data.mut_var (pconcrete_ident name) with + | Some l -> snd l + | None -> []) + + and new_arguments lis iis (arguments : SSP.AST.argument list) = + List.map + ~f:(fun x -> + SSP.AST.Implicit (SSP.AST.Ident x, SSP.AST.NameTy "{fset Location}")) + lis + @ List.map + ~f:(fun x -> + SSP.AST.Implicit (SSP.AST.Ident x, SSP.AST.NameTy "Interface")) + iis + @ snd + (List.fold_left ~init:(0, []) + ~f:(fun (i, y) arg -> + let f = + SSPExtraDefinitions.wrap_type_in_both + ("L" ^ Int.to_string (i + 1)) + ("I" ^ Int.to_string (i + 1)) + in + match arg with + | Implicit (p, t) -> (i, y @ [ SSP.AST.Implicit (p, t) ]) + | Explicit (p, t) -> (i + 1, y @ [ SSP.AST.Explicit (p, f t) ]) + | Typeclass (so, t) -> (i, y @ [ SSP.AST.Typeclass (so, t) ])) + arguments) + + and lift_definition_type_to_both (name : concrete_ident) + (arguments : SSP.AST.argument list) (typ : SSP.AST.ty) + (extra_L : string list) : SSP.AST.argument list * SSP.AST.ty = + let lis, iis = get_lis_and_iis_both arguments in + let new_args = new_arguments lis iis arguments in + let return_typ = both_return_type_from_name lis iis name typ extra_L in + (new_args, return_typ) + + and both_return_type_from_name lis iis name typ (extra_L : string list) = + let mvars_ext_L = + match Map.find ctx.analysis_data.mut_var (pconcrete_ident name) with + | Some (l, _l2) when List.length l > 0 -> + [ + "fset" ^ " " ^ "[" + ^ String.concat ~sep:";" + (List.map ~f:(fun x -> plocal_ident x ^ "_loc") l) + ^ "]"; + ] + | _ -> [] + in + let lis = lis @ mvars_ext_L @ extra_L in + let iis = iis in + SSPExtraDefinitions.wrap_type_in_both + (let lis_str = String.concat ~sep:" :|: " lis in + if List.length lis <= 1 then lis_str else "(" ^ lis_str ^ ")") + (let iis_str = String.concat ~sep:" :|: " iis in + if List.length iis <= 1 then iis_str else "(" ^ iis_str ^ ")") + typ + + and get_lis_and_iis_both (arguments : SSP.AST.argument list) : + string list * string list = + let num_explicit_args = + List.length + (List.filter ~f:(function Explicit _ -> true | _ -> false) arguments) + in + let lis, iis = + if Stdlib.(num_explicit_args == 0) (* TODO: arguments that are updated? *) + then ([ "L" ], [ "I" ]) + else + List.unzip + (List.map + ~f:(fun i -> + ("L" ^ Int.to_string (i + 1), "I" ^ Int.to_string (i + 1))) + (List.range 0 num_explicit_args)) + in + (lis, iis) + + and p_record_record span arguments : (string * SSP.AST.ty) list = + List.map + ~f:(function + | arg_name, arg_ty, _arg_attrs -> + (pconcrete_ident arg_name, pty span arg_ty)) + arguments +end + +module type S = sig + val pitem : AST.item -> SSP.AST.decl list + (* val pgeneric : Ast.span -> AST.generics -> SSP.AST.argument list *) +end + +let make ctx = + (module Make (struct + let ctx = ctx + end) : S) + +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 : AST.item) + : SSP.AST.decl list = + let (module Print) = + make + { + current_namespace = U.Concrete_ident_view.to_namespace item.ident; + analysis_data; + } + in + Print.pitem item + +let cleanup_item_strings = + List.map ~f:String.strip + >> 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 *) + +let process_annotation (x : 'a list) (f2 : ('b * ('a -> 'b)) list) : 'b list = + List.concat_map + ~f:(fun (d, f) -> + let temp = List.map ~f x in + if List.is_empty (List.concat temp) then [] else d :: temp) + f2 + +let string_of_items (x, y) = + cleanup_item_strings + (List.map ~f:decls_to_string + (process_annotation x + [ + ([], print_item y); + (* ConCert.(concert_header, translate_concert_annotations y); *) + ] + (* @ ConCert.concert_contract_type_decls x *))) + +(* TODO move into string_of_items, as SSP.AST decl *) +let hardcoded_coq_headers = + "(* File automatically generated by Hacspec *)\n\ + Set Warnings \"-notation-overridden,-ambiguous-paths\".\n\ + From Crypt Require Import choice_type Package Prelude.\n\ + Import PackageNotation.\n\ + From extructures Require Import ord fset.\n\ + From mathcomp Require Import word_ssrZ word.\n\ + From Jasmin Require Import word.\n\n\ + From Coq Require Import ZArith.\n\ + From Coq Require Import Strings.String.\n\ + Import List.ListNotations.\n\ + Open Scope list_scope.\n\ + Open Scope Z_scope.\n\ + Open Scope bool_scope.\n\n\ + From Hacspec Require Import ChoiceEquality.\n\ + From Hacspec Require Import LocationUtility.\n\ + From Hacspec Require Import Hacspec_Lib_Comparable.\n\ + From Hacspec Require Import Hacspec_Lib_Pre.\n\ + From Hacspec Require Import Hacspec_Lib.\n\n\ + Open Scope hacspec_scope.\n\ + Import choice.Choice.Exports.\n\n\ + Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.\n" + +let translate _ (_bo : BackendOptions.t) (items : AST.item list) : + Types.file list = + let analysis_data = StaticAnalysis.analyse items in + U.group_items_by_namespace items + |> Map.to_alist + |> List.map ~f:(fun (ns, items) -> + let mod_name = + String.concat ~sep:"_" + (List.map + ~f:(map_first_letter String.uppercase) + (fst ns :: snd ns)) + in + let file_content = + hardcoded_coq_headers ^ "\n" + ^ string_of_items (items, analysis_data) + ^ "\n" + in + + Types.{ path = mod_name ^ ".v"; contents = file_content }) + +let apply_phases (_bo : BackendOptions.t) (i : Ast.Rust.item list) : + AST.item list = + TransformToInputLanguage.ditems i diff --git a/engine/backends/coq/ssprove/ssprove_backend.mli b/engine/backends/coq/ssprove/ssprove_backend.mli new file mode 100644 index 000000000..67448d149 --- /dev/null +++ b/engine/backends/coq/ssprove/ssprove_backend.mli @@ -0,0 +1,2 @@ +open Hax_engine.Backend +include T with module BackendOptions = UnitBackendOptions diff --git a/engine/backends/easycrypt/dune b/engine/backends/easycrypt/dune index d8a111ebf..3936a87e8 100644 --- a/engine/backends/easycrypt/dune +++ b/engine/backends/easycrypt/dune @@ -17,4 +17,4 @@ (env (_ (flags - (:standard -warn-error -A -warn-error +8)))) + (:standard -w -A)))) diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml index a10b4522e..1977f7cc0 100644 --- a/engine/backends/easycrypt/easycrypt_backend.ml +++ b/engine/backends/easycrypt/easycrypt_backend.ml @@ -1,6 +1,5 @@ (* -------------------------------------------------------------------- *) open Hax_engine -open Utils open Base (* -------------------------------------------------------------------- *) @@ -20,9 +19,6 @@ include let backend = Diagnostics.Backend.EasyCrypt end) -let apply_phases _ = failwith "xx" -let translate _ = failwith "xx" - module BackendOptions = Backend.UnitBackendOptions module AST = Ast.Make (InputLanguage) module ECNamePolicy = Concrete_ident.DefaultNamePolicy @@ -44,7 +40,6 @@ module RejectNotEC (FA : Features.T) = struct let continue = reject let mutable_reference = reject let mutable_pointer = reject - let mutable_borrow = reject let reference = reject let slice = reject let raw_pointer = reject @@ -110,20 +105,22 @@ let suffix_of_signedness (s : Ast.signedness) = match s with Signed -> "S" | Unsigned -> "U" let intmodule_of_kind (Ast.{ size; signedness } : Ast.int_kind) = - Format.sprintf "W%s%s" (suffix_of_signedness signedness) (suffix_of_size size) + Stdlib.Format.sprintf "W%s%s" + (suffix_of_signedness signedness) + (suffix_of_size size) -let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list - = +let translate' (_bo : BackendOptions.t) (items : AST.item list) : + Types.file list = let items = List.fold_left ~init:NM.empty ~f:NM.push items in - let rec doit (fmt : Format.formatter) (the : nmtree) = + let rec doit (fmt : Formatter.t) (the : nmtree) = the.subnms |> Map.Poly.iteri ~f:(fun ~key ~data -> - Format.fprintf fmt "theory %s.@." key; + Stdlib.Format.fprintf fmt "theory %s.@." key; doit fmt data; - Format.fprintf fmt "end.@."); + Stdlib.Format.fprintf fmt "end.@."); - let doitems (fmt : Format.formatter) = + let doitems (fmt : Formatter.t) = the.items |> List.iter ~f:(fun item -> match item.v with @@ -138,65 +135,66 @@ let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list | Trait _ -> assert false | Impl _ -> assert false | HaxError _ -> () - | IMacroInvokation mi -> () + | IMacroInvokation _ -> () | Use _ -> () | Alias _ -> () - | NotImplementedYet -> ()) + | NotImplementedYet -> () + | _ -> .) in if not (List.is_empty the.items) then - Format.fprintf fmt "@[module Procs = {@, @[%t@]@,}@]@," doitems - and doit_fn (fmt : Format.formatter) (name, params, body) = - let pp_param (fmt : Format.formatter) (p : param) = + Stdlib.Format.fprintf fmt "@[module Procs = {@, @[%t@]@,}@]@," + doitems + and doit_fn (fmt : Formatter.t) (name, params, body) = + let pp_param (fmt : Formatter.t) (p : param) = match p.pat.p with | PBinding { var; typ; mode = ByValue; mut = Immutable; subpat = None } -> - Format.fprintf fmt "%s : %a" var.name doit_type typ + Stdlib.Format.fprintf fmt "%s : %a" var.name doit_type typ | _ -> assert false in - Format.fprintf fmt "@[proc %s(%a) = {@, @[%a@]@,}@]@\n@\n" name - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ") + Stdlib.Format.fprintf fmt "@[proc %s(%a) = {@, @[%a@]@,}@]@\n@\n" + name + (Stdlib.Format.pp_print_list + ~pp_sep:(fun fmt () -> Stdlib.Format.fprintf fmt ", ") pp_param) params doit_stmt body - and doit_concrete_ident (fmt : Format.formatter) (p : Concrete_ident.t) = - Format.fprintf fmt "%s" (U.Concrete_ident_view.to_definition_name p) - and doit_type (fmt : Format.formatter) (typ : ty) = + and doit_concrete_ident (fmt : Formatter.t) (p : Concrete_ident.t) = + Stdlib.Format.fprintf fmt "%s" (U.Concrete_ident_view.to_definition_name p) + and doit_type (fmt : Formatter.t) (typ : ty) = match typ with | TBool -> assert false | TChar -> assert false - | TInt kind -> Format.fprintf fmt "%s.t" (intmodule_of_kind kind) + | TInt kind -> Stdlib.Format.fprintf fmt "%s.t" (intmodule_of_kind kind) | TFloat _ -> assert false | TStr -> assert false | TApp { ident = `Concrete ident; args = [] } -> doit_concrete_ident fmt ident | TApp { ident = `Concrete ident; args } -> - Format.fprintf fmt "(%a) %a" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ") + Stdlib.Format.fprintf fmt "(%a) %a" + (Stdlib.Format.pp_print_list + ~pp_sep:(fun fmt () -> Stdlib.Format.fprintf fmt ", ") doit_type_arg) args doit_concrete_ident ident | TApp _ -> assert false | TArray _ -> assert false - | TSlice _ -> assert false - | TRawPointer _ -> assert false - | TRef _ -> assert false | TParam _ -> assert false | TArrow (_, _) -> assert false | TAssociatedType _ -> assert false | TOpaque _ -> assert false - and doit_type_arg (fmt : Format.formatter) (tyarg : generic_value) = + | _ -> . + and doit_type_arg (fmt : Formatter.t) (tyarg : generic_value) = match tyarg with GType ty -> doit_type fmt ty | _ -> assert false - and doit_stmt (fmt : Format.formatter) (expr : expr) = + and doit_stmt (fmt : Formatter.t) (expr : expr) = let foo () = - Format.eprintf "%a@.@." pp_expr expr; + Stdlib.Format.eprintf "%a@.@." pp_expr expr; assert false in match expr.e with | If { cond; then_; else_ = None } -> - Format.fprintf fmt "@[if (%a) {@, @[%a@]@,}@]" doit_expr cond - doit_stmt then_ + Stdlib.Format.fprintf fmt "@[if (%a) {@, @[%a@]@,}@]" doit_expr + cond doit_stmt then_ | If _ -> assert false | Let { @@ -204,67 +202,70 @@ let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list { p = PBinding - { mut = _; mode = ByValue; var = { name }; subpat = None }; + { + mut = _; + mode = ByValue; + var = { name; _ }; + subpat = None; + _; + }; + _; }; rhs; body; monadic = None; } -> - Format.fprintf fmt "%s <- %a;@," name doit_expr rhs; - Format.fprintf fmt "%a" doit_stmt body + Stdlib.Format.fprintf fmt "%s <- %a;@," name doit_expr rhs; + Stdlib.Format.fprintf fmt "%a" doit_stmt body | Let { - lhs = { p = PWild; typ = TApp { ident = `TupleType 0; args = [] } }; + lhs = { p = PWild; typ = TApp { ident = `TupleType 0; args = [] }; _ }; rhs; body; monadic = None; } -> - Format.fprintf fmt "%a@," doit_stmt rhs; - Format.fprintf fmt "%a" doit_stmt body + Stdlib.Format.fprintf fmt "%a@," doit_stmt rhs; + Stdlib.Format.fprintf fmt "%a" doit_stmt body | Let _ -> foo () - | Assign { lhs; e } -> - Format.fprintf fmt "%a <- %a;" doit_lhs lhs doit_expr e + | Assign { lhs; e; _ } -> + Stdlib.Format.fprintf fmt "%a <- %a;" doit_lhs lhs doit_expr e | Match _ -> foo () | Loop { body; - kind = ForIndexLoop { start; end_; var = { name }; witness; _ }; + kind = ForIndexLoop { start; end_; var = { name; _ }; _ }; state = None; _; } -> - let vty = - match start.typ with TInt kind -> kind | _ -> assert false - in + let _ = match start.typ with TInt kind -> kind | _ -> assert false in - Format.fprintf fmt "%s <- %a;@," name doit_expr start; - Format.fprintf fmt "@[while (%s < %a) {@, @[%a%t@]@,}@]" name - doit_expr end_ doit_stmt body (fun fmt -> - Format.fprintf fmt "%s <- %s + 1;@," name name) + Stdlib.Format.fprintf fmt "%s <- %a;@," name doit_expr start; + Stdlib.Format.fprintf fmt "@[while (%s < %a) {@, @[%a%t@]@,}@]" + name doit_expr end_ doit_stmt body (fun fmt -> + Stdlib.Format.fprintf fmt "%s <- %s + 1;@," name name) | Loop _ -> foo () - | Return _ -> foo () | MacroInvokation _ -> foo () | GlobalVar (`TupleCons 0) -> () - | Ascription _ | Array _ | Break _ | Continue _ | Closure _ | Borrow _ - | EffectAction _ | AddressOf _ -> - assert false + | Ascription _ | Array _ | Closure _ -> assert false | App _ | Literal _ | Construct _ | LocalVar _ | GlobalVar _ -> - Format.fprintf fmt "return %a;" doit_expr expr + Stdlib.Format.fprintf fmt "return %a;" doit_expr expr | _ -> . - and doit_lhs (fmt : Format.formatter) (lhs : lhs) = + and doit_lhs (fmt : Formatter.t) (lhs : lhs) = match lhs with | LhsFieldAccessor _ -> assert false - | LhsArrayAccessor { e = LhsLocalVar { var = { name } }; index; typ = _ } -> - Format.fprintf fmt "%s.[%a]" name doit_expr index - | LhsArrayAccessor _ -> assert false - | LhsLocalVar { var = { name } } -> Format.fprintf fmt "%s" name - | LhsArbitraryExpr _ -> assert false - and doit_expr (fmt : Format.formatter) (expr : expr) = + | LhsArrayAccessor + { e = LhsLocalVar { var = { name; _ }; _ }; index; typ = _; _ } -> + Stdlib.Format.fprintf fmt "%s.[%a]" name doit_expr index + | LhsLocalVar { var = { name; _ }; _ } -> + Stdlib.Format.fprintf fmt "%s" name + | _ -> . + and doit_expr (fmt : Formatter.t) (expr : expr) = match expr.e with | If _ -> assert false - | App { f = { e = GlobalVar ident }; args = [ a; i ] } + | App { f = { e = GlobalVar ident; _ }; args = [ a; i ]; _ } when Ast.Global_ident.eq_name Core__ops__index__Index__index ident -> - Format.fprintf fmt "(%a).[%a]" doit_expr a doit_expr i - | App { f = { e = GlobalVar (`Concrete op); _ }; args = [ e1; e2 ] } + Stdlib.Format.fprintf fmt "(%a).[%a]" doit_expr a doit_expr i + | App { f = { e = GlobalVar (`Concrete op); _ }; args = [ e1; e2 ]; _ } when Concrete_ident.( eq_name Core__ops__bit__BitXor__bitxor op || eq_name Core__ops__bit__BitAnd__bitand op @@ -273,7 +274,7 @@ let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list || eq_name Core__ops__arith__Mul__mul op || eq_name Core__cmp__PartialEq__ne op || eq_name Core__cmp__PartialEq__eq op) -> - Format.fprintf fmt "(%a) %s (%a)" doit_expr e1 + Stdlib.Format.fprintf fmt "(%a) %s (%a)" doit_expr e1 (match U.Concrete_ident_view.to_definition_name op with | "bitxor" -> "^" | "bitand" -> "&" @@ -284,20 +285,20 @@ let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list | "ne" -> "<>" | _ -> assert false) doit_expr e2 - | App { f = { e = GlobalVar (`Concrete ident) }; args = [] } -> - Format.fprintf fmt "%a" doit_concrete_ident ident - | App { f = { e = GlobalVar (`Concrete ident) }; args } -> - Format.fprintf fmt "%a %a" doit_concrete_ident ident - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt " ") - (fun fmt e -> Format.fprintf fmt "(%a)" doit_expr e)) + | App { f = { e = GlobalVar (`Concrete ident); _ }; args = []; _ } -> + Stdlib.Format.fprintf fmt "%a" doit_concrete_ident ident + | App { f = { e = GlobalVar (`Concrete ident); _ }; args; _ } -> + Stdlib.Format.fprintf fmt "%a %a" doit_concrete_ident ident + (Stdlib.Format.pp_print_list + ~pp_sep:(fun fmt () -> Stdlib.Format.fprintf fmt " ") + (fun fmt e -> Stdlib.Format.fprintf fmt "(%a)" doit_expr e)) args | App _ -> - Format.eprintf "%a@.@." pp_expr expr; + Stdlib.Format.eprintf "%a@.@." pp_expr expr; assert false - | Literal (Int { value; kind }) -> - Format.fprintf fmt "%s.ofint %a" (intmodule_of_kind kind) String.pp - value + | Literal (Int { value; kind; _ }) -> + Stdlib.Format.fprintf fmt "%s.ofint %a" (intmodule_of_kind kind) + String.pp value | Literal _ -> assert false | Array _ -> assert false | Construct @@ -306,30 +307,24 @@ let translate' (bo : BackendOptions.t) (items : AST.item list) : Types.file list is_record = false; is_struct = false; base = None; - fields = args; + fields = _; } -> - Format.eprintf "%a." doit_concrete_ident ident + Stdlib.Format.eprintf "%a." doit_concrete_ident ident | Construct _ -> assert false | Match _ -> assert false | Let _ -> assert false - | LocalVar { name } -> Format.fprintf fmt "%s" name + | LocalVar { name; _ } -> Stdlib.Format.fprintf fmt "%s" name | GlobalVar _ -> assert false | Ascription _ -> assert false | MacroInvokation _ -> assert false | Assign _ -> assert false | Loop _ -> assert false (* | ForLoop _ -> assert false *) - | Break _ -> assert false - | Return _ -> assert false - | Continue _ -> assert false - | Borrow _ -> assert false - | AddressOf _ -> assert false | Closure _ -> assert false - | EffectAction _ -> assert false | _ -> . in - doit Format.err_formatter items; + doit Stdlib.Format.err_formatter items; [] let translate _ (bo : BackendOptions.t) (items : AST.item list) : @@ -352,6 +347,6 @@ Phases.Reject.RawOrMutPointer Features.Rust |> Phases.And_mut_defsite |> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks |> Phases.Reject.Continue |> Phases.Drop_references |> RejectNotEC] -let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) : +let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) : AST.item list = TransformToInputLanguage.ditems items diff --git a/engine/bin/dune b/engine/bin/dune index 185e630c3..085686c48 100644 --- a/engine/bin/dune +++ b/engine/bin/dune @@ -6,6 +6,7 @@ hax_engine fstar_backend coq_backend + ssprove_backend easycrypt_backend proverif_backend logs diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index d45b035cc..7f2291390 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -88,6 +88,7 @@ let run (options : Types.engine_options) : Types.output = match options.backend.backend with | Fstar opts -> run (module Fstar_backend) opts | Coq -> run (module Coq_backend) () + | Ssprove -> run (module Ssprove_backend) () | Easycrypt -> run (module Easycrypt_backend) () | ProVerif -> run (module Proverif_backend) ()) in diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index a88e711e5..8a1457e74 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -2,7 +2,7 @@ open! Prelude module T = Types module Backend = struct - type t = Coq | FStar | EasyCrypt | ProVerif + type t = Coq | SSProve | FStar | EasyCrypt | ProVerif [@@deriving show { with_path = false }, eq, yojson, compare, hash, sexp] end diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index 86f4120db..48ac454a6 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -33,7 +33,7 @@ Import List.ListNotations. Open Scope Z_scope. Open Scope bool_scope. -Class t_Trait Self := { +Class t_Trait (Self : Type) := { }. (*Not implemented yet? todo(item)*) @@ -48,9 +48,9 @@ Definition main_a_c (_ : unit) : unit := tt. Definition main_a (x : T) : unit := - let _ := (main_a_a tt) : unit in - let _ := (main_a_b tt) : unit in - let _ := (main_a_c tt) : unit in + let _ := main_a_a tt : unit in + let _ := main_a_b tt : unit in + let _ := main_a_c tt : unit in tt. Definition main_b_a (_ : unit) : unit := @@ -63,9 +63,9 @@ Definition main_b_c (_ : unit) : unit := tt. Definition main_b (_ : unit) : unit := - let _ := (main_b_a tt) : unit in - let _ := (main_b_b tt) : unit in - let _ := (main_b_c tt) : unit in + let _ := main_b_a tt : unit in + let _ := main_b_b tt : unit in + let _ := main_b_c tt : unit in tt. Definition main_c_a (_ : unit) : unit := @@ -78,20 +78,20 @@ Definition main_c_c (_ : unit) : unit := tt. Definition main_c (_ : unit) : unit := - let _ := (main_c_a tt) : unit in - let _ := (main_c_b tt) : unit in - let _ := (main_c_c tt) : unit in + let _ := main_c_a tt : unit in + let _ := main_c_b tt : unit in + let _ := main_c_c tt : unit in tt. -Record t_Foo : Type :={ +Record t_Foo : Type := { }. -Instance t_Foo_t_t_Trait : t_Trait t_Foo_t := { +#[global] Instance t_Foo_t_t_Trait : t_Trait t_Foo_t := { }. Definition main (_ : unit) : unit := - let _ := (main_a Foot_Foo_t) : unit in - let _ := (main_b tt) : unit in - let _ := (main_c tt) : unit in + let _ := main_a Foot_Foo_t : unit in + let _ := main_b tt : unit in + let _ := main_c tt : unit in tt. ''' diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap index 8e9d75e12..ec402079b 100644 --- a/test-harness/src/snapshots/toolchain__naming into-coq.snap +++ b/test-harness/src/snapshots/toolchain__naming into-coq.snap @@ -17,6 +17,7 @@ info: snapshot: stderr: false stdout: true + include_flag: ~ --- exit = 0 @@ -24,55 +25,6 @@ exit = 0 diagnostics = [] [stdout.files] -"Naming.Ambiguous_names.v" = ''' -(* File automatically generated by Hacspec *) -From Hacspec Require Import Hacspec_Lib MachineIntegers. -From Coq Require Import ZArith. -Import List.ListNotations. -Open Scope Z_scope. -Open Scope bool_scope. - -(*Not implemented yet? todo(item)*) - -Definition debug (label : int32) (value : int32) : unit := - let _ := (v__print (impl_2__new_v1 (unsize (array_from_list [[; - ] a=; - -])) (unsize (array_from_list [impl_1__new_display label; - impl_1__new_display value])))) : unit in - tt. - -Definition f (_ : unit) : unit := - let a_1 := ((@repr WORDSIZE32 104)) : int32 in - let a_2 := ((@repr WORDSIZE32 205)) : int32 in - let a_3 := ((@repr WORDSIZE32 306)) : int32 in - let a := ((@repr WORDSIZE32 123)) : int32 in - let _ := (debug (@repr WORDSIZE32 3) a_3) : unit in - let _ := (debug (@repr WORDSIZE32 2) a_2) : unit in - let _ := (debug (@repr WORDSIZE32 1) a_1) : unit in - debug (@repr WORDSIZE32 4) a. - -Definition ff_expand (_ : unit) : unit := - let a := ((@repr WORDSIZE32 104)) : int32 in - let a := ((@repr WORDSIZE32 205)) : int32 in - let a := ((@repr WORDSIZE32 306)) : int32 in - let a := ((@repr WORDSIZE32 123)) : int32 in - let _ := (debug (@repr WORDSIZE32 3) a) : unit in - let _ := (debug (@repr WORDSIZE32 2) a) : unit in - let _ := (debug (@repr WORDSIZE32 1) a) : unit in - debug (@repr WORDSIZE32 0) a. -''' -"Naming.F.G.Impl_1.G.Hello.v" = ''' -(* File automatically generated by Hacspec *) -From Hacspec Require Import Hacspec_Lib MachineIntegers. -From Coq Require Import ZArith. -Import List.ListNotations. -Open Scope Z_scope. -Open Scope bool_scope. - -Definition h (_ : unit) : unit := - tt. -''' "Naming.v" = ''' (* File automatically generated by Hacspec *) From Hacspec Require Import Hacspec_Lib MachineIntegers. @@ -81,43 +33,37 @@ Import List.ListNotations. Open Scope Z_scope. Open Scope bool_scope. -Record Foo_B : Type :={ - f_x : uint_size; -}. Inductive t_Foo : Type := -| Foo_At_Foo +| Foo_A : t_Foo | Foo_B : Foo_B -> t_Foo. Definition impl__Foo__f (self : t_Foo_t) : t_Foo_t := Foo_At_Foo_t. -Record Foo2_B : Type :={ - f_x : uint_size; -}. Inductive t_Foo2 : Type := -| Foo2_At_Foo2 +| Foo2_A : t_Foo2 | Foo2_B : Foo2_B -> t_Foo2. -Class t_FooTrait Self := { - f_ASSOCIATED_CONSTANT:uint_size ; +Class t_FooTrait (Self : Type) := { + f_ASSOCIATED_CONSTANT : uint_size ; }. -Class t_T1 Self := { +Class t_T1 (Self : Type) := { }. -Instance t_Foo_t_t_T1 : t_T1 t_Foo_t := { +#[global] Instance t_Foo_t_t_T1 : t_T1 t_Foo_t := { }. -Instance (t_Foo_t × int8)_t_T1 : t_T1 (t_Foo_t × int8) := { +#[global] Instance t_Foo_t × int8_t_T1 : t_T1 (t_Foo_t × int8) := { }. -Class t_T2_for_a Self := { +Class t_T2_for_a (Self : Type) := { }. -Class t_T3_e_for_a Self := { +Class t_T3_e_for_a (Self : Type) := { }. -Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := { +#[global] Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := { }. (*Not implemented yet? todo(item)*) @@ -133,11 +79,8 @@ Definition constants (_ : unit) : uint_size := Definition ff__g (_ : unit) : unit := tt. -Record C_f__g__impl__g__Foo_B : Type :={ - f_x : uint_size; -}. Inductive t_f__g__impl__g__Foo : Type := -| C_f__g__impl__g__Foo_At_f__g__impl__g__Foo +| C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo | C_f__g__impl__g__Foo_B : C_f__g__impl__g__Foo_B -> t_f__g__impl__g__Foo. Definition ff__g__impl_1__g (self : t_Foo_t) : uint_size := @@ -148,53 +91,53 @@ Definition ff__g__impl_1__g (self : t_Foo_t) : uint_size := Definition reserved_names (val : int8) (noeq : int8) (of : int8) : int8 := (val.+noeq).+of. -Record t_Arity1 : Type :={ +Record t_Arity1 (T : _) : Type := { 0 : T; }. -Instance t_Arity1_t (t_Foo_t × int8)_t_T2_for_a : t_T2_for_a t_Arity1_t (t_Foo_t × int8) := { +#[global] Instance t_Arity1_t (t_Foo_t × int8)_t_T2_for_a : t_T2_for_a (t_Arity1_t (t_Foo_t × int8)) := { }. -Record t_B : Type :={ +Record t_B : Type := { }. Definition impl__B__f (self : t_B_t) : t_B_t := Bt_B_t. -Record t_C : Type :={ +Record t_C : Type := { f_x : uint_size; }. -Record t_Foobar : Type :={ +Record t_Foobar : Type := { f_a : t_Foo_t; }. -Record t_StructA : Type :={ +Record t_StructA : Type := { f_a : uint_size; }. -Record t_StructB : Type :={ - f_b : uint_size; +Record t_StructB : Type := { f_a : uint_size; + f_b : uint_size; }. -Record t_StructC : Type :={ +Record t_StructC : Type := { f_a : uint_size; }. -Record t_StructD : Type :={ - f_b : uint_size; +Record t_StructD : Type := { f_a : uint_size; + f_b : uint_size; }. -Record t_X : Type :={ +Record t_X : Type := { }. Definition construct_structs (a : uint_size) (b : uint_size) : unit := - let _ := (Build_StructA a) : t_StructA_t in - let _ := (Build_StructB ab) : t_StructB_t in - let _ := (Build_StructC a) : t_StructC_t in - let _ := (Build_StructD ab) : t_StructD_t in + let _ := Build_StructA (f_a := a) : t_StructA_t in + let _ := Build_StructB (f_a := a) (f_b := b) : t_StructB_t in + let _ := Build_StructC (f_a := a) : t_StructC_t in + let _ := Build_StructD (f_a := a) (f_b := b) : t_StructD_t in tt. Definition f (x : t_Foobar_t) : uint_size := @@ -204,7 +147,56 @@ Definition ff__g__impl__g (self : t_B_t) : uint_size := (@repr WORDSIZE32 0). Definition mk_c (_ : unit) : t_C_t := - let _ := (Build_Foo_B (@repr WORDSIZE32 3)) : t_Foo_t in - let _ := (Xt_X_t) : t_X_t in - Build_C (@repr WORDSIZE32 3). + let _ := Build_Foo_B (f_x := (@repr WORDSIZE32 3)) : t_Foo_t in + let _ := Xt_X_t : t_X_t in + Build_C (f_x := (@repr WORDSIZE32 3)). +''' +"Naming_Ambiguous_names.v" = ''' +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib MachineIntegers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +(*Not implemented yet? todo(item)*) + +Definition debug (label : int32) (value : int32) : unit := + let _ := v__print (impl_2__new_v1 (unsize (array_from_list [[; + ] a=; + +])) (unsize (array_from_list [impl_1__new_display label; + impl_1__new_display value]))) : unit in + tt. + +Definition f (_ : unit) : unit := + let a_1 := (@repr WORDSIZE32 104) : int32 in + let a_2 := (@repr WORDSIZE32 205) : int32 in + let a_3 := (@repr WORDSIZE32 306) : int32 in + let a := (@repr WORDSIZE32 123) : int32 in + let _ := debug (@repr WORDSIZE32 3) a_3 : unit in + let _ := debug (@repr WORDSIZE32 2) a_2 : unit in + let _ := debug (@repr WORDSIZE32 1) a_1 : unit in + debug (@repr WORDSIZE32 4) a. + +Definition ff_expand (_ : unit) : unit := + let a := (@repr WORDSIZE32 104) : int32 in + let a := (@repr WORDSIZE32 205) : int32 in + let a := (@repr WORDSIZE32 306) : int32 in + let a := (@repr WORDSIZE32 123) : int32 in + let _ := debug (@repr WORDSIZE32 3) a : unit in + let _ := debug (@repr WORDSIZE32 2) a : unit in + let _ := debug (@repr WORDSIZE32 1) a : unit in + debug (@repr WORDSIZE32 0) a. +''' +"Naming_F_G_Impl_1_G_Hello.v" = ''' +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib MachineIntegers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +Definition h (_ : unit) : unit := + tt. ''' diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap index 82e366f35..1315276b1 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap @@ -36,13 +36,14 @@ Open Scope Z_scope. Open Scope bool_scope. Inductive t_E : Type := -| E_At_E -| E_Bt_E. +| E_A : t_E +| E_B : t_E. (*Not implemented yet? todo(item)*) Definition bar (x : t_E_t) : unit := match x with - | E_A | E_B => tt + | E_A | E_B => + tt end. ''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index 48829d0aa..b5b4e972a 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap @@ -33,8 +33,8 @@ Open Scope Z_scope. Open Scope bool_scope. Inductive t_Foo : Type := -| Foo_At_Foo -| Foo_Bt_Foo. +| Foo_A : t_Foo +| Foo_B : t_Foo. (*Not implemented yet? todo(item)*) @@ -47,7 +47,7 @@ Definition no_dependency_1_ (_ : unit) : unit := Definition no_dependency_2_ (_ : unit) : unit := tt. -Record t_Bar : Type :={ +Record t_Bar : Type := { 0 : t_Foo_t; }. diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap new file mode 100644 index 000000000..c510de7b5 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap @@ -0,0 +1,103 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: reordering + manifest: reordering/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Reordering.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +Definition t_Foo : choice_type := + ('unit ∐ 'unit). +Notation "'Foo_A_case'" := (inl tt) (at level 100). +Equations Foo_A {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_A := + solve_lift (ret_both (inl (tt : 'unit) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. +Notation "'Foo_B_case'" := (inr tt) (at level 100). +Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_B := + solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo := + f _ := + Foo_A : both L1 I1 t_Foo. +Fail Next Obligation. + +Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_1_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_2_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Definition t_Bar : choice_type := + (t_Foo). +Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo := + 0 s := + bind_both s (fun x => + solve_lift (ret_both (x : t_Foo))) : both L I t_Foo. +Fail Next Obligation. +Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_Foo} : both L0 I0 (t_Bar) := + Build_t_Bar := + bind_both 0 (fun 0 => + solve_lift (ret_both ((0) : (t_Bar)))) : both L0 I0 (t_Bar). +Fail Next Obligation. +Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)). + +Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar := + g _ := + Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar. +Fail Next Obligation. +''' diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap new file mode 100644 index 000000000..01ca06526 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -0,0 +1,275 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: side-effects + manifest: side-effects/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ +--- +exit = 0 +stderr = ''' +Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Side_effects.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +(*Not implemented yet? todo(item)*) + +Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := + add3 x y z := + solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. +Fail Next Obligation. + +Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := impl__map_err y f_from in + Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark_coercion y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist1 := impl__map_err y f_from in + Result_Ok (Result_Ok hoist1))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := + early_returns x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) + then letm[choice_typeMonad.result_bind_code int32] hoist2 := v_Break (ret_both (0 : int32)) in + ControlFlow_Continue (never_to_any hoist2) + else () in + letb hoist3 := x >.? (ret_both (30 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3 + then matchb ret_both (true : 'bool) with + | true => + letm[choice_typeMonad.result_bind_code int32] hoist4 := v_Break (ret_both (34 : int32)) in + ControlFlow_Continue (solve_lift (never_to_any hoist4)) + | _ => + ControlFlow_Continue (solve_lift (ret_both (3 : int32))) + end + else ControlFlow_Continue (letb _ := assign todo(term) in + x .+ (ret_both (1 : int32))) in + letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in + letb hoist7 := impl__u32__wrapping_add hoist6 x in + letm[choice_typeMonad.result_bind_code int32] hoist8 := v_Break hoist7 in + ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32. +Fail Next Obligation. + +Definition y_loc : Location := + (int32;0%nat). +Definition y_loc : Location := + (int32;1%nat). +Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 := + local_mutation x := + letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb hoist9 := x >.? (ret_both (3 : int32)) in + solve_lift (ifb hoist9 + then letb _ := assign todo(term) in + letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in + letb _ := assign todo(term) in + letb hoist10 := ret_both (0 : int32) in + letb hoist11 := Build_t_Range (f_start := hoist10) (f_end := ret_both (10 : int32)) in + letb hoist12 := f_into_iter hoist11 in + letb _ := foldi_both_list hoist12 (fun i => + ssp (fun _ => + assign todo(term) : (both (*1*)(L1:|:fset [y_loc]) (I1) 'unit))) (ret_both (tt : 'unit)) in + impl__u32__wrapping_add x y + else letb hoist15 := matchb x with + | 12 => + letb _ := assign todo(term) in + solve_lift (ret_both (3 : int32)) + | 13 => + letb hoist14 := x in + letb _ := assign todo(term) in + letb hoist13 := impl__u32__wrapping_add (ret_both (123 : int32)) x in + solve_lift (add3 hoist14 hoist13 x) + | _ => + solve_lift (ret_both (0 : int32)) + end in + letb _ := assign todo(term) in + impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32. +Fail Next Obligation. + +Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) := + options x y z := + solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist19 := x in + letb hoist20 := hoist19 >.? (ret_both (10 : int8)) in + letm[choice_typeMonad.option_bind_code] hoist26 := ifb hoist20 + then letm[choice_typeMonad.option_bind_code] hoist21 := x in + Option_Some (letb hoist22 := impl__u8__wrapping_add hoist21 (ret_both (3 : int8)) in + Option_Some hoist22) + else letm[choice_typeMonad.option_bind_code] hoist24 := x in + letm[choice_typeMonad.option_bind_code] hoist23 := y in + Option_Some (letb hoist25 := impl__u8__wrapping_add hoist24 hoist23 in + Option_Some hoist25) in + letm[choice_typeMonad.option_bind_code] hoist27 := hoist26 in + letm[choice_typeMonad.option_bind_code] v := matchb hoist27 with + | 3 => + Option_None + | 4 => + letm[choice_typeMonad.option_bind_code] hoist16 := z in + Option_Some (letb hoist17 := hoist16 >.? (ret_both (4 : int64)) in + letb hoist18 := ifb hoist17 + then ret_both (0 : int8) + else ret_both (3 : int8) in + solve_lift ((ret_both (4 : int8)) .+ hoist18)) + | _ => + Option_Some (solve_lift (ret_both (12 : int8))) + end in + letm[choice_typeMonad.option_bind_code] hoist28 := x in + letb hoist30 := impl__u8__wrapping_add v hoist28 in + letm[choice_typeMonad.option_bind_code] hoist29 := y in + Option_Some (letb hoist31 := impl__u8__wrapping_add hoist30 hoist29 in + Option_Some hoist31))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). +Fail Next Obligation. + +Definition y_loc : Location := + (int32;2%nat). +Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) := + question_mark x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32)) + then letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb hoist32 := x >.? (ret_both (90 : int32)) in + ifb hoist32 + then impl__map_err (Result_Err (ret_both (12 : int8))) f_from + else () + else () in + Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32). +Fail Next Obligation. + +Definition t_A : choice_type := + 'unit. +Equations Build_t_A : both (fset []) (fset []) (t_A) := + Build_t_A := + solve_lift (ret_both (tt (* Empty tuple *) : (t_A))) : both (fset []) (fset []) (t_A). +Fail Next Obligation. + +Definition t_B : choice_type := + 'unit. +Equations Build_t_B : both (fset []) (fset []) (t_B) := + Build_t_B := + solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B). +Fail Next Obligation. + +Definition t_Bar : choice_type := + ('bool × nseq ('bool × 'bool) 6 × 'bool). +Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool := + f_a s := + bind_both s (fun x => + solve_lift (ret_both (fst x : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_b {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I (nseq ('bool × 'bool) 6 × 'bool) := + f_b s := + bind_both s (fun x => + solve_lift (ret_both (snd x : (nseq ('bool × 'bool) 6 × 'bool)))) : both L I (nseq ('bool × 'bool) 6 × 'bool). +Fail Next Obligation. +Equations Build_t_Bar {L0 : {fset Location}} {L1 : {fset Location}} {I0 : Interface} {I1 : Interface} {f_a : both L0 I0 'bool} {f_b : both L1 I1 (nseq ('bool × 'bool) 6 × 'bool)} : both (L0:|:L1) (I0:|:I1) (t_Bar) := + Build_t_Bar := + bind_both f_b (fun f_b => + bind_both f_a (fun f_a => + solve_lift (ret_both ((f_a,f_b) : (t_Bar))))) : both (L0:|:L1) (I0:|:I1) (t_Bar). +Fail Next Obligation. +Notation "'Build_t_Bar' '[' x ']' '(' 'f_a' ':=' y ')'" := (Build_t_Bar (f_a := y) (f_b := f_b x)). +Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := f_a x) (f_b := y)). + +Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := + monad_lifting x := + solve_lift (run (ifb x >.? (ret_both (123 : int8)) + then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (impl__map_err (Result_Err B) f_from) in + letb hoist34 := Result_Ok hoist33 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := v_Break hoist34 in + ControlFlow_Continue (never_to_any hoist35) + else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). +Fail Next Obligation. + +Definition t_Foo : choice_type := + ('bool × 'bool × t_Vec t_Bar t_Global × nseq t_Bar 6 × t_Bar). +Equations f_x {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I 'bool := + f_x s := + bind_both s (fun x => + solve_lift (ret_both (fst (fst (fst x)) : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I ('bool × t_Vec t_Bar t_Global) := + f_y s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst (fst x)) : ('bool × t_Vec t_Bar t_Global)))) : both L I ('bool × t_Vec t_Bar t_Global). +Fail Next Obligation. +Equations f_z {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I (nseq t_Bar 6) := + f_z s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst x) : (nseq t_Bar 6)))) : both L I (nseq t_Bar 6). +Fail Next Obligation. +Equations f_bar {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I t_Bar := + f_bar s := + bind_both s (fun x => + solve_lift (ret_both (snd x : t_Bar))) : both L I t_Bar. +Fail Next Obligation. +Equations Build_t_Foo {L0 : {fset Location}} {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I0 : Interface} {I1 : Interface} {I2 : Interface} {I3 : Interface} {f_x : both L0 I0 'bool} {f_y : both L1 I1 ('bool × t_Vec t_Bar t_Global)} {f_z : both L2 I2 (nseq t_Bar 6)} {f_bar : both L3 I3 t_Bar} : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo) := + Build_t_Foo := + bind_both f_bar (fun f_bar => + bind_both f_z (fun f_z => + bind_both f_y (fun f_y => + bind_both f_x (fun f_x => + solve_lift (ret_both ((f_x,f_y,f_z,f_bar) : (t_Foo))))))) : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo). +Fail Next Obligation. +Notation "'Build_t_Foo' '[' x ']' '(' 'f_x' ':=' y ')'" := (Build_t_Foo (f_x := y) (f_y := f_y x) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := y) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)). + +Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo := + assign_non_trivial_lhs foo := + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + solve_lift foo : both L1 I1 t_Foo. +Fail Next Obligation. +''' diff --git a/tests/enum-repr/Cargo.toml b/tests/enum-repr/Cargo.toml index eec13f544..cfc6cefdf 100644 --- a/tests/enum-repr/Cargo.toml +++ b/tests/enum-repr/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "162" } +into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "162" } diff --git a/tests/enum-struct-variant/Cargo.toml b/tests/enum-struct-variant/Cargo.toml index c6fba86f4..5651c0608 100644 --- a/tests/enum-struct-variant/Cargo.toml +++ b/tests/enum-struct-variant/Cargo.toml @@ -9,3 +9,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar+coq" = {broken = false, snapshot = "none"} +into."ssprove" = {broken = true, snapshot = "none"} \ No newline at end of file diff --git a/tests/if-let/Cargo.toml b/tests/if-let/Cargo.toml index fe86f0b0e..544318ca9 100644 --- a/tests/if-let/Cargo.toml +++ b/tests/if-let/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "85" } +into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "85" } diff --git a/tests/literals/Cargo.toml b/tests/literals/Cargo.toml index f70ce2bfc..319378b16 100644 --- a/tests/literals/Cargo.toml +++ b/tests/literals/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar" = { broken = false, snapshot = "none", issue_id = "85" } into."coq" = { broken = true, snapshot = "none", issue_id = "85" } +into."ssprove" = { broken = true, snapshot = "none", issue_id = "85" } diff --git a/tests/loops/Cargo.toml b/tests/loops/Cargo.toml index 033a5bf29..a6139c47a 100644 --- a/tests/loops/Cargo.toml +++ b/tests/loops/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar" = { } into."coq" = { broken = true, snapshot = "none", issue_id = "137" } +into."ssprove" = { broken = true, snapshot = "none", issue_id = "137" } diff --git a/tests/nested-derefs/Cargo.toml b/tests/nested-derefs/Cargo.toml index f40fa4504..d28b7545e 100644 --- a/tests/nested-derefs/Cargo.toml +++ b/tests/nested-derefs/Cargo.toml @@ -4,4 +4,4 @@ version = "0.1.0" edition = "2021" [package.metadata.hax-tests] -into."fstar+coq" = { snapshot = "none" } +into."fstar+coq+ssprove" = { snapshot = "none" } diff --git a/tests/pattern-or/Cargo.toml b/tests/pattern-or/Cargo.toml index abce1ec8e..31b4a1901 100644 --- a/tests/pattern-or/Cargo.toml +++ b/tests/pattern-or/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."coq" = { issue_id = "161" } into."fstar" = { } +# into."ssprove" = { broken = true, snapshot = "none" } \ No newline at end of file diff --git a/tests/reordering/Cargo.toml b/tests/reordering/Cargo.toml index 189657e54..937ec2bf8 100644 --- a/tests/reordering/Cargo.toml +++ b/tests/reordering/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { snapshot = "stdout" } +into."fstar+coq+ssprove" = { snapshot = "stdout" } diff --git a/tests/side-effects/Cargo.toml b/tests/side-effects/Cargo.toml index 3f113dc10..f946b27d2 100644 --- a/tests/side-effects/Cargo.toml +++ b/tests/side-effects/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into.fstar = {} into.coq = {broken = true, snapshot = "none", issue_id = 134} +into.ssprove = {}