diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 9 | ||||
| -rw-r--r-- | interp/constrintern.ml | 52 | ||||
| -rw-r--r-- | interp/declare.ml | 9 | ||||
| -rw-r--r-- | interp/discharge.ml | 11 | ||||
| -rw-r--r-- | interp/impargs.ml | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 7 |
8 files changed, 57 insertions, 47 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7497d4e8e..c03a5fee90 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -121,6 +120,9 @@ type internalization_error = | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int + | NotAProjection of qualid + | NotAProjectionOf of qualid * qualid + | ProjectionsOfDifferentRecords of qualid * qualid exception InternalizationError of internalization_error Loc.located @@ -146,6 +148,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let explain_field_not_a_projection field_id = + pr_qualid field_id ++ str ": Not a projection" + +let explain_field_not_a_projection_of field_id inductive_id = + pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id + +let explain_projections_of_diff_records inductive1_id inductive2_id = + str "This record contains fields of both " ++ pr_qualid inductive1_id ++ + str " and " ++ pr_qualid inductive2_id + let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' @@ -154,6 +166,11 @@ let explain_internalization_error e = | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | NotAProjection field_id -> explain_field_not_a_projection field_id + | NotAProjectionOf (field_id, inductive_id) -> + explain_field_not_a_projection_of field_id inductive_id + | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> + explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." let error_bad_inductive_type ?loc = @@ -633,7 +650,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -721,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let gc = intern nenv c in Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +1003,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1075,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1282,6 +1299,10 @@ let check_duplicate loc fields = user_err ?loc (str "This record defines several times the field " ++ pr_qualid r ++ str ".") +let inductive_of_record loc record = + let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1304,15 +1325,14 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc ~hdr:"intern" - (pr_qualid first_field_ref ++ str": Not a projection") + raise (InternalizationError(loc, NotAProjection first_field_ref)) in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1364,12 +1384,18 @@ let sort_fields ~complete loc fields completer = with Not_found -> user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in + let this_field_record = try Recordops.find_projection field_glob_ref + with Not_found -> + let inductive_ref = inductive_of_record loc record in + raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) + in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> - user_err ?loc - (str "This record contains fields of different records.") + let ind1 = inductive_of_record loc record in + let ind2 = inductive_of_record loc this_field_record in + raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> @@ -1493,7 +1519,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1576,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then diff --git a/interp/declare.ml b/interp/declare.ml index 07a0066ea8..7a32018c0e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - match (Global.lookup_constant con).const_body with - | (Def _ | Undef _) -> () - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with - | Some f when Future.is_val f -> - Global.push_context_set false (Future.force f) - | _ -> () + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) diff --git a/interp/discharge.ml b/interp/discharge.ml index 0e44a8b467..21b2e85e8f 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open CErrors open Util open Term open Constr @@ -17,17 +15,10 @@ open Vars open Declarations open Cooking open Entries -open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = - function - | LocalAssum (Name id, p) -> id, LocalAssumEntry p - | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable.") - (* Replace Var(y1)..Var(yq):C1..Cq |- Ij:Bj @@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds = (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparamdecls' arity in - List.map detype_param params + params in let ind'' = List.map diff --git a/interp/impargs.ml b/interp/impargs.ml index ce33cb8731..d8582d856e 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -450,13 +450,13 @@ let compute_mib_implicits flags kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar, _ = Global.type_of_global_in_context env (IndRef ind) in + let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) @@ -694,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in let sigma = Evd.from_env env in - let t, _ = Global.type_of_global_in_context env ref in + let t, _ = Typeops.type_of_global_in_context env ref in let t = of_constr t in let enriching = Option.default flags.auto enriching in let autoimpls = compute_auto_implicits env sigma flags enriching t in diff --git a/interp/notation.ml b/interp/notation.ml index 6104ab16c7..db8ee5bc18 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let scs,cls = compute_arguments_scope_full sigma typ in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> @@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let l',cls = compute_arguments_scope_full sigma typ in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in @@ -1369,7 +1369,7 @@ let find_arguments_scope r = let declare_ref_arguments_scope sigma ref = let env = Global.env () in (* FIXME? *) - let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in + let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in let (scs,cls as o) = compute_arguments_scope_full sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ab57176643..7a525f84a5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -892,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable.") + | t -> + (* The term is a non-variable pattern *) + raise No_match with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def |