diff options
-rw-r--r-- | interp/constrintern.ml | 92 | ||||
-rw-r--r-- | interp/constrintern.mli | 4 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 | ||||
-rw-r--r-- | plugins/subtac/subtac_command.ml | 18 | ||||
-rw-r--r-- | theories/Vectors/Fin.v | 12 | ||||
-rw-r--r-- | theories/Vectors/VectorDef.v | 4 | ||||
-rw-r--r-- | toplevel/record.ml | 4 |
9 files changed, 74 insertions, 70 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6db69807e..d380e9af6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -44,7 +44,7 @@ type var_internalization_data = scope_name option list type internalization_env = - (identifier * var_internalization_data) list + (var_internalization_data) Idmap.t type glob_binder = (name * binding_kind * glob_constr option * glob_constr) @@ -165,7 +165,7 @@ let error_inductive_parameter_not_implicit loc = (* Pre-computing the implicit arguments and arguments scopes needed *) (* for interpretation *) -let empty_internalization_env = [] +let empty_internalization_env = Idmap.empty let compute_explicitable_implicit imps = function | Inductive params -> @@ -183,8 +183,9 @@ let compute_internalization_data env ty typ impl = (ty, expls_impl, impl, compute_arguments_scope typ) let compute_internalization_env env ty = - list_map3 - (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) + list_fold_left3 + (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map) + empty_internalization_env (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -233,10 +234,11 @@ let contract_pat_notation ntn (l,ll) = !ntn',(l,ll) type intern_env = { - ids : Names.Idset.t ; - unb : bool ; - tmp_scope : Topconstr.tmp_scope_name option ; - scopes : Topconstr.scope_name list } + ids: Names.Idset.t; + unb: bool; + tmp_scope: Topconstr.tmp_scope_name option; + scopes: Topconstr.scope_name list; + impls: internalization_env } (**********************************************************************) (* Remembering the parsing scope of variables in notations *) @@ -324,26 +326,26 @@ let locate_if_isevar loc na = function with Not_found -> GHole (loc, Evd.BinderType na)) | x -> x -let check_hidden_implicit_parameters id (_,_,_,impls) = - if List.exists (function - | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams +let check_hidden_implicit_parameters id impls = + if Idmap.exists (fun _ -> function + | (Inductive indparams,_,_,_) -> List.mem id indparams | _ -> false) impls then errorlabstrm "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") -let push_name_env ?(global_level=false) lvar env = +let push_name_env ?(global_level=false) lvar implargs env = function | loc,Anonymous -> if global_level then user_err_loc (loc,"", str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id lvar; - set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars); + check_hidden_implicit_parameters id env.impls ; + set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars); if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding loc id; - {env with ids = Idset.add id env.ids} + {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls} let intern_generalized_binder ?(global_level=false) intern_type lvar env bl (loc, na) b b' t ty = @@ -554,11 +556,11 @@ let string_of_ty = function | Recursive -> "def" | Method -> "meth" -let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id = +let intern_var genv (ltacvars,ntnvars) namedctx loc id = let (ltacvars,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let ty,expl_impls,impls,argsc = List.assoc id impls in + let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in let expl_impls = List.map (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in @@ -570,6 +572,7 @@ let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id = then GVar (loc,id), [], [], [] (* Is [id] a notation variable *) + else if List.mem_assoc id ntnvars then (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) @@ -586,7 +589,7 @@ let intern_var genv (ltacvars,namedctxvars,ntnvars,impls) loc id = | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id namedctxvars in + let _ = Sign.lookup_named id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -650,12 +653,12 @@ let intern_non_secvar_qualid loc qid intern env lvar args = | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r -let intern_applied_reference intern env lvar args = function +let intern_applied_reference intern env namedctx lvar args = function | Qualid (loc, qid) -> let r,args2 = intern_qualid loc qid intern env lvar args in find_appl_head_data r, args2 | Ident (loc, id) -> - try intern_var env lvar loc id, args + try intern_var env lvar namedctx loc id, args with Not_found -> let qid = qualid_of_ident id in try @@ -671,8 +674,8 @@ let interp_reference vars r = let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) {ids = Idset.empty; unb = false ; - tmp_scope = None; scopes = []} - (vars,[],[],[]) [] r + tmp_scope = None; scopes = []; impls = empty_internalization_env} [] + (vars,[]) [] r in r let apply_scope_env env = function @@ -1116,7 +1119,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let rec intern env = function | CRef ref as x -> let (c,imp,subscopes,l),_ = - intern_applied_reference intern env lvar [] ref in + intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in (match intern_impargs c env imp subscopes l with | [] -> c | l -> GApp (constr_loc x, c, l)) @@ -1207,7 +1210,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes,_),args = let args = List.map (fun a -> (a,None)) args in - intern_applied_reference intern env lvar args ref in + intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in check_projection isproj (List.length args) f; (* Rem: GApp(_,f,[]) stands for @f *) GApp (loc, f, intern_args env args_scopes (List.map fst args)) @@ -1219,7 +1222,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | _ -> isproj,f,args in let (c,impargs,args_scopes,l),args = match f with - | CRef ref -> intern_applied_reference intern env lvar args ref + | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref | CNotation (loc,ntn,([],[],[])) -> let c = intern_notation intern env lvar loc ntn ([],[],[]) in find_appl_head_data c, args @@ -1431,7 +1434,7 @@ let internalize sigma globalenv env allow_patvar lvar c = explain_internalization_error e) (**************************************************************************) -(* Functions to translate constr_expr into glob_constr *) +(* Functions to translate constr_expr into glob_constr *) (**************************************************************************) let extract_ids env = @@ -1440,13 +1443,14 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in internalize sigma env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []} - allow_patvar (ltacvars,Environ.named_context env, [], impls) c + tmp_scope = tmp_scope; scopes = []; + impls = impls} + allow_patvar (ltacvars, []) c let intern_constr sigma env c = intern_gen false sigma env c @@ -1464,7 +1468,7 @@ let intern_pattern env patt = (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in Default.understand_gen kind sigma env c @@ -1472,10 +1476,10 @@ let interp_gen kind sigma env let interp_constr sigma env c = interp_gen (OfType None) sigma env c -let interp_type sigma env ?(impls=[]) c = +let interp_type sigma env ?(impls=empty_internalization_env) c = interp_gen IsType sigma env ~impls c -let interp_casted_constr sigma env ?(impls=[]) c typ = +let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = @@ -1503,7 +1507,7 @@ let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) - env ?(impls=[]) kind c = + env ?(impls=empty_internalization_env) kind c = let evdref = match evdref with | None -> ref Evd.empty @@ -1515,23 +1519,23 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) - env ?(impls=[]) c typ = + env ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c -let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = +let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c -let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = +let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c -let interp_constr_evars_gen evdref env ?(impls=[]) kind c = +let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c = let c = intern_gen (kind=IsType) ~impls !evdref env c in Default.understand_tcc_evars evdref env kind c -let interp_casted_constr_evars evdref env ?(impls=[]) c typ = +let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c -let interp_type_evars evdref env ?(impls=[]) c = +let interp_type_evars evdref env ?(impls=empty_internalization_env) c = interp_constr_evars_gen evdref env IsType ~impls c type ltac_sign = identifier list * unbound_ltac_var_map @@ -1540,13 +1544,13 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in pattern_of_glob_constr c -let interp_aconstr ?(impls=[]) vars recvars a = +let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []} - false (([],[]),Environ.named_context env,vl,impls) a in + tmp_scope = None; scopes = []; impls = impls} + false (([],[]),vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) let a = aconstr_of_glob_constr vars recvars c in (* Splits variables into those that are binding, bound, or both *) @@ -1577,11 +1581,11 @@ let my_intern_constr sigma env lvar acc c = let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c let intern_context global_level sigma env params = - let lvar = (([],[]),Environ.named_context env, [], []) in + let lvar = (([],[]), []) in snd (List.fold_left (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) ({ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []}, []) params) + tmp_scope = None; scopes = []; impls = empty_internalization_env}, []) params) let interp_rawcontext_gen understand_type understand_judgment env bl = let (env, par, _, impls) = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12dc6be16..2cb706589 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -40,6 +40,7 @@ type var_internalization_type = | Inductive of identifier list (* list of params *) | Recursive | Method + | Definition type var_internalization_data = var_internalization_type * @@ -52,8 +53,7 @@ type var_internalization_data = scope_name option list (** subscopes of the args of the variable *) (** A map of free variables to their implicit arguments and scopes *) -type internalization_env = - (identifier * var_internalization_data) list +type internalization_env = var_internalization_data Idmap.t val empty_internalization_env : internalization_env diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e57180327..38492f88b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -152,8 +152,8 @@ let build_newrecursive let arityc = Topconstr.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls)) - (env0,[]) lnameargsardef in + (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls)) + (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) let fs = States.freeze() in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index feff5d67c..4217b83fa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1410,7 +1410,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Definition) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = interp_constr diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index aae538389..640d3e60d 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -26,11 +26,11 @@ open Util module SPretyping = Subtac_pretyping.Pretyping -let interp_constr_evars_gen evdref env ?(impls=[]) kind c = +let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = SPretyping.understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls !evdref env c) -let interp_casted_constr_evars evdref env ?(impls=[]) c typ = +let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c let interp_context_evars evdref env params = diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 9098922e3..6fe31646b 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -52,7 +52,7 @@ let evar_nf isevars c = Evarutil.nf_evar !isevars c let interp_gen kind isevars env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in let c' = SPretyping.understand_tcc_evars isevars env kind c' in @@ -61,13 +61,13 @@ let interp_gen kind isevars env let interp_constr isevars env c = interp_gen (OfType None) isevars env c -let interp_type_evars isevars env ?(impls=[]) c = +let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c = interp_gen IsType isevars env ~impls c -let interp_casted_constr isevars env ?(impls=[]) c typ = +let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c -let interp_casted_constr_evars isevars env ?(impls=[]) c typ = +let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = @@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in - let newimpls = [(recname, (r, l, impls @ - [Some (id_of_string "recproof", Impargs.Manual, (true, false))], - scopes @ [None]))] in - interp_casted_constr isevars ~impls:newimpls - (push_rel_context ctx env) body (lift 1 top_arity) + let newimpls = Idmap.singleton recname + (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))], + scopes @ [None]) in + interp_casted_constr isevars ~impls:newimpls + (push_rel_context ctx env) body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index b90937a40..97ae56e16 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -53,10 +53,10 @@ fix rectS_fix n (p: t (S n)): P n p:= end. Definition rect2 (P: forall {n} (a b: t n), Type) - (H0: forall n, P (S n) F1 F1) - (H1: forall n (f: t n), P (S n) F1 (FS f)) - (H2: forall n (f: t n), P (S n) (FS f) F1) - (HS: forall n (f g : t n), P n f g -> P (S n) (FS f) (FS g)): + (H0: forall n, P F1 F1) + (H1: forall n (f: t n), P F1 (FS f)) + (H2: forall n (f: t n), P (FS f) F1) + (HS: forall n (f g : t n), P f g -> P (FS f) (FS g)): forall n (a b: t n), P n a b := fix rect2_fix n (a: t n): forall (b: t n), P n a b := match a with @@ -64,7 +64,7 @@ match a with return match n' as n0 return t n0 -> Type with |0 => fun _ => @ID - |S n0 => fun b0 => P (S n0) F1 b0 + |S n0 => fun b0 => P _ F1 b0 end b' with |F1 m' => H0 m' |FS m' b' => H1 m' b' @@ -74,7 +74,7 @@ match a with return t n0 -> Type with |0 => fun _ => @ID |S n0 => fun b0 => - forall (a0: t n0), P (S n0) (FS a0) b0 + forall (a0: t n0), P _ (FS a0) b0 end b' with |F1 m' => fun aa => H2 m' aa |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b') diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index e5bb66a20..150342ee8 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -34,8 +34,8 @@ Section SCHEMES. (** An induction scheme for non-empty vectors *) Definition rectS {A} (P:forall {n}, t A (S n) -> Type) - (bas: forall a: A, P 0 (a :: [])) - (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) := + (bas: forall a: A, P (a :: [])) + (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) := fix rectS_fix {n} (v: t A (S n)) : P n v := match v with |nil => @id diff --git a/toplevel/record.ml b/toplevel/record.ml index 27b6ffabe..74a33f6f9 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -41,12 +41,12 @@ let interp_fields_evars evars env nots l = let impls = match i with | Anonymous -> impls - | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls + | Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls in let d = (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], []) nots l + (env, [], [], empty_internalization_env) nots l let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) |