From 464a192183432b4c741d3651c6b972c94027d0a7 Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Sat, 17 Feb 2024 13:04:03 +0000 Subject: [PATCH 1/2] attributes with type parameters in ML AST --- src/extraction/FStar.Extraction.Krml.fst | 14 ++++++------ src/extraction/FStar.Extraction.ML.Code.fst | 5 ++++- src/extraction/FStar.Extraction.ML.Modul.fst | 22 ++++++++++++------- ...r.Extraction.ML.RemoveUnusedParameters.fst | 7 +++--- src/extraction/FStar.Extraction.ML.Syntax.fst | 19 +++++++++++----- src/extraction/FStar.Extraction.ML.Term.fst | 13 ++++++----- src/extraction/FStar.Extraction.ML.UEnv.fst | 5 +++-- src/extraction/FStar.Extraction.ML.Util.fst | 2 +- src/extraction/FStar.Extraction.ML.Util.fsti | 2 +- 9 files changed, 55 insertions(+), 34 deletions(-) diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index 5cee9a726c6..4ec2cc33a79 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/src/extraction/FStar.Extraction.Krml.fst @@ -1115,7 +1115,7 @@ let translate_type_decl' env ty: option decl = tydecl_meta=flags; tydecl_defn= Some (MLTD_Abbrev t)} -> let name = env.module_name, name in - let env = List.fold_left (fun env name -> extend_t env name) env args in + let env = List.fold_left (fun env {ty_param_name} -> extend_t env ty_param_name) env args in if assumed && List.mem Syntax.CAbstract flags then Some (DTypeAbstractStruct name) else if assumed then @@ -1131,7 +1131,7 @@ let translate_type_decl' env ty: option decl = tydecl_meta=flags; tydecl_defn=Some (MLTD_Record fields)} -> let name = env.module_name, name in - let env = List.fold_left (fun env name -> extend_t env name) env args in + let env = List.fold_left (fun env {ty_param_name} -> extend_t env ty_param_name) env args in Some (DTypeFlat (name, translate_flags flags, List.length args, List.map (fun (f, t) -> f, (translate_type_without_decay env t, false)) fields)) @@ -1141,7 +1141,7 @@ let translate_type_decl' env ty: option decl = tydecl_defn=Some (MLTD_DType branches)} -> let name = env.module_name, name in let flags = translate_flags flags in - let env = List.fold_left extend_t env args in + let env = args |> ty_param_names |> List.fold_left extend_t env in Some (DTypeVariant (name, flags, List.length args, List.map (fun (cons, ts) -> cons, List.map (fun (name, t) -> name, (translate_type_without_decay env t, false) @@ -1183,7 +1183,7 @@ let translate_let' env flavor lb: option decl = else // Case 1: a possibly-polymorphic function. let env = if flavor = Rec then extend env name else env in - let env = List.fold_left (fun env name -> extend_t env name) env tvars in + let env = tvars |> ty_param_names |> List.fold_left (fun env name -> extend_t env name) env in let rec find_return_type eff i = function | MLTY_Fun (_, eff, t) when i > 0 -> find_return_type eff (i - 1) t @@ -1230,7 +1230,7 @@ let translate_let' env flavor lb: option decl = else // Case 2: this is a global let meta = translate_flags meta in - let env = List.fold_left (fun env name -> extend_t env name) env tvars in + let env = tvars |> ty_param_names |> List.fold_left (fun env name -> extend_t env name) env in let t = translate_type env t in let name = env.module_name, name in begin try @@ -1245,9 +1245,9 @@ let translate_let' env flavor lb: option decl = // TODO JP: figure out what exactly we're hitting here...? Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format1 "Not extracting %s to KaRaMeL\n" name)); begin match ts with - | Some (idents, t) -> + | Some (tps, t) -> BU.print2 "Type scheme is: forall %s. %s\n" - (String.concat ", " idents) + (String.concat ", " (ty_param_names tps)) (ML.Code.string_of_mlty ([], "") t) | None -> () diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index f2a8d6c3aec..03daa7dd6a8 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/src/extraction/FStar.Extraction.ML.Code.fst @@ -629,7 +629,9 @@ and doc_of_lets (currentModule : mlsymbol) (rec_, top_level, lets) = reduce1 [text ":"; ty] | Some (vs, ty) -> let ty = doc_of_mltype currentModule (min_op_prec, NonAssoc) ty in - let vars = vs |> List.map (fun x -> doc_of_mltype currentModule (min_op_prec, NonAssoc) (MLTY_Var x)) |> reduce1 in + let vars = vs |> ty_param_names + |> List.map (fun x -> doc_of_mltype currentModule (min_op_prec, NonAssoc) (MLTY_Var x)) + |> reduce1 in reduce1 [text ":"; vars; text "."; ty] else text "" in reduce1 [text name; reduce1 ids; ty_annot; text "="; e] in @@ -658,6 +660,7 @@ let doc_of_mltydecl (currentModule : mlsymbol) (decls : mltydecl) = | None -> x | Some y -> y in let tparams = + let tparams = ty_param_names tparams in match tparams with | [] -> empty | [x] -> text x diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index a0c51b99fcb..268f03d4817 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -168,16 +168,19 @@ let rec extract_meta x : option meta = let extract_metadata metas = List.choose extract_meta metas -let binders_as_mlty_binders (env:UEnv.uenv) bs = +let binders_as_mlty_binders (env:UEnv.uenv) bs : UEnv.uenv & list ty_param = BU.fold_map - (fun env ({binder_bv=bv}) -> + (fun env ({binder_bv=bv; binder_attrs}) -> let env = UEnv.extend_ty env bv false in - let name = + let ty_param_name = match lookup_bv env bv with | Inl ty -> ty.ty_b_name | _ -> failwith "Impossible" in - env, name) + let ty_param_attrs = + List.map (fun attr -> let e, _, _ = Term.term_as_mlexpr env attr in e) binder_attrs + in + env, {ty_param_name; ty_param_attrs}) env bs (*******************************************************************************) @@ -449,7 +452,7 @@ let extract_let_rec_type env quals attrs lb let extract_bundle_iface env se : env_t * iface = let extract_ctor (env_iparams:env_t) - (ml_tyvars:list mlsymbol) + (ml_tyvars:list ty_param) (env:env_t) (ctor: data_constructor) : env_t * (fv * exp_binding) = @@ -586,7 +589,7 @@ let extract_reifiable_effect g ed BU.print1 "Extracted action term: %s\n" (Code.string_of_mlexpr a_nm a_let); if Env.debug (tcenv_of_uenv g) <| Options.Other "ExtractionReify" then begin BU.print1 "Extracted action type: %s\n" (Code.string_of_mlty a_nm (snd tysc)); - List.iter (fun x -> BU.print1 "and binders: %s\n" x) (fst tysc) end; + List.iter (fun x -> BU.print1 "and binders: %s\n" x) (ty_param_names (fst tysc)) end; let iface, impl = extend_iface a_lid a_nm exp exp_b in g, (iface, impl) in @@ -900,7 +903,7 @@ let extract_iface (g:env_t) modul = let extract_bundle env se = let extract_ctor (env_iparams:env_t) - (ml_tyvars:list mlsymbol) + (ml_tyvars:list ty_param) (env:env_t) (ctor: data_constructor): env_t * (mlsymbol * list (mlsymbol * mlty)) @@ -923,7 +926,10 @@ let extract_bundle env se = let env_iparams, vars = binders_as_mlty_binders env ind.iparams in let env, ctors = ind.idatas |> BU.fold_map (extract_ctor env_iparams vars) env in let indices, _ = U.arrow_formals ind.ityp in - let ml_params = List.append vars (indices |> List.mapi (fun i _ -> "'dummyV" ^ BU.string_of_int i)) in + let ml_params = List.append vars (indices |> List.mapi (fun i _ -> { + ty_param_name = "'dummyV" ^ BU.string_of_int i; + ty_param_attrs = [] + })) in let tbody, env = match BU.find_opt (function RecordType _ -> true | _ -> false) ind.iquals with | Some (RecordType (ns, ids)) -> diff --git a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst index d30fb091753..a157982cb1f 100644 --- a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst +++ b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst @@ -204,7 +204,8 @@ let elim_tydef (env:env_t) name metadata parameters mlty let freevars = freevars_of_mlty mlty in let _, parameters, entry = List.fold_left - (fun (i, params, entry) p -> + (fun (i, params, entry) param -> + let p = param.ty_param_name in if Set.mem p freevars then begin if must_eliminate i @@ -215,7 +216,7 @@ let elim_tydef (env:env_t) name metadata parameters mlty "Expected parameter %s of %s to be unused in its definition and eliminated" p name) end; - i+1, p::params, Retain::entry + i+1, param::params, Retain::entry end else begin if can_eliminate i //there's no val @@ -240,7 +241,7 @@ let elim_tydef (env:env_t) name metadata parameters mlty name (string_of_int i)); raise Drop_tydef - else i+1, p::params, Retain::entry + else i+1, param::params, Retain::entry end) (0, [], []) parameters diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index 15af6d1ef48..39746931632 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/src/extraction/FStar.Extraction.ML.Syntax.fst @@ -96,8 +96,6 @@ type mlty = | MLTY_Top (* \mathbb{T} type in the thesis, to be used when OCaml is not expressive enough for the source type *) | MLTY_Erased //a type that extracts to unit -type mltyscheme = mlidents * mlty //forall a1..an. t (the list of binders can be empty) - type mlconstant = | MLC_Unit | MLC_Bool of bool @@ -202,6 +200,13 @@ and mlletbinding = mlletflavor * list mllb and mlattribute = mlexpr +and ty_param = { + ty_param_name : mlident; + ty_param_attrs : list mlattribute; +} + +and mltyscheme = list ty_param * mlty //forall a1..an. t (the list of binders can be empty) + type mltybody = | MLTD_Abbrev of mlty | MLTD_Record of list (mlsymbol * mlty) @@ -210,12 +215,11 @@ type mltybody = One could have instead used a mlty and tupled the argument types? *) - type one_mltydecl = { tydecl_assumed : bool; // bool: this was assumed (C backend) tydecl_name : mlsymbol; tydecl_ignored : option mlsymbol; - tydecl_parameters : mlidents; + tydecl_parameters : list ty_param; tydecl_meta : metadata; tydecl_defn : option mltybody } @@ -271,6 +275,9 @@ let apply_obj_repr : mlexpr -> mlty -> mlexpr = fun x t -> let obj_repr = with_ty (MLTY_Fun(t, E_PURE, MLTY_Top)) repr_name in with_ty_loc MLTY_Top (MLE_App(obj_repr, [x])) x.loc +let ty_param_names (tys:list ty_param) = + tys |> List.map (fun {ty_param_name} -> ty_param_name) + open FStar.Syntax.Syntax let push_unit (ts : mltyscheme) : mltyscheme = @@ -304,7 +311,7 @@ let rec mlty_to_string (t:mlty) = let mltyscheme_to_string (tsc:mltyscheme) = BU.format2 "( [%s], %s)" - (String.concat ", " (fst tsc)) + (String.concat ", " (tsc |> fst |> ty_param_names)) (mlty_to_string (snd tsc)) let rec mlexpr_to_string (e:mlexpr) = @@ -404,7 +411,7 @@ let mltybody_to_string (d:mltybody) : string = let one_mltydecl_to_string (d:one_mltydecl) : string = BU.format3 "{tydecl_name = %s; tydecl_parameters = %s; tydecl_defn = %s}" d.tydecl_name - (String.concat "," d.tydecl_parameters) + (String.concat "," (d.tydecl_parameters |> ty_param_names)) (match d.tydecl_defn with | None -> "" | Some d -> mltybody_to_string d) diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index cb67c4fe15a..94d8ea9d2ae 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/src/extraction/FStar.Extraction.ML.Term.fst @@ -1203,7 +1203,7 @@ let maybe_promote_effect ml_e tag t = | _ -> ml_e, tag -let extract_lb_sig (g:uenv) (lbs:letbindings) = +let rec extract_lb_sig (g:uenv) (lbs:letbindings) = let maybe_generalize {lbname=lbname_; lbeff=lbeff; lbtyp=lbtyp; lbdef=lbdef; lbattrs=lbattrs} : lbname //just lbname returned back * e_tag //the ML version of the effect label lbeff @@ -1252,6 +1252,9 @@ let extract_lb_sig (g:uenv) (lbs:letbindings) = let n_tbinders = List.length tbinders in let lbdef = normalize_abs lbdef |> U.unmeta in + let tbinders_as_ty_params env = List.map (fun ({binder_bv=x; binder_attrs}) -> { + ty_param_name = (UEnv.lookup_ty env x).ty_b_name; + ty_param_attrs = List.map (fun attr -> let e, _, _ = term_as_mlexpr g attr in e) binder_attrs}) in begin match lbdef.n with | Tm_abs {bs; body; rc_opt=copt} -> let bs, body = SS.open_term bs body in @@ -1262,7 +1265,7 @@ let extract_lb_sig (g:uenv) (lbs:letbindings) = SS.subst s tbody in let env = List.fold_left (fun env ({binder_bv=a}) -> UEnv.extend_ty env a false) g targs in let expected_t = term_as_mlty env expected_source_ty in - let polytype = targs |> List.map (fun ({binder_bv=x}) -> (UEnv.lookup_ty env x).ty_b_name), expected_t in + let polytype = tbinders_as_ty_params env targs, expected_t in let add_unit = match rest_args with | [] -> @@ -1289,7 +1292,7 @@ let extract_lb_sig (g:uenv) (lbs:letbindings) = | Tm_name _ -> let env = List.fold_left (fun env ({binder_bv=a}) -> UEnv.extend_ty env a false) g tbinders in let expected_t = term_as_mlty env tbody in - let polytype = tbinders |> List.map (fun ({binder_bv=x}) -> (UEnv.lookup_ty env x).ty_b_name), expected_t in + let polytype = tbinders_as_ty_params env tbinders, expected_t in //In this case, an eta expansion is safe let args = tbinders |> List.map (fun ({binder_bv=bv}) -> S.bv_to_name bv |> as_arg) in let e = mk (Tm_app {hd=lbdef; args}) lbdef.pos in @@ -1315,7 +1318,7 @@ let extract_lb_sig (g:uenv) (lbs:letbindings) = in snd lbs |> List.map maybe_generalize -let extract_lb_iface (g:uenv) (lbs:letbindings) +and extract_lb_iface (g:uenv) (lbs:letbindings) : uenv * list (fv * exp_binding) = let is_top = FStar.Syntax.Syntax.is_top_level (snd lbs) in let is_rec = not is_top && fst lbs in @@ -1329,7 +1332,7 @@ let extract_lb_iface (g:uenv) (lbs:letbindings) lbs //The main extraction function -let rec check_term_as_mlexpr (g:uenv) (e:term) (f:e_tag) (ty:mlty) : (mlexpr * mlty) = +and check_term_as_mlexpr (g:uenv) (e:term) (f:e_tag) (ty:mlty) : (mlexpr * mlty) = debug g (fun () -> BU.print3 "Checking %s at type %s and eff %s\n" (Print.term_to_string e) diff --git a/src/extraction/FStar.Extraction.ML.UEnv.fst b/src/extraction/FStar.Extraction.ML.UEnv.fst index 2a9b6060b8d..1121edc0916 100644 --- a/src/extraction/FStar.Extraction.ML.UEnv.fst +++ b/src/extraction/FStar.Extraction.ML.UEnv.fst @@ -484,7 +484,7 @@ let extend_fv (g:uenv) (x:fv) (t_x:mltyscheme) (add_unit:bool) | [] -> true in let tySchemeIsClosed (tys : mltyscheme) : bool = - subsetMlidents (mltyFvars (snd tys)) (fst tys) + subsetMlidents (mltyFvars (snd tys)) (tys |> fst |> ty_param_names) in if tySchemeIsClosed t_x then @@ -631,7 +631,8 @@ let new_uenv (e:TypeChecker.Env.env) (* We handle [failwith] specially, extracting it to OCaml's 'failwith' rather than FStar.Compiler.Effect.failwith. Not sure this is necessary *) let a = "'a" in - let failwith_ty = ([a], MLTY_Fun(MLTY_Named([], (["Prims"], "string")), E_IMPURE, MLTY_Var a)) in + let failwith_ty = ([{ty_param_name=a; ty_param_attrs=[]}], + MLTY_Fun(MLTY_Named([], (["Prims"], "string")), E_IMPURE, MLTY_Var a)) in let g, _, _ = extend_lb env (Inr (lid_as_fv (Const.failwith_lid()) None)) tun failwith_ty false in diff --git a/src/extraction/FStar.Extraction.ML.Util.fst b/src/extraction/FStar.Extraction.ML.Util.fst index 6b9a6fa4fc4..d1de2a05164 100644 --- a/src/extraction/FStar.Extraction.ML.Util.fst +++ b/src/extraction/FStar.Extraction.ML.Util.fst @@ -128,7 +128,7 @@ let rec subst_aux (subst:list (mlident * mlty)) (t:mlty) : mlty = let try_subst ((formals, t):mltyscheme) (args:list mlty) : option mlty = if List.length formals <> List.length args then None - else Some (subst_aux (List.zip formals args) t) + else Some (subst_aux (List.zip (ty_param_names formals) args) t) let subst ts args = match try_subst ts args with diff --git a/src/extraction/FStar.Extraction.ML.Util.fsti b/src/extraction/FStar.Extraction.ML.Util.fsti index 3371e204974..f911fd492e5 100644 --- a/src/extraction/FStar.Extraction.ML.Util.fsti +++ b/src/extraction/FStar.Extraction.ML.Util.fsti @@ -28,7 +28,7 @@ val mk_range_mle : mlexpr val mlconst_of_const : p:Range.range -> c:Const.sconst -> mlconstant val mlexpr_of_const : p:Range.range -> c:Const.sconst -> mlexpr' val mlexpr_of_range : r:Range.range -> mlexpr' -val subst : mlidents * mlty -> args:list mlty -> mlty +val subst : list ty_param * mlty -> args:list mlty -> mlty val udelta_unfold : g:UEnv.uenv -> _arg1:mlty -> option mlty val eff_leq : f:e_tag -> f':e_tag -> bool val eff_to_string : _arg1:e_tag -> string From 0cefa352c18b1eb86934de225778d1d989fa0b42 Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Sat, 17 Feb 2024 13:04:07 +0000 Subject: [PATCH 2/2] snap --- .../fstar-lib/FStar_Extraction_ML_PrintML.ml | 4 +- .../generated/FStar_Extraction_Krml.ml | 39 ++++-- .../generated/FStar_Extraction_ML_Code.ml | 11 +- .../generated/FStar_Extraction_ML_Modul.ml | 49 +++++--- ...ar_Extraction_ML_RemoveUnusedParameters.ml | 18 +-- .../generated/FStar_Extraction_ML_Syntax.ml | 43 +++++-- .../generated/FStar_Extraction_ML_Term.ml | 112 ++++++------------ .../generated/FStar_Extraction_ML_UEnv.ml | 10 +- .../generated/FStar_Extraction_ML_Util.ml | 8 +- 9 files changed, 169 insertions(+), 125 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml index 8160729975b..100564959f6 100644 --- a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml +++ b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml @@ -391,7 +391,7 @@ and build_binding (toplevel: bool) (lb: mllb): value_binding = | None -> None | Some ts -> if lb.print_typ && toplevel - then let vars = List.map mk1 (fst ts) in + then let vars = List.map mk1 (ty_param_names (fst ts)) in let ty = snd ts in Some (build_core_type ~annots:vars ty) else None @@ -460,7 +460,7 @@ let build_one_tydecl ({tydecl_name=x; let ptype_name = match mangle_opt with | Some y -> mk_sym y | None -> mk_sym x in - let ptype_params = Some (map (fun sym -> Typ.mk (Ptyp_var (mk_typ_name sym)), (NoVariance, NoInjectivity)) tparams) in + let ptype_params = Some (map (fun sym -> Typ.mk (Ptyp_var (mk_typ_name sym)), (NoVariance, NoInjectivity)) (ty_param_names tparams)) in let (ptype_manifest: core_type option) = BatOption.map_default build_ty_manifest None body |> add_deriving_const attrs in let ptype_kind = Some (BatOption.map_default build_ty_kind Ptype_abstract body) in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index e61e613d5dc..2283c9c9090 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -2729,7 +2729,14 @@ let (translate_type_decl' : let name2 = ((env1.module_name), name1) in let env2 = FStar_Compiler_List.fold_left - (fun env3 -> fun name3 -> extend_t env3 name3) env1 args in + (fun env3 -> + fun uu___1 -> + match uu___1 with + | { + FStar_Extraction_ML_Syntax.ty_param_name = + ty_param_name; + FStar_Extraction_ML_Syntax.ty_param_attrs = uu___2;_} + -> extend_t env3 ty_param_name) env1 args in if assumed && (FStar_Compiler_List.mem FStar_Extraction_ML_Syntax.CAbstract @@ -2763,7 +2770,14 @@ let (translate_type_decl' : let name2 = ((env1.module_name), name1) in let env2 = FStar_Compiler_List.fold_left - (fun env3 -> fun name3 -> extend_t env3 name3) env1 args in + (fun env3 -> + fun uu___2 -> + match uu___2 with + | { + FStar_Extraction_ML_Syntax.ty_param_name = + ty_param_name; + FStar_Extraction_ML_Syntax.ty_param_attrs = uu___3;_} + -> extend_t env3 ty_param_name) env1 args in let uu___2 = let uu___3 = let uu___4 = translate_flags flags in @@ -2790,7 +2804,9 @@ let (translate_type_decl' : -> let name2 = ((env1.module_name), name1) in let flags1 = translate_flags flags in - let env2 = FStar_Compiler_List.fold_left extend_t env1 args in + let env2 = + let uu___2 = FStar_Extraction_ML_Syntax.ty_param_names args in + FStar_Compiler_List.fold_left extend_t env1 uu___2 in let uu___2 = let uu___3 = let uu___4 = @@ -2903,8 +2919,9 @@ let (translate_let' : then extend env1 name1 else env1 in let env3 = + let uu___6 = FStar_Extraction_ML_Syntax.ty_param_names tvars in FStar_Compiler_List.fold_left - (fun env4 -> fun name2 -> extend_t env4 name2) env2 tvars in + (fun env4 -> fun name2 -> extend_t env4 name2) env2 uu___6 in let rec find_return_type eff i uu___6 = match uu___6 with | FStar_Extraction_ML_Syntax.MLTY_Fun (uu___7, eff1, t) when @@ -2987,8 +3004,9 @@ let (translate_let' : else (let meta1 = translate_flags meta in let env2 = + let uu___4 = FStar_Extraction_ML_Syntax.ty_param_names tvars in FStar_Compiler_List.fold_left - (fun env3 -> fun name2 -> extend_t env3 name2) env1 tvars in + (fun env3 -> fun name2 -> extend_t env3 name2) env1 uu___4 in let t1 = translate_type env2 t in let name2 = ((env2.module_name), name1) in try @@ -3034,12 +3052,15 @@ let (translate_let' : FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange uu___6); (match ts with - | FStar_Pervasives_Native.Some (idents, t) -> + | FStar_Pervasives_Native.Some (tps, t) -> let uu___7 = + let uu___8 = + FStar_Extraction_ML_Syntax.ty_param_names tps in + FStar_Compiler_String.concat ", " uu___8 in + let uu___8 = 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___7 + "Type scheme is: forall %s. %s\n" uu___7 uu___8 | FStar_Pervasives_Native.None -> ()); FStar_Pervasives_Native.None) type translate_let_t = @@ -3135,7 +3156,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___1700 : unit) = +let (uu___1702 : 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 9b4402a382c..a938e50496b 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml @@ -1071,12 +1071,15 @@ and (doc_of_lets : (min_op_prec, NonAssoc) ty in let vars = let uu___8 = + let uu___9 = + FStar_Extraction_ML_Syntax.ty_param_names + vs in FStar_Compiler_List.map (fun x -> doc_of_mltype currentModule (min_op_prec, NonAssoc) (FStar_Extraction_ML_Syntax.MLTY_Var - x)) vs in + x)) uu___9 in reduce1 uu___8 in reduce1 [text ":"; vars; text "."; ty1]) else text "") in @@ -1136,12 +1139,14 @@ let (doc_of_mltydecl : | FStar_Pervasives_Native.None -> x | FStar_Pervasives_Native.Some y -> y in let tparams1 = - match tparams with + let tparams2 = + FStar_Extraction_ML_Syntax.ty_param_names tparams in + match tparams2 with | [] -> empty | x2::[] -> text x2 | uu___3 -> let doc1 = - FStar_Compiler_List.map (fun x2 -> text x2) tparams in + FStar_Compiler_List.map (fun x2 -> text x2) tparams2 in let uu___4 = combine (text ", ") doc1 in parens uu___4 in let forbody body1 = match body1 with diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index 73c3809197d..58dcb7cf5c0 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -325,7 +325,7 @@ let (extract_metadata : let (binders_as_mlty_binders : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.binder Prims.list -> - (FStar_Extraction_ML_UEnv.uenv * FStar_Extraction_ML_Syntax.mlident + (FStar_Extraction_ML_UEnv.uenv * FStar_Extraction_ML_Syntax.ty_param Prims.list)) = fun env -> @@ -337,15 +337,27 @@ let (binders_as_mlty_binders : | { FStar_Syntax_Syntax.binder_bv = bv; FStar_Syntax_Syntax.binder_qual = uu___1; FStar_Syntax_Syntax.binder_positivity = uu___2; - FStar_Syntax_Syntax.binder_attrs = uu___3;_} -> + FStar_Syntax_Syntax.binder_attrs = binder_attrs;_} -> let env2 = FStar_Extraction_ML_UEnv.extend_ty env1 bv false in - let name = - let uu___4 = FStar_Extraction_ML_UEnv.lookup_bv env2 bv in - match uu___4 with + let ty_param_name = + let uu___3 = FStar_Extraction_ML_UEnv.lookup_bv env2 bv in + match uu___3 with | FStar_Pervasives.Inl ty -> ty.FStar_Extraction_ML_UEnv.ty_b_name - | uu___5 -> FStar_Compiler_Effect.failwith "Impossible" in - (env2, name)) env bs + | uu___4 -> FStar_Compiler_Effect.failwith "Impossible" in + let ty_param_attrs = + FStar_Compiler_List.map + (fun attr -> + let uu___3 = + FStar_Extraction_ML_Term.term_as_mlexpr env2 attr in + match uu___3 with | (e, uu___4, uu___5) -> e) + binder_attrs in + (env2, + { + FStar_Extraction_ML_Syntax.ty_param_name = ty_param_name; + FStar_Extraction_ML_Syntax.ty_param_attrs = + ty_param_attrs + })) env bs type data_constructor = { dname: FStar_Ident.lident ; @@ -1290,11 +1302,13 @@ let (extract_reifiable_effect : (FStar_Pervasives_Native.snd tysc) in FStar_Compiler_Util.print1 "Extracted action type: %s\n" uu___9); - FStar_Compiler_List.iter - (fun x -> - FStar_Compiler_Util.print1 - "and binders: %s\n" x) - (FStar_Pervasives_Native.fst tysc)) + (let uu___9 = + FStar_Extraction_ML_Syntax.ty_param_names + (FStar_Pervasives_Native.fst tysc) in + FStar_Compiler_List.iter + (fun x -> + FStar_Compiler_Util.print1 + "and binders: %s\n" x) uu___9)) else ()); (let uu___7 = extend_iface a_lid a_nm exp exp_b in match uu___7 with @@ -1968,8 +1982,15 @@ let (extract_bundle : (fun i -> fun uu___5 -> let uu___6 = - FStar_Compiler_Util.string_of_int i in - Prims.strcat "'dummyV" uu___6) indices in + let uu___7 = + FStar_Compiler_Util.string_of_int i in + Prims.strcat "'dummyV" uu___7 in + { + FStar_Extraction_ML_Syntax.ty_param_name = + uu___6; + FStar_Extraction_ML_Syntax.ty_param_attrs + = [] + }) indices in FStar_Compiler_List.append vars uu___4 in let uu___4 = let uu___5 = diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml index 97d2d331e5c..543896ed1d2 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml @@ -273,10 +273,10 @@ let (elim_tydef : env_t -> Prims.string -> FStar_Extraction_ML_Syntax.meta Prims.list -> - Prims.string Prims.list -> + FStar_Extraction_ML_Syntax.ty_param Prims.list -> FStar_Extraction_ML_Syntax.mlty -> (env_t * (Prims.string * FStar_Extraction_ML_Syntax.meta - Prims.list * Prims.string Prims.list * + Prims.list * FStar_Extraction_ML_Syntax.ty_param Prims.list * FStar_Extraction_ML_Syntax.mlty))) = fun env -> @@ -321,9 +321,11 @@ let (elim_tydef : let uu___ = FStar_Compiler_List.fold_left (fun uu___1 -> - fun p -> + fun param -> match uu___1 with | (i, params, entry1) -> + let p = + param.FStar_Extraction_ML_Syntax.ty_param_name in let uu___2 = FStar_Compiler_Set.mem FStar_Class_Ord.ord_string p freevars in @@ -340,8 +342,8 @@ let (elim_tydef : uu___5) in FStar_Errors.log_issue range_of_tydef uu___4) else (); - ((i + Prims.int_one), (p :: params), (Retain :: - entry1))) + ((i + Prims.int_one), (param :: params), (Retain + :: entry1))) else if (can_eliminate i) || (must_eliminate i) then @@ -372,9 +374,9 @@ let (elim_tydef : FStar_Errors.log_issue range uu___7); FStar_Compiler_Effect.raise Drop_tydef) else - ((i + Prims.int_one), (p :: params), (Retain - :: entry1)))) (Prims.int_zero, [], []) - parameters in + ((i + Prims.int_one), (param :: params), + (Retain :: entry1)))) + (Prims.int_zero, [], []) parameters in match uu___ with | (uu___1, parameters1, entry1) -> let uu___2 = diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index 5837b1ac859..4cea14c5875 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -215,7 +215,6 @@ let (uu___is_MLTY_Top : mlty -> Prims.bool) = let (uu___is_MLTY_Erased : mlty -> Prims.bool) = fun projectee -> match projectee with | MLTY_Erased -> true | uu___ -> false -type mltyscheme = (mlidents * mlty) type mlconstant = | MLC_Unit | MLC_Bool of Prims.bool @@ -448,12 +447,15 @@ and mlexpr = { and mllb = { mllb_name: mlident ; - mllb_tysc: mltyscheme FStar_Pervasives_Native.option ; + mllb_tysc: (ty_param Prims.list * mlty) FStar_Pervasives_Native.option ; mllb_add_unit: Prims.bool ; mllb_def: mlexpr ; mllb_attrs: mlexpr Prims.list ; mllb_meta: metadata ; print_typ: Prims.bool } +and ty_param = { + ty_param_name: mlident ; + ty_param_attrs: mlexpr Prims.list } let (__proj__Mkmlbinder__item__mlbinder_name : mlbinder -> mlident) = fun projectee -> match projectee with @@ -569,7 +571,7 @@ let (__proj__Mkmllb__item__mllb_name : mllb -> mlident) = | { 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) = + mllb -> (ty_param Prims.list * mlty) FStar_Pervasives_Native.option) = fun projectee -> match projectee with | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; @@ -599,9 +601,19 @@ let (__proj__Mkmllb__item__print_typ : mllb -> Prims.bool) = match projectee with | { mllb_name; mllb_tysc; mllb_add_unit; mllb_def; mllb_attrs; mllb_meta; print_typ;_} -> print_typ +let (__proj__Mkty_param__item__ty_param_name : ty_param -> mlident) = + fun projectee -> + match projectee with + | { ty_param_name; ty_param_attrs;_} -> ty_param_name +let (__proj__Mkty_param__item__ty_param_attrs : + ty_param -> mlexpr Prims.list) = + fun projectee -> + match projectee with + | { ty_param_name; ty_param_attrs;_} -> ty_param_attrs type mlbranch = (mlpattern * mlexpr FStar_Pervasives_Native.option * mlexpr) type mlletbinding = (mlletflavor * mllb Prims.list) type mlattribute = mlexpr +type mltyscheme = (ty_param Prims.list * mlty) type mltybody = | MLTD_Abbrev of mlty | MLTD_Record of (mlsymbol * mlty) Prims.list @@ -628,7 +640,7 @@ type one_mltydecl = tydecl_assumed: Prims.bool ; tydecl_name: mlsymbol ; tydecl_ignored: mlsymbol FStar_Pervasives_Native.option ; - tydecl_parameters: mlidents ; + tydecl_parameters: ty_param Prims.list ; tydecl_meta: metadata ; tydecl_defn: mltybody FStar_Pervasives_Native.option } let (__proj__Mkone_mltydecl__item__tydecl_assumed : @@ -649,7 +661,7 @@ let (__proj__Mkone_mltydecl__item__tydecl_ignored : | { tydecl_assumed; tydecl_name; tydecl_ignored; tydecl_parameters; tydecl_meta; tydecl_defn;_} -> tydecl_ignored let (__proj__Mkone_mltydecl__item__tydecl_parameters : - one_mltydecl -> mlidents) = + one_mltydecl -> ty_param Prims.list) = fun projectee -> match projectee with | { tydecl_assumed; tydecl_name; tydecl_ignored; tydecl_parameters; @@ -763,6 +775,12 @@ let (apply_obj_repr : mlexpr -> mlty -> mlexpr) = if uu___ then MLE_Name ([], "box") else MLE_Name (["Obj"], "repr") in let obj_repr = with_ty (MLTY_Fun (t, E_PURE, MLTY_Top)) repr_name in with_ty_loc MLTY_Top (MLE_App (obj_repr, [x])) x.loc +let (ty_param_names : ty_param Prims.list -> mlident Prims.list) = + fun tys -> + FStar_Compiler_List.map + (fun uu___ -> + match uu___ with + | { ty_param_name; ty_param_attrs = uu___1;_} -> ty_param_name) tys let (push_unit : mltyscheme -> mltyscheme) = fun ts -> let uu___ = ts in @@ -811,10 +829,11 @@ let rec (mlty_to_string : mlty -> Prims.string) = | MLTY_Erased -> "MLTY_Erased" let (mltyscheme_to_string : mltyscheme -> Prims.string) = fun tsc -> - let uu___ = mlty_to_string (FStar_Pervasives_Native.snd tsc) in - FStar_Compiler_Util.format2 "( [%s], %s)" - (FStar_Compiler_String.concat ", " (FStar_Pervasives_Native.fst tsc)) - uu___ + let uu___ = + let uu___1 = ty_param_names (FStar_Pervasives_Native.fst tsc) in + FStar_Compiler_String.concat ", " uu___1 in + let uu___1 = mlty_to_string (FStar_Pervasives_Native.snd tsc) in + FStar_Compiler_Util.format2 "( [%s], %s)" uu___ uu___1 let rec (mlexpr_to_string : mlexpr -> Prims.string) = fun e -> match e.expr with @@ -1055,13 +1074,15 @@ let (mltybody_to_string : mltybody -> Prims.string) = let (one_mltydecl_to_string : one_mltydecl -> Prims.string) = fun d -> let uu___ = + let uu___1 = ty_param_names d.tydecl_parameters in + FStar_Compiler_String.concat "," uu___1 in + let uu___1 = match d.tydecl_defn with | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some d1 -> mltybody_to_string d1 in FStar_Compiler_Util.format3 "{tydecl_name = %s; tydecl_parameters = %s; tydecl_defn = %s}" - d.tydecl_name (FStar_Compiler_String.concat "," d.tydecl_parameters) - uu___ + d.tydecl_name uu___ uu___1 let (mlmodule1_to_string : mlmodule1 -> Prims.string) = fun m -> match m.mlmodule1_m with diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 5c91fa3ca93..b7897c1c3fd 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -2171,7 +2171,7 @@ let (maybe_promote_effect : (FStar_Extraction_ML_Syntax.ml_unit, FStar_Extraction_ML_Syntax.E_PURE) | uu___ -> (ml_e, tag) -let (extract_lb_sig : +let rec (extract_lb_sig : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.letbindings -> (FStar_Syntax_Syntax.lbname * FStar_Extraction_ML_Syntax.e_tag * @@ -2234,6 +2234,37 @@ let (extract_lb_sig : let lbdef1 = let uu___7 = normalize_abs lbdef in FStar_Syntax_Util.unmeta uu___7 in + let tbinders_as_ty_params env = + FStar_Compiler_List.map + (fun uu___7 -> + match uu___7 with + | { FStar_Syntax_Syntax.binder_bv = x; + FStar_Syntax_Syntax.binder_qual = + uu___8; + FStar_Syntax_Syntax.binder_positivity + = uu___9; + FStar_Syntax_Syntax.binder_attrs = + binder_attrs;_} + -> + let uu___10 = + let uu___11 = + FStar_Extraction_ML_UEnv.lookup_ty + env x in + uu___11.FStar_Extraction_ML_UEnv.ty_b_name in + let uu___11 = + FStar_Compiler_List.map + (fun attr -> + let uu___12 = + term_as_mlexpr g attr in + match uu___12 with + | (e, uu___13, uu___14) -> e) + binder_attrs in + { + FStar_Extraction_ML_Syntax.ty_param_name + = uu___10; + FStar_Extraction_ML_Syntax.ty_param_attrs + = uu___11 + }) in (match lbdef1.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = bs2; @@ -2313,23 +2344,7 @@ let (extract_lb_sig : expected_source_ty in let polytype = let uu___9 = - FStar_Compiler_List.map - (fun uu___10 -> - match uu___10 with - | { - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___11; - FStar_Syntax_Syntax.binder_positivity - = uu___12; - FStar_Syntax_Syntax.binder_attrs - = uu___13;_} - -> - let uu___14 = - FStar_Extraction_ML_UEnv.lookup_ty - env x in - uu___14.FStar_Extraction_ML_UEnv.ty_b_name) + tbinders_as_ty_params env targs in (uu___9, expected_t) in let add_unit = @@ -2387,24 +2402,7 @@ let (extract_lb_sig : let expected_t = term_as_mlty env tbody in let polytype = let uu___8 = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Extraction_ML_UEnv.lookup_ty - env x in - uu___13.FStar_Extraction_ML_UEnv.ty_b_name) - tbinders in + tbinders_as_ty_params env tbinders in (uu___8, expected_t) in let args = FStar_Compiler_List.map @@ -2455,24 +2453,7 @@ let (extract_lb_sig : let expected_t = term_as_mlty env tbody in let polytype = let uu___8 = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Extraction_ML_UEnv.lookup_ty - env x in - uu___13.FStar_Extraction_ML_UEnv.ty_b_name) - tbinders in + tbinders_as_ty_params env tbinders in (uu___8, expected_t) in let args = FStar_Compiler_List.map @@ -2523,24 +2504,7 @@ let (extract_lb_sig : let expected_t = term_as_mlty env tbody in let polytype = let uu___8 = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Extraction_ML_UEnv.lookup_ty - env x in - uu___13.FStar_Extraction_ML_UEnv.ty_b_name) - tbinders in + tbinders_as_ty_params env tbinders in (uu___8, expected_t) in let args = FStar_Compiler_List.map @@ -2574,7 +2538,7 @@ let (extract_lb_sig : | uu___5 -> no_gen ()) in FStar_Compiler_List.map maybe_generalize (FStar_Pervasives_Native.snd lbs) -let (extract_lb_iface : +and (extract_lb_iface : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.letbindings -> (FStar_Extraction_ML_UEnv.uenv * (FStar_Syntax_Syntax.fv * @@ -2602,7 +2566,7 @@ let (extract_lb_iface : let uu___4 = FStar_Compiler_Util.right lbname in (uu___4, exp_binding) in (env1, uu___3))) g lbs1 -let rec (check_term_as_mlexpr : +and (check_term_as_mlexpr : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> FStar_Extraction_ML_Syntax.e_tag -> diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml index 7848a2aa53e..dfdc829a9d2 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml @@ -819,7 +819,10 @@ let (extend_fv : | [] -> true in let tySchemeIsClosed tys = let uu___ = mltyFvars (FStar_Pervasives_Native.snd tys) in - subsetMlidents uu___ (FStar_Pervasives_Native.fst tys) in + let uu___1 = + FStar_Extraction_ML_Syntax.ty_param_names + (FStar_Pervasives_Native.fst tys) in + subsetMlidents uu___ uu___1 in let uu___ = tySchemeIsClosed t_x in if uu___ then @@ -1137,7 +1140,10 @@ let (new_uenv : FStar_TypeChecker_Env.env -> uenv) = } in let a = "'a" in let failwith_ty = - ([a], + ([{ + FStar_Extraction_ML_Syntax.ty_param_name = a; + FStar_Extraction_ML_Syntax.ty_param_attrs = [] + }], (FStar_Extraction_ML_Syntax.MLTY_Fun ((FStar_Extraction_ML_Syntax.MLTY_Named ([], (["Prims"], "string"))), diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml index 8a9d2fbf160..2cf40d16ba3 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml @@ -186,11 +186,15 @@ let (try_subst : then FStar_Pervasives_Native.None else (let uu___2 = - let uu___3 = FStar_Compiler_List.zip formals args in + let uu___3 = + let uu___4 = + FStar_Extraction_ML_Syntax.ty_param_names formals in + FStar_Compiler_List.zip uu___4 args in subst_aux uu___3 t in FStar_Pervasives_Native.Some uu___2) let (subst : - (FStar_Extraction_ML_Syntax.mlidents * FStar_Extraction_ML_Syntax.mlty) -> + (FStar_Extraction_ML_Syntax.ty_param Prims.list * + FStar_Extraction_ML_Syntax.mlty) -> FStar_Extraction_ML_Syntax.mlty Prims.list -> FStar_Extraction_ML_Syntax.mlty) =