diff --git a/examples/dsls/bool_refinement/BoolRefinement.fst b/examples/dsls/bool_refinement/BoolRefinement.fst index be1988f1b1f..7880c41a598 100755 --- a/examples/dsls/bool_refinement/BoolRefinement.fst +++ b/examples/dsls/bool_refinement/BoolRefinement.fst @@ -1690,7 +1690,7 @@ let main (src:src_exp) : RT.dsl_tac_t = then let (| src_ty, _ |) = check f [] src in soundness_lemma f [] src src_ty; - elab_exp src, elab_ty src_ty + Some (elab_exp src), None, elab_ty src_ty else T.fail "Not locally nameless" (***** Examples *****) diff --git a/examples/dsls/dependent_bool_refinement/DependentBoolRefinement.fst b/examples/dsls/dependent_bool_refinement/DependentBoolRefinement.fst index dd6be6b772e..3865178b356 100755 --- a/examples/dsls/dependent_bool_refinement/DependentBoolRefinement.fst +++ b/examples/dsls/dependent_bool_refinement/DependentBoolRefinement.fst @@ -876,12 +876,12 @@ and closed_ty (t:src_ty) | TRefineBool e -> closed e | TArrow t1 t2 -> closed_ty t1 && closed_ty t2 -let main (f:fstar_top_env) - (src:src_exp) - : T.Tac (e:R.term & t:R.term { RT.tot_typing f e t }) - = if closed src - then - let (| src_ty, _ |) = check f [] src in - soundness_lemma f [] src src_ty; - (| elab_exp src, elab_ty src_ty |) - else T.fail "Not locally nameless" +let main (src:src_exp) + : RT.dsl_tac_t + = fun f -> + if closed src + then + let (| src_ty, _ |) = check f [] src in + soundness_lemma f [] src src_ty; + Some(elab_exp src), None, elab_ty src_ty + else T.fail "Not locally nameless" diff --git a/examples/dsls/stlc/STLC.Core.fst b/examples/dsls/stlc/STLC.Core.fst index af3f3ee29f4..e746c6d8d9a 100755 --- a/examples/dsls/stlc/STLC.Core.fst +++ b/examples/dsls/stlc/STLC.Core.fst @@ -542,7 +542,7 @@ let main (src:stlc_exp) : RT.dsl_tac_t = then let (| src_ty, d |) = check g [] src in soundness_lemma [] src src_ty g; - elab_exp src, elab_ty src_ty + Some (elab_exp src), None, elab_ty src_ty else T.fail "Not locally nameless" (***** Tests *****) diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 1f1d1650f53..c8dd7b28bd3 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -1,5 +1,5 @@ open Prims -let (cache_version_number : Prims.int) = (Prims.of_int (60)) +let (cache_version_number : Prims.int) = (Prims.of_int (61)) type tc_result = { checked_module: FStar_Syntax_Syntax.modul ; diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index 127bfbb3a66..7b1fe67fa12 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -1,4 +1,21 @@ open Prims +type extension_extractor = + FStar_Extraction_ML_UEnv.uenv -> + FStar_Compiler_Dyn.dyn -> + ((FStar_Extraction_ML_Syntax.mlexpr * FStar_Extraction_ML_Syntax.e_tag + * FStar_Extraction_ML_Syntax.mlty), + Prims.string) FStar_Pervasives.either +let (extension_extractor_table : + extension_extractor FStar_Compiler_Util.smap) = + FStar_Compiler_Util.smap_create (Prims.of_int (20)) +let (register_extension_extractor : + Prims.string -> extension_extractor -> unit) = + fun ext -> + fun callback -> + FStar_Compiler_Util.smap_add extension_extractor_table ext callback +let (lookup_extension_extractor : + Prims.string -> extension_extractor FStar_Pervasives_Native.option) = + fun ext -> FStar_Compiler_Util.smap_try_find extension_extractor_table ext type env_t = FStar_Extraction_ML_UEnv.uenv let (fail_exp : FStar_Ident.lident -> @@ -2158,482 +2175,75 @@ let rec (extract_sig : let uu___6 = extract_let_rec_types se1 g lbs in (match uu___6 with | (env, uu___7, impl) -> (env, impl)) | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = lbs; + { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); FStar_Syntax_Syntax.lids1 = uu___5;_} + when + Prims.uu___is_Cons + (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data -> - let attrs = se1.FStar_Syntax_Syntax.sigattrs in - let quals = se1.FStar_Syntax_Syntax.sigquals in - let maybe_postprocess_lbs lbs1 = - let post_tau = - let uu___6 = - FStar_Syntax_Util.extract_attr' - FStar_Parser_Const.postprocess_extr_with attrs in - match uu___6 with - | FStar_Pervasives_Native.None -> - FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some - (uu___7, - (tau, FStar_Pervasives_Native.None)::uu___8) - -> FStar_Pervasives_Native.Some tau - | FStar_Pervasives_Native.Some uu___7 -> - (FStar_Errors.log_issue - se1.FStar_Syntax_Syntax.sigrng - (FStar_Errors_Codes.Warning_UnrecognizedAttribute, - "Ill-formed application of 'postprocess_for_extraction_with'"); - FStar_Pervasives_Native.None) in - let postprocess_lb tau lb = - let env = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in - let lbdef = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_TypeChecker_Env.current_module env in - FStar_Ident.string_of_lid uu___8 in - FStar_Pervasives_Native.Some uu___7 in - FStar_Profiling.profile - (fun uu___7 -> - FStar_TypeChecker_Env.postprocess env tau - lb.FStar_Syntax_Syntax.lbtyp - lb.FStar_Syntax_Syntax.lbdef) uu___6 - "FStar.Extraction.ML.Module.post_process_for_extraction" in - { - FStar_Syntax_Syntax.lbname = - (lb.FStar_Syntax_Syntax.lbname); - FStar_Syntax_Syntax.lbunivs = - (lb.FStar_Syntax_Syntax.lbunivs); - FStar_Syntax_Syntax.lbtyp = - (lb.FStar_Syntax_Syntax.lbtyp); - FStar_Syntax_Syntax.lbeff = - (lb.FStar_Syntax_Syntax.lbeff); - FStar_Syntax_Syntax.lbdef = lbdef; - FStar_Syntax_Syntax.lbattrs = - (lb.FStar_Syntax_Syntax.lbattrs); - FStar_Syntax_Syntax.lbpos = - (lb.FStar_Syntax_Syntax.lbpos) - } in - match post_tau with - | FStar_Pervasives_Native.None -> lbs1 - | FStar_Pervasives_Native.Some tau -> - let uu___6 = - FStar_Compiler_List.map (postprocess_lb tau) - (FStar_Pervasives_Native.snd lbs1) in - ((FStar_Pervasives_Native.fst lbs1), uu___6) in - let maybe_normalize_for_extraction lbs1 = - let norm_steps = - let uu___6 = - FStar_Syntax_Util.extract_attr' - FStar_Parser_Const.normalize_for_extraction_lid - attrs in - match uu___6 with - | FStar_Pervasives_Native.None -> - FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some - (uu___7, - (steps, FStar_Pervasives_Native.None)::uu___8) - -> - let steps1 = - let uu___9 = - FStar_Extraction_ML_UEnv.tcenv_of_uenv g in - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Zeta; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Primops] uu___9 steps in - let uu___9 = - let uu___10 = - FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_norm_step in - FStar_TypeChecker_Cfg.try_unembed_simple uu___10 - steps1 in - (match uu___9 with - | FStar_Pervasives_Native.Some steps2 -> - let uu___10 = - FStar_TypeChecker_Cfg.translate_norm_steps - steps2 in - FStar_Pervasives_Native.Some uu___10 - | uu___10 -> - ((let uu___12 = - let uu___13 = - let uu___14 = - FStar_Syntax_Print.term_to_string - steps1 in - FStar_Compiler_Util.format1 - "Ill-formed application of 'normalize_for_extraction': normalization steps '%s' could not be interpreted" - uu___14 in - (FStar_Errors_Codes.Warning_UnrecognizedAttribute, - uu___13) in - FStar_Errors.log_issue - se1.FStar_Syntax_Syntax.sigrng uu___12); - FStar_Pervasives_Native.None)) - | FStar_Pervasives_Native.Some uu___7 -> - (FStar_Errors.log_issue - se1.FStar_Syntax_Syntax.sigrng - (FStar_Errors_Codes.Warning_UnrecognizedAttribute, - "Ill-formed application of 'normalize_for_extraction'"); - FStar_Pervasives_Native.None) in - let norm_one_lb steps lb = - let env = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in - let env1 = - { - FStar_TypeChecker_Env.solver = - (env.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = - (env.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (env.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (env.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (env.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (env.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (env.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (env.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = - (env.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (env.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (env.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = - (env.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (env.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (env.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (env.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (env.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (env.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (env.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = - (env.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = - (env.FStar_TypeChecker_Env.lax); - FStar_TypeChecker_Env.lax_universes = - (env.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = - (env.FStar_TypeChecker_Env.phase1); - FStar_TypeChecker_Env.failhard = - (env.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (env.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (env.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (env.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.nocoerce = - (env.FStar_TypeChecker_Env.nocoerce); - FStar_TypeChecker_Env.tc_term = - (env.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (env.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term - = - (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (env.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (env.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (env.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (env.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (env.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (env.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (env.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (env.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = - (env.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (env.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (env.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (env.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (env.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = - (env.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = - (env.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (env.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (env.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (env.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (env.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = true; - FStar_TypeChecker_Env.core_check = - (env.FStar_TypeChecker_Env.core_check) - } in - let lbd = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_TypeChecker_Env.current_module env1 in - FStar_Ident.string_of_lid uu___8 in - FStar_Pervasives_Native.Some uu___7 in - FStar_Profiling.profile - (fun uu___7 -> - FStar_TypeChecker_Normalize.normalize steps - env1 lb.FStar_Syntax_Syntax.lbdef) uu___6 - "FStar.Extraction.ML.Module.normalize_for_extraction" in - { - FStar_Syntax_Syntax.lbname = - (lb.FStar_Syntax_Syntax.lbname); - FStar_Syntax_Syntax.lbunivs = - (lb.FStar_Syntax_Syntax.lbunivs); - FStar_Syntax_Syntax.lbtyp = - (lb.FStar_Syntax_Syntax.lbtyp); - FStar_Syntax_Syntax.lbeff = - (lb.FStar_Syntax_Syntax.lbeff); - FStar_Syntax_Syntax.lbdef = lbd; - FStar_Syntax_Syntax.lbattrs = - (lb.FStar_Syntax_Syntax.lbattrs); - FStar_Syntax_Syntax.lbpos = - (lb.FStar_Syntax_Syntax.lbpos) - } in - match norm_steps with - | FStar_Pervasives_Native.None -> lbs1 - | FStar_Pervasives_Native.Some steps -> - let uu___6 = - FStar_Compiler_List.map (norm_one_lb steps) - (FStar_Pervasives_Native.snd lbs1) in - ((FStar_Pervasives_Native.fst lbs1), uu___6) in let uu___6 = - let lbs1 = - let uu___7 = maybe_postprocess_lbs lbs in - maybe_normalize_for_extraction uu___7 in - let uu___7 = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_let - { - FStar_Syntax_Syntax.lbs = lbs1; - FStar_Syntax_Syntax.body1 = - FStar_Syntax_Util.exp_false_bool - }) se1.FStar_Syntax_Syntax.sigrng in - FStar_Extraction_ML_Term.term_as_mlexpr g uu___7 in + FStar_Compiler_List.tryPick + (fun uu___7 -> + match uu___7 with + | (ext, blob) -> + let uu___8 = lookup_extension_extractor ext in + (match uu___8 with + | FStar_Pervasives_Native.None -> + FStar_Pervasives_Native.None + | FStar_Pervasives_Native.Some extractor -> + FStar_Pervasives_Native.Some + (ext, blob, extractor))) + (se1.FStar_Syntax_Syntax.sigmeta).FStar_Syntax_Syntax.sigmeta_extension_data in (match uu___6 with - | (ml_let, uu___7, uu___8) -> - (match ml_let.FStar_Extraction_ML_Syntax.expr with - | FStar_Extraction_ML_Syntax.MLE_Let - ((flavor, bindings), uu___9) -> - let flags = - FStar_Compiler_List.choose flag_of_qual quals in - let flags' = extract_metadata attrs in - let uu___10 = - FStar_Compiler_List.fold_left2 - (fun uu___11 -> - fun ml_lb -> - fun uu___12 -> - match (uu___11, uu___12) with - | ((env, ml_lbs), - { - FStar_Syntax_Syntax.lbname = - lbname; - FStar_Syntax_Syntax.lbunivs = - uu___13; - FStar_Syntax_Syntax.lbtyp = t; - FStar_Syntax_Syntax.lbeff = - uu___14; - FStar_Syntax_Syntax.lbdef = - uu___15; - FStar_Syntax_Syntax.lbattrs = - uu___16; - FStar_Syntax_Syntax.lbpos = - uu___17;_}) - -> - let uu___18 = - FStar_Compiler_Effect.op_Bar_Greater - ml_lb.FStar_Extraction_ML_Syntax.mllb_meta - (FStar_Compiler_List.contains - FStar_Extraction_ML_Syntax.Erased) in - if uu___18 - then (env, ml_lbs) - else - (let lb_lid = - let uu___20 = - let uu___21 = - FStar_Compiler_Util.right - lbname in - uu___21.FStar_Syntax_Syntax.fv_name in - uu___20.FStar_Syntax_Syntax.v in - let flags'' = - let uu___20 = - let uu___21 = - FStar_Syntax_Subst.compress - t in - uu___21.FStar_Syntax_Syntax.n in - match uu___20 with - | FStar_Syntax_Syntax.Tm_arrow - { - FStar_Syntax_Syntax.bs1 - = uu___21; - FStar_Syntax_Syntax.comp - = - { - FStar_Syntax_Syntax.n - = - FStar_Syntax_Syntax.Comp - { - FStar_Syntax_Syntax.comp_univs - = uu___22; - FStar_Syntax_Syntax.effect_name - = e; - FStar_Syntax_Syntax.result_typ - = uu___23; - FStar_Syntax_Syntax.effect_args - = uu___24; - FStar_Syntax_Syntax.flags - = uu___25;_}; - FStar_Syntax_Syntax.pos - = uu___26; - FStar_Syntax_Syntax.vars - = uu___27; - FStar_Syntax_Syntax.hash_code - = uu___28;_};_} - when - let uu___29 = - FStar_Ident.string_of_lid - e in - uu___29 = - "FStar.HyperStack.ST.StackInline" - -> - [FStar_Extraction_ML_Syntax.StackInline] - | uu___21 -> [] in - let meta = - FStar_Compiler_List.op_At - flags - (FStar_Compiler_List.op_At - flags' flags'') in - let ml_lb1 = - { - FStar_Extraction_ML_Syntax.mllb_name - = - (ml_lb.FStar_Extraction_ML_Syntax.mllb_name); - FStar_Extraction_ML_Syntax.mllb_tysc - = - (ml_lb.FStar_Extraction_ML_Syntax.mllb_tysc); - FStar_Extraction_ML_Syntax.mllb_add_unit - = - (ml_lb.FStar_Extraction_ML_Syntax.mllb_add_unit); - FStar_Extraction_ML_Syntax.mllb_def - = - (ml_lb.FStar_Extraction_ML_Syntax.mllb_def); - FStar_Extraction_ML_Syntax.mllb_meta - = meta; - FStar_Extraction_ML_Syntax.print_typ - = - (ml_lb.FStar_Extraction_ML_Syntax.print_typ) - } in - let uu___20 = - let uu___21 = - FStar_Compiler_Effect.op_Bar_Greater - quals - (FStar_Compiler_Util.for_some - (fun uu___22 -> - match uu___22 with - | FStar_Syntax_Syntax.Projector - uu___23 -> - true - | uu___23 -> false)) in - if uu___21 - then - let uu___22 = - let uu___23 = - FStar_Compiler_Util.right - lbname in - let uu___24 = - FStar_Compiler_Util.must - ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc in - FStar_Extraction_ML_UEnv.extend_fv - env uu___23 uu___24 - ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit in - match uu___22 with - | (env1, mls, uu___23) -> - (env1, - { - FStar_Extraction_ML_Syntax.mllb_name - = mls; - FStar_Extraction_ML_Syntax.mllb_tysc - = - (ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc); - FStar_Extraction_ML_Syntax.mllb_add_unit - = - (ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit); - FStar_Extraction_ML_Syntax.mllb_def - = - (ml_lb1.FStar_Extraction_ML_Syntax.mllb_def); - FStar_Extraction_ML_Syntax.mllb_meta - = - (ml_lb1.FStar_Extraction_ML_Syntax.mllb_meta); - FStar_Extraction_ML_Syntax.print_typ - = - (ml_lb1.FStar_Extraction_ML_Syntax.print_typ) - }) - else - (let uu___23 = - let uu___24 = - FStar_Compiler_Util.must - ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc in - FStar_Extraction_ML_UEnv.extend_lb - env lbname t uu___24 - ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit in - match uu___23 with - | (env1, uu___24, - uu___25) -> - (env1, ml_lb1)) in - match uu___20 with - | (g1, ml_lb2) -> - (g1, (ml_lb2 :: ml_lbs)))) - (g, []) bindings - (FStar_Pervasives_Native.snd lbs) in - (match uu___10 with - | (g1, ml_lbs') -> - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = - FStar_Extraction_ML_Util.mlloc_of_range - se1.FStar_Syntax_Syntax.sigrng in - FStar_Extraction_ML_Syntax.MLM_Loc - uu___14 in - [uu___13; - FStar_Extraction_ML_Syntax.MLM_Let - (flavor, - (FStar_Compiler_List.rev ml_lbs'))] in - let uu___13 = - FStar_Extraction_ML_RegEmb.maybe_register_plugin - g1 se1 in - FStar_Compiler_List.op_At uu___12 uu___13 in - (g1, uu___11)) - | uu___9 -> - let uu___10 = - let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlexpr - uu___12 ml_let in - FStar_Compiler_Util.format1 - "Impossible: Translated a let to a non-let: %s" - uu___11 in - failwith uu___10)) + | FStar_Pervasives_Native.None -> extract_sig_let g se1 + | FStar_Pervasives_Native.Some (ext, blob, extractor) -> + let uu___7 = extractor g blob in + (match uu___7 with + | FStar_Pervasives.Inl (term, e_tag, ty) -> + let meta = + extract_metadata + se1.FStar_Syntax_Syntax.sigattrs in + let ty1 = + FStar_Extraction_ML_Term.term_as_mlty g + lb.FStar_Syntax_Syntax.lbtyp in + let tysc = ([], ty1) in + let uu___8 = + FStar_Extraction_ML_UEnv.extend_lb g + lb.FStar_Syntax_Syntax.lbname + lb.FStar_Syntax_Syntax.lbtyp tysc false in + (match uu___8 with + | (g1, mlid, uu___9) -> + let mllet = + FStar_Extraction_ML_Syntax.MLM_Let + (FStar_Extraction_ML_Syntax.NonRec, + [{ + FStar_Extraction_ML_Syntax.mllb_name + = mlid; + FStar_Extraction_ML_Syntax.mllb_tysc + = + (FStar_Pervasives_Native.Some + tysc); + FStar_Extraction_ML_Syntax.mllb_add_unit + = false; + FStar_Extraction_ML_Syntax.mllb_def + = term; + FStar_Extraction_ML_Syntax.mllb_meta + = meta; + FStar_Extraction_ML_Syntax.print_typ + = false + }]) in + (g1, [mllet])) + | FStar_Pervasives.Inr err -> + let uu___8 = + let uu___9 = + FStar_Compiler_Util.format2 + "Extension %s failed to extract term: %s" + ext err in + (FStar_Errors_Codes.Fatal_ExtractionUnsupported, + uu___9) in + FStar_Errors.raise_error uu___8 + se1.FStar_Syntax_Syntax.sigrng)) + | FStar_Syntax_Syntax.Sig_let uu___5 -> extract_sig_let g se1 | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = uu___5; @@ -2730,6 +2340,464 @@ let rec (extract_sig : (FStar_Syntax_Util.process_pragma p se1.FStar_Syntax_Syntax.sigrng; (g, []))))) +and (extract_sig_let : + FStar_Extraction_ML_UEnv.uenv -> + FStar_Syntax_Syntax.sigelt -> + (FStar_Extraction_ML_UEnv.uenv * FStar_Extraction_ML_Syntax.mlmodule1 + Prims.list)) + = + fun g -> + fun se -> + if + Prims.op_Negation + (FStar_Syntax_Syntax.uu___is_Sig_let se.FStar_Syntax_Syntax.sigel) + then failwith "Impossible: should only be called with Sig_let" + else + (let uu___1 = se.FStar_Syntax_Syntax.sigel in + match uu___1 with + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = lbs; + FStar_Syntax_Syntax.lids1 = uu___2;_} + -> + let attrs = se.FStar_Syntax_Syntax.sigattrs in + let quals = se.FStar_Syntax_Syntax.sigquals in + let maybe_postprocess_lbs lbs1 = + let post_tau = + let uu___3 = + FStar_Syntax_Util.extract_attr' + FStar_Parser_Const.postprocess_extr_with attrs in + match uu___3 with + | FStar_Pervasives_Native.None -> + FStar_Pervasives_Native.None + | FStar_Pervasives_Native.Some + (uu___4, (tau, FStar_Pervasives_Native.None)::uu___5) -> + FStar_Pervasives_Native.Some tau + | FStar_Pervasives_Native.Some uu___4 -> + (FStar_Errors.log_issue se.FStar_Syntax_Syntax.sigrng + (FStar_Errors_Codes.Warning_UnrecognizedAttribute, + "Ill-formed application of 'postprocess_for_extraction_with'"); + FStar_Pervasives_Native.None) in + let postprocess_lb tau lb = + let env = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + let lbdef = + let uu___3 = + let uu___4 = + let uu___5 = FStar_TypeChecker_Env.current_module env in + FStar_Ident.string_of_lid uu___5 in + FStar_Pervasives_Native.Some uu___4 in + FStar_Profiling.profile + (fun uu___4 -> + FStar_TypeChecker_Env.postprocess env tau + lb.FStar_Syntax_Syntax.lbtyp + lb.FStar_Syntax_Syntax.lbdef) uu___3 + "FStar.Extraction.ML.Module.post_process_for_extraction" in + { + FStar_Syntax_Syntax.lbname = + (lb.FStar_Syntax_Syntax.lbname); + FStar_Syntax_Syntax.lbunivs = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.lbtyp = (lb.FStar_Syntax_Syntax.lbtyp); + FStar_Syntax_Syntax.lbeff = (lb.FStar_Syntax_Syntax.lbeff); + FStar_Syntax_Syntax.lbdef = lbdef; + FStar_Syntax_Syntax.lbattrs = + (lb.FStar_Syntax_Syntax.lbattrs); + FStar_Syntax_Syntax.lbpos = (lb.FStar_Syntax_Syntax.lbpos) + } in + match post_tau with + | FStar_Pervasives_Native.None -> lbs1 + | FStar_Pervasives_Native.Some tau -> + let uu___3 = + FStar_Compiler_List.map (postprocess_lb tau) + (FStar_Pervasives_Native.snd lbs1) in + ((FStar_Pervasives_Native.fst lbs1), uu___3) in + let maybe_normalize_for_extraction lbs1 = + let norm_steps = + let uu___3 = + FStar_Syntax_Util.extract_attr' + FStar_Parser_Const.normalize_for_extraction_lid attrs in + match uu___3 with + | FStar_Pervasives_Native.None -> + FStar_Pervasives_Native.None + | FStar_Pervasives_Native.Some + (uu___4, (steps, FStar_Pervasives_Native.None)::uu___5) + -> + let steps1 = + let uu___6 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Zeta; + FStar_TypeChecker_Env.Iota; + FStar_TypeChecker_Env.Primops] uu___6 steps in + let uu___6 = + let uu___7 = + FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_norm_step in + FStar_TypeChecker_Cfg.try_unembed_simple uu___7 steps1 in + (match uu___6 with + | FStar_Pervasives_Native.Some steps2 -> + let uu___7 = + FStar_TypeChecker_Cfg.translate_norm_steps steps2 in + FStar_Pervasives_Native.Some uu___7 + | uu___7 -> + ((let uu___9 = + let uu___10 = + let uu___11 = + FStar_Syntax_Print.term_to_string steps1 in + FStar_Compiler_Util.format1 + "Ill-formed application of 'normalize_for_extraction': normalization steps '%s' could not be interpreted" + uu___11 in + (FStar_Errors_Codes.Warning_UnrecognizedAttribute, + uu___10) in + FStar_Errors.log_issue + se.FStar_Syntax_Syntax.sigrng uu___9); + FStar_Pervasives_Native.None)) + | FStar_Pervasives_Native.Some uu___4 -> + (FStar_Errors.log_issue se.FStar_Syntax_Syntax.sigrng + (FStar_Errors_Codes.Warning_UnrecognizedAttribute, + "Ill-formed application of 'normalize_for_extraction'"); + FStar_Pervasives_Native.None) in + let norm_one_lb steps lb = + let env = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + let env1 = + { + FStar_TypeChecker_Env.solver = + (env.FStar_TypeChecker_Env.solver); + FStar_TypeChecker_Env.range = + (env.FStar_TypeChecker_Env.range); + FStar_TypeChecker_Env.curmodule = + (env.FStar_TypeChecker_Env.curmodule); + FStar_TypeChecker_Env.gamma = + (env.FStar_TypeChecker_Env.gamma); + FStar_TypeChecker_Env.gamma_sig = + (env.FStar_TypeChecker_Env.gamma_sig); + FStar_TypeChecker_Env.gamma_cache = + (env.FStar_TypeChecker_Env.gamma_cache); + FStar_TypeChecker_Env.modules = + (env.FStar_TypeChecker_Env.modules); + FStar_TypeChecker_Env.expected_typ = + (env.FStar_TypeChecker_Env.expected_typ); + FStar_TypeChecker_Env.sigtab = + (env.FStar_TypeChecker_Env.sigtab); + FStar_TypeChecker_Env.attrtab = + (env.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp = + (env.FStar_TypeChecker_Env.instantiate_imp); + FStar_TypeChecker_Env.effects = + (env.FStar_TypeChecker_Env.effects); + FStar_TypeChecker_Env.generalize = + (env.FStar_TypeChecker_Env.generalize); + FStar_TypeChecker_Env.letrecs = + (env.FStar_TypeChecker_Env.letrecs); + FStar_TypeChecker_Env.top_level = + (env.FStar_TypeChecker_Env.top_level); + FStar_TypeChecker_Env.check_uvars = + (env.FStar_TypeChecker_Env.check_uvars); + FStar_TypeChecker_Env.use_eq_strict = + (env.FStar_TypeChecker_Env.use_eq_strict); + FStar_TypeChecker_Env.is_iface = + (env.FStar_TypeChecker_Env.is_iface); + FStar_TypeChecker_Env.admit = + (env.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = + (env.FStar_TypeChecker_Env.lax); + FStar_TypeChecker_Env.lax_universes = + (env.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = + (env.FStar_TypeChecker_Env.phase1); + FStar_TypeChecker_Env.failhard = + (env.FStar_TypeChecker_Env.failhard); + FStar_TypeChecker_Env.nosynth = + (env.FStar_TypeChecker_Env.nosynth); + FStar_TypeChecker_Env.uvar_subtyping = + (env.FStar_TypeChecker_Env.uvar_subtyping); + FStar_TypeChecker_Env.intactics = + (env.FStar_TypeChecker_Env.intactics); + FStar_TypeChecker_Env.nocoerce = + (env.FStar_TypeChecker_Env.nocoerce); + FStar_TypeChecker_Env.tc_term = + (env.FStar_TypeChecker_Env.tc_term); + FStar_TypeChecker_Env.typeof_tot_or_gtot_term = + (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + FStar_TypeChecker_Env.universe_of = + (env.FStar_TypeChecker_Env.universe_of); + FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term + = + (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + FStar_TypeChecker_Env.teq_nosmt_force = + (env.FStar_TypeChecker_Env.teq_nosmt_force); + FStar_TypeChecker_Env.subtype_nosmt_force = + (env.FStar_TypeChecker_Env.subtype_nosmt_force); + FStar_TypeChecker_Env.qtbl_name_and_index = + (env.FStar_TypeChecker_Env.qtbl_name_and_index); + FStar_TypeChecker_Env.normalized_eff_names = + (env.FStar_TypeChecker_Env.normalized_eff_names); + FStar_TypeChecker_Env.fv_delta_depths = + (env.FStar_TypeChecker_Env.fv_delta_depths); + FStar_TypeChecker_Env.proof_ns = + (env.FStar_TypeChecker_Env.proof_ns); + FStar_TypeChecker_Env.synth_hook = + (env.FStar_TypeChecker_Env.synth_hook); + FStar_TypeChecker_Env.try_solve_implicits_hook = + (env.FStar_TypeChecker_Env.try_solve_implicits_hook); + FStar_TypeChecker_Env.splice = + (env.FStar_TypeChecker_Env.splice); + FStar_TypeChecker_Env.mpreprocess = + (env.FStar_TypeChecker_Env.mpreprocess); + FStar_TypeChecker_Env.postprocess = + (env.FStar_TypeChecker_Env.postprocess); + FStar_TypeChecker_Env.identifier_info = + (env.FStar_TypeChecker_Env.identifier_info); + FStar_TypeChecker_Env.tc_hooks = + (env.FStar_TypeChecker_Env.tc_hooks); + FStar_TypeChecker_Env.dsenv = + (env.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = + (env.FStar_TypeChecker_Env.nbe); + FStar_TypeChecker_Env.strict_args_tab = + (env.FStar_TypeChecker_Env.strict_args_tab); + FStar_TypeChecker_Env.erasable_types_tab = + (env.FStar_TypeChecker_Env.erasable_types_tab); + FStar_TypeChecker_Env.enable_defer_to_tac = + (env.FStar_TypeChecker_Env.enable_defer_to_tac); + FStar_TypeChecker_Env.unif_allow_ref_guards = + (env.FStar_TypeChecker_Env.unif_allow_ref_guards); + FStar_TypeChecker_Env.erase_erasable_args = true; + FStar_TypeChecker_Env.core_check = + (env.FStar_TypeChecker_Env.core_check) + } in + let lbd = + let uu___3 = + let uu___4 = + let uu___5 = FStar_TypeChecker_Env.current_module env1 in + FStar_Ident.string_of_lid uu___5 in + FStar_Pervasives_Native.Some uu___4 in + FStar_Profiling.profile + (fun uu___4 -> + FStar_TypeChecker_Normalize.normalize steps env1 + lb.FStar_Syntax_Syntax.lbdef) uu___3 + "FStar.Extraction.ML.Module.normalize_for_extraction" in + { + FStar_Syntax_Syntax.lbname = + (lb.FStar_Syntax_Syntax.lbname); + FStar_Syntax_Syntax.lbunivs = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.lbtyp = (lb.FStar_Syntax_Syntax.lbtyp); + FStar_Syntax_Syntax.lbeff = (lb.FStar_Syntax_Syntax.lbeff); + FStar_Syntax_Syntax.lbdef = lbd; + FStar_Syntax_Syntax.lbattrs = + (lb.FStar_Syntax_Syntax.lbattrs); + FStar_Syntax_Syntax.lbpos = (lb.FStar_Syntax_Syntax.lbpos) + } in + match norm_steps with + | FStar_Pervasives_Native.None -> lbs1 + | FStar_Pervasives_Native.Some steps -> + let uu___3 = + FStar_Compiler_List.map (norm_one_lb steps) + (FStar_Pervasives_Native.snd lbs1) in + ((FStar_Pervasives_Native.fst lbs1), uu___3) in + let uu___3 = + let lbs1 = + let uu___4 = maybe_postprocess_lbs lbs in + maybe_normalize_for_extraction uu___4 in + let uu___4 = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_let + { + FStar_Syntax_Syntax.lbs = lbs1; + FStar_Syntax_Syntax.body1 = + FStar_Syntax_Util.exp_false_bool + }) se.FStar_Syntax_Syntax.sigrng in + FStar_Extraction_ML_Term.term_as_mlexpr g uu___4 in + (match uu___3 with + | (ml_let, uu___4, uu___5) -> + (match ml_let.FStar_Extraction_ML_Syntax.expr with + | FStar_Extraction_ML_Syntax.MLE_Let + ((flavor, bindings), uu___6) -> + let flags = + FStar_Compiler_List.choose flag_of_qual quals in + let flags' = extract_metadata attrs in + let uu___7 = + FStar_Compiler_List.fold_left2 + (fun uu___8 -> + fun ml_lb -> + fun uu___9 -> + match (uu___8, uu___9) with + | ((env, ml_lbs), + { FStar_Syntax_Syntax.lbname = lbname; + FStar_Syntax_Syntax.lbunivs = uu___10; + FStar_Syntax_Syntax.lbtyp = t; + FStar_Syntax_Syntax.lbeff = uu___11; + FStar_Syntax_Syntax.lbdef = uu___12; + FStar_Syntax_Syntax.lbattrs = uu___13; + FStar_Syntax_Syntax.lbpos = uu___14;_}) + -> + let uu___15 = + FStar_Compiler_Effect.op_Bar_Greater + ml_lb.FStar_Extraction_ML_Syntax.mllb_meta + (FStar_Compiler_List.contains + FStar_Extraction_ML_Syntax.Erased) in + if uu___15 + then (env, ml_lbs) + else + (let lb_lid = + let uu___17 = + let uu___18 = + FStar_Compiler_Util.right + lbname in + uu___18.FStar_Syntax_Syntax.fv_name in + uu___17.FStar_Syntax_Syntax.v in + let flags'' = + let uu___17 = + let uu___18 = + FStar_Syntax_Subst.compress t in + uu___18.FStar_Syntax_Syntax.n in + match uu___17 with + | FStar_Syntax_Syntax.Tm_arrow + { + FStar_Syntax_Syntax.bs1 = + uu___18; + FStar_Syntax_Syntax.comp = + { + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Comp + { + FStar_Syntax_Syntax.comp_univs + = uu___19; + FStar_Syntax_Syntax.effect_name + = e; + FStar_Syntax_Syntax.result_typ + = uu___20; + FStar_Syntax_Syntax.effect_args + = uu___21; + FStar_Syntax_Syntax.flags + = uu___22;_}; + FStar_Syntax_Syntax.pos + = uu___23; + FStar_Syntax_Syntax.vars + = uu___24; + FStar_Syntax_Syntax.hash_code + = uu___25;_};_} + when + let uu___26 = + FStar_Ident.string_of_lid e in + uu___26 = + "FStar.HyperStack.ST.StackInline" + -> + [FStar_Extraction_ML_Syntax.StackInline] + | uu___18 -> [] in + let meta = + FStar_Compiler_List.op_At flags + (FStar_Compiler_List.op_At + flags' flags'') in + let ml_lb1 = + { + FStar_Extraction_ML_Syntax.mllb_name + = + (ml_lb.FStar_Extraction_ML_Syntax.mllb_name); + FStar_Extraction_ML_Syntax.mllb_tysc + = + (ml_lb.FStar_Extraction_ML_Syntax.mllb_tysc); + FStar_Extraction_ML_Syntax.mllb_add_unit + = + (ml_lb.FStar_Extraction_ML_Syntax.mllb_add_unit); + FStar_Extraction_ML_Syntax.mllb_def + = + (ml_lb.FStar_Extraction_ML_Syntax.mllb_def); + FStar_Extraction_ML_Syntax.mllb_meta + = meta; + FStar_Extraction_ML_Syntax.print_typ + = + (ml_lb.FStar_Extraction_ML_Syntax.print_typ) + } in + let uu___17 = + let uu___18 = + FStar_Compiler_Effect.op_Bar_Greater + quals + (FStar_Compiler_Util.for_some + (fun uu___19 -> + match uu___19 with + | FStar_Syntax_Syntax.Projector + uu___20 -> true + | uu___20 -> false)) in + if uu___18 + then + let uu___19 = + let uu___20 = + FStar_Compiler_Util.right + lbname in + let uu___21 = + FStar_Compiler_Util.must + ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc in + FStar_Extraction_ML_UEnv.extend_fv + env uu___20 uu___21 + ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit in + match uu___19 with + | (env1, mls, uu___20) -> + (env1, + { + FStar_Extraction_ML_Syntax.mllb_name + = mls; + FStar_Extraction_ML_Syntax.mllb_tysc + = + (ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc); + FStar_Extraction_ML_Syntax.mllb_add_unit + = + (ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit); + FStar_Extraction_ML_Syntax.mllb_def + = + (ml_lb1.FStar_Extraction_ML_Syntax.mllb_def); + FStar_Extraction_ML_Syntax.mllb_meta + = + (ml_lb1.FStar_Extraction_ML_Syntax.mllb_meta); + FStar_Extraction_ML_Syntax.print_typ + = + (ml_lb1.FStar_Extraction_ML_Syntax.print_typ) + }) + else + (let uu___20 = + let uu___21 = + FStar_Compiler_Util.must + ml_lb1.FStar_Extraction_ML_Syntax.mllb_tysc in + FStar_Extraction_ML_UEnv.extend_lb + env lbname t uu___21 + ml_lb1.FStar_Extraction_ML_Syntax.mllb_add_unit in + match uu___20 with + | (env1, uu___21, uu___22) -> + (env1, ml_lb1)) in + match uu___17 with + | (g1, ml_lb2) -> + (g1, (ml_lb2 :: ml_lbs)))) + (g, []) bindings (FStar_Pervasives_Native.snd lbs) in + (match uu___7 with + | (g1, ml_lbs') -> + let uu___8 = + 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 + [uu___10; + FStar_Extraction_ML_Syntax.MLM_Let + (flavor, (FStar_Compiler_List.rev ml_lbs'))] in + let uu___10 = + FStar_Extraction_ML_RegEmb.maybe_register_plugin + g1 se in + FStar_Compiler_List.op_At uu___9 uu___10 in + (g1, uu___8)) + | uu___6 -> + let uu___7 = + 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 + ml_let in + FStar_Compiler_Util.format1 + "Impossible: Translated a let to a non-let: %s" + uu___8 in + failwith uu___7))) let (extract' : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.modul -> diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index f8c3c943bbb..a9e5e7c1def 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -733,4 +733,229 @@ let (pop_unit : mltyscheme -> mltyscheme) = if l = ml_unit_ty then (vs, t) else failwith "unexpected: pop_unit: domain was not unit" - | uu___1 -> failwith "unexpected: pop_unit: not a function type") \ No newline at end of file + | uu___1 -> failwith "unexpected: pop_unit: not a function type") +let (mlpath_to_string : + (Prims.string Prims.list * Prims.string) -> Prims.string) = + fun mlp -> + Prims.op_Hat (FStar_String.concat "." (FStar_Pervasives_Native.fst mlp)) + (Prims.op_Hat "." (FStar_Pervasives_Native.snd mlp)) +let rec (mlty_to_string : mlty -> Prims.string) = + fun t -> + match t with + | MLTY_Var v -> v + | MLTY_Fun (t1, uu___, t2) -> + let uu___1 = mlty_to_string t1 in + let uu___2 = mlty_to_string t2 in + FStar_Compiler_Util.format2 "(%s -> %s)" uu___1 uu___2 + | MLTY_Named (ts, p) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlty_to_string ts in + FStar_String.concat " " uu___1 in + FStar_Compiler_Util.format2 "(%s %s)" uu___ (mlpath_to_string p) + | MLTY_Tuple ts -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlty_to_string ts in + FStar_String.concat " * " uu___1 in + FStar_Compiler_Util.format1 "(%s)" uu___ + | MLTY_Top -> "MLTY_Top" + | MLTY_Erased -> "MLTY_Erased" +let rec (mlexpr_to_string : mlexpr -> Prims.string) = + fun e -> + match e.expr with + | MLE_Const c -> + let uu___ = mlconstant_to_string c in + FStar_Compiler_Util.format1 "(MLE_Const %s)" uu___ + | MLE_Var x -> FStar_Compiler_Util.format1 "(MLE_Var %s)" x + | MLE_Name (p, x) -> + FStar_Compiler_Util.format2 "(MLE_Name (%s, %s))" + (FStar_String.concat "." p) x + | MLE_Let (lbs, e1) -> + let uu___ = mlletbinding_to_string lbs in + let uu___1 = mlexpr_to_string e1 in + FStar_Compiler_Util.format2 "(MLE_Let (%s, %s))" uu___ uu___1 + | MLE_App (e1, es) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = + let uu___2 = FStar_Compiler_List.map mlexpr_to_string es in + FStar_String.concat "; " uu___2 in + FStar_Compiler_Util.format2 "(MLE_App (%s, [%s]))" uu___ uu___1 + | MLE_TApp (e1, ts) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = + let uu___2 = FStar_Compiler_List.map mlty_to_string ts in + FStar_String.concat "; " uu___2 in + FStar_Compiler_Util.format2 "(MLE_TApp (%s, [%s]))" uu___ uu___1 + | MLE_Fun (xs, 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 + FStar_String.concat "; " uu___1 in + let uu___1 = mlexpr_to_string e1 in + FStar_Compiler_Util.format2 "(MLE_Fun ([%s], %s))" uu___ uu___1 + | MLE_Match (e1, bs) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = + let uu___2 = FStar_Compiler_List.map mlbranch_to_string bs in + FStar_String.concat "; " uu___2 in + FStar_Compiler_Util.format2 "(MLE_Match (%s, [%s]))" uu___ uu___1 + | MLE_Coerce (e1, t1, t2) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = mlty_to_string t1 in + let uu___2 = mlty_to_string t2 in + FStar_Compiler_Util.format3 "(MLE_Coerce (%s, %s, %s))" uu___ uu___1 + uu___2 + | MLE_CTor (p, es) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlexpr_to_string es in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format2 "(MLE_CTor (%s, [%s]))" + (mlpath_to_string p) uu___ + | MLE_Seq es -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlexpr_to_string es in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(MLE_Seq [%s])" uu___ + | MLE_Tuple es -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlexpr_to_string es in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(MLE_Tuple [%s])" uu___ + | MLE_Record (p, es) -> + let uu___ = + let uu___1 = + FStar_Compiler_List.map + (fun uu___2 -> + match uu___2 with + | (x, e1) -> + let uu___3 = mlexpr_to_string e1 in + FStar_Compiler_Util.format2 "(%s, %s)" x uu___3) es in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format2 "(MLE_Record (%s, [%s]))" + (FStar_String.concat "; " p) uu___ + | MLE_Proj (e1, p) -> + let uu___ = mlexpr_to_string e1 in + FStar_Compiler_Util.format2 "(MLE_Proj (%s, %s))" uu___ + (mlpath_to_string p) + | MLE_If (e1, e2, FStar_Pervasives_Native.None) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = mlexpr_to_string e2 in + FStar_Compiler_Util.format2 "(MLE_If (%s, %s, None))" uu___ uu___1 + | MLE_If (e1, e2, FStar_Pervasives_Native.Some e3) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = mlexpr_to_string e2 in + let uu___2 = mlexpr_to_string e3 in + FStar_Compiler_Util.format3 "(MLE_If (%s, %s, %s))" uu___ uu___1 + uu___2 + | MLE_Raise (p, es) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlexpr_to_string es in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format2 "(MLE_Raise (%s, [%s]))" + (mlpath_to_string p) uu___ + | MLE_Try (e1, bs) -> + let uu___ = mlexpr_to_string e1 in + let uu___1 = + let uu___2 = FStar_Compiler_List.map mlbranch_to_string bs in + FStar_String.concat "; " uu___2 in + FStar_Compiler_Util.format2 "(MLE_Try (%s, [%s]))" uu___ uu___1 +and (mlbranch_to_string : + (mlpattern * mlexpr FStar_Pervasives_Native.option * mlexpr) -> + Prims.string) + = + fun uu___ -> + match uu___ with + | (p, e1, e2) -> + (match e1 with + | FStar_Pervasives_Native.None -> + let uu___1 = mlpattern_to_string p in + let uu___2 = mlexpr_to_string e2 in + FStar_Compiler_Util.format2 "(%s, None, %s)" uu___1 uu___2 + | FStar_Pervasives_Native.Some e11 -> + let uu___1 = mlpattern_to_string p in + let uu___2 = mlexpr_to_string e11 in + let uu___3 = mlexpr_to_string e2 in + FStar_Compiler_Util.format3 "(%s, Some %s, %s)" uu___1 uu___2 + uu___3) +and (mlletbinding_to_string : + (mlletflavor * mllb Prims.list) -> Prims.string) = + fun lbs -> + match lbs with + | (Rec, lbs1) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mllb_to_string lbs1 in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(Rec, [%s])" uu___ + | (NonRec, lbs1) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mllb_to_string lbs1 in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(NonRec, [%s])" uu___ +and (mllb_to_string : mllb -> Prims.string) = + fun lb -> + let uu___ = + match lb.mllb_tysc with + | FStar_Pervasives_Native.None -> "None" + | FStar_Pervasives_Native.Some (uu___1, t) -> + let uu___2 = mlty_to_string t in + FStar_Compiler_Util.format1 "Some %s" uu___2 in + let uu___1 = FStar_Compiler_Util.string_of_bool lb.mllb_add_unit in + let uu___2 = mlexpr_to_string lb.mllb_def in + FStar_Compiler_Util.format4 + "{mllb_name = %s; mllb_tysc = %s; mllb_add_unit = %s; mllb_def = %s}" + lb.mllb_name uu___ uu___1 uu___2 +and (mlconstant_to_string : mlconstant -> Prims.string) = + fun mlc -> + match mlc with + | MLC_Unit -> "MLC_Unit" + | MLC_Bool b -> + let uu___ = FStar_Compiler_Util.string_of_bool b in + FStar_Compiler_Util.format1 "(MLC_Bool %s)" uu___ + | MLC_Int (s, FStar_Pervasives_Native.None) -> + FStar_Compiler_Util.format1 "(MLC_Int %s)" s + | MLC_Int (s, FStar_Pervasives_Native.Some (s1, s2)) -> + FStar_Compiler_Util.format1 "(MLC_Int (%s, _, _))" s + | MLC_Float f -> "(MLC_Float _)" + | MLC_Char c -> "(MLC_Char _)" + | MLC_String s -> FStar_Compiler_Util.format1 "(MLC_String %s)" s + | MLC_Bytes b -> "(MLC_Bytes _)" +and (mlpattern_to_string : mlpattern -> Prims.string) = + fun mlp -> + match mlp with + | MLP_Wild -> "MLP_Wild" + | MLP_Const c -> + let uu___ = mlconstant_to_string c in + FStar_Compiler_Util.format1 "(MLP_Const %s)" uu___ + | MLP_Var x -> FStar_Compiler_Util.format1 "(MLP_Var %s)" x + | MLP_CTor (p, ps) -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlpattern_to_string ps in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format2 "(MLP_CTor (%s, [%s]))" + (mlpath_to_string p) uu___ + | MLP_Branch ps -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlpattern_to_string ps in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(MLP_Branch [%s])" uu___ + | MLP_Record (p, ps) -> + let uu___ = + let uu___1 = + FStar_Compiler_List.map + (fun uu___2 -> + match uu___2 with + | (x, p1) -> + let uu___3 = mlpattern_to_string p1 in + FStar_Compiler_Util.format2 "(%s, %s)" x uu___3) ps in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format2 "(MLP_Record (%s, [%s]))" + (FStar_String.concat "; " p) uu___ + | MLP_Tuple ps -> + let uu___ = + let uu___1 = FStar_Compiler_List.map mlpattern_to_string ps in + FStar_String.concat "; " uu___1 in + FStar_Compiler_Util.format1 "(MLP_Tuple [%s])" uu___ \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 4079e6eb72e..c1399521af5 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -211,21 +211,24 @@ let (effect_as_etag : else FStar_Extraction_ML_Syntax.E_IMPURE | FStar_Pervasives_Native.None -> FStar_Extraction_ML_Syntax.E_IMPURE)) -let rec (is_arity : - FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> Prims.bool) = - fun env -> +let rec (is_arity_aux : + FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> Prims.bool) = + fun tcenv -> fun t -> let t1 = FStar_Syntax_Util.unmeta t in let uu___ = let uu___1 = FStar_Syntax_Subst.compress t1 in uu___1.FStar_Syntax_Syntax.n in match uu___ with - | FStar_Syntax_Syntax.Tm_unknown -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_delayed uu___1 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_ascribed uu___1 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_meta uu___1 -> failwith "Impossible" + | FStar_Syntax_Syntax.Tm_unknown -> failwith "Impossible: is_arity" + | FStar_Syntax_Syntax.Tm_delayed uu___1 -> + failwith "Impossible: is_arity" + | FStar_Syntax_Syntax.Tm_ascribed uu___1 -> + failwith "Impossible: is_arity" + | FStar_Syntax_Syntax.Tm_meta uu___1 -> failwith "Impossible: is_arity" | FStar_Syntax_Syntax.Tm_lazy i -> - let uu___1 = FStar_Syntax_Util.unfold_lazy i in is_arity env uu___1 + let uu___1 = FStar_Syntax_Util.unfold_lazy i in + is_arity_aux tcenv uu___1 | FStar_Syntax_Syntax.Tm_uvar uu___1 -> false | FStar_Syntax_Syntax.Tm_constant uu___1 -> false | FStar_Syntax_Syntax.Tm_name uu___1 -> false @@ -234,32 +237,33 @@ let rec (is_arity : | FStar_Syntax_Syntax.Tm_type uu___1 -> true | FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = uu___1; FStar_Syntax_Syntax.comp = c;_} - -> is_arity env (FStar_Syntax_Util.comp_result c) + -> is_arity_aux tcenv (FStar_Syntax_Util.comp_result c) | FStar_Syntax_Syntax.Tm_fvar fv -> let topt = - let uu___1 = FStar_Extraction_ML_UEnv.tcenv_of_uenv env in FStar_TypeChecker_Env.lookup_definition [FStar_TypeChecker_Env.Unfold - FStar_Syntax_Syntax.delta_constant] uu___1 + FStar_Syntax_Syntax.delta_constant] tcenv (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in (match topt with | FStar_Pervasives_Native.None -> false - | FStar_Pervasives_Native.Some (uu___1, t2) -> is_arity env t2) + | FStar_Pervasives_Native.Some (uu___1, t2) -> + is_arity_aux tcenv t2) | FStar_Syntax_Syntax.Tm_app uu___1 -> let uu___2 = FStar_Syntax_Util.head_and_args t1 in - (match uu___2 with | (head, uu___3) -> is_arity env head) - | FStar_Syntax_Syntax.Tm_uinst (head, uu___1) -> is_arity env head + (match uu___2 with | (head, uu___3) -> is_arity_aux tcenv head) + | FStar_Syntax_Syntax.Tm_uinst (head, uu___1) -> + is_arity_aux tcenv head | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = uu___1;_} -> - is_arity env x.FStar_Syntax_Syntax.sort + is_arity_aux tcenv x.FStar_Syntax_Syntax.sort | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = uu___1; FStar_Syntax_Syntax.body = body; FStar_Syntax_Syntax.rc_opt = uu___2;_} - -> is_arity env body + -> is_arity_aux tcenv body | FStar_Syntax_Syntax.Tm_let { FStar_Syntax_Syntax.lbs = uu___1; FStar_Syntax_Syntax.body1 = body;_} - -> is_arity env body + -> is_arity_aux tcenv body | FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = uu___1; FStar_Syntax_Syntax.ret_opt = uu___2; @@ -267,8 +271,23 @@ let rec (is_arity : FStar_Syntax_Syntax.rc_opt1 = uu___3;_} -> (match branches with - | (uu___4, uu___5, e)::uu___6 -> is_arity env e + | (uu___4, uu___5, e)::uu___6 -> is_arity_aux tcenv e | uu___4 -> false) +let (is_arity : + FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> Prims.bool) = + fun env -> + fun t -> + let uu___ = FStar_Extraction_ML_UEnv.tcenv_of_uenv env in + is_arity_aux uu___ t +let (push_tcenv_binders : + FStar_Extraction_ML_UEnv.uenv -> + FStar_Syntax_Syntax.binders -> FStar_Extraction_ML_UEnv.uenv) + = + fun u -> + fun bs -> + let tcenv = FStar_Extraction_ML_UEnv.tcenv_of_uenv u in + let tcenv1 = FStar_TypeChecker_Env.push_binders tcenv bs in + FStar_Extraction_ML_UEnv.set_tcenv u tcenv1 let rec (is_type_aux : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> Prims.bool) = fun env -> @@ -305,11 +324,17 @@ let rec (is_type_aux : FStar_Syntax_Syntax.index = uu___1; FStar_Syntax_Syntax.sort = t2;_} -> is_arity env t2 - | FStar_Syntax_Syntax.Tm_name - { FStar_Syntax_Syntax.ppname = uu___; - FStar_Syntax_Syntax.index = uu___1; - FStar_Syntax_Syntax.sort = t2;_} - -> is_arity env t2 + | FStar_Syntax_Syntax.Tm_name x -> + let g = FStar_Extraction_ML_UEnv.tcenv_of_uenv env in + let uu___ = FStar_TypeChecker_Env.try_lookup_bv g x in + (match uu___ with + | FStar_Pervasives_Native.Some (t2, uu___1) -> is_arity env t2 + | uu___1 -> + let uu___2 = + let uu___3 = FStar_Syntax_Print.tag_of_term t1 in + FStar_Compiler_Util.format1 + "Extraction: variable not found: %s" uu___3 in + failwith uu___2) | FStar_Syntax_Syntax.Tm_ascribed { FStar_Syntax_Syntax.tm = t2; FStar_Syntax_Syntax.asc = uu___; FStar_Syntax_Syntax.eff_opt = uu___1;_} @@ -320,7 +345,10 @@ let rec (is_type_aux : FStar_Syntax_Syntax.rc_opt = uu___;_} -> let uu___1 = FStar_Syntax_Subst.open_term bs body in - (match uu___1 with | (uu___2, body1) -> is_type_aux env body1) + (match uu___1 with + | (bs1, body1) -> + let env1 = push_tcenv_binders env bs1 in + is_type_aux env1 body1) | FStar_Syntax_Syntax.Tm_let { FStar_Syntax_Syntax.lbs = (false, lb::[]); FStar_Syntax_Syntax.body1 = body;_} @@ -330,13 +358,26 @@ let rec (is_type_aux : let uu___1 = let uu___2 = FStar_Syntax_Syntax.mk_binder x in [uu___2] in FStar_Syntax_Subst.open_term uu___1 body in - (match uu___ with | (uu___1, body1) -> is_type_aux env body1) + (match uu___ with + | (bs, body1) -> + let env1 = push_tcenv_binders env bs in is_type_aux env1 body1) | FStar_Syntax_Syntax.Tm_let { FStar_Syntax_Syntax.lbs = (uu___, lbs); FStar_Syntax_Syntax.body1 = body;_} -> let uu___1 = FStar_Syntax_Subst.open_let_rec lbs body in - (match uu___1 with | (uu___2, body1) -> is_type_aux env body1) + (match uu___1 with + | (lbs1, body1) -> + let env1 = + let uu___2 = + FStar_Compiler_List.map + (fun lb -> + let uu___3 = + FStar_Compiler_Util.left + lb.FStar_Syntax_Syntax.lbname in + FStar_Syntax_Syntax.mk_binder uu___3) lbs1 in + push_tcenv_binders env uu___2 in + is_type_aux env1 body1) | FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = uu___; FStar_Syntax_Syntax.ret_opt = uu___1; @@ -346,7 +387,20 @@ let rec (is_type_aux : (match branches with | b::uu___3 -> let uu___4 = FStar_Syntax_Subst.open_branch b in - (match uu___4 with | (uu___5, uu___6, e) -> is_type_aux env e) + (match uu___4 with + | (pat, uu___5, e) -> + let uu___6 = + let uu___7 = FStar_Extraction_ML_UEnv.tcenv_of_uenv env in + FStar_TypeChecker_PatternUtils.raw_pat_as_exp uu___7 + pat in + (match uu___6 with + | FStar_Pervasives_Native.None -> false + | FStar_Pervasives_Native.Some (uu___7, bvs) -> + let binders = + FStar_Compiler_List.map + (fun bv -> FStar_Syntax_Syntax.mk_binder bv) bvs in + let env1 = push_tcenv_binders env binders in + is_type_aux env1 e)) | uu___3 -> false) | FStar_Syntax_Syntax.Tm_quoted uu___ -> false | FStar_Syntax_Syntax.Tm_meta @@ -1006,6 +1060,14 @@ let (extraction_norm_steps : FStar_TypeChecker_Env.step Prims.list) = extraction_norm_steps_core in let uu___ = FStar_Options.use_nbe_for_extraction () in if uu___ then extraction_norm_steps_nbe else extraction_norm_steps_core +let (normalize_for_extraction : + FStar_Extraction_ML_UEnv.uenv -> + FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) + = + fun env -> + fun e -> + let uu___ = FStar_Extraction_ML_UEnv.tcenv_of_uenv env in + FStar_TypeChecker_Normalize.normalize extraction_norm_steps uu___ e let maybe_reify_comp : 'uuuuu . 'uuuuu -> @@ -1059,6 +1121,27 @@ let (maybe_reify_term : | FStar_Syntax_Syntax.Extract_none s -> let uu___1 = FStar_Syntax_Print.term_to_string t in err_cannot_extract_effect l t.FStar_Syntax_Syntax.pos s uu___1 +let (has_extract_as_impure_effect : + FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.fv -> Prims.bool) = + fun g -> + fun fv -> + let uu___ = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + FStar_TypeChecker_Env.fv_has_attr uu___ fv + FStar_Parser_Const.extract_as_impure_effect_lid +let (head_of_type_is_extract_as_impure_effect : + FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> Prims.bool) = + fun g -> + fun t -> + let uu___ = FStar_Syntax_Util.head_and_args t in + match uu___ with + | (hd, uu___1) -> + let uu___2 = + let uu___3 = FStar_Syntax_Util.un_uinst hd in + uu___3.FStar_Syntax_Syntax.n in + (match uu___2 with + | FStar_Syntax_Syntax.Tm_fvar fv -> + has_extract_as_impure_effect g fv + | uu___3 -> false) let rec (translate_term_to_mlty : FStar_Extraction_ML_UEnv.uenv -> FStar_Syntax_Syntax.term -> FStar_Extraction_ML_Syntax.mlty) @@ -1079,40 +1162,47 @@ let rec (translate_term_to_mlty : if uu___ then FStar_Extraction_ML_Syntax.MLTY_Top else - (let uu___2 = - let uu___3 = - let uu___4 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g1 in - FStar_TypeChecker_Env.lookup_lid uu___4 - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + (let uu___2 = has_extract_as_impure_effect g1 fv in + if uu___2 + then + let uu___3 = args in match uu___3 with - | ((uu___4, fvty), uu___5) -> - let fvty1 = - let uu___6 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g1 in - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.ForExtraction] uu___6 fvty in - FStar_Syntax_Util.arrow_formals fvty1 in - match uu___2 with - | (formals, uu___3) -> - let mlargs = FStar_Compiler_List.map (arg_as_mlty g1) args in - let mlargs1 = - let n_args = FStar_Compiler_List.length args in - if (FStar_Compiler_List.length formals) > n_args - then - let uu___4 = FStar_Compiler_Util.first_N n_args formals in - match uu___4 with - | (uu___5, rest) -> - let uu___6 = - FStar_Compiler_List.map - (fun uu___7 -> - FStar_Extraction_ML_Syntax.MLTY_Erased) rest in - FStar_Compiler_List.op_At mlargs uu___6 - else mlargs in - let nm = - FStar_Extraction_ML_UEnv.mlpath_of_lident g1 - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Extraction_ML_Syntax.MLTY_Named (mlargs1, nm)) in + | (a, uu___4)::uu___5 -> translate_term_to_mlty g1 a + else + (let uu___4 = + let uu___5 = + let uu___6 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g1 in + FStar_TypeChecker_Env.lookup_lid uu___6 + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + match uu___5 with + | ((uu___6, fvty), uu___7) -> + let fvty1 = + let uu___8 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g1 in + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.ForExtraction] uu___8 fvty in + FStar_Syntax_Util.arrow_formals fvty1 in + match uu___4 with + | (formals, uu___5) -> + let mlargs = FStar_Compiler_List.map (arg_as_mlty g1) args in + let mlargs1 = + let n_args = FStar_Compiler_List.length args in + if (FStar_Compiler_List.length formals) > n_args + then + let uu___6 = FStar_Compiler_Util.first_N n_args formals in + match uu___6 with + | (uu___7, rest) -> + let uu___8 = + FStar_Compiler_List.map + (fun uu___9 -> + FStar_Extraction_ML_Syntax.MLTY_Erased) rest in + FStar_Compiler_List.op_At mlargs uu___8 + else mlargs in + let nm = + FStar_Extraction_ML_UEnv.mlpath_of_lident g1 + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Extraction_ML_Syntax.MLTY_Named (mlargs1, nm))) in let aux env t = let t1 = FStar_Syntax_Subst.compress t in match t1.FStar_Syntax_Syntax.n with @@ -1174,15 +1264,24 @@ let rec (translate_term_to_mlty : let uu___1 = binders_as_ml_binders env bs1 in (match uu___1 with | (mlbs, env1) -> - let t_ret = + let codom = let uu___2 = - let uu___3 = - FStar_Extraction_ML_UEnv.tcenv_of_uenv env1 in - maybe_reify_comp env1 uu___3 c1 in - translate_term_to_mlty env1 uu___2 in - let erase = + FStar_Extraction_ML_UEnv.tcenv_of_uenv env1 in + maybe_reify_comp env1 uu___2 c1 in + let t_ret = translate_term_to_mlty env1 codom in + let etag = effect_as_etag env1 (FStar_Syntax_Util.comp_effect_name c1) in + let etag1 = + if etag = FStar_Extraction_ML_Syntax.E_IMPURE + then etag + else + (let uu___3 = + head_of_type_is_extract_as_impure_effect env1 + codom in + if uu___3 + then FStar_Extraction_ML_Syntax.E_IMPURE + else etag) in let uu___2 = FStar_Compiler_List.fold_right (fun uu___3 -> @@ -1191,41 +1290,30 @@ let rec (translate_term_to_mlty : | ((uu___5, t2), (tag, t')) -> (FStar_Extraction_ML_Syntax.E_PURE, (FStar_Extraction_ML_Syntax.MLTY_Fun - (t2, tag, t')))) mlbs (erase, t_ret) in + (t2, tag, t')))) mlbs (etag1, t_ret) in (match uu___2 with | (uu___3, t2) -> t2))) - | FStar_Syntax_Syntax.Tm_app - { FStar_Syntax_Syntax.hd = head; - FStar_Syntax_Syntax.args = args;_} - -> - let res = - let uu___ = - let uu___1 = - let uu___2 = FStar_Syntax_Util.un_uinst head in - uu___2.FStar_Syntax_Syntax.n in - (uu___1, args) in - match uu___ with - | (FStar_Syntax_Syntax.Tm_name bv, uu___1) -> bv_as_mlty env bv - | (FStar_Syntax_Syntax.Tm_fvar fv, uu___1::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.steel_memory_inv_lid - -> translate_term_to_mlty env FStar_Syntax_Syntax.t_unit - | (FStar_Syntax_Syntax.Tm_fvar fv, uu___1) -> - fv_app_as_mlty env fv args - | (FStar_Syntax_Syntax.Tm_app - { FStar_Syntax_Syntax.hd = head1; - FStar_Syntax_Syntax.args = args';_}, - uu___1) -> - let uu___2 = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_app - { - FStar_Syntax_Syntax.hd = head1; - FStar_Syntax_Syntax.args = - (FStar_Compiler_List.op_At args' args) - }) t1.FStar_Syntax_Syntax.pos in - translate_term_to_mlty env uu___2 - | uu___1 -> FStar_Extraction_ML_Syntax.MLTY_Top in - res + | FStar_Syntax_Syntax.Tm_app uu___ -> + let uu___1 = FStar_Syntax_Util.head_and_args_full t1 in + (match uu___1 with + | (head, args) -> + let res = + let uu___2 = + let uu___3 = + let uu___4 = FStar_Syntax_Util.un_uinst head in + uu___4.FStar_Syntax_Syntax.n in + (uu___3, args) in + match uu___2 with + | (FStar_Syntax_Syntax.Tm_name bv, uu___3) -> + bv_as_mlty env bv + | (FStar_Syntax_Syntax.Tm_fvar fv, uu___3::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.steel_memory_inv_lid + -> + translate_term_to_mlty env FStar_Syntax_Syntax.t_unit + | (FStar_Syntax_Syntax.Tm_fvar fv, uu___3) -> + fv_app_as_mlty env fv args + | uu___3 -> FStar_Extraction_ML_Syntax.MLTY_Top in + res) | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = bs; FStar_Syntax_Syntax.body = ty; FStar_Syntax_Syntax.rc_opt = uu___;_} diff --git a/ocaml/fstar-lib/generated/FStar_Main.ml b/ocaml/fstar-lib/generated/FStar_Main.ml index 00827179932..f9e8cd54b98 100644 --- a/ocaml/fstar-lib/generated/FStar_Main.ml +++ b/ocaml/fstar-lib/generated/FStar_Main.ml @@ -296,6 +296,9 @@ let (lazy_chooser : | FStar_Syntax_Syntax.Lazy_ident -> FStar_Syntax_Util.exp_string "((ident))" | FStar_Syntax_Syntax.Lazy_embedding (uu___, t) -> FStar_Thunk.force t + | FStar_Syntax_Syntax.Lazy_extension s -> + let uu___ = FStar_Compiler_Util.format1 "((extension %s))" s in + FStar_Syntax_Util.exp_string uu___ let (setup_hooks : unit -> unit) = fun uu___ -> FStar_Errors.set_parse_warn_error FStar_Parser_ParseIt.parse_warn_error; diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 21261f83e99..34606f6d0c7 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -607,4 +607,6 @@ let (unseal_lid : FStar_Ident.lident) = p2l ["FStar"; "Tactics"; "Unseal"; "unseal"] let (document_lid : FStar_Ident.lident) = p2l ["FStar"; "Stubs"; "Pprint"; "document"] -let (issue_lid : FStar_Ident.lident) = p2l ["FStar"; "Issue"; "issue"] \ No newline at end of file +let (issue_lid : FStar_Ident.lident) = p2l ["FStar"; "Issue"; "issue"] +let (extract_as_impure_effect_lid : FStar_Ident.lident) = + p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml b/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml index 996999672ad..97bf128fd3a 100644 --- a/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml +++ b/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml @@ -1562,10 +1562,15 @@ let (equiv_abs_close : type 'g fstar_env_fvs = unit type fstar_env = FStar_Reflection_Types.env type fstar_top_env = fstar_env +type blob = (Prims.string * FStar_Reflection_Types.term) +type dsl_tac_result_base_t = + (FStar_Reflection_Types.term FStar_Pervasives_Native.option * blob + FStar_Pervasives_Native.option * FStar_Reflection_Types.typ) +type ('g, 'e) well_typed = Obj.t +type 'g dsl_tac_result_t = dsl_tac_result_base_t type dsl_tac_t = fstar_top_env -> - ((FStar_Reflection_Types.term * FStar_Reflection_Types.typ), unit) - FStar_Tactics_Effect.tac_repr + (unit dsl_tac_result_t, unit) FStar_Tactics_Effect.tac_repr let (if_complete_match : FStar_Reflection_Types.env -> FStar_Reflection_Types.term -> diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml index fdc914f6581..a5da9e15475 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml @@ -418,6 +418,7 @@ and lazy_kind = | Lazy_issue | Lazy_ident | Lazy_doc + | Lazy_extension of Prims.string and binding = | Binding_var of bv | Binding_lid of (FStar_Ident.lident * (univ_names * term' syntax)) @@ -1076,6 +1077,11 @@ let (uu___is_Lazy_ident : lazy_kind -> Prims.bool) = fun projectee -> match projectee with | Lazy_ident -> true | uu___ -> false let (uu___is_Lazy_doc : lazy_kind -> Prims.bool) = fun projectee -> match projectee with | Lazy_doc -> true | uu___ -> false +let (uu___is_Lazy_extension : lazy_kind -> Prims.bool) = + fun projectee -> + match projectee with | Lazy_extension _0 -> true | uu___ -> false +let (__proj__Lazy_extension__item___0 : lazy_kind -> Prims.string) = + fun projectee -> match projectee with | Lazy_extension _0 -> _0 let (uu___is_Binding_var : binding -> Prims.bool) = fun projectee -> match projectee with | Binding_var _0 -> true | uu___ -> false @@ -1650,25 +1656,32 @@ type sig_metadata = { sigmeta_active: Prims.bool ; sigmeta_fact_db_ids: Prims.string Prims.list ; - sigmeta_admit: Prims.bool } + sigmeta_admit: Prims.bool ; + sigmeta_extension_data: (Prims.string * FStar_Compiler_Dyn.dyn) Prims.list } let (__proj__Mksig_metadata__item__sigmeta_active : sig_metadata -> Prims.bool) = fun projectee -> match projectee with - | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit;_} -> - sigmeta_active + | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit; + sigmeta_extension_data;_} -> sigmeta_active let (__proj__Mksig_metadata__item__sigmeta_fact_db_ids : sig_metadata -> Prims.string Prims.list) = fun projectee -> match projectee with - | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit;_} -> - sigmeta_fact_db_ids + | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit; + sigmeta_extension_data;_} -> sigmeta_fact_db_ids let (__proj__Mksig_metadata__item__sigmeta_admit : sig_metadata -> Prims.bool) = fun projectee -> match projectee with - | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit;_} -> - sigmeta_admit + | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit; + sigmeta_extension_data;_} -> sigmeta_admit +let (__proj__Mksig_metadata__item__sigmeta_extension_data : + sig_metadata -> (Prims.string * FStar_Compiler_Dyn.dyn) Prims.list) = + fun projectee -> + match projectee with + | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit; + sigmeta_extension_data;_} -> sigmeta_extension_data type open_kind = | Open_module | Open_namespace @@ -2309,7 +2322,12 @@ let (mk_Tac : typ -> comp) = flags = [SOMETRIVIAL; TRIVIAL_POSTCONDITION] } let (default_sigmeta : sig_metadata) = - { sigmeta_active = true; sigmeta_fact_db_ids = []; sigmeta_admit = false } + { + sigmeta_active = true; + sigmeta_fact_db_ids = []; + sigmeta_admit = false; + sigmeta_extension_data = [] + } let (mk_sigelt : sigelt' -> sigelt) = fun e -> { diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 7259e4ea727..9020782f577 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -928,6 +928,8 @@ let (eq_lazy_kind : | (FStar_Syntax_Syntax.Lazy_ident, FStar_Syntax_Syntax.Lazy_ident) -> true | (FStar_Syntax_Syntax.Lazy_doc, FStar_Syntax_Syntax.Lazy_doc) -> true + | (FStar_Syntax_Syntax.Lazy_extension s, + FStar_Syntax_Syntax.Lazy_extension t) -> s = t | (FStar_Syntax_Syntax.Lazy_embedding uu___, uu___1) -> false | (uu___, FStar_Syntax_Syntax.Lazy_embedding uu___1) -> false | uu___ -> failwith "FIXME! eq_lazy_kind must be complete" @@ -953,6 +955,8 @@ let (lazy_kind_to_string : FStar_Syntax_Syntax.lazy_kind -> Prims.string) = | FStar_Syntax_Syntax.Lazy_doc -> "Lazy_doc" | FStar_Syntax_Syntax.Lazy_ident -> "Lazy_ident" | FStar_Syntax_Syntax.Lazy_embedding uu___ -> "Lazy_embedding _" + | FStar_Syntax_Syntax.Lazy_extension s -> + Prims.op_Hat "Lazy_extension " s | uu___ -> failwith "FIXME! lazy_kind_to_string must be complete" let unlazy_as_t : 'uuuuu . @@ -3934,18 +3938,19 @@ let eqopt : | uu___ -> false let (debug_term_eq : Prims.bool FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref false -let (check : Prims.string -> Prims.bool -> Prims.bool) = - fun msg -> - fun cond -> - if cond - then true - else - ((let uu___2 = FStar_Compiler_Effect.op_Bang debug_term_eq in - if uu___2 - then FStar_Compiler_Util.print1 ">>> term_eq failing: %s\n" msg - else ()); - false) -let (fail : Prims.string -> Prims.bool) = fun msg -> check msg false +let (check : Prims.bool -> Prims.string -> Prims.bool -> Prims.bool) = + fun dbg -> + fun msg -> + fun cond -> + if cond + then true + else + (if dbg + then FStar_Compiler_Util.print1 ">>> term_eq failing: %s\n" msg + else (); + false) +let (fail : Prims.bool -> Prims.string -> Prims.bool) = + fun dbg -> fun msg -> check dbg msg false let rec (term_eq_dbg : Prims.bool -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term -> Prims.bool) @@ -3955,6 +3960,8 @@ let rec (term_eq_dbg : fun t2 -> let t11 = let uu___ = unmeta_safe t1 in canon_app uu___ in let t21 = let uu___ = unmeta_safe t2 in canon_app uu___ in + let check1 = check dbg in + let fail1 = fail dbg in let uu___ = let uu___1 = let uu___2 = @@ -3979,16 +3986,17 @@ let rec (term_eq_dbg : | (uu___1, FStar_Syntax_Syntax.Tm_ascribed uu___2) -> failwith "term_eq: impossible, should have been removed" | (FStar_Syntax_Syntax.Tm_bvar x, FStar_Syntax_Syntax.Tm_bvar y) -> - check "bvar" + check1 "bvar" (x.FStar_Syntax_Syntax.index = y.FStar_Syntax_Syntax.index) | (FStar_Syntax_Syntax.Tm_name x, FStar_Syntax_Syntax.Tm_name y) -> - check "name" + check1 "name" (x.FStar_Syntax_Syntax.index = y.FStar_Syntax_Syntax.index) | (FStar_Syntax_Syntax.Tm_fvar x, FStar_Syntax_Syntax.Tm_fvar y) -> - let uu___1 = FStar_Syntax_Syntax.fv_eq x y in check "fvar" uu___1 + let uu___1 = FStar_Syntax_Syntax.fv_eq x y in + check1 "fvar" uu___1 | (FStar_Syntax_Syntax.Tm_constant c1, FStar_Syntax_Syntax.Tm_constant c2) -> - let uu___1 = FStar_Const.eq_const c1 c2 in check "const" uu___1 + let uu___1 = FStar_Const.eq_const c1 c2 in check1 "const" uu___1 | (FStar_Syntax_Syntax.Tm_type uu___1, FStar_Syntax_Syntax.Tm_type uu___2) -> true | (FStar_Syntax_Syntax.Tm_abs @@ -3999,18 +4007,18 @@ let rec (term_eq_dbg : FStar_Syntax_Syntax.rc_opt = k2;_}) -> (let uu___1 = eqlist (binder_eq_dbg dbg) b1 b2 in - check "abs binders" uu___1) && + check1 "abs binders" uu___1) && (let uu___1 = term_eq_dbg dbg t12 t22 in - check "abs bodies" uu___1) + check1 "abs bodies" uu___1) | (FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = b1; FStar_Syntax_Syntax.comp = c1;_}, FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = b2; FStar_Syntax_Syntax.comp = c2;_}) -> (let uu___1 = eqlist (binder_eq_dbg dbg) b1 b2 in - check "arrow binders" uu___1) && + check1 "arrow binders" uu___1) && (let uu___1 = comp_eq_dbg dbg c1 c2 in - check "arrow comp" uu___1) + check1 "arrow comp" uu___1) | (FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = b1; FStar_Syntax_Syntax.phi = t12;_}, FStar_Syntax_Syntax.Tm_refine @@ -4018,18 +4026,18 @@ let rec (term_eq_dbg : (let uu___1 = term_eq_dbg dbg b1.FStar_Syntax_Syntax.sort b2.FStar_Syntax_Syntax.sort in - check "refine bv sort" uu___1) && + check1 "refine bv sort" uu___1) && (let uu___1 = term_eq_dbg dbg t12 t22 in - check "refine formula" uu___1) + check1 "refine formula" uu___1) | (FStar_Syntax_Syntax.Tm_app { FStar_Syntax_Syntax.hd = f1; FStar_Syntax_Syntax.args = a1;_}, FStar_Syntax_Syntax.Tm_app { FStar_Syntax_Syntax.hd = f2; FStar_Syntax_Syntax.args = a2;_}) -> - (let uu___1 = term_eq_dbg dbg f1 f2 in check "app head" uu___1) + (let uu___1 = term_eq_dbg dbg f1 f2 in check1 "app head" uu___1) && (let uu___1 = eqlist (arg_eq_dbg dbg) a1 a2 in - check "app args" uu___1) + check1 "app args" uu___1) | (FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = t12; FStar_Syntax_Syntax.ret_opt = FStar_Pervasives_Native.None; @@ -4042,17 +4050,17 @@ let rec (term_eq_dbg : FStar_Syntax_Syntax.rc_opt1 = uu___2;_}) -> (let uu___3 = term_eq_dbg dbg t12 t22 in - check "match head" uu___3) && + check1 "match head" uu___3) && (let uu___3 = eqlist (branch_eq_dbg dbg) bs1 bs2 in - check "match branches" uu___3) + check1 "match branches" uu___3) | (FStar_Syntax_Syntax.Tm_lazy uu___1, uu___2) -> let uu___3 = let uu___4 = unlazy t11 in term_eq_dbg dbg uu___4 t21 in - check "lazy_l" uu___3 + check1 "lazy_l" uu___3 | (uu___1, FStar_Syntax_Syntax.Tm_lazy uu___2) -> let uu___3 = let uu___4 = unlazy t21 in term_eq_dbg dbg t11 uu___4 in - check "lazy_r" uu___3 + check1 "lazy_r" uu___3 | (FStar_Syntax_Syntax.Tm_let { FStar_Syntax_Syntax.lbs = (b1, lbs1); FStar_Syntax_Syntax.body1 = t12;_}, @@ -4060,23 +4068,23 @@ let rec (term_eq_dbg : { FStar_Syntax_Syntax.lbs = (b2, lbs2); FStar_Syntax_Syntax.body1 = t22;_}) -> - ((check "let flag" (b1 = b2)) && + ((check1 "let flag" (b1 = b2)) && (let uu___1 = eqlist (letbinding_eq_dbg dbg) lbs1 lbs2 in - check "let lbs" uu___1)) + check1 "let lbs" uu___1)) && (let uu___1 = term_eq_dbg dbg t12 t22 in - check "let body" uu___1) + check1 "let body" uu___1) | (FStar_Syntax_Syntax.Tm_uvar (u1, uu___1), FStar_Syntax_Syntax.Tm_uvar (u2, uu___2)) -> - check "uvar" + check1 "uvar" (u1.FStar_Syntax_Syntax.ctx_uvar_head = u2.FStar_Syntax_Syntax.ctx_uvar_head) | (FStar_Syntax_Syntax.Tm_quoted (qt1, qi1), FStar_Syntax_Syntax.Tm_quoted (qt2, qi2)) -> (let uu___1 = let uu___2 = eq_quoteinfo qi1 qi2 in uu___2 = Equal in - check "tm_quoted qi" uu___1) && + check1 "tm_quoted qi" uu___1) && (let uu___1 = term_eq_dbg dbg qt1 qt2 in - check "tm_quoted payload" uu___1) + check1 "tm_quoted payload" uu___1) | (FStar_Syntax_Syntax.Tm_meta { FStar_Syntax_Syntax.tm2 = t12; FStar_Syntax_Syntax.meta = m1;_}, FStar_Syntax_Syntax.Tm_meta @@ -4086,47 +4094,47 @@ let rec (term_eq_dbg : | (FStar_Syntax_Syntax.Meta_monadic (n1, ty1), FStar_Syntax_Syntax.Meta_monadic (n2, ty2)) -> (let uu___1 = FStar_Ident.lid_equals n1 n2 in - check "meta_monadic lid" uu___1) && + check1 "meta_monadic lid" uu___1) && (let uu___1 = term_eq_dbg dbg ty1 ty2 in - check "meta_monadic type" uu___1) + check1 "meta_monadic type" uu___1) | (FStar_Syntax_Syntax.Meta_monadic_lift (s1, t13, ty1), FStar_Syntax_Syntax.Meta_monadic_lift (s2, t23, ty2)) -> ((let uu___1 = FStar_Ident.lid_equals s1 s2 in - check "meta_monadic_lift src" uu___1) && + check1 "meta_monadic_lift src" uu___1) && (let uu___1 = FStar_Ident.lid_equals t13 t23 in - check "meta_monadic_lift tgt" uu___1)) + check1 "meta_monadic_lift tgt" uu___1)) && (let uu___1 = term_eq_dbg dbg ty1 ty2 in - check "meta_monadic_lift type" uu___1) - | uu___1 -> fail "metas") - | (FStar_Syntax_Syntax.Tm_unknown, uu___1) -> fail "unk" - | (uu___1, FStar_Syntax_Syntax.Tm_unknown) -> fail "unk" - | (FStar_Syntax_Syntax.Tm_bvar uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_name uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_fvar uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_constant uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_type uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_abs uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_arrow uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_refine uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_app uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_match uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_let uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_uvar uu___1, uu___2) -> fail "bottom" - | (FStar_Syntax_Syntax.Tm_meta uu___1, uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_bvar uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_name uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_fvar uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_constant uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_type uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_abs uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_arrow uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_refine uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_app uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_match uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_let uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_uvar uu___2) -> fail "bottom" - | (uu___1, FStar_Syntax_Syntax.Tm_meta uu___2) -> fail "bottom" + check1 "meta_monadic_lift type" uu___1) + | uu___1 -> fail1 "metas") + | (FStar_Syntax_Syntax.Tm_unknown, uu___1) -> fail1 "unk" + | (uu___1, FStar_Syntax_Syntax.Tm_unknown) -> fail1 "unk" + | (FStar_Syntax_Syntax.Tm_bvar uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_name uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_fvar uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_constant uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_type uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_abs uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_arrow uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_refine uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_app uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_match uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_let uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_uvar uu___1, uu___2) -> fail1 "bottom" + | (FStar_Syntax_Syntax.Tm_meta uu___1, uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_bvar uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_name uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_fvar uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_constant uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_type uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_abs uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_arrow uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_refine uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_app uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_match uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_let uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_uvar uu___2) -> fail1 "bottom" + | (uu___1, FStar_Syntax_Syntax.Tm_meta uu___2) -> fail1 "bottom" and (arg_eq_dbg : Prims.bool -> (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * @@ -4141,11 +4149,11 @@ and (arg_eq_dbg : eqprod (fun t1 -> fun t2 -> - let uu___ = term_eq_dbg dbg t1 t2 in check "arg tm" uu___) + let uu___ = term_eq_dbg dbg t1 t2 in check dbg "arg tm" uu___) (fun q1 -> fun q2 -> let uu___ = let uu___1 = eq_aqual q1 q2 in uu___1 = Equal in - check "arg qual" uu___) a1 a2 + check dbg "arg qual" uu___) a1 a2 and (binder_eq_dbg : Prims.bool -> FStar_Syntax_Syntax.binder -> FStar_Syntax_Syntax.binder -> Prims.bool) @@ -4157,18 +4165,18 @@ and (binder_eq_dbg : term_eq_dbg dbg (b1.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort (b2.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort in - check "binder_sort" uu___) && + check dbg "binder_sort" uu___) && (let uu___ = let uu___1 = eq_bqual b1.FStar_Syntax_Syntax.binder_qual b2.FStar_Syntax_Syntax.binder_qual in uu___1 = Equal in - check "binder qual" uu___)) + check dbg "binder qual" uu___)) && (let uu___ = eqlist (term_eq_dbg dbg) b1.FStar_Syntax_Syntax.binder_attrs b2.FStar_Syntax_Syntax.binder_attrs in - check "binder attrs" uu___) + check dbg "binder attrs" uu___) and (comp_eq_dbg : Prims.bool -> FStar_Syntax_Syntax.comp' FStar_Syntax_Syntax.syntax -> @@ -4184,9 +4192,9 @@ and (comp_eq_dbg : (match uu___1 with | (eff2, res2, args2) -> ((let uu___2 = FStar_Ident.lid_equals eff1 eff2 in - check "comp eff" uu___2) && + check dbg "comp eff" uu___2) && (let uu___2 = term_eq_dbg dbg res1 res2 in - check "comp result typ" uu___2)) + check dbg "comp result typ" uu___2)) && true) and (branch_eq_dbg : Prims.bool -> @@ -4205,9 +4213,9 @@ and (branch_eq_dbg : match (uu___, uu___1) with | ((p1, w1, t1), (p2, w2, t2)) -> ((let uu___2 = FStar_Syntax_Syntax.eq_pat p1 p2 in - check "branch pat" uu___2) && + check dbg "branch pat" uu___2) && (let uu___2 = term_eq_dbg dbg t1 t2 in - check "branch body" uu___2)) + check dbg "branch body" uu___2)) && (let uu___2 = match (w1, w2) with @@ -4216,7 +4224,7 @@ and (branch_eq_dbg : | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None) -> true | uu___3 -> false in - check "branch when" uu___2) + check dbg "branch when" uu___2) and (letbinding_eq_dbg : Prims.bool -> FStar_Syntax_Syntax.letbinding -> @@ -4228,16 +4236,16 @@ and (letbinding_eq_dbg : ((let uu___ = eqsum (fun bv1 -> fun bv2 -> true) FStar_Syntax_Syntax.fv_eq lb1.FStar_Syntax_Syntax.lbname lb2.FStar_Syntax_Syntax.lbname in - check "lb bv" uu___) && + check dbg "lb bv" uu___) && (let uu___ = term_eq_dbg dbg lb1.FStar_Syntax_Syntax.lbtyp lb2.FStar_Syntax_Syntax.lbtyp in - check "lb typ" uu___)) + check dbg "lb typ" uu___)) && (let uu___ = term_eq_dbg dbg lb1.FStar_Syntax_Syntax.lbdef lb2.FStar_Syntax_Syntax.lbdef in - check "lb def" uu___) + check dbg "lb def" uu___) let (term_eq : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term -> Prims.bool) = fun t1 -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml index ebff8a08083..617e04b29d9 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml @@ -1796,8 +1796,17 @@ let (splice : then let uu___7 = let uu___8 = - FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V2_Embeddings.e_term + let uu___9 = + FStar_Syntax_Embeddings.e_option + FStar_Reflection_V2_Embeddings.e_term in + let uu___10 = + let uu___11 = + FStar_Syntax_Embeddings.e_tuple2 + FStar_Syntax_Embeddings.e_string + FStar_Reflection_V2_Embeddings.e_term in + FStar_Syntax_Embeddings.e_option uu___11 in + FStar_Syntax_Embeddings.e_tuple3 uu___9 + uu___10 FStar_Reflection_V2_Embeddings.e_term in FStar_Tactics_V2_Interpreter.run_tactic_on_ps tau1.FStar_Syntax_Syntax.pos @@ -1919,7 +1928,22 @@ let (splice : (env.FStar_TypeChecker_Env.core_check) } uu___8 tau1 tactic_already_typed ps in match uu___7 with - | (gs, (e, t)) -> + | (gs, (tm_opt, blob_opt, typ)) -> + let e = + match tm_opt with + | FStar_Pervasives_Native.None -> + FStar_Syntax_Syntax.tun + | FStar_Pervasives_Native.Some t -> t in + let sig_extension_data = + match blob_opt with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some (s, blob) + -> + let uu___8 = + let uu___9 = + FStar_Compiler_Dyn.mkdyn blob in + (s, uu___9) in + [uu___8] in let lb = let uu___8 = let uu___9 = @@ -1930,8 +1954,9 @@ let (splice : FStar_Pervasives_Native.None in FStar_Pervasives.Inr uu___9 in FStar_Syntax_Util.mk_letbinding uu___8 - [] t FStar_Parser_Const.effect_Tot_lid - e [] rng in + [] typ + FStar_Parser_Const.effect_Tot_lid e [] + rng in (gs, [{ FStar_Syntax_Syntax.sigel = @@ -1946,7 +1971,19 @@ let (splice : FStar_Syntax_Syntax.sigquals = [FStar_Syntax_Syntax.Visible_default]; FStar_Syntax_Syntax.sigmeta = - FStar_Syntax_Syntax.default_sigmeta; + { + FStar_Syntax_Syntax.sigmeta_active + = + (FStar_Syntax_Syntax.default_sigmeta.FStar_Syntax_Syntax.sigmeta_active); + FStar_Syntax_Syntax.sigmeta_fact_db_ids + = + (FStar_Syntax_Syntax.default_sigmeta.FStar_Syntax_Syntax.sigmeta_fact_db_ids); + FStar_Syntax_Syntax.sigmeta_admit + = + (FStar_Syntax_Syntax.default_sigmeta.FStar_Syntax_Syntax.sigmeta_admit); + FStar_Syntax_Syntax.sigmeta_extension_data + = sig_extension_data + }; FStar_Syntax_Syntax.sigattrs = []; FStar_Syntax_Syntax.sigopens_and_abbrevs = []; diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_DMFF.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_DMFF.ml index 5669545116c..8f9b188e7e8 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_DMFF.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_DMFF.ml @@ -183,7 +183,9 @@ let (gen_wps_for_free : (uu___3.FStar_Syntax_Syntax.sigmeta_active); FStar_Syntax_Syntax.sigmeta_fact_db_ids = (uu___3.FStar_Syntax_Syntax.sigmeta_fact_db_ids); - FStar_Syntax_Syntax.sigmeta_admit = true + FStar_Syntax_Syntax.sigmeta_admit = true; + FStar_Syntax_Syntax.sigmeta_extension_data = + (uu___3.FStar_Syntax_Syntax.sigmeta_extension_data) }); FStar_Syntax_Syntax.sigattrs = (sigelt.FStar_Syntax_Syntax.sigattrs); @@ -4492,7 +4494,10 @@ let (cps_and_elaborate : = (uu___16.FStar_Syntax_Syntax.sigmeta_fact_db_ids); FStar_Syntax_Syntax.sigmeta_admit - = true + = true; + FStar_Syntax_Syntax.sigmeta_extension_data + = + (uu___16.FStar_Syntax_Syntax.sigmeta_extension_data) }); FStar_Syntax_Syntax.sigattrs = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index 61d3c9030cd..10650da82d4 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -2629,7 +2629,10 @@ let (tc_decl' : = (uu___3.FStar_Syntax_Syntax.sigmeta_fact_db_ids); FStar_Syntax_Syntax.sigmeta_admit = - true + true; + FStar_Syntax_Syntax.sigmeta_extension_data + = + (uu___3.FStar_Syntax_Syntax.sigmeta_extension_data) }); FStar_Syntax_Syntax.sigattrs = (sigelt.FStar_Syntax_Syntax.sigattrs); diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index 3d8266f8430..5c3c83bb59e 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -49,6 +49,16 @@ module TcUtil = FStar.TypeChecker.Util module EMB = FStar.Syntax.Embeddings module Cfg = FStar.TypeChecker.Cfg +let extension_extractor_table + : BU.smap extension_extractor + = FStar.Compiler.Util.smap_create 20 + +let register_extension_extractor (ext:string) (callback:extension_extractor) = + FStar.Compiler.Util.smap_add extension_extractor_table ext callback + +let lookup_extension_extractor (ext:string) = + FStar.Compiler.Util.smap_try_find extension_extractor_table ext + type env_t = UEnv.uenv (*This approach assumes that failwith already exists in scope. This might be problematic, see below.*) @@ -1009,154 +1019,43 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t * list mlmodule1 = in env, impl - | Sig_let {lbs} -> - let attrs = se.sigattrs in - let quals = se.sigquals in - let maybe_postprocess_lbs lbs = - let post_tau = - match U.extract_attr' PC.postprocess_extr_with attrs with - | None -> None - | Some (_, (tau, None)::_) -> Some tau - | Some _ -> - Errors.log_issue - se.sigrng - (Errors.Warning_UnrecognizedAttribute, - "Ill-formed application of 'postprocess_for_extraction_with'"); - None - in - let postprocess_lb (tau:term) (lb:letbinding) : letbinding = - let env = tcenv_of_uenv g in - let lbdef = - Profiling.profile - (fun () -> Env.postprocess env tau lb.lbtyp lb.lbdef) - (Some (Ident.string_of_lid (Env.current_module env))) - "FStar.Extraction.ML.Module.post_process_for_extraction" - in - { lb with lbdef = lbdef } - in - match post_tau with - | None -> lbs - | Some tau -> fst lbs, List.map (postprocess_lb tau) (snd lbs) - in - let maybe_normalize_for_extraction lbs = - let norm_steps = - match U.extract_attr' PC.normalize_for_extraction_lid attrs with - | None -> None - | Some (_, (steps, None)::_) -> - let steps = - //just normalizing the steps themselves, so that the user - //does not have to write a literal at every use of the attribute - N.normalize - [Env.UnfoldUntil delta_constant; Env.Zeta; Env.Iota; Env.Primops] - (tcenv_of_uenv g) - steps - in - begin - match Cfg.try_unembed_simple (EMB.e_list EMB.e_norm_step) steps with - | Some steps -> - Some (Cfg.translate_norm_steps steps) - | _ -> - Errors.log_issue - se.sigrng - (Errors.Warning_UnrecognizedAttribute, - BU.format1 - "Ill-formed application of 'normalize_for_extraction': normalization steps '%s' could not be interpreted" - (Print.term_to_string steps)); - None - end - | Some _ -> - Errors.log_issue - se.sigrng - (Errors.Warning_UnrecognizedAttribute, - "Ill-formed application of 'normalize_for_extraction'"); - None - in - let norm_one_lb steps lb = - let env = tcenv_of_uenv g in - let env = {env with erase_erasable_args=true} in - let lbd = - Profiling.profile - (fun () -> N.normalize steps env lb.lbdef) - (Some (Ident.string_of_lid (Env.current_module env))) - "FStar.Extraction.ML.Module.normalize_for_extraction" - in - { lb with lbdef = lbd } - in - match norm_steps with - | None -> lbs - | Some steps -> - fst lbs, List.map (norm_one_lb steps) (snd lbs) - in - let ml_let, _, _ = - let lbs = maybe_normalize_for_extraction (maybe_postprocess_lbs lbs) in - Term.term_as_mlexpr - g - (mk (Tm_let {lbs; body=U.exp_false_bool}) se.sigrng) - in - begin - match ml_let.expr with - | MLE_Let((flavor, bindings), _) -> - - (* Treatment of qualifiers: we synthesize the metadata that goes - * onto each let-binding as follows: - * - F* keywords (qualifiers, such as "inline_for_extraction" or - * "private") are in [quals] and are distributed on each - * let-binding in the mutually recursive block of bindings - * - F* attributes (custom arbitrary terms, such as "[@ GcType - * ]"), are attached to the block of mutually recursive - * definitions, we don't have syntax YET for attaching these - * to individual definitions - * - some extra information is looked up here and added as a - * bonus; in particular, the MustDisappear attribute (that - * StackInline bestows upon an individual let-binding) is - * specific to each let-binding! *) - let flags = List.choose flag_of_qual quals in - let flags' = extract_metadata attrs in - - let g, ml_lbs' = - List.fold_left2 - (fun (env, ml_lbs) (ml_lb:mllb) {lbname=lbname; lbtyp=t } -> - if ml_lb.mllb_meta |> List.contains Erased - then env, ml_lbs - else - // debug g (fun () -> printfn "Translating source lb %s at type %s to %A" (Print.lbname_to_string lbname) (Print.typ_to_string t) (must (mllb.mllb_tysc))); - let lb_lid = (right lbname).fv_name.v in - let flags'' = - match (SS.compress t).n with - | Tm_arrow {comp={ n = Comp { effect_name = e }}} - when string_of_lid e = "FStar.HyperStack.ST.StackInline" -> - [ StackInline ] - | _ -> - [] - in - let meta = flags @ flags' @ flags'' in - let ml_lb = { ml_lb with 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, _ = - UEnv.extend_fv - env - (right lbname) - (must ml_lb.mllb_tysc) - ml_lb.mllb_add_unit - in - env, {ml_lb with mllb_name=mls } - else let env, _, _ = UEnv.extend_lb env lbname t (must ml_lb.mllb_tysc) ml_lb.mllb_add_unit in - env, ml_lb in - g, ml_lb::ml_lbs) - (g, []) - bindings - (snd lbs) in - g, - [MLM_Loc (Util.mlloc_of_range se.sigrng); - MLM_Let (flavor, List.rev ml_lbs')] - @ maybe_register_plugin g se - - | _ -> - failwith (BU.format1 "Impossible: Translated a let to a non-let: %s" (Code.string_of_mlexpr (current_module_of_uenv g) ml_let)) - end + (* 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 g blob with + | Inl (term, e_tag, ty) -> + let meta = extract_metadata se.sigattrs in + let ty = Term.term_as_mlty g lb.lbtyp in + let tysc = [], ty in + let g, mlid, _ = UEnv.extend_lb g lb.lbname lb.lbtyp tysc false in + let mllet = MLM_Let (NonRec, [{ mllb_name = mlid; + mllb_tysc= Some tysc; + mllb_add_unit = false; + mllb_def=term; + mllb_meta=meta; + print_typ=false }]) in + g, [mllet] + | 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} -> + | 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) @@ -1188,7 +1087,159 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t * list mlmodule1 = U.process_pragma p se.sigrng; g, [] ) - + +and extract_sig_let (g:uenv) (se:sigelt) : uenv * list mlmodule1 = + if not (Sig_let? se.sigel) + then failwith "Impossible: should only be called with Sig_let" + else begin + let Sig_let { lbs } = se.sigel in + let attrs = se.sigattrs in + let quals = se.sigquals in + let maybe_postprocess_lbs lbs = + let post_tau = + match U.extract_attr' PC.postprocess_extr_with attrs with + | None -> None + | Some (_, (tau, None)::_) -> Some tau + | Some _ -> + Errors.log_issue + se.sigrng + (Errors.Warning_UnrecognizedAttribute, + "Ill-formed application of 'postprocess_for_extraction_with'"); + None + in + let postprocess_lb (tau:term) (lb:letbinding) : letbinding = + let env = tcenv_of_uenv g in + let lbdef = + Profiling.profile + (fun () -> Env.postprocess env tau lb.lbtyp lb.lbdef) + (Some (Ident.string_of_lid (Env.current_module env))) + "FStar.Extraction.ML.Module.post_process_for_extraction" + in + { lb with lbdef = lbdef } + in + match post_tau with + | None -> lbs + | Some tau -> fst lbs, List.map (postprocess_lb tau) (snd lbs) + in + let maybe_normalize_for_extraction lbs = + let norm_steps = + match U.extract_attr' PC.normalize_for_extraction_lid attrs with + | None -> None + | Some (_, (steps, None)::_) -> + let steps = + //just normalizing the steps themselves, so that the user + //does not have to write a literal at every use of the attribute + N.normalize + [Env.UnfoldUntil delta_constant; Env.Zeta; Env.Iota; Env.Primops] + (tcenv_of_uenv g) + steps + in + begin + match Cfg.try_unembed_simple (EMB.e_list EMB.e_norm_step) steps with + | Some steps -> + Some (Cfg.translate_norm_steps steps) + | _ -> + Errors.log_issue + se.sigrng + (Errors.Warning_UnrecognizedAttribute, + BU.format1 + "Ill-formed application of 'normalize_for_extraction': normalization steps '%s' could not be interpreted" + (Print.term_to_string steps)); + None + end + | Some _ -> + Errors.log_issue + se.sigrng + (Errors.Warning_UnrecognizedAttribute, + "Ill-formed application of 'normalize_for_extraction'"); + None + in + let norm_one_lb steps lb = + let env = tcenv_of_uenv g in + let env = {env with erase_erasable_args=true} in + let lbd = + Profiling.profile + (fun () -> N.normalize steps env lb.lbdef) + (Some (Ident.string_of_lid (Env.current_module env))) + "FStar.Extraction.ML.Module.normalize_for_extraction" + in + { lb with lbdef = lbd } + in + match norm_steps with + | None -> lbs + | Some steps -> + fst lbs, List.map (norm_one_lb steps) (snd lbs) + in + let ml_let, _, _ = + let lbs = maybe_normalize_for_extraction (maybe_postprocess_lbs lbs) in + Term.term_as_mlexpr + g + (mk (Tm_let {lbs; body=U.exp_false_bool}) se.sigrng) + in + begin + match ml_let.expr with + | MLE_Let((flavor, bindings), _) -> + + (* Treatment of qualifiers: we synthesize the metadata that goes + * onto each let-binding as follows: + * - F* keywords (qualifiers, such as "inline_for_extraction" or + * "private") are in [quals] and are distributed on each + * let-binding in the mutually recursive block of bindings + * - F* attributes (custom arbitrary terms, such as "[@ GcType + * ]"), are attached to the block of mutually recursive + * definitions, we don't have syntax YET for attaching these + * to individual definitions + * - some extra information is looked up here and added as a + * bonus; in particular, the MustDisappear attribute (that + * StackInline bestows upon an individual let-binding) is + * specific to each let-binding! *) + let flags = List.choose flag_of_qual quals in + let flags' = extract_metadata attrs in + + let g, ml_lbs' = + List.fold_left2 + (fun (env, ml_lbs) (ml_lb:mllb) {lbname=lbname; lbtyp=t } -> + if ml_lb.mllb_meta |> List.contains Erased + then env, ml_lbs + else + // debug g (fun () -> printfn "Translating source lb %s at type %s to %A" (Print.lbname_to_string lbname) (Print.typ_to_string t) (must (mllb.mllb_tysc))); + let lb_lid = (right lbname).fv_name.v in + let flags'' = + match (SS.compress t).n with + | Tm_arrow {comp={ n = Comp { effect_name = e }}} + when string_of_lid e = "FStar.HyperStack.ST.StackInline" -> + [ StackInline ] + | _ -> + [] + in + let meta = flags @ flags' @ flags'' in + let ml_lb = { ml_lb with 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, _ = + UEnv.extend_fv + env + (right lbname) + (must ml_lb.mllb_tysc) + ml_lb.mllb_add_unit + in + env, {ml_lb with mllb_name=mls } + else let env, _, _ = UEnv.extend_lb env lbname t (must ml_lb.mllb_tysc) ml_lb.mllb_add_unit in + env, ml_lb in + g, ml_lb::ml_lbs) + (g, []) + bindings + (snd lbs) in + g, + [MLM_Loc (Util.mlloc_of_range se.sigrng); + MLM_Let (flavor, List.rev ml_lbs')] + @ maybe_register_plugin g se + + | _ -> + failwith (BU.format1 "Impossible: Translated a let to a non-let: %s" (Code.string_of_mlexpr (current_module_of_uenv g) ml_let)) + end + end + let extract' (g:uenv) (m:modul) : uenv * option mllib = let _ = Options.restore_cmd_line_options true in let name, g = UEnv.extend_with_module_name g m.name in diff --git a/src/extraction/FStar.Extraction.ML.Modul.fsti b/src/extraction/FStar.Extraction.ML.Modul.fsti index f4e1919a50f..995fafa2f46 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fsti +++ b/src/extraction/FStar.Extraction.ML.Modul.fsti @@ -20,6 +20,15 @@ open FStar.Compiler.Effect open FStar.Syntax.Syntax open FStar.Extraction.ML.Syntax open FStar.Extraction.ML.UEnv +module S = FStar.Syntax.Syntax + +type extension_extractor = + uenv -> FStar.Compiler.Dyn.dyn -> either (mlexpr * e_tag * mlty) string + +val register_extension_extractor + (extension_name:string) + (extractor:extension_extractor) + : unit val iface : Type0 val extract_iface: uenv -> modul -> uenv * iface diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index fb6696317ec..f9f82598236 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/src/extraction/FStar.Extraction.ML.Syntax.fst @@ -267,3 +267,97 @@ let pop_unit (ts : mltyscheme) : mltyscheme = else failwith "unexpected: pop_unit: domain was not unit" | _ -> failwith "unexpected: pop_unit: not a function type" +module BU = FStar.Compiler.Util + +let mlpath_to_string mlp = String.concat "." (fst mlp) ^ "." ^ snd mlp + +let rec mlty_to_string (t:mlty) = + match t with + | MLTY_Var v -> v + | MLTY_Fun (t1, _, t2) -> + BU.format2 "(%s -> %s)" (mlty_to_string t1) (mlty_to_string t2) + | MLTY_Named (ts, p) -> + BU.format2 "(%s %s)" (String.concat " " (List.map mlty_to_string ts)) (mlpath_to_string p) + | MLTY_Tuple ts -> + BU.format1 "(%s)" (String.concat " * " (List.map mlty_to_string ts)) + | MLTY_Top -> "MLTY_Top" + | MLTY_Erased -> "MLTY_Erased" + +let rec mlexpr_to_string (e:mlexpr) = + match e.expr with + | MLE_Const c -> + BU.format1 "(MLE_Const %s)" (mlconstant_to_string c) + | MLE_Var x -> + BU.format1 "(MLE_Var %s)" x + | MLE_Name (p, x) -> + BU.format2 "(MLE_Name (%s, %s))" (String.concat "." p) x + | MLE_Let (lbs, e) -> + BU.format2 "(MLE_Let (%s, %s))" (mlletbinding_to_string lbs) (mlexpr_to_string e) + | MLE_App (e, es) -> + 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_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) -> + BU.format3 "(MLE_Coerce (%s, %s, %s))" (mlexpr_to_string e) (mlty_to_string t1) (mlty_to_string t2) + | MLE_CTor (p, es) -> + BU.format2 "(MLE_CTor (%s, [%s]))" (mlpath_to_string p) (String.concat "; " (List.map mlexpr_to_string es)) + | MLE_Seq es -> + BU.format1 "(MLE_Seq [%s])" (String.concat "; " (List.map mlexpr_to_string es)) + | MLE_Tuple es -> + BU.format1 "(MLE_Tuple [%s])" (String.concat "; " (List.map mlexpr_to_string es)) + | MLE_Record (p, es) -> + BU.format2 "(MLE_Record (%s, [%s]))" (String.concat "; " p) (String.concat "; " (List.map (fun (x, e) -> BU.format2 "(%s, %s)" x (mlexpr_to_string e)) es)) + | MLE_Proj (e, p) -> + BU.format2 "(MLE_Proj (%s, %s))" (mlexpr_to_string e) (mlpath_to_string p) + | MLE_If (e1, e2, None) -> + BU.format2 "(MLE_If (%s, %s, None))" (mlexpr_to_string e1) (mlexpr_to_string e2) + | MLE_If (e1, e2, Some e3) -> + BU.format3 "(MLE_If (%s, %s, %s))" (mlexpr_to_string e1) (mlexpr_to_string e2) (mlexpr_to_string e3) + | MLE_Raise (p, es) -> + BU.format2 "(MLE_Raise (%s, [%s]))" (mlpath_to_string p) (String.concat "; " (List.map mlexpr_to_string es)) + | MLE_Try (e, bs) -> + BU.format2 "(MLE_Try (%s, [%s]))" (mlexpr_to_string e) (String.concat "; " (List.map mlbranch_to_string bs)) + +and mlbranch_to_string (p, e1, e2) = + match e1 with + | None -> BU.format2 "(%s, None, %s)" (mlpattern_to_string p) (mlexpr_to_string e2) + | Some e1 -> BU.format3 "(%s, Some %s, %s)" (mlpattern_to_string p) (mlexpr_to_string e1) (mlexpr_to_string e2) + +and mlletbinding_to_string (lbs) = + match lbs with + | (Rec, lbs) -> BU.format1 "(Rec, [%s])" (String.concat "; " (List.map mllb_to_string lbs)) + | (NonRec, lbs) -> BU.format1 "(NonRec, [%s])" (String.concat "; " (List.map mllb_to_string lbs)) + +and mllb_to_string (lb) = + BU.format4 "{mllb_name = %s; mllb_tysc = %s; mllb_add_unit = %s; mllb_def = %s}" + lb.mllb_name + (match lb.mllb_tysc with + | None -> "None" + | Some (_, t) -> BU.format1 "Some %s" (mlty_to_string t)) + (string_of_bool lb.mllb_add_unit) + (mlexpr_to_string lb.mllb_def) + +and mlconstant_to_string mlc = + match mlc with + | MLC_Unit -> "MLC_Unit" + | MLC_Bool b -> BU.format1 "(MLC_Bool %s)" (string_of_bool b) + | MLC_Int (s, None) -> BU.format1 "(MLC_Int %s)" s + | MLC_Int (s, Some (s1, s2)) -> BU.format1 "(MLC_Int (%s, _, _))" s + | MLC_Float f -> "(MLC_Float _)" + | MLC_Char c -> "(MLC_Char _)" + | MLC_String s -> BU.format1 "(MLC_String %s)" s + | MLC_Bytes b -> "(MLC_Bytes _)" + +and mlpattern_to_string mlp = + match mlp with + | MLP_Wild -> "MLP_Wild" + | MLP_Const c -> BU.format1 "(MLP_Const %s)" (mlconstant_to_string c) + | MLP_Var x -> BU.format1 "(MLP_Var %s)" x + | MLP_CTor (p, ps) -> BU.format2 "(MLP_CTor (%s, [%s]))" (mlpath_to_string p) (String.concat "; " (List.map mlpattern_to_string ps)) + | MLP_Branch ps -> BU.format1 "(MLP_Branch [%s])" (String.concat "; " (List.map mlpattern_to_string ps)) + | MLP_Record (p, ps) -> BU.format2 "(MLP_Record (%s, [%s]))" (String.concat "; " p) (String.concat "; " (List.map (fun (x, p) -> BU.format2 "(%s, %s)" x (mlpattern_to_string p)) ps)) + | MLP_Tuple ps -> BU.format1 "(MLP_Tuple [%s])" (String.concat "; " (List.map mlpattern_to_string ps)) \ No newline at end of file diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index e65b11b598e..7941861e77a 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/src/extraction/FStar.Extraction.ML.Term.fst @@ -50,6 +50,7 @@ module U = FStar.Syntax.Util exception Un_extractable + (* Below, "the thesis" refers to: Letouzey, Pierre. @@ -153,14 +154,14 @@ let effect_as_etag = where PC.result_type is an arity *) -let rec is_arity env t = +let rec is_arity_aux tcenv t = let t = U.unmeta t in match (SS.compress t).n with | Tm_unknown | Tm_delayed _ | Tm_ascribed _ - | Tm_meta _ -> failwith "Impossible" - | Tm_lazy i -> is_arity env (U.unfold_lazy i) + | Tm_meta _ -> failwith "Impossible: is_arity" + | Tm_lazy i -> is_arity_aux tcenv (U.unfold_lazy i) | Tm_uvar _ | Tm_constant _ | Tm_name _ @@ -168,35 +169,42 @@ let rec is_arity env t = | Tm_bvar _ -> false | Tm_type _ -> true | Tm_arrow {comp=c} -> - is_arity env (FStar.Syntax.Util.comp_result c) + is_arity_aux tcenv (FStar.Syntax.Util.comp_result c) | Tm_fvar fv -> let topt = FStar.TypeChecker.Env.lookup_definition [Env.Unfold delta_constant] - (tcenv_of_uenv env) + tcenv fv.fv_name.v in begin match topt with | None -> false - | Some (_, t) -> is_arity env t + | Some (_, t) -> is_arity_aux tcenv t end | Tm_app _ -> let head, _ = U.head_and_args t in - is_arity env head + is_arity_aux tcenv head | Tm_uinst(head, _) -> - is_arity env head + is_arity_aux tcenv head | Tm_refine {b=x} -> - is_arity env x.sort + is_arity_aux tcenv x.sort | Tm_abs {body} | Tm_let {body} -> - is_arity env body + is_arity_aux tcenv body | Tm_match {brs=branches} -> begin match branches with - | (_, _, e)::_ -> is_arity env e + | (_, _, e)::_ -> is_arity_aux tcenv e | _ -> false end +let is_arity env t = is_arity_aux (tcenv_of_uenv env) t + +let push_tcenv_binders (u:uenv) (bs:binders) = + let tcenv = tcenv_of_uenv u in + let tcenv = TcEnv.push_binders tcenv bs in + set_tcenv u tcenv + //is_type_aux env t: // Determines whether or not t is a type // syntactic structure and type annotations @@ -227,10 +235,19 @@ let rec is_type_aux env t = let t= U.ctx_uvar_typ u in is_arity env (SS.subst' s t) - | Tm_bvar ({sort=t}) - | Tm_name ({sort=t}) -> + | Tm_bvar ({sort=t}) -> is_arity env t + | Tm_name x -> ( + let g = UEnv.tcenv_of_uenv env in + match try_lookup_bv g x with + | Some (t, _) -> + is_arity env t + | _ -> ( + failwith (BU.format1 "Extraction: variable not found: %s" (Print.tag_of_term t)) + ) + ) + | Tm_ascribed {tm=t} -> is_type_aux env t @@ -238,23 +255,32 @@ let rec is_type_aux env t = is_type_aux env t | Tm_abs {bs; body} -> - let _, body = SS.open_term bs body in + let bs, body = SS.open_term bs body in + let env = push_tcenv_binders env bs in is_type_aux env body | Tm_let {lbs=(false, [lb]); body} -> let x = BU.left lb.lbname in - let _, body = SS.open_term [S.mk_binder x] body in + let bs, body = SS.open_term [S.mk_binder x] body in + let env = push_tcenv_binders env bs in is_type_aux env body | Tm_let {lbs=(_, lbs); body} -> - let _, body = SS.open_let_rec lbs body in + let lbs, body = SS.open_let_rec lbs body in + let env = push_tcenv_binders env (List.map (fun lb -> S.mk_binder (BU.left lb.lbname)) lbs) in is_type_aux env body | Tm_match {brs=branches} -> begin match branches with - | b::_ -> - let _, _, e = SS.open_branch b in - is_type_aux env e + | b::_ -> ( + let pat, _, e = SS.open_branch b in + match FStar.TypeChecker.PatternUtils.raw_pat_as_exp (tcenv_of_uenv env) pat with + | None -> false + | Some (_, bvs) -> + let binders = List.map (fun bv -> S.mk_binder bv) bvs in + let env = push_tcenv_binders env binders in + is_type_aux env e + ) | _ -> false end @@ -651,6 +677,9 @@ let extraction_norm_steps = then extraction_norm_steps_nbe else extraction_norm_steps_core +let normalize_for_extraction (env:uenv) (e:S.term) = + N.normalize extraction_norm_steps (tcenv_of_uenv env) e + let maybe_reify_comp g (env:TcEnv.env) (c:S.comp) : S.term = match c |> U.comp_effect_name |> TcUtil.effect_extraction_mode env with @@ -671,33 +700,45 @@ let maybe_reify_term (env:TcEnv.env) (t:S.term) (l:lident) : S.term = | S.Extract_none s -> err_cannot_extract_effect l t.pos s (Print.term_to_string t) +let has_extract_as_impure_effect (g:uenv) (fv:S.fv) = + TcEnv.fv_has_attr (tcenv_of_uenv g) fv FStar.Parser.Const.extract_as_impure_effect_lid + +let head_of_type_is_extract_as_impure_effect g t = + let hd, _ = U.head_and_args t in + match (U.un_uinst hd).n with + | Tm_fvar fv -> has_extract_as_impure_effect g fv + | _ -> false + let rec translate_term_to_mlty (g:uenv) (t0:term) : mlty = let arg_as_mlty (g:uenv) (a, _) : mlty = if is_type g a //This is just an optimization; we could in principle always emit MLTY_Erased, at the expense of more magics then translate_term_to_mlty g a else MLTY_Erased in - let fv_app_as_mlty (g:uenv) (fv:fv) (args : args) : mlty = if not (is_fv_type g fv) then MLTY_Top //it was translated as an expression or erased - else - let formals, _ = + else ( + if has_extract_as_impure_effect g fv + then let (a, _)::_ = args in + translate_term_to_mlty g a + else ( + let formals, _ = let (_, fvty), _ = FStar.TypeChecker.Env.lookup_lid (tcenv_of_uenv g) fv.fv_name.v in let fvty = N.normalize [Env.UnfoldUntil delta_constant; Env.ForExtraction] (tcenv_of_uenv g) fvty in U.arrow_formals fvty in - let mlargs = List.map (arg_as_mlty g) args in - let mlargs = + let mlargs = List.map (arg_as_mlty g) args in + let mlargs = let n_args = List.length args in if List.length formals > n_args //it's not fully applied; so apply the rest to unit then let _, rest = BU.first_N n_args formals in mlargs @ (List.map (fun _ -> MLTY_Erased) rest) else mlargs in - let nm = UEnv.mlpath_of_lident g fv.fv_name.v in - MLTY_Named (mlargs, nm) - + let nm = UEnv.mlpath_of_lident g fv.fv_name.v in + MLTY_Named (mlargs, nm) + ) + ) in - let aux env t = let t = SS.compress t in match t.n with @@ -730,14 +771,22 @@ let rec translate_term_to_mlty (g:uenv) (t0:term) : mlty = | Tm_arrow {bs; comp=c} -> let bs, c = SS.open_comp bs c in let mlbs, env = binders_as_ml_binders env bs in - let t_ret = translate_term_to_mlty env (maybe_reify_comp env (tcenv_of_uenv env) c) in - let erase = effect_as_etag env (U.comp_effect_name c) in - let _, t = List.fold_right (fun (_, t) (tag, t') -> (E_PURE, MLTY_Fun(t, tag, t'))) mlbs (erase, t_ret) in + let codom = maybe_reify_comp env (tcenv_of_uenv env) c in + let t_ret = translate_term_to_mlty env codom in + let etag = effect_as_etag env (U.comp_effect_name c) in + let etag = + if etag = E_IMPURE then etag + else if head_of_type_is_extract_as_impure_effect env codom + then E_IMPURE + else etag + in + let _, t = List.fold_right (fun (_, t) (tag, t') -> (E_PURE, MLTY_Fun(t, tag, t'))) mlbs (etag, t_ret) in t (*can this be a partial type application? , i.e can the result of this application be something like Type -> Type, or nat -> Type? : Yes *) (* should we try to apply additional arguments here? if not, where? FIX!! *) - | Tm_app {hd=head; args} -> + | Tm_app _ -> + let head, args = U.head_and_args_full t in let res = match (U.un_uinst head).n, args with | Tm_name bv, _ -> (*the args are thrown away, because in OCaml, type variables have type Type and not something like -> .. -> .. Type *) @@ -750,11 +799,6 @@ let rec translate_term_to_mlty (g:uenv) (t0:term) : mlty = | Tm_fvar fv, _ -> fv_app_as_mlty env fv args - - - | Tm_app {hd=head; args=args'}, _ -> - translate_term_to_mlty env (S.mk (Tm_app {hd=head; args=args'@args}) t.pos) - | _ -> MLTY_Top in res diff --git a/src/extraction/FStar.Extraction.ML.Term.fsti b/src/extraction/FStar.Extraction.ML.Term.fsti index 96e23b4b730..f6c29e980a3 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fsti +++ b/src/extraction/FStar.Extraction.ML.Term.fsti @@ -21,6 +21,7 @@ open FStar.Syntax.Syntax open FStar.Extraction.ML.Syntax val normalize_abs: term -> term +val normalize_for_extraction (env:uenv) (e:term) : term val is_arity: uenv -> term -> bool val ind_discriminator_body : env:uenv -> discName:lident -> constrName:lident -> mlmodule1 val term_as_mlty: uenv -> term -> mlty diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index b2578a6ecd8..286b4b79465 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -40,7 +40,7 @@ module Dep = FStar.Parser.Dep * detect when loading the cache that the version number is same * It needs to be kept in sync with prims.fst *) -let cache_version_number = 60 +let cache_version_number = 61 (* * Abbreviation for what we store in the checked files (stages as described below) diff --git a/src/fstar/FStar.Main.fst b/src/fstar/FStar.Main.fst index 27754e14481..080c7e98058 100644 --- a/src/fstar/FStar.Main.fst +++ b/src/fstar/FStar.Main.fst @@ -225,7 +225,8 @@ let lazy_chooser k i = match k with | FStar.Syntax.Syntax.Lazy_ident -> FStar.Syntax.Util.exp_string "((ident))" | FStar.Syntax.Syntax.Lazy_embedding (_, t) -> Thunk.force t - + | FStar.Syntax.Syntax.Lazy_extension s -> FStar.Syntax.Util.exp_string (format1 "((extension %s))" s) + // This is called directly by the Javascript port (it doesn't call Main) let setup_hooks () = FStar.Errors.set_parse_warn_error FStar.Parser.ParseIt.parse_warn_error; diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index f8f45e8e1ce..a4ec6ae6890 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -558,3 +558,5 @@ let unseal_lid = p2l ["FStar"; "Tactics"; "Unseal"; "unseal"] let document_lid = p2l ["FStar"; "Stubs"; "Pprint"; "document"] let issue_lid = p2l ["FStar"; "Issue"; "issue"] + +let extract_as_impure_effect_lid = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] \ No newline at end of file diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index e57c663a324..4ebbbb7f93b 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -412,7 +412,7 @@ and bqual_to_string' s = function | None -> s and aqual_to_string' s = function - | Some ({aqual_implicit=true}) -> "#" ^ s + | Some { aqual_implicit=true } -> "#" ^ s | _ -> s and binder_to_string' is_arrow b = diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst index 84f438797ae..034eaf1b795 100644 --- a/src/syntax/FStar.Syntax.Syntax.fst +++ b/src/syntax/FStar.Syntax.Syntax.fst @@ -160,7 +160,12 @@ let mk_Tac t = flags = [SOMETRIVIAL; TRIVIAL_POSTCONDITION]; }) -let default_sigmeta = { sigmeta_active=true; sigmeta_fact_db_ids=[]; sigmeta_admit=false } +let default_sigmeta = { + sigmeta_active=true; + sigmeta_fact_db_ids=[]; + sigmeta_admit=false; + sigmeta_extension_data=[] +} let mk_sigelt (e: sigelt') = { sigel = e; sigrng = Range.dummyRange; diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti index 1b61b9bcec4..0a226ef111b 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsti +++ b/src/syntax/FStar.Syntax.Syntax.fsti @@ -413,6 +413,7 @@ and lazy_kind = | Lazy_issue | Lazy_ident | Lazy_doc + | Lazy_extension of string and binding = | Binding_var of bv | Binding_lid of lident * (univ_names * typ) @@ -620,6 +621,7 @@ type sig_metadata = { sigmeta_fact_db_ids:list string; sigmeta_admit:bool; //An internal flag to record that a sigelt's SMT proof should be admitted //Used in DM4Free + sigmeta_extension_data: list (string & dyn) //each extension can register some data with a sig } diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index 3078b813d73..7f07a41ac01 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -490,6 +490,8 @@ let eq_lazy_kind k k' = | Lazy_ident, Lazy_ident | Lazy_doc, Lazy_doc -> true + | Lazy_extension s, Lazy_extension t -> + s = t | Lazy_embedding _, _ | _, Lazy_embedding _ -> false | _ -> failwith "FIXME! eq_lazy_kind must be complete" @@ -515,7 +517,8 @@ let lazy_kind_to_string k = | Lazy_doc -> "Lazy_doc" | Lazy_ident -> "Lazy_ident" | Lazy_embedding _ -> "Lazy_embedding _" - | _ -> failwith "FIXME! lazy_kind_to_string must be complete" + | Lazy_extension s -> "Lazy_extension " ^ s + | _ -> failwith "FIXME! lazy_kind_to_string must be complete" let unlazy_as_t k t = match (compress t).n with @@ -1850,16 +1853,18 @@ let eqopt (e : 'a -> 'a -> bool) (x : option 'a) (y : option 'a) : bool = // reason against it, so I don't have to go crazy again. let debug_term_eq = U.mk_ref false -let check msg cond = +let check dbg msg cond = if cond then true - else (if !debug_term_eq then U.print1 ">>> term_eq failing: %s\n" msg; false) + else (if dbg then U.print1 ">>> term_eq failing: %s\n" msg; false) -let fail msg = check msg false +let fail dbg msg = check dbg msg false let rec term_eq_dbg (dbg : bool) t1 t2 = let t1 = canon_app (unmeta_safe t1) in let t2 = canon_app (unmeta_safe t2) in + let check = check dbg in + let fail = fail dbg in match (compress (un_uinst t1)).n, (compress (un_uinst t2)).n with | Tm_uinst _, _ | _, Tm_uinst _ @@ -1961,26 +1966,26 @@ let rec term_eq_dbg (dbg : bool) t1 t2 = | _, Tm_meta _ -> fail "bottom" and arg_eq_dbg (dbg : bool) a1 a2 = - eqprod (fun t1 t2 -> check "arg tm" (term_eq_dbg dbg t1 t2)) - (fun q1 q2 -> check "arg qual" (eq_aqual q1 q2 = Equal)) + eqprod (fun t1 t2 -> check dbg "arg tm" (term_eq_dbg dbg t1 t2)) + (fun q1 q2 -> check dbg "arg qual" (eq_aqual q1 q2 = Equal)) a1 a2 and binder_eq_dbg (dbg : bool) b1 b2 = - (check "binder_sort" (term_eq_dbg dbg b1.binder_bv.sort b2.binder_bv.sort)) && - (check "binder qual" (eq_bqual b1.binder_qual b2.binder_qual = Equal)) && //AR: not checking attributes, should we? - (check "binder attrs" (eqlist (term_eq_dbg dbg) b1.binder_attrs b2.binder_attrs)) + (check dbg "binder_sort" (term_eq_dbg dbg b1.binder_bv.sort b2.binder_bv.sort)) && + (check dbg "binder qual" (eq_bqual b1.binder_qual b2.binder_qual = Equal)) && //AR: not checking attributes, should we? + (check dbg "binder attrs" (eqlist (term_eq_dbg dbg) b1.binder_attrs b2.binder_attrs)) and comp_eq_dbg (dbg : bool) c1 c2 = let eff1, res1, args1 = comp_eff_name_res_and_args c1 in let eff2, res2, args2 = comp_eff_name_res_and_args c2 in - (check "comp eff" (lid_equals eff1 eff2)) && + (check dbg "comp eff" (lid_equals eff1 eff2)) && //(check "comp univs" (c1.comp_univs = c2.comp_univs)) && - (check "comp result typ" (term_eq_dbg dbg res1 res2)) && + (check dbg "comp result typ" (term_eq_dbg dbg res1 res2)) && (* (check "comp args" (eqlist arg_eq_dbg dbg c1.effect_args c2.effect_args)) && *) true //eq_flags c1.flags c2.flags and branch_eq_dbg (dbg : bool) (p1,w1,t1) (p2,w2,t2) = - (check "branch pat" (eq_pat p1 p2)) && - (check "branch body" (term_eq_dbg dbg t1 t2)) - && (check "branch when" ( + (check dbg "branch pat" (eq_pat p1 p2)) && + (check dbg "branch body" (term_eq_dbg dbg t1 t2)) + && (check dbg "branch when" ( match w1, w2 with | Some x, Some y -> term_eq_dbg dbg x y | None, None -> true @@ -1988,10 +1993,10 @@ and branch_eq_dbg (dbg : bool) (p1,w1,t1) (p2,w2,t2) = and letbinding_eq_dbg (dbg : bool) (lb1 : letbinding) lb2 = // bvars have no meaning here, so we just check they have the same name - (check "lb bv" (eqsum (fun bv1 bv2 -> true) fv_eq lb1.lbname lb2.lbname)) && + (check dbg "lb bv" (eqsum (fun bv1 bv2 -> true) fv_eq lb1.lbname lb2.lbname)) && (* (check "lb univs" (lb1.lbunivs = lb2.lbunivs)) *) - (check "lb typ" (term_eq_dbg dbg lb1.lbtyp lb2.lbtyp)) && - (check "lb def" (term_eq_dbg dbg lb1.lbdef lb2.lbdef)) + (check dbg "lb typ" (term_eq_dbg dbg lb1.lbtyp lb2.lbtyp)) && + (check dbg "lb def" (term_eq_dbg dbg lb1.lbdef lb2.lbdef)) // Ignoring eff and attrs.. let term_eq t1 t2 = diff --git a/src/tactics/FStar.Tactics.Hooks.fst b/src/tactics/FStar.Tactics.Hooks.fst index 270ea6ff9d2..5ca2a2bd0b7 100644 --- a/src/tactics/FStar.Tactics.Hooks.fst +++ b/src/tactics/FStar.Tactics.Hooks.fst @@ -832,18 +832,30 @@ let splice (env:Env.env) (is_typed:bool) (lids:list Ident.lident) (tau:term) (rn let gs, sigelts = if is_typed then begin - let gs, (e, t) = run_tactic_on_ps tau.pos tau.pos false + let gs, (tm_opt, blob_opt, typ) = run_tactic_on_ps tau.pos tau.pos false RE.e_env {env with gamma=[]} - (e_tuple2 RE.e_term RE.e_term) + (e_tuple3 (e_option RE.e_term) + (e_option (e_tuple2 e_string RE.e_term)) + RE.e_term) tau tactic_already_typed - ps in - + ps + in + let e = + match tm_opt with + | None -> S.tun + | Some t -> t + in + let sig_extension_data = + match blob_opt with + | None -> [] + | Some (s,blob) -> [s, FStar.Compiler.Dyn.mkdyn blob] + in let lb = U.mk_letbinding (Inr (S.lid_as_fv (List.hd lids) None)) [] // no universe polymorphism yet - t + typ PC.effect_Tot_lid // only Tot top-level effect so far e [] @@ -853,7 +865,7 @@ let splice (env:Env.env) (is_typed:bool) (lids:list Ident.lident) (tau:term) (rn [{sigel = S.Sig_let {lbs=(false, [lb]); lids}; // false ==> non-recursive sigrng = rng; sigquals = [S.Visible_default]; // default visibility - sigmeta = S.default_sigmeta; + sigmeta = { S.default_sigmeta with sigmeta_extension_data=sig_extension_data }; sigattrs = []; sigopts = None; sigopens_and_abbrevs=[] diff --git a/ulib/FStar.Ghost.fsti b/ulib/FStar.Ghost.fsti index 8223a543184..243b270b448 100644 --- a/ulib/FStar.Ghost.fsti +++ b/ulib/FStar.Ghost.fsti @@ -45,6 +45,7 @@ module FStar.Ghost (** [erased t] is the computationally irrelevant counterpart of [t] *) [@@ erasable] +new val erased ([@@@strictly_positive] a: Type u#a) : Type u#a (** [erased t] is in a bijection with [t], as witnessed by [reveal] diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index ce0c46da13f..77e48b78b7c 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -174,6 +174,8 @@ let effect_param = () let bind_has_range_args = () let primitive_extraction = () +let extract_as_impure_effect = () + let strictly_positive = () let unused = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index f30fc50cf92..a9cde4283b6 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -1125,6 +1125,20 @@ val bind_has_range_args : unit *) val primitive_extraction : unit +(** A qualifier on a type definition which when used in co-domain position + on an arrow type will be extracted as if it were an impure effect type. + + e.g., if you have + + [@@extract_as_impure_effect] + val stt (a:Type) (pre:_) (post:_) : Type + + then arrows of the form `a -> stt b p q` will be extracted + similarly to `a -> Dv b`. + *) +val extract_as_impure_effect : unit + + (** A binder in a definition/declaration may optionally be annotated as strictly_positive When the let definition is used in a data constructor type in an inductive definition, this annotation is used to check the positivity of the inductive diff --git a/ulib/experimental/FStar.Reflection.Typing.fsti b/ulib/experimental/FStar.Reflection.Typing.fsti index 41fbdcb490e..467ad9981ae 100644 --- a/ulib/experimental/FStar.Reflection.Typing.fsti +++ b/ulib/experimental/FStar.Reflection.Typing.fsti @@ -1756,7 +1756,29 @@ type fstar_top_env = g:fstar_env { // g:fstar_top_env -> T.tac ((us, e, t):(univ_names & term & typ){typing (push g us) e t}) // -type dsl_tac_t = g:fstar_top_env -> T.Tac (r:(R.term & R.typ){typing g (fst r) (T.E_Total, snd r)}) +(** + * The type of the top-level tactic that would splice-in the definitions + * It returns either: + * - Some tm, blob, typ, with a proof that `typing g tm typ` + * - None, blob, typ), with a proof that `exists tm. typing g tm typ` + * The blob itself is optional and can store some additional metadata that + * constructed by the tactic. If present, it will be stored in the + * sigmeta_extension_data field of the enclosing sigelt. + * + * The blob can be used later, e.g., during extraction, and passed back to the + * extension to perform additional processing. + *) +let blob = string & R.term +let dsl_tac_result_base_t = option R.term & option blob & R.typ +let well_typed g (e:dsl_tac_result_base_t) = + let tm_opt, _, typ = e in + match tm_opt with + | None -> exists (tm:R.term). typing g tm (T.E_Total, typ) + | Some tm -> typing g tm (T.E_Total, typ) + +let dsl_tac_result_t g = e:dsl_tac_result_base_t { well_typed g e } + +type dsl_tac_t = g:fstar_top_env -> T.Tac (dsl_tac_result_t g) val if_complete_match (g:env) (t:term) : T.match_complete_token g t bool_ty [ diff --git a/ulib/prims.fst b/ulib/prims.fst index af39252f2f3..90025867937 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -708,4 +708,4 @@ val string_of_int: int -> Tot string (** THIS IS MEANT TO BE KEPT IN SYNC WITH FStar.CheckedFiles.fs Incrementing this forces all .checked files to be invalidated *) irreducible -let __cache_version_number__ = 60 +let __cache_version_number__ = 61