diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 55 | ||||
| -rw-r--r-- | interp/constrintern.mli | 29 | ||||
| -rw-r--r-- | interp/declare.ml | 151 |
3 files changed, 115 insertions, 120 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 14234b3118..61b33aa415 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2098,39 +2098,36 @@ let interp_open_constr env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls env evdref +let interp_constr_evars_gen_impls env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c, imps + let sigma, c = understand_tcc env sigma ~expected_type c in + sigma, (c, imps) -let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c +let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c -let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls IsType c +let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) -let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c = +let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c + understand_tcc env sigma ~expected_type c let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c -let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c +let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen env sigma ~impls (OfType typ) c -let interp_type_evars env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen env evdref IsType ~impls c +let interp_type_evars env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen env sigma IsType ~impls c (* Miscellaneous *) @@ -2185,17 +2182,16 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_glob_context_evars env evdref k bl = +let interp_glob_context_evars env sigma k bl = let open EConstr in - let (env, par, _, impls) = + let env, sigma, par, _, impls = List.fold_left - (fun (env,params,n,impls) (na, k, b, t) -> + (fun (env,sigma,params,n,impls) (na, k, b, t) -> let t' = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t in - let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in - evdref := evd; + let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in match b with None -> let d = LocalAssum (na,t) in @@ -2205,16 +2201,15 @@ let interp_glob_context_evars env evdref k bl = (ExplByPos (n, na), (true, true, true)) :: impls else impls in - (push_rel d env, d::params, succ n, impls) + (push_rel d env, sigma, d::params, succ n, impls) | Some b -> - let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in - evdref := evd; + let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in let d = LocalDef (na, c, t) in - (push_rel d env, d::params, n, impls)) - (env,[],k+1,[]) (List.rev bl) - in (env, par), impls + (push_rel d env, sigma, d::params, n, impls)) + (env,sigma,[],k+1,[]) (List.rev bl) + in sigma, ((env, par), impls) -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_glob_context_evars env evdref shift bl in - int_env, x + let sigma, x = interp_glob_context_evars env sigma shift bl in + sigma, (int_env, x) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index af4e4a9c55..632b423b05 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -112,29 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co (** Accepting unresolved evars *) -val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.constr +val interp_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr +val interp_casted_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr -val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.types -> EConstr.constr - -val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.types +val interp_type_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : env -> evar_map ref -> +val interp_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_casted_constr_evars_impls : env -> evar_map ref -> +val interp_casted_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> EConstr.types -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_type_evars_impls : env -> evar_map ref -> +val interp_type_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.types * Impargs.manual_implicits + evar_map * (EConstr.types * Impargs.manual_implicits) (** Interprets constr patterns *) @@ -159,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder_expr list -> - internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) + env -> evar_map -> local_binder_expr list -> + evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) diff --git a/interp/declare.ml b/interp/declare.ml index 0adad14198..8781c87192 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -31,64 +31,6 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) -(** Declaration of section variables and local definitions *) - -type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -let cache_variable ((sp,_),o) = - match o with - | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); - - let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - let univs = Global.push_named_def (id,de) in - let poly = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in - Explicit, de.const_entry_opaque, - poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; - Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id (p,opaq,ctx,poly,mk) - -let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope (VarRef id); - Heads.declare_head (EvalVarRef id); - oname - - (** Declaration of constants and parameters *) type constant_obj = { @@ -195,6 +137,20 @@ let update_tables c = Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c) +let register_side_effect (c, role) = + let o = inConstant { + cst_decl = None; + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + let declare_constant_common id cst = let o = inConstant cst in let _, kn as oname = add_leaf id o in @@ -229,25 +185,11 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e (** This globally defines the side-effects in the environment. We mark exported constants as being side-effect not to redeclare them at caching time. *) - let cd, export = Global.export_private_constants ~in_section cd in - export, ConstantEntry (PureEntry, cd) + let de, export = Global.export_private_constants ~in_section de in + export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) in - let iter_eff (c, role) = - let o = inConstant { - cst_decl = None; - cst_hyps = [] ; - cst_kind = IsProof Theorem; - cst_locl = false; - } in - let id = Label.to_id (pi3 (Constant.repr3 c)) in - ignore(add_leaf id o); - update_tables c; - match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] - in - let () = List.iter iter_eff export in + let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; cst_hyps = [] ; @@ -265,6 +207,65 @@ let declare_definition ?(internal=UserIndividualRequest) declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) +(** Declaration of section variables and local definitions *) + +type section_variable_entry = + | SectionLocalDef of Safe_typing.private_constants definition_entry + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + +type variable_declaration = DirPath.t * section_variable_entry * logical_kind + +let cache_variable ((sp,_),o) = + match o with + | Inl ctx -> Global.push_context_set false ctx + | Inr (id,(p,d,mk)) -> + (* Constr raisonne sur les noms courts *) + if variable_exists id then + alreadydeclared (Id.print id ++ str " already exists"); + + let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum ((ty,ctx),poly,impl) -> + let () = Global.push_named_assum ((id,ty,poly),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx + | SectionLocalDef (de) -> + let (de, eff) = Global.export_private_constants ~in_section:true de in + let () = List.iter register_side_effect eff in + let univs = Global.push_named_def (id,de) in + let poly = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in + Explicit, de.const_entry_opaque, + poly, univs in + Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + add_section_variable id impl poly ctx; + Dischargedhypsmap.set_discharged_hyps sp []; + add_variable_data id (p,opaq,ctx,poly,mk) + +let discharge_variable (_,o) = match o with + | Inr (id,_) -> + if variable_polymorphic id then None + else Some (Inl (variable_context id)) + | Inl _ -> Some o + +type variable_obj = + (Univ.ContextSet.t, Id.t * variable_declaration) union + +let inVariable : variable_obj -> obj = + declare_object { (default_object "VARIABLE") with + cache_function = cache_variable; + discharge_function = discharge_variable; + classify_function = (fun _ -> Dispose) } + +(* for initial declaration *) +let declare_variable id obj = + let oname = add_leaf id (inVariable (Inr (id,obj))) in + declare_var_implicits id; + Notation.declare_ref_arguments_scope (VarRef id); + Heads.declare_head (EvalVarRef id); + oname + (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = |