From 96befa6e89933702509a4519c830ae42a52e204e Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Wed, 9 Oct 2024 16:21:22 +0200 Subject: [PATCH 1/6] AST printer --- engine/backends/coq/coq/coq_backend.ml | 1188 ++++++++++++------------ 1 file changed, 581 insertions(+), 607 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 11f29348f..a455fc320 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -63,12 +63,9 @@ struct 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 CoqLibrary : Library = struct module Notation = struct @@ -83,621 +80,598 @@ end module C = Coq (CoqLibrary) -module Context = struct - type t = { current_namespace : string * string list } -end - -let primitive_to_string (id : primitive_ident) : string = - match id with - | Deref -> "(TODO: Deref)" (* failwith "Deref" *) - | Cast -> "cast" (* failwith "Cast" *) - | LogicalOp op -> ( match op with And -> "andb" | Or -> "orb") +open Ast -module Make (Ctx : sig - val ctx : Context.t -end) = +module Make + (F : Features.T) (Default : sig + val default : string -> string + end) = struct - open Ctx - - let pconcrete_ident (id : concrete_ident) : string = - let id = U.Concrete_ident_view.to_view id in - let crate, path = ctx.current_namespace in - if String.(crate = id.crate) && [%eq: string list] id.path path then - id.definition - else - (* id.crate ^ "_" ^ *) - (* List.fold_left ~init:"" ~f:(fun x y -> x ^ "_" ^ y) *) - id.definition - - let pglobal_ident (id : 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 _) | `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.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 + module AST = Ast.Make (F) + open Ast.Make (F) + module Base = Generic_printer.Make (F) + open PPrint - module TODOs = struct - let __TODO_ty__ span s : C.AST.ty = - Error.unimplemented ~details:("[ty] node " ^ s) span + let default_string_for s = "TODO: please implement the method `" ^ s ^ "`" + let default_document_for = default_string_for >> string - let __TODO_pat__ span s = - Error.unimplemented ~details:("[pat] node " ^ s) span + let any_number_of x = brackets ( x ) ^^ string "*" + let option_of x = brackets ( x ) ^^ string "?" - let __TODO_term__ span s = - Error.unimplemented ~details:("[expr] node " ^ s) span + class printer = + object + inherit Base.base - let __TODO_item__ _span s = C.AST.Unimplemented (s ^ " todo(item)") - end + (* BEGIN GENERATED *) + method arm ~arm:_ ~span:_ = default_document_for "arm" + + method arm' ~super:_ ~arm_pat:_ ~body:_ ~guard:_ = + default_document_for "arm'" + + method attrs _x1 = default_document_for "attrs" + + method binding_mode_ByRef _x1 _x2 = + default_document_for "binding_mode_ByRef" + + method binding_mode_ByValue = default_document_for "binding_mode_ByValue" + method borrow_kind_Mut _x1 = default_document_for "borrow_kind_Mut" + method borrow_kind_Shared = default_document_for "borrow_kind_Shared" + method borrow_kind_Unique = default_document_for "borrow_kind_Unique" + method common_array _x1 = default_document_for "common_array" + + method dyn_trait_goal ~trait:_ ~non_self_args:_ = + default_document_for "dyn_trait_goal" + + method error_expr _x1 = default_document_for "error_expr" + method error_item _x1 = default_document_for "error_item" + method error_pat _x1 = default_document_for "error_pat" + method expr ~e:_ ~span:_ ~typ:_ = default_document_for "expr" + + method expr'_AddressOf ~super:_ ~mut:_ ~e:_ ~witness:_ = + default_document_for "expr'_AddressOf" + + method expr'_App_application ~super:_ ~f:_ ~args:_ ~generics:_ = + default_document_for "expr'_App_application" + + method expr'_App_constant ~super:_ ~constant:_ ~generics:_ = + default_document_for "expr'_App_constant" + + method expr'_App_field_projection ~super:_ ~field:_ ~e:_ = + default_document_for "expr'_App_field_projection" + + method expr'_App_tuple_projection ~super:_ ~size:_ ~nth:_ ~e:_ = + default_document_for "expr'_App_tuple_projection" + + method expr'_Ascription ~super:_ ~e:_ ~typ:_ = + default_document_for "expr'_Ascription" + + method expr'_Assign ~super:_ ~lhs:_ ~e:_ ~witness:_ = + default_document_for "expr'_Assign" + + method expr'_Block ~super:_ ~e:_ ~safety_mode:_ ~witness:_ = + default_document_for "expr'_Block" + + method expr'_Borrow ~super:_ ~kind:_ ~e:_ ~witness:_ = + default_document_for "expr'_Borrow" + + method expr'_Break ~super:_ ~e:_ ~label:_ ~witness:_ = + default_document_for "expr'_Break" + + method expr'_Closure ~super:_ ~params:_ ~body:_ ~captures:_ = + default_document_for "expr'_Closure" + + method expr'_Construct_inductive ~super:_ ~constructor:_ ~is_record:_ + ~is_struct:_ ~fields:_ ~base:_ = + default_document_for "expr'_Construct_inductive" + + method expr'_Construct_tuple ~super:_ ~components:_ = + default_document_for "expr'_Construct_tuple" + + method expr'_Continue ~super:_ ~e:_ ~label:_ ~witness:_ = + default_document_for "expr'_Continue" + + method expr'_EffectAction ~super:_ ~action:_ ~argument:_ = + default_document_for "expr'_EffectAction" + + method expr'_GlobalVar ~super:_ _x2 = + default_document_for "expr'_GlobalVar" + + method expr'_If ~super:_ ~cond:_ ~then_:_ ~else_:_ = + default_document_for "expr'_If" + + method expr'_Let ~super:_ ~monadic:_ ~lhs:_ ~rhs:_ ~body:_ = + default_document_for "expr'_Let" + + method expr'_Literal ~super:_ _x2 = default_document_for "expr'_Literal" + method expr'_LocalVar ~super:_ _x2 = default_document_for "expr'_LocalVar" + + method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~label:_ ~witness:_ = + default_document_for "expr'_Loop" + + method expr'_MacroInvokation ~super:_ ~macro:_ ~args:_ ~witness:_ = + default_document_for "expr'_MacroInvokation" + + method expr'_Match ~super:_ ~scrutinee:_ ~arms:_ = + default_document_for "expr'_Match" + + method expr'_QuestionMark ~super:_ ~e:_ ~return_typ:_ ~witness:_ = + default_document_for "expr'_QuestionMark" + + method expr'_Quote ~super:_ _x2 = default_document_for "expr'_Quote" + + method expr'_Return ~super:_ ~e:_ ~witness:_ = + default_document_for "expr'_Return" + + method field_pat ~field:_ ~pat:_ = default_document_for "field_pat" + + method generic_constraint_GCLifetime _x1 _x2 = + default_document_for "generic_constraint_GCLifetime" + + method generic_constraint_GCProjection _x1 = + default_document_for "generic_constraint_GCProjection" + + method generic_constraint_GCType _x1 = + default_document_for "generic_constraint_GCType" + + method generic_param ~ident:_ ~span:_ ~attrs:_ ~kind:_ = + default_document_for "generic_param" + + method generic_param_kind_GPConst ~typ:_ = + default_document_for "generic_param_kind_GPConst" + + method generic_param_kind_GPLifetime ~witness:_ = + default_document_for "generic_param_kind_GPLifetime" + + method generic_param_kind_GPType ~default:_ = + default_document_for "generic_param_kind_GPType" + + method generic_value_GConst _x1 = + default_document_for "generic_value_GConst" + + method generic_value_GLifetime ~lt:_ ~witness:_ = + default_document_for "generic_value_GLifetime" + + method generic_value_GType _x1 = + default_document_for "generic_value_GType" + + method generics ~params:_ ~constraints:_ = default_document_for "generics" + method guard ~guard:_ ~span:_ = default_document_for "guard" + + method guard'_IfLet ~super:_ ~lhs:_ ~rhs:_ ~witness:_ = + default_document_for "guard'_IfLet" + + method impl_expr ~kind:_ ~goal:_ = default_document_for "impl_expr" + + method impl_expr_kind_Builtin _x1 = + default_document_for "impl_expr_kind_Builtin" + + method impl_expr_kind_Concrete _x1 = + default_document_for "impl_expr_kind_Concrete" + + method impl_expr_kind_Dyn = default_document_for "impl_expr_kind_Dyn" + + method impl_expr_kind_ImplApp ~impl:_ ~args:_ = + default_document_for "impl_expr_kind_ImplApp" + + method impl_expr_kind_LocalBound ~id:_ = + default_document_for "impl_expr_kind_LocalBound" + + method impl_expr_kind_Parent ~impl:_ ~ident:_ = + default_document_for "impl_expr_kind_Parent" + + method impl_expr_kind_Projection ~impl:_ ~item:_ ~ident:_ = + default_document_for "impl_expr_kind_Projection" + + method impl_expr_kind_Self = default_document_for "impl_expr_kind_Self" + method impl_ident ~goal:_ ~name:_ = default_document_for "impl_ident" + + method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v:_ ~ii_ident:_ ~ii_attrs:_ + = + default_document_for "impl_item" + + method impl_item'_IIFn ~body:_ ~params:_ = + default_document_for "impl_item'_IIFn" + + method impl_item'_IIType ~typ:_ ~parent_bounds:_ = + default_document_for "impl_item'_IIType" + + method item ~v ~span:_ ~ident:_ ~attrs:_ = v#p (* default_document_for "item" *) + + method item'_Alias ~super:_ ~name:_ ~item:_ = + default_document_for "item'_Alias" + + method item'_Fn ~super:_ ~name:_ ~generics:_ ~body:_ ~params:_ ~safety:_ = + (* TODOD: pub, const, pub(crate) *) + string "" ^^ space ^^ string "fn" ^^ space ^^ string "" ^^ parens ( any_number_of (string "" ^^ space ^^ colon ^^ string "") ) ^^ braces ( string "" ) + + + method item'_HaxError ~super:_ _x2 = default_document_for "item'_HaxError" + + method item'_IMacroInvokation ~super:_ ~macro:_ ~argument:_ ~span:_ + ~witness:_ = + default_document_for "item'_IMacroInvokation" + + method item'_Impl ~super:_ ~generics:_ ~self_ty:_ ~of_trait:_ ~items:_ + ~parent_bounds:_ ~safety:_ = + default_document_for "item'_Impl" + + method item'_NotImplementedYet = + default_document_for "item'_NotImplementedYet" + + method item'_Quote ~super:_ _x2 = default_document_for "item'_Quote" + + method item'_Trait ~super:_ ~name:_ ~generics:_ ~items:_ ~safety:_ = + string "trait" ^^ space ^^ string "" ^^ braces ( any_number_of (string "") ) + + method item'_TyAlias ~super:_ ~name:_ ~generics:_ ~ty:_ = + string "type" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ string "" + + method item'_Type ~super:_ ~name:_ ~generics:_ ~variants:_ ~is_struct = + (* TODO globality *) + if is_struct + then string "struct" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ braces ( any_number_of ( string "" ^^ colon ^^ space ^^ string "" ^^ comma ) ) + else string "enum" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ braces ( any_number_of (string "" ^^ option_of (parens (any_number_of (string ""))) ^^ comma ) ) + + method item'_Use ~super:_ ~path:_ ~is_external:_ ~rename:_ = + default_document_for "item'_Use" + + method lhs_LhsArbitraryExpr ~e:_ ~witness:_ = + default_document_for "lhs_LhsArbitraryExpr" + + method lhs_LhsArrayAccessor ~e:_ ~typ:_ ~index:_ ~witness:_ = + default_document_for "lhs_LhsArrayAccessor" + + method lhs_LhsFieldAccessor_field ~e:_ ~typ:_ ~field:_ ~witness:_ = + default_document_for "lhs_LhsFieldAccessor_field" + + method lhs_LhsFieldAccessor_tuple ~e:_ ~typ:_ ~nth:_ ~size:_ ~witness:_ = + default_document_for "lhs_LhsFieldAccessor_tuple" + + method lhs_LhsLocalVar ~var:_ ~typ:_ = + default_document_for "lhs_LhsLocalVar" + + method literal_Bool _x1 = default_document_for "literal_Bool" + method literal_Char _x1 = default_document_for "literal_Char" + + method literal_Float ~value:_ ~negative:_ ~kind:_ = + default_document_for "literal_Float" + + method literal_Int ~value:_ ~negative:_ ~kind:_ = + default_document_for "literal_Int" + + method literal_String _x1 = default_document_for "literal_String" + + method loop_kind_ForIndexLoop ~start:_ ~end_:_ ~var:_ ~var_typ:_ + ~witness:_ = + default_document_for "loop_kind_ForIndexLoop" + + method loop_kind_ForLoop ~pat:_ ~it:_ ~witness:_ = + default_document_for "loop_kind_ForLoop" + + method loop_kind_UnconditionalLoop = + default_document_for "loop_kind_UnconditionalLoop" + + method loop_kind_WhileLoop ~condition:_ ~witness:_ = + default_document_for "loop_kind_WhileLoop" + + method loop_state ~init:_ ~bpat:_ ~witness:_ = + default_document_for "loop_state" + + method modul _x1 = default_document_for "modul" + + method param ~pat:_ ~typ:_ ~typ_span:_ ~attrs:_ = + default_document_for "param" + + method pat ~p:_ ~span:_ ~typ:_ = default_document_for "pat" + + method pat'_PAscription ~super:_ ~typ:_ ~typ_span:_ ~pat:_ = + default_document_for "pat'_PAscription" + + method pat'_PBinding ~super:_ ~mut:_ ~mode:_ ~var:_ ~typ:_ ~subpat:_ = + default_document_for "pat'_PBinding" + + method pat'_PConstant ~super:_ ~lit:_ = + default_document_for "pat'_PConstant" + + method pat'_PConstruct_inductive ~super:_ ~constructor:_ ~is_record:_ + ~is_struct:_ ~fields:_ = + default_document_for "pat'_PConstruct_inductive" + + method pat'_PConstruct_tuple ~super:_ ~components:_ = + default_document_for "pat'_PConstruct_tuple" + + method pat'_PDeref ~super:_ ~subpat:_ ~witness:_ = + default_document_for "pat'_PDeref" + + method pat'_PWild = default_document_for "pat'_PWild" + method printer_name = default_string_for "printer_name" + + method projection_predicate ~impl:_ ~assoc_item:_ ~typ:_ = + default_document_for "projection_predicate" + + method safety_kind_Safe = default_document_for "safety_kind_Safe" + method safety_kind_Unsafe _x1 = default_document_for "safety_kind_Unsafe" + + method supported_monads_MException _x1 = + default_document_for "supported_monads_MException" + + method supported_monads_MOption = + default_document_for "supported_monads_MOption" + + method supported_monads_MResult _x1 = + default_document_for "supported_monads_MResult" + + method trait_goal ~trait:_ ~args:_ = default_document_for "trait_goal" + + method trait_item ~ti_span:_ ~ti_generics:_ ~ti_v:_ ~ti_ident:_ + ~ti_attrs:_ = + default_document_for "trait_item" + + method trait_item'_TIDefault ~params:_ ~body:_ ~witness:_ = + default_document_for "trait_item'_TIDefault" + + method trait_item'_TIFn _x1 = default_document_for "trait_item'_TIFn" + method trait_item'_TIType _x1 = default_document_for "trait_item'_TIType" + + method ty_TApp_application ~typ:_ ~generics:_ = + default_document_for "ty_TApp_application" + + method ty_TApp_tuple ~types:_ = default_document_for "ty_TApp_tuple" + method ty_TArray ~typ:_ ~length:_ = default_document_for "ty_TArray" + method ty_TArrow _x1 _x2 = default_document_for "ty_TArrow" + + method ty_TAssociatedType ~impl:_ ~item:_ = + default_document_for "ty_TAssociatedType" + + method ty_TBool = default_document_for "ty_TBool" + method ty_TChar = default_document_for "ty_TChar" + method ty_TDyn ~witness:_ ~goals:_ = default_document_for "ty_TDyn" + method ty_TFloat _x1 = default_document_for "ty_TFloat" + method ty_TInt _x1 = default_document_for "ty_TInt" + method ty_TOpaque _x1 = default_document_for "ty_TOpaque" + method ty_TParam _x1 = default_document_for "ty_TParam" + method ty_TRawPointer ~witness:_ = default_document_for "ty_TRawPointer" + + method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut:_ = + default_document_for "ty_TRef" + + method ty_TSlice ~witness:_ ~ty:_ = default_document_for "ty_TSlice" + method ty_TStr = default_document_for "ty_TStr" - open TODOs - - let pint_kind (k : int_kind) : C.AST.int_type = - { - size = - (match k.size with - | S8 -> U8 - | S16 -> U16 - | S32 -> U32 - | S64 -> U64 - | S128 -> U128 - | SSize -> USize); - signed = (match k.signedness with Signed -> true | _ -> false); - } - - 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) - | Float _ -> Error.unimplemented ~details:"pliteral: Float" span - | Bool b -> C.AST.Const_bool b - - let rec pty span (t : ty) : C.AST.ty = - match t with - | TBool -> C.AST.Bool - | TChar -> __TODO_ty__ span "char" - | TInt k -> C.AST.Int (pint_kind k) - | TStr -> __TODO_ty__ span "str" - | 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 - (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; _ } -> - C.AST.ArrayTy (pty span typ, "TODO: Int.to_string length") - | TSlice { ty; _ } -> C.AST.SliceTy (pty span ty) - | TParam i -> C.AST.NameTy i.name - | TAssociatedType _ -> C.AST.WildTy - | TOpaque _ -> __TODO_ty__ span "pty: TAssociatedType/TOpaque" - | _ -> . - - and args_ty span (args : generic_value list) : C.AST.ty list = - (* List.map ~f:pty *) - match args with - | arg :: xs -> - (match arg with - | GLifetime _ -> __TODO_ty__ span "lifetime" - | GType x -> pty span x - | GConst _ -> __TODO_ty__ span "const") - :: args_ty span xs - | [] -> [] - - let rec ppat (p : pat) : C.AST.pat = - match p.p with - | PWild -> C.AST.WildPat - | PAscription { typ; pat; _ } -> - C.AST.AscriptionPat (ppat pat, pty p.span typ) - | PBinding - { - mut = Immutable; - mode = _; - subpat = None; - var; - typ = _ (* we skip type annot here *); - } -> - C.AST.Ident var.name - | POr { subpats } -> C.AST.DisjunctivePat (List.map ~f:ppat subpats) - | PArray _ -> __TODO_pat__ p.span "Parray?" - | PConstruct { constructor = `TupleCons 0; fields = []; _ } -> C.AST.UnitPat - | PConstruct { constructor = `TupleCons 1; fields = [ _ ]; _ } -> - __TODO_pat__ p.span "tuple 1" - | PConstruct { constructor = `TupleCons _n; fields; _ } -> - C.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) fields) - | PConstruct { constructor; fields; is_record = true; _ } -> - C.AST.RecordPat (pglobal_ident constructor, pfield_pats fields) - | PConstruct { constructor; fields; is_record = false; _ } -> - C.AST.ConstructorPat - (pglobal_ident constructor, List.map ~f:(fun p -> ppat p.pat) fields) - | PConstant { lit } -> C.AST.Lit (pliteral p.span lit) - | _ -> . - - and pfield_pats (args : field_pat list) : (string * C.AST.pat) list = - match args with - | { field; pat } :: xs -> (pglobal_ident field, ppat pat) :: pfield_pats xs - | _ -> [] - - (* TODO: I guess this should be named `notations` rather than `operators`, for the Coq backend, right? *) - let operators = - let c = Global_ident.of_name Value in - [ - (c Rust_primitives__hax__array_of_list, (3, [ ""; ".["; "]<-"; "" ])); - (c Core__ops__index__Index__index, (2, [ ""; ".["; "]" ])); - (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 "; "" ])); - (* TODO: those two are not notations/operators at all, right? *) - (* (c "secret_integers::rotate_left", (2, [ "rol "; " "; "" ])); *) - (* (c "hacspec::lib::foldi", (4, [ "foldi "; " "; " "; " "; "" ])); *) - - (* (c "secret_integers::u8", (0, ["U8"])); *) - (* (c "secret_integers::u16", (0, ["U16"])); *) - (* (c "secret_integers::u32", (0, ["U32"])); *) - (* (c "secret_integers::u64", (0, ["U64"])); *) - (* (c "secret_integers::u128", (0, ["U128"])); *) - ] - |> Map.of_alist_exn (module Global_ident) - - let rec pexpr (e : expr) = - try pexpr_unwrapped e - with Diagnostics.SpanFreeError.Exn _ -> - TODOs_debug.__TODO_term__ e.span "failure" - - and pexpr_unwrapped (e : expr) : C.AST.term = - let span = e.span in - match e.e with - | Literal l -> C.AST.Const (pliteral e.span l) - | LocalVar local_ident -> C.AST.NameTerm local_ident.name - | GlobalVar (`TupleCons 0) - | Construct { constructor = `TupleCons 0; fields = []; _ } -> - C.AST.UnitTerm - | GlobalVar global_ident -> C.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 - Error.assertion_failure span "expr: function application: bad arity"; - 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; _ } -> - let base = pexpr f in - let args = List.map ~f:pexpr args in - C.AST.App (base, args) - | If { cond; then_; else_ } -> - C.AST.If - ( pexpr cond, - 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 } -> - 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; - } - | Match { scrutinee; arms } -> - C.AST.Match - ( pexpr scrutinee, - List.map - ~f:(fun { arm = { arm_pat; body; _ }; _ } -> - (ppat arm_pat, pexpr body)) - arms ) - | Ascription _ -> __TODO_term__ span "asciption" - | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> - pexpr e - | Construct { constructor = `TupleCons _n; fields; _ } -> - C.AST.Tuple (List.map ~f:(snd >> pexpr) fields) - | Construct { is_record = true; constructor; fields; _ } -> - (* TODO: handle base *) - C.AST.RecordConstructor - ( pglobal_ident constructor, - List.map ~f:(fun (f, e) -> (pglobal_ident f, pexpr e)) fields ) - | Construct { is_record = false; constructor; fields = [ (_f, e) ]; _ } -> - C.AST.App (C.AST.Var (pglobal_ident constructor), [ pexpr e ]) - | Construct { constructor; _ } -> - (* __TODO_term__ span "constructor" *) - C.AST.Var - (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; _ } -> - Error.raise - @@ { - kind = UnsupportedMacro { id = [%show: global_ident] macro }; - span = e.span; - } - | _ -> . - - 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 pitem_unwrapped (e : item) : C.AST.decl list = - let span = e.span in - match e.v with - | Fn { name; body; params; _ } -> - [ - C.AST.Definition - ( pconcrete_ident name, - List.map - ~f:(fun { pat; typ; _ } -> - C.AST.Explicit (ppat pat, pty span typ)) - params, - pexpr body, - pty span body.typ ); - ] - | 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, - 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; _ } -> - [ - C.AST.Inductive - ( U.Concrete_ident_view.to_definition_name name, - List.map ~f:(pgeneric_param_as_argument span) generics.params, - p_inductive span variants name ); - ] - (* TODO: this is never matched, now *) - (* | Type { name; generics; variants } -> *) - (* [ *) - (* C.AST.Notation *) - (* ( U.Concrete_ident_view.to_definition_name name, *) - (* C.AST.Product (List.map ~f:snd (p_record span variants name)) ); *) - (* C.AST.Definition *) - (* ( U.Concrete_ident_view.to_definition_name name, *) - (* [], *) - (* C.AST.Var "id", *) - (* C.AST.Arrow *) - (* ( 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; _ } -> ( - 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 - [ - C.AST.Notation - ( "'" ^ 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.NameTy (o.type_name ^ "_t"), - C.AST.NameTy (o.type_name ^ "_t") ) ); - ] - | "bytes" -> - let open Hacspeclib_macro_parser in - let o : Bytes.t = - Bytes.parse argument |> Result.ok_or_failwith - in - [ - C.AST.Notation - ( "'" ^ 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.NameTy (o.bytes_name ^ "_t"), - C.AST.NameTy (o.bytes_name ^ "_t") ) ); - ] - | "unsigned_public_integer" -> - let open Hacspeclib_macro_parser in - let o = - UnsignedPublicInteger.parse argument |> Result.ok_or_failwith - in - [ - C.AST.Notation - ( "'" ^ 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.NameTy (o.integer_name ^ "_t"), - C.AST.NameTy (o.integer_name ^ "_t") ) ); - ] - | "public_bytes" -> - let open Hacspeclib_macro_parser in - let o : Bytes.t = - Bytes.parse argument |> Result.ok_or_failwith - in - let typ = - C.AST.ArrayTy - ( C.AST.Int { size = C.AST.U8; signed = false }, - (* int_of_string *) o.size ) - in - [ - 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.NameTy (o.bytes_name ^ "_t"), - C.AST.NameTy (o.bytes_name ^ "_t") ) ); - ] - | "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 - (* Some *) - | "U128" -> C.AST.U128 - (* Some *) - | "U64" -> C.AST.U64 - (* Some *) - | "U32" -> C.AST.U32 - (* Some *) - | "U16" -> C.AST.U16 - (* Some *) - | "U8" -> C.AST.U8 - | _usize -> C.AST.U32 (* TODO: usize? *) - in - [ - C.AST.Notation - ( "'" ^ 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.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 (None, 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; generics; items } -> - [ - 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 -> - 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 - | TIDefault _ -> . - | _ -> __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 - ~f:(fun x -> - match x.ii_v with - | IIFn { body; params } -> - ( U.Concrete_ident_view.to_definition_name x.ii_ident, - List.map - ~f:(fun { pat; typ; _ } -> - C.AST.Explicit (ppat pat, pty span typ)) - params, - pexpr body, - pty span body.typ ) - | _ -> - ( "todo_name", - [], - __TODO_term__ span "body", - __TODO_ty__ span "typ" )) - items ); - ] - - 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, - C.AST.RecordTy - (pconcrete_ident name, p_record_record span arguments) ) - else - let name = U.Concrete_ident_view.to_definition_name name in - match arguments with - | [] -> C.AST.BaseCase name - | [ (_arg_name, arg_ty, _arg_attrs) ] -> - C.AST.InductiveCase (name, pty span arg_ty) - | _ -> - C.AST.InductiveCase - (name, C.AST.Product (List.map ~f:(snd3 >> pty span) arguments))) - (* match variants with _ -> [] *) - (* TODO: I don't get this pattern maching below. Variant with more than one payloads are rejected implicitely? *) - (* | { name; arguments = [ (arg_name, arg_ty) ] } :: xs -> *) - (* if (index_of_field >> Option.is_some) arg_name then *) - (* C.AST.InductiveCase (U.Concrete_ident_view.to_definition_name name, pty span arg_ty) *) - (* :: p_inductive span xs parrent_name *) - (* else *) - (* C.AST.InductiveCase (U.Concrete_ident_view.to_definition_name arg_name, pty span arg_ty) *) - (* :: p_inductive span xs parrent_name *) - (* | { name; arguments = [] } :: xs -> *) - (* C.AST.BaseCase (U.Concrete_ident_view.to_definition_name name) *) - (* :: p_inductive span xs parrent_name *) - (* | { name; arguments } :: xs -> *) - (* C.AST.InductiveCase *) - (* ( U.Concrete_ident_view.to_definition_name name, *) - (* C.AST.RecordTy (pglobal_ident name, p_record_record span arguments) *) - (* ) *) - (* :: p_inductive span xs parrent_name *) - (* | _ -> [] *) - - and p_record_record span arguments : (string * C.AST.ty) list = - List.map - ~f:(function - | arg_name, arg_ty, _arg_attrs -> - (U.Concrete_ident_view.to_definition_name arg_name, pty span arg_ty)) - arguments + method variant ~name:_ ~arguments:_ ~is_record:_ ~attrs:_ = + default_document_for "variant" + (* END GENERATED *) + end end -module type S = sig - val pitem : item -> C.AST.decl list +module HaxCFG = struct + module MyPrinter = Make (Features.Full) (struct let default x = x end) + + module AST = Ast.Make (Features.Full) + open AST + + let print_ast (_ : unit) = + let my_printer = new MyPrinter.printer in + + let dummy_ident : concrete_ident = + Concrete_ident.of_name Value Hax_lib__RefineAs__into_checked + in + let dummy_ty : ty = TStr in + let dummy_expr : expr = { e = Literal (String "dummy"); span = Span.dummy (); typ = dummy_ty } in + let dummy_generics : generics = { params = []; constraints = [] } in + let dummy_global_ident : global_ident = + `Concrete (dummy_ident) + in + let dummy_pat = { p = PWild; span = Span.dummy(); typ = dummy_ty } in + let dummy_local_ident : local_ident = { name = "dummy"; id = Local_ident.mk_id Typ 0 } in + + (* print#_do_not_override_lazy_of_item' ~super AstPos_item__v v *) + + let my_items' : item' list = + [ + Fn { + name = dummy_ident; + generics = dummy_generics; + body = dummy_expr; + params = []; + safety = Safe}; + TyAlias { + name = dummy_ident; + generics = dummy_generics; + ty = dummy_ty}; + (* struct *) + Type { + name = dummy_ident; + generics = dummy_generics; + variants = []; + is_struct = false; + } ; + (* enum *) + Type { + name = dummy_ident; + generics = dummy_generics; + variants = []; + is_struct = true; + } ; + ] + (* @ List.map ~f:(fun x -> IMacroInvokation { *) + (* macro = x; *) + (* argument = "TODO"; *) + (* span = Span.dummy(); *) + (* witness : Features.On.macro; (\* TODO: Check feature enabled in target langauge *\) *) + (* }) ["public_nat_mod"; *) + (* "bytes"; *) + (* "public_bytes"; *) + (* "array"; *) + (* "unsigned_public_integer"] *) + @ [ + Trait { + name = dummy_ident; + generics = dummy_generics; + items = []; + safety = Safe; + } ; + Impl { + generics = dummy_generics; + self_ty = dummy_ty; + of_trait = (dummy_global_ident , []); + items = []; + parent_bounds = []; + safety = Safe; + }; + Alias { name = dummy_ident; item = dummy_ident }; + Use { path = []; is_external = false; rename = None; }; + Quote { contents = []; witness = Features.On.quote (* TODO: Check if feature enabled *); }; + HaxError "dummy"; + NotImplementedYet + ] + in + let my_items : item list = List.map ~f:(fun x -> { v = x; span = Span.dummy(); ident = dummy_ident; attrs = [] }) my_items' in + let item_string = + " ::=\n" ^ + String.concat ~sep:"\n" ( + List.map + ~f:(fun item -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_item item); + "| " ^ Buffer.contents buf + ) + my_items) + in + + let my_exprs' = [ + If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; + App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; + Literal (String "dummy"); + Array []; + (* Construct { *) + (* constructor = dummy_global_ident; *) + (* is_record = false; *) + (* is_struct = false; *) + (* fields = []; *) + (* base = None; *) + (* }; *) + (* Match { scrutinee = dummy_expr; arms = [] }; *) + (* Let { monadic = None; lhs = dummy_pat; rhs = dummy_expr; body = dummy_expr; }; *) + (* Block { e = dummy_expr; safety_mode = Safe; witness = Features.On.block _ _ }; *) + (* LocalVar dummy_local_ident; *) + (* GlobalVar dummy_global_ident; *) + (* Ascription { e = dummy_expr; typ = dummy_ty }; *) + (* MacroInvokation { macro = dummy_global_ident; args = "dummy"; witness = Features.On.macro; } *) + (* Assign { lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; e = dummy_expr; witness = _ } *) + (* Loop { body = dummy_expr; kind = UnconditionalLoop; state = None; label = None; witness = Features.On.loop; }; *) + (* Break { e = dummy_expr; label = None; witness = (Features.On.break , Features.On.loop) }; *) + (* Return { e = dummy_expr; witness = Features.On.early_exit }; *) + (* QuestionMark { e = dummy_expr; return_typ = dummy_ty; witness = Features.On.question_mark }; *) + (* Continue { *) + (* e = None; *) + (* label = None; *) + (* witness = (Features.On.continue , Features.On.loop); *) + (* }; *) + (* (\* Mem *\) *) + (* | Borrow of { kind : borrow_kind; e : expr; witness : Features.On.reference } *) + (* (\* Raw borrow *\) *) + (* | AddressOf of { *) + (* mut : Features.On.mutable_pointer mutability; *) + (* e : expr; *) + (* witness : Features.On.raw_pointer; *) + (* } *) + (* | Closure of { params : pat list; body : expr; captures : expr list } *) + (* | EffectAction of { action : Features.On.monadic_action; argument : expr } *) + (* | Quote of quote *) + (* (\** A quotation is an inlined piece of backend code *) + (* interleaved with Rust code *\) *) + ] in + let my_exprs = List.map ~f:(fun x -> { e = x; span = Span.dummy(); typ = dummy_ty }) my_exprs' in + let expr_string = + " ::=\n" ^ + String.concat ~sep:"\n" ( + List.map + ~f:(fun expr -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_expr expr); + "| " ^ Buffer.contents buf + ) + my_exprs) + in + + let my_tys = [ + TBool; + TChar; + TInt ({ size = S8; signedness = Signed }); + (* TFloat of float_kind; *) + TStr; + (* TApp of { ident : global_ident; args : generic_value list }; *) + (* TArray of { typ : ty; length : expr }; *) + (* TSlice of { witness : F.slice; ty : ty }; *) + (* TRawPointer of { witness : F.raw_pointer } (\* todo *\); *) + (* TRef of { *) + (* witness : F.reference; *) + (* region : todo; *) + (* typ : ty; *) + (* mut : F.mutable_reference mutability; *) + (* }; *) + (* TParam of local_ident; *) + (* TArrow of ty list * ty; *) + (* TAssociatedType of { impl : impl_expr; item : concrete_ident }; *) + (* TOpaque of concrete_ident; *) + (* TDyn of { witness : F.dyn; goals : dyn_trait_goal list }; *) + ] in + let ty_string = + " ::=\n" ^ + String.concat ~sep:"\n" ( + List.map + ~f:(fun ty -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); + "| " ^ Buffer.contents buf + ) + my_tys) + in + + let my_pats' = [ + PWild; + (* PAscription of { typ : ty; typ_span : span; pat : pat }; *) + (* PConstruct of { constructor : global_ident; is_record : bool; (\* are fields named? *\) is_struct : bool; (\* a struct has one constructor *\) fields : field_pat list; }; *) + (* POr of { subpats : pat list }; *) + (* PArray of { args : pat list }; *) + (* PDeref of { subpat : pat; witness : F.reference }; *) + (* PConstant of { lit : literal }; *) + (* PBinding of { mut : F.mutable_variable mutability; mode : binding_mode; var : local_ident; typ : ty; subpat : (pat * F.as_pattern) option; }; *) + ] in + let my_pats = List.map ~f:(fun x -> { p = x; span = Span.dummy(); typ = dummy_ty }) my_pats' in + let pat_string = + " ::=\n" ^ + String.concat ~sep:"\n" ( + List.map + ~f:(fun pat -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); + "| " ^ Buffer.contents buf + ) + my_pats) + in + + [Types. + { + path = "ast_spec.txt"; + contents = + "Hax CFG" + ^ "\n" + ^ "=======" + ^ "\n" + ^ expr_string + ^ "\n\n" + ^ ty_string + ^ "\n\n" + ^ pat_string + ^ "\n\n" + ^ item_string; + sourcemap = None; + }] end -let make ctx = - (module Make (struct - let ctx = ctx - end) : S) - -let string_of_item (item : item) : string = - let (module Print) = - make { current_namespace = U.Concrete_ident_view.to_namespace item.ident } - in - List.map ~f:C.decl_to_string @@ Print.pitem item |> String.concat ~sep:"\n" - -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" - -let hardcoded_coq_headers = - "(* File automatically generated by Hacspec *)\n\ - From Hacspec Require Import Hacspec_Lib MachineIntegers.\n\ - From Coq Require Import ZArith.\n\ - Import List.ListNotations.\n\ - Open Scope Z_scope.\n\ - Open Scope bool_scope.\n" - -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:"_" - (List.map - ~f:(map_first_letter String.uppercase) - (fst ns :: snd ns)) - in - - Types. - { - path = mod_name ^ ".v"; - contents = - hardcoded_coq_headers ^ "\n" ^ string_of_items items ^ "\n"; - sourcemap = None; - }) +let translate _ (_bo) _ = HaxCFG.print_ast () open Phase_utils From ef38bed99d38192ac1a4e2195977c294dc9702ee Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Wed, 9 Oct 2024 18:25:27 +0200 Subject: [PATCH 2/6] Documentation WIP --- engine/backends/coq/coq/coq_backend.ml | 161 +++++++++++++------------ 1 file changed, 83 insertions(+), 78 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index a455fc320..3f0b61317 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -125,7 +125,7 @@ struct method error_expr _x1 = default_document_for "error_expr" method error_item _x1 = default_document_for "error_item" method error_pat _x1 = default_document_for "error_pat" - method expr ~e:_ ~span:_ ~typ:_ = default_document_for "expr" + method expr ~e ~span:_ ~typ:_ = e#p method expr'_AddressOf ~super:_ ~mut:_ ~e:_ ~witness:_ = default_document_for "expr'_AddressOf" @@ -177,7 +177,7 @@ struct default_document_for "expr'_GlobalVar" method expr'_If ~super:_ ~cond:_ ~then_:_ ~else_:_ = - default_document_for "expr'_If" + string "if" ^^ space ^^ string "" ^^ braces ( string "" ) ^^ space ^^ option_of (string "else" ^^ braces (string "")) method expr'_Let ~super:_ ~monadic:_ ~lhs:_ ~rhs:_ ~body:_ = default_document_for "expr'_Let" @@ -362,7 +362,7 @@ struct method param ~pat:_ ~typ:_ ~typ_span:_ ~attrs:_ = default_document_for "param" - method pat ~p:_ ~span:_ ~typ:_ = default_document_for "pat" + method pat ~p ~span:_ ~typ:_ = p#p method pat'_PAscription ~super:_ ~typ:_ ~typ_span:_ ~pat:_ = default_document_for "pat'_PAscription" @@ -423,8 +423,8 @@ struct method ty_TAssociatedType ~impl:_ ~item:_ = default_document_for "ty_TAssociatedType" - method ty_TBool = default_document_for "ty_TBool" - method ty_TChar = default_document_for "ty_TChar" + method ty_TBool = string "bool" + method ty_TChar = string "char" method ty_TDyn ~witness:_ ~goals:_ = default_document_for "ty_TDyn" method ty_TFloat _x1 = default_document_for "ty_TFloat" method ty_TInt _x1 = default_document_for "ty_TInt" @@ -436,7 +436,7 @@ struct default_document_for "ty_TRef" method ty_TSlice ~witness:_ ~ty:_ = default_document_for "ty_TSlice" - method ty_TStr = default_document_for "ty_TStr" + method ty_TStr = string "str" method variant ~name:_ ~arguments:_ ~is_record:_ ~attrs:_ = default_document_for "variant" @@ -444,6 +444,8 @@ struct end end +(* TODO: Write quoted expression shallowly, to get a generator for full AST *) + module HaxCFG = struct module MyPrinter = Make (Features.Full) (struct let default x = x end) @@ -456,8 +458,10 @@ module HaxCFG = struct let dummy_ident : concrete_ident = Concrete_ident.of_name Value Hax_lib__RefineAs__into_checked in - let dummy_ty : ty = TStr in - let dummy_expr : expr = { e = Literal (String "dummy"); span = Span.dummy (); typ = dummy_ty } in + + let dummy_literal = String "dummy" in + + let dummy_expr : expr = { e = Literal (dummy_literal); span = Span.dummy (); typ = dummy_ty } in let dummy_generics : generics = { params = []; constraints = [] } in let dummy_global_ident : global_ident = `Concrete (dummy_ident) @@ -494,16 +498,16 @@ module HaxCFG = struct is_struct = true; } ; ] - (* @ List.map ~f:(fun x -> IMacroInvokation { *) - (* macro = x; *) - (* argument = "TODO"; *) - (* span = Span.dummy(); *) - (* witness : Features.On.macro; (\* TODO: Check feature enabled in target langauge *\) *) - (* }) ["public_nat_mod"; *) - (* "bytes"; *) - (* "public_bytes"; *) - (* "array"; *) - (* "unsigned_public_integer"] *) + @ List.map ~f:(fun x -> IMacroInvokation { + macro = Concrete_ident.of_name Macro Alloc__string__String ; (* TODO *) + argument = "TODO"; + span = Span.dummy(); + witness = Features.On.macro; + }) ["public_nat_mod"; + "bytes"; + "public_bytes"; + "array"; + "unsigned_public_integer"] @ [ Trait { name = dummy_ident; @@ -521,7 +525,7 @@ module HaxCFG = struct }; Alias { name = dummy_ident; item = dummy_ident }; Use { path = []; is_external = false; rename = None; }; - Quote { contents = []; witness = Features.On.quote (* TODO: Check if feature enabled *); }; + Quote { contents = []; witness = Features.On.quote; }; HaxError "dummy"; NotImplementedYet ] @@ -541,46 +545,35 @@ module HaxCFG = struct let my_exprs' = [ If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; - App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; + (* App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; *) Literal (String "dummy"); Array []; - (* Construct { *) - (* constructor = dummy_global_ident; *) - (* is_record = false; *) - (* is_struct = false; *) - (* fields = []; *) - (* base = None; *) - (* }; *) - (* Match { scrutinee = dummy_expr; arms = [] }; *) - (* Let { monadic = None; lhs = dummy_pat; rhs = dummy_expr; body = dummy_expr; }; *) - (* Block { e = dummy_expr; safety_mode = Safe; witness = Features.On.block _ _ }; *) - (* LocalVar dummy_local_ident; *) - (* GlobalVar dummy_global_ident; *) - (* Ascription { e = dummy_expr; typ = dummy_ty }; *) - (* MacroInvokation { macro = dummy_global_ident; args = "dummy"; witness = Features.On.macro; } *) - (* Assign { lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; e = dummy_expr; witness = _ } *) - (* Loop { body = dummy_expr; kind = UnconditionalLoop; state = None; label = None; witness = Features.On.loop; }; *) - (* Break { e = dummy_expr; label = None; witness = (Features.On.break , Features.On.loop) }; *) - (* Return { e = dummy_expr; witness = Features.On.early_exit }; *) - (* QuestionMark { e = dummy_expr; return_typ = dummy_ty; witness = Features.On.question_mark }; *) - (* Continue { *) - (* e = None; *) - (* label = None; *) - (* witness = (Features.On.continue , Features.On.loop); *) - (* }; *) - (* (\* Mem *\) *) - (* | Borrow of { kind : borrow_kind; e : expr; witness : Features.On.reference } *) - (* (\* Raw borrow *\) *) - (* | AddressOf of { *) - (* mut : Features.On.mutable_pointer mutability; *) - (* e : expr; *) - (* witness : Features.On.raw_pointer; *) - (* } *) - (* | Closure of { params : pat list; body : expr; captures : expr list } *) - (* | EffectAction of { action : Features.On.monadic_action; argument : expr } *) - (* | Quote of quote *) - (* (\** A quotation is an inlined piece of backend code *) - (* interleaved with Rust code *\) *) + Construct { + constructor = dummy_global_ident; + is_record = false; + is_struct = false; + fields = []; + base = None; + }; + Match { scrutinee = dummy_expr; arms = [] }; + Let { monadic = None; lhs = dummy_pat; rhs = dummy_expr; body = dummy_expr; }; + Block { e = dummy_expr; safety_mode = Safe; witness = Features.On.block }; + LocalVar dummy_local_ident; + GlobalVar dummy_global_ident; + Ascription { e = dummy_expr; typ = dummy_ty }; + MacroInvokation { macro = dummy_global_ident; args = "dummy"; witness = Features.On.macro; }; + Assign { lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; e = dummy_expr; witness = Features.On.mutable_variable; }; + Loop { body = dummy_expr; kind = UnconditionalLoop; state = None; label = None; witness = Features.On.loop; }; + Break { e = dummy_expr; label = None; witness = (Features.On.break , Features.On.loop) }; + Return { e = dummy_expr; witness = Features.On.early_exit }; + QuestionMark { e = dummy_expr; return_typ = dummy_ty; witness = Features.On.question_mark }; + Continue { e = None; label = None; witness = (Features.On.continue , Features.On.loop) }; + Borrow { kind = Shared; e = dummy_expr; witness = Features.On.reference }; + AddressOf { mut = Immutable; e = dummy_expr; witness = Features.On.raw_pointer; }; + AddressOf { mut = (Mutable Features.On.mutable_pointer) ; e = dummy_expr; witness = Features.On.raw_pointer; }; + Closure { params = []; body = dummy_expr; captures = [] }; + EffectAction { action = Features.On.monadic_action; argument = dummy_expr }; + Quote { contents = []; witness = Features.On.quote; } ] in let my_exprs = List.map ~f:(fun x -> { e = x; span = Span.dummy(); typ = dummy_ty }) my_exprs' in let expr_string = @@ -602,20 +595,26 @@ module HaxCFG = struct (* TFloat of float_kind; *) TStr; (* TApp of { ident : global_ident; args : generic_value list }; *) - (* TArray of { typ : ty; length : expr }; *) - (* TSlice of { witness : F.slice; ty : ty }; *) - (* TRawPointer of { witness : F.raw_pointer } (\* todo *\); *) - (* TRef of { *) - (* witness : F.reference; *) - (* region : todo; *) - (* typ : ty; *) - (* mut : F.mutable_reference mutability; *) - (* }; *) - (* TParam of local_ident; *) - (* TArrow of ty list * ty; *) - (* TAssociatedType of { impl : impl_expr; item : concrete_ident }; *) - (* TOpaque of concrete_ident; *) - (* TDyn of { witness : F.dyn; goals : dyn_trait_goal list }; *) + TArray { typ = dummy_ty; length = dummy_expr (* const *) }; + TSlice { witness = Features.On.slice; ty = dummy_ty }; + TRawPointer { witness = Features.On.raw_pointer }; + TRef { + witness = Features.On.reference; + region = "todo"; + typ = dummy_ty; + mut = Immutable; + }; + TRef { + witness = Features.On.reference; + region = "todo"; + typ = dummy_ty; + mut = Mutable (Features.On.mutable_reference); + }; + TParam dummy_local_ident; + TArrow ([] , dummy_ty); + (* TAssociatedType { impl = impl_expr; item : concrete_ident }; *) + TOpaque (dummy_ident); + TDyn { witness = Features.On.dyn; goals = [] }; ] in let ty_string = " ::=\n" ^ @@ -631,13 +630,19 @@ module HaxCFG = struct let my_pats' = [ PWild; - (* PAscription of { typ : ty; typ_span : span; pat : pat }; *) - (* PConstruct of { constructor : global_ident; is_record : bool; (\* are fields named? *\) is_struct : bool; (\* a struct has one constructor *\) fields : field_pat list; }; *) - (* POr of { subpats : pat list }; *) - (* PArray of { args : pat list }; *) - (* PDeref of { subpat : pat; witness : F.reference }; *) - (* PConstant of { lit : literal }; *) - (* PBinding of { mut : F.mutable_variable mutability; mode : binding_mode; var : local_ident; typ : ty; subpat : (pat * F.as_pattern) option; }; *) + PAscription { typ = dummy_ty; typ_span = Span.dummy(); pat = dummy_pat }; + PConstruct { constructor = dummy_global_ident; is_record = false; is_struct = false; fields = []; }; + POr { subpats = [] }; + PArray { args = [] }; + PDeref { subpat = dummy_pat; witness = Features.On.reference }; + PConstant { lit = dummy_literal }; + PBinding { + mut = Mutable Features.On.mutable_variable; + mode = ByValue; + var = dummy_local_ident; + typ = dummy_ty; + subpat = None; + }; ] in let my_pats = List.map ~f:(fun x -> { p = x; span = Span.dummy(); typ = dummy_ty }) my_pats' in let pat_string = From f7240e74ae85851c90fe482f7941e7df82a2ecb5 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Sat, 12 Oct 2024 01:49:31 +0200 Subject: [PATCH 3/6] Print more of ast --- ast_spec.md | 83 +++ engine/backends/coq/coq/coq_backend.ml | 755 ++++++++++++++++--------- hax-lib-macros/src/lib.rs | 21 + hax-lib/src/proc_macros.rs | 2 +- 4 files changed, 606 insertions(+), 255 deletions(-) create mode 100644 ast_spec.md diff --git a/ast_spec.md b/ast_spec.md new file mode 100644 index 000000000..31ad93321 --- /dev/null +++ b/ast_spec.md @@ -0,0 +1,83 @@ +# Hax CFG + +```ebnf +literal ::= +| """ string """ +| "'" char "'" +| int +| float +| ("true" | "false") +``` + +```ebnf +expr ::= +| "if" expr "{" expr "}" ("else" "{" expr "}")? +| literal +| ("[" (expr ",")* "]" | "[" expr ";" int "]") +| constructor (expr)* +| "match" expr "{" (("|" pat)* "=>" (expr "," | "{" "}"))* "}" +| "let" pat (":" ty)? ":=" expr ";" +| (%features: block) modifiers "{" expr "}" +| local_var +| global_var +| expr ":" ty +| macro_name "!" "(" macro_args ")" +| mut var "=" expr +| (%features: loop) TODO: please implement the method `expr'_Loop` +| (%features: break , loop) "break" +| (%features: early_exit) "return" expr +| (%features: question_mark) expr "?" +| (%features: continue , loop) "continue" +| (%features: reference) "&" expr +| "*" expr +| (%features: mutable_pointer) "*mut" expr +| "|" param "|" expr +| (%features: monadic_action) TODO: please implement the method `expr'_EffectAction` +| TODO: please implement the method `expr'_Quote` +``` + +```ebnf +ty ::= +| "bool" +| "char" +| ("u8" | "u16" | "u32" | "u64" | "u128" | "usize") +| ("f16" | "f32" | "f64") +| "str" +| "[" ty ";" int "]" +| (%features: slice) "[" ty "]" +| ((%features: raw_pointer) "*const" ty | (%features: raw_pointer) "*mut" ty) +| (%features: reference) * expr +| (%features: reference , mutable_reference) *mut expr +| TODO: please implement the method `ty_TParam` +| (ty "->")* ty +| TODO: please implement the method `ty_TOpaque` +| TODO: please implement the method `ty_TDyn` +``` + +```ebnf +pat ::= +| "_" +| pat ":" +| constructor pat +| ("pat" "|")* "pat" +| ("[" (expr ",")* "]" | "[" expr ";" int "]") +| TODO: please implement the method `pat'_PDeref` +| literal +| TODO: please implement the method `pat'_PBinding` +``` + +```ebnf +item ::= +| modifiers "fn" ident "(" (pat ":"ty ",")* ")" (":"ty)? "{" expr "}" +| "type" ident "=" ty +| "enum" ident "=" "{" (ident ("(" (ty)* ")")? ",")* "}" +| "struct" ident "=" "{" (ident ":" ty ",")* "}" +| (%features: macro) (public_nat_mod | bytes | public_bytes | array | unsigned_public_integer) +| "trait" ident "{" (trait_item)* "}" +| "impl" ("<" (generics ",")* ">")? ident "for" ty "{" (impl_item)* "}" +| TODO: please implement the method `item'_Alias` +| "use" path ";" +| (%features: quote) TODO: please implement the method `item'_Quote` +| TODO: please implement the method `item'_HaxError` +| TODO: please implement the method `item'_NotImplementedYet` +``` diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 3f0b61317..ec4e08e43 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -79,11 +79,11 @@ module CoqLibrary : Library = struct end module C = Coq (CoqLibrary) - open Ast module Make - (F : Features.T) (Default : sig + (F : Features.T) + (Default : sig val default : string -> string end) = struct @@ -94,9 +94,37 @@ struct let default_string_for s = "TODO: please implement the method `" ^ s ^ "`" let default_document_for = default_string_for >> string - - let any_number_of x = brackets ( x ) ^^ string "*" - let option_of x = brackets ( x ) ^^ string "?" + let any_number_of x = parens x ^^ string "*" + let option_of x = parens x ^^ string "?" + let either_of x = parens (separate (space ^^ string "|" ^^ space) x) + let symbol_of x = string "\"" ^^ x ^^ string "\"" + let symbol_str x = string "\"" ^^ string x ^^ string "\"" + let symbol_colon = symbol_of colon + let symbol_semi = symbol_of semi + let symbol_comma = symbol_of comma + + let symbol_parens x = + string "\"" + ^^ parens (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let symbol_brackets x = + string "\"" + ^^ brackets (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let symbol_braces x = + string "\"" + ^^ braces (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let features l = + parens + (string "%features:" ^^ space + ^^ separate_map (space ^^ comma ^^ space) (fun x -> string x) l) + ^^ space + + (* let code_parens x = string "1;31m" ^ parens ( x ^^ string "\x1b[1;31m" ) ^^ string "\x1b[0m" *) class printer = object @@ -117,7 +145,15 @@ struct method borrow_kind_Mut _x1 = default_document_for "borrow_kind_Mut" method borrow_kind_Shared = default_document_for "borrow_kind_Shared" method borrow_kind_Unique = default_document_for "borrow_kind_Unique" - method common_array _x1 = default_document_for "common_array" + + method common_array x1 = + either_of + [ + symbol_brackets + (any_number_of (string "expr" ^^ space ^^ symbol_comma)); + symbol_brackets + (string "expr" ^^ space ^^ symbol_str ";" ^^ space ^^ string "int"); + ] method dyn_trait_goal ~trait:_ ~non_self_args:_ = default_document_for "dyn_trait_goal" @@ -127,8 +163,12 @@ struct method error_pat _x1 = default_document_for "error_pat" method expr ~e ~span:_ ~typ:_ = e#p - method expr'_AddressOf ~super:_ ~mut:_ ~e:_ ~witness:_ = - default_document_for "expr'_AddressOf" + method expr'_AddressOf ~super:_ ~mut ~e:_ ~witness:_ = + match mut with + | Immutable -> symbol_str "*" ^^ space ^^ string "expr" + | Mutable _ -> + features [ "mutable_pointer" ] + ^^ symbol_str "*mut" ^^ space ^^ string "expr" method expr'_App_application ~super:_ ~f:_ ~args:_ ~generics:_ = default_document_for "expr'_App_application" @@ -143,64 +183,85 @@ struct default_document_for "expr'_App_tuple_projection" method expr'_Ascription ~super:_ ~e:_ ~typ:_ = - default_document_for "expr'_Ascription" + string "expr" ^^ space ^^ symbol_colon ^^ space ^^ string "ty" method expr'_Assign ~super:_ ~lhs:_ ~e:_ ~witness:_ = - default_document_for "expr'_Assign" + string "mut var" ^^ space ^^ symbol_str "=" ^^ space ^^ string "expr" method expr'_Block ~super:_ ~e:_ ~safety_mode:_ ~witness:_ = - default_document_for "expr'_Block" + features [ "block" ] ^^ string "modifiers" ^^ space + ^^ symbol_braces (string "expr") method expr'_Borrow ~super:_ ~kind:_ ~e:_ ~witness:_ = - default_document_for "expr'_Borrow" + features [ "reference" ] ^^ symbol_str "&" ^^ space ^^ string "expr" method expr'_Break ~super:_ ~e:_ ~label:_ ~witness:_ = - default_document_for "expr'_Break" + features [ "break"; "loop" ] ^^ symbol_str "break" method expr'_Closure ~super:_ ~params:_ ~body:_ ~captures:_ = - default_document_for "expr'_Closure" + symbol_str "|" ^^ space ^^ string "param" ^^ space ^^ symbol_str "|" + ^^ space ^^ string "expr" method expr'_Construct_inductive ~super:_ ~constructor:_ ~is_record:_ ~is_struct:_ ~fields:_ ~base:_ = - default_document_for "expr'_Construct_inductive" + string "constructor" ^^ space ^^ any_number_of (string "expr") method expr'_Construct_tuple ~super:_ ~components:_ = default_document_for "expr'_Construct_tuple" method expr'_Continue ~super:_ ~e:_ ~label:_ ~witness:_ = - default_document_for "expr'_Continue" + features [ "continue"; "loop" ] ^^ symbol_str "continue" method expr'_EffectAction ~super:_ ~action:_ ~argument:_ = - default_document_for "expr'_EffectAction" + features [ "monadic_action" ] + ^^ default_document_for "expr'_EffectAction" - method expr'_GlobalVar ~super:_ _x2 = - default_document_for "expr'_GlobalVar" + method expr'_GlobalVar ~super:_ _x2 = string "global_var" method expr'_If ~super:_ ~cond:_ ~then_:_ ~else_:_ = - string "if" ^^ space ^^ string "" ^^ braces ( string "" ) ^^ space ^^ option_of (string "else" ^^ braces (string "")) + symbol_str "if" ^^ space ^^ string "expr" ^^ space + ^^ symbol_braces (string "expr") + ^^ space + ^^ option_of + (symbol_str "else" ^^ space ^^ symbol_braces (string "expr")) method expr'_Let ~super:_ ~monadic:_ ~lhs:_ ~rhs:_ ~body:_ = - default_document_for "expr'_Let" + symbol_str "let" ^^ space ^^ string "pat" ^^ space + ^^ option_of (symbol_colon ^^ space ^^ string "ty") + ^^ space ^^ symbol_str ":=" ^^ space ^^ string "expr" ^^ space + ^^ symbol_semi - method expr'_Literal ~super:_ _x2 = default_document_for "expr'_Literal" - method expr'_LocalVar ~super:_ _x2 = default_document_for "expr'_LocalVar" + method expr'_Literal ~super:_ _x2 = string "literal" + method expr'_LocalVar ~super:_ _x2 = string "local_var" method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~label:_ ~witness:_ = - default_document_for "expr'_Loop" + (* Type of loop *) + features [ "loop" ] ^^ default_document_for "expr'_Loop" method expr'_MacroInvokation ~super:_ ~macro:_ ~args:_ ~witness:_ = - default_document_for "expr'_MacroInvokation" + string "macro_name" ^^ space ^^ symbol_str "!" ^^ space + ^^ symbol_parens (string "macro_args") method expr'_Match ~super:_ ~scrutinee:_ ~arms:_ = - default_document_for "expr'_Match" + symbol_str "match" ^^ space ^^ string "expr" ^^ space + ^^ symbol_braces + (any_number_of + (any_number_of (symbol_str "|" ^^ space ^^ string "pat") + ^^ space ^^ symbol_str "=>" ^^ space + ^^ either_of + [ + string "expr" ^^ space ^^ symbol_comma; + symbol_braces (string ""); + ])) method expr'_QuestionMark ~super:_ ~e:_ ~return_typ:_ ~witness:_ = - default_document_for "expr'_QuestionMark" + features [ "question_mark" ] ^^ string "expr" ^^ space ^^ symbol_str "?" method expr'_Quote ~super:_ _x2 = default_document_for "expr'_Quote" method expr'_Return ~super:_ ~e:_ ~witness:_ = - default_document_for "expr'_Return" + features [ "early_exit" ] ^^ symbol_str "return" ^^ space + ^^ string "expr" method field_pat ~field:_ ~pat:_ = default_document_for "field_pat" @@ -275,45 +336,84 @@ struct method impl_item'_IIType ~typ:_ ~parent_bounds:_ = default_document_for "impl_item'_IIType" - method item ~v ~span:_ ~ident:_ ~attrs:_ = v#p (* default_document_for "item" *) + method item ~v ~span:_ ~ident:_ ~attrs:_ = + v#p (* default_document_for "item" *) method item'_Alias ~super:_ ~name:_ ~item:_ = default_document_for "item'_Alias" method item'_Fn ~super:_ ~name:_ ~generics:_ ~body:_ ~params:_ ~safety:_ = - (* TODOD: pub, const, pub(crate) *) - string "" ^^ space ^^ string "fn" ^^ space ^^ string "" ^^ parens ( any_number_of (string "" ^^ space ^^ colon ^^ string "") ) ^^ braces ( string "" ) - + (* TODOD: safe, pub, const, pub(crate) *) + string "modifiers" ^^ space ^^ symbol_str "fn" ^^ space + ^^ string "ident" ^^ space + ^^ symbol_parens + (any_number_of + (string "pat" ^^ space ^^ symbol_colon ^^ string "ty" ^^ space + ^^ symbol_comma)) + ^^ space + ^^ option_of (symbol_colon ^^ string "ty") + ^^ space + ^^ symbol_braces (string "expr") method item'_HaxError ~super:_ _x2 = default_document_for "item'_HaxError" method item'_IMacroInvokation ~super:_ ~macro:_ ~argument:_ ~span:_ ~witness:_ = - default_document_for "item'_IMacroInvokation" + features [ "macro" ] + ^^ either_of + [ + string "public_nat_mod"; + string "bytes"; + string "public_bytes"; + string "array"; + string "unsigned_public_integer"; + ] method item'_Impl ~super:_ ~generics:_ ~self_ty:_ ~of_trait:_ ~items:_ ~parent_bounds:_ ~safety:_ = - default_document_for "item'_Impl" + symbol_str "impl" ^^ space + ^^ option_of + (symbol_str "<" ^^ space + ^^ any_number_of (string "generics" ^^ space ^^ symbol_comma) + ^^ space ^^ symbol_str ">") + ^^ space ^^ string "ident" ^^ space ^^ symbol_str "for" ^^ space + ^^ string "ty" ^^ space + ^^ symbol_braces (any_number_of (string "impl_item")) method item'_NotImplementedYet = default_document_for "item'_NotImplementedYet" - method item'_Quote ~super:_ _x2 = default_document_for "item'_Quote" + method item'_Quote ~super:_ _x2 = + features [ "quote" ] ^^ default_document_for "item'_Quote" method item'_Trait ~super:_ ~name:_ ~generics:_ ~items:_ ~safety:_ = - string "trait" ^^ space ^^ string "" ^^ braces ( any_number_of (string "") ) + symbol_str "trait" ^^ space ^^ string "ident" ^^ space + ^^ symbol_braces (any_number_of (string "trait_item")) method item'_TyAlias ~super:_ ~name:_ ~generics:_ ~ty:_ = - string "type" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ string "" + symbol_str "type" ^^ space ^^ string "ident" ^^ space ^^ symbol_str "=" + ^^ space ^^ string "ty" method item'_Type ~super:_ ~name:_ ~generics:_ ~variants:_ ~is_struct = (* TODO globality *) - if is_struct - then string "struct" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ braces ( any_number_of ( string "" ^^ colon ^^ space ^^ string "" ^^ comma ) ) - else string "enum" ^^ space ^^ string "" ^^ space ^^ string "=" ^^ space ^^ braces ( any_number_of (string "" ^^ option_of (parens (any_number_of (string ""))) ^^ comma ) ) + if is_struct then + symbol_str "struct" ^^ space ^^ string "ident" ^^ space + ^^ symbol_str "=" ^^ space + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space ^^ symbol_colon ^^ space + ^^ string "ty" ^^ space ^^ symbol_comma)) + else + symbol_str "enum" ^^ space ^^ string "ident" ^^ space + ^^ symbol_str "=" ^^ space + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space + ^^ option_of (symbol_parens (any_number_of (string "ty"))) + ^^ space ^^ symbol_comma)) method item'_Use ~super:_ ~path:_ ~is_external:_ ~rename:_ = - default_document_for "item'_Use" + symbol_str "use" ^^ space ^^ string "path" ^^ space ^^ symbol_semi method lhs_LhsArbitraryExpr ~e:_ ~witness:_ = default_document_for "lhs_LhsArbitraryExpr" @@ -330,16 +430,17 @@ struct method lhs_LhsLocalVar ~var:_ ~typ:_ = default_document_for "lhs_LhsLocalVar" - method literal_Bool _x1 = default_document_for "literal_Bool" - method literal_Char _x1 = default_document_for "literal_Char" + method literal_Bool _x1 = + either_of [ symbol_str "true"; symbol_str "false" ] - method literal_Float ~value:_ ~negative:_ ~kind:_ = - default_document_for "literal_Float" + method literal_Char _x1 = + symbol_str "'" ^^ space ^^ string "char" ^^ space ^^ symbol_str "'" - method literal_Int ~value:_ ~negative:_ ~kind:_ = - default_document_for "literal_Int" + method literal_Float ~value:_ ~negative:_ ~kind:_ = string "float" + method literal_Int ~value:_ ~negative:_ ~kind:_ = string "int" - method literal_String _x1 = default_document_for "literal_String" + method literal_String _x1 = + symbol_str "\"" ^^ space ^^ string "string" ^^ space ^^ symbol_str "\"" method loop_kind_ForIndexLoop ~start:_ ~end_:_ ~var:_ ~var_typ:_ ~witness:_ = @@ -365,17 +466,16 @@ struct method pat ~p ~span:_ ~typ:_ = p#p method pat'_PAscription ~super:_ ~typ:_ ~typ_span:_ ~pat:_ = - default_document_for "pat'_PAscription" + string "pat" ^^ space ^^ symbol_colon method pat'_PBinding ~super:_ ~mut:_ ~mode:_ ~var:_ ~typ:_ ~subpat:_ = default_document_for "pat'_PBinding" - method pat'_PConstant ~super:_ ~lit:_ = - default_document_for "pat'_PConstant" + method pat'_PConstant ~super:_ ~lit:_ = string "literal" method pat'_PConstruct_inductive ~super:_ ~constructor:_ ~is_record:_ ~is_struct:_ ~fields:_ = - default_document_for "pat'_PConstruct_inductive" + string "constructor" ^^ space ^^ string "pat" method pat'_PConstruct_tuple ~super:_ ~components:_ = default_document_for "pat'_PConstruct_tuple" @@ -383,7 +483,12 @@ struct method pat'_PDeref ~super:_ ~subpat:_ ~witness:_ = default_document_for "pat'_PDeref" - method pat'_PWild = default_document_for "pat'_PWild" + method pat'_PWild = symbol_str "_" + + method pat'_POr ~super:_ ~subpats:_ = + any_number_of (symbol_str "pat" ^^ space ^^ symbol_str "|") + ^^ space ^^ symbol_str "pat" + method printer_name = default_string_for "printer_name" method projection_predicate ~impl:_ ~assoc_item:_ ~typ:_ = @@ -417,26 +522,60 @@ struct default_document_for "ty_TApp_application" method ty_TApp_tuple ~types:_ = default_document_for "ty_TApp_tuple" - method ty_TArray ~typ:_ ~length:_ = default_document_for "ty_TArray" - method ty_TArrow _x1 _x2 = default_document_for "ty_TArrow" + + method ty_TArray ~typ:_ ~length:_ = + symbol_brackets + (string "ty" ^^ space ^^ symbol_semi ^^ space ^^ string "int") + + method ty_TArrow _x1 _x2 = + any_number_of (string "ty" ^^ space ^^ symbol_str "->") + ^^ space ^^ string "ty" method ty_TAssociatedType ~impl:_ ~item:_ = default_document_for "ty_TAssociatedType" - method ty_TBool = string "bool" - method ty_TChar = string "char" + method ty_TBool = symbol_str "bool" + method ty_TChar = symbol_str "char" method ty_TDyn ~witness:_ ~goals:_ = default_document_for "ty_TDyn" - method ty_TFloat _x1 = default_document_for "ty_TFloat" - method ty_TInt _x1 = default_document_for "ty_TInt" + + method ty_TFloat _x1 = + either_of [ symbol_str "f16"; symbol_str "f32"; symbol_str "f64" ] + + method ty_TInt _x1 = + either_of + [ + symbol_str "u8"; + symbol_str "u16"; + symbol_str "u32"; + symbol_str "u64"; + symbol_str "u128"; + symbol_str "usize"; + ] + method ty_TOpaque _x1 = default_document_for "ty_TOpaque" method ty_TParam _x1 = default_document_for "ty_TParam" - method ty_TRawPointer ~witness:_ = default_document_for "ty_TRawPointer" - method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut:_ = - default_document_for "ty_TRef" + method ty_TRawPointer ~witness:_ = + either_of + [ + features [ "raw_pointer" ] ^^ symbol_str "*const" ^^ space + ^^ string "ty"; + features [ "raw_pointer" ] ^^ symbol_str "*mut" ^^ space + ^^ string "ty"; + ] + + method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut = + match mut with + | Immutable -> + features [ "reference" ] ^^ string "*" ^^ space ^^ string "expr" + | Mutable _ -> + features [ "reference"; "mutable_reference" ] + ^^ string "*mut" ^^ space ^^ string "expr" + + method ty_TSlice ~witness:_ ~ty:_ = + features [ "slice" ] ^^ symbol_brackets (string "ty") - method ty_TSlice ~witness:_ ~ty:_ = default_document_for "ty_TSlice" - method ty_TStr = string "str" + method ty_TStr = symbol_str "str" method variant ~name:_ ~arguments:_ ~is_record:_ ~attrs:_ = default_document_for "variant" @@ -445,9 +584,16 @@ struct end (* TODO: Write quoted expression shallowly, to get a generator for full AST *) +(* ppx_deriving_random, metaquote *) +(* [%expr 1 + [%e some_expr_node]] *) module HaxCFG = struct - module MyPrinter = Make (Features.Full) (struct let default x = x end) + module MyPrinter = + Make + (Features.Full) + (struct + let default x = x + end) module AST = Ast.Make (Features.Full) open AST @@ -461,222 +607,323 @@ module HaxCFG = struct let dummy_literal = String "dummy" in - let dummy_expr : expr = { e = Literal (dummy_literal); span = Span.dummy (); typ = dummy_ty } in + let dummy_ty = TBool in + + let dummy_expr : expr = + { e = Literal dummy_literal; span = Span.dummy (); typ = dummy_ty } + in let dummy_generics : generics = { params = []; constraints = [] } in - let dummy_global_ident : global_ident = - `Concrete (dummy_ident) + let dummy_global_ident : global_ident = `Concrete dummy_ident in + let dummy_pat = { p = PWild; span = Span.dummy (); typ = dummy_ty } in + let dummy_local_ident : local_ident = + { name = "dummy"; id = Local_ident.mk_id Typ 0 } in - let dummy_pat = { p = PWild; span = Span.dummy(); typ = dummy_ty } in - let dummy_local_ident : local_ident = { name = "dummy"; id = Local_ident.mk_id Typ 0 } in (* print#_do_not_override_lazy_of_item' ~super AstPos_item__v v *) + let my_literals = + [ + String "dummy"; + Char 'a'; + Int + { + value = "dummy"; + kind = { size = S8; signedness = Unsigned }; + negative = false; + }; + Float { value = "dummy"; kind = F16; negative = false }; + Bool false; + ] + in + let literal_string = + "\n\n```ebnf\nliteral ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun literal -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_literal literal); + "| " ^ Buffer.contents buf) + my_literals) + ^ "\n```" + in let my_items' : item' list = [ - Fn { - name = dummy_ident; - generics = dummy_generics; - body = dummy_expr; - params = []; - safety = Safe}; - TyAlias { - name = dummy_ident; - generics = dummy_generics; - ty = dummy_ty}; + Fn + { + name = dummy_ident; + generics = dummy_generics; + body = dummy_expr; + params = []; + safety = Safe; + }; + TyAlias { name = dummy_ident; generics = dummy_generics; ty = dummy_ty }; (* struct *) - Type { - name = dummy_ident; - generics = dummy_generics; - variants = []; - is_struct = false; - } ; + Type + { + name = dummy_ident; + generics = dummy_generics; + variants = []; + is_struct = false; + }; (* enum *) - Type { - name = dummy_ident; - generics = dummy_generics; - variants = []; - is_struct = true; - } ; - ] - @ List.map ~f:(fun x -> IMacroInvokation { - macro = Concrete_ident.of_name Macro Alloc__string__String ; (* TODO *) - argument = "TODO"; - span = Span.dummy(); - witness = Features.On.macro; - }) ["public_nat_mod"; - "bytes"; - "public_bytes"; - "array"; - "unsigned_public_integer"] - @ [ - Trait { - name = dummy_ident; - generics = dummy_generics; - items = []; - safety = Safe; - } ; - Impl { - generics = dummy_generics; - self_ty = dummy_ty; - of_trait = (dummy_global_ident , []); - items = []; - parent_bounds = []; - safety = Safe; - }; + Type + { + name = dummy_ident; + generics = dummy_generics; + variants = []; + is_struct = true; + }; + IMacroInvokation + { + macro = dummy_ident; + argument = "TODO"; + span = Span.dummy (); + witness = Features.On.macro; + }; + Trait + { + name = dummy_ident; + generics = dummy_generics; + items = []; + safety = Safe; + }; + Impl + { + generics = dummy_generics; + self_ty = dummy_ty; + of_trait = (dummy_global_ident, []); + items = []; + parent_bounds = []; + safety = Safe; + }; Alias { name = dummy_ident; item = dummy_ident }; - Use { path = []; is_external = false; rename = None; }; - Quote { contents = []; witness = Features.On.quote; }; + Use { path = []; is_external = false; rename = None }; + Quote { contents = []; witness = Features.On.quote }; HaxError "dummy"; - NotImplementedYet + NotImplementedYet; ] in - let my_items : item list = List.map ~f:(fun x -> { v = x; span = Span.dummy(); ident = dummy_ident; attrs = [] }) my_items' in + let my_items : item list = + List.map + ~f:(fun x -> + { v = x; span = Span.dummy (); ident = dummy_ident; attrs = [] }) + my_items' + in let item_string = - " ::=\n" ^ - String.concat ~sep:"\n" ( - List.map - ~f:(fun item -> - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_item item); - "| " ^ Buffer.contents buf - ) - my_items) + "\n\n```ebnf\nitem ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun item -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_item item); + "| " ^ Buffer.contents buf) + my_items) + ^ "\n```" in - let my_exprs' = [ - If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; - (* App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; *) - Literal (String "dummy"); - Array []; - Construct { - constructor = dummy_global_ident; - is_record = false; - is_struct = false; - fields = []; - base = None; - }; - Match { scrutinee = dummy_expr; arms = [] }; - Let { monadic = None; lhs = dummy_pat; rhs = dummy_expr; body = dummy_expr; }; - Block { e = dummy_expr; safety_mode = Safe; witness = Features.On.block }; - LocalVar dummy_local_ident; - GlobalVar dummy_global_ident; - Ascription { e = dummy_expr; typ = dummy_ty }; - MacroInvokation { macro = dummy_global_ident; args = "dummy"; witness = Features.On.macro; }; - Assign { lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; e = dummy_expr; witness = Features.On.mutable_variable; }; - Loop { body = dummy_expr; kind = UnconditionalLoop; state = None; label = None; witness = Features.On.loop; }; - Break { e = dummy_expr; label = None; witness = (Features.On.break , Features.On.loop) }; - Return { e = dummy_expr; witness = Features.On.early_exit }; - QuestionMark { e = dummy_expr; return_typ = dummy_ty; witness = Features.On.question_mark }; - Continue { e = None; label = None; witness = (Features.On.continue , Features.On.loop) }; - Borrow { kind = Shared; e = dummy_expr; witness = Features.On.reference }; - AddressOf { mut = Immutable; e = dummy_expr; witness = Features.On.raw_pointer; }; - AddressOf { mut = (Mutable Features.On.mutable_pointer) ; e = dummy_expr; witness = Features.On.raw_pointer; }; - Closure { params = []; body = dummy_expr; captures = [] }; - EffectAction { action = Features.On.monadic_action; argument = dummy_expr }; - Quote { contents = []; witness = Features.On.quote; } - ] in - let my_exprs = List.map ~f:(fun x -> { e = x; span = Span.dummy(); typ = dummy_ty }) my_exprs' in + let my_exprs' = + [ + If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; + (* App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; *) + Literal (String "dummy"); + Array []; + Construct + { + constructor = dummy_global_ident; + is_record = false; + is_struct = false; + fields = []; + base = None; + }; + Match { scrutinee = dummy_expr; arms = [] }; + Let + { + monadic = None; + lhs = dummy_pat; + rhs = dummy_expr; + body = dummy_expr; + }; + Block + { e = dummy_expr; safety_mode = Safe; witness = Features.On.block }; + LocalVar dummy_local_ident; + GlobalVar dummy_global_ident; + Ascription { e = dummy_expr; typ = dummy_ty }; + MacroInvokation + { + macro = dummy_global_ident; + args = "dummy"; + witness = Features.On.macro; + }; + Assign + { + lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; + e = dummy_expr; + witness = Features.On.mutable_variable; + }; + Loop + { + body = dummy_expr; + kind = UnconditionalLoop; + state = None; + label = None; + witness = Features.On.loop; + }; + Break + { + e = dummy_expr; + label = None; + witness = (Features.On.break, Features.On.loop); + }; + Return { e = dummy_expr; witness = Features.On.early_exit }; + QuestionMark + { + e = dummy_expr; + return_typ = dummy_ty; + witness = Features.On.question_mark; + }; + Continue + { + e = None; + label = None; + witness = (Features.On.continue, Features.On.loop); + }; + Borrow + { kind = Shared; e = dummy_expr; witness = Features.On.reference }; + AddressOf + { mut = Immutable; e = dummy_expr; witness = Features.On.raw_pointer }; + AddressOf + { + mut = Mutable Features.On.mutable_pointer; + e = dummy_expr; + witness = Features.On.raw_pointer; + }; + Closure { params = []; body = dummy_expr; captures = [] }; + EffectAction + { action = Features.On.monadic_action; argument = dummy_expr }; + Quote { contents = []; witness = Features.On.quote }; + ] + in + let my_exprs = + List.map + ~f:(fun x -> { e = x; span = Span.dummy (); typ = dummy_ty }) + my_exprs' + in let expr_string = - " ::=\n" ^ - String.concat ~sep:"\n" ( - List.map - ~f:(fun expr -> - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_expr expr); - "| " ^ Buffer.contents buf - ) - my_exprs) + "\n\n```ebnf\nexpr ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun expr -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_expr expr); + "| " ^ Buffer.contents buf) + my_exprs) + ^ "\n```" in - let my_tys = [ - TBool; - TChar; - TInt ({ size = S8; signedness = Signed }); - (* TFloat of float_kind; *) - TStr; - (* TApp of { ident : global_ident; args : generic_value list }; *) - TArray { typ = dummy_ty; length = dummy_expr (* const *) }; - TSlice { witness = Features.On.slice; ty = dummy_ty }; - TRawPointer { witness = Features.On.raw_pointer }; - TRef { - witness = Features.On.reference; - region = "todo"; - typ = dummy_ty; - mut = Immutable; - }; - TRef { - witness = Features.On.reference; - region = "todo"; - typ = dummy_ty; - mut = Mutable (Features.On.mutable_reference); - }; - TParam dummy_local_ident; - TArrow ([] , dummy_ty); - (* TAssociatedType { impl = impl_expr; item : concrete_ident }; *) - TOpaque (dummy_ident); - TDyn { witness = Features.On.dyn; goals = [] }; - ] in + let my_tys = + [ + TBool; + TChar; + TInt { size = S8; signedness = Signed }; + TFloat F16; + TStr; + (* TApp of { ident : global_ident; args : generic_value list }; *) + TArray { typ = dummy_ty; length = dummy_expr (* const *) }; + TSlice { witness = Features.On.slice; ty = dummy_ty }; + TRawPointer { witness = Features.On.raw_pointer }; + TRef + { + witness = Features.On.reference; + region = "todo"; + typ = dummy_ty; + mut = Immutable; + }; + TRef + { + witness = Features.On.reference; + region = "todo"; + typ = dummy_ty; + mut = Mutable Features.On.mutable_reference; + }; + TParam dummy_local_ident; + TArrow ([], dummy_ty); + (* TAssociatedType { impl = impl_expr; item : concrete_ident }; *) + TOpaque dummy_ident; + TDyn { witness = Features.On.dyn; goals = [] }; + ] + in let ty_string = - " ::=\n" ^ - String.concat ~sep:"\n" ( - List.map - ~f:(fun ty -> - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); - "| " ^ Buffer.contents buf - ) - my_tys) + "\n\n```ebnf\nty ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun ty -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); + "| " ^ Buffer.contents buf) + my_tys) + ^ "\n```" in - let my_pats' = [ - PWild; - PAscription { typ = dummy_ty; typ_span = Span.dummy(); pat = dummy_pat }; - PConstruct { constructor = dummy_global_ident; is_record = false; is_struct = false; fields = []; }; - POr { subpats = [] }; - PArray { args = [] }; - PDeref { subpat = dummy_pat; witness = Features.On.reference }; - PConstant { lit = dummy_literal }; - PBinding { - mut = Mutable Features.On.mutable_variable; - mode = ByValue; - var = dummy_local_ident; - typ = dummy_ty; - subpat = None; - }; - ] in - let my_pats = List.map ~f:(fun x -> { p = x; span = Span.dummy(); typ = dummy_ty }) my_pats' in + let my_pats' = + [ + PWild; + PAscription + { typ = dummy_ty; typ_span = Span.dummy (); pat = dummy_pat }; + PConstruct + { + constructor = dummy_global_ident; + is_record = false; + is_struct = false; + fields = []; + }; + POr { subpats = [ dummy_pat; dummy_pat ] }; + (* Does not render *) + PArray { args = [] }; + PDeref { subpat = dummy_pat; witness = Features.On.reference }; + PConstant { lit = dummy_literal }; + PBinding + { + mut = Mutable Features.On.mutable_variable; + mode = ByValue; + var = dummy_local_ident; + typ = dummy_ty; + subpat = None; + }; + ] + in + let my_pats = + List.map + ~f:(fun x -> { p = x; span = Span.dummy (); typ = dummy_ty }) + my_pats' + in let pat_string = - " ::=\n" ^ - String.concat ~sep:"\n" ( - List.map - ~f:(fun pat -> - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); - "| " ^ Buffer.contents buf - ) - my_pats) + "\n\n```ebnf\npat ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun pat -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); + "| " ^ Buffer.contents buf) + my_pats) + ^ "\n```" in - [Types. - { - path = "ast_spec.txt"; - contents = - "Hax CFG" - ^ "\n" - ^ "=======" - ^ "\n" - ^ expr_string - ^ "\n\n" - ^ ty_string - ^ "\n\n" - ^ pat_string - ^ "\n\n" - ^ item_string; - sourcemap = None; - }] + [ + Types. + { + path = "ast_spec.md"; + contents = + "# Hax CFG" ^ literal_string ^ expr_string ^ ty_string ^ pat_string + ^ item_string; + sourcemap = None; + }; + ] end -let translate _ (_bo) _ = HaxCFG.print_ast () +let translate _ _bo _ = HaxCFG.print_ast () open Phase_utils diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 22261bf84..e81913c09 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -382,6 +382,27 @@ pub fn ensures(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream .into() } +/// Exclude this item from the Hax translation. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn interface(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let ItemFn { + // The function signature + sig, + // The visibility specifier of this function + vis, + // The function block or body + block, + // Other attributes applied to this function + attrs, + } = item.clone(); + + quote! { + #(#attrs)* #vis #sig { todo!() } + }.into() +} + mod kw { syn::custom_keyword!(hax_lib); syn::custom_keyword!(decreases); diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 866c7cfda..e5cf39666 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,7 +2,7 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type, + attributes, ensures, exclude, impl_fn_decoration, include, interface, lemma, loop_invariant, opaque_type, refinement_type, requires, trait_fn_decoration, }; From 0b595b65654f519e27f666e518f08cb836bdb91e Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Sat, 12 Oct 2024 01:54:23 +0200 Subject: [PATCH 4/6] version issues --- engine/lib/backend.ml | 6 +++--- engine/utils/sourcemaps/source_maps.ml | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/engine/lib/backend.ml b/engine/lib/backend.ml index 83007df16..676d5aee0 100644 --- a/engine/lib/backend.ml +++ b/engine/lib/backend.ml @@ -77,7 +77,7 @@ module Make (InputLanguage : Features.T) (M : BackendMetadata) = struct ("[TODO: this error uses failwith, and thus leads to bad error \ messages, please update it using [Diagnostics.*] helpers] " ^ msg) span - [@@ocaml.deprecated - "Use more precise errors: Error.unimplemented, Error.assertion_failure \ - or a raw Error.t (with Error.raise)"] + (* [@@ocaml.deprecated *) + (* "Use more precise errors: Error.unimplemented, Error.assertion_failure \ *) + (* or a raw Error.t (with Error.raise)"] *) end diff --git a/engine/utils/sourcemaps/source_maps.ml b/engine/utils/sourcemaps/source_maps.ml index 6da383baa..64f2aa3fb 100644 --- a/engine/utils/sourcemaps/source_maps.ml +++ b/engine/utils/sourcemaps/source_maps.ml @@ -1,4 +1,5 @@ open Prelude +open Ppx_yojson_conv_lib.Yojson_conv.Primitives module Location = Location include Mappings From dce1d27edd107af15646a3e89ed302835364799f Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Sun, 13 Oct 2024 01:52:27 +0200 Subject: [PATCH 5/6] Print more of AST --- ast_spec.md | 56 +++++---- engine/backends/coq/coq/coq_backend.ml | 153 +++++++++++-------------- 2 files changed, 95 insertions(+), 114 deletions(-) diff --git a/ast_spec.md b/ast_spec.md index 31ad93321..949b26296 100644 --- a/ast_spec.md +++ b/ast_spec.md @@ -12,28 +12,26 @@ literal ::= ```ebnf expr ::= | "if" expr "{" expr "}" ("else" "{" expr "}")? +| expr "(" (expr ",")* ")" | literal | ("[" (expr ",")* "]" | "[" expr ";" int "]") -| constructor (expr)* -| "match" expr "{" (("|" pat)* "=>" (expr "," | "{" "}"))* "}" -| "let" pat (":" ty)? ":=" expr ";" -| (%features: block) modifiers "{" expr "}" +| (ident"(" (expr ",")* ")" | ident"{" (ident ":"expr ";")* "}" | /* features: construct_base */ ident"{" (ident ":"expr ";")* ".." base "}") +| "match" expr "{" (("|" pat)* "=>" (expr "," | "{" expr "}"))* "}" +| ("let" pat (":" ty)? ":=" expr ";" expr | /* features: monadic_binding */ monadic_binding "<" monad ">" "(" "|" pat "|" expr","expr ")") +| /* features: block */ modifiers "{" expr "}" | local_var | global_var -| expr ":" ty +| expr "as" ty | macro_name "!" "(" macro_args ")" -| mut var "=" expr -| (%features: loop) TODO: please implement the method `expr'_Loop` -| (%features: break , loop) "break" -| (%features: early_exit) "return" expr -| (%features: question_mark) expr "?" -| (%features: continue , loop) "continue" -| (%features: reference) "&" expr -| "*" expr -| (%features: mutable_pointer) "*mut" expr +| lhs "=" expr +| (/* features: loop */ "loop" "{" expr "}" | /* features: loop , while_loop */ "while" "(" expr ")" "{" expr "}" | /* features: loop , for_loop */ "for" "(" pat "in" expr ")" "{" expr "}" | /* features: loop , for_index_loop */ "for" "(" "let" ident "in" expr ".." expr ")" "{" expr "}") +| /* features: break , loop */ "break" expr +| /* features: early_exit */ "return" expr +| /* features: question_mark */ expr "?" +| /* features: continue , loop */ "continue" +| /* features: reference */ "&" ("mut")? expr +| ("&" expr "as" "&const _" | /* features: mutable_pointer */ "&mut" expr"as" "&mut _") | "|" param "|" expr -| (%features: monadic_action) TODO: please implement the method `expr'_EffectAction` -| TODO: please implement the method `expr'_Quote` ``` ```ebnf @@ -43,15 +41,16 @@ ty ::= | ("u8" | "u16" | "u32" | "u64" | "u128" | "usize") | ("f16" | "f32" | "f64") | "str" +| (ty ",")* | "[" ty ";" int "]" -| (%features: slice) "[" ty "]" -| ((%features: raw_pointer) "*const" ty | (%features: raw_pointer) "*mut" ty) -| (%features: reference) * expr -| (%features: reference , mutable_reference) *mut expr -| TODO: please implement the method `ty_TParam` +| /* features: slice */ "[" ty "]" +| (/* features: raw_pointer */ "*const" ty | /* features: raw_pointer */ "*mut" ty) +| (/* features: reference */ "*" expr | /* features: reference , mutable_reference */ "*mut" expr) +| ident | (ty "->")* ty -| TODO: please implement the method `ty_TOpaque` -| TODO: please implement the method `ty_TDyn` +| impl "::" item +| "impl" ty +| /* features: dyn */ (goal)* ``` ```ebnf @@ -61,9 +60,9 @@ pat ::= | constructor pat | ("pat" "|")* "pat" | ("[" (expr ",")* "]" | "[" expr ";" int "]") -| TODO: please implement the method `pat'_PDeref` +| /* features: reference */ "&" pat | literal -| TODO: please implement the method `pat'_PBinding` +| /*TODO: please implement the method `pat'_PBinding`*/ ``` ```ebnf @@ -72,12 +71,9 @@ item ::= | "type" ident "=" ty | "enum" ident "=" "{" (ident ("(" (ty)* ")")? ",")* "}" | "struct" ident "=" "{" (ident ":" ty ",")* "}" -| (%features: macro) (public_nat_mod | bytes | public_bytes | array | unsigned_public_integer) +| /* features: macro */ (public_nat_mod | bytes | public_bytes | array | unsigned_public_integer) | "trait" ident "{" (trait_item)* "}" | "impl" ("<" (generics ",")* ">")? ident "for" ty "{" (impl_item)* "}" -| TODO: please implement the method `item'_Alias` +| /*TODO: please implement the method `item'_Alias`*/ | "use" path ";" -| (%features: quote) TODO: please implement the method `item'_Quote` -| TODO: please implement the method `item'_HaxError` -| TODO: please implement the method `item'_NotImplementedYet` ``` diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index ec4e08e43..e83f8a9e3 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -92,7 +92,7 @@ struct module Base = Generic_printer.Make (F) open PPrint - let default_string_for s = "TODO: please implement the method `" ^ s ^ "`" + let default_string_for s = "/*" ^ "TODO: please implement the method `" ^ s ^ "`" ^ "*/" let default_document_for = default_string_for >> string let any_number_of x = parens x ^^ string "*" let option_of x = parens x ^^ string "?" @@ -119,9 +119,10 @@ struct ^^ string "\"" let features l = - parens - (string "%features:" ^^ space - ^^ separate_map (space ^^ comma ^^ space) (fun x -> string x) l) + string "/*" ^^ space + ^^ string "features:" ^^ space + ^^ separate_map (space ^^ comma ^^ space) (fun x -> string x) l + ^^ space ^^ string "*/" ^^ space (* let code_parens x = string "1;31m" ^ parens ( x ^^ string "\x1b[1;31m" ) ^^ string "\x1b[0m" *) @@ -164,12 +165,14 @@ struct method expr ~e ~span:_ ~typ:_ = e#p method expr'_AddressOf ~super:_ ~mut ~e:_ ~witness:_ = - match mut with - | Immutable -> symbol_str "*" ^^ space ^^ string "expr" - | Mutable _ -> - features [ "mutable_pointer" ] - ^^ symbol_str "*mut" ^^ space ^^ string "expr" - + either_of [ + symbol_str "&" ^^ space ^^ string "expr" ^^ space ^^ symbol_str "as" ^^ space ^^ symbol_str "&const _"; + features [ "mutable_pointer" ] ^^ symbol_str "&mut" ^^ space ^^ string "expr" ^^ symbol_str "as" ^^ space ^^ symbol_str "&mut _"; + ] + + method _do_not_override_expr'_App ~super ~f ~args ~generic_args ~bounds_impls ~trait = + string "expr" ^^ space ^^ symbol_parens ( any_number_of (string "expr" ^^ space ^^ symbol_comma) ) + method expr'_App_application ~super:_ ~f:_ ~args:_ ~generics:_ = default_document_for "expr'_App_application" @@ -183,20 +186,20 @@ struct default_document_for "expr'_App_tuple_projection" method expr'_Ascription ~super:_ ~e:_ ~typ:_ = - string "expr" ^^ space ^^ symbol_colon ^^ space ^^ string "ty" + string "expr" ^^ space ^^ symbol_str "as" ^^ space ^^ string "ty" method expr'_Assign ~super:_ ~lhs:_ ~e:_ ~witness:_ = - string "mut var" ^^ space ^^ symbol_str "=" ^^ space ^^ string "expr" + string "lhs" ^^ space ^^ symbol_str "=" ^^ space ^^ string "expr" method expr'_Block ~super:_ ~e:_ ~safety_mode:_ ~witness:_ = features [ "block" ] ^^ string "modifiers" ^^ space ^^ symbol_braces (string "expr") method expr'_Borrow ~super:_ ~kind:_ ~e:_ ~witness:_ = - features [ "reference" ] ^^ symbol_str "&" ^^ space ^^ string "expr" + features [ "reference" ] ^^ symbol_str "&" ^^ space ^^ option_of ( symbol_str "mut" ) ^^ space ^^ string "expr" method expr'_Break ~super:_ ~e:_ ~label:_ ~witness:_ = - features [ "break"; "loop" ] ^^ symbol_str "break" + features [ "break"; "loop" ] ^^ symbol_str "break" ^^ space ^^ string "expr" method expr'_Closure ~super:_ ~params:_ ~body:_ ~captures:_ = symbol_str "|" ^^ space ^^ string "param" ^^ space ^^ symbol_str "|" @@ -204,7 +207,12 @@ struct method expr'_Construct_inductive ~super:_ ~constructor:_ ~is_record:_ ~is_struct:_ ~fields:_ ~base:_ = - string "constructor" ^^ space ^^ any_number_of (string "expr") + either_of [ + string "ident" ^^ symbol_parens ( any_number_of ( string "expr" ^^ space ^^ symbol_comma ) ); + string "ident" ^^ symbol_braces ( any_number_of ( string "ident" ^^ space ^^ symbol_colon ^^ string "expr" ^^ space ^^ symbol_semi ) ); + features ["construct_base"] ^^ string "ident" ^^ symbol_braces ( any_number_of ( string "ident" ^^ space ^^ symbol_colon ^^ string "expr" ^^ space ^^ symbol_semi ) ^^ space ^^ symbol_str ".." ^^ space ^^ string "base" ); + ] + (* string "constructor" ^^ space ^^ any_number_of (string "expr") *) method expr'_Construct_tuple ~super:_ ~components:_ = default_document_for "expr'_Construct_tuple" @@ -226,17 +234,29 @@ struct (symbol_str "else" ^^ space ^^ symbol_braces (string "expr")) method expr'_Let ~super:_ ~monadic:_ ~lhs:_ ~rhs:_ ~body:_ = - symbol_str "let" ^^ space ^^ string "pat" ^^ space - ^^ option_of (symbol_colon ^^ space ^^ string "ty") - ^^ space ^^ symbol_str ":=" ^^ space ^^ string "expr" ^^ space - ^^ symbol_semi + either_of [ + symbol_str "let" ^^ space ^^ string "pat" ^^ space + ^^ option_of ( symbol_colon ^^ space ^^ string "ty" ) + ^^ space ^^ symbol_str ":=" ^^ space ^^ string "expr" ^^ space + ^^ symbol_semi ^^ space ^^ string "expr"; + features ["monadic_binding"] ^^ string "monadic_binding" ^^ space ^^ symbol_str "<" ^^ space ^^ string "monad" ^^ space ^^ symbol_str ">" ^^ space ^^ symbol_parens ( + symbol_str "|" ^^ space ^^ string "pat" ^^ space ^^ symbol_str "|" ^^ space ^^ string "expr" + ^^ symbol_comma + ^^ string "expr"; + ) + ] method expr'_Literal ~super:_ _x2 = string "literal" method expr'_LocalVar ~super:_ _x2 = string "local_var" method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~label:_ ~witness:_ = (* Type of loop *) - features [ "loop" ] ^^ default_document_for "expr'_Loop" + either_of [ + features [ "loop" ] ^^ symbol_str "loop" ^^ space ^^ symbol_braces( string "expr" ); + features [ "loop"; "while_loop" ] ^^ symbol_str "while" ^^ space ^^ symbol_parens( string "expr" ) ^^ space ^^ symbol_braces( string "expr" ); + features [ "loop"; "for_loop" ] ^^ symbol_str "for" ^^ space ^^ symbol_parens( string "pat" ^^ space ^^ symbol_str "in" ^^ space ^^ string "expr" ) ^^ space ^^ symbol_braces ( string "expr" ); + features [ "loop"; "for_index_loop" ] ^^ symbol_str "for" ^^ space ^^ symbol_parens( symbol_str "let" ^^ space ^^ string "ident" ^^ space ^^ symbol_str "in" ^^ space ^^ string "expr" ^^ space ^^ symbol_str ".." ^^ space ^^ string "expr" ) ^^ space ^^ symbol_braces ( string "expr" ); + ] method expr'_MacroInvokation ~super:_ ~macro:_ ~args:_ ~witness:_ = string "macro_name" ^^ space ^^ symbol_str "!" ^^ space @@ -251,7 +271,7 @@ struct ^^ either_of [ string "expr" ^^ space ^^ symbol_comma; - symbol_braces (string ""); + symbol_braces (string "expr"); ])) method expr'_QuestionMark ~super:_ ~e:_ ~return_typ:_ ~witness:_ = @@ -260,8 +280,7 @@ struct method expr'_Quote ~super:_ _x2 = default_document_for "expr'_Quote" method expr'_Return ~super:_ ~e:_ ~witness:_ = - features [ "early_exit" ] ^^ symbol_str "return" ^^ space - ^^ string "expr" + features [ "early_exit" ] ^^ symbol_str "return" ^^ space ^^ string "expr" method field_pat ~field:_ ~pat:_ = default_document_for "field_pat" @@ -481,7 +500,7 @@ struct default_document_for "pat'_PConstruct_tuple" method pat'_PDeref ~super:_ ~subpat:_ ~witness:_ = - default_document_for "pat'_PDeref" + features ["reference"] ^^ symbol_str "&" ^^ space ^^ string "pat" method pat'_PWild = symbol_str "_" @@ -519,7 +538,7 @@ struct method trait_item'_TIType _x1 = default_document_for "trait_item'_TIType" method ty_TApp_application ~typ:_ ~generics:_ = - default_document_for "ty_TApp_application" + any_number_of (string "ty" ^^ space ^^ symbol_comma) (* TODO uses top level implementation ? *) method ty_TApp_tuple ~types:_ = default_document_for "ty_TApp_tuple" @@ -532,11 +551,11 @@ struct ^^ space ^^ string "ty" method ty_TAssociatedType ~impl:_ ~item:_ = - default_document_for "ty_TAssociatedType" + string "impl" ^^ space ^^ symbol_str "::" ^^ space ^^ string "item" method ty_TBool = symbol_str "bool" method ty_TChar = symbol_str "char" - method ty_TDyn ~witness:_ ~goals:_ = default_document_for "ty_TDyn" + method ty_TDyn ~witness:_ ~goals:_ = features ["dyn"] ^^ any_number_of (string "goal") method ty_TFloat _x1 = either_of [ symbol_str "f16"; symbol_str "f32"; symbol_str "f64" ] @@ -552,8 +571,8 @@ struct symbol_str "usize"; ] - method ty_TOpaque _x1 = default_document_for "ty_TOpaque" - method ty_TParam _x1 = default_document_for "ty_TParam" + method ty_TOpaque _x1 = symbol_str "impl" ^^ space ^^ string "ty" + method ty_TParam _x1 = string "ident" method ty_TRawPointer ~witness:_ = either_of @@ -564,13 +583,11 @@ struct ^^ string "ty"; ] - method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut = - match mut with - | Immutable -> - features [ "reference" ] ^^ string "*" ^^ space ^^ string "expr" - | Mutable _ -> - features [ "reference"; "mutable_reference" ] - ^^ string "*mut" ^^ space ^^ string "expr" + method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut:_ = + either_of [ + features [ "reference" ] ^^ symbol_str "*" ^^ space ^^ string "expr"; + features [ "reference"; "mutable_reference" ] ^^ symbol_str "*mut" ^^ space ^^ string "expr"; + ] method ty_TSlice ~witness:_ ~ty:_ = features [ "slice" ] ^^ symbol_brackets (string "ty") @@ -618,7 +635,10 @@ module HaxCFG = struct let dummy_local_ident : local_ident = { name = "dummy"; id = Local_ident.mk_id Typ 0 } in - + let dummy_trait_item = { kind = Self; goal = { trait = dummy_ident; args = [] } } in + + (** Can use rendering tools for EBNF e.g. https://rr.red-dove.com/ui **) + (* print#_do_not_override_lazy_of_item' ~super AstPos_item__v v *) let my_literals = [ @@ -699,9 +719,9 @@ module HaxCFG = struct }; Alias { name = dummy_ident; item = dummy_ident }; Use { path = []; is_external = false; rename = None }; - Quote { contents = []; witness = Features.On.quote }; - HaxError "dummy"; - NotImplementedYet; + (* Quote { contents = []; witness = Features.On.quote }; *) + (* HaxError "dummy"; *) + (* NotImplementedYet; *) ] in let my_items : item list = @@ -726,7 +746,7 @@ module HaxCFG = struct let my_exprs' = [ If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; - (* App { f = dummy_expr; args = []; generic_args = []; bounds_impls = []; trait = None; }; *) + App { f = dummy_expr; args = [ dummy_expr (* must have 1+ items *) ]; generic_args = []; bounds_impls = []; trait = None; }; Literal (String "dummy"); Array []; Construct @@ -793,16 +813,11 @@ module HaxCFG = struct { kind = Shared; e = dummy_expr; witness = Features.On.reference }; AddressOf { mut = Immutable; e = dummy_expr; witness = Features.On.raw_pointer }; - AddressOf - { - mut = Mutable Features.On.mutable_pointer; - e = dummy_expr; - witness = Features.On.raw_pointer; - }; Closure { params = []; body = dummy_expr; captures = [] }; - EffectAction - { action = Features.On.monadic_action; argument = dummy_expr }; - Quote { contents = []; witness = Features.On.quote }; + (* TODO: The two remaing ast elements! *) + (* EffectAction *) + (* { action = Features.On.monadic_action; argument = dummy_expr }; *) + (* Quote { contents = []; witness = Features.On.quote }; *) ] in let my_exprs = @@ -830,7 +845,7 @@ module HaxCFG = struct TInt { size = S8; signedness = Signed }; TFloat F16; TStr; - (* TApp of { ident : global_ident; args : generic_value list }; *) + TApp { ident = dummy_global_ident; args = [] }; TArray { typ = dummy_ty; length = dummy_expr (* const *) }; TSlice { witness = Features.On.slice; ty = dummy_ty }; TRawPointer { witness = Features.On.raw_pointer }; @@ -841,16 +856,9 @@ module HaxCFG = struct typ = dummy_ty; mut = Immutable; }; - TRef - { - witness = Features.On.reference; - region = "todo"; - typ = dummy_ty; - mut = Mutable Features.On.mutable_reference; - }; TParam dummy_local_ident; TArrow ([], dummy_ty); - (* TAssociatedType { impl = impl_expr; item : concrete_ident }; *) + TAssociatedType { impl = dummy_trait_item ; item = dummy_ident }; TOpaque dummy_ident; TDyn { witness = Features.On.dyn; goals = [] }; ] @@ -930,32 +938,9 @@ open Phase_utils module TransformToInputLanguage = [%functor_application Phases.Reject.Unsafe(Features.Rust) - |> Phases.Reject.RawOrMutPointer - |> Phases.And_mut_defsite - |> Phases.Reconstruct_asserts - |> Phases.Reconstruct_for_loops - |> Phases.Direct_and_mut - |> Phases.Reject.Arbitrary_lhs - |> Phases.Drop_blocks - |> Phases.Drop_match_guards - |> Phases.Reject.Continue - |> Phases.Drop_references - |> Phases.Trivialize_assign_lhs - |> Phases.Reconstruct_question_marks - |> Side_effect_utils.Hoist - |> Phases.Local_mutation - |> Phases.Reject.Continue - |> Phases.Cf_into_monads - |> Phases.Reject.EarlyExit - |> Phases.Functionalize_loops - |> Phases.Reject.As_pattern - |> Phases.Reject.Dyn - |> Phases.Reject.Trait_item_default - |> SubtypeToInputLanguage - |> Identity ] [@ocamlformat "disable"] let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) : - AST.item list = - TransformToInputLanguage.ditems items + AST.item list = + [] From 01626c1075a2d2b2ba46796991ba75428d8d371c Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Mon, 14 Oct 2024 18:08:47 +0200 Subject: [PATCH 6/6] Expression generator --- ast_spec.md | 2 +- engine/backends/coq/coq/coq_backend.ml | 894 ++++++++++++++++++------- 2 files changed, 641 insertions(+), 255 deletions(-) diff --git a/ast_spec.md b/ast_spec.md index 949b26296..6f7291cab 100644 --- a/ast_spec.md +++ b/ast_spec.md @@ -76,4 +76,4 @@ item ::= | "impl" ("<" (generics ",")* ">")? ident "for" ty "{" (impl_item)* "}" | /*TODO: please implement the method `item'_Alias`*/ | "use" path ";" -``` +``` \ No newline at end of file diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index e83f8a9e3..147b3ee4e 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -172,7 +172,7 @@ struct method _do_not_override_expr'_App ~super ~f ~args ~generic_args ~bounds_impls ~trait = string "expr" ^^ space ^^ symbol_parens ( any_number_of (string "expr" ^^ space ^^ symbol_comma) ) - + method expr'_App_application ~super:_ ~f:_ ~args:_ ~generics:_ = default_document_for "expr'_App_application" @@ -598,6 +598,7 @@ struct default_document_for "variant" (* END GENERATED *) end + end (* TODO: Write quoted expression shallowly, to get a generator for full AST *) @@ -615,45 +616,490 @@ module HaxCFG = struct module AST = Ast.Make (Features.Full) open AST + type ast_types = + | CONCRETE_IDENT + | LITERAL + | TY + | EXPR + | GENERICS + | GLOBAL_IDENT + | PAT + | LOCAL_IDENT + | IMPL_EXPR + | ITEM + + let rec generate_helper (t : ast_types) (indexes : int list) : Yojson.Safe.t * int list = + let i, indexes = List.hd_exn indexes, Option.value ~default:[] (List.tl indexes) in + let cases: (unit -> Yojson.Safe.t * int list) list = + (match t with + | CONCRETE_IDENT -> + [ + (fun () -> ([%yojson_of: concrete_ident] (Concrete_ident.of_name Value Hax_lib__RefineAs__into_checked), indexes)) + ] + + | LITERAL -> + [ + (fun () -> ([%yojson_of: literal] (String "dummy"), indexes)); + (fun () -> ([%yojson_of: literal] (Char 'a'), indexes)); + (fun () -> ([%yojson_of: literal] (Int {value = "dummy"; negative = false; kind = { size = S8; signedness = Unsigned }}), indexes)); + (fun () -> ([%yojson_of: literal] (Float {value = "dummy"; negative = false; kind = F16}), indexes)); + (fun () -> ([%yojson_of: literal] (Bool false), indexes)); + ] + + | TY -> + [ + (fun () -> ([%yojson_of: ty] TBool, indexes)); + (fun () -> ([%yojson_of: ty] TChar, indexes)); + (fun () -> ([%yojson_of: ty] (TInt { size = S8 ; signedness = Unsigned}), indexes)); + (fun () -> ([%yojson_of: ty] (TFloat F16), indexes)); + (fun () -> ([%yojson_of: ty] TStr, indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + ([%yojson_of: ty] (TApp { ident = g_ident ; args = [] }), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + let length, indexes = generate_helper EXPR indexes in (* Should be const expr ! *) + let length = [%of_yojson: expr] length in + ([%yojson_of: ty] (TArray {typ; length;}), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: ty] (TSlice {witness = Features.On.slice; ty = typ;}), indexes)); + (fun () -> + ([%yojson_of: ty] (TRawPointer {witness = Features.On.raw_pointer;}), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: ty] (TRef { + witness = Features.On.reference; + region = "todo"; + typ = typ; + mut = Immutable; + }), indexes)); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson : local_ident] l_ident in + ([%yojson_of: ty] (TParam l_ident), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson : ty] typ in + ([%yojson_of: ty] (TArrow ([] ,typ)), indexes)); + (fun () -> + let impl_expr, indexes = generate_helper IMPL_EXPR indexes in + let impl_expr = [%of_yojson: impl_expr] impl_expr in + + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + let c_ident = [%of_yojson: concrete_ident] c_ident in + ([%yojson_of: ty] (TAssociatedType {impl = impl_expr; item = c_ident}), indexes)); + (fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + let c_ident = [%of_yojson: concrete_ident] c_ident in + ([%yojson_of: ty] (TOpaque c_ident), indexes)); + (fun () -> + ([%yojson_of: ty] (TDyn { witness = Features.On.dyn; goals= []}), indexes)); + ] + + | EXPR -> + let expr_shell e indexes = + let typ, indexes = generate_helper TY indexes in + (`Assoc [ + ("e" , e ) ; + ("span" , `Assoc [("id" , `Int 79902) ; ("data" , `List [])]) ; + ("typ" , typ) + ], indexes) + in + List.map ~f:(fun expr_f -> (fun () -> + let (expr', indexes) = expr_f () in + expr_shell expr' indexes)) + [ + (fun () -> + let cond, indexes = generate_helper EXPR indexes in + let cond = [%of_yojson: expr] cond in + + let then_, indexes = generate_helper EXPR indexes in + let then_ = [%of_yojson: expr] then_ in + + ([%yojson_of: expr'] (If { + cond = cond; + then_ = then_; + else_ = None + }), indexes)); + (fun () -> + let f, indexes = generate_helper EXPR indexes in + let f = [%of_yojson: expr] f in + + let args, indexes = generate_helper EXPR indexes in + let args = [%of_yojson: expr] args in + + ([%yojson_of: expr'] (App { f; args = [ args (* must have 1+ items *) ]; generic_args = []; bounds_impls = []; trait = None; }), indexes)); + (fun () -> + let lit, indexes = generate_helper LITERAL indexes in + let lit = [%of_yojson: literal] lit in + ([%yojson_of: expr'] (Literal lit), indexes)); + (fun () -> ([%yojson_of: expr'] (Array []), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + + ([%yojson_of: expr'] (Construct { + constructor = g_ident; + is_record = false; + is_struct = false; + fields = []; + base = None; + }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + ([%yojson_of: expr'] (Match { scrutinee = expr; arms = [] }), indexes)); + (fun () -> + let lhs, indexes = generate_helper PAT indexes in + let lhs = [%of_yojson: pat] lhs in + + let rhs, indexes = generate_helper EXPR indexes in + let rhs = [%of_yojson: expr] rhs in + + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + + ([%yojson_of: expr'] (Let { monadic = None; lhs; rhs; body; }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + ([%yojson_of: expr'] (Block { e = expr; safety_mode = Safe; witness = Features.On.block }), indexes)); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson : local_ident] l_ident in + ([%yojson_of: expr'] (LocalVar l_ident), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson : global_ident] g_ident in + ([%yojson_of: expr'] (GlobalVar g_ident), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: expr'] (Ascription { e = expr; typ; }), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson : global_ident] g_ident in + ([%yojson_of: expr'] (MacroInvokation { + macro = g_ident; + args = "dummy"; + witness = Features.On.macro; + }), indexes)); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson : local_ident] l_ident in + + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: expr'] (Assign { + lhs = LhsLocalVar { var = l_ident; typ; }; + e = expr; + witness = Features.On.mutable_variable; + }), indexes)); + (fun () -> + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + + ([%yojson_of: expr'] (Loop { + body = body; + kind = UnconditionalLoop; + state = None; + label = None; + witness = Features.On.loop; + }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + ([%yojson_of: expr'] (Break { + e = expr; + label = None; + witness = (Features.On.break, Features.On.loop); + }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + ([%yojson_of: expr'] (Return { e = expr; witness = Features.On.early_exit }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: expr'] (QuestionMark { + e = expr; + return_typ = typ; + witness = Features.On.question_mark; + }), indexes)); + (fun () -> ([%yojson_of: expr'] (Continue { + e = None; + label = None; + witness = (Features.On.continue, Features.On.loop); + }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + ([%yojson_of: expr'] (Borrow { + kind = Shared; + e = expr; + witness = Features.On.reference + }), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + ([%yojson_of: expr'] (AddressOf + { mut = Immutable; e = expr; witness = Features.On.raw_pointer }), indexes)); + (fun () -> + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + ([%yojson_of: expr'] (Closure { params = []; body; captures = [] }), indexes)); + (* TODO: The two remaing ast elements! *) + (* EffectAction *) + (* { action = Features.On.monadic_action; argument = dummy_expr }; *) + (* Quote { contents = []; witness = Features.On.quote }; *) + ] + + | GENERICS -> + [ + (fun () -> ([%yojson_of: generics] { params = []; constraints = [] }, indexes)); + ] + + | GLOBAL_IDENT -> + [fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + (`List [ `String "Concrete" ; c_ident ], indexes) + ] + + | PAT -> + + let pat_shell v indexes = + let typ, indexes = generate_helper TY indexes in + (`Assoc [ + ("p" , v ) ; + ("span" , `Assoc [("id" , `Int 79902) ; ("data" , `List [])]) ; + ("typ" , typ) ; + ], indexes) + in + List.map ~f:(fun pat_f -> (fun () -> + let (pat', indexes) = pat_f () in + pat_shell pat' indexes)) + [ + (fun () -> ([%yojson_of: pat'] PWild, indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let pat, indexes = generate_helper PAT indexes in + let pat = [%of_yojson: pat] pat in + ([%yojson_of: pat'] (PAscription { + typ; + typ_span = Span.dummy (); + pat; + }), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + ([%yojson_of: pat'] (PConstruct + { + constructor = g_ident; + is_record = false; + is_struct = false; + fields = []; + }), indexes)); + (fun () -> + let lhs_pat, indexes = generate_helper PAT indexes in + let lhs_pat = [%of_yojson: pat] lhs_pat in + + let rhs_pat, indexes = generate_helper PAT indexes in + let rhs_pat = [%of_yojson: pat] rhs_pat in + ([%yojson_of: pat'] (POr { + subpats = [ lhs_pat; rhs_pat ] + }), indexes)); + (fun () -> ([%yojson_of: pat'] (PArray { args = [] }), indexes)); + (fun () -> + let pat, indexes = generate_helper PAT indexes in + let pat = [%of_yojson: pat] pat in + ([%yojson_of: pat'] (PDeref { + subpat = pat; + witness = Features.On.reference + }), indexes)); + (fun () -> + let lit, indexes = generate_helper LITERAL indexes in + let lit = [%of_yojson: literal] lit in + ([%yojson_of: pat'] (PConstant { lit }), indexes)); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson: local_ident] l_ident in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: pat'] (PBinding + { + mut = Mutable Features.On.mutable_variable; + mode = ByValue; + var = l_ident; + typ; + subpat = None; + }), indexes)); + ] + + | LOCAL_IDENT -> + [fun () -> + (`Assoc [("name" , `String "dummy") ; ("id" , `List [`List [`String "Typ"] ; `Int 0])], indexes) + ] + + | IMPL_EXPR -> + [fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + (`Assoc [ + ("kind" , `List [`String "Self"]) ; + ("goal" , `Assoc [ + ("trait" , c_ident) ; + ("args" , `List [])]) + ], indexes) + ] + + | ITEM -> + let item_shell v indexes = + let ident, indexes = generate_helper CONCRETE_IDENT indexes in + (`Assoc [ + ("v" , v ) ; + ("span" , `Assoc [("id" , `Int 79902) ; ("data" , `List [])]) ; + ("ident" , ident) ; + ("attrs" , `List []) + ], indexes) + in + List.map ~f:(fun item_f -> (fun () -> + let (item', indexes) = item_f () in + item_shell item' indexes)) + [ + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + ([%yojson_of: item'] (Fn {name; generics; body; params = []; safety = Safe}), indexes)); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: item'] (TyAlias {name; generics; ty = typ;}), indexes)); + (* enum *) + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ([%yojson_of: item'] (Type {name; generics; variants = []; is_struct = false}), indexes)); + (* struct *) + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ([%yojson_of: item'] (Type {name; generics; variants = []; is_struct = true}), indexes)); + (fun () -> + let macro, indexes = generate_helper CONCRETE_IDENT indexes in + let macro = [%of_yojson: concrete_ident] macro in + ([%yojson_of: item'] (IMacroInvokation {macro; argument = "TODO"; span = Span.dummy(); witness = Features.On.macro}), indexes)); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ([%yojson_of: item'] (Trait { + name ; + generics ; + items = []; + safety = Safe; + }), indexes)); + (fun () -> + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let ty, indexes = generate_helper TY indexes in + let ty = [%of_yojson: ty] ty in + + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + ([%yojson_of: item'] (Impl { + generics; + self_ty = ty; + of_trait = (g_ident, []) ; + items = [] ; + parent_bounds = [] ; + safety = Safe + }), indexes)); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let item, indexes = generate_helper CONCRETE_IDENT indexes in + let item = [%of_yojson: concrete_ident] item in + ([%yojson_of: item'] (Alias { name; item }), indexes)); + (fun () -> + ([%yojson_of: item'] (Use { + path = []; + is_external = false; + rename = None + }), indexes)); + (* Quote { contents = []; witness = Features.On.quote }; *) + (* HaxError "dummy"; *) + (* NotImplementedYet; *) + ] + ) in + List.nth_exn cases i () + + let generate (t : ast_types) (indexes : int list) : Yojson.Safe.t = + fst (generate_helper t indexes) + let print_ast (_ : unit) = let my_printer = new MyPrinter.printer in - let dummy_ident : concrete_ident = - Concrete_ident.of_name Value Hax_lib__RefineAs__into_checked - in - - let dummy_literal = String "dummy" in - - let dummy_ty = TBool in - - let dummy_expr : expr = - { e = Literal dummy_literal; span = Span.dummy (); typ = dummy_ty } - in - let dummy_generics : generics = { params = []; constraints = [] } in - let dummy_global_ident : global_ident = `Concrete dummy_ident in - let dummy_pat = { p = PWild; span = Span.dummy (); typ = dummy_ty } in - let dummy_local_ident : local_ident = - { name = "dummy"; id = Local_ident.mk_id Typ 0 } - in - let dummy_trait_item = { kind = Self; goal = { trait = dummy_ident; args = [] } } in - (** Can use rendering tools for EBNF e.g. https://rr.red-dove.com/ui **) - - (* print#_do_not_override_lazy_of_item' ~super AstPos_item__v v *) - let my_literals = - [ - String "dummy"; - Char 'a'; - Int - { - value = "dummy"; - kind = { size = S8; signedness = Unsigned }; - negative = false; - }; - Float { value = "dummy"; kind = F16; negative = false }; - Bool false; - ] - in + + let concrete_ident_args = [0] in + let global_ident_args = [0] @ concrete_ident_args in + let local_ident_args = [0] in + let generics_args = [0] in + let impl_expr_args = [0;0] in + + let literal_args = [ + (* String *) + [0]; + (* Char *) + [1]; + (* Int *) + [2]; + (* Float *) + [3]; + (* Bool *) + [4] + ] in + let my_literals = List.map ~f:(fun x -> [%of_yojson: literal] (generate LITERAL x)) literal_args in let literal_string = "\n\n```ebnf\nliteral ::=\n" ^ String.concat ~sep:"\n" @@ -667,163 +1113,149 @@ module HaxCFG = struct ^ "\n```" in - let my_items' : item' list = - [ - Fn - { - name = dummy_ident; - generics = dummy_generics; - body = dummy_expr; - params = []; - safety = Safe; - }; - TyAlias { name = dummy_ident; generics = dummy_generics; ty = dummy_ty }; - (* struct *) - Type - { - name = dummy_ident; - generics = dummy_generics; - variants = []; - is_struct = false; - }; - (* enum *) - Type - { - name = dummy_ident; - generics = dummy_generics; - variants = []; - is_struct = true; - }; - IMacroInvokation - { - macro = dummy_ident; - argument = "TODO"; - span = Span.dummy (); - witness = Features.On.macro; - }; - Trait - { - name = dummy_ident; - generics = dummy_generics; - items = []; - safety = Safe; - }; - Impl - { - generics = dummy_generics; - self_ty = dummy_ty; - of_trait = (dummy_global_ident, []); - items = []; - parent_bounds = []; - safety = Safe; - }; - Alias { name = dummy_ident; item = dummy_ident }; - Use { path = []; is_external = false; rename = None }; - (* Quote { contents = []; witness = Features.On.quote }; *) - (* HaxError "dummy"; *) - (* NotImplementedYet; *) - ] + (* TODO: BFS generator *) + let ty_args ~ty ~expr = [ + (* TBool *) + [0]; + (* TChar *) + [1]; + (* TInt *) + [2]; + (* TFloat *) + [3]; + (* TStr *) + [4]; + (* TApp *) + [5] @ global_ident_args; + (* TArray *) + [6] @ ty @ expr; + (* TSlice *) + [7] @ ty; + (* TRawPointer *) + [8]; + (* TRef *) + [9] @ ty; + (* TParam *) + [10] @ local_ident_args; + (* TArrow *) + [11] @ ty; + (* TAssociatedType *) + [12] @ impl_expr_args @ concrete_ident_args ; + (* TOpaque *) + [13] @ concrete_ident_args; + (* TDyn *) + [14]; + ] in + let ty_args = ty_args ~ty:[0] ~expr:[2;0;0] (* TODO: generate random elements in ty and expr *) in + + let my_tys = List.map ~f:(fun x -> [%of_yojson: ty] (generate TY x)) ty_args in + let ty_string = + "\n\n```ebnf\nty ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun ty -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); + "| " ^ Buffer.contents buf) + my_tys) + ^ "\n```" in - let my_items : item list = - List.map - ~f:(fun x -> - { v = x; span = Span.dummy (); ident = dummy_ident; attrs = [] }) - my_items' + + let pat_args ~ty ~ty1 ~literal ~pat1 ~pat2 = List.map ~f:(fun x -> x @ ty) [ + (* PWild *) + [0]; + (* PAscription *) + [1] @ ty1 @ pat1; + (* PConstruct *) + [2] @ global_ident_args; + (* POr *) + [3] @ pat1 @ pat2; + (* PArray *) + [4]; + (* PDeref *) + [5] @ pat1; + (* PConstant *) + [6] @ literal; + (* PBinding *) + [7] @ local_ident_args @ ty1; + ] in + let pat_args = pat_args ~ty:[0] ~ty1:[0] ~literal:(List.nth_exn literal_args 0) ~pat1:[0;0] ~pat2:[0;0] in + + let my_pats = + List.map ~f:(fun x -> [%of_yojson: pat] (generate PAT x)) pat_args in - let item_string = - "\n\n```ebnf\nitem ::=\n" + let pat_string = + "\n\n```ebnf\npat ::=\n" ^ String.concat ~sep:"\n" (List.map - ~f:(fun item -> + ~f:(fun pat -> let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf - (my_printer#entrypoint_item item); + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); "| " ^ Buffer.contents buf) - my_items) + my_pats) ^ "\n```" in - let my_exprs' = - [ - If { cond = dummy_expr; then_ = dummy_expr; else_ = None }; - App { f = dummy_expr; args = [ dummy_expr (* must have 1+ items *) ]; generic_args = []; bounds_impls = []; trait = None; }; - Literal (String "dummy"); - Array []; - Construct - { - constructor = dummy_global_ident; - is_record = false; - is_struct = false; - fields = []; - base = None; - }; - Match { scrutinee = dummy_expr; arms = [] }; - Let - { - monadic = None; - lhs = dummy_pat; - rhs = dummy_expr; - body = dummy_expr; - }; - Block - { e = dummy_expr; safety_mode = Safe; witness = Features.On.block }; - LocalVar dummy_local_ident; - GlobalVar dummy_global_ident; - Ascription { e = dummy_expr; typ = dummy_ty }; - MacroInvokation - { - macro = dummy_global_ident; - args = "dummy"; - witness = Features.On.macro; - }; - Assign - { - lhs = LhsLocalVar { var = dummy_local_ident; typ = dummy_ty }; - e = dummy_expr; - witness = Features.On.mutable_variable; - }; - Loop - { - body = dummy_expr; - kind = UnconditionalLoop; - state = None; - label = None; - witness = Features.On.loop; - }; - Break - { - e = dummy_expr; - label = None; - witness = (Features.On.break, Features.On.loop); - }; - Return { e = dummy_expr; witness = Features.On.early_exit }; - QuestionMark - { - e = dummy_expr; - return_typ = dummy_ty; - witness = Features.On.question_mark; - }; - Continue - { - e = None; - label = None; - witness = (Features.On.continue, Features.On.loop); - }; - Borrow - { kind = Shared; e = dummy_expr; witness = Features.On.reference }; - AddressOf - { mut = Immutable; e = dummy_expr; witness = Features.On.raw_pointer }; - Closure { params = []; body = dummy_expr; captures = [] }; - (* TODO: The two remaing ast elements! *) - (* EffectAction *) - (* { action = Features.On.monadic_action; argument = dummy_expr }; *) - (* Quote { contents = []; witness = Features.On.quote }; *) - ] + let expr_args ~expr_ty ~literal ~ty ~expr0 ~expr1 ~expr2 ~pat = + List.map ~f:(fun x -> x @ expr_ty) + [ + (* If *) + [0] @ expr1 @ expr2 (* @ expr3 *) ; + (* App *) + [1] @ expr1 @ expr2; + (* Literal *) + [2] @ literal; + (* Array *) + [3]; + (* Construct *) + [4] @ global_ident_args; + (* Match *) + [5] @ expr1; + (* Let *) + [6] @ pat @ expr1 @ expr2; + (* Block *) + [7] @ expr1; + (* LocalVar *) + [8] @ local_ident_args; + (* GlobalVar *) + [9] @ global_ident_args; + (* Ascription *) + [10] @ expr1 @ ty; + (* MacroInvokation *) + [11] @ global_ident_args; + (* Assign *) + [12] @ local_ident_args @ expr1 @ ty; + (* Loop *) + [13] @ expr1; + (* Break *) + [14] @ expr1; + (* Return *) + [15] @ expr1; + (* QuestionMark *) + [16] @ expr1 @ ty; + (* Continue *) + [17]; + (* Borrow *) + [18] @ expr1; + (* AddressOf *) + [19] @ expr1; + (* Closure *) + [20] @ expr1; + ] in + let expr_args = + expr_args + ~expr_ty:[0] + ~literal:(List.nth_exn literal_args 0) + ~ty:[0] + ~expr0:[2;0;0] + ~expr1:[2;0;0] + ~expr2:[2;0;0] + ~pat:[0;0] + in + let my_exprs = - List.map - ~f:(fun x -> { e = x; span = Span.dummy (); typ = dummy_ty }) - my_exprs' + List.map ~f:(fun x -> [%of_yojson: expr] (generate EXPR x)) expr_args in let expr_string = "\n\n```ebnf\nexpr ::=\n" @@ -838,84 +1270,38 @@ module HaxCFG = struct ^ "\n```" in - let my_tys = - [ - TBool; - TChar; - TInt { size = S8; signedness = Signed }; - TFloat F16; - TStr; - TApp { ident = dummy_global_ident; args = [] }; - TArray { typ = dummy_ty; length = dummy_expr (* const *) }; - TSlice { witness = Features.On.slice; ty = dummy_ty }; - TRawPointer { witness = Features.On.raw_pointer }; - TRef - { - witness = Features.On.reference; - region = "todo"; - typ = dummy_ty; - mut = Immutable; - }; - TParam dummy_local_ident; - TArrow ([], dummy_ty); - TAssociatedType { impl = dummy_trait_item ; item = dummy_ident }; - TOpaque dummy_ident; - TDyn { witness = Features.On.dyn; goals = [] }; - ] - in - let ty_string = - "\n\n```ebnf\nty ::=\n" - ^ String.concat ~sep:"\n" - (List.map - ~f:(fun ty -> - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); - "| " ^ Buffer.contents buf) - my_tys) - ^ "\n```" - in - - let my_pats' = - [ - PWild; - PAscription - { typ = dummy_ty; typ_span = Span.dummy (); pat = dummy_pat }; - PConstruct - { - constructor = dummy_global_ident; - is_record = false; - is_struct = false; - fields = []; - }; - POr { subpats = [ dummy_pat; dummy_pat ] }; - (* Does not render *) - PArray { args = [] }; - PDeref { subpat = dummy_pat; witness = Features.On.reference }; - PConstant { lit = dummy_literal }; - PBinding - { - mut = Mutable Features.On.mutable_variable; - mode = ByValue; - var = dummy_local_ident; - typ = dummy_ty; - subpat = None; - }; + let item_args = List.map ~f:(fun x -> x @ concrete_ident_args) [ + (* Fn *) + [0] @ concrete_ident_args @ generics_args @ List.nth_exn expr_args 2; + (* TyAlias *) + [1] @ concrete_ident_args @ generics_args @ List.nth_exn ty_args 0; + (* Type *) + [2] @ concrete_ident_args @ generics_args; + (* Type *) + [3] @ concrete_ident_args @ generics_args; + (* IMacroInvokation *) + [4] @ concrete_ident_args; + (* Trait *) + [5] @ concrete_ident_args @ generics_args; + (* Impl *) + [6] @ generics_args @ List.nth_exn ty_args 0 @ global_ident_args; + (* Alias *) + [7] @ concrete_ident_args @ concrete_ident_args; + (* Use *) + [8]; ] in - let my_pats = - List.map - ~f:(fun x -> { p = x; span = Span.dummy (); typ = dummy_ty }) - my_pats' - in - let pat_string = - "\n\n```ebnf\npat ::=\n" + let my_items : item list = List.map ~f:(fun x -> [%of_yojson: item] (generate ITEM x)) item_args in + let item_string = + "\n\n```ebnf\nitem ::=\n" ^ String.concat ~sep:"\n" (List.map - ~f:(fun pat -> + ~f:(fun item -> let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_item item); "| " ^ Buffer.contents buf) - my_pats) + my_items) ^ "\n```" in