diff options
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrexpr.ml | 16 | ||||
-rw-r--r-- | interp/constrexpr_ops.ml | 11 | ||||
-rw-r--r-- | interp/constrexpr_ops.mli | 3 | ||||
-rw-r--r-- | interp/constrextern.ml | 13 | ||||
-rw-r--r-- | interp/constrintern.ml | 42 | ||||
-rw-r--r-- | interp/constrintern.mli | 1 | ||||
-rw-r--r-- | interp/declare.mli | 2 | ||||
-rw-r--r-- | interp/dumpglob.mli | 4 | ||||
-rw-r--r-- | interp/genintern.ml | 8 | ||||
-rw-r--r-- | interp/genintern.mli | 8 | ||||
-rw-r--r-- | interp/genredexpr.ml | 3 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 4 | ||||
-rw-r--r-- | interp/modintern.ml | 5 | ||||
-rw-r--r-- | interp/modintern.mli | 3 | ||||
-rw-r--r-- | interp/notation_ops.ml | 22 | ||||
-rw-r--r-- | interp/notation_term.ml | 3 | ||||
-rw-r--r-- | interp/reserve.mli | 2 | ||||
-rw-r--r-- | interp/smartlocate.ml | 5 | ||||
-rw-r--r-- | interp/smartlocate.mli | 5 | ||||
-rw-r--r-- | interp/stdarg.ml | 15 | ||||
-rw-r--r-- | interp/stdarg.mli | 27 | ||||
-rw-r--r-- | interp/tactypes.ml | 34 |
23 files changed, 95 insertions, 143 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index ca6ea94f0..d725f5afa 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Decl_kinds (** {6 Concrete syntax for terms } *) @@ -23,6 +22,15 @@ type name_decl = lname * universe_decl_expr option type notation = string +type 'a or_by_notation_r = + | AN of 'a + | ByNotation of (string * string option) + +type 'a or_by_notation = 'a or_by_notation_r CAst.t + +(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], + but this formulation avoids a useless dependency. *) + type explicitation = | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) | ExplByName of Id.t @@ -94,11 +102,11 @@ and constr_expr_r = constr_expr * constr_expr | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr - | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option - | CPatVar of patvar + | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort - | CCast of constr_expr * constr_expr cast_type + | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation * constr_notation_substitution | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 1be1dd96c..d626630ef 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -14,8 +14,9 @@ open CAst open Names open Nameops open Libnames +open Namegen +open Glob_term open Constrexpr -open Misctypes open Decl_kinds (***********************) @@ -161,7 +162,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 + Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(n1, s1), CNotation(n2, s2) -> @@ -395,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, @@ -545,7 +546,7 @@ let coerce_to_id = function let coerce_to_name = function | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id - | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous + | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -569,7 +570,7 @@ let mkAppPattern ?loc p lp = let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CRef (r,None) -> CPatAtom (Some r) - | CHole (None,Misctypes.IntroAnonymous,None) -> + | CHole (None,IntroAnonymous,None) -> CPatAtom None | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index b4f0886ac..1c2348457 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) @@ -44,7 +43,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 86f6ce9ae..c613effcd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -17,6 +17,7 @@ open Nameops open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr @@ -719,7 +720,7 @@ let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> match DAst.get t with - | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) | _ -> GLocalDef (p,bk,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -754,13 +755,13 @@ let rec extern inctx scopes vars r = | GVar id -> CRef (make ?loc @@ Ident id,None) - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> - if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else + if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) @@ -916,7 +917,7 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, - Miscops.map_cast_type (extern_typ scopes vars) c') + map_cast_type (extern_typ scopes vars) c') | GProj (p, c) -> let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in CProj (pr, sub_extern inctx scopes vars c) @@ -1159,7 +1160,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in @@ -1183,7 +1184,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id - | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) + | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e09b7a793..d7345b701 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,8 +14,8 @@ open Util open CAst open Names open Nameops -open Constr open Namegen +open Constr open Libnames open Globnames open Impargs @@ -394,7 +394,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -431,7 +431,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") @@ -472,7 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let tyc = match ty with | Some ty -> ty - | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) + | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) in let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in @@ -502,11 +502,11 @@ let intern_generalization intern env ntnvars loc bk ak c = if pi then (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) else (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in @@ -564,7 +564,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -606,7 +606,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam (renaming',env), None, Name id' type binder_action = -| AddLetIn of Misctypes.lname * constr_expr * constr_expr option +| AddLetIn of lname * constr_expr * constr_expr option | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) @@ -626,7 +626,7 @@ let terms_of_binders bl = | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in - let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in + let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with @@ -1073,11 +1073,11 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = - | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname + | RCPatAlias of 'a raw_cases_pattern_expr * lname | RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) - | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option + | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1385,7 +1385,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Misctypes.lident list; + alias_ids : lident list; alias_map : Id.t Id.Map.t; } @@ -1725,15 +1725,15 @@ let get_implicit_name n imps = let set_hole_implicit i b c = let loc = c.CAst.loc in match DAst.get c with - | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | GApp (r, _) -> let loc = r.CAst.loc in begin match DAst.get r with | GRef (r, _) -> - Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1919,13 +1919,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let fields = sort_fields ~complete:true loc fs (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - Misctypes.IntroAnonymous, None)) + IntroAnonymous, None)) in begin match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in + let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in intern env app end @@ -1965,12 +1965,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) - DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in + DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in @@ -2001,7 +2001,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with - | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | IntroIdentifier id -> Evar_kinds.NamedHole id | _ -> Evar_kinds.QuestionMark (st,Anonymous)) | Some k -> k in @@ -2046,7 +2046,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type env) c2) | CProj (pr, c) -> match intern_reference pr with | ConstRef p -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4dd719e1f..12f77af30 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -11,7 +11,6 @@ open Names open Evd open Environ -open Misctypes open Libnames open Glob_term open Pattern diff --git a/interp/declare.mli b/interp/declare.mli index 4a9f54278..02e73cd66 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -87,6 +87,6 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit -val do_universe : polymorphic -> Misctypes.lident list -> unit +val do_universe : polymorphic -> lident list -> unit val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index bf83d2df4..931d05a97 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -27,7 +27,7 @@ val continue : unit -> unit val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit -val dump_definition : Misctypes.lident -> bool -> string -> unit +val dump_definition : Names.lident -> bool -> string -> unit val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit @@ -39,7 +39,7 @@ val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : Misctypes.lname -> bool -> string -> unit +val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genintern.ml b/interp/genintern.ml index 161201c44..d9a0db040 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -26,9 +26,15 @@ let empty_glob_sign env = { extra = Store.empty; } +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct diff --git a/interp/genintern.mli b/interp/genintern.mli index d818713fc..f4f064bca 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -22,6 +22,12 @@ type glob_sign = { val empty_glob_sign : Environ.env -> glob_sign +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + (** {5 Internalization functions} *) type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb @@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun (** {5 Notation functions} *) -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 80697461a..42c1fe429 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -52,12 +52,11 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Misctypes.lident * 'a + | ConstrContext of Names.lident * 'a | ConstrTypeOf of 'a open Libnames open Constrexpr -open Misctypes type r_trm = constr_expr type r_pat = constr_pattern_expr diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b48db9ac5..b54e2badd 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -53,7 +53,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * Misctypes.lident list option -> obj = +let in_generalizable : bool * lident list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index e64c5c542..25394fc0d 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : local:bool -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t @@ -31,7 +31,7 @@ val free_vars_of_binders : order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> - glob_constr -> Misctypes.lident list + glob_constr -> lident list val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t diff --git a/interp/modintern.ml b/interp/modintern.ml index fefd2ab6f..33c07d551 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,7 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Misctypes +open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = match kind with + let e = let open Declaremods in match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,6 +46,7 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind {CAst.loc;v=qid} = + let open Declaremods in try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in diff --git a/interp/modintern.mli b/interp/modintern.mli index ef37aead8..529c438c1 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -11,7 +11,6 @@ open Environ open Entries open Constrexpr -open Misctypes (** Module internalization errors *) @@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error isn't ModAny. *) val interp_module_ast : - env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t + env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f208b23fb..ab0bf9c6f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -16,7 +16,7 @@ open Nameops open Constr open Globnames open Decl_kinds -open Misctypes +open Namegen open Glob_term open Glob_ops open Mod_subst @@ -86,7 +86,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Array.equal (eq_notation_constr vars) us1 us2 && Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 + glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | NProj (p1, c1), NProj (p2, c2) -> @@ -158,7 +158,7 @@ let protect g e na = let apply_cases_pattern ?loc ((ids,disjpat),id) c = let tm = DAst.make ?loc (GVar id) in let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in - DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) + DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with @@ -216,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) @@ -434,7 +434,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GCast (c,k) -> NCast (aux c,map_cast_type aux k) | GSort s -> NSort s | GHole (w,naming,arg) -> if arg != None then has_ltac := true; @@ -637,7 +637,7 @@ let rec subst_notation_constr subst bound raw = | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') | NProj (p, c) -> @@ -666,11 +666,11 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr tml rtn = abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal) (fun na c -> DAst.make @@ - GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn + GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false @@ -1194,7 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma - | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma @@ -1208,7 +1208,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in - let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 @@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let store, get = set_temporary_memory () in match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b1)}] -> diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 52a6354a0..6d9effcef 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes open Glob_term (** [notation_constr] *) @@ -25,7 +24,7 @@ type notation_constr = | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr diff --git a/interp/reserve.mli b/interp/reserve.mli index daee58639..a10858e71 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -11,5 +11,5 @@ open Names open Notation_term -val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit +val declare_reserved_type : lident list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 1f4a93a6f..e1fbdba87 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -18,7 +18,6 @@ open Pp open CErrors open Libnames open Globnames -open Misctypes open Syntax_def open Notation_term @@ -65,13 +64,13 @@ let global_with_alias ?head r = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = CAst.with_loc_val (fun ?loc -> function +let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_with_alias ?head r | ByNotation (ntn,sc) -> Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) -let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function +let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_inductive_with_alias r | ByNotation (ntn,sc) -> diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 45037b8b3..6b574d7b5 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -11,7 +11,6 @@ open Names open Libnames open Globnames -open Misctypes (** [locate_global_with_alias] locates global reference possibly following a notation if this notation has a role of aliasing; raise [Not_found] @@ -33,7 +32,7 @@ val global_with_alias : ?head:bool -> reference -> GlobRef.t val global_inductive_with_alias : reference -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t +val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t (** The same for inductive types *) -val smart_global_inductive : reference or_by_notation -> inductive +val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e5ed58be6..7b01b6dc1 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -11,6 +11,8 @@ open Genarg open Geninterp +type 'a and_short_name = 'a * Names.lident option + let make0 ?dyn name = let wit = Genarg.make0 name in let () = register_val0 wit dyn in @@ -34,9 +36,6 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" -let wit_intro_pattern = - make0 "intropattern" - let wit_ident = make0 "ident" @@ -45,8 +44,6 @@ let wit_var = let wit_ref = make0 "ref" -let wit_quant_hyp = make0 "quant_hyp" - let wit_sort_family = make0 "sort_family" let wit_constr = @@ -56,12 +53,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" - -let wit_bindings = make0 "bindings" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = @@ -74,6 +65,4 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dc9c370a1..4792cda08 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -17,9 +17,11 @@ open Libnames open Genredexpr open Pattern open Constrexpr -open Misctypes -open Tactypes open Genarg +open Genintern +open Locus + +type 'a and_short_name = 'a * lident option val wit_unit : unit uniform_genarg_type @@ -35,16 +37,12 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type - val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_quant_hyp : quantified_hypothesis uniform_genarg_type - val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type @@ -54,21 +52,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_open_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_bindings : - (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type - val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, @@ -83,8 +66,6 @@ val wit_preident : string uniform_genarg_type val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type -val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/interp/tactypes.ml b/interp/tactypes.ml deleted file mode 100644 index 83e42be89..000000000 --- a/interp/tactypes.ml +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Tactic-related types that are not totally Ltac specific and still used in - lower API. It's not clear whether this is a temporary API or if this is - meant to stay. *) - -open Names -open Constrexpr -open Pattern -open Misctypes - -(** In globalize tactics, we need to keep the initial [constr_expr] to recompute - in the environment by the effective calls to Intro, Inversion, etc - The [constr_expr] field is [None] in TacDef though *) -type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option -type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t -type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t |