diff --git a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml index b9b4cdee919..35e5a990d9d 100644 --- a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml +++ b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml @@ -89,6 +89,7 @@ let mk_top_mllb (e: mlexpr): mllb = mllb_add_unit=false; mllb_def=e; mllb_meta=[]; + mllb_attrs=[]; print_typ=false } (* names of F* functions which need to be handled differently *) @@ -338,7 +339,7 @@ and resugar_app f args es: expression = and get_variants (e : mlexpr) : Parsetree.case list = match e.expr with - | MLE_Fun ([(id, _)], e) -> + | MLE_Fun ([{mlbinder_name=id}], e) -> (match e.expr with | MLE_Match ({expr = MLE_Var id'}, branches) when id = id' -> map build_case branches @@ -369,7 +370,7 @@ and build_constructor_expr ((path, sym), exp): expression = and build_fun l e = match l with - | ((id, ty)::tl) -> + | ({mlbinder_name=id; mlbinder_ty=ty}::tl) -> let p = build_binding_pattern id in Exp.fun_ Nolabel None p (build_fun tl e) | [] -> build_expr e @@ -476,7 +477,7 @@ let build_exn (sym, tys): type_exception = Te.mk_exception ctor let build_module1 path (m1: mlmodule1): structure_item option = - match m1 with + match m1.mlmodule1_m with | MLM_Ty tydecl -> (match build_tydecl tydecl with | Some t -> Some (Str.mk t) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index 9617bbe9608..e61e613d5dc 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -785,30 +785,29 @@ let (find_t : env -> Prims.string -> Prims.int) = FStar_Compiler_Util.format1 "Internal error: name not found %s\n" x in FStar_Compiler_Effect.failwith uu___1 -let add_binders : 'uuuuu . env -> (Prims.string * 'uuuuu) Prims.list -> env = +let (add_binders : + env -> FStar_Extraction_ML_Syntax.mlbinder Prims.list -> env) = fun env1 -> - fun binders -> + fun bs -> FStar_Compiler_List.fold_left (fun env2 -> fun uu___ -> - match uu___ with | (name1, uu___1) -> extend env2 name1) env1 - binders + match uu___ with + | { FStar_Extraction_ML_Syntax.mlbinder_name = mlbinder_name; + FStar_Extraction_ML_Syntax.mlbinder_ty = uu___1; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___2;_} -> + extend env2 mlbinder_name) env1 bs let (list_elements : FStar_Extraction_ML_Syntax.mlexpr -> FStar_Extraction_ML_Syntax.mlexpr Prims.list) = - fun e2 -> - let rec list_elements1 acc e21 = - match e21.FStar_Extraction_ML_Syntax.expr with - | FStar_Extraction_ML_Syntax.MLE_CTor - (("Prims"::[], "Cons"), hd::tl::[]) -> - list_elements1 (hd :: acc) tl - | FStar_Extraction_ML_Syntax.MLE_CTor (("Prims"::[], "Nil"), []) -> - FStar_Compiler_List.rev acc - | uu___ -> - FStar_Compiler_Effect.failwith - "Argument of FStar.Buffer.createL is not a list literal!" in - list_elements1 [] e2 + fun e -> + let lopt = FStar_Extraction_ML_Util.list_elements e in + match lopt with + | FStar_Pervasives_Native.None -> + FStar_Compiler_Effect.failwith + "Argument of FStar.Buffer.createL is not a list literal!" + | FStar_Pervasives_Native.Some l -> l let (translate_flags : FStar_Extraction_ML_Syntax.meta Prims.list -> flag Prims.list) = fun flags -> @@ -1177,20 +1176,18 @@ let rec (translate_type_without_decay' : and (translate_type' : env -> FStar_Extraction_ML_Syntax.mlty -> typ) = fun env1 -> fun t -> translate_type_without_decay env1 t and (translate_binders : - env -> - (Prims.string * FStar_Extraction_ML_Syntax.mlty) Prims.list -> - binder Prims.list) + env -> FStar_Extraction_ML_Syntax.mlbinder Prims.list -> binder Prims.list) + = fun env1 -> fun bs -> FStar_Compiler_List.map (translate_binder env1) bs +and (translate_binder : env -> FStar_Extraction_ML_Syntax.mlbinder -> binder) = - fun env1 -> - fun args -> FStar_Compiler_List.map (translate_binder env1) args -and (translate_binder : - env -> (Prims.string * FStar_Extraction_ML_Syntax.mlty) -> binder) = fun env1 -> fun uu___ -> match uu___ with - | (name1, typ1) -> - let uu___1 = translate_type env1 typ1 in - { name = name1; typ = uu___1; mut = false } + | { FStar_Extraction_ML_Syntax.mlbinder_name = mlbinder_name; + FStar_Extraction_ML_Syntax.mlbinder_ty = mlbinder_ty; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___1;_} -> + let uu___2 = translate_type env1 mlbinder_ty in + { name = mlbinder_name; typ = uu___2; mut = false } and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = fun env1 -> fun e -> @@ -1220,13 +1217,14 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = FStar_Pervasives_Native.Some ([], typ1); FStar_Extraction_ML_Syntax.mllb_add_unit = add_unit; FStar_Extraction_ML_Syntax.mllb_def = body; + FStar_Extraction_ML_Syntax.mllb_attrs = uu___; FStar_Extraction_ML_Syntax.mllb_meta = flags; FStar_Extraction_ML_Syntax.print_typ = print;_}::[]), continuation) -> let binder1 = - let uu___ = translate_type env1 typ1 in - { name = name1; typ = uu___; mut = false } in + let uu___1 = translate_type env1 typ1 in + { name = name1; typ = uu___1; mut = false } in let body1 = translate_expr env1 body in let env2 = extend env1 name1 in let continuation1 = translate_expr env2 continuation in @@ -2505,9 +2503,9 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___3 = FStar_Compiler_List.map (translate_expr env1) es in (uu___2, cons, uu___3) in ECons uu___1 - | FStar_Extraction_ML_Syntax.MLE_Fun (args, body) -> - let binders = translate_binders env1 args in - let env2 = add_binders env1 args in + | FStar_Extraction_ML_Syntax.MLE_Fun (bs, body) -> + let binders = translate_binders env1 bs in + let env2 = add_binders env1 bs in let uu___ = let uu___1 = translate_expr env2 body in let uu___2 = @@ -2842,36 +2840,45 @@ let (translate_let' : FStar_Pervasives_Native.Some (tvars, t0); FStar_Extraction_ML_Syntax.mllb_add_unit = uu___; FStar_Extraction_ML_Syntax.mllb_def = e; + FStar_Extraction_ML_Syntax.mllb_attrs = uu___1; FStar_Extraction_ML_Syntax.mllb_meta = meta; - FStar_Extraction_ML_Syntax.print_typ = uu___1;_} when + FStar_Extraction_ML_Syntax.print_typ = uu___2;_} when FStar_Compiler_Util.for_some - (fun uu___2 -> - match uu___2 with + (fun uu___3 -> + match uu___3 with | FStar_Extraction_ML_Syntax.Assumed -> true - | uu___3 -> false) meta + | uu___4 -> false) meta -> let name2 = ((env1.module_name), name1) in let arg_names = match e.FStar_Extraction_ML_Syntax.expr with - | FStar_Extraction_ML_Syntax.MLE_Fun (args, uu___2) -> - FStar_Compiler_List.map FStar_Pervasives_Native.fst args - | uu___2 -> [] in + | FStar_Extraction_ML_Syntax.MLE_Fun (bs, uu___3) -> + FStar_Compiler_List.map + (fun uu___4 -> + match uu___4 with + | { + FStar_Extraction_ML_Syntax.mlbinder_name = + mlbinder_name; + FStar_Extraction_ML_Syntax.mlbinder_ty = uu___5; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___6;_} + -> mlbinder_name) bs + | uu___3 -> [] in if (FStar_Compiler_List.length tvars) = Prims.int_zero then - let uu___2 = - let uu___3 = - let uu___4 = translate_cc meta in - let uu___5 = translate_flags meta in - let uu___6 = translate_type env1 t0 in - (uu___4, uu___5, name2, uu___6, arg_names) in - DExternal uu___3 in - FStar_Pervasives_Native.Some uu___2 + let uu___3 = + let uu___4 = + let uu___5 = translate_cc meta in + let uu___6 = translate_flags meta in + let uu___7 = translate_type env1 t0 in + (uu___5, uu___6, name2, uu___7, arg_names) in + DExternal uu___4 in + FStar_Pervasives_Native.Some uu___3 else - ((let uu___4 = + ((let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in FStar_Compiler_Util.print1_warning "Not extracting %s to KaRaMeL (polymorphic assumes are not supported)\n" - uu___4); + uu___5); FStar_Pervasives_Native.None) | { FStar_Extraction_ML_Syntax.mllb_name = name1; FStar_Extraction_ML_Syntax.mllb_tysc = @@ -2883,8 +2890,9 @@ let (translate_let' : FStar_Extraction_ML_Syntax.MLE_Fun (args, body); FStar_Extraction_ML_Syntax.mlty = uu___1; FStar_Extraction_ML_Syntax.loc = uu___2;_}; + FStar_Extraction_ML_Syntax.mllb_attrs = uu___3; FStar_Extraction_ML_Syntax.mllb_meta = meta; - FStar_Extraction_ML_Syntax.print_typ = uu___3;_} -> + FStar_Extraction_ML_Syntax.print_typ = uu___4;_} -> if FStar_Compiler_List.mem FStar_Extraction_ML_Syntax.NoExtract meta @@ -2897,26 +2905,26 @@ let (translate_let' : let env3 = FStar_Compiler_List.fold_left (fun env4 -> fun name2 -> extend_t env4 name2) env2 tvars in - let rec find_return_type eff i uu___5 = - match uu___5 with - | FStar_Extraction_ML_Syntax.MLTY_Fun (uu___6, eff1, t) when + let rec find_return_type eff i uu___6 = + match uu___6 with + | FStar_Extraction_ML_Syntax.MLTY_Fun (uu___7, eff1, t) when i > Prims.int_zero -> find_return_type eff1 (i - Prims.int_one) t | t -> (i, eff, t) in let name2 = ((env3.module_name), name1) in - let uu___5 = + let uu___6 = find_return_type FStar_Extraction_ML_Syntax.E_PURE (FStar_Compiler_List.length args) t0 in - match uu___5 with + match uu___6 with | (i, eff, t) -> (if i > Prims.int_zero then (let msg = "function type annotation has less arrows than the number of arguments; please mark the return type abbreviation as inline_for_extraction" in - let uu___7 = + let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in FStar_Compiler_Util.print2_warning - "Not extracting %s to KaRaMeL (%s)\n" uu___7 msg) + "Not extracting %s to KaRaMeL (%s)\n" uu___8 msg) else (); (let t1 = translate_type env3 t in let binders = translate_binders env3 args in @@ -2924,15 +2932,15 @@ let (translate_let' : let cc1 = translate_cc meta in let meta1 = match (eff, t1) with - | (FStar_Extraction_ML_Syntax.E_ERASABLE, uu___7) -> + | (FStar_Extraction_ML_Syntax.E_ERASABLE, uu___8) -> + let uu___9 = translate_flags meta in MustDisappear + :: uu___9 + | (FStar_Extraction_ML_Syntax.E_PURE, TUnit) -> let uu___8 = translate_flags meta in MustDisappear :: uu___8 - | (FStar_Extraction_ML_Syntax.E_PURE, TUnit) -> - let uu___7 = translate_flags meta in MustDisappear - :: uu___7 - | uu___7 -> translate_flags meta in + | uu___8 -> translate_flags meta in try - (fun uu___7 -> + (fun uu___8 -> match () with | () -> let body1 = translate_expr env4 body in @@ -2942,20 +2950,20 @@ let (translate_let' : (FStar_Compiler_List.length tvars), t1, name2, binders, body1))) () with - | uu___7 -> - let msg = FStar_Compiler_Util.print_exn uu___7 in - ((let uu___9 = - let uu___10 = - let uu___11 = + | uu___8 -> + let msg = FStar_Compiler_Util.print_exn uu___8 in + ((let uu___10 = + let uu___11 = + let uu___12 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in FStar_Compiler_Util.format2 "Error while extracting %s to KaRaMeL (%s)\n" - uu___11 msg in + uu___12 msg in (FStar_Errors_Codes.Warning_FunctionNotExtacted, - uu___10) in + uu___11) in FStar_Errors.log_issue - FStar_Compiler_Range_Type.dummyRange uu___9); + FStar_Compiler_Range_Type.dummyRange uu___10); (let msg1 = Prims.strcat "This function was not extracted:\n" msg in @@ -2969,8 +2977,9 @@ let (translate_let' : FStar_Pervasives_Native.Some (tvars, t); FStar_Extraction_ML_Syntax.mllb_add_unit = uu___; FStar_Extraction_ML_Syntax.mllb_def = expr1; + FStar_Extraction_ML_Syntax.mllb_attrs = uu___1; FStar_Extraction_ML_Syntax.mllb_meta = meta; - FStar_Extraction_ML_Syntax.print_typ = uu___1;_} -> + FStar_Extraction_ML_Syntax.print_typ = uu___2;_} -> if FStar_Compiler_List.mem FStar_Extraction_ML_Syntax.NoExtract meta @@ -2983,7 +2992,7 @@ let (translate_let' : let t1 = translate_type env2 t in let name2 = ((env2.module_name), name1) in try - (fun uu___3 -> + (fun uu___4 -> match () with | () -> let expr2 = translate_expr env2 expr1 in @@ -2993,19 +3002,19 @@ let (translate_let' : (FStar_Compiler_List.length tvars), t1, expr2))) () with - | uu___3 -> - ((let uu___5 = - let uu___6 = - let uu___7 = + | uu___4 -> + ((let uu___6 = + let uu___7 = + let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath name2 in - let uu___8 = FStar_Compiler_Util.print_exn uu___3 in + let uu___9 = FStar_Compiler_Util.print_exn uu___4 in FStar_Compiler_Util.format2 - "Error extracting %s to KaRaMeL (%s)\n" uu___7 - uu___8 in + "Error extracting %s to KaRaMeL (%s)\n" uu___8 + uu___9 in (FStar_Errors_Codes.Warning_DefinitionNotTranslated, - uu___6) in + uu___7) in FStar_Errors.log_issue - FStar_Compiler_Range_Type.dummyRange uu___5); + FStar_Compiler_Range_Type.dummyRange uu___6); FStar_Pervasives_Native.Some (DGlobal (meta1, name2, (FStar_Compiler_List.length tvars), @@ -3014,22 +3023,23 @@ let (translate_let' : FStar_Extraction_ML_Syntax.mllb_tysc = ts; FStar_Extraction_ML_Syntax.mllb_add_unit = uu___; FStar_Extraction_ML_Syntax.mllb_def = uu___1; - FStar_Extraction_ML_Syntax.mllb_meta = uu___2; - FStar_Extraction_ML_Syntax.print_typ = uu___3;_} -> - ((let uu___5 = - let uu___6 = + FStar_Extraction_ML_Syntax.mllb_attrs = uu___2; + FStar_Extraction_ML_Syntax.mllb_meta = uu___3; + FStar_Extraction_ML_Syntax.print_typ = uu___4;_} -> + ((let uu___6 = + let uu___7 = FStar_Compiler_Util.format1 "Not extracting %s to KaRaMeL\n" name1 in - (FStar_Errors_Codes.Warning_DefinitionNotTranslated, uu___6) in + (FStar_Errors_Codes.Warning_DefinitionNotTranslated, uu___7) in FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange - uu___5); + uu___6); (match ts with | FStar_Pervasives_Native.Some (idents, t) -> - let uu___6 = + let uu___7 = FStar_Extraction_ML_Code.string_of_mlty ([], "") t in FStar_Compiler_Util.print2 "Type scheme is: forall %s. %s\n" - (FStar_Compiler_String.concat ", " idents) uu___6 + (FStar_Compiler_String.concat ", " idents) uu___7 | FStar_Pervasives_Native.None -> ()); FStar_Pervasives_Native.None) type translate_let_t = @@ -3059,7 +3069,7 @@ let (translate_decl : env -> FStar_Extraction_ML_Syntax.mlmodule1 -> decl Prims.list) = fun env1 -> fun d -> - match d with + match d.FStar_Extraction_ML_Syntax.mlmodule1_m with | FStar_Extraction_ML_Syntax.MLM_Let (flavor, lbs) -> FStar_Compiler_List.choose (translate_let env1 flavor) lbs | FStar_Extraction_ML_Syntax.MLM_Loc uu___ -> [] @@ -3125,7 +3135,7 @@ let (translate : FStar_Extraction_ML_Syntax.mllib -> file Prims.list) = "Unable to translate module: %s because:\n %s\n" m_name uu___3); FStar_Pervasives_Native.None)) modules -let (uu___1715 : unit) = +let (uu___1700 : unit) = register_post_translate_type_without_decay translate_type_without_decay'; register_post_translate_type translate_type'; register_post_translate_type_decl translate_type_decl'; diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml index 61feeb97ee4..2c984538990 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml @@ -633,19 +633,24 @@ let rec (doc_of_expr : FStar_Extraction_ML_Syntax.expr = FStar_Extraction_ML_Syntax.MLE_Fun - ((arg, - uu___3)::[], + ({ + FStar_Extraction_ML_Syntax.mlbinder_name + = arg; + FStar_Extraction_ML_Syntax.mlbinder_ty + = uu___3; + FStar_Extraction_ML_Syntax.mlbinder_attrs + = uu___4;_}::[], possible_match); FStar_Extraction_ML_Syntax.mlty - = uu___4; + = uu___5; FStar_Extraction_ML_Syntax.loc - = uu___5;_}::[]) + = uu___6;_}::[]) when - (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "FStar.Compiler.Effect.try_with") || - (let uu___6 = + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "FStar.Compiler.Effect.try_with") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "FStar.All.try_with") + uu___7 = "FStar.All.try_with") -> let branches = match possible_match with @@ -655,11 +660,11 @@ let rec (doc_of_expr : ({ FStar_Extraction_ML_Syntax.expr = FStar_Extraction_ML_Syntax.MLE_Var arg'; - FStar_Extraction_ML_Syntax.mlty = uu___6; - FStar_Extraction_ML_Syntax.loc = uu___7;_}, + FStar_Extraction_ML_Syntax.mlty = uu___7; + FStar_Extraction_ML_Syntax.loc = uu___8;_}, branches1); - FStar_Extraction_ML_Syntax.mlty = uu___8; - FStar_Extraction_ML_Syntax.loc = uu___9;_} when + FStar_Extraction_ML_Syntax.mlty = uu___9; + FStar_Extraction_ML_Syntax.loc = uu___10;_} when arg = arg' -> branches1 | e2 -> [(FStar_Extraction_ML_Syntax.MLP_Wild, @@ -752,8 +757,10 @@ let rec (doc_of_expr : FStar_Compiler_List.map (fun uu___ -> match uu___ with - | (x, xt) -> - bvar_annot x (FStar_Pervasives_Native.Some xt)) ids in + | { FStar_Extraction_ML_Syntax.mlbinder_name = x; + FStar_Extraction_ML_Syntax.mlbinder_ty = xt; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___1;_} + -> bvar_annot x (FStar_Pervasives_Native.Some xt)) ids in let body1 = doc_of_expr currentModule (min_op_prec, NonAssoc) body in let doc1 = @@ -1024,7 +1031,8 @@ and (doc_of_lets : FStar_Extraction_ML_Syntax.mllb_tysc = tys; FStar_Extraction_ML_Syntax.mllb_add_unit = uu___2; FStar_Extraction_ML_Syntax.mllb_def = e; - FStar_Extraction_ML_Syntax.mllb_meta = uu___3; + FStar_Extraction_ML_Syntax.mllb_attrs = uu___3; + FStar_Extraction_ML_Syntax.mllb_meta = uu___4; FStar_Extraction_ML_Syntax.print_typ = pt;_} -> let e1 = doc_of_expr currentModule (min_op_prec, NonAssoc) e in let ids = [] in @@ -1032,15 +1040,15 @@ and (doc_of_lets : if Prims.op_Negation pt then text "" else - (let uu___5 = + (let uu___6 = (FStar_Extraction_ML_Util.codegen_fsharp ()) && ((rec_ = FStar_Extraction_ML_Syntax.Rec) || top_level) in - if uu___5 + if uu___6 then match tys with | FStar_Pervasives_Native.Some - (uu___6::uu___7, uu___8) -> text "" + (uu___7::uu___8, uu___9) -> text "" | FStar_Pervasives_Native.None -> text "" | FStar_Pervasives_Native.Some ([], ty) -> let ty1 = @@ -1062,22 +1070,22 @@ and (doc_of_lets : doc_of_mltype currentModule (min_op_prec, NonAssoc) ty in let vars = - let uu___7 = + let uu___8 = FStar_Compiler_List.map (fun x -> doc_of_mltype currentModule (min_op_prec, NonAssoc) (FStar_Extraction_ML_Syntax.MLTY_Var x)) vs in - reduce1 uu___7 in + reduce1 uu___8 in reduce1 [text ":"; vars; text "."; ty1]) else text "") in - let uu___4 = - let uu___5 = - let uu___6 = reduce1 ids in - [uu___6; ty_annot; text "="; e1] in - (text name) :: uu___5 in - reduce1 uu___4 in + let uu___5 = + let uu___6 = + let uu___7 = reduce1 ids in + [uu___7; ty_annot; text "="; e1] in + (text name) :: uu___6 in + reduce1 uu___5 in let letdoc = if rec_ = FStar_Extraction_ML_Syntax.Rec then reduce1 [text "let"; text "rec"] @@ -1245,7 +1253,7 @@ let (doc_of_mod1 : = fun currentModule -> fun m -> - match m with + match m.FStar_Extraction_ML_Syntax.mlmodule1_m with | FStar_Extraction_ML_Syntax.MLM_Exn (x, []) -> reduce1 [text "exception"; text x] | FStar_Extraction_ML_Syntax.MLM_Exn (x, args) -> @@ -1284,7 +1292,7 @@ let (doc_of_mod : (fun x -> let doc1 = doc_of_mod1 currentModule x in [doc1; - (match x with + (match x.FStar_Extraction_ML_Syntax.mlmodule1_m with | FStar_Extraction_ML_Syntax.MLM_Loc uu___ -> empty | uu___ -> hardline); hardline]) m in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index 9214b07b477..73c3809197d 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -716,10 +716,21 @@ let (gamma_to_string : FStar_Extraction_ML_UEnv.uenv -> Prims.string) = let uu___1 = FStar_Compiler_List.map (print_binding cm) gamma in FStar_Compiler_String.concat "\n" uu___1 in FStar_Compiler_Util.format1 "Gamma = {\n %s }" uu___ +let (extract_attrs : + FStar_Extraction_ML_UEnv.uenv -> + FStar_Syntax_Syntax.attribute Prims.list -> + FStar_Extraction_ML_Syntax.mlattribute Prims.list) + = + fun env -> + fun attrs -> + FStar_Compiler_List.map + (fun attr -> + let uu___ = FStar_Extraction_ML_Term.term_as_mlexpr env attr in + match uu___ with | (e, uu___1, uu___2) -> e) attrs let (extract_typ_abbrev : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.qualifier Prims.list -> - FStar_Syntax_Syntax.term Prims.list -> + FStar_Syntax_Syntax.attribute Prims.list -> FStar_Syntax_Syntax.letbinding -> (env_t * iface * FStar_Extraction_ML_Syntax.mlmodule1 Prims.list)) = @@ -847,20 +858,29 @@ let (extract_typ_abbrev : (FStar_Extraction_ML_Syntax.MLTD_Abbrev body1)) } in + let loc_mlmodule1 = + let uu___4 = + let uu___5 = FStar_Ident.range_of_lid lid in + FStar_Extraction_ML_Util.mlloc_of_range + uu___5 in + FStar_Extraction_ML_Syntax.MLM_Loc uu___4 in + let ty_mlmodule1 = + FStar_Extraction_ML_Syntax.MLM_Ty [td] in let def2 = let uu___4 = let uu___5 = - let uu___6 = FStar_Ident.range_of_lid lid in - FStar_Extraction_ML_Util.mlloc_of_range - uu___6 in - FStar_Extraction_ML_Syntax.MLM_Loc uu___5 in - [uu___4; - FStar_Extraction_ML_Syntax.MLM_Ty [td]] in + let uu___6 = extract_attrs env2 attrs in + FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + ty_mlmodule1 uu___6 in + [uu___5] in + (FStar_Extraction_ML_Syntax.mk_mlmodule1 + loc_mlmodule1) + :: uu___4 in (env2, iface1, def2)))) let (extract_let_rec_type : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.qualifier Prims.list -> - FStar_Syntax_Syntax.term Prims.list -> + FStar_Syntax_Syntax.attribute Prims.list -> FStar_Syntax_Syntax.letbinding -> (env_t * iface * FStar_Extraction_ML_Syntax.mlmodule1 Prims.list)) = @@ -916,13 +936,23 @@ let (extract_let_rec_type : (FStar_Pervasives_Native.Some (FStar_Extraction_ML_Syntax.MLTD_Abbrev body)) } in + let loc_mlmodule1 = + let uu___4 = + let uu___5 = FStar_Ident.range_of_lid lid in + FStar_Extraction_ML_Util.mlloc_of_range uu___5 in + FStar_Extraction_ML_Syntax.MLM_Loc uu___4 in + let td_mlmodule1 = + FStar_Extraction_ML_Syntax.MLM_Ty [td] in let def = let uu___4 = let uu___5 = - let uu___6 = FStar_Ident.range_of_lid lid in - FStar_Extraction_ML_Util.mlloc_of_range uu___6 in - FStar_Extraction_ML_Syntax.MLM_Loc uu___5 in - [uu___4; FStar_Extraction_ML_Syntax.MLM_Ty [td]] in + let uu___6 = extract_attrs env2 attrs in + FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + td_mlmodule1 uu___6 in + [uu___5] in + (FStar_Extraction_ML_Syntax.mk_mlmodule1 + loc_mlmodule1) + :: uu___4 in let iface1 = iface_of_tydefs [tydef] in (env2, iface1, def))) let (extract_bundle_iface : @@ -1130,12 +1160,14 @@ let (extract_reifiable_effect : FStar_Pervasives_Native.None; FStar_Extraction_ML_Syntax.mllb_add_unit = false; FStar_Extraction_ML_Syntax.mllb_def = exp; + FStar_Extraction_ML_Syntax.mllb_attrs = []; FStar_Extraction_ML_Syntax.mllb_meta = []; FStar_Extraction_ML_Syntax.print_typ = false } in ((iface_of_bindings [(fv, exp_binding)]), - (FStar_Extraction_ML_Syntax.MLM_Let - (FStar_Extraction_ML_Syntax.NonRec, [lb]))) in + (FStar_Extraction_ML_Syntax.mk_mlmodule1 + (FStar_Extraction_ML_Syntax.MLM_Let + (FStar_Extraction_ML_Syntax.NonRec, [lb])))) in let rec extract_fv tm = (let uu___1 = let uu___2 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in @@ -2003,6 +2035,7 @@ let (extract_bundle : FStar_Extraction_ML_Syntax.tydecl_defn = tbody } in (env3, td)))) in + let mlattrs = extract_attrs env se.FStar_Syntax_Syntax.sigattrs in match ((se.FStar_Syntax_Syntax.sigel), (se.FStar_Syntax_Syntax.sigquals)) with @@ -2028,7 +2061,9 @@ let (extract_bundle : let uu___11 = extract_ctor env [] env { dname = l; dtyp = t } in (match uu___11 with | (env1, ctor) -> - (env1, [FStar_Extraction_ML_Syntax.MLM_Exn ctor])) + (env1, + [FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + (FStar_Extraction_ML_Syntax.MLM_Exn ctor) mlattrs])) | (FStar_Syntax_Syntax.Sig_bundle { FStar_Syntax_Syntax.ses = ses; FStar_Syntax_Syntax.lids = uu___;_}, quals) -> @@ -2045,7 +2080,9 @@ let (extract_bundle : FStar_Compiler_Util.fold_map extract_one_family env1 ifams in (match uu___4 with | (env2, td) -> - (env2, [FStar_Extraction_ML_Syntax.MLM_Ty td]))) + (env2, + [FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + (FStar_Extraction_ML_Syntax.MLM_Ty td) mlattrs]))) | uu___ -> FStar_Compiler_Effect.failwith "Unexpected signature element" let (lb_irrelevant : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = @@ -2218,12 +2255,16 @@ let rec (extract_sig : let meta = extract_metadata se1.FStar_Syntax_Syntax.sigattrs in + let mlattrs = + extract_attrs g + se1.FStar_Syntax_Syntax.sigattrs in FStar_Compiler_List.fold_left (fun uu___8 -> fun d -> match uu___8 with | (g1, decls1) -> - (match d with + (match d.FStar_Extraction_ML_Syntax.mlmodule1_m + with | FStar_Extraction_ML_Syntax.MLM_Let (maybe_rec, mllb::[]) -> let uu___9 = @@ -2251,6 +2292,8 @@ let rec (extract_sig : FStar_Extraction_ML_Syntax.mllb_def = (mllb.FStar_Extraction_ML_Syntax.mllb_def); + FStar_Extraction_ML_Syntax.mllb_attrs + = mlattrs; FStar_Extraction_ML_Syntax.mllb_meta = meta; FStar_Extraction_ML_Syntax.print_typ @@ -2260,9 +2303,11 @@ let rec (extract_sig : (g2, (FStar_Compiler_List.op_At decls1 - [FStar_Extraction_ML_Syntax.MLM_Let - (maybe_rec, - [mllb1])]))) + [FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + (FStar_Extraction_ML_Syntax.MLM_Let + (maybe_rec, + [mllb1])) + mlattrs]))) | uu___9 -> let uu___10 = let uu___11 = @@ -2344,9 +2389,13 @@ let rec (extract_sig : let uu___9 = let uu___10 = let uu___11 = - FStar_Extraction_ML_Util.mlloc_of_range - se1.FStar_Syntax_Syntax.sigrng in - FStar_Extraction_ML_Syntax.MLM_Loc uu___11 in + let uu___12 = + FStar_Extraction_ML_Util.mlloc_of_range + se1.FStar_Syntax_Syntax.sigrng in + FStar_Extraction_ML_Syntax.MLM_Loc + uu___12 in + FStar_Extraction_ML_Syntax.mk_mlmodule1 + uu___11 in let uu___11 = let uu___12 = FStar_Extraction_ML_Term.ind_discriminator_body @@ -2651,6 +2700,8 @@ and (extract_sig_let : FStar_Extraction_ML_Term.term_as_mlexpr g uu___4 in (match uu___3 with | (ml_let, uu___4, uu___5) -> + let mlattrs = + extract_attrs g se.FStar_Syntax_Syntax.sigattrs in (match ml_let.FStar_Extraction_ML_Syntax.expr with | FStar_Extraction_ML_Syntax.MLE_Let ((flavor, bindings), uu___6) -> @@ -2742,6 +2793,8 @@ and (extract_sig_let : FStar_Extraction_ML_Syntax.mllb_def = (ml_lb.FStar_Extraction_ML_Syntax.mllb_def); + FStar_Extraction_ML_Syntax.mllb_attrs + = mlattrs; FStar_Extraction_ML_Syntax.mllb_meta = meta; FStar_Extraction_ML_Syntax.print_typ @@ -2783,6 +2836,9 @@ and (extract_sig_let : FStar_Extraction_ML_Syntax.mllb_def = (ml_lb1.FStar_Extraction_ML_Syntax.mllb_def); + FStar_Extraction_ML_Syntax.mllb_attrs + = + (ml_lb1.FStar_Extraction_ML_Syntax.mllb_attrs); FStar_Extraction_ML_Syntax.mllb_meta = (ml_lb1.FStar_Extraction_ML_Syntax.mllb_meta); @@ -2811,12 +2867,19 @@ and (extract_sig_let : let uu___9 = let uu___10 = let uu___11 = - FStar_Extraction_ML_Util.mlloc_of_range - se.FStar_Syntax_Syntax.sigrng in - FStar_Extraction_ML_Syntax.MLM_Loc uu___11 in + let uu___12 = + FStar_Extraction_ML_Util.mlloc_of_range + se.FStar_Syntax_Syntax.sigrng in + FStar_Extraction_ML_Syntax.MLM_Loc + uu___12 in + FStar_Extraction_ML_Syntax.mk_mlmodule1 + uu___11 in [uu___10; - FStar_Extraction_ML_Syntax.MLM_Let - (flavor, (FStar_Compiler_List.rev ml_lbs'))] in + FStar_Extraction_ML_Syntax.mk_mlmodule1_with_attrs + (FStar_Extraction_ML_Syntax.MLM_Let + (flavor, + (FStar_Compiler_List.rev ml_lbs'))) + mlattrs] in let uu___10 = FStar_Extraction_ML_RegEmb.maybe_register_plugin g1 se in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml index 6c1d0ecd219..aac544dad71 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml @@ -54,6 +54,17 @@ let (ml_record : ([], uu___2, args) in FStar_Extraction_ML_Syntax.MLE_Record uu___1 in mk uu___ +let (mk_binder : + FStar_Extraction_ML_Syntax.mlident -> + FStar_Extraction_ML_Syntax.mlty -> FStar_Extraction_ML_Syntax.mlbinder) + = + fun x -> + fun t -> + { + FStar_Extraction_ML_Syntax.mlbinder_name = x; + FStar_Extraction_ML_Syntax.mlbinder_ty = t; + FStar_Extraction_ML_Syntax.mlbinder_attrs = [] + } let (ml_lam : FStar_Extraction_ML_Syntax.mlident -> FStar_Extraction_ML_Syntax.mlexpr -> FStar_Extraction_ML_Syntax.mlexpr) @@ -62,7 +73,7 @@ let (ml_lam : fun e -> mk (FStar_Extraction_ML_Syntax.MLE_Fun - ([(nm, FStar_Extraction_ML_Syntax.MLTY_Top)], e)) + ([mk_binder nm FStar_Extraction_ML_Syntax.MLTY_Top], e)) let (ml_none : FStar_Extraction_ML_Syntax.mlexpr) = mk (FStar_Extraction_ML_Syntax.MLE_Name @@ -1747,8 +1758,8 @@ let (mk_unembed : let body2 = mk (FStar_Extraction_ML_Syntax.MLE_Fun - ([(v, - FStar_Extraction_ML_Syntax.MLTY_Top)], + ([mk_binder v + FStar_Extraction_ML_Syntax.MLTY_Top], body1)) in let uu___4 = let uu___5 = @@ -1801,7 +1812,8 @@ let (mk_unembed : let lam = mk (FStar_Extraction_ML_Syntax.MLE_Fun - ([(arg_v, FStar_Extraction_ML_Syntax.MLTY_Top)], def)) in + ([mk_binder arg_v FStar_Extraction_ML_Syntax.MLTY_Top], + def)) in lam) let (mk_embed : FStar_TypeChecker_Env.env -> @@ -1953,7 +1965,8 @@ let (mk_embed : let lam = mk (FStar_Extraction_ML_Syntax.MLE_Fun - ([(arg_v, FStar_Extraction_ML_Syntax.MLTY_Top)], def)) in + ([mk_binder arg_v FStar_Extraction_ML_Syntax.MLTY_Top], + def)) in lam) let (__do_handle_plugin : FStar_Extraction_ML_UEnv.uenv -> @@ -2012,7 +2025,8 @@ let (__do_handle_plugin : (h, (FStar_Compiler_List.op_At [mk ml_name_str; mk arity1] args))) in - [FStar_Extraction_ML_Syntax.MLM_Top app]) + [FStar_Extraction_ML_Syntax.mk_mlmodule1 + (FStar_Extraction_ML_Syntax.MLM_Top app)]) | FStar_Pervasives_Native.None -> [] in FStar_Compiler_List.collect mk_registration (FStar_Pervasives_Native.snd lbs) @@ -2116,8 +2130,8 @@ let (__do_handle_plugin : let def1 = mk (FStar_Extraction_ML_Syntax.MLE_Fun - ([("_", FStar_Extraction_ML_Syntax.MLTY_Erased)], - def)) in + ([mk_binder "_" + FStar_Extraction_ML_Syntax.MLTY_Erased], def)) in let lb = { FStar_Extraction_ML_Syntax.mllb_name = @@ -2126,6 +2140,7 @@ let (__do_handle_plugin : FStar_Pervasives_Native.None; FStar_Extraction_ML_Syntax.mllb_add_unit = false; FStar_Extraction_ML_Syntax.mllb_def = def1; + FStar_Extraction_ML_Syntax.mllb_attrs = []; FStar_Extraction_ML_Syntax.mllb_meta = []; FStar_Extraction_ML_Syntax.print_typ = false } in @@ -2179,15 +2194,18 @@ let (__do_handle_plugin : FStar_Pervasives_Native.None; FStar_Extraction_ML_Syntax.mllb_add_unit = false; FStar_Extraction_ML_Syntax.mllb_def = app; + FStar_Extraction_ML_Syntax.mllb_attrs = []; FStar_Extraction_ML_Syntax.mllb_meta = []; FStar_Extraction_ML_Syntax.print_typ = false } in - [FStar_Extraction_ML_Syntax.MLM_Let - (FStar_Extraction_ML_Syntax.NonRec, [lb])]) + [FStar_Extraction_ML_Syntax.mk_mlmodule1 + (FStar_Extraction_ML_Syntax.MLM_Let + (FStar_Extraction_ML_Syntax.NonRec, [lb]))]) mutual_sigelts in FStar_Compiler_List.op_At - [FStar_Extraction_ML_Syntax.MLM_Let - (FStar_Extraction_ML_Syntax.Rec, lbs)] unthunking + [FStar_Extraction_ML_Syntax.mk_mlmodule1 + (FStar_Extraction_ML_Syntax.MLM_Let + (FStar_Extraction_ML_Syntax.Rec, lbs))] unthunking | uu___ -> [] let (do_handle_plugin : FStar_Extraction_ML_UEnv.uenv -> diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml index d176a94d1c3..97d2d331e5c 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml @@ -135,10 +135,18 @@ let rec (elim_mlexpr' : let uu___ = let uu___1 = FStar_Compiler_List.map - (fun uu___2 -> - match uu___2 with - | (x, t) -> let uu___3 = elim_mlty env t in (x, uu___3)) - bvs in + (fun b -> + let uu___2 = + elim_mlty env b.FStar_Extraction_ML_Syntax.mlbinder_ty in + let uu___3 = + FStar_Compiler_List.map (elim_mlexpr env) + b.FStar_Extraction_ML_Syntax.mlbinder_attrs in + { + FStar_Extraction_ML_Syntax.mlbinder_name = + (b.FStar_Extraction_ML_Syntax.mlbinder_name); + FStar_Extraction_ML_Syntax.mlbinder_ty = uu___2; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___3 + }) bvs in let uu___2 = elim_mlexpr env e1 in (uu___1, uu___2) in FStar_Extraction_ML_Syntax.MLE_Fun uu___ | FStar_Extraction_ML_Syntax.MLE_Match (e1, branches) -> @@ -222,6 +230,8 @@ and (elim_letbinding : FStar_Extraction_ML_Syntax.mllb_add_unit = (lb.FStar_Extraction_ML_Syntax.mllb_add_unit); FStar_Extraction_ML_Syntax.mllb_def = expr; + FStar_Extraction_ML_Syntax.mllb_attrs = + (lb.FStar_Extraction_ML_Syntax.mllb_attrs); FStar_Extraction_ML_Syntax.mllb_meta = (lb.FStar_Extraction_ML_Syntax.mllb_meta); FStar_Extraction_ML_Syntax.print_typ = @@ -514,34 +524,59 @@ let (elim_module : fun env -> fun m -> let elim_module1 env1 m1 = - match m1 with + match m1.FStar_Extraction_ML_Syntax.mlmodule1_m with | FStar_Extraction_ML_Syntax.MLM_Ty td -> let uu___ = FStar_Compiler_Util.fold_map elim_one_mltydecl env1 td in (match uu___ with - | (env2, td1) -> (env2, (FStar_Extraction_ML_Syntax.MLM_Ty td1))) + | (env2, td1) -> + (env2, + { + FStar_Extraction_ML_Syntax.mlmodule1_m = + (FStar_Extraction_ML_Syntax.MLM_Ty td1); + FStar_Extraction_ML_Syntax.mlmodule1_attrs = + (m1.FStar_Extraction_ML_Syntax.mlmodule1_attrs) + })) | FStar_Extraction_ML_Syntax.MLM_Let lb -> let uu___ = - let uu___1 = elim_letbinding env1 lb in - FStar_Extraction_ML_Syntax.MLM_Let uu___1 in + let uu___1 = + let uu___2 = elim_letbinding env1 lb in + FStar_Extraction_ML_Syntax.MLM_Let uu___2 in + { + FStar_Extraction_ML_Syntax.mlmodule1_m = uu___1; + FStar_Extraction_ML_Syntax.mlmodule1_attrs = + (m1.FStar_Extraction_ML_Syntax.mlmodule1_attrs) + } in (env1, uu___) | FStar_Extraction_ML_Syntax.MLM_Exn (name, sym_tys) -> let uu___ = let uu___1 = let uu___2 = - FStar_Compiler_List.map - (fun uu___3 -> - match uu___3 with - | (s, t) -> - let uu___4 = elim_mlty env1 t in (s, uu___4)) - sym_tys in - (name, uu___2) in - FStar_Extraction_ML_Syntax.MLM_Exn uu___1 in + let uu___3 = + FStar_Compiler_List.map + (fun uu___4 -> + match uu___4 with + | (s, t) -> + let uu___5 = elim_mlty env1 t in (s, uu___5)) + sym_tys in + (name, uu___3) in + FStar_Extraction_ML_Syntax.MLM_Exn uu___2 in + { + FStar_Extraction_ML_Syntax.mlmodule1_m = uu___1; + FStar_Extraction_ML_Syntax.mlmodule1_attrs = + (m1.FStar_Extraction_ML_Syntax.mlmodule1_attrs) + } in (env1, uu___) | FStar_Extraction_ML_Syntax.MLM_Top e -> let uu___ = - let uu___1 = elim_mlexpr env1 e in - FStar_Extraction_ML_Syntax.MLM_Top uu___1 in + let uu___1 = + let uu___2 = elim_mlexpr env1 e in + FStar_Extraction_ML_Syntax.MLM_Top uu___2 in + { + FStar_Extraction_ML_Syntax.mlmodule1_m = uu___1; + FStar_Extraction_ML_Syntax.mlmodule1_attrs = + (m1.FStar_Extraction_ML_Syntax.mlmodule1_attrs) + } in (env1, uu___) | uu___ -> (env1, m1) in let uu___ = diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index 359062050a0..5837b1ac859 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -415,14 +415,19 @@ let (uu___is_Rec : mlletflavor -> Prims.bool) = fun projectee -> match projectee with | Rec -> true | uu___ -> false let (uu___is_NonRec : mlletflavor -> Prims.bool) = fun projectee -> match projectee with | NonRec -> true | uu___ -> false -type mlexpr' = +type mlbinder = + { + mlbinder_name: mlident ; + mlbinder_ty: mlty ; + mlbinder_attrs: mlexpr Prims.list } +and mlexpr' = | MLE_Const of mlconstant | MLE_Var of mlident | MLE_Name of mlpath | MLE_Let of ((mlletflavor * mllb Prims.list) * mlexpr) | MLE_App of (mlexpr * mlexpr Prims.list) | MLE_TApp of (mlexpr * mlty Prims.list) - | MLE_Fun of ((mlident * mlty) Prims.list * mlexpr) + | MLE_Fun of (mlbinder Prims.list * mlexpr) | MLE_Match of (mlexpr * (mlpattern * mlexpr FStar_Pervasives_Native.option * mlexpr) Prims.list) | MLE_Coerce of (mlexpr * mlty * mlty) @@ -446,8 +451,22 @@ and mllb = mllb_tysc: mltyscheme FStar_Pervasives_Native.option ; mllb_add_unit: Prims.bool ; mllb_def: mlexpr ; + mllb_attrs: mlexpr Prims.list ; mllb_meta: metadata ; print_typ: Prims.bool } +let (__proj__Mkmlbinder__item__mlbinder_name : mlbinder -> mlident) = + fun projectee -> + match projectee with + | { mlbinder_name; mlbinder_ty; mlbinder_attrs;_} -> mlbinder_name +let (__proj__Mkmlbinder__item__mlbinder_ty : mlbinder -> mlty) = + fun projectee -> + match projectee with + | { mlbinder_name; mlbinder_ty; mlbinder_attrs;_} -> mlbinder_ty +let (__proj__Mkmlbinder__item__mlbinder_attrs : + mlbinder -> mlexpr Prims.list) = + fun projectee -> + match projectee with + | { mlbinder_name; mlbinder_ty; mlbinder_attrs;_} -> mlbinder_attrs let (uu___is_MLE_Const : mlexpr' -> Prims.bool) = fun projectee -> match projectee with | MLE_Const _0 -> true | uu___ -> false @@ -478,8 +497,7 @@ let (__proj__MLE_TApp__item___0 : mlexpr' -> (mlexpr * mlty Prims.list)) = fun projectee -> match projectee with | MLE_TApp _0 -> _0 let (uu___is_MLE_Fun : mlexpr' -> Prims.bool) = fun projectee -> match projectee with | MLE_Fun _0 -> true | uu___ -> false -let (__proj__MLE_Fun__item___0 : - mlexpr' -> ((mlident * mlty) Prims.list * mlexpr)) = +let (__proj__MLE_Fun__item___0 : mlexpr' -> (mlbinder Prims.list * mlexpr)) = fun projectee -> match projectee with | MLE_Fun _0 -> _0 let (uu___is_MLE_Match : mlexpr' -> Prims.bool) = fun projectee -> @@ -548,36 +566,42 @@ let (__proj__Mkmlexpr__item__loc : mlexpr -> mlloc) = let (__proj__Mkmllb__item__mllb_name : mllb -> mlident) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> mllb_name let (__proj__Mkmllb__item__mllb_tysc : mllb -> mltyscheme FStar_Pervasives_Native.option) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> mllb_tysc let (__proj__Mkmllb__item__mllb_add_unit : mllb -> Prims.bool) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> mllb_add_unit let (__proj__Mkmllb__item__mllb_def : mllb -> mlexpr) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> mllb_def +let (__proj__Mkmllb__item__mllb_attrs : mllb -> mlexpr Prims.list) = + fun projectee -> + match projectee with + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; + print_typ;_} -> mllb_attrs let (__proj__Mkmllb__item__mllb_meta : mllb -> metadata) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> mllb_meta let (__proj__Mkmllb__item__print_typ : mllb -> Prims.bool) = fun projectee -> match projectee with - | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_meta; + | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> print_typ type mlbranch = (mlpattern * mlexpr FStar_Pervasives_Native.option * mlexpr) type mlletbinding = (mlletflavor * mllb Prims.list) +type mlattribute = mlexpr type mltybody = | MLTD_Abbrev of mlty | MLTD_Record of (mlsymbol * mlty) Prims.list @@ -642,33 +666,50 @@ let (__proj__Mkone_mltydecl__item__tydecl_defn : | { tydecl_assumed; tydecl_name; tydecl_ignored; tydecl_parameters; tydecl_meta; tydecl_defn;_} -> tydecl_defn type mltydecl = one_mltydecl Prims.list -type mlmodule1 = +type mlmodule1' = | MLM_Ty of mltydecl | MLM_Let of mlletbinding | MLM_Exn of (mlsymbol * (mlsymbol * mlty) Prims.list) | MLM_Top of mlexpr | MLM_Loc of mlloc -let (uu___is_MLM_Ty : mlmodule1 -> Prims.bool) = +let (uu___is_MLM_Ty : mlmodule1' -> Prims.bool) = fun projectee -> match projectee with | MLM_Ty _0 -> true | uu___ -> false -let (__proj__MLM_Ty__item___0 : mlmodule1 -> mltydecl) = +let (__proj__MLM_Ty__item___0 : mlmodule1' -> mltydecl) = fun projectee -> match projectee with | MLM_Ty _0 -> _0 -let (uu___is_MLM_Let : mlmodule1 -> Prims.bool) = +let (uu___is_MLM_Let : mlmodule1' -> Prims.bool) = fun projectee -> match projectee with | MLM_Let _0 -> true | uu___ -> false -let (__proj__MLM_Let__item___0 : mlmodule1 -> mlletbinding) = +let (__proj__MLM_Let__item___0 : mlmodule1' -> mlletbinding) = fun projectee -> match projectee with | MLM_Let _0 -> _0 -let (uu___is_MLM_Exn : mlmodule1 -> Prims.bool) = +let (uu___is_MLM_Exn : mlmodule1' -> Prims.bool) = fun projectee -> match projectee with | MLM_Exn _0 -> true | uu___ -> false let (__proj__MLM_Exn__item___0 : - mlmodule1 -> (mlsymbol * (mlsymbol * mlty) Prims.list)) = + mlmodule1' -> (mlsymbol * (mlsymbol * mlty) Prims.list)) = fun projectee -> match projectee with | MLM_Exn _0 -> _0 -let (uu___is_MLM_Top : mlmodule1 -> Prims.bool) = +let (uu___is_MLM_Top : mlmodule1' -> Prims.bool) = fun projectee -> match projectee with | MLM_Top _0 -> true | uu___ -> false -let (__proj__MLM_Top__item___0 : mlmodule1 -> mlexpr) = +let (__proj__MLM_Top__item___0 : mlmodule1' -> mlexpr) = fun projectee -> match projectee with | MLM_Top _0 -> _0 -let (uu___is_MLM_Loc : mlmodule1 -> Prims.bool) = +let (uu___is_MLM_Loc : mlmodule1' -> Prims.bool) = fun projectee -> match projectee with | MLM_Loc _0 -> true | uu___ -> false -let (__proj__MLM_Loc__item___0 : mlmodule1 -> mlloc) = +let (__proj__MLM_Loc__item___0 : mlmodule1' -> mlloc) = fun projectee -> match projectee with | MLM_Loc _0 -> _0 +type mlmodule1 = + { + mlmodule1_m: mlmodule1' ; + mlmodule1_attrs: mlattribute Prims.list } +let (__proj__Mkmlmodule1__item__mlmodule1_m : mlmodule1 -> mlmodule1') = + fun projectee -> + match projectee with | { mlmodule1_m; mlmodule1_attrs;_} -> mlmodule1_m +let (__proj__Mkmlmodule1__item__mlmodule1_attrs : + mlmodule1 -> mlattribute Prims.list) = + fun projectee -> + match projectee with + | { mlmodule1_m; mlmodule1_attrs;_} -> mlmodule1_attrs +let (mk_mlmodule1 : mlmodule1' -> mlmodule1) = + fun m -> { mlmodule1_m = m; mlmodule1_attrs = [] } +let (mk_mlmodule1_with_attrs : + mlmodule1' -> mlattribute Prims.list -> mlmodule1) = + fun m -> fun attrs -> { mlmodule1_m = m; mlmodule1_attrs = attrs } type mlmodule = mlmodule1 Prims.list type mlsig1 = | MLS_Mod of (mlsymbol * mlsig1 Prims.list) @@ -800,15 +841,14 @@ let rec (mlexpr_to_string : mlexpr -> Prims.string) = let uu___2 = FStar_Compiler_List.map mlty_to_string ts in FStar_Compiler_String.concat "; " uu___2 in FStar_Compiler_Util.format2 "(MLE_TApp (%s, [%s]))" uu___ uu___1 - | MLE_Fun (xs, e1) -> + | MLE_Fun (bs, e1) -> let uu___ = let uu___1 = FStar_Compiler_List.map - (fun uu___2 -> - match uu___2 with - | (x, t) -> - let uu___3 = mlty_to_string t in - FStar_Compiler_Util.format2 "(%s, %s)" x uu___3) xs in + (fun b -> + let uu___2 = mlty_to_string b.mlbinder_ty in + FStar_Compiler_Util.format2 "(%s, %s)" b.mlbinder_name + uu___2) bs in FStar_Compiler_String.concat "; " uu___1 in let uu___1 = mlexpr_to_string e1 in FStar_Compiler_Util.format2 "(MLE_Fun ([%s], %s))" uu___ uu___1 @@ -1024,7 +1064,7 @@ let (one_mltydecl_to_string : one_mltydecl -> Prims.string) = uu___ let (mlmodule1_to_string : mlmodule1 -> Prims.string) = fun m -> - match m with + match m.mlmodule1_m with | MLM_Ty d -> let uu___ = let uu___1 = FStar_Compiler_List.map one_mltydecl_to_string d in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 7fcfd765d0f..5c91fa3ca93 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -686,6 +686,28 @@ let (fresh_mlidents : (match uu___2 with | (uenv1, v) -> (uenv1, ((v, t) :: vs)))) ts (g, []) in match uu___ with | (g1, vs_ts) -> (vs_ts, g1) +let (fresh_binders : + FStar_Extraction_ML_Syntax.mlty Prims.list -> + FStar_Extraction_ML_UEnv.uenv -> + (FStar_Extraction_ML_Syntax.mlbinder Prims.list * + FStar_Extraction_ML_UEnv.uenv)) + = + fun ts -> + fun g -> + let uu___ = fresh_mlidents ts g in + match uu___ with + | (vs_ts, g1) -> + let uu___1 = + FStar_Compiler_List.map + (fun uu___2 -> + match uu___2 with + | (v, t) -> + { + FStar_Extraction_ML_Syntax.mlbinder_name = v; + FStar_Extraction_ML_Syntax.mlbinder_ty = t; + FStar_Extraction_ML_Syntax.mlbinder_attrs = [] + }) vs_ts in + (uu___1, g1) let (instantiate_maybe_partial : FStar_Extraction_ML_UEnv.uenv -> FStar_Extraction_ML_Syntax.mlexpr -> @@ -748,7 +770,7 @@ let (instantiate_maybe_partial : FStar_Extraction_ML_Syntax.MLTY_Fun (t2, FStar_Extraction_ML_Syntax.E_PURE, out)) ts extra_tyargs in - let uu___2 = fresh_mlidents extra_tyargs g in + let uu___2 = fresh_binders extra_tyargs g in match uu___2 with | (vs_ts, g1) -> let f = @@ -772,14 +794,18 @@ let (eta_expand : if ts = [] then e else - (let uu___2 = fresh_mlidents ts g in + (let uu___2 = fresh_binders ts g in match uu___2 with | (vs_ts, g1) -> let vs_es = FStar_Compiler_List.map (fun uu___3 -> match uu___3 with - | (v, t1) -> + | { FStar_Extraction_ML_Syntax.mlbinder_name = v; + FStar_Extraction_ML_Syntax.mlbinder_ty = t1; + FStar_Extraction_ML_Syntax.mlbinder_attrs = + uu___4;_} + -> FStar_Extraction_ML_Syntax.with_ty t1 (FStar_Extraction_ML_Syntax.MLE_Var v)) vs_ts in let body = @@ -817,7 +843,7 @@ let (default_value_for_ty : if ts = [] then body r else - (let uu___2 = fresh_mlidents ts g in + (let uu___2 = fresh_binders ts g in match uu___2 with | (vs_ts, g1) -> let uu___3 = @@ -908,7 +934,7 @@ let (apply_coercion : (let lb = { FStar_Extraction_ML_Syntax.mllb_name = - (FStar_Pervasives_Native.fst arg); + (arg.FStar_Extraction_ML_Syntax.mlbinder_name); FStar_Extraction_ML_Syntax.mllb_tysc = (FStar_Pervasives_Native.Some ([], t0)); FStar_Extraction_ML_Syntax.mllb_add_unit = false; @@ -917,8 +943,9 @@ let (apply_coercion : (FStar_Extraction_ML_Syntax.MLE_Coerce ((FStar_Extraction_ML_Syntax.with_ty s0 (FStar_Extraction_ML_Syntax.MLE_Var - (FStar_Pervasives_Native.fst arg))), + (arg.FStar_Extraction_ML_Syntax.mlbinder_name))), s0, t0))); + FStar_Extraction_ML_Syntax.mllb_attrs = []; FStar_Extraction_ML_Syntax.mllb_meta = []; FStar_Extraction_ML_Syntax.print_typ = false } in @@ -928,7 +955,13 @@ let (apply_coercion : ((FStar_Extraction_ML_Syntax.NonRec, [lb]), body2)) in FStar_Extraction_ML_Syntax.with_ty expect1 - (mk_fun ((FStar_Pervasives_Native.fst arg), s0) body3)) + (mk_fun + { + FStar_Extraction_ML_Syntax.mlbinder_name = + (arg.FStar_Extraction_ML_Syntax.mlbinder_name); + FStar_Extraction_ML_Syntax.mlbinder_ty = s0; + FStar_Extraction_ML_Syntax.mlbinder_attrs = [] + } body3)) | (FStar_Extraction_ML_Syntax.MLE_Let (lbs, body), uu___2, uu___3) -> let uu___4 = @@ -1935,10 +1968,25 @@ let (maybe_eta_data_and_project_record : (FStar_Compiler_List.op_At args eargs1)))) in FStar_Extraction_ML_Util.resugar_exp uu___3 in + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Compiler_List.map + (fun uu___6 -> + match uu___6 with + | (x, t) -> + { + FStar_Extraction_ML_Syntax.mlbinder_name + = x; + FStar_Extraction_ML_Syntax.mlbinder_ty + = t; + FStar_Extraction_ML_Syntax.mlbinder_attrs + = [] + }) binders in + (uu___5, body) in + FStar_Extraction_ML_Syntax.MLE_Fun uu___4 in FStar_Extraction_ML_Syntax.with_ty - e.FStar_Extraction_ML_Syntax.mlty - (FStar_Extraction_ML_Syntax.MLE_Fun - (binders, body)) + e.FStar_Extraction_ML_Syntax.mlty uu___3 | uu___3 -> FStar_Compiler_Effect.failwith "Impossible: Not a constructor"))) in @@ -3017,6 +3065,27 @@ and (term_as_mlexpr' : let uu___2 = binders_as_ml_binders g bs1 in (match uu___2 with | (ml_bs, env) -> + let ml_bs1 = + FStar_Compiler_List.map2 + (fun uu___3 -> + fun b -> + match uu___3 with + | (x, t1) -> + let uu___4 = + FStar_Compiler_List.map + (fun attr -> + let uu___5 = term_as_mlexpr env attr in + match uu___5 with + | (e, uu___6, uu___7) -> e) + b.FStar_Syntax_Syntax.binder_attrs in + { + FStar_Extraction_ML_Syntax.mlbinder_name + = x; + FStar_Extraction_ML_Syntax.mlbinder_ty = + t1; + FStar_Extraction_ML_Syntax.mlbinder_attrs + = uu___4 + }) ml_bs bs1 in let body2 = match rcopt with | FStar_Pervasives_Native.Some rc -> @@ -3040,15 +3109,23 @@ and (term_as_mlexpr' : (fun uu___5 -> fun uu___6 -> match (uu___5, uu___6) with - | ((uu___7, targ), (f1, t2)) -> + | ({ + FStar_Extraction_ML_Syntax.mlbinder_name + = uu___7; + FStar_Extraction_ML_Syntax.mlbinder_ty + = targ; + FStar_Extraction_ML_Syntax.mlbinder_attrs + = uu___8;_}, + (f1, t2)) -> (FStar_Extraction_ML_Syntax.E_PURE, (FStar_Extraction_ML_Syntax.MLTY_Fun - (targ, f1, t2)))) ml_bs (f, t1) in + (targ, f1, t2)))) ml_bs1 + (f, t1) in (match uu___4 with | (f1, tfun) -> ((FStar_Extraction_ML_Syntax.with_ty tfun (FStar_Extraction_ML_Syntax.MLE_Fun - (ml_bs, ml_body))), f1, tfun))))) + (ml_bs1, ml_body))), f1, tfun))))) | FStar_Syntax_Syntax.Tm_app { FStar_Syntax_Syntax.hd = @@ -3978,6 +4055,8 @@ and (term_as_mlexpr' : FStar_Extraction_ML_Syntax.mllb_add_unit = add_unit; FStar_Extraction_ML_Syntax.mllb_def = e2; + FStar_Extraction_ML_Syntax.mllb_attrs = + []; FStar_Extraction_ML_Syntax.mllb_meta = meta; FStar_Extraction_ML_Syntax.print_typ = @@ -4354,6 +4433,21 @@ let (ind_discriminator_body : let targ = FStar_Extraction_ML_Syntax.MLTY_Top in let disc_ty = FStar_Extraction_ML_Syntax.MLTY_Top in let discrBody = + let bs = + FStar_Compiler_List.map + (fun uu___4 -> + match uu___4 with + | (x, t) -> + { + FStar_Extraction_ML_Syntax.mlbinder_name + = x; + FStar_Extraction_ML_Syntax.mlbinder_ty = + t; + FStar_Extraction_ML_Syntax.mlbinder_attrs + = [] + }) + (FStar_Compiler_List.op_At wildcards + [(mlid, targ)]) in let uu___4 = let uu___5 = let uu___6 = @@ -4390,8 +4484,7 @@ let (ind_discriminator_body : FStar_Extraction_ML_Syntax.MLE_Match uu___8 in FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.ml_bool_ty uu___7 in - ((FStar_Compiler_List.op_At wildcards - [(mlid, targ)]), uu___6) in + (bs, uu___6) in FStar_Extraction_ML_Syntax.MLE_Fun uu___5 in FStar_Extraction_ML_Syntax.with_ty disc_ty uu___4 in let uu___4 = @@ -4399,17 +4492,22 @@ let (ind_discriminator_body : discName in (match uu___4 with | (uu___5, name) -> - FStar_Extraction_ML_Syntax.MLM_Let - (FStar_Extraction_ML_Syntax.NonRec, - [{ - FStar_Extraction_ML_Syntax.mllb_name = name; - FStar_Extraction_ML_Syntax.mllb_tysc = - FStar_Pervasives_Native.None; - FStar_Extraction_ML_Syntax.mllb_add_unit = - false; - FStar_Extraction_ML_Syntax.mllb_def = - discrBody; - FStar_Extraction_ML_Syntax.mllb_meta = []; - FStar_Extraction_ML_Syntax.print_typ = - false - }])))) \ No newline at end of file + FStar_Extraction_ML_Syntax.mk_mlmodule1 + (FStar_Extraction_ML_Syntax.MLM_Let + (FStar_Extraction_ML_Syntax.NonRec, + [{ + FStar_Extraction_ML_Syntax.mllb_name = + name; + FStar_Extraction_ML_Syntax.mllb_tysc = + FStar_Pervasives_Native.None; + FStar_Extraction_ML_Syntax.mllb_add_unit + = false; + FStar_Extraction_ML_Syntax.mllb_def = + discrBody; + FStar_Extraction_ML_Syntax.mllb_attrs = + []; + FStar_Extraction_ML_Syntax.mllb_meta = + []; + FStar_Extraction_ML_Syntax.print_typ = + false + }]))))) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml index 4dd2e9c33e2..b7d8624e9cf 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml @@ -303,17 +303,18 @@ let (join_l : FStar_Compiler_List.fold_left (join r) FStar_Extraction_ML_Syntax.E_PURE fs let (mk_ty_fun : - (FStar_Extraction_ML_Syntax.mlident * FStar_Extraction_ML_Syntax.mlty) - Prims.list -> + FStar_Extraction_ML_Syntax.mlbinder Prims.list -> FStar_Extraction_ML_Syntax.mlty -> FStar_Extraction_ML_Syntax.mlty) = FStar_Compiler_List.fold_right (fun uu___ -> fun t -> match uu___ with - | (uu___1, t0) -> + | { FStar_Extraction_ML_Syntax.mlbinder_name = uu___1; + FStar_Extraction_ML_Syntax.mlbinder_ty = mlbinder_ty; + FStar_Extraction_ML_Syntax.mlbinder_attrs = uu___2;_} -> FStar_Extraction_ML_Syntax.MLTY_Fun - (t0, FStar_Extraction_ML_Syntax.E_PURE, t)) + (mlbinder_ty, FStar_Extraction_ML_Syntax.E_PURE, t)) type unfold_t = FStar_Extraction_ML_Syntax.mlty -> FStar_Extraction_ML_Syntax.mlty FStar_Pervasives_Native.option @@ -638,9 +639,18 @@ let (prims_op_equality : FStar_Extraction_ML_Syntax.mlexpr) = let (prims_op_amp_amp : FStar_Extraction_ML_Syntax.mlexpr) = let uu___ = mk_ty_fun - [("x", FStar_Extraction_ML_Syntax.ml_bool_ty); - ("y", FStar_Extraction_ML_Syntax.ml_bool_ty)] - FStar_Extraction_ML_Syntax.ml_bool_ty in + [{ + FStar_Extraction_ML_Syntax.mlbinder_name = "x"; + FStar_Extraction_ML_Syntax.mlbinder_ty = + FStar_Extraction_ML_Syntax.ml_bool_ty; + FStar_Extraction_ML_Syntax.mlbinder_attrs = [] + }; + { + FStar_Extraction_ML_Syntax.mlbinder_name = "y"; + FStar_Extraction_ML_Syntax.mlbinder_ty = + FStar_Extraction_ML_Syntax.ml_bool_ty; + FStar_Extraction_ML_Syntax.mlbinder_attrs = [] + }] FStar_Extraction_ML_Syntax.ml_bool_ty in FStar_Extraction_ML_Syntax.with_ty uu___ (FStar_Extraction_ML_Syntax.MLE_Name (["Prims"], "op_AmpAmp")) let (conjoin : @@ -699,4 +709,19 @@ let rec (uncurry_mlty_fun : | FStar_Extraction_ML_Syntax.MLTY_Fun (a, uu___, b) -> let uu___1 = uncurry_mlty_fun b in (match uu___1 with | (args, res) -> ((a :: args), res)) - | uu___ -> ([], t) \ No newline at end of file + | uu___ -> ([], t) +let (list_elements : + FStar_Extraction_ML_Syntax.mlexpr -> + FStar_Extraction_ML_Syntax.mlexpr Prims.list + FStar_Pervasives_Native.option) + = + fun e -> + let rec list_elements1 acc e1 = + match e1.FStar_Extraction_ML_Syntax.expr with + | FStar_Extraction_ML_Syntax.MLE_CTor + (("Prims"::[], "Cons"), hd::tl::[]) -> + list_elements1 (hd :: acc) tl + | FStar_Extraction_ML_Syntax.MLE_CTor (("Prims"::[], "Nil"), []) -> + FStar_Pervasives_Native.Some (FStar_Compiler_List.rev acc) + | uu___ -> FStar_Pervasives_Native.None in + list_elements1 [] e \ No newline at end of file diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index 6d7156ac9cf..5cee9a726c6 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/src/extraction/FStar.Extraction.Krml.fst @@ -326,22 +326,16 @@ let find_t env x = with _ -> failwith (BU.format1 "Internal error: name not found %s\n" x) -let add_binders env binders = - List.fold_left (fun env (name, _) -> extend env name) env binders +let add_binders env bs = + List.fold_left (fun env {mlbinder_name} -> extend env mlbinder_name) env bs (* Actual translation ********************************************************) -let list_elements e2 = - let rec list_elements acc e2 = - match e2.expr with - | MLE_CTor (([ "Prims" ], "Cons" ), [ hd; tl ]) -> - list_elements (hd :: acc) tl - | MLE_CTor (([ "Prims" ], "Nil" ), []) -> - List.rev acc - | _ -> - failwith "Argument of FStar.Buffer.createL is not a list literal!" - in - list_elements [] e2 +let list_elements e = + let lopt = FStar.Extraction.ML.Util.list_elements e in + match lopt with + | None -> failwith "Argument of FStar.Buffer.createL is not a list literal!" + | Some l -> l let translate_flags flags = List.choose (function @@ -589,11 +583,11 @@ and translate_type' env t: typ = | t -> translate_type_without_decay env t -and translate_binders env args = - List.map (translate_binder env) args +and translate_binders env bs = + List.map (translate_binder env) bs -and translate_binder env (name, typ) = - { name = name; typ = translate_type env typ; mut = false } +and translate_binder env ({mlbinder_name;mlbinder_ty}) = + { name = mlbinder_name; typ = translate_type env mlbinder_ty; mut = false } and translate_expr' env e: expr = match e.expr with @@ -995,9 +989,9 @@ and translate_expr' env e: expr = | MLE_CTor ((_, cons), es) -> ECons (assert_lid env e.mlty, cons, List.map (translate_expr env) es) - | MLE_Fun (args, body) -> - let binders = translate_binders env args in - let env = add_binders env args in + | MLE_Fun (bs, body) -> + let binders = translate_binders env bs in + let env = add_binders env bs in EFun (binders, translate_expr env body, translate_type env body.mlty) | MLE_If (e1, e2, e3) -> @@ -1168,7 +1162,7 @@ let translate_let' env flavor lb: option decl = } when BU.for_some (function Syntax.Assumed -> true | _ -> false) meta -> let name = env.module_name, name in let arg_names = match e.expr with - | MLE_Fun (args, _) -> List.map fst args + | MLE_Fun (bs, _) -> List.map (fun {mlbinder_name} -> mlbinder_name) bs | _ -> [] in if List.length tvars = 0 then @@ -1277,7 +1271,7 @@ let translate_let env flavor lb: option decl = !ref_translate_let env flavor lb let translate_decl env d: list decl = - match d with + match d.mlmodule1_m with | MLM_Let (flavor, lbs) -> // We don't care about mutual recursion, since every C file will include // its own header with the forward declarations. diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index d41e997511d..4116e96783d 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/src/extraction/FStar.Extraction.ML.Code.fst @@ -433,7 +433,7 @@ let rec doc_of_expr (currentModule : mlsymbol) (outer : level) (e : mlexpr) : do match e.expr, args with | MLE_Name p, [ ({ expr = MLE_Fun ([ _ ], scrutinee) }); - ({ expr = MLE_Fun ([ (arg, _) ], possible_match)}) + ({ expr = MLE_Fun ([ {mlbinder_name=arg} ], possible_match)}) ] when (string_of_mlpath p = "FStar.Compiler.Effect.try_with" || string_of_mlpath p = "FStar.All.try_with") -> let branches = @@ -479,7 +479,7 @@ let rec doc_of_expr (currentModule : mlsymbol) (outer : level) (e : mlexpr) : do (match xt with | Some xxt -> reduce1 [text " : "; doc_of_mltype currentModule outer xxt] | _ -> text ""); text ")"] else text x in - let ids = List.map (fun (x ,xt) -> bvar_annot x (Some xt)) ids in + let ids = List.map (fun {mlbinder_name=x;mlbinder_ty=xt} -> bvar_annot x (Some xt)) ids in let body = doc_of_expr currentModule (min_op_prec, NonAssoc) body in let doc = reduce1 [text "fun"; reduce1 ids; text "->"; body] in parens doc @@ -745,7 +745,7 @@ and doc_of_sig (currentModule : mlsymbol) (s : mlsig) = (* -------------------------------------------------------------------- *) let doc_of_mod1 (currentModule : mlsymbol) (m : mlmodule1) = - match m with + match m.mlmodule1_m with | MLM_Exn (x, []) -> reduce1 [text "exception"; text x] @@ -774,7 +774,7 @@ let doc_of_mod1 (currentModule : mlsymbol) (m : mlmodule1) = let doc_of_mod (currentModule : mlsymbol) (m : mlmodule) = let docs = List.map (fun x -> let doc = doc_of_mod1 currentModule x in - [doc; (match x with | MLM_Loc _ -> empty | _ -> hardline); hardline]) m in + [doc; (match x.mlmodule1_m with | MLM_Loc _ -> empty | _ -> hardline); hardline]) m in reduce (List.flatten docs) (* -------------------------------------------------------------------- *) diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index f9bfdc8a791..a0c51b99fcb 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -320,6 +320,8 @@ let gamma_to_string env = BU.format1 "Gamma = {\n %s }" (List.map (print_binding cm) gamma |> String.concat "\n") +let extract_attrs env (attrs:list S.attribute) : list mlattribute = + List.map (fun attr -> let e, _, _ = Term.term_as_mlexpr env attr in e) attrs (* Type abbreviations: //extracting `type t = e` @@ -390,7 +392,10 @@ let extract_typ_abbrev env quals attrs lb tydecl_meta = metadata; tydecl_defn = Some (MLTD_Abbrev body) } in - let def = [MLM_Loc (Util.mlloc_of_range (Ident.range_of_lid lid)); MLM_Ty [td]] in + let loc_mlmodule1 = MLM_Loc (Util.mlloc_of_range (Ident.range_of_lid lid)) in + let ty_mlmodule1 = MLM_Ty [td] in + let def = [mk_mlmodule1 loc_mlmodule1; + mk_mlmodule1_with_attrs ty_mlmodule1 (extract_attrs env attrs)] in env, iface, def @@ -426,7 +431,10 @@ let extract_let_rec_type env quals attrs lb tydecl_meta = metadata; tydecl_defn = Some (MLTD_Abbrev body) } in - let def = [MLM_Loc (Util.mlloc_of_range (Ident.range_of_lid lid)); MLM_Ty [td]] in + let loc_mlmodule1 = MLM_Loc (Util.mlloc_of_range (Ident.range_of_lid lid)) in + let td_mlmodule1 = MLM_Ty [td] in + let def = [mk_mlmodule1 loc_mlmodule1; + mk_mlmodule1_with_attrs td_mlmodule1 (extract_attrs env attrs)] in let iface = iface_of_tydefs [tydef] in env, iface, @@ -534,11 +542,12 @@ let extract_reifiable_effect g ed mllb_tysc=None; mllb_add_unit=false; mllb_def=exp; + mllb_attrs=[]; mllb_meta = []; print_typ=false } in - iface_of_bindings [fv, exp_binding], MLM_Let(NonRec, [lb]) + iface_of_bindings [fv, exp_binding], mk_mlmodule1 (MLM_Let(NonRec, [lb])) in let rec extract_fv tm = @@ -621,7 +630,7 @@ let should_split_let_rec_types_and_terms (env:uenv) (lbs:list letbinding) false in not (is_homogeneous None lbs) - + let split_let_rec_types_and_terms se (env:uenv) (lbs:list letbinding) : list sigelt = let rec aux (out:list sigelt) (mutuals:list letbinding) (lbs:list letbinding) @@ -947,10 +956,11 @@ let extract_bundle env se = td in + let mlattrs = extract_attrs env se.sigattrs in match se.sigel, se.sigquals with | Sig_bundle {ses=[{sigel = Sig_datacon {lid=l; t}}]}, [ExceptionConstructor] -> let env, ctor = extract_ctor env [] env ({dname=l; dtyp=t}) in - env, [MLM_Exn ctor] + env, [mk_mlmodule1_with_attrs (MLM_Exn ctor) mlattrs] | Sig_bundle {ses}, quals -> if U.has_attribute se.sigattrs PC.erasable_attr @@ -958,7 +968,7 @@ let extract_bundle env se = else begin let env, ifams = bundle_as_inductive_families env ses quals in let env, td = BU.fold_map extract_one_family env ifams in - env, [MLM_Ty td] + env, [mk_mlmodule1_with_attrs (MLM_Ty td) mlattrs] end | _ -> failwith "Unexpected signature element" @@ -973,144 +983,144 @@ let lb_irrelevant (g:env_t) (lb:letbinding) : bool = (*****************************************************************************) let rec extract_sig (g:env_t) (se:sigelt) : env_t * list mlmodule1 = Errors.with_ctx (BU.format1 "While extracting top-level definition `%s`" (Print.sigelt_to_string_short se)) (fun () -> - debug g (fun u -> BU.print1 ">>>> extract_sig %s \n" (Print.sigelt_to_string_short se)); + debug g (fun u -> BU.print1 ">>>> extract_sig %s \n" (Print.sigelt_to_string_short se)); - if sigelt_has_noextract se then - let g = mark_sigelt_erased se g in - g, [] - else + if sigelt_has_noextract se then + let g = mark_sigelt_erased se g in + g, [] + else begin let se = karamel_fixup_qual se in - match se.sigel with - | Sig_bundle _ - | Sig_inductive_typ _ - | Sig_datacon _ -> - let g, ses = extract_bundle g se in - g, ses @ maybe_register_plugin g se + match se.sigel with + | Sig_bundle _ + | Sig_inductive_typ _ + | Sig_datacon _ -> + let g, ses = extract_bundle g se in + g, ses @ maybe_register_plugin g se - | Sig_new_effect ed when Env.is_reifiable_effect (tcenv_of_uenv g) ed.mname -> - let env, _iface, impl = - extract_reifiable_effect g ed in - env, impl + | Sig_new_effect ed when Env.is_reifiable_effect (tcenv_of_uenv g) ed.mname -> + let env, _iface, impl = + extract_reifiable_effect g ed in + env, impl - | Sig_splice _ -> - failwith "impossible: trying to extract splice" + | Sig_splice _ -> + failwith "impossible: trying to extract splice" - | Sig_fail _ -> - failwith "impossible: trying to extract Sig_fail" + | Sig_fail _ -> + failwith "impossible: trying to extract Sig_fail" - | Sig_new_effect _ -> - g, [] + | Sig_new_effect _ -> + g, [] - (* Ignore all non-informative sigelts *) - | Sig_let {lbs=(_, lbs)} when List.for_all (lb_irrelevant g) lbs -> - g, [] + (* Ignore all non-informative sigelts *) + | Sig_let {lbs=(_, lbs)} when List.for_all (lb_irrelevant g) lbs -> + g, [] - | Sig_declare_typ {lid; us=univs; t} when Term.is_arity g t -> //lid is a type - //extracting `assume type t : k` - let env, _, impl = extract_type_declaration g false lid se.sigquals se.sigattrs univs t in - env, impl + | Sig_declare_typ {lid; us=univs; t} when Term.is_arity g t -> //lid is a type + //extracting `assume type t : k` + let env, _, impl = extract_type_declaration g false lid se.sigquals se.sigattrs univs t in + env, impl - | Sig_let {lbs=(false, [lb])} when Term.is_arity g lb.lbtyp -> - //extracting `type t = e` - //or `let t = e` when e is a type - if se.sigquals |> BU.for_some (function Projector _ -> true | _ -> false) - then ( - //Don't extract projectors returning types---not useful for typing generated code and - //And can actually break F# extraction, in case there are unused type parameters - g, [] - ) else ( - let env, _, impl = - extract_typ_abbrev g se.sigquals se.sigattrs lb - in - env, impl - ) + | Sig_let {lbs=(false, [lb])} when Term.is_arity g lb.lbtyp -> + //extracting `type t = e` + //or `let t = e` when e is a type + if se.sigquals |> BU.for_some (function Projector _ -> true | _ -> false) + then ( + //Don't extract projectors returning types---not useful for typing generated code and + //And can actually break F# extraction, in case there are unused type parameters + g, [] + ) else ( + let env, _, impl = + extract_typ_abbrev g se.sigquals se.sigattrs lb + in + env, impl + ) - | Sig_let {lbs=(true, lbs)} - when should_split_let_rec_types_and_terms g lbs -> - let ses = split_let_rec_types_and_terms se g lbs in - List.fold_left - (fun (g, out) se -> - let g, mls = extract_sig g se in - g, out@mls) - (g, []) ses - - | Sig_let {lbs=(true, lbs)} - when BU.for_some (fun lb -> Term.is_arity g lb.lbtyp) lbs -> - //extracting `let rec t .. : Type = e - // and ... - let env, _, impl = - extract_let_rec_types se g lbs - in - env, impl - - (* Extension extraction is only supported for non-recursive let bindings *) - | Sig_let { lbs=(false, [lb]) } when (Cons? se.sigmeta.sigmeta_extension_data) -> ( - match List.tryPick - (fun (ext, blob) -> - match lookup_extension_extractor ext with - | None -> None - | Some extractor -> Some (ext, blob, extractor)) - se.sigmeta.sigmeta_extension_data - with - | None -> - extract_sig_let g se - - | Some (ext, blob, extractor) -> - match extractor.extract_sigelt g se blob with - | Inl decls -> - let meta = extract_metadata se.sigattrs in - List.fold_left (fun (g, decls) d -> - match d with - | MLM_Let (maybe_rec, [mllb]) -> - let g, mlid, _ = - UEnv.extend_lb g lb.lbname lb.lbtyp (must mllb.mllb_tysc) mllb.mllb_add_unit in - let mllb = { mllb with mllb_name = mlid; mllb_meta = meta } in - g, decls@[MLM_Let (maybe_rec, [mllb])] - | _ -> - failwith (BU.format1 "Unexpected ML decl returned by the extension: %s" (mlmodule1_to_string d)) - ) (g, []) decls - | Inr err -> - Errors.raise_error - (Errors.Fatal_ExtractionUnsupported, - BU.format2 "Extension %s failed to extract term: %s" ext err) - se.sigrng - ) - - | Sig_let _ -> - extract_sig_let g se - - | Sig_declare_typ {lid; t} -> - let quals = se.sigquals in - if quals |> List.contains Assumption - && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) - then let always_fail = - { se with sigel = Sig_let {lbs=(false, [always_fail lid t]); lids=[]} } in - let g, mlm = extract_sig g always_fail in //extend the scope with the new name - match BU.find_map quals (function Discriminator l -> Some l | _ -> None) with - | Some l -> //if it's a discriminator, generate real code for it, rather than mlm - g, [MLM_Loc (Util.mlloc_of_range se.sigrng); Term.ind_discriminator_body g lid l] - - | _ -> - begin match BU.find_map quals (function Projector (l,_) -> Some l | _ -> None) with - (* TODO : this could fail, it happens that projectors for variants are assumed *) - | Some _ -> //it must be a record projector, since other projectors are not assumed - g, [] //records are extracted as ML records; no projectors for them - | _ -> - g, mlm //in all other cases, generate mlm, a stub that always fails - end - else g, [] //it's not assumed, so wait for the corresponding Sig_let to generate code - //or, it must be erased + | Sig_let {lbs=(true, lbs)} + when should_split_let_rec_types_and_terms g lbs -> + let ses = split_let_rec_types_and_terms se g lbs in + List.fold_left + (fun (g, out) se -> + let g, mls = extract_sig g se in + g, out@mls) (g, []) ses + + | Sig_let {lbs=(true, lbs)} + when BU.for_some (fun lb -> Term.is_arity g lb.lbtyp) lbs -> + //extracting `let rec t .. : Type = e + // and ... + let env, _, impl = + extract_let_rec_types se g lbs + in + env, impl + + (* Extension extraction is only supported for non-recursive let bindings *) + | Sig_let { lbs=(false, [lb]) } when (Cons? se.sigmeta.sigmeta_extension_data) -> ( + match List.tryPick + (fun (ext, blob) -> + match lookup_extension_extractor ext with + | None -> None + | Some extractor -> Some (ext, blob, extractor)) + se.sigmeta.sigmeta_extension_data with + | None -> + extract_sig_let g se - | Sig_assume _ //not needed; purely logical - | Sig_sub_effect _ - | Sig_effect_abbrev _ //effects are all primitive; so these are not extracted; this may change as we add user-defined non-primitive effects - | Sig_polymonadic_bind _ - | Sig_polymonadic_subcomp _ -> - g, [] - | Sig_pragma (p) -> - U.process_pragma p se.sigrng; - g, [] + | Some (ext, blob, extractor) -> + match extractor.extract_sigelt g se blob with + | Inl decls -> + let meta = extract_metadata se.sigattrs in + let mlattrs = extract_attrs g se.sigattrs in + List.fold_left (fun (g, decls) d -> + match d.mlmodule1_m with + | MLM_Let (maybe_rec, [mllb]) -> + let g, mlid, _ = + UEnv.extend_lb g lb.lbname lb.lbtyp (must mllb.mllb_tysc) mllb.mllb_add_unit in + let mllb = { mllb with mllb_name = mlid; mllb_attrs = mlattrs; mllb_meta = meta } in + g, decls@[mk_mlmodule1_with_attrs (MLM_Let (maybe_rec, [mllb])) mlattrs] + | _ -> + failwith (BU.format1 "Unexpected ML decl returned by the extension: %s" (mlmodule1_to_string d)) + ) (g, []) decls + | Inr err -> + Errors.raise_error + (Errors.Fatal_ExtractionUnsupported, + BU.format2 "Extension %s failed to extract term: %s" ext err) + se.sigrng + ) + + | Sig_let _ -> extract_sig_let g se + + | Sig_declare_typ {lid; t} -> + let quals = se.sigquals in + if quals |> List.contains Assumption + && not (TcUtil.must_erase_for_extraction (tcenv_of_uenv g) t) + then let always_fail = + { se with sigel = Sig_let {lbs=(false, [always_fail lid t]); lids=[]} } in + let g, mlm = extract_sig g always_fail in //extend the scope with the new name + match BU.find_map quals (function Discriminator l -> Some l | _ -> None) with + | Some l -> //if it's a discriminator, generate real code for it, rather than mlm + g, [mk_mlmodule1 (MLM_Loc (Util.mlloc_of_range se.sigrng)); + Term.ind_discriminator_body g lid l] + + | _ -> + begin match BU.find_map quals (function Projector (l,_) -> Some l | _ -> None) with + (* TODO : this could fail, it happens that projectors for variants are assumed *) + | Some _ -> //it must be a record projector, since other projectors are not assumed + g, [] //records are extracted as ML records; no projectors for them + | _ -> + g, mlm //in all other cases, generate mlm, a stub that always fails + end + else g, [] //it's not assumed, so wait for the corresponding Sig_let to generate code + //or, it must be erased + + | Sig_assume _ //not needed; purely logical + | Sig_sub_effect _ + | Sig_effect_abbrev _ //effects are all primitive; so these are not extracted; this may change as we add user-defined non-primitive effects + | Sig_polymonadic_bind _ + | Sig_polymonadic_subcomp _ -> + g, [] + | Sig_pragma (p) -> + U.process_pragma p se.sigrng; + g, [] + end ) and extract_sig_let (g:uenv) (se:sigelt) : uenv * list mlmodule1 = @@ -1201,6 +1211,7 @@ and extract_sig_let (g:uenv) (se:sigelt) : uenv * list mlmodule1 = g (mk (Tm_let {lbs; body=U.exp_false_bool}) se.sigrng) in + let mlattrs = extract_attrs g se.sigattrs in begin match ml_let.expr with | MLE_Let((flavor, bindings), _) -> @@ -1238,7 +1249,7 @@ and extract_sig_let (g:uenv) (se:sigelt) : uenv * list mlmodule1 = [] in let meta = flags @ flags' @ flags'' in - let ml_lb = { ml_lb with mllb_meta = meta } in + let ml_lb = { ml_lb with mllb_attrs = mlattrs; mllb_meta = meta } in let g, ml_lb = if quals |> BU.for_some (function Projector _ -> true | _ -> false) //projector names have to mangled then let env, mls, _ = @@ -1256,8 +1267,8 @@ and extract_sig_let (g:uenv) (se:sigelt) : uenv * list mlmodule1 = bindings (snd lbs) in g, - [MLM_Loc (Util.mlloc_of_range se.sigrng); - MLM_Let (flavor, List.rev ml_lbs')] + [mk_mlmodule1 (MLM_Loc (Util.mlloc_of_range se.sigrng)); + mk_mlmodule1_with_attrs (MLM_Let (flavor, List.rev ml_lbs')) mlattrs] @ maybe_register_plugin g se | _ -> diff --git a/src/extraction/FStar.Extraction.ML.RegEmb.fst b/src/extraction/FStar.Extraction.ML.RegEmb.fst index d4332a12cf0..113465cdef2 100644 --- a/src/extraction/FStar.Extraction.ML.RegEmb.fst +++ b/src/extraction/FStar.Extraction.ML.RegEmb.fst @@ -72,8 +72,10 @@ let ml_record : Ident.lid -> list (string & mlexpr) -> mlexpr = // [] -> assuming same module mk (MLE_Record ([], l |> Ident.ident_of_lid |> Ident.string_of_id, args)) +let mk_binder x t = {mlbinder_name=x; mlbinder_ty=t; mlbinder_attrs=[]} + let ml_lam nm e = - mk <| MLE_Fun ([(nm, MLTY_Top)], e) + mk <| MLE_Fun ([mk_binder nm MLTY_Top ], e) let ml_none : mlexpr = mk (MLE_Name (["FStar"; "Pervasives"; "Native"], "None")) let ml_some : mlexpr = mk (MLE_Name (["FStar"; "Pervasives"; "Native"], "Some")) @@ -595,7 +597,7 @@ let mk_unembed let ret = mk (MLE_App (ml_some, [ret])) in // final return let body = List.fold_right (fun (v, ty) body -> - let body = mk (MLE_Fun ([(v, MLTY_Top)], body)) in + let body = mk (MLE_Fun ([mk_binder v MLTY_Top], body)) in mk (MLE_App (ml_name bind_opt_lid, [ mk (MLE_App (ml_name unembed_lid, [embedding_for tcenv mutuals SyntaxTerm [] ty; mk (MLE_Var v)])); @@ -612,7 +614,7 @@ let mk_unembed let branches = List.rev (nomatch :: !e_branches) in let sc = mk (MLE_Var arg_v) in let def = mk (MLE_Match (sc, branches)) in - let lam = mk (MLE_Fun ([arg_v, MLTY_Top], def)) in + let lam = mk (MLE_Fun ([mk_binder arg_v MLTY_Top], def)) in lam (* Creates an embedding function for the type *) @@ -663,7 +665,7 @@ let mk_embed let branches = List.rev !e_branches in let sc = mk (MLE_Var arg_v) in let def = mk (MLE_Match (sc, branches)) in - let lam = mk (MLE_Fun ([arg_v, MLTY_Top], def)) in + let lam = mk (MLE_Fun ([mk_binder arg_v MLTY_Top], def)) in lam @@ -689,7 +691,7 @@ let __do_handle_plugin (g: uenv) (arity_opt: option int) (se: sigelt) : list mlm let h = with_ty MLTY_Top <| MLE_Name register in let arity = MLE_Const (MLC_Int(string_of_int arity, None)) in let app = with_ty MLTY_Top <| MLE_App (h, [mk ml_name_str; mk arity] @ args) in - [MLM_Top app] + [MLM_Top app |> mk_mlmodule1] | None -> [] in List.collect mk_registration (snd lbs) @@ -728,13 +730,14 @@ let __do_handle_plugin (g: uenv) (arity_opt: option int) (se: sigelt) : list mlm ml_unembed; ml_embed])) in - let def = mk (MLE_Fun ([("_", MLTY_Erased)], def)) in // thunk + let def = mk (MLE_Fun ([mk_binder "_" MLTY_Erased], def)) in // thunk let lb = { mllb_name = "__knot_e_" ^ name; mllb_tysc = None; mllb_add_unit = false; mllb_def = def; mllb_meta = []; + mllb_attrs = []; print_typ = false; } in @@ -761,14 +764,15 @@ let __do_handle_plugin (g: uenv) (arity_opt: option int) (se: sigelt) : list mlm mllb_add_unit = false; mllb_def = app; mllb_meta = []; + mllb_attrs = []; print_typ = false; } in - [MLM_Let (NonRec, [lb])] + [MLM_Let (NonRec, [lb]) |> mk_mlmodule1] ) in // TODO: We always make a let rec, we could check if that's really needed. - [MLM_Let (Rec, lbs)] @ unthunking + [MLM_Let (Rec, lbs) |> mk_mlmodule1] @ unthunking | _ -> [] diff --git a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst index eb7a8080d60..d30fb091753 100644 --- a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst +++ b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst @@ -136,7 +136,10 @@ let rec elim_mlexpr' (env:env_t) (e:mlexpr') = | MLE_Let (lb, e) -> MLE_Let(elim_letbinding env lb, elim_mlexpr env e) | MLE_App(e, es) -> MLE_App(elim_mlexpr env e, List.map (elim_mlexpr env) es) | MLE_TApp (e, tys) -> MLE_TApp(e, List.map (elim_mlty env) tys) - | MLE_Fun(bvs, e) -> MLE_Fun(List.map (fun (x, t) -> x, elim_mlty env t) bvs, elim_mlexpr env e) + | MLE_Fun(bvs, e) -> + MLE_Fun (List.map (fun b -> {mlbinder_name=b.mlbinder_name; + mlbinder_ty=elim_mlty env b.mlbinder_ty; + mlbinder_attrs=List.map (elim_mlexpr env) b.mlbinder_attrs}) bvs, elim_mlexpr env e) | MLE_Match(e, branches) -> MLE_Match(elim_mlexpr env e, List.map (elim_branch env) branches) | MLE_Coerce(e, t0, t1) -> MLE_Coerce(elim_mlexpr env e, elim_mlty env t0, elim_mlty env t1) | MLE_CTor(l, es) -> MLE_CTor(l, List.map (elim_mlexpr env) es) @@ -333,16 +336,16 @@ let elim_one_mltydecl (env:env_t) (td:one_mltydecl) let elim_module env m = let elim_module1 env m = - match m with + match m.mlmodule1_m with | MLM_Ty td -> let env, td = BU.fold_map elim_one_mltydecl env td in - env, MLM_Ty td + env, { m with mlmodule1_m = MLM_Ty td } | MLM_Let lb -> - env, MLM_Let (elim_letbinding env lb) + env, { m with mlmodule1_m = MLM_Let (elim_letbinding env lb) } | MLM_Exn (name, sym_tys) -> - env, MLM_Exn (name, List.map (fun (s, t) -> s, elim_mlty env t) sym_tys) + env, { m with mlmodule1_m = MLM_Exn (name, List.map (fun (s, t) -> s, elim_mlty env t) sym_tys) } | MLM_Top e -> - env, MLM_Top (elim_mlexpr env e) + env, { m with mlmodule1_m = MLM_Top (elim_mlexpr env e) } | _ -> env, m in diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index 070b0fc2143..15af6d1ef48 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/src/extraction/FStar.Extraction.ML.Syntax.fst @@ -152,14 +152,20 @@ type mlletflavor = | Rec | NonRec -type mlexpr' = +type mlbinder = { + mlbinder_name:mlident; + mlbinder_ty:mlty; + mlbinder_attrs:list mlattribute; +} + +and mlexpr' = | MLE_Const of mlconstant | MLE_Var of mlident | MLE_Name of mlpath | MLE_Let of mlletbinding * mlexpr //tyscheme for polymorphic recursion | MLE_App of mlexpr * list mlexpr //why are function types curried, but the applications not curried | MLE_TApp of mlexpr * list mlty -| MLE_Fun of list (mlident * mlty) * mlexpr +| MLE_Fun of list mlbinder * mlexpr | MLE_Match of mlexpr * list mlbranch | MLE_Coerce of mlexpr * mlty * mlty (* SUGAR *) @@ -187,12 +193,15 @@ and mllb = { mllb_tysc:option mltyscheme; // May be None for top-level bindings only mllb_add_unit:bool; mllb_def:mlexpr; + mllb_attrs:list mlattribute; mllb_meta:metadata; print_typ:bool; } and mlletbinding = mlletflavor * list mllb +and mlattribute = mlexpr + type mltybody = | MLTD_Abbrev of mlty | MLTD_Record of list (mlsymbol * mlty) @@ -213,13 +222,21 @@ type one_mltydecl = { type mltydecl = list one_mltydecl // each element of this list is one among a collection of mutually defined types -type mlmodule1 = +type mlmodule1' = | MLM_Ty of mltydecl | MLM_Let of mlletbinding | MLM_Exn of mlsymbol * list (mlsymbol * mlty) | MLM_Top of mlexpr // this seems outdated | MLM_Loc of mlloc // Location information; line number + file; only for the OCaml backend +type mlmodule1 = { + mlmodule1_m : mlmodule1'; + mlmodule1_attrs : list mlattribute; +} + +let mk_mlmodule1 m = { mlmodule1_m = m; mlmodule1_attrs = [] } +let mk_mlmodule1_with_attrs m attrs = { mlmodule1_m = m; mlmodule1_attrs = attrs } + type mlmodule = list mlmodule1 type mlsig1 = @@ -304,8 +321,10 @@ let rec mlexpr_to_string (e:mlexpr) = BU.format2 "(MLE_App (%s, [%s]))" (mlexpr_to_string e) (String.concat "; " (List.map mlexpr_to_string es)) | MLE_TApp (e, ts) -> BU.format2 "(MLE_TApp (%s, [%s]))" (mlexpr_to_string e) (String.concat "; " (List.map mlty_to_string ts)) - | MLE_Fun (xs, e) -> - BU.format2 "(MLE_Fun ([%s], %s))" (String.concat "; " (List.map (fun (x, t) -> BU.format2 "(%s, %s)" x (mlty_to_string t)) xs)) (mlexpr_to_string e) + | MLE_Fun (bs, e) -> + BU.format2 "(MLE_Fun ([%s], %s))" + (String.concat "; " (List.map (fun b -> BU.format2 "(%s, %s)" b.mlbinder_name (mlty_to_string b.mlbinder_ty)) bs)) + (mlexpr_to_string e) | MLE_Match (e, bs) -> BU.format2 "(MLE_Match (%s, [%s]))" (mlexpr_to_string e) (String.concat "; " (List.map mlbranch_to_string bs)) | MLE_Coerce (e, t1, t2) -> @@ -391,7 +410,7 @@ let one_mltydecl_to_string (d:one_mltydecl) : string = | Some d -> mltybody_to_string d) let mlmodule1_to_string (m:mlmodule1) : string = - match m with + match m.mlmodule1_m with | MLM_Ty d -> BU.format1 "MLM_Ty [%s]" (List.map one_mltydecl_to_string d |> String.concat "; ") | MLM_Let l -> BU.format1 "MLM_Let %s" (mlletbinding_to_string l) | MLM_Exn (s, l) -> diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index 72df6af7cd0..cb67c4fe15a 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/src/extraction/FStar.Extraction.ML.Term.fst @@ -447,6 +447,11 @@ let fresh_mlidents (ts:list mlty) (g:uenv) : list (mlident * mlty) * uenv = in vs_ts, g +let fresh_binders (ts:list mlty) (g:uenv) : list mlbinder * uenv = + let vs_ts, g = fresh_mlidents ts g in + List.map (fun (v, t) -> {mlbinder_name=v; mlbinder_ty=t; mlbinder_attrs=[]}) vs_ts, + g + //instantiate_maybe_partial: // When `e` has polymorphic type `s` // and isn't instantiated in F* (e.g., because of first-class polymorphism) @@ -492,7 +497,7 @@ let instantiate_maybe_partial (g:uenv) (e:mlexpr) (s:mltyscheme) (tyargs:list ml ts extra_tyargs in - let vs_ts, g = fresh_mlidents extra_tyargs g in + let vs_ts, g = fresh_binders extra_tyargs g in let f = with_ty t <| MLE_Fun (vs_ts, tapp) in (f, E_PURE, t) else failwith "Impossible: instantiate_maybe_partial called with too many arguments" @@ -503,8 +508,8 @@ let eta_expand (g:uenv) (t : mlty) (e : mlexpr) : mlexpr = if ts = [] then e else // just quit if this is not a function type - let vs_ts, g = fresh_mlidents ts g in - let vs_es = List.map (fun (v, t) -> with_ty t (MLE_Var v)) vs_ts in + let vs_ts, g = fresh_binders ts g in + let vs_es = List.map (fun {mlbinder_name=v; mlbinder_ty=t} -> with_ty t (MLE_Var v)) vs_ts in let body = with_ty r <| MLE_App (e, vs_es) in with_ty t <| MLE_Fun (vs_ts, body) @@ -526,7 +531,7 @@ let default_value_for_ty (g:uenv) (t : mlty) : mlexpr = in if ts = [] then body r - else let vs_ts, g = fresh_mlidents ts g in + else let vs_ts, g = fresh_binders ts g in with_ty t <| MLE_Fun (vs_ts, body r) let maybe_eta_expand_coercion g expect e = @@ -582,14 +587,15 @@ let apply_coercion pos (g:uenv) (e:mlexpr) (ty:mlty) (expect:mlty) : mlexpr = then with_ty expect (mk_fun arg body) else let lb = { mllb_meta = []; - mllb_name = fst arg; + mllb_attrs = []; + mllb_name = arg.mlbinder_name; mllb_tysc = Some ([], t0); mllb_add_unit = false; - mllb_def = with_ty t0 (MLE_Coerce(with_ty s0 <| MLE_Var (fst arg), s0, t0)); + mllb_def = with_ty t0 (MLE_Coerce(with_ty s0 <| MLE_Var arg.mlbinder_name, s0, t0)); print_typ=false } in let body = with_ty s1 <| MLE_Let((NonRec, [lb]), body) in - with_ty expect (mk_fun (fst arg, s0) body) + with_ty expect (mk_fun {mlbinder_name=arg.mlbinder_name;mlbinder_ty=s0;mlbinder_attrs=[]} body) | MLE_Let(lbs, body), _, _ -> with_ty expect <| (MLE_Let(lbs, aux body ty expect)) @@ -1161,7 +1167,7 @@ let maybe_eta_data_and_project_record (g:uenv) (qual : option fv_qual) (residual match e.expr with | MLE_CTor(head, args) -> let body = Util.resugar_exp <| (as_record qual <| (with_ty tres <| MLE_CTor(head, args@eargs))) in - with_ty e.mlty <| MLE_Fun(binders, body) + with_ty e.mlty <| MLE_Fun(List.map (fun (x,t) -> {mlbinder_name=x;mlbinder_ty=t;mlbinder_attrs=[]}) binders, body) | _ -> failwith "Impossible: Not a constructor" in match mlAppExpr.expr, qual with @@ -1541,6 +1547,11 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) = | Tm_abs {bs;body;rc_opt=rcopt} (* the annotated computation type of the body *) -> let bs, body = SS.open_term bs body in let ml_bs, env = binders_as_ml_binders g bs in + let ml_bs = List.map2 (fun (x,t) b -> { + mlbinder_name=x; + mlbinder_ty=t; + mlbinder_attrs=List.map (fun attr -> let e, _, _ = term_as_mlexpr env attr in e) b.binder_attrs; + }) ml_bs bs in let body = match rcopt with | Some rc -> @@ -1548,7 +1559,7 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) = | None -> debug g (fun () -> BU.print1 "No computation type for: %s\n" (Print.term_to_string body)); body in let ml_body, f, t = term_as_mlexpr env body in let f, tfun = List.fold_right - (fun (_, targ) (f, t) -> E_PURE, MLTY_Fun (targ, f, t)) + (fun {mlbinder_ty=targ} (f, t) -> E_PURE, MLTY_Fun (targ, f, t)) ml_bs (f, t) in with_ty tfun <| MLE_Fun(ml_bs, ml_body), f, tfun @@ -1912,7 +1923,7 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) = | E_ERASABLE, MLTY_Erased -> [Erased] | _ -> [] in - f, {mllb_meta = meta; mllb_name=nm; mllb_tysc=Some polytype; mllb_add_unit=add_unit; mllb_def=e; print_typ=true} + f, {mllb_meta = meta; mllb_attrs = []; mllb_name=nm; mllb_tysc=Some polytype; mllb_add_unit=add_unit; mllb_def=e; print_typ=true} in let lbs = extract_lb_sig g (is_rec, lbs) in @@ -2059,8 +2070,11 @@ let ind_discriminator_body env (discName:lident) (constrName:lident) : mlmodule1 // polymorphic value to make sure that the type is not printed. let disc_ty = MLTY_Top in let discrBody = + let bs = + wildcards @ [(mlid, targ)] + |> List.map (fun (x,t) -> {mlbinder_name=x;mlbinder_ty=t;mlbinder_attrs=[]}) in with_ty disc_ty <| - MLE_Fun(wildcards @ [(mlid, targ)], + MLE_Fun(bs, with_ty ml_bool_ty <| (MLE_Match(with_ty targ <| MLE_Name([], mlid), // Note: it is legal in OCaml to write [Foo _] for a constructor with zero arguments, so don't bother. @@ -2075,8 +2089,9 @@ let ind_discriminator_body env (discName:lident) (constrName:lident) : mlmodule1 let _, name = mlpath_of_lident env discName in MLM_Let (NonRec, [{ mllb_meta=[]; + mllb_attrs=[]; mllb_name=name; mllb_tysc=None; mllb_add_unit=false; mllb_def=discrBody; - print_typ=false}] ) + print_typ=false}] ) |> mk_mlmodule1 diff --git a/src/extraction/FStar.Extraction.ML.Util.fst b/src/extraction/FStar.Extraction.ML.Util.fst index a5c1dcebc62..d9bd4aa609b 100644 --- a/src/extraction/FStar.Extraction.ML.Util.fst +++ b/src/extraction/FStar.Extraction.ML.Util.fst @@ -179,7 +179,7 @@ let join r f f' = match f, f' with let join_l r fs = List.fold_left (join r) E_PURE fs -let mk_ty_fun = List.fold_right (fun (_, t0) t -> MLTY_Fun(t0, E_PURE, t)) +let mk_ty_fun = List.fold_right (fun {mlbinder_ty} t -> MLTY_Fun(mlbinder_ty, E_PURE, t)) (* type_leq is essentially the lifting of the sub-effect relation, eff_leq, into function types. type_leq_c is a coercive variant of type_leq, which implements an optimization to erase the bodies of ghost functions. @@ -356,7 +356,8 @@ let rec eraseTypeDeep unfold_ty (t:mlty) : mlty = | _ -> t let prims_op_equality = with_ty MLTY_Top <| MLE_Name (["Prims"], "op_Equality") -let prims_op_amp_amp = with_ty (mk_ty_fun [("x", ml_bool_ty); ("y", ml_bool_ty)] ml_bool_ty) <| MLE_Name (["Prims"], "op_AmpAmp") +let prims_op_amp_amp = with_ty (mk_ty_fun [{mlbinder_name="x";mlbinder_ty=ml_bool_ty;mlbinder_attrs=[]}; + {mlbinder_name="y";mlbinder_ty=ml_bool_ty;mlbinder_attrs=[]}] ml_bool_ty) <| MLE_Name (["Prims"], "op_AmpAmp") let conjoin e1 e2 = with_ty ml_bool_ty <| MLE_App(prims_op_amp_amp, [e1;e2]) let conjoin_opt e1 e2 = match e1, e2 with | None, None -> None @@ -386,3 +387,14 @@ let rec uncurry_mlty_fun t = let args, res = uncurry_mlty_fun b in a::args, res | _ -> [], t + +let list_elements (e:mlexpr) : option (list mlexpr) = + let rec list_elements acc e = + match e.expr with + | MLE_CTor (([ "Prims" ], "Cons" ), [ hd; tl ]) -> + list_elements (hd :: acc) tl + | MLE_CTor (([ "Prims" ], "Nil" ), []) -> + List.rev acc |> Some + | _ -> None + in + list_elements [] e diff --git a/src/extraction/FStar.Extraction.ML.Util.fsti b/src/extraction/FStar.Extraction.ML.Util.fsti index 30e1572f109..3371e204974 100644 --- a/src/extraction/FStar.Extraction.ML.Util.fsti +++ b/src/extraction/FStar.Extraction.ML.Util.fsti @@ -34,7 +34,7 @@ val eff_leq : f:e_tag -> f':e_tag -> bool val eff_to_string : _arg1:e_tag -> string val join : r:Range.range -> f:e_tag -> f':e_tag -> e_tag val join_l : r:Range.range -> fs:Prims.list e_tag -> e_tag -val mk_ty_fun : (Prims.list (mlident * mlty) -> mlty -> mlty) +val mk_ty_fun : (Prims.list mlbinder -> mlty -> mlty) type unfold_t = mlty -> option mlty val type_leq_c : unfold_ty:unfold_t -> e:option mlexpr -> t:mlty -> t':mlty -> bool * option mlexpr val type_leq : g:unfold_t -> t1:mlty -> t2:mlty -> bool @@ -60,3 +60,5 @@ val mlloc_of_range : r:Range.range -> int * string val doms_and_cod : t:mlty -> list mlty * mlty val argTypes : t:mlty -> list mlty val uncurry_mlty_fun : t:mlty -> list mlty * mlty + +val list_elements : mlexpr -> option (list mlexpr)