diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml index 544b1527b85..f688a4c826a 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml @@ -446,6 +446,12 @@ let (string_of_mlconstant : | uu___ -> FStar_Compiler_Effect.failwith "TODO: extract integer constants properly into OCaml" +let (string_of_etag : FStar_Extraction_ML_Syntax.e_tag -> Prims.string) = + fun uu___ -> + match uu___ with + | FStar_Extraction_ML_Syntax.E_PURE -> "" + | FStar_Extraction_ML_Syntax.E_ERASABLE -> "Erased" + | FStar_Extraction_ML_Syntax.E_IMPURE -> "Impure" let rec (doc_of_mltype' : FStar_Extraction_ML_Syntax.mlsymbol -> level -> FStar_Extraction_ML_Syntax.mlty -> doc) @@ -485,12 +491,12 @@ let rec (doc_of_mltype' : parens uu___1 in let name1 = ptsym currentModule name in let uu___ = reduce1 [args1; text name1] in hbox uu___ - | FStar_Extraction_ML_Syntax.MLTY_Fun (t1, uu___, t2) -> + | FStar_Extraction_ML_Syntax.MLTY_Fun (t1, et, t2) -> let d1 = doc_of_mltype currentModule (t_prio_fun, Left) t1 in let d2 = doc_of_mltype currentModule (t_prio_fun, Right) t2 in - let uu___1 = - let uu___2 = reduce1 [d1; text " -> "; d2] in hbox uu___2 in - maybe_paren outer t_prio_fun uu___1 + let uu___ = + let uu___1 = reduce1 [d1; text " -> "; d2] in hbox uu___1 in + maybe_paren outer t_prio_fun uu___ | FStar_Extraction_ML_Syntax.MLTY_Top -> let uu___ = FStar_Extraction_ML_Util.codegen_fsharp () in if uu___ then text "obj" else text "Obj.t" @@ -1430,4 +1436,10 @@ let (string_of_mlty : pretty Prims.int_zero doc1 let (showable_mlexpr : FStar_Extraction_ML_Syntax.mlexpr FStar_Class_Show.showable) = - { FStar_Class_Show.show = (string_of_mlexpr ([], "")) } \ No newline at end of file + { FStar_Class_Show.show = (string_of_mlexpr ([], "")) } +let (showable_mlty : + FStar_Extraction_ML_Syntax.mlty FStar_Class_Show.showable) = + { FStar_Class_Show.show = (string_of_mlty ([], "")) } +let (showable_etag : + FStar_Extraction_ML_Syntax.e_tag FStar_Class_Show.showable) = + { FStar_Class_Show.show = string_of_etag } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index 90976fb772b..2fe120d3f45 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -1224,12 +1224,13 @@ let (extract_reifiable_effect : (match uu___2 with | { FStar_Extraction_ML_UEnv.exp_b_name = uu___3; FStar_Extraction_ML_UEnv.exp_b_expr = uu___4; - FStar_Extraction_ML_UEnv.exp_b_tscheme = tysc;_} -> - let uu___5 = + FStar_Extraction_ML_UEnv.exp_b_tscheme = tysc; + FStar_Extraction_ML_UEnv.exp_b_eff = uu___5;_} -> + let uu___6 = FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.MLTY_Top (FStar_Extraction_ML_Syntax.MLE_Name mlp) in - (uu___5, tysc)) + (uu___6, tysc)) | uu___2 -> let uu___3 = let uu___4 = diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index 499e8ad75c4..3d1a2f85e51 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -779,19 +779,20 @@ let (ty_param_names : ty_param Prims.list -> Prims.string Prims.list) = (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 - match uu___ with | (vs, ty) -> (vs, (MLTY_Fun (ml_unit_ty, E_PURE, ty))) -let (pop_unit : mltyscheme -> mltyscheme) = +let (push_unit : e_tag -> mltyscheme -> mltyscheme) = + fun eff -> + fun ts -> + let uu___ = ts in + match uu___ with | (vs, ty) -> (vs, (MLTY_Fun (ml_unit_ty, eff, ty))) +let (pop_unit : mltyscheme -> (e_tag * mltyscheme)) = fun ts -> let uu___ = ts in match uu___ with | (vs, ty) -> (match ty with - | MLTY_Fun (l, E_PURE, t) -> + | MLTY_Fun (l, eff, t) -> if l = ml_unit_ty - then (vs, t) + then (eff, (vs, t)) else FStar_Compiler_Effect.failwith "unexpected: pop_unit: domain was not unit" diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 13ff460f260..d066ced9222 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -723,75 +723,78 @@ let (fresh_binders : let (instantiate_maybe_partial : FStar_Extraction_ML_UEnv.uenv -> FStar_Extraction_ML_Syntax.mlexpr -> - FStar_Extraction_ML_Syntax.mltyscheme -> - FStar_Extraction_ML_Syntax.mlty Prims.list -> - (FStar_Extraction_ML_Syntax.mlexpr * - FStar_Extraction_ML_Syntax.e_tag * - FStar_Extraction_ML_Syntax.mlty)) + FStar_Extraction_ML_Syntax.e_tag -> + FStar_Extraction_ML_Syntax.mltyscheme -> + FStar_Extraction_ML_Syntax.mlty Prims.list -> + (FStar_Extraction_ML_Syntax.mlexpr * + FStar_Extraction_ML_Syntax.e_tag * + FStar_Extraction_ML_Syntax.mlty)) = fun g -> fun e -> - fun s -> - fun tyargs -> - let uu___ = s in - match uu___ with - | (vars, t) -> - let n_vars = FStar_Compiler_List.length vars in - let n_args = FStar_Compiler_List.length tyargs in - if n_args = n_vars - then - (if n_args = Prims.int_zero - then (e, FStar_Extraction_ML_Syntax.E_PURE, t) - else - (let ts = instantiate_tyscheme (vars, t) tyargs in - let tapp = - { - FStar_Extraction_ML_Syntax.expr = - (FStar_Extraction_ML_Syntax.MLE_TApp (e, tyargs)); - FStar_Extraction_ML_Syntax.mlty = ts; - FStar_Extraction_ML_Syntax.loc = - (e.FStar_Extraction_ML_Syntax.loc) - } in - (tapp, FStar_Extraction_ML_Syntax.E_PURE, ts))) - else - if n_args < n_vars + fun eff -> + fun s -> + fun tyargs -> + let uu___ = s in + match uu___ with + | (vars, t) -> + let n_vars = FStar_Compiler_List.length vars in + let n_args = FStar_Compiler_List.length tyargs in + if n_args = n_vars then - (let extra_tyargs = - let uu___2 = FStar_Compiler_Util.first_N n_args vars in - match uu___2 with - | (uu___3, rest_vars) -> - FStar_Compiler_List.map - (fun uu___4 -> - FStar_Extraction_ML_Syntax.MLTY_Erased) - rest_vars in - let tyargs1 = - FStar_Compiler_List.op_At tyargs extra_tyargs in - let ts = instantiate_tyscheme (vars, t) tyargs1 in - let tapp = - { - FStar_Extraction_ML_Syntax.expr = - (FStar_Extraction_ML_Syntax.MLE_TApp (e, tyargs1)); - FStar_Extraction_ML_Syntax.mlty = ts; - FStar_Extraction_ML_Syntax.loc = - (e.FStar_Extraction_ML_Syntax.loc) - } in - let t1 = - FStar_Compiler_List.fold_left - (fun out -> - fun t2 -> - FStar_Extraction_ML_Syntax.MLTY_Fun - (t2, FStar_Extraction_ML_Syntax.E_PURE, out)) - ts extra_tyargs in - let uu___2 = fresh_binders extra_tyargs g in - match uu___2 with - | (vs_ts, g1) -> - let f = - FStar_Extraction_ML_Syntax.with_ty t1 - (FStar_Extraction_ML_Syntax.MLE_Fun (vs_ts, tapp)) in - (f, FStar_Extraction_ML_Syntax.E_PURE, t1)) + (if n_args = Prims.int_zero + then (e, eff, t) + else + (let ts = instantiate_tyscheme (vars, t) tyargs in + let tapp = + { + FStar_Extraction_ML_Syntax.expr = + (FStar_Extraction_ML_Syntax.MLE_TApp (e, tyargs)); + FStar_Extraction_ML_Syntax.mlty = ts; + FStar_Extraction_ML_Syntax.loc = + (e.FStar_Extraction_ML_Syntax.loc) + } in + (tapp, eff, ts))) else - FStar_Compiler_Effect.failwith - "Impossible: instantiate_maybe_partial called with too many arguments" + if n_args < n_vars + then + (let extra_tyargs = + let uu___2 = FStar_Compiler_Util.first_N n_args vars in + match uu___2 with + | (uu___3, rest_vars) -> + FStar_Compiler_List.map + (fun uu___4 -> + FStar_Extraction_ML_Syntax.MLTY_Erased) + rest_vars in + let tyargs1 = + FStar_Compiler_List.op_At tyargs extra_tyargs in + let ts = instantiate_tyscheme (vars, t) tyargs1 in + let tapp = + { + FStar_Extraction_ML_Syntax.expr = + (FStar_Extraction_ML_Syntax.MLE_TApp (e, tyargs1)); + FStar_Extraction_ML_Syntax.mlty = ts; + FStar_Extraction_ML_Syntax.loc = + (e.FStar_Extraction_ML_Syntax.loc) + } in + let t1 = + FStar_Compiler_List.fold_left + (fun out -> + fun t2 -> + FStar_Extraction_ML_Syntax.MLTY_Fun + (t2, FStar_Extraction_ML_Syntax.E_PURE, out)) + ts extra_tyargs in + let uu___2 = fresh_binders extra_tyargs g in + match uu___2 with + | (vs_ts, g1) -> + let f = + FStar_Extraction_ML_Syntax.with_ty t1 + (FStar_Extraction_ML_Syntax.MLE_Fun + (vs_ts, tapp)) in + (f, eff, t1)) + else + FStar_Compiler_Effect.failwith + "Impossible: instantiate_maybe_partial called with too many arguments" let (eta_expand : FStar_Extraction_ML_UEnv.uenv -> FStar_Extraction_ML_Syntax.mlty -> @@ -1720,7 +1723,8 @@ let rec (extract_one_pat : FStar_Extraction_ML_Syntax.MLE_Name n; FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}; - FStar_Extraction_ML_UEnv.exp_b_tscheme = ttys;_} + FStar_Extraction_ML_UEnv.exp_b_tscheme = ttys; + FStar_Extraction_ML_UEnv.exp_b_eff = uu___6;_} -> (n, ttys) | FStar_Pervasives_Native.Some uu___3 -> FStar_Compiler_Effect.failwith "Expected a constructor" @@ -2264,6 +2268,9 @@ let rec (extract_lb_sig : let uu___5 = FStar_Syntax_Subst.open_comp bs c in (match uu___5 with | (bs1, c1) -> + let etag_of_comp c2 = + effect_as_etag g + (FStar_Syntax_Util.comp_effect_name c2) in let uu___6 = let uu___7 = FStar_Compiler_Util.prefix_until @@ -2272,13 +2279,16 @@ let rec (extract_lb_sig : Prims.op_Negation uu___8) bs1 in match uu___7 with | FStar_Pervasives_Native.None -> - (bs1, (FStar_Syntax_Util.comp_result c1)) + let uu___8 = etag_of_comp c1 in + (bs1, uu___8, + (FStar_Syntax_Util.comp_result c1)) | FStar_Pervasives_Native.Some (bs2, b, rest) -> let uu___8 = FStar_Syntax_Util.arrow (b :: rest) c1 in - (bs2, uu___8) in + (bs2, FStar_Extraction_ML_Syntax.E_PURE, + uu___8) in (match uu___6 with - | (tbinders, tbody) -> + | (tbinders, eff_body, tbody) -> let n_tbinders = FStar_Compiler_List.length tbinders in let lbdef1 = @@ -2420,7 +2430,7 @@ let rec (extract_lb_sig : if add_unit then FStar_Extraction_ML_Syntax.push_unit - polytype + eff_body polytype else polytype in let body2 = FStar_Syntax_Util.abs @@ -2655,27 +2665,48 @@ and (check_term_as_mlexpr : let uu___2 = term_as_mlexpr g e in (match uu___2 with | (ml_e, tag, t) -> - let uu___3 = FStar_Extraction_ML_Util.eff_leq tag f in - if uu___3 - then - let uu___4 = - maybe_coerce e.FStar_Syntax_Syntax.pos g ml_e t ty in - (uu___4, ty) - else - (match (tag, f, ty) with - | (FStar_Extraction_ML_Syntax.E_ERASABLE, - FStar_Extraction_ML_Syntax.E_PURE, - FStar_Extraction_ML_Syntax.MLTY_Erased) -> - let uu___5 = - maybe_coerce e.FStar_Syntax_Syntax.pos g ml_e t - ty in - (uu___5, ty) - | uu___5 -> - (err_unexpected_eff g e ty f tag; - (let uu___7 = + (FStar_Extraction_ML_UEnv.debug g + (fun uu___4 -> + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e in + let uu___6 = + let uu___7 = + FStar_Extraction_ML_UEnv.current_module_of_uenv + g in + FStar_Extraction_ML_Code.string_of_mlexpr uu___7 + ml_e in + let uu___7 = + FStar_Extraction_ML_Util.eff_to_string tag in + let uu___8 = + let uu___9 = + FStar_Extraction_ML_UEnv.current_module_of_uenv + g in + FStar_Extraction_ML_Code.string_of_mlty uu___9 t in + FStar_Compiler_Util.print4 + "Extracted %s to %s at eff %s and type %s\n" + uu___5 uu___6 uu___7 uu___8); + (let uu___4 = FStar_Extraction_ML_Util.eff_leq tag f in + if uu___4 + then + let uu___5 = + maybe_coerce e.FStar_Syntax_Syntax.pos g ml_e t ty in + (uu___5, ty) + else + (match (tag, f, ty) with + | (FStar_Extraction_ML_Syntax.E_ERASABLE, + FStar_Extraction_ML_Syntax.E_PURE, + FStar_Extraction_ML_Syntax.MLTY_Erased) -> + let uu___6 = maybe_coerce e.FStar_Syntax_Syntax.pos g ml_e t ty in - (uu___7, ty)))))) + (uu___6, ty) + | uu___6 -> + (err_unexpected_eff g e ty f tag; + (let uu___8 = + maybe_coerce e.FStar_Syntax_Syntax.pos g + ml_e t ty in + (uu___8, ty)))))))) and (term_as_mlexpr : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> @@ -2845,23 +2876,24 @@ and (term_as_mlexpr' : (match uu___2 with | { FStar_Extraction_ML_UEnv.exp_b_name = uu___3; FStar_Extraction_ML_UEnv.exp_b_expr = fw; - FStar_Extraction_ML_UEnv.exp_b_tscheme = uu___4;_} -> - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = - let uu___9 = + FStar_Extraction_ML_UEnv.exp_b_tscheme = uu___4; + FStar_Extraction_ML_UEnv.exp_b_eff = uu___5;_} -> + let uu___6 = + let uu___7 = + let uu___8 = + let uu___9 = + let uu___10 = FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.ml_string_ty (FStar_Extraction_ML_Syntax.MLE_Const (FStar_Extraction_ML_Syntax.MLC_String "Cannot evaluate open quotation at runtime")) in - [uu___9] in - (fw, uu___8) in - FStar_Extraction_ML_Syntax.MLE_App uu___7 in + [uu___10] in + (fw, uu___9) in + FStar_Extraction_ML_Syntax.MLE_App uu___8 in FStar_Extraction_ML_Syntax.with_ty - FStar_Extraction_ML_Syntax.ml_int_ty uu___6 in - (uu___5, FStar_Extraction_ML_Syntax.E_PURE, + FStar_Extraction_ML_Syntax.ml_int_ty uu___7 in + (uu___6, FStar_Extraction_ML_Syntax.E_PURE, FStar_Extraction_ML_Syntax.ml_int_ty)) | FStar_Syntax_Syntax.Tm_quoted (qt, @@ -3035,18 +3067,17 @@ and (term_as_mlexpr' : | (FStar_Pervasives.Inr { FStar_Extraction_ML_UEnv.exp_b_name = uu___5; FStar_Extraction_ML_UEnv.exp_b_expr = x; - FStar_Extraction_ML_UEnv.exp_b_tscheme = mltys;_}, + FStar_Extraction_ML_UEnv.exp_b_tscheme = mltys; + FStar_Extraction_ML_UEnv.exp_b_eff = etag;_}, qual) -> (match mltys with | ([], t1) when t1 = FStar_Extraction_ML_Syntax.ml_unit_ty - -> - (FStar_Extraction_ML_Syntax.ml_unit, - FStar_Extraction_ML_Syntax.E_PURE, t1) + -> (FStar_Extraction_ML_Syntax.ml_unit, etag, t1) | ([], t1) -> let uu___6 = maybe_eta_data_and_project_record g qual t1 x in - (uu___6, FStar_Extraction_ML_Syntax.E_PURE, t1) - | uu___6 -> instantiate_maybe_partial g x mltys [])) + (uu___6, etag, t1) + | uu___6 -> instantiate_maybe_partial g x etag mltys [])) | FStar_Syntax_Syntax.Tm_fvar fv -> let uu___1 = is_type g t in if uu___1 @@ -3066,36 +3097,37 @@ and (term_as_mlexpr' : | FStar_Pervasives_Native.Some { FStar_Extraction_ML_UEnv.exp_b_name = uu___4; FStar_Extraction_ML_UEnv.exp_b_expr = x; - FStar_Extraction_ML_UEnv.exp_b_tscheme = mltys;_} + FStar_Extraction_ML_UEnv.exp_b_tscheme = mltys; + FStar_Extraction_ML_UEnv.exp_b_eff = uu___5;_} -> (FStar_Extraction_ML_UEnv.debug g - (fun uu___6 -> - let uu___7 = + (fun uu___7 -> + let uu___8 = FStar_Class_Show.show FStar_Syntax_Print.showable_fv fv in - let uu___8 = - let uu___9 = - FStar_Extraction_ML_UEnv.current_module_of_uenv g in - FStar_Extraction_ML_Code.string_of_mlexpr uu___9 x in let uu___9 = - let uu___10 = - FStar_Extraction_ML_UEnv.current_module_of_uenv g in - FStar_Extraction_ML_Code.string_of_mlty uu___10 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr x in + let uu___10 = + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd mltys) in FStar_Compiler_Util.print3 - "looked up %s: got %s at %s \n" uu___7 uu___8 - uu___9); + "looked up %s: got %s at %s \n" uu___8 uu___9 + uu___10); (match mltys with | ([], t1) when t1 = FStar_Extraction_ML_Syntax.ml_unit_ty -> (FStar_Extraction_ML_Syntax.ml_unit, FStar_Extraction_ML_Syntax.E_PURE, t1) | ([], t1) -> - let uu___6 = + let uu___7 = maybe_eta_data_and_project_record g fv.FStar_Syntax_Syntax.fv_qual t1 x in - (uu___6, FStar_Extraction_ML_Syntax.E_PURE, t1) - | uu___6 -> instantiate_maybe_partial g x mltys []))) + (uu___7, FStar_Extraction_ML_Syntax.E_PURE, t1) + | uu___7 -> + instantiate_maybe_partial g x + FStar_Extraction_ML_Syntax.E_PURE mltys []))) | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = bs; FStar_Syntax_Syntax.body = body; FStar_Syntax_Syntax.rc_opt = rcopt;_} @@ -3223,23 +3255,24 @@ and (term_as_mlexpr' : (match uu___6 with | { FStar_Extraction_ML_UEnv.exp_b_name = uu___7; FStar_Extraction_ML_UEnv.exp_b_expr = fw; - FStar_Extraction_ML_UEnv.exp_b_tscheme = uu___8;_} -> - let uu___9 = - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = + FStar_Extraction_ML_UEnv.exp_b_tscheme = uu___8; + FStar_Extraction_ML_UEnv.exp_b_eff = uu___9;_} -> + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.ml_string_ty (FStar_Extraction_ML_Syntax.MLE_Const (FStar_Extraction_ML_Syntax.MLC_String "Extraction of reflect is not supported")) in - [uu___13] in - (fw, uu___12) in - FStar_Extraction_ML_Syntax.MLE_App uu___11 in + [uu___14] in + (fw, uu___13) in + FStar_Extraction_ML_Syntax.MLE_App uu___12 in FStar_Extraction_ML_Syntax.with_ty - FStar_Extraction_ML_Syntax.ml_int_ty uu___10 in - (uu___9, FStar_Extraction_ML_Syntax.E_PURE, + FStar_Extraction_ML_Syntax.ml_int_ty uu___11 in + (uu___10, FStar_Extraction_ML_Syntax.E_PURE, FStar_Extraction_ML_Syntax.ml_int_ty)) | FStar_Syntax_Syntax.Tm_app uu___1 when is_steel_with_invariant_g t -> @@ -3515,29 +3548,28 @@ and (term_as_mlexpr' : FStar_Class_Show.show FStar_Syntax_Print.showable_term head1 in let uu___10 = - let uu___11 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlexpr - uu___11 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr exp_b.FStar_Extraction_ML_UEnv.exp_b_expr in let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlty - uu___12 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme) in - FStar_Compiler_Util.print3 - "@@@looked up %s: got %s at %s\n" uu___9 - uu___10 uu___11); + let uu___12 = + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_etag + exp_b.FStar_Extraction_ML_UEnv.exp_b_eff in + FStar_Compiler_Util.print4 + "@@@looked up %s: got %s at %s with eff <%s>\n" + uu___9 uu___10 uu___11 uu___12); (((exp_b.FStar_Extraction_ML_UEnv.exp_b_expr), - (exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme)), + (exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme), + (exp_b.FStar_Extraction_ML_UEnv.exp_b_eff)), q)) | uu___7 -> FStar_Compiler_Effect.failwith "FIXME Ty" in (match uu___5 with - | ((head_ml, (vars, t1)), qual) -> + | ((head_ml, (vars, t1), head_eff), qual) -> let has_typ_apps = match args with | (a, uu___6)::uu___7 -> is_type g a @@ -3575,16 +3607,20 @@ and (term_as_mlexpr' : uu___9 -> let uu___10 = instantiate_maybe_partial g head_ml - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___10 with - | (head2, uu___11, t2) -> (head2, t2)) + | (head2, eff, t2) -> + (head2, eff, t2)) | FStar_Extraction_ML_Syntax.MLE_Var uu___9 -> let uu___10 = instantiate_maybe_partial g head_ml - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___10 with - | (head2, uu___11, t2) -> (head2, t2)) + | (head2, eff, t2) -> + (head2, eff, t2)) | FStar_Extraction_ML_Syntax.MLE_App (head2, { @@ -3598,36 +3634,34 @@ and (term_as_mlexpr' : -> let uu___11 = instantiate_maybe_partial g head2 - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___11 with - | (head3, uu___12, t2) -> - let uu___13 = + | (head3, eff, t2) -> + let uu___12 = FStar_Extraction_ML_Syntax.with_ty t2 (FStar_Extraction_ML_Syntax.MLE_App (head3, [FStar_Extraction_ML_Syntax.ml_unit])) in - (uu___13, t2)) + (uu___12, eff, t2)) | uu___9 -> FStar_Compiler_Effect.failwith "Impossible: Unexpected head term" in (match uu___8 with - | (head2, t2) -> (head2, t2, rest)) in + | (head2, head_eff1, t2) -> + (head2, head_eff1, t2, rest)) in (match uu___6 with - | (head_ml1, head_t, args1) -> + | (head_ml1, head_eff1, head_t, args1) -> (match args1 with | [] -> let uu___7 = maybe_eta_data_and_project_record g qual head_t head_ml1 in - (uu___7, - FStar_Extraction_ML_Syntax.E_PURE, - head_t) + (uu___7, head_eff1, head_t) | uu___7 -> extract_app_maybe_projector qual - head_ml1 - (FStar_Extraction_ML_Syntax.E_PURE, - head_t) args1))) + head_ml1 (head_eff1, head_t) args1))) | FStar_Syntax_Syntax.Tm_fvar uu___4 -> let uu___5 = let uu___6 = @@ -3640,29 +3674,28 @@ and (term_as_mlexpr' : FStar_Class_Show.show FStar_Syntax_Print.showable_term head1 in let uu___10 = - let uu___11 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlexpr - uu___11 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr exp_b.FStar_Extraction_ML_UEnv.exp_b_expr in let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlty - uu___12 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme) in - FStar_Compiler_Util.print3 - "@@@looked up %s: got %s at %s\n" uu___9 - uu___10 uu___11); + let uu___12 = + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_etag + exp_b.FStar_Extraction_ML_UEnv.exp_b_eff in + FStar_Compiler_Util.print4 + "@@@looked up %s: got %s at %s with eff <%s>\n" + uu___9 uu___10 uu___11 uu___12); (((exp_b.FStar_Extraction_ML_UEnv.exp_b_expr), - (exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme)), + (exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme), + (exp_b.FStar_Extraction_ML_UEnv.exp_b_eff)), q)) | uu___7 -> FStar_Compiler_Effect.failwith "FIXME Ty" in (match uu___5 with - | ((head_ml, (vars, t1)), qual) -> + | ((head_ml, (vars, t1), head_eff), qual) -> let has_typ_apps = match args with | (a, uu___6)::uu___7 -> is_type g a @@ -3700,16 +3733,20 @@ and (term_as_mlexpr' : uu___9 -> let uu___10 = instantiate_maybe_partial g head_ml - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___10 with - | (head2, uu___11, t2) -> (head2, t2)) + | (head2, eff, t2) -> + (head2, eff, t2)) | FStar_Extraction_ML_Syntax.MLE_Var uu___9 -> let uu___10 = instantiate_maybe_partial g head_ml - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___10 with - | (head2, uu___11, t2) -> (head2, t2)) + | (head2, eff, t2) -> + (head2, eff, t2)) | FStar_Extraction_ML_Syntax.MLE_App (head2, { @@ -3723,36 +3760,34 @@ and (term_as_mlexpr' : -> let uu___11 = instantiate_maybe_partial g head2 - (vars, t1) provided_type_args in + head_eff (vars, t1) + provided_type_args in (match uu___11 with - | (head3, uu___12, t2) -> - let uu___13 = + | (head3, eff, t2) -> + let uu___12 = FStar_Extraction_ML_Syntax.with_ty t2 (FStar_Extraction_ML_Syntax.MLE_App (head3, [FStar_Extraction_ML_Syntax.ml_unit])) in - (uu___13, t2)) + (uu___12, eff, t2)) | uu___9 -> FStar_Compiler_Effect.failwith "Impossible: Unexpected head term" in (match uu___8 with - | (head2, t2) -> (head2, t2, rest)) in + | (head2, head_eff1, t2) -> + (head2, head_eff1, t2, rest)) in (match uu___6 with - | (head_ml1, head_t, args1) -> + | (head_ml1, head_eff1, head_t, args1) -> (match args1 with | [] -> let uu___7 = maybe_eta_data_and_project_record g qual head_t head_ml1 in - (uu___7, - FStar_Extraction_ML_Syntax.E_PURE, - head_t) + (uu___7, head_eff1, head_t) | uu___7 -> extract_app_maybe_projector qual - head_ml1 - (FStar_Extraction_ML_Syntax.E_PURE, - head_t) args1))) + head_ml1 (head_eff1, head_t) args1))) | uu___4 -> let uu___5 = term_as_mlexpr g head1 in (match uu___5 with @@ -4366,26 +4401,28 @@ and (term_as_mlexpr' : FStar_Extraction_ML_UEnv.exp_b_expr = fw; FStar_Extraction_ML_UEnv.exp_b_tscheme - = uu___9;_} + = uu___9; + FStar_Extraction_ML_UEnv.exp_b_eff = + uu___10;_} -> - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.ml_string_ty (FStar_Extraction_ML_Syntax.MLE_Const (FStar_Extraction_ML_Syntax.MLC_String "unreachable")) in - [uu___14] in - (fw, uu___13) in + [uu___15] in + (fw, uu___14) in FStar_Extraction_ML_Syntax.MLE_App - uu___12 in + uu___13 in FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.ml_int_ty - uu___11 in - (uu___10, + uu___12 in + (uu___11, FStar_Extraction_ML_Syntax.E_PURE, FStar_Extraction_ML_Syntax.ml_int_ty)) | (uu___7, uu___8, (uu___9, f_first, t_first))::rest diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml index 9931aaf7807..4a5ab217e08 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml @@ -14,22 +14,28 @@ type exp_binding = { exp_b_name: FStar_Extraction_ML_Syntax.mlident ; exp_b_expr: FStar_Extraction_ML_Syntax.mlexpr ; - exp_b_tscheme: FStar_Extraction_ML_Syntax.mltyscheme } + exp_b_tscheme: FStar_Extraction_ML_Syntax.mltyscheme ; + exp_b_eff: FStar_Extraction_ML_Syntax.e_tag } let (__proj__Mkexp_binding__item__exp_b_name : exp_binding -> FStar_Extraction_ML_Syntax.mlident) = fun projectee -> match projectee with - | { exp_b_name; exp_b_expr; exp_b_tscheme;_} -> exp_b_name + | { exp_b_name; exp_b_expr; exp_b_tscheme; exp_b_eff;_} -> exp_b_name let (__proj__Mkexp_binding__item__exp_b_expr : exp_binding -> FStar_Extraction_ML_Syntax.mlexpr) = fun projectee -> match projectee with - | { exp_b_name; exp_b_expr; exp_b_tscheme;_} -> exp_b_expr + | { exp_b_name; exp_b_expr; exp_b_tscheme; exp_b_eff;_} -> exp_b_expr let (__proj__Mkexp_binding__item__exp_b_tscheme : exp_binding -> FStar_Extraction_ML_Syntax.mltyscheme) = fun projectee -> match projectee with - | { exp_b_name; exp_b_expr; exp_b_tscheme;_} -> exp_b_tscheme + | { exp_b_name; exp_b_expr; exp_b_tscheme; exp_b_eff;_} -> exp_b_tscheme +let (__proj__Mkexp_binding__item__exp_b_eff : + exp_binding -> FStar_Extraction_ML_Syntax.e_tag) = + fun projectee -> + match projectee with + | { exp_b_name; exp_b_expr; exp_b_tscheme; exp_b_eff;_} -> exp_b_eff type ty_or_exp_b = (ty_binding, exp_binding) FStar_Pervasives.either type binding = | Bv of (FStar_Syntax_Syntax.bv * ty_or_exp_b) @@ -757,34 +763,38 @@ let (extend_bv : FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.MLTY_Top uu___2) else FStar_Extraction_ML_Syntax.with_ty ml_ty mlx in - let t_x1 = + let uu___1 = if add_unit then FStar_Extraction_ML_Syntax.pop_unit t_x - else t_x in - let exp_binding1 = - { - exp_b_name = mlident; - exp_b_expr = mlx1; - exp_b_tscheme = t_x1 - } in - let gamma = (Bv (x, (FStar_Pervasives.Inr exp_binding1))) :: - (g.env_bindings) in - let tcenv = - let uu___1 = FStar_Syntax_Syntax.binders_of_list [x] in - FStar_TypeChecker_Env.push_binders g.env_tcenv uu___1 in - ({ - env_tcenv = tcenv; - env_bindings = gamma; - env_mlident_map = mlident_map; - env_remove_typars = (g.env_remove_typars); - mlpath_of_lid = (g.mlpath_of_lid); - env_fieldname_map = (g.env_fieldname_map); - mlpath_of_fieldname = (g.mlpath_of_fieldname); - tydefs = (g.tydefs); - type_names = (g.type_names); - tydef_declarations = (g.tydef_declarations); - currentModule = (g.currentModule) - }, mlident, exp_binding1) + else (FStar_Extraction_ML_Syntax.E_PURE, t_x) in + (match uu___1 with + | (eff, t_x1) -> + let exp_binding1 = + { + exp_b_name = mlident; + exp_b_expr = mlx1; + exp_b_tscheme = t_x1; + exp_b_eff = eff + } in + let gamma = + (Bv (x, (FStar_Pervasives.Inr exp_binding1))) :: + (g.env_bindings) in + let tcenv = + let uu___2 = FStar_Syntax_Syntax.binders_of_list [x] in + FStar_TypeChecker_Env.push_binders g.env_tcenv uu___2 in + ({ + env_tcenv = tcenv; + env_bindings = gamma; + env_mlident_map = mlident_map; + env_remove_typars = (g.env_remove_typars); + mlpath_of_lid = (g.mlpath_of_lid); + env_fieldname_map = (g.env_fieldname_map); + mlpath_of_fieldname = (g.mlpath_of_fieldname); + tydefs = (g.tydefs); + type_names = (g.type_names); + tydef_declarations = (g.tydef_declarations); + currentModule = (g.currentModule) + }, mlident, exp_binding1)) let (burn_name : uenv -> FStar_Extraction_ML_Syntax.mlident -> uenv) = fun g -> fun i -> @@ -874,33 +884,36 @@ let (extend_fv : FStar_Extraction_ML_Syntax.with_ty FStar_Extraction_ML_Syntax.MLTY_Top uu___2 else FStar_Extraction_ML_Syntax.with_ty ml_ty mly in - let t_x1 = + let uu___2 = if add_unit then FStar_Extraction_ML_Syntax.pop_unit t_x - else t_x in - let exp_binding1 = - { - exp_b_name = mlsymbol; - exp_b_expr = mly1; - exp_b_tscheme = t_x1 - } in - let gamma = (Fv (x, exp_binding1)) :: (g1.env_bindings) in - let mlident_map = - FStar_Compiler_Util.psmap_add g1.env_mlident_map mlsymbol - "" in - ({ - env_tcenv = (g1.env_tcenv); - env_bindings = gamma; - env_mlident_map = mlident_map; - env_remove_typars = (g1.env_remove_typars); - mlpath_of_lid = (g1.mlpath_of_lid); - env_fieldname_map = (g1.env_fieldname_map); - mlpath_of_fieldname = (g1.mlpath_of_fieldname); - tydefs = (g1.tydefs); - type_names = (g1.type_names); - tydef_declarations = (g1.tydef_declarations); - currentModule = (g1.currentModule) - }, mlsymbol, exp_binding1) + else (FStar_Extraction_ML_Syntax.E_PURE, t_x) in + (match uu___2 with + | (eff, t_x1) -> + let exp_binding1 = + { + exp_b_name = mlsymbol; + exp_b_expr = mly1; + exp_b_tscheme = t_x1; + exp_b_eff = eff + } in + let gamma = (Fv (x, exp_binding1)) :: (g1.env_bindings) in + let mlident_map = + FStar_Compiler_Util.psmap_add g1.env_mlident_map + mlsymbol "" in + ({ + env_tcenv = (g1.env_tcenv); + env_bindings = gamma; + env_mlident_map = mlident_map; + env_remove_typars = (g1.env_remove_typars); + mlpath_of_lid = (g1.mlpath_of_lid); + env_fieldname_map = (g1.env_fieldname_map); + mlpath_of_fieldname = (g1.mlpath_of_fieldname); + tydefs = (g1.tydefs); + type_names = (g1.type_names); + tydef_declarations = (g1.tydef_declarations); + currentModule = (g1.currentModule) + }, mlsymbol, exp_binding1)) else (let uu___2 = let uu___3 = diff --git a/ocaml/fstar-lib/generated/FStar_MRef.ml b/ocaml/fstar-lib/generated/FStar_MRef.ml index d71cd8c5d87..da6bd9cfc0f 100644 --- a/ocaml/fstar-lib/generated/FStar_MRef.ml +++ b/ocaml/fstar-lib/generated/FStar_MRef.ml @@ -4,10 +4,10 @@ type ('a, 'b, 'r, 'p, 'h) p_pred = unit type ('uuuuu, 'uuuuu1, 'r, 'p) token = unit FStar_ST.witnessed let witness_token : 'uuuuu 'uuuuu1 . ('uuuuu, 'uuuuu1) FStar_ST.mref -> unit -> unit = - fun m -> fun p -> () + fun m -> fun p -> FStar_ST.gst_recall (); FStar_ST.gst_witness () let recall_token : 'uuuuu 'uuuuu1 . ('uuuuu, 'uuuuu1) FStar_ST.mref -> unit -> unit = - fun m -> fun p -> () + fun m -> fun p -> FStar_ST.gst_recall () type ('a, 'rel) spred = unit -let recall : 'p . unit -> unit = fun uu___ -> () -let witness : 'p . unit -> unit = fun uu___ -> () \ No newline at end of file +let recall : 'p . unit -> unit = fun uu___ -> FStar_ST.gst_recall () +let witness : 'p . unit -> unit = fun uu___ -> FStar_ST.gst_witness () \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml index 1f8425ded08..0a74422fc2d 100644 --- a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml +++ b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml @@ -158,4 +158,7 @@ let testify_seqn : fun i -> fun l -> fun log -> - fun max -> fun ctr -> let n = FStar_HyperStack_ST.op_Bang ctr in () \ No newline at end of file + fun max -> + fun ctr -> + let n = FStar_HyperStack_ST.op_Bang ctr in + FStar_HyperStack_ST.testify () \ No newline at end of file diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index 9a9685fd577..5b879ad77d4 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/src/extraction/FStar.Extraction.ML.Code.fst @@ -314,6 +314,11 @@ let string_of_mlconstant (sctt : mlconstant) = (* -------------------------------------------------------------------- *) +let string_of_etag = function + | E_PURE -> "" + | E_ERASABLE -> "Erased" + | E_IMPURE -> "Impure" + let rec doc_of_mltype' (currentModule : mlsymbol) (outer : level) (ty : mlty) = match ty with | MLTY_Var x -> @@ -344,7 +349,7 @@ let rec doc_of_mltype' (currentModule : mlsymbol) (outer : level) (ty : mlty) = hbox (reduce1 [args; text name]) end - | MLTY_Fun (t1, _, t2) -> + | MLTY_Fun (t1, et, t2) -> let d1 = doc_of_mltype currentModule (t_prio_fun, Left ) t1 in let d2 = doc_of_mltype currentModule (t_prio_fun, Right) t2 in maybe_paren outer t_prio_fun (hbox (reduce1 [d1; text " -> "; d2])) @@ -854,3 +859,11 @@ let string_of_mlty (cmod) (e:mlty) = instance showable_mlexpr : showable mlexpr = { show = string_of_mlexpr ([], ""); } + +instance showable_mlty : showable mlty = { + show = string_of_mlty ([], ""); +} + +instance showable_etag : showable e_tag = { + show = string_of_etag +} diff --git a/src/extraction/FStar.Extraction.ML.Code.fsti b/src/extraction/FStar.Extraction.ML.Code.fsti index 0ca581c2bd4..c12b92fc661 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fsti +++ b/src/extraction/FStar.Extraction.ML.Code.fsti @@ -30,3 +30,5 @@ val string_of_mlty: mlpath -> mlty -> string val pretty: int -> doc -> string instance val showable_mlexpr : showable mlexpr +instance val showable_mlty : showable mlty +instance val showable_etag : showable e_tag \ No newline at end of file diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index 6ee9223330e..eefa196a3e3 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/src/extraction/FStar.Extraction.ML.Syntax.fst @@ -97,16 +97,16 @@ let apply_obj_repr : mlexpr -> mlty -> mlexpr = fun x t -> let ty_param_names (tys:list ty_param) : list string = tys |> List.map (fun {ty_param_name} -> ty_param_name) -let push_unit (ts : mltyscheme) : mltyscheme = +let push_unit eff (ts : mltyscheme) : mltyscheme = let vs, ty = ts in - vs, MLTY_Fun(ml_unit_ty, E_PURE, ty) + vs, MLTY_Fun(ml_unit_ty, eff, ty) -let pop_unit (ts : mltyscheme) : mltyscheme = +let pop_unit (ts : mltyscheme) : e_tag & mltyscheme = let vs, ty = ts in match ty with - | MLTY_Fun (l, E_PURE, t) -> + | MLTY_Fun (l, eff, t) -> if l = ml_unit_ty - then vs, t + then eff, (vs, t) else failwith "unexpected: pop_unit: domain was not unit" | _ -> failwith "unexpected: pop_unit: not a function type" diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fsti b/src/extraction/FStar.Extraction.ML.Syntax.fsti index d18da69e236..3f68517fdda 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fsti +++ b/src/extraction/FStar.Extraction.ML.Syntax.fsti @@ -239,8 +239,8 @@ val apply_obj_repr : mlexpr -> mlty -> mlexpr val ty_param_names (tys:list ty_param) : list string -val push_unit (ts : mltyscheme) : mltyscheme -val pop_unit (ts : mltyscheme) : mltyscheme +val push_unit (eff:e_tag) (ts : mltyscheme) : mltyscheme +val pop_unit (ts : mltyscheme) : e_tag & mltyscheme val mltyscheme_to_string (tsc:mltyscheme) : string val mlbranch_to_string (b:mlbranch) : string diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index 46f6c663d04..9e481e2423f 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/src/extraction/FStar.Extraction.ML.Term.fst @@ -457,14 +457,14 @@ let fresh_binders (ts:list mlty) (g:uenv) : list mlbinder & uenv = // and isn't instantiated in F* (e.g., because of first-class polymorphism) // we extract e to a type application in ML by instantiating all its // type arguments to MLTY_Erased (later, perhaps, being forced to insert magics) -let instantiate_maybe_partial (g:uenv) (e:mlexpr) (s:mltyscheme) (tyargs:list mlty) : (mlexpr & e_tag & mlty) = +let instantiate_maybe_partial (g:uenv) (e:mlexpr) (eff:e_tag) (s:mltyscheme) (tyargs:list mlty) : (mlexpr & e_tag & mlty) = let vars, t = s in let n_vars = List.length vars in let n_args = List.length tyargs in if n_args = n_vars then //easy, just make a type application node if n_args = 0 - then (e, E_PURE, t) + then (e, eff, t) else let ts = instantiate_tyscheme (vars, t) tyargs in let tapp = { @@ -472,7 +472,7 @@ let instantiate_maybe_partial (g:uenv) (e:mlexpr) (s:mltyscheme) (tyargs:list ml expr=MLE_TApp(e, tyargs); mlty=ts } in - (tapp, E_PURE, ts) + (tapp, eff, ts) else if n_args < n_vars then //We have a partial type-application in F* //So, make a full type application node in ML, @@ -499,7 +499,7 @@ let instantiate_maybe_partial (g:uenv) (e:mlexpr) (s:mltyscheme) (tyargs:list ml 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) + (f, eff, t) else failwith "Impossible: instantiate_maybe_partial called with too many arguments" (* eta-expand `e` according to its type `t` *) @@ -1244,13 +1244,18 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig = //If, after erasure, what remains is not a value, then add an extra unit arg. to preserve order of evaluation/generativity //and to circumvent the value restriction - //TODO: ERASE ONLY THOSE THAT ABSTRACT OVER PURE FUNCTIONS in Type(i), - // NOT, e.g., (x:int -> St Type) - let tbinders, tbody = + //We also erase type arguments that abstract over impure functions, + //replacing the type arguments with a single unit. + //For example, `a:Type -> Dv a` is extracted to `unit -Impure-> 'a` + //The important thing is that we retain an effect tag on the arrow to note + //that the type application is impure. + //See Issue #3473 + let etag_of_comp c = effect_as_etag g (U.comp_effect_name c) in + let tbinders, eff_body, tbody = match BU.prefix_until (fun x -> not (is_type_binder g x)) bs with - | None -> bs, U.comp_result c - | Some (bs, b, rest) -> bs, U.arrow (b::rest) c in - + | None -> bs, etag_of_comp c, U.comp_result c + | Some (bs, b, rest) -> bs, E_PURE, U.arrow (b::rest) c + in 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}) -> { @@ -1274,7 +1279,12 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig = || not (U.is_pure_comp c) | _ -> false in let rest_args = if add_unit then (unit_binder()::rest_args) else rest_args in - let polytype = if add_unit then push_unit polytype else polytype in + let polytype = + if add_unit + then (* record the effect of type application, eff_body *) + push_unit eff_body polytype + else polytype + in let body = U.abs rest_args body copt in (lbname_, f_e, (lbtyp, (targs, polytype)), add_unit, has_c_inline, body) @@ -1344,6 +1354,12 @@ and check_term_as_mlexpr (g:uenv) (e:term) (f:e_tag) (ty:mlty) : (mlexpr & mlty | E_PURE, MLTY_Erased -> ml_unit, MLTY_Erased | _ -> let ml_e, tag, t = term_as_mlexpr g e in + debug g (fun _ -> + BU.print4 "Extracted %s to %s at eff %s and type %s\n" + (show e) + (Code.string_of_mlexpr (current_module_of_uenv g) ml_e) + (Util.eff_to_string tag) + (Code.string_of_mlty (current_module_of_uenv g) t)); if eff_leq tag f then maybe_coerce e.pos g ml_e t ty, ty else match tag, f, ty with @@ -1511,19 +1527,21 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = | Inl _, _ -> ml_unit, E_PURE, ml_unit_ty - | Inr ({exp_b_expr=x; exp_b_tscheme=mltys}), qual -> - //let _ = printfn "\n (*looked up tyscheme of \n %A \n as \n %A *) \n" x s in + | Inr ({exp_b_expr=x; exp_b_tscheme=mltys; exp_b_eff=etag}), qual -> + //etag is the effect associated with simply using t, since it may + //be an effectful type application in F* + //in the common case, etag is E_PURE begin match mltys with | ([], t) when t=ml_unit_ty -> - ml_unit, E_PURE, t //optimize (x:unit) to () + ml_unit, etag, t //optimize (x:unit) to () | ([], t) -> - maybe_eta_data_and_project_record g qual t x, E_PURE, t + maybe_eta_data_and_project_record g qual t x, etag, t | _ -> (* We have a first-class polymorphic value; Extract it to ML by instantiating its type arguments to MLTY_Erased *) - instantiate_maybe_partial g x mltys [] + instantiate_maybe_partial g x etag mltys [] end end @@ -1542,12 +1560,12 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = let _ = debug g (fun () -> BU.print3 "looked up %s: got %s at %s \n" (show fv) - (Code.string_of_mlexpr (current_module_of_uenv g) x) - (Code.string_of_mlty (current_module_of_uenv g) (snd mltys))) in + (show x) + (show (snd mltys))) in begin match mltys with | ([], t) when (t=ml_unit_ty) -> ml_unit, E_PURE, t //optimize (x:unit) to () | ([], t) -> maybe_eta_data_and_project_record g fv.fv_qual t x, E_PURE, t - | _ -> instantiate_maybe_partial g x mltys [] + | _ -> instantiate_maybe_partial g x E_PURE mltys [] end end @@ -1715,21 +1733,22 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = | Tm_name _ | Tm_fvar _ -> // debug g (fun () -> printfn "head of app is %s\n" (Print.exp_to_string head)); - let (head_ml, (vars, t)), qual = + let (head_ml, (vars, t), head_eff), qual = match lookup_term g head with | Inr exp_b, q -> debug g (fun () -> - BU.print3 "@@@looked up %s: got %s at %s\n" + BU.print4 "@@@looked up %s: got %s at %s with eff <%s>\n" (show head) - (Code.string_of_mlexpr (current_module_of_uenv g) exp_b.exp_b_expr) - (Code.string_of_mlty (current_module_of_uenv g) (snd exp_b.exp_b_tscheme))); - (exp_b.exp_b_expr, exp_b.exp_b_tscheme), q + (show exp_b.exp_b_expr) + (show (snd exp_b.exp_b_tscheme)) + (show exp_b.exp_b_eff)); + (exp_b.exp_b_expr, exp_b.exp_b_tscheme, exp_b.exp_b_eff), q | _ -> failwith "FIXME Ty" in let has_typ_apps = match args with | (a, _)::_ -> is_type g a | _ -> false in - let head_ml, head_t, args = + let head_ml, head_eff, head_t, args = (* Here, we have, say, f extracted to head_ml, with a polymorphic ML type with n type-args If, in F*, `f` is applied to exactly `n` type args, then things are easy: We extract those n arguments to ML types @@ -1755,32 +1774,33 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = List.map (fun (x, _) -> term_as_mlty g x) prefix, rest in - let head, t = + let head, head_eff, t = match head_ml.expr with | MLE_Name _ | MLE_Var _ -> - let head, _, t = - instantiate_maybe_partial g head_ml (vars, t) provided_type_args + let head, eff, t = + instantiate_maybe_partial g head_ml head_eff (vars, t) provided_type_args in - head, t + head, eff, t | MLE_App(head, [{expr=MLE_Const MLC_Unit}]) -> //this happens when the extraction inserted an extra //unit argument to circumvent ML's value restriction - let head, _, t = - instantiate_maybe_partial g head (vars, t) provided_type_args + let head, eff, t = + instantiate_maybe_partial g head head_eff (vars, t) provided_type_args in MLE_App(head, [ ml_unit ]) |> with_ty t, + eff, t | _ -> failwith "Impossible: Unexpected head term" in - head, t, rest + head, head_eff, t, rest in begin match args with - | [] -> maybe_eta_data_and_project_record g qual head_t head_ml, E_PURE, head_t - | _ -> extract_app_maybe_projector qual head_ml (E_PURE, head_t) args + | [] -> maybe_eta_data_and_project_record g qual head_t head_ml, head_eff, head_t + | _ -> extract_app_maybe_projector qual head_ml (head_eff, head_t) args end | _ -> diff --git a/src/extraction/FStar.Extraction.ML.UEnv.fst b/src/extraction/FStar.Extraction.ML.UEnv.fst index 55739302496..605d37b6cb4 100644 --- a/src/extraction/FStar.Extraction.ML.UEnv.fst +++ b/src/extraction/FStar.Extraction.ML.UEnv.fst @@ -449,8 +449,8 @@ let extend_bv (g:uenv) (x:bv) (t_x:mltyscheme) (add_unit:bool) else if add_unit then with_ty MLTY_Top <| MLE_App(with_ty MLTY_Top mlx, [ml_unit]) else with_ty ml_ty mlx in - let t_x = if add_unit then pop_unit t_x else t_x in - let exp_binding = {exp_b_name=mlident; exp_b_expr=mlx; exp_b_tscheme=t_x } in + let eff, t_x = if add_unit then pop_unit t_x else E_PURE, t_x in + let exp_binding = {exp_b_name=mlident; exp_b_expr=mlx; exp_b_tscheme=t_x; exp_b_eff=eff } in let gamma = Bv(x, Inr exp_binding)::g.env_bindings in let tcenv = TypeChecker.Env.push_binders g.env_tcenv (binders_of_list [x]) in {g with env_bindings=gamma; env_mlident_map = mlident_map; env_tcenv=tcenv}, mlident, exp_binding @@ -497,8 +497,8 @@ let extend_fv (g:uenv) (x:fv) (t_x:mltyscheme) (add_unit:bool) let mlsymbol = snd mlpath in let mly = MLE_Name mlpath in let mly = if add_unit then with_ty MLTY_Top <| MLE_App(with_ty MLTY_Top mly, [ml_unit]) else with_ty ml_ty mly in - let t_x = if add_unit then pop_unit t_x else t_x in - let exp_binding = {exp_b_name=mlsymbol; exp_b_expr=mly; exp_b_tscheme=t_x } in + let eff, t_x = if add_unit then pop_unit t_x else E_PURE, t_x in + let exp_binding = {exp_b_name=mlsymbol; exp_b_expr=mly; exp_b_tscheme=t_x; exp_b_eff=eff } in let gamma = Fv(x, exp_binding)::g.env_bindings in let mlident_map = BU.psmap_add g.env_mlident_map mlsymbol "" in {g with env_bindings=gamma; env_mlident_map=mlident_map}, mlsymbol, exp_binding diff --git a/src/extraction/FStar.Extraction.ML.UEnv.fsti b/src/extraction/FStar.Extraction.ML.UEnv.fsti index 6475dcb5a87..a44db2a3738 100644 --- a/src/extraction/FStar.Extraction.ML.UEnv.fsti +++ b/src/extraction/FStar.Extraction.ML.UEnv.fsti @@ -42,7 +42,8 @@ type ty_binding = { type exp_binding = { exp_b_name:mlident; exp_b_expr:mlexpr; - exp_b_tscheme:mltyscheme + exp_b_tscheme:mltyscheme; + exp_b_eff: e_tag } type ty_or_exp_b = either ty_binding exp_binding diff --git a/tests/bug-reports/Bug3473.fst b/tests/bug-reports/Bug3473.fst new file mode 100644 index 00000000000..a602013274e --- /dev/null +++ b/tests/bug-reports/Bug3473.fst @@ -0,0 +1,5 @@ +module Bug3473 +let rec uhoh t : Dv t = uhoh t + +let foo (x: option nat) : Dv string = + uhoh unit; "foo" \ No newline at end of file diff --git a/tests/bug-reports/Bug3473.ml.expected b/tests/bug-reports/Bug3473.ml.expected new file mode 100644 index 00000000000..cc003b42de0 --- /dev/null +++ b/tests/bug-reports/Bug3473.ml.expected @@ -0,0 +1,4 @@ +open Prims +let rec uhoh : 't . unit -> 't = fun uu___ -> uhoh () +let (foo : Prims.nat FStar_Pervasives_Native.option -> Prims.string) = + fun x -> uhoh (); "foo" \ No newline at end of file diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index 1c5ed101806..c40778f342d 100644 --- a/tests/bug-reports/Makefile +++ b/tests/bug-reports/Makefile @@ -144,7 +144,7 @@ SHOULD_EXTRACT_CLOSED=Bug086.fst Bug314.fst Bug540.fst Bug541.fst Bug589.fst \ ExtractionBug2.fst Bug1101.fst Bug1485.fst Bug734.fst Bug310.fst \ Bug2058.fst RemoveUnusedTypars.B.fst RemoveUnusedTyparsIFace.B.fst \ PushPopProjectors.fst Bug2412.fst Bug2595.fst Bug2699.fst Bug2895.fst \ - ValLetRec.fst + ValLetRec.fst Bug3473.fst #ExtractionBug03.fst # Bug1479.fst Crashes when in CI with "Error: Unbound module FStar_Tactics_Effect" @@ -230,6 +230,11 @@ Bug2895.ml: Bug2895.extract: Bug2895.ml diff -u --strip-trailing-cr Bug2895.ml Bug2895.ml.expected +Bug3473.ml: + $(FSTAR) $(FSTAR_DEFAULT_ARGS) --extract Bug3473 --codegen OCaml Bug3473.fst + +Bug3473.extract: Bug3473.ml + diff -u --strip-trailing-cr Bug3473.ml Bug3473.ml.expected RemoveUnusedTypars.B.extract: RemoveUnusedTypars.A.fst RemoveUnusedTypars.B.fst $(FSTAR) $(FSTAR_DEFAULT_ARGS) --cache_checked_modules RemoveUnusedTypars.A.fst