diff options
120 files changed, 958 insertions, 730 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index c1a95cdb2..8ba207000 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -68,6 +68,8 @@ Goptions Decls Heads Assumptions +Locusops +Miscops Termops Namegen Evd diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2e74b809f..d45e6b9b3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -28,6 +28,8 @@ open Nametab open Notation open Reserve open Detyping +open Misctypes +open Decl_kinds (*i*) (* Translation from glob_constr to front constr *) @@ -218,7 +220,7 @@ let rec check_same_type ty1 ty2 = | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () - | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) -> + | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> check_same_type a1 a2; check_same_type b1 b2 | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> @@ -644,7 +646,8 @@ let extern_optimal_prim_token scopes r r' = (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GProp _ as s -> s + | GProp -> GProp + | GSet -> GSet | GType (Some _) as s when !print_universes -> s | GType _ -> GType None @@ -811,10 +814,9 @@ let rec extern inctx scopes vars r = | GHole (loc,e) -> CHole (loc, Some e) - | GCast (loc,c, CastConv (k,t)) -> - CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) - | GCast (loc,c, CastCoerce) -> - CCast (loc,sub_extern true scopes vars c, CastCoerce) + | GCast (loc,c, c') -> + CCast (loc,sub_extern true scopes vars c, + Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index c112506ab..21c33f3f3 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -18,6 +18,7 @@ open Glob_term open Pattern open Topconstr open Notation +open Misctypes val check_same_type : constr_expr -> constr_expr -> unit diff --git a/interp/constrintern.ml b/interp/constrintern.ml index af48a37c9..4467cf9f2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -23,6 +23,8 @@ open Topconstr open Nametab open Notation open Inductiveops +open Misctypes +open Decl_kinds (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -1516,10 +1518,8 @@ let internalize sigma globalenv env allow_patvar lvar c = GEvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> GSort(loc,s) - | CCast (loc, c1, CastConv (k, c2)) -> - GCast (loc,intern env c1, CastConv (k, intern_type env c2)) - | CCast (loc, c1, CastCoerce) -> - GCast (loc,intern env c1, CastCoerce) + | CCast (loc, c1, c2) -> + GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2) and intern_type env = intern (set_type_scope env) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 7d0009021..b1bc63658 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -17,6 +17,8 @@ open Pattern open Topconstr open Termops open Pretyping +open Misctypes +open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) diff --git a/interp/genarg.ml b/interp/genarg.ml index 0d640640b..3597879de 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -16,6 +16,7 @@ open Glob_term open Topconstr open Term open Evd +open Misctypes type argument_type = (* Basic types *) @@ -43,11 +44,6 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string -type 'a and_short_name = 'a * identifier located option -type 'a or_by_notation = - | AN of 'a - | ByNotation of (loc * string * Notation.delimiters option) - let loc_of_or_by_notation f = function | AN c -> f c | ByNotation (loc,s,_) -> loc @@ -68,16 +64,6 @@ type rlevel type glevel type tlevel -type intro_pattern_expr = - | IntroOrAndPattern of or_and_intro_pattern_expr - | IntroWildcard - | IntroRewrite of bool - | IntroIdentifier of identifier - | IntroFresh of identifier - | IntroForthcoming of bool - | IntroAnonymous -and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list - let rec pr_intro_pattern (_,pat) = match pat with | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll | IntroWildcard -> str "_" diff --git a/interp/genarg.mli b/interp/genarg.mli index 540fc400c..0368e99e0 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -16,12 +16,7 @@ open Pattern open Topconstr open Term open Evd - -type 'a and_short_name = 'a * identifier located option - -type 'a or_by_notation = - | AN of 'a - | ByNotation of (loc * string * Notation.delimiters option) +open Misctypes val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc @@ -37,16 +32,6 @@ type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern type 'a with_ebindings = 'a * open_constr bindings -type intro_pattern_expr = - | IntroOrAndPattern of or_and_intro_pattern_expr - | IntroWildcard - | IntroRewrite of bool - | IntroIdentifier of identifier - | IntroFresh of identifier - | IntroForthcoming of bool - | IntroAnonymous -and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list - val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e92699f64..3384d79a5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -25,6 +25,7 @@ open Typeclasses_errors open Pp open Libobject open Nameops +open Misctypes (*i*) let generalizable_table = ref Idpred.empty @@ -182,7 +183,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty in array_fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bound vs c in - (match k with CastConv (_,t) -> vars bound v t | _ -> v) + (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bound vs (loc,idl,p,c) = diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 043c255a4..66efe5982 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -17,7 +17,7 @@ open Errors open Util open Names open Libnames -open Genarg +open Misctypes open Syntax_def open Topconstr diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 0c7bc6157..b4e121b4b 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -9,7 +9,7 @@ open Pp open Names open Libnames -open Genarg +open Misctypes (** [locate_global_with_alias] locates global reference possibly following a notation if this notation has a role of aliasing; raise Not_found diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1a86170f3..d3773305a 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -16,6 +16,8 @@ open Libnames open Glob_term open Term open Mod_subst +open Misctypes +open Decl_kinds (*i*) (**********************************************************************) @@ -148,10 +150,7 @@ let glob_constr_of_aconstr_with_binders loc g f e = function (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = array_fold_map (to_id g) e idl in GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | ACast (c,k) -> GCast (loc,f e c, - match k with - | CastConv (k,t) -> CastConv (k,f e t) - | CastCoerce -> CastCoerce) + | ACast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) | ASort x -> GSort (loc,x) | AHole x -> GHole (loc,x) | APatVar n -> GPatVar (loc,(false,n)) @@ -315,9 +314,7 @@ let aconstr_and_vars_of_glob_constr a = error "Binders marked as implicit not allowed in notations."; add_name found na; (na,Option.map aux oc,aux b))) dll in ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (_,c,k) -> ACast (aux c, - match k with CastConv (k,t) -> CastConv (k,aux t) - | CastCoerce -> CastCoerce) + | GCast (_,c,k) -> ACast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> ASort s | GHole (_,w) -> AHole w | GRef (_,r) -> ARef r @@ -495,16 +492,9 @@ let rec subst_aconstr subst bound raw = |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw | ACast (r1,k) -> - match k with - CastConv (k, r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - ACast (r1',CastConv (k,r2')) - | CastCoerce -> - let r1' = subst_aconstr subst bound r1 in - if r1' == r1 then raw else - ACast (r1',CastCoerce) + let r1' = subst_aconstr subst bound r1 in + let k' = Miscops.smartmap_cast_type (subst_aconstr subst bound) k in + if r1' == r1 && k' == k then raw else ACast(r1',k') let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in @@ -728,7 +718,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in array_fold_left2 (match_in u alp metas) sigma bl1 bl2 - | GCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> + | GCast(_,c1,CastConv t1), ACast (c2,CastConv t2) + | GCast(_,c1,CastVM t1), ACast (c2,CastVM t2) -> match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> match_in u alp metas sigma c1 c2 @@ -1079,7 +1070,7 @@ let fold_constr_expr_with_binders g f n acc = function | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] - | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b + | CCast (loc,a,(CastConv b|CastVM b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bll)) -> (* The following is an approximation: we don't know exactly if @@ -1236,8 +1227,7 @@ let map_constr_expr_with_binders g f e = function | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) - | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b)) - | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce) + | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c) | CNotation (loc,n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll, diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 48871432e..101c39eea 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -13,6 +13,8 @@ open Libnames open Glob_term open Term open Mod_subst +open Misctypes +open Decl_kinds (** Topconstr: definitions of [aconstr] et [constr_expr] *) diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6ee6f707d..d20bae0b5 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -8,9 +8,9 @@ (** Informal mathematical status of declarations *) -type locality = - | Local - | Global +type locality = Local | Global + +type binding_kind = Explicit | Implicit type theorem_kind = | Theorem diff --git a/intf/locus.mli b/intf/locus.mli new file mode 100644 index 000000000..b69117547 --- /dev/null +++ b/intf/locus.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Misctypes + +(** Locus : positions in hypotheses and goals *) + +(** {6 Occurrences} *) + +type 'a occurrences_gen = + | AllOccurrences + | AllOccurrencesBut of 'a list (** non-empty *) + | NoOccurrences + | OnlyOccurrences of 'a list (** non-empty *) + +type occurrences_expr = (int or_var) occurrences_gen +type 'a with_occurrences = occurrences_expr * 'a + +type occurrences = int occurrences_gen + + +(** {6 Locations} + + Selecting the occurrences in body (if any), in type, or in both *) + +type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly + + +(** {6 Abstract clauses expressions} + + A [clause_expr] (and its instance [clause]) denotes occurrences and + hypotheses in a goal in an abstract way; in particular, it can refer + to the set of all hypotheses independently of the effective contents + of the current goal + + Concerning the field [onhyps]: + - [None] means *on every hypothesis* + - [Some l] means on hypothesis belonging to l *) + +type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag + +type 'id clause_expr = + { onhyps : 'id hyp_location_expr list option; + concl_occs : occurrences_expr } + +type clause = identifier clause_expr + + +(** {6 Concrete view of occurrence clauses} *) + +(** [clause_atom] refers either to an hypothesis location (i.e. an + hypothesis with occurrences and a position, in body if any, in type + or in both) or to some occurrences of the conclusion *) + +type clause_atom = + | OnHyp of identifier * occurrences_expr * hyp_location_flag + | OnConcl of occurrences_expr + +(** A [concrete_clause] is an effective collection of occurrences + in the hypotheses and the conclusion *) + +type concrete_clause = clause_atom list + + +(** {6 A weaker form of clause with no mention of occurrences} *) + +(** A [hyp_location] is an hypothesis together with a location *) + +type hyp_location = identifier * hyp_location_flag + +(** A [goal_location] is either an hypothesis (together with a location) + or the conclusion (represented by None) *) + +type goal_location = hyp_location option + + +(** {6 Simple clauses, without occurrences nor location} *) + +(** A [simple_clause] is a set of hypotheses, possibly extended with + the conclusion (conclusion is represented by None) *) + +type simple_clause = identifier option list diff --git a/intf/misctypes.mli b/intf/misctypes.mli new file mode 100644 index 000000000..9d6820346 --- /dev/null +++ b/intf/misctypes.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Libnames + +(** Basic types used both in [constr_expr] and in [glob_constr] *) + +(** Cases pattern variables *) + +type patvar = identifier + +(** Introduction patterns *) + +type intro_pattern_expr = + | IntroOrAndPattern of or_and_intro_pattern_expr + | IntroWildcard + | IntroRewrite of bool + | IntroIdentifier of identifier + | IntroFresh of identifier + | IntroForthcoming of bool + | IntroAnonymous +and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list + + +(** Sorts *) + +type glob_sort = GProp | GSet | GType of Univ.universe option + +(** Casts *) + +type 'a cast_type = + | CastConv of 'a + | CastVM of 'a + | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier + +type 'a explicit_bindings = (Pp.loc * quantified_hypothesis * 'a) list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings + + +(** Some utility types for parsing *) + +type 'a or_var = + | ArgArg of 'a + | ArgVar of Names.identifier Pp.located + +type 'a and_short_name = 'a * identifier Pp.located option + +type 'a or_by_notation = + | AN of 'a + | ByNotation of (Pp.loc * string * string option) + +(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], + but this formulation avoids a useless dependency. *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 238400806..fc3f94920 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -9,7 +9,7 @@ open Pp open Names open Tacexpr -open Genarg +open Misctypes open Topconstr open Decl_kinds open Libnames @@ -133,7 +133,7 @@ type option_ref_value = | StringRefValue of string | QualidRefValue of reference -type sort_expr = Glob_term.glob_sort +type sort_expr = glob_sort type definition_expr = | ProveBody of local_binder list * constr_expr diff --git a/kernel/typeops.mli b/kernel/typeops.mli index c1c805f38..ae2b76754 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -32,8 +32,10 @@ val assumption_of_judgment : env -> unsafe_judgment -> types val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment (** {6 Type of sorts. } *) -val judge_of_prop_contents : contents -> unsafe_judgment -val judge_of_type : universe -> unsafe_judgment +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment +val judge_of_prop_contents : contents -> unsafe_judgment +val judge_of_type : universe -> unsafe_judgment (** {6 Type of a bound variable. } *) val judge_of_relative : env -> int -> unsafe_judgment diff --git a/library/declare.ml b/library/declare.ml index f3df8347e..10e8f3a5d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -65,11 +65,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,cst = match d with (* Fails if not well-typed *) | SectionLocalAssum (ty, impl) -> let cst = Global.push_named_assum (id,ty) in - let impl = if impl then Lib.Implicit else Lib.Explicit in + let impl = if impl then Implicit else Explicit in impl, true, cst | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in - Lib.Explicit, opaq, cst in + Explicit, opaq, cst in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl; Dischargedhypsmap.set_discharged_hyps sp []; diff --git a/library/impargs.ml b/library/impargs.ml index 6b01c5fb1..d7d0d4879 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -22,6 +22,7 @@ open Pp open Topconstr open Termops open Namegen +open Decl_kinds (*s Flags governing the computation of implicit arguments *) @@ -485,7 +486,9 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,list_smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, (true,true)) else None) + List.rev_map + (fun (id,impl,_,_) -> + if impl = Implicit then Some (id, Manual, (true,true)) else None) (List.filter (fun (_,_,b,_) -> b = None) ctx) let section_segment_of_reference = function diff --git a/library/lib.ml b/library/lib.ml index 40a427e49..ff7e9b841 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -395,14 +395,14 @@ let find_opening_node id = - the list of variables on which each inductive depends in this section - the list of substitution to do at section closing *) -type binding_kind = Explicit | Implicit -type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_info = Names.identifier * Decl_kinds.binding_kind * Term.constr option * Term.types type variable_context = variable_info list type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t let sectab = - ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * Decl_kinds.binding_kind) list * + Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab diff --git a/library/lib.mli b/library/lib.mli index 781ecfe32..360eada85 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -176,10 +176,9 @@ val init : unit -> unit val set_xml_open_section : (Names.identifier -> unit) -> unit val set_xml_close_section : (Names.identifier -> unit) -> unit -type binding_kind = Explicit | Implicit - (** {6 Section management for discharge } *) -type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_info = Names.identifier * Decl_kinds.binding_kind * + Term.constr option * Term.types type variable_context = variable_info list val instance_from_variable_context : variable_context -> Names.identifier array @@ -191,7 +190,7 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont val section_instance : Libnames.global_reference -> Names.identifier array val is_in_section : Libnames.global_reference -> bool -val add_section_variable : Names.identifier -> binding_kind -> unit +val add_section_variable : Names.identifier -> Decl_kinds.binding_kind -> unit val add_section_constant : Names.constant -> Sign.named_context -> unit val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 06d922a7c..c8ca6cbab 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -18,6 +18,8 @@ open Topconstr open Util open Tok open Compat +open Misctypes +open Decl_kinds let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; @@ -29,7 +31,7 @@ let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty) let binders_of_names l = List.map (fun (loc, na) -> @@ -38,7 +40,7 @@ let binders_of_names l = let binders_of_lidents l = List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, + LocalRawAssum ([loc, Name id], Default Explicit, CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -144,8 +146,8 @@ GEXTEND Gram [ [ c = lconstr -> c ] ] ; sort: - [ [ "Set" -> GProp Pos - | "Prop" -> GProp Null + [ [ "Set" -> GSet + | "Prop" -> GProp | "Type" -> GType None ] ] ; lconstr: @@ -160,13 +162,13 @@ GEXTEND Gram [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - CCast(loc,c1, CastConv (VMcast,c2)) + CCast(loc,c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> - CCast(loc,c1, CastConv (VMcast,c2)) + CCast(loc,c1, CastVM c2) | c1 = operconstr; ":";c2 = binder_constr -> - CCast(loc,c1, CastConv (DEFAULTcast,c2)) + CCast(loc,c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv (DEFAULTcast,c2)) + CCast(loc,c1, CastConv c2) | c1 = operconstr; ":>" -> CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] @@ -410,7 +412,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] + [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))] | "{"; id=name; "}" -> [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index bf0e13e02..e2edbb096 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -17,6 +17,7 @@ open Pcoq open Prim open Tactic open Tok +open Misctypes let fail_default_value = ArgArg 0 @@ -177,7 +178,7 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) + | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index fd6fc7dd8..d6b2d8380 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -86,8 +86,8 @@ GEXTEND Gram [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ] ; smart_global: - [ [ c = reference -> Genarg.AN c - | ntn = by_notation -> Genarg.ByNotation ntn ] ] + [ [ c = reference -> Misctypes.AN c + | ntn = by_notation -> Misctypes.ByNotation ntn ] ] ; qualid: [ [ qid = basequalid -> loc, qid ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5f44a9e9c..6edb0bfc1 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -17,6 +17,7 @@ open Locality open Prim open Constr open Tok +open Misctypes let thm_token = G_vernac.thm_token @@ -113,6 +114,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8b72a5e93..7cbcd584c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -18,6 +18,9 @@ open Libnames open Termops open Tok open Compat +open Misctypes +open Locus +open Decl_kinds let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] @@ -166,17 +169,17 @@ let mkCLambdaN_simple bl c = let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) let map_int_or_var f = function - | Glob_term.ArgArg x -> Glob_term.ArgArg (f x) - | Glob_term.ArgVar _ as y -> y + | ArgArg x -> ArgArg (f x) + | ArgVar _ as y -> y -let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr } +let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } let has_no_specified_occs cl = (cl.onhyps = None || - List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr) + List.for_all (fun ((occs,_),_) -> occs = AllOccurrences) (Option.get cl.onhyps)) - && (cl.concl_occs = all_occurrences_expr - || cl.concl_occs = no_occurrences_expr) + && (cl.concl_occs = AllOccurrences + || cl.concl_occs = NoOccurrences) let merge_occurrences loc cl = function | None -> @@ -185,11 +188,11 @@ let merge_occurrences loc cl = function user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.") | Some (occs,p) -> (Some p, - if occs = all_occurrences_expr then cl + if occs = AllOccurrences then cl else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs } else match cl.onhyps with | Some [(occs',id),l] when - occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr -> + occs' = AllOccurrences && cl.concl_occs = NoOccurrences -> { cl with onhyps=Some[(occs,id),l] } | _ -> if has_no_specified_occs cl then @@ -205,12 +208,12 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Glob_term.ArgArg n - | id = identref -> Glob_term.ArgVar id ] ] + [ [ n = integer -> ArgArg n + | id = identref -> ArgVar id ] ] ; nat_or_var: - [ [ n = natural -> Glob_term.ArgArg n - | id = identref -> Glob_term.ArgVar id ] ] + [ [ n = natural -> ArgArg n + | id = identref -> ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -236,18 +239,18 @@ GEXTEND Gram ; conversion: [ [ c = constr -> (None, c) - | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2) + | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2) | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> (Some (occs,c1), c2) ] ] ; occs_nums: - [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl + [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl | "-"; n = nat_or_var; nl = LIST0 int_or_var -> (* have used int_or_var instead of nat_or_var for compatibility *) - all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ] + AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ] ; occs: - [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ] + [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ] ; pattern_occ: [ [ c = constr; nl = occs -> (nl,c) ] ] @@ -374,7 +377,7 @@ GEXTEND Gram | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> {onhyps=Some hl; concl_occs=occs} | hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ] + {onhyps=Some hl; concl_occs=NoOccurrences} ] ] ; clause_dft_concl: [ [ "in"; cl = in_clause -> cl @@ -383,14 +386,14 @@ GEXTEND Gram ; clause_dft_all: [ [ "in"; cl = in_clause -> cl - | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ] + | -> {onhyps=None; concl_occs=AllOccurrences} ] ] ; opt_clause: [ [ "in"; cl = in_clause -> Some cl | -> None ] ] ; concl_occ: [ [ "*"; occs = occs -> occs - | -> no_occurrences_expr ] ] + | -> NoOccurrences ] ] ; in_hyp_list: [ [ "in"; idl = LIST1 id_or_meta -> idl @@ -546,9 +549,9 @@ GEXTEND Gram TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacLetTac (Names.Name id,b,nowhere,true) + TacLetTac (Names.Name id,b,Locusops.nowhere,true) | IDENT "pose"; b = constr; na = as_name -> - TacLetTac (na,b,nowhere,true) + TacLetTac (na,b,Locusops.nowhere,true) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> TacLetTac (Names.Name id,c,p,true) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> @@ -572,9 +575,9 @@ GEXTEND Gram | IDENT "cut"; c = constr -> TacCut c | IDENT "generalize"; c = constr -> - TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)] + TacGeneralize [((AllOccurrences,c),Names.Anonymous)] | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in + let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in TacGeneralize (List.map gen_everywhere (c::l)) | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; na = as_name; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f684b9a0d..34e0d9532 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -23,6 +23,7 @@ open Genarg open Ppextend open Goptions open Declaremods +open Misctypes open Prim open Constr @@ -240,7 +241,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -343,7 +344,7 @@ GEXTEND Gram (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, Glob_term.CastConv (_, t)) -> + | CCast(_,b, (CastConv t|CastVM t)) -> (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | _ -> (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ] @@ -568,7 +569,7 @@ GEXTEND Gram VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> Some r | ":="; c = lconstr -> Some c | -> None ] -> @@ -714,7 +715,7 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> VernacInstance (true, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 3cb553437..7c26ac124 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -20,6 +20,8 @@ open Libnames open Nametab open Detyping open Tok +open Misctypes +open Decl_kinds (* Generic xml parser without raw data *) @@ -96,8 +98,8 @@ let inductive_of_cdata a = match global_of_cdata a with let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) let sort_of_cdata (loc,a) = match a with - | "Prop" -> GProp Null - | "Set" -> GProp Pos + | "Prop" -> GProp + | "Set" -> GSet | "Type" -> GType None | _ -> user_err_loc (loc,"",str "sort expected.") @@ -191,7 +193,7 @@ let rec interp_xml_constr = function let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) + GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> GSort (loc, get_xml_sort al) | XmlTag (loc,s,_,_) -> diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 39fd88506..cae4b13d6 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -56,11 +56,13 @@ Lib Goptions Decl_kinds Global +Locusops Termops Namegen Evd Reductionops Inductiveops +Miscops Glob_term Detyping Pattern diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ebcc53264..5bc6bddd9 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -17,6 +17,7 @@ open Topconstr open Tacexpr open Libnames open Compat +open Misctypes (** The parser of Coq *) @@ -220,7 +221,7 @@ module Tactic : val int_or_var : int or_var Gram.entry val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_atomic_tactic_expr Gram.entry - val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry + val simple_intropattern : intro_pattern_expr located Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 98ed6883e..45ea77d13 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -21,6 +21,9 @@ open Pattern open Glob_term open Constrextern open Termops +open Decl_kinds +open Misctypes +open Locus (*i*) let sep_v = fun _ -> str"," ++ spc() @@ -110,8 +113,8 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_universe = Univ.pr_uni let pr_glob_sort = function - | GProp Term.Null -> str "Prop" - | GProp Term.Pos -> str "Set" + | GProp -> str "Prop" + | GSet -> str "Set" | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) let pr_id = pr_id @@ -253,7 +256,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,k,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c, CastConv (_,t)) -> c, t + | CCast(_,c, (CastConv t|CastVM t)) -> c, t | _ -> c, CHole (dummy_loc, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) @@ -530,13 +533,12 @@ let pr pr sep inherited a = | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_glob_sort s, latom - | CCast (_,a,CastConv (k,b)) -> - let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in - hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), - lcast - | CCast (_,a,CastCoerce) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), - lcast + | CCast (_,a,b) -> + hv 0 (pr mt (lcast,L) a ++ cut () ++ + match b with + | CastConv b -> str ":" ++ pr mt (-lcast,E) b + | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastCoerce -> str ":>"), lcast | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> @@ -581,12 +583,15 @@ let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders spc (pr ltop) -let pr_with_occurrences pr occs = +let pr_with_occurrences pr (occs,c) = match occs with - ((false,[]),c) -> pr c - | ((nowhere_except_in,nl),c) -> + | AllOccurrences -> pr c + | NoOccurrences -> failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> hov 1 (pr c ++ spc() ++ str"at " ++ - (if nowhere_except_in then mt() else str "- ") ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc() ++ str"at - " ++ hov 0 (prlist_with_sep spc (pr_or_var int) nl)) let pr_red_flag pr r = diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index c61d4c206..1497c90e7 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -16,7 +16,8 @@ open Topconstr open Names open Errors open Util -open Genarg +open Misctypes +open Locus val extract_lam_binders : constr_expr -> local_binder list * constr_expr diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 513034194..c50ab9fcd 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -20,6 +20,9 @@ open Pattern open Ppextend open Ppconstr open Printer +open Misctypes +open Locus +open Decl_kinds let pr_global x = Nametab.pr_global_env Idset.empty x @@ -384,11 +387,11 @@ let pr_by_tactic prt = function | tac -> spc() ++ str "by " ++ prt tac let pr_hyp_location pr_id = function - | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs - | occs, Termops.InHypTypeOnly -> + | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, InHypTypeOnly -> spc () ++ pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs - | occs, Termops.InHypValueOnly -> + | occs, InHypValueOnly -> spc () ++ pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs @@ -403,17 +406,17 @@ let pr_in_hyp_as pr_id = function | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat let pr_clauses default_is_concl pr_id = function - | { onhyps=Some []; concl_occs=occs } - when occs = all_occurrences_expr & default_is_concl = Some true -> mt () - | { onhyps=None; concl_occs=occs } - when occs = all_occurrences_expr & default_is_concl = Some false -> mt () + | { onhyps=Some []; concl_occs=AllOccurrences } + when default_is_concl = Some true -> mt () + | { onhyps=None; concl_occs=AllOccurrences } + when default_is_concl = Some false -> mt () | { onhyps=None; concl_occs=occs } -> - if occs = no_occurrences_expr then pr_in (str " * |-") + if occs = NoOccurrences then pr_in (str " * |-") else pr_in (pr_with_occurrences (fun () -> str " *") (occs,())) | { onhyps=Some l; concl_occs=occs } -> pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ - (if occs = no_occurrences_expr then mt () + (if occs = NoOccurrences then mt () else pr_with_occurrences (fun () -> str" |- *") (occs,()))) let pr_orient b = if b then mt () else str " <-" @@ -690,7 +693,7 @@ and pr_atom1 = function | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg c) - | TacLetTac (na,c,cl,true) when cl = nowhere -> + | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere -> hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c) | TacLetTac (na,c,cl,b) -> hov 1 ((if b then str "set" else str "remember") ++ diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index d85f1ec3f..afcc83c68 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -17,6 +17,7 @@ open Pattern open Ppextend open Environ open Evd +open Misctypes val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index fad4e879e..5dbef1fe5 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -31,6 +31,7 @@ open Printmod open Libnames open Nametab open Recordops +open Misctypes type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -644,11 +645,11 @@ let print_any_name = function "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_name = function - | Genarg.ByNotation (loc,ntn,sc) -> + | ByNotation (loc,ntn,sc) -> print_any_name (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) - | Genarg.AN ref -> + | AN ref -> print_any_name (locate_any_name ref) let print_opaque_name qid = @@ -686,11 +687,11 @@ let print_about_any k = hov 0 (pr_located_qualid k) ++ fnl() let print_about = function - | Genarg.ByNotation (loc,ntn,sc) -> + | ByNotation (loc,ntn,sc) -> print_about_any (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) - | Genarg.AN ref -> + | AN ref -> print_about_any (locate_any_name ref) (* for debug *) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 40ba7f047..b3271d141 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -16,7 +16,7 @@ open Environ open Reductionops open Libnames open Nametab -open Genarg +open Misctypes (** A Pretty-Printer for the Calculus of Inductive Constructions. *) diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index f5225feb3..543240a82 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -17,6 +17,7 @@ open Pp open Compat open Pcaml open PcamlSig +open Misctypes let loc = dummy_loc let dloc = <:expr< Pp.dummy_loc >> @@ -33,8 +34,8 @@ EXTEND <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> GProp Pos - | "Prop" -> GProp Null + [ [ "Set" -> GSet + | "Prop" -> GProp | "Type" -> GType None ] ] ; ident: @@ -49,9 +50,9 @@ EXTEND constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> (* fix todo *) @@ -61,7 +62,7 @@ EXTEND <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ] + <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index f36465207..6ef7ba1d8 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -51,18 +51,18 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> let mlexpr_of_loc loc = <:expr< $dloc$ >> let mlexpr_of_by_notation f = function - | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> - | Genarg.ByNotation (loc,s,sco) -> - <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> + | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >> + | Misctypes.ByNotation (loc,s,sco) -> + <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> let mlexpr_of_intro_pattern = function - | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> - | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> - | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> - | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> - | Genarg.IntroIdentifier id -> - <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> - | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ -> + | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >> + | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> + | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> + | Misctypes.IntroIdentifier id -> + <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ -> failwith "mlexpr_of_intro_pattern: TODO" let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) @@ -72,34 +72,40 @@ let mlexpr_of_or_metaid f = function | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> let mlexpr_of_quantified_hypothesis = function - | Glob_term.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> - | Glob_term.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> + | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> + | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> let mlexpr_of_or_var f = function - | Glob_term.ArgArg x -> <:expr< Glob_term.ArgArg $f x$ >> - | Glob_term.ArgVar id -> <:expr< Glob_term.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> + | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >> + | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) -let mlexpr_of_occs = - mlexpr_of_pair - mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)) +let mlexpr_of_occs = function + | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >> + | Locus.AllOccurrencesBut l -> + <:expr< Locus.AllOccurrencesBut + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> + | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >> + | Locus.OnlyOccurrences l -> + <:expr< Locus.OnlyOccurrences + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f let mlexpr_of_hyp_location = function - | occs, Termops.InHyp -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >> - | occs, Termops.InHypTypeOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >> - | occs, Termops.InHypValueOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >> + | occs, Locus.InHyp -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >> + | occs, Locus.InHypTypeOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >> + | occs, Locus.InHypValueOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >> let mlexpr_of_clause cl = - <:expr< {Tacexpr.onhyps= + <:expr< {Locus.onhyps= $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) - cl.Tacexpr.onhyps$; - Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >> + cl.Locus.onhyps$; + Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >> let mlexpr_of_red_flags { Glob_term.rBeta = bb; @@ -120,8 +126,8 @@ let mlexpr_of_explicitation = function | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >> let mlexpr_of_binding_kind = function - | Glob_term.Implicit -> <:expr< Glob_term.Implicit >> - | Glob_term.Explicit -> <:expr< Glob_term.Explicit >> + | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >> + | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >> let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> @@ -215,14 +221,14 @@ let rec mlexpr_of_may_eval f = function <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >> let mlexpr_of_binding_kind = function - | Glob_term.ExplicitBindings l -> + | Misctypes.ExplicitBindings l -> let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in - <:expr< Glob_term.ExplicitBindings $l$ >> - | Glob_term.ImplicitBindings l -> + <:expr< Misctypes.ExplicitBindings $l$ >> + | Misctypes.ImplicitBindings l -> let l = mlexpr_of_list mlexpr_of_constr l in - <:expr< Glob_term.ImplicitBindings $l$ >> - | Glob_term.NoBindings -> - <:expr< Glob_term.NoBindings >> + <:expr< Misctypes.ImplicitBindings $l$ >> + | Misctypes.NoBindings -> + <:expr< Misctypes.NoBindings >> let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a1e968668..58111f597 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -19,6 +19,8 @@ open Glob_term open Term open Pp open Compat +open Decl_kinds +open Misctypes (* INTERN *) @@ -194,7 +196,7 @@ let abstract_one_hyp inject h glob = let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let glob_prop = GSort (dummy_loc,GProp Null) +let glob_prop = GSort (dummy_loc,GProp) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -345,13 +347,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null) + Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Glob_term.GSort(dummy_loc,GProp Null) + Glob_term.GSort(dummy_loc,GProp) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps glob_prop in let loc_ids,npatt = @@ -361,7 +363,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let term2 = GLetIn(dummy_loc,Anonymous, GCast(dummy_loc,glob_of_pat npatt, - CastConv (DEFAULTcast,app_ind)),term1) in + CastConv app_ind),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 2870e8f7e..956a561aa 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,7 +29,7 @@ open Termops open Namegen open Reductionops open Goptions - +open Misctypes (* Strictness option *) @@ -237,7 +237,7 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) + tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere) (thin_body [id]) gls in tclMAP add_aux items gls @@ -750,7 +750,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) + (forward None (Some (dummy_loc, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls @@ -781,7 +781,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac None (Name id) t None Tacexpr.nowhere gls + letin_tac None (Name id) t None Locusops.nowhere gls (* tactics for reconsider *) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 8d580d235..a45d3075f 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -25,6 +25,7 @@ open Formula open Sequent open Names open Libnames +open Misctypes let compare_instance inst1 inst2= match inst1,inst2 with @@ -181,12 +182,12 @@ let right_instance_tac inst continue seq= [tclTHENLIST [introf; (fun gls-> - split (Glob_term.ImplicitBindings + split (ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Glob_term.ImplicitBindings [t])) + (tclTHEN (split (ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b56fe4e50..a226cc455 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -18,6 +18,7 @@ open Declarations open Formula open Sequent open Libnames +open Locus type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -203,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [all_occurrences,EvalConstRef (destConst (constant "not")); - all_occurrences,EvalConstRef (destConst (constant "iff"))] + [AllOccurrences,EvalConstRef (destConst (constant "not")); + AllOccurrences,EvalConstRef (destConst (constant "iff"))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4d5cbe223..5bf772fc5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -15,6 +15,7 @@ open Tacticals open Tactics open Indfun_common open Libnames +open Misctypes let msgnl = Pp.msgnl @@ -441,13 +442,8 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = decompose_prod_n_assum (List.length context) reduced_type_of_hyp in tclTHENLIST - [ - h_reduce_with_zeta - (Tacticals.onHyp hyp_id) - ; - scan_type new_context new_typ_of_hyp - - ] + [ h_reduce_with_zeta (Locusops.onHyp hyp_id); + scan_type new_context new_typ_of_hyp ] else if isProd type_of_hyp then begin @@ -688,13 +684,13 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id if args_id = [] then tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; do_prove hyps ] else tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; tclMAP instanciate_one_hyp hyps; (fun g -> let all_g_hyps_id = @@ -732,7 +728,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [(false,[1]),t] None; + pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( tclTHENSEQ [h_simplest_case t; (fun g' -> @@ -818,9 +814,10 @@ let build_proof tclTHENLIST [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + (fun hyp_id -> + h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g @@ -850,9 +847,9 @@ let build_proof tclTHENLIST [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g | Rel _ -> anomaly "Free var in goal conclusion !" @@ -1010,7 +1007,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings)); intros_reflexivity] g ) ] @@ -1346,7 +1343,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)]; + [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1442,12 +1439,12 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let build_clause eqs = { - Tacexpr.onhyps = + Locus.onhyps = Some (List.map - (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp) + (fun id -> (Locus.AllOccurrences, id), Locus.InHyp) eqs ); - Tacexpr.concl_occs = Glob_term.no_occurrences_expr + Locus.concl_occs = Locus.NoOccurrences } let rec rewrite_eqs_in_eqs eqs = @@ -1460,7 +1457,8 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences + true (* dep proofs also: *) true id (mkVar eq) false)) gl ) eqs @@ -1482,7 +1480,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 0f776ee6e..b38503cb9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -15,6 +15,7 @@ open Tacticals open Tactics open Indfun_common open Functional_principles_proofs +open Misctypes exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -504,7 +505,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in let funs = List.map fst fas in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 1c02c16ec..00d130d28 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,6 +1,6 @@ open Names open Term - +open Misctypes val generate_functional_principle : (* do we accept interactive proving *) @@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found -val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list +val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list -val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit -val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit +val build_scheme : (identifier*Libnames.reference*glob_sort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e8fec0dd8..aed71c3ae 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -17,19 +17,20 @@ open Genarg open Pcoq open Tacticals open Constr +open Misctypes let pr_binding prc = function - | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function - | Glob_term.ImplicitBindings l -> + | ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence prc l - | Glob_term.ExplicitBindings l -> + | ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Glob_term.NoBindings -> mt () + | NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) @@ -308,7 +309,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = let typ = Tacmach.pf_type_of gl cstr in tclTHEN - (Tactics.letin_tac None (Name idunsafe) cstr None allHypsAndConcl) + (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl) (tclTHENFIRST (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 954e389a4..f18309d04 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -8,6 +8,7 @@ open Indfun_common open Errors open Util open Glob_termops +open Misctypes let observe strm = if do_observe () @@ -1258,7 +1259,8 @@ let rec rebuild_return_type rt = Topconstr.CProdN(loc,n,rebuild_return_type t') | Topconstr.CLetIn(loc,na,t,t') -> Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],Topconstr.Default Glob_term.Explicit,rt], + | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], + Topconstr.Default Decl_kinds.Explicit,rt], Topconstr.CSort(dummy_loc,GType None)) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b14197891..6433fe37c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -3,6 +3,9 @@ open Glob_term open Errors open Util open Names +open Decl_kinds +open Misctypes + (* Ocaml 3.06 Map.S does not handle is_empty *) let idmap_is_empty m = m = Idmap.empty @@ -19,7 +22,7 @@ let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(dummy_loc,s) let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous) -let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) +let mkGCast(b,t) = GCast(dummy_loc,b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -180,10 +183,9 @@ let change_vars = | GRec _ -> error "Local (co)fixes are not supported" | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv (k,t)) -> - GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,change_vars mapping b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,change_vars mapping b, + Miscops.map_cast_type (change_vars mapping) c) and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in if idmap_is_empty new_mapping @@ -360,10 +362,9 @@ let rec alpha_rt excluded rt = | GRec _ -> error "Not handled GRec" | GSort _ -> rt | GHole _ -> rt - | GCast (loc,b,CastConv (k,t)) -> - GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | GCast (loc,b,CastCoerce) -> - GCast(loc,alpha_rt excluded b,CastCoerce) + | GCast (loc,b,c) -> + GCast(loc,alpha_rt excluded b, + Miscops.map_cast_type (alpha_rt excluded) c) | GApp(loc,f,args) -> GApp(loc, alpha_rt excluded f, @@ -411,7 +412,7 @@ let is_free_in id = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,(CastConv t|CastVM t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -507,10 +508,9 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,replace_var_by_pattern b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,replace_var_by_pattern b, + Miscops.map_cast_type replace_var_by_pattern c) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl then br @@ -593,7 +593,7 @@ let ids_of_glob_constr c = | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,(CastConv t|CastVM t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc | GLetTuple (_,nal,(na,po),b,c) -> @@ -661,10 +661,9 @@ let zeta_normalize = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,zeta_normalize_term b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,zeta_normalize_term b, + Miscops.map_cast_type zeta_normalize_term c) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -702,8 +701,9 @@ let expand_as = GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" - | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,expand_as map b, + Miscops.map_cast_type (expand_as map) c) | GCases(loc,sty,po,el,brl) -> GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 80a8811f1..761337b07 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,4 +1,5 @@ open Glob_term +open Misctypes (* Ocaml 3.06 Map.S does not handle is_empty *) val idmap_is_empty : 'a Names.Idmap.t -> bool diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 42df294a0..96bde6f1b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -7,6 +7,8 @@ open Indfun_common open Libnames open Glob_term open Declarations +open Misctypes +open Decl_kinds let is_rec_info scheme_info = let test_branche min acc (_,_,br) = @@ -64,7 +66,7 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ) + (princ,NoBindings, Tacmach.pf_type_of g princ) | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> @@ -109,7 +111,7 @@ let functional_induction with_clean c princl pat = in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl ) - (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) + (Hiddentac.h_reduce flag Locusops.allHypsAndConcl) g else Tacticals.tclIDTAC g in @@ -480,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let b = Names.id_of_string "___b" in Topconstr.mkLambdaC( [dummy_loc,Name a;dummy_loc,Name b], - Topconstr.Default Lib.Explicit, + Topconstr.Default Explicit, wf_arg_type, Topconstr.mkAppC(wf_rel_expr, [ @@ -744,10 +746,9 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,CastConv(ck,b2)) -> - CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) - | CCast(loc,b1,CastCoerce) -> - CCast(loc,add_args id new_args b1,CastCoerce) + | CCast(loc,b1,b2) -> + CCast(loc,add_args id new_args b1, + Miscops.map_cast_type (add_args id new_args) b2) | CRecord (loc, w, pars) -> CRecord (loc, (match w with Some w -> Some (add_args id new_args w) | _ -> None), diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index faa5f2e46..c0b72f0b3 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -7,6 +7,7 @@ open Indfun_common open Libnames open Glob_term open Declarations +open Misctypes val do_generate_principle : bool -> @@ -17,8 +18,8 @@ val do_generate_principle : val functional_induction : bool -> Term.constr -> - (Term.constr * Term.constr Glob_term.bindings) option -> - Genarg.intro_pattern_expr Pp.located option -> + (Term.constr * Term.constr bindings) option -> + intro_pattern_expr Pp.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b92a8daf3..667be89d0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,22 +19,23 @@ open Indfun_common open Tacmach open Sign open Hiddentac +open Misctypes (* Some pretty printing function for debugging purpose *) let pr_binding prc = function - | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function - | Glob_term.ImplicitBindings l -> + | ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence prc l - | Glob_term.ExplicitBindings l -> + | ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Glob_term.NoBindings -> mt () + | NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -272,7 +273,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.map (fun (_,_,br_type) -> List.map - (fun id -> dummy_loc, Genarg.IntroIdentifier id) + (fun id -> dummy_loc, IntroIdentifier id) (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches @@ -319,7 +320,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem match b with | None -> pre_tac | Some b -> - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac else pre_tac ) (pf_hyps g) @@ -330,7 +331,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_right (fun (_,pat) acc -> match pat with - | Genarg.IntroIdentifier id -> id::acc + | IntroIdentifier id -> id::acc | _ -> anomaly "Not an identifier" ) (List.nth intro_pats (pred i)) @@ -420,7 +421,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Glob_term.rConst = [] } ) - onConcl; + Locusops.onConcl; observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -571,7 +572,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) ) @@ -754,15 +755,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Termops.InHyp) )) + unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; + tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Termops.InHyp) )) + unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; + tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -797,7 +798,7 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Glob_term.NoBindings); + h_case false (v,NoBindings); intros_with_rewrite ] g | LetIn _ -> @@ -807,7 +808,7 @@ and intros_with_rewrite_aux : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; intros_with_rewrite ] g @@ -822,7 +823,7 @@ and intros_with_rewrite_aux : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; intros_with_rewrite ] g @@ -834,7 +835,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Glob_term.NoBindings); + h_case false (v,NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -961,12 +962,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))] + else unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in @@ -1004,7 +1005,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -1056,7 +1057,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs)) + (make_scheme (array_map_to_list (fun const -> const,GType None) funs)) ) in let proving_tac = @@ -1209,7 +1210,7 @@ let functional_inversion kn hid fconst f_correct : tactic = let pre_tac,f_args,res = match kind_of_term args.(1),kind_of_term args.(2) with | App(f,f_args),_ when eq_constr f fconst -> - ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2)) + ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2)) |_,App(f,f_args) when eq_constr f fconst -> ((fun hid -> tclIDTAC),f_args,args.(1)) | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) @@ -1219,7 +1220,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; h_intro hid; - Inv.inv FullInversion None (Glob_term.NamedHyp hid); + Inv.inv FullInversion None (NamedHyp hid); (fun g -> let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3ea9c3d3e..0ec5f7bce 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -23,6 +23,7 @@ open Declarations open Environ open Glob_term open Glob_termops +open Decl_kinds (** {1 Utilities} *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8eb7d0e8f..d11909043 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -44,7 +44,7 @@ open Equality open Auto open Eauto -open Genarg +open Misctypes open Indfun_common @@ -288,7 +288,7 @@ let tclUSER tac is_mes l g = if is_mes then tclTHENLIST [ - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]; tac ] @@ -566,9 +566,9 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = tclTHENLIST[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; - observe_tac (str "simple_iter") (simpl_iter onConcl); + observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") - (unfold_in_concl[((true,[1]), + (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)]); observe_tac (str "test" ) ( tclTHENLIST[ @@ -685,7 +685,7 @@ let mkDestructEq : [h_generalize new_hyps; (fun g2 -> change_in_concl None - (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case expr], to_revert @@ -857,7 +857,7 @@ let rec make_rewrite_list expr_info max = function let def_na,_,_ = destProd t in Nameops.out_name k_na,Nameops.out_name def_na in - general_rewrite_bindings false Termops.all_occurrences + general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[dummy_loc,NamedHyp def, @@ -883,7 +883,8 @@ let make_rewrite expr_info l hp max = let def_na,_,_ = destProd t in Nameops.out_name k_na,Nameops.out_name def_na in - observe_tac (str "general_rewrite_bindings") (general_rewrite_bindings false Termops.all_occurrences + observe_tac (str "general_rewrite_bindings") + (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[dummy_loc,NamedHyp def, @@ -892,9 +893,9 @@ let make_rewrite expr_info l hp max = [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (tclTHENLIST[ - simpl_iter onConcl; + simpl_iter Locusops.onConcl; observe_tac (str "unfold functional") - (unfold_in_concl[((true,[1]), + (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)]); (list_rewrite true @@ -1413,7 +1414,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)]; + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; observe_tac (str "simplest_case") (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))); diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 9deeb6066..cd87e93ec 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -21,6 +21,7 @@ open Ring open Mutils open Glob_term open Errors +open Misctypes let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 1057c646f..2c82bab7b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -34,6 +34,7 @@ open Logic open Libnames open Nametab open Contradiction +open Misctypes module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -129,12 +130,12 @@ let intern_id,unintern_id = let mk_then = tclTHENLIST -let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c]) +let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) -let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s] +let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = let rec loop = function diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index b3151f26c..4bf08912a 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -827,9 +827,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences true false c'i_eq_c''i) + Locus.AllOccurrences true false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences true false c'i_eq_c''i)) + Locus.AllOccurrences true false c'i_eq_c''i)) [tac])) else (tclORELSE diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index e834650ac..a74666fdd 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -33,6 +33,7 @@ open Printer open Declare open Decl_kinds open Entries +open Misctypes (****************************************************************************) (* controlled reduction *) @@ -102,7 +103,7 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; TACTIC EXTEND protect_fv diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 33e1ecdf2..832d32086 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,6 +25,8 @@ open Libnames open Nametab open Evd open Mod_subst +open Misctypes +open Decl_kinds let dl = dummy_loc @@ -361,7 +363,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function - | Prop c -> GProp c + | Prop Null -> GProp + | Prop Pos -> GSet | Type u -> GType (Some u) type binder_kind = BProd | BLambda | BLetIn @@ -391,7 +394,9 @@ let rec detype (isgoal:bool) avoid env t = GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) | Cast (c1,k,c2) -> - GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) + let d1 = detype isgoal avoid env c1 in + let d2 = detype isgoal avoid env c2 in + GCast(dl,d1,if k = VMcast then CastVM d2 else CastConv d2) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c @@ -668,14 +673,9 @@ let rec subst_glob_constr subst raw = |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _)) -> raw | GCast (loc,r1,k) -> - (match k with - CastConv (k,r2) -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in - if r1' == r1 && r2' == r2 then raw else - GCast (loc,r1', CastConv (k,r2')) - | CastCoerce -> - let r1' = subst_glob_constr subst r1 in - if r1' == r1 then raw else GCast (loc,r1',k)) + let r1' = subst_glob_constr subst r1 in + let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + if r1' == r1 && k' == k then raw else GCast (loc,r1',k') (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f9592194c..439609b02 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -15,6 +15,7 @@ open Environ open Glob_term open Termops open Mod_subst +open Misctypes val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ab11df450..e49f2b4eb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -662,7 +662,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with - | Some (false,[]) -> mkVar id + | Some Locus.AllOccurrences -> mkVar id | Some _ -> error "Selection of specific occurrences not supported" | None -> let evty = set_holes evdref cty subst in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 3e2ca7aed..3d3760f18 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -13,6 +13,7 @@ open Environ open Termops open Reductionops open Evd +open Locus (** returns exception Reduction.NotConvertible if not unifiable *) val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index fc1e1247f..466e73b8e 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -15,6 +15,9 @@ open Sign open Term open Libnames open Nametab +open Decl_kinds +open Misctypes +open Locus (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -29,27 +32,6 @@ let cases_pattern_loc = function PatVar(loc,_) -> loc | PatCstr(loc,_,_,_) -> loc -type patvar = identifier - -type glob_sort = GProp of Term.contents | GType of Univ.universe option - -type binding_kind = Lib.binding_kind = Explicit | Implicit - -type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier - -type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list - -type 'a bindings = - | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_bindings - | NoBindings - -type 'a with_bindings = 'a * 'a bindings - -type 'a cast_type = - | CastConv of cast_kind * 'a - | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) - type glob_constr = | GRef of (loc * global_reference) | GVar of (loc * identifier) @@ -142,7 +124,7 @@ let map_glob_constr_left_to_right f = function GRec (loc,fk,idl,comp1,comp2,comp3) | GCast (loc,c,k) -> let comp1 = f c in - let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in + let comp2 = Miscops.map_cast_type f k in GCast (loc,comp1,comp2) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x @@ -204,7 +186,7 @@ let fold_glob_constr f acc = (List.fold_left (fun acc (na,k,bbd,bty) -> fold (Option.fold_left fold acc bbd) bty)) acc bl in Array.fold_left fold (Array.fold_left fold acc tyl) bv - | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c + | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc and fold_pattern acc (_,idl,p,c) = fold acc c @@ -243,7 +225,7 @@ let occur_glob_constr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) + | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -301,7 +283,7 @@ let free_glob_vars = in array_fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv (_,t) -> vars bounded v t | _ -> v) + (match k with CastConv t | CastVM t -> vars bounded v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = @@ -380,17 +362,6 @@ type 'a glob_red_flag = { let all_flags = {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} -type 'a or_var = ArgArg of 'a | ArgVar of identifier located - -type occurrences_expr = bool * int or_var list - -let all_occurrences_expr_but l = (false,l) -let no_occurrences_expr_but l = (true,l) -let all_occurrences_expr = (false,[]) -let no_occurrences_expr = (true,[]) - -type 'a with_occurrences = occurrences_expr * 'a - type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index d7d182833..f654925ef 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -19,6 +19,9 @@ open Sign open Term open Libnames open Nametab +open Decl_kinds +open Misctypes +open Locus (** The kind of patterns that occurs in "match ... with ... end" @@ -30,27 +33,6 @@ type cases_pattern = val cases_pattern_loc : cases_pattern -> loc -type patvar = identifier - -type glob_sort = GProp of Term.contents | GType of Univ.universe option - -type binding_kind = Lib.binding_kind = Explicit | Implicit - -type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier - -type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list - -type 'a bindings = - | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_bindings - | NoBindings - -type 'a with_bindings = 'a * 'a bindings - -type 'a cast_type = - | CastConv of cast_kind * 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) - type glob_constr = | GRef of (loc * global_reference) | GVar of (loc * identifier) @@ -137,17 +119,6 @@ type 'a glob_red_flag = { val all_flags : 'a glob_red_flag -type 'a or_var = ArgArg of 'a | ArgVar of identifier located - -type occurrences_expr = bool * int or_var list - -val all_occurrences_expr_but : int or_var list -> occurrences_expr -val no_occurrences_expr_but : int or_var list -> occurrences_expr -val all_occurrences_expr : occurrences_expr -val no_occurrences_expr : occurrences_expr - -type 'a with_occurrences = occurrences_expr * 'a - type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml new file mode 100644 index 000000000..5f136c536 --- /dev/null +++ b/pretyping/locusops.ml @@ -0,0 +1,81 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Misctypes +open Locus + +(** Utilities on occurrences *) + +let occurrences_map f = function + | OnlyOccurrences l -> + let l' = f l in + if l' = [] then NoOccurrences else OnlyOccurrences l' + | AllOccurrencesBut l -> + let l' = f l in + if l' = [] then AllOccurrences else AllOccurrencesBut l' + | (NoOccurrences|AllOccurrences) as o -> o + +let convert_occs = function + | AllOccurrences -> (false,[]) + | AllOccurrencesBut l -> (false,l) + | NoOccurrences -> (true,[]) + | OnlyOccurrences l -> (true,l) + +let is_selected occ = function + | AllOccurrences -> true + | AllOccurrencesBut l -> not (List.mem occ l) + | OnlyOccurrences l -> List.mem occ l + | NoOccurrences -> false + +(** Usual clauses *) + +let allHypsAndConcl = { onhyps=None; concl_occs=AllOccurrences } +let allHyps = { onhyps=None; concl_occs=NoOccurrences } +let onConcl = { onhyps=Some[]; concl_occs=AllOccurrences } +let nowhere = { onhyps=Some[]; concl_occs=NoOccurrences } +let onHyp h = + { onhyps=Some[(AllOccurrences,h),InHyp]; concl_occs=NoOccurrences } + + +(** Clause conversion functions, parametrized by a hyp enumeration function *) + +(** From [clause] to [simple_clause] *) + +let simple_clause_of enum_hyps cl = + let error_occurrences () = + Errors.error "This tactic does not support occurrences selection" in + let error_body_selection () = + Errors.error "This tactic does not support body selection" in + let hyps = + match cl.onhyps with + | None -> + List.map Option.make (enum_hyps ()) + | Some l -> + List.map (fun ((occs,id),w) -> + if occs <> AllOccurrences then error_occurrences (); + if w = InHypValueOnly then error_body_selection (); + Some id) l in + if cl.concl_occs = NoOccurrences then hyps + else + if cl.concl_occs <> AllOccurrences then error_occurrences () + else None :: hyps + +(** From [clause] to [concrete_clause] *) + +let concrete_clause_of enum_hyps cl = + let hyps = + match cl.onhyps with + | None -> + let f id = OnHyp (id,AllOccurrences,InHyp) in + List.map f (enum_hyps ()) + | Some l -> + List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in + if cl.concl_occs = NoOccurrences then hyps + else + OnConcl cl.concl_occs :: hyps diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli new file mode 100644 index 000000000..285d9412e --- /dev/null +++ b/pretyping/locusops.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Misctypes +open Locus + +(** Utilities on occurrences *) + +val occurrences_map : + ('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen + +(** From occurrences to a list of positions (or complement of positions) *) +val convert_occs : occurrences -> bool * int list + +val is_selected : int -> occurrences -> bool + +(** Usual clauses *) + +val allHypsAndConcl : 'a clause_expr +val allHyps : 'a clause_expr +val onConcl : 'a clause_expr +val nowhere : 'a clause_expr +val onHyp : 'a -> 'a clause_expr + +(** Clause conversion functions, parametrized by a hyp enumeration function *) + +val simple_clause_of : (unit -> identifier list) -> clause -> simple_clause +val concrete_clause_of : (unit -> identifier list) -> clause -> concrete_clause diff --git a/pretyping/matching.ml b/pretyping/matching.ml index ac0022c8c..6be95cd82 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -20,6 +20,7 @@ open Glob_term open Sign open Environ open Pattern +open Misctypes (*i*) (* Given a term with second-order variables in it, @@ -170,7 +171,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst + | PSort GProp, Sort (Prop Null) -> subst + + | PSort GSet, Sort (Prop Pos) -> subst | PSort (GType _), Sort (Type _) -> subst diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml new file mode 100644 index 000000000..2528d57f3 --- /dev/null +++ b/pretyping/miscops.ml @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Misctypes +open Pp +open Nameops + +let map_cast_type f = function + | CastConv a -> CastConv (f a) + | CastVM a -> CastVM (f a) + | CastCoerce -> CastCoerce + +let smartmap_cast_type f c = + match c with + | CastConv a -> let a' = f a in if a' == a then c else CastConv a' + | CastVM a -> let a' = f a in if a' == a then c else CastVM a' + | CastCoerce -> CastCoerce + +(** Printing of [intro_pattern] *) + +let rec pr_intro_pattern (_,pat) = match pat with + | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll + | IntroWildcard -> str "_" + | IntroRewrite true -> str "->" + | IntroRewrite false -> str "<-" + | IntroIdentifier id -> pr_id id + | IntroFresh id -> str "?" ++ pr_id id + | IntroForthcoming true -> str "*" + | IntroForthcoming false -> str "**" + | IntroAnonymous -> str "?" + +and pr_or_and_intro_pattern = function + | [pl] -> + str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")" + | pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) + ++ str "]" diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli new file mode 100644 index 000000000..b8f6f6860 --- /dev/null +++ b/pretyping/miscops.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Misctypes + +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type + +val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type + +(** Printing of [intro_pattern] *) + +val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds +val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 47cc57fd1..ef81aa4d3 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -17,6 +17,8 @@ open Environ open Nametab open Pp open Mod_subst +open Misctypes +open Decl_kinds (* Metavariables *) @@ -100,7 +102,8 @@ let pattern_of_constr sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop c) -> PSort (GProp c) + | Sort (Prop Null) -> PSort GProp + | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType None) | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index e6ec9a498..f9c2358b7 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -18,6 +18,7 @@ open Libnames open Nametab open Glob_term open Mod_subst +open Misctypes (** {5 Maps of pattern variables} *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d2553828f..82f030ae0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -44,6 +44,7 @@ open Pretype_errors open Glob_term open Evarconv open Pattern +open Misctypes type typing_constraint = OfType of types option | IsType type var_map = (identifier * constr_under_binders) list @@ -95,12 +96,13 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) let interp_sort = function - | GProp c -> Prop c + | GProp -> Prop Null + | GSet -> Prop Pos | GType _ -> new_Type_sort () let interp_elimination_sort = function - | GProp Null -> InProp - | GProp Pos -> InSet + | GProp -> InProp + | GSet -> InSet | GType _ -> InType let resolve_evars env evdref fail_evar resolve_classes = @@ -239,7 +241,8 @@ let pretype_ref evdref env ref = make_judge c (Retyping.get_type_of env Evd.empty c) let pretype_sort evdref = function - | GProp c -> judge_of_prop_contents c + | GProp -> judge_of_prop + | GSet -> judge_of_set | GType _ -> evd_comb0 judge_of_new_Type evdref exception Found of fixpoint @@ -474,7 +477,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function | GLetIn(loc,name,c1,c2) -> let j = match c1 with - | GCast (loc, c, CastConv (DEFAULTcast, t)) -> + | GCast (loc, c, CastConv t) -> let tj = pretype_type empty_valcon env evdref lvar t in pretype (mk_tycon tj.utj_val) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 @@ -632,7 +635,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj - | CastConv (k,t) -> + | CastConv t | CastVM t -> + let k = (match k with CastVM _ -> VMcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in let tval = nf_evar !evdref tj.utj_val in let cj = match k with diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 75e507afd..9401edc2d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -19,6 +19,7 @@ open Environ open Evd open Glob_term open Evarutil +open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 199adf6a7..e520602db 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Locusops Termops Evd Reductionops @@ -13,6 +14,7 @@ Recordops Evarconv Arguments_renaming Typing +Miscops Glob_term Pattern Matching diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index cc1f6f941..6ff469012 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -25,6 +25,7 @@ open Cbv open Glob_term open Pattern open Matching +open Locus (* Errors *) @@ -842,7 +843,8 @@ let matches_head c t = | App (f,_) -> matches c f | _ -> raise PatternMatchingFailure -let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = +let contextually byhead (occs,c) f env sigma t = + let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref 1 in let rec traverse (env,c as envc) t = @@ -913,15 +915,20 @@ let unfold env sigma name = * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. * Performs a betaiota reduction after unfolding. *) -let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = - if locs = [] then if nowhere_except_in then c else unfold env sigma name c - else - let (nbocc,uc) = substlin env name 1 plocs c in +let unfoldoccs env sigma (occs,name) c = + let unfo nowhere_except_in locs = + let (nbocc,uc) = substlin env name 1 (nowhere_except_in,locs) c in if nbocc = 1 then error ((string_of_evaluable_ref env name)^" does not occur."); let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; nf_betaiotazeta sigma uc + in + match occs with + | NoOccurrences -> c + | AllOccurrences -> unfold env sigma name c + | OnlyOccurrences l -> unfo true l + | AllOccurrencesBut l -> unfo false l (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 8fd14dccb..c9b139ac9 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -16,6 +16,7 @@ open Glob_term open Termops open Pattern open Libnames +open Locus type reduction_tactic_error = InvalidAbstraction of env * constr * (env * Type_errors.type_error) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f64625707..a9cb72504 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -16,6 +16,7 @@ open Sign open Environ open Libnames open Nametab +open Locus (* Sorts and sort family *) @@ -692,15 +693,6 @@ let replace_term = replace_term_gen eq_constr occurrence except the ones in l and b=false, means all occurrences except the ones in l *) -type hyp_location_flag = (* To distinguish body and type of local defs *) - | InHyp - | InHypTypeOnly - | InHypValueOnly - -type occurrences = bool * int list -let all_occurrences = (false,[]) -let no_occurrences_in_set = (true,[]) - let error_invalid_occurrence l = let l = list_uniquize (List.sort Pervasives.compare l) in errorlabstrm "" @@ -715,7 +707,7 @@ let pr_position (cl,pos) = | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in int pos ++ clpos -let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_except_in,locs) = +let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) = let s = if nested then "Found nested occurrences of the pattern" else "Found incompatible occurrences of the pattern" in errorlabstrm "" @@ -726,10 +718,6 @@ let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_e quote (print_constr t1) ++ strbrk " at position " ++ pr_position (cl1,pos1) ++ str ".") -let is_selected pos (nowhere_except_in,locs) = - nowhere_except_in && List.mem pos locs || - not nowhere_except_in && not (List.mem pos locs) - exception NotUnifiable type 'a testing_function = { @@ -739,7 +727,8 @@ type 'a testing_function = { mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option } -let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t = +let subst_closed_term_occ_gen_modulo occs test cl occ t = + let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref occ in let nested = ref false in @@ -749,12 +738,12 @@ let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl o test.last_found <- Some (cl,!pos,t) with NotUnifiable -> let lastpos = Option.get test.last_found in - error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in + error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos in let rec substrec k t = if nowhere_except_in & !pos > maxocc then t else try let subst = test.match_fun t in - if is_selected !pos plocs then + if Locusops.is_selected !pos occs then (add_subst t subst; incr pos; (* Check nested matching subterms *) nested := true; ignore (subst_below k t); nested := false; @@ -770,15 +759,15 @@ let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl o let t' = substrec 1 t in (!pos, t') -let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] - let check_used_occurrences nbocc (nowhere_except_in,locs) = let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest -let proceed_with_occurrences f plocs x = - if is_nowhere plocs then (* optimization *) x else - begin +let proceed_with_occurrences f occs x = + if occs = NoOccurrences then x + else begin + (* TODO FINISH ADAPTING WITH HUGO *) + let plocs = Locusops.convert_occs occs in assert (List.for_all (fun x -> x >= 0) (snd plocs)); let (nbocc,x) = f 1 x in check_used_occurrences nbocc plocs; @@ -792,16 +781,17 @@ let make_eq_test c = { last_found = None } -let subst_closed_term_occ_gen plocs pos c t = - subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t +let subst_closed_term_occ_gen occs pos c t = + subst_closed_term_occ_gen_modulo occs (make_eq_test c) None pos t -let subst_closed_term_occ plocs c t = - proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c) - plocs t +let subst_closed_term_occ occs c t = + proceed_with_occurrences + (fun occ -> subst_closed_term_occ_gen occs occ c) + occs t -let subst_closed_term_occ_modulo plocs test cl t = +let subst_closed_term_occ_modulo occs test cl t = proceed_with_occurrences - (subst_closed_term_occ_gen_modulo plocs test cl) plocs t + (subst_closed_term_occ_gen_modulo occs test cl) occs t let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = let f = f (Some (id,hyploc)) in diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 68db293b6..e5dc2448b 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -13,6 +13,7 @@ open Names open Term open Sign open Environ +open Locus (** Universes *) val new_univ_level : unit -> Univ.universe_level @@ -145,11 +146,6 @@ val subst_term : constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -(** In occurrences sets, false = everywhere except and true = nowhere except *) -type occurrences = bool * int list -val all_occurrences : occurrences -val no_occurrences_in_set : occurrences - (** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at positions [occl], counting from [n], by [Rel 1] in [d] *) val subst_closed_term_occ_gen : @@ -161,11 +157,6 @@ val subst_closed_term_occ_gen : failing with NotUnifiable) and an initial substitution are required too *) -type hyp_location_flag = (** To distinguish body and type of local defs *) - | InHyp - | InHypTypeOnly - | InHypValueOnly - type 'a testing_function = { match_fun : constr -> 'a; merge_fun : 'a -> 'a -> 'a; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2344f6e46..fd40cca7c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -25,6 +25,7 @@ open Pretype_errors open Retyping open Coercion open Recordops +open Locus let occur_meta_or_undefined_evar evd c = let rec occrec c = match kind_of_term c with @@ -56,7 +57,7 @@ let abstract_scheme env c l lname_typ = let abstract_list_all env evd typ c l = let ctxt,_ = splay_prod_n env evd (List.length l) typ in - let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in + let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in try if is_conv_leq env evd (Typing.type_of env evd p) typ then p @@ -65,7 +66,7 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l let set_occurrences_of_last_arg args = - Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args) + Some AllOccurrences :: List.tl (array_map_to_list (fun _ -> None) args) let abstract_list_all_with_dependencies env evd typ c l = let evd,ev = new_evar evd env typ in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index cfe69c705..23a21414d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -27,6 +27,7 @@ open Evarutil open Unification open Mod_subst open Coercion +open Misctypes (* Abbreviations *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 04f532654..e0ad1acf9 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -17,6 +17,7 @@ open Evarutil open Mod_subst open Glob_term open Unification +open Misctypes (** {6 The Type of Constructions clausale environments.} *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index bddf77d1f..21948b481 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -21,6 +21,7 @@ open Closure open RedFlags open Libobject open Summary +open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = @@ -169,8 +170,8 @@ let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" | ArgArg x -> x -let out_with_occurrences ((b,l),c) = - ((b,List.map out_arg l), c) +let out_with_occurrences (occs,c) = + (Locusops.occurrences_map (List.map out_arg) occs, c) let rec reduction_of_red_expr = function | Red internal -> diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index ae82153d2..99f942e11 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -13,6 +13,7 @@ open Pattern open Glob_term open Reductionops open Termops +open Locus type red_expr = (constr, evaluable_global_reference, constr_pattern) red_expr_gen diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b48605657..4f960243c 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -17,6 +17,8 @@ open Util open Genarg open Pattern open Decl_kinds +open Misctypes +open Locus type 'a or_metaid = AI of 'a | MetaId of loc * string @@ -60,7 +62,7 @@ let make_red_flag = add_flag {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} -type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag +type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag type 'id move_location = | MoveAfter of 'id @@ -100,21 +102,12 @@ type 'id message_token = | MsgInt of int | MsgIdent of 'id -(* onhyps: - [None] means *on every hypothesis* - [Some l] means on hypothesis belonging to l *) -type 'id gclause = - { onhyps : 'id raw_hyp_location list option; - concl_occs : occurrences_expr } - -let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} - type 'constr induction_clause = ('constr with_bindings induction_arg list * 'constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) type ('constr,'id) induction_clause_list = - 'constr induction_clause list * 'id gclause option + 'constr induction_clause list * 'id clause_expr option type multi = | Precisely of int @@ -162,7 +155,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = | TacAssert of 'tac option * intro_pattern_expr located option * 'constr | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr - | TacLetTac of name * 'constr * 'id gclause * letin_flag + | TacLetTac of name * 'constr * 'id clause_expr * letin_flag (* Derived basic tactics *) | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis @@ -193,17 +186,17 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = | TacConstructor of evars_flag * int or_var * 'constr bindings (* Conversion *) - | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause - | TacChange of 'pat option * 'constr * 'id gclause + | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id clause_expr + | TacChange of 'pat option * 'constr * 'id clause_expr (* Equivalence relations *) | TacReflexivity - | TacSymmetry of 'id gclause + | TacSymmetry of 'id clause_expr | TacTransitivity of 'constr option (* Equality and inversion *) | TacRewrite of - evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option + evars_flag * (bool * multi * 'constr with_bindings) list * 'id clause_expr * 'tac option | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 402002de1..86a1edd76 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -18,6 +18,7 @@ open Redexpr open Tacexpr open Glob_term open Pattern +open Locus (** Operations for handling terms under a local typing context. *) @@ -71,7 +72,7 @@ val pf_nf_betaiota : goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types val pf_compute : goal sigma -> constr -> constr -val pf_unfoldn : (Termops.occurrences * evaluable_global_reference) list +val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> constant -> constr diff --git a/tactics/auto.ml b/tactics/auto.ml index 8b4f5eb61..6e338c4cb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -42,6 +42,8 @@ open Printer open Declarations open Tacexpr open Mod_subst +open Misctypes +open Locus (****************************************************************************) (* The Type of Constructions Autotactic Hints *) @@ -1316,7 +1318,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) = | Unfold_nth c -> (fun gl -> if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl + tclPROGRESS (h_reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl else tclFAIL 0 (str"Unbound reference") gl) | Extern tacast -> conclPattern concl p tacast in diff --git a/tactics/auto.mli b/tactics/auto.mli index 49a7ef305..0dfcb0b68 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -20,6 +20,7 @@ open Evd open Libnames open Vernacexpr open Mod_subst +open Misctypes (** Auto and related automation tactics *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 990da9306..4981e7033 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -22,6 +22,7 @@ open Glob_term open Vernacinterp open Tacexpr open Mod_subst +open Locus (* Rewriting rules *) type rew_rule = { rew_lemma: constr; @@ -118,7 +119,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = tclTHEN tac (one_base (fun dir c tac -> let tac = tac, conds in - general_rewrite dir all_occurrences true false ~tac c) + general_rewrite dir AllOccurrences true false ~tac c) tac_main bas)) tclIDTAC lbas)) @@ -136,7 +137,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis: " ^ (string_of_id !id) ^".") in - let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in + let gl' = general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false gl in let gls = gl'.Evd.it in match gls with g::_ -> @@ -172,8 +173,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs <> all_occurrences_expr & - cl.concl_occs <> no_occurrences_expr + if cl.concl_occs <> AllOccurrences & + cl.concl_occs <> NoOccurrences then error "The \"at\" syntax isn't available yet for the autorewrite tactic." else @@ -183,7 +184,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | _ -> tclTHENFIRST t1 t2 in compose_tac - (if cl.concl_occs <> no_occurrences_expr then autorewrite ~conds tac_main lbas else tclIDTAC) + (if cl.concl_occs <> NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC) (match cl.onhyps with | Some l -> try_do_hyps (fun ((_,id),_) -> id) l | None -> @@ -196,8 +197,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = - let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in - match onconcl,cl.Tacexpr.onhyps with + let onconcl = cl.Locus.concl_occs <> NoOccurrences in + match onconcl,cl.Locus.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> (* autorewrite with .... in clause using tac n'est sur que si clause represente soit le but soit UNE hypothese diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 6481217b6..a3fc72959 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -35,9 +35,9 @@ val find_rewrites : string -> rew_rule list val find_matches : string -> constr -> rew_rule list -val auto_multi_rewrite : ?conds:conditions -> string list -> Tacticals.clause -> tactic +val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> tactic -val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Tacticals.clause -> tactic +val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Locus.clause -> tactic val print_rewrite_hintdb : string -> unit diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index f4c032e73..cafe17ad9 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -37,6 +37,8 @@ open Command open Libnames open Evd open Compat +open Locus +open Misctypes let typeclasses_db = "typeclass_instances" let typeclasses_debug = ref false @@ -177,7 +179,7 @@ and e_my_find_search db_list local_db hdc complete concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags)) (if complete then tclIDTAC else e_trivial_fail_db db_list local_db) - | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c]) + | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]) | Extern tacast -> (* tclTHEN *) (* (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *) @@ -807,7 +809,7 @@ let rec head_of_constr t = TACTIC EXTEND head_of_constr [ "head_of_constr" ident(h) constr(c) ] -> [ let c = head_of_constr c in - letin_tac None (Name h) c None allHyps + letin_tac None (Name h) c None Locusops.allHyps ] END diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c4cf7b62f..76ee9ff68 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -17,6 +17,7 @@ open Tactics open Coqlib open Reductionops open Glob_term +open Misctypes (* Absurd *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index b77b2721a..302098139 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -9,8 +9,7 @@ open Names open Term open Proof_type -open Glob_term -open Genarg +open Misctypes val absurd : constr -> tactic val contradiction : constr with_bindings option -> tactic diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 2700b2b7d..8b773762f 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -29,6 +29,9 @@ open Auto open Glob_term open Hiddentac open Tacexpr +open Misctypes +open Locus +open Locusops let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } @@ -73,7 +76,7 @@ let prolog_tac l n gl = let l = List.map (prepare_hint (pf_env gl)) l in let n = match n with - | ArgArg n -> n + | ArgArg n -> n | _ -> error "Prolog called with a non closed argument." in try (prolog l n gl) @@ -134,7 +137,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> h_reduce (Unfold [all_occurrences_expr,c]) onConcl + | Unfold_nth c -> h_reduce (Unfold [AllOccurrences,c]) onConcl | Extern tacast -> conclPattern concl p tacast in (tac,lazy (pr_autotactic t))) @@ -459,12 +462,12 @@ let autounfolds db occs = with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in - Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts - (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) + Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts + (Idset.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in unfold_option unfolds let autounfold db cls gl = - let cls = concrete_clause_of cls gl in + let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in let tac = autounfolds db in tclMAP (function | OnHyp (id,occs,where) -> tac occs (Some (id,where)) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 5e656139b..e0893f439 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -35,4 +35,4 @@ val eauto_with_bases : bool * int -> open_constr list -> Auto.hint_db list -> Proof_type.tactic -val autounfold : hint_db_name list -> Tacticals.clause -> tactic +val autounfold : hint_db_name list -> Locus.clause -> tactic diff --git a/tactics/elim.mli b/tactics/elim.mli index c40d1cbbc..fe19c0b24 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -12,6 +12,7 @@ open Proof_type open Tacmach open Genarg open Tacticals +open Misctypes (** Eliminations tactics. *) @@ -30,5 +31,5 @@ val h_decompose : inductive list -> constr -> tactic val h_decompose_or : constr -> tactic val h_decompose_and : constr -> tactic -val double_ind : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis -> tactic -val h_double_induction : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis->tactic +val double_ind : quantified_hypothesis -> quantified_hypothesis -> tactic +val h_double_induction : quantified_hypothesis -> quantified_hypothesis->tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index e3b62e496..03f3811b7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -45,6 +45,9 @@ open Clenvtac open Evd open Ind_tables open Eqschemes +open Locus +open Locusops +open Misctypes (* Options *) @@ -317,7 +320,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac ((c,l) : constr with_bindings) with_evars gl = - if occs <> all_occurrences then ( + if occs <> AllOccurrences then ( rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl) else let env = pf_env gl in @@ -367,7 +370,7 @@ let general_rewrite_in l2r occs frzevars dep_proof_ok ?tac id c = frzevars dep_proof_ok ?tac (c,NoBindings) let general_multi_rewrite l2r with_evars ?tac c cl = - let occs_of = on_snd (List.fold_left + let occs_of = occurrences_map (List.fold_left (fun acc -> function ArgArg x -> x :: acc | ArgVar _ -> acc) []) @@ -383,7 +386,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars) (do_hyps l) in - if cl.concl_occs = no_occurrences_expr then do_hyps l else + if cl.concl_occs = NoOccurrences then do_hyps l else tclTHENFIRST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) (do_hyps l) @@ -394,7 +397,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = | [] -> (fun gl -> error "Nothing to rewrite.") | id :: l -> tclIFTHENTRYELSEMUST - (general_rewrite_ebindings_in l2r all_occurrences false true ?tac id c with_evars) + (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) (do_hyps_atleastonce l) in let do_hyps gl = @@ -404,7 +407,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in - if cl.concl_occs = no_occurrences_expr then do_hyps else + if cl.concl_occs = NoOccurrences then do_hyps else tclIFTHENTRYELSEMUST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps @@ -431,8 +434,8 @@ let general_multi_multi_rewrite with_evars l cl tac = | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l) in loop l -let rewriteLR = general_rewrite true all_occurrences true true -let rewriteRL = general_rewrite false all_occurrences true true +let rewriteLR = general_rewrite true AllOccurrences true true +let rewriteRL = general_rewrite false AllOccurrences true true (* Replacing tactics *) @@ -1439,7 +1442,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl = tclTHENLIST ((if need_rewrite then [generalize abshyps; - general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp); + general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); thin dephyps; tclMAP introtac depdecls] else diff --git a/tactics/equality.mli b/tactics/equality.mli index 12deb7d32..098e92721 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -25,6 +25,8 @@ open Termops open Glob_term open Genarg open Ind_tables +open Locus +open Misctypes (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a33b6b19b..4b5229010 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -16,7 +16,7 @@ open Refiner open Proof_type open Evd open Sign -open Termops +open Locus (* The instantiate tactic *) @@ -55,4 +55,4 @@ let let_evar name typ gls = let src = (dummy_loc,Evar_kinds.GoalEvar) in let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') - (Tactics.letin_tac None name evar None nowhere) gls + (Tactics.letin_tac None name evar None Locusops.nowhere) gls diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 882cf3ce6..f32160425 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -9,7 +9,7 @@ open Tacmach open Names open Tacexpr -open Termops +open Locus val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> (identifier * hyp_location_flag, unit) location -> tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index bd1145bd7..4677d87ef 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -15,6 +15,8 @@ open Names open Tacexpr open Tacinterp open Termops +open Misctypes +open Locus (* Rewriting orientation *) @@ -44,6 +46,14 @@ let pr_occurrences _prc _prlc _prt l = | ArgArg x -> pr_int_list x | ArgVar (loc, id) -> Nameops.pr_id id +let occurrences_of = function + | [] -> NoOccurrences + | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + Errors.error "Illegal negative occurrence number."; + OnlyOccurrences nl + let coerce_to_int = function | VInteger n -> n | v -> raise (CannotCoerceTo "an integer") @@ -259,16 +269,16 @@ END let pr_in_arg_hyp = pr_in_arg_hyp_typed () () () -let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = - {Tacexpr.onhyps= +let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : clause = + {onhyps= Option.map (fun l -> List.map - (fun id -> ( (all_occurrences_expr,trad_id id),InHyp)) + (fun id -> ( (AllOccurrences,trad_id id),InHyp)) l ) hyps; - Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr} + concl_occs = if concl then AllOccurrences else NoOccurrences} let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 35344c99c..5d3691b54 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -13,6 +13,7 @@ open Proof_type open Topconstr open Termops open Glob_term +open Misctypes val rawwit_orient : bool raw_abstract_argument_type val globwit_orient : bool glob_abstract_argument_type @@ -23,13 +24,14 @@ val pr_orient : bool -> Pp.std_ppcmds val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type -val pr_occurrences : int list Glob_term.or_var -> Pp.std_ppcmds +val pr_occurrences : int list or_var -> Pp.std_ppcmds +val occurrences_of : int list -> Locus.occurrences val rawwit_glob : constr_expr raw_abstract_argument_type val wit_glob : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type val glob : constr_expr Pcoq.Gram.entry -type 'id gen_place= ('id * hyp_location_flag,unit) location +type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location type loc_place = identifier Pp.located gen_place type place = identifier gen_place @@ -43,8 +45,8 @@ val in_arg_hyp: (Names.identifier Pp.located list option * bool) Pcoq.Gram.ent val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type -val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause -val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause +val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Locus.clause +val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Locus.clause val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e497581ed..a2d1caf5f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -22,6 +22,7 @@ open Util open Evd open Equality open Compat +open Misctypes (**********************************************************************) (* admit, replace, discriminate, injection, simplify_eq *) @@ -230,24 +231,17 @@ let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = Refiner. tclWITHHOLES false (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true -let occurrences_of = function - | n::_ as nl when n < 0 -> (false,List.map abs nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number."; - (true,nl) - TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> [ rewrite_star (Some id) o (occurrences_of occ) c tac ] | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> [ rewrite_star (Some id) o (occurrences_of occ) c tac ] | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star (Some id) o Termops.all_occurrences c tac ] + [ rewrite_star (Some id) o Locus.AllOccurrences c tac ] | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> [ rewrite_star None o (occurrences_of occ) c tac ] | [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] -> - [ rewrite_star None o Termops.all_occurrences c tac ] + [ rewrite_star None o Locus.AllOccurrences c tac ] END (**********************************************************************) @@ -340,7 +334,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (Glob_term.GProp Term.Null) false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] END open Term @@ -351,7 +345,7 @@ VERNAC COMMAND EXTEND DeriveInversion -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (GProp Null) false inv_tac ] + -> [ add_inversion_lemma_exn na c GProp false inv_tac ] | [ "Derive" "Inversion" ident(na) hyp(id) ] -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ] @@ -660,7 +654,7 @@ exception Found of tactic let rewrite_except h g = tclMAP (fun id -> if id = h then tclIDTAC else - tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true true id (mkVar h) false)) + tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) (Tacmach.pf_ids_of_hyps g) g @@ -681,7 +675,7 @@ let mkCaseEq a : tactic = [Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; (fun g2 -> change_in_concl None - (Tacred.pattern_occs [((false,[1]), a)] (Tacmach.pf_env g2) Evd.empty (Tacmach.pf_concl g2)) + (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] (Tacmach.pf_env g2) Evd.empty (Tacmach.pf_concl g2)) g2); simplest_case a] g);; diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 302bde6e6..8410e08cc 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -16,6 +16,8 @@ open Genarg open Tacexpr open Tactics open Util +open Locus +open Misctypes (* Basic tactics *) let h_intro_move x y = @@ -57,7 +59,7 @@ let h_generalize_gen cl = abstract_tactic (TacGeneralize cl) (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) let h_generalize cl = - h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous)) + h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous)) cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c) (generalize_dep c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index ca683cc24..af7a2061b 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -17,6 +17,7 @@ open Glob_term open Evd open Clenv open Termops +open Misctypes (** Tactics for the interpreter. They left a trace in the proof tree when they are called. *) @@ -53,12 +54,12 @@ val h_cofix : identifier option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic -val h_generalize_gen : (constr with_occurrences * name) list -> tactic +val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic val h_let_tac : letin_flag -> name -> constr -> - Tacticals.clause -> tactic + Locus.clause -> tactic val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> - Tacticals.clause -> tactic + Locus.clause -> tactic (** Derived basic tactics *) @@ -69,17 +70,17 @@ val h_new_induction : evars_flag -> (evar_map * constr with_bindings) induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> - Tacticals.clause option -> tactic + Locus.clause option -> tactic val h_new_destruct : evars_flag -> (evar_map * constr with_bindings) induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> - Tacticals.clause option -> tactic + Locus.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> ((evar_map * constr with_bindings) induction_arg list * constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) list - * Tacticals.clause option -> tactic + * Locus.clause option -> tactic val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic @@ -106,13 +107,13 @@ val h_simplest_right : tactic (** Conversion *) -val h_reduce : Redexpr.red_expr -> Tacticals.clause -> tactic +val h_reduce : Redexpr.red_expr -> Locus.clause -> tactic val h_change : - Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic + Pattern.constr_pattern option -> constr -> Locus.clause -> tactic (** Equivalence relations *) val h_reflexivity : tactic -val h_symmetry : Tacticals.clause -> tactic +val h_symmetry : Locus.clause -> tactic val h_transitivity : constr option -> tactic val h_simplest_apply : constr -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index 47e50d832..f5762768e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -34,7 +34,7 @@ open Typing open Pattern open Matching open Glob_term -open Genarg +open Misctypes open Tacexpr let collect_meta_variables c = diff --git a/tactics/inv.mli b/tactics/inv.mli index a7e70dd0d..7dc9feb2c 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -10,7 +10,7 @@ open Pp open Names open Term open Tacmach -open Genarg +open Misctypes open Tacexpr open Glob_term diff --git a/tactics/leminv.mli b/tactics/leminv.mli index d5deff1f5..21fcc0f5d 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -4,6 +4,7 @@ open Term open Glob_term open Proof_type open Topconstr +open Misctypes val lemInv_gen : quantified_hypothesis -> constr -> tactic val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 88170d6dd..04a1734fb 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -38,6 +38,10 @@ open Command open Libnames open Evd open Compat +open Misctypes +open Locus +open Locusops +open Decl_kinds (** Typeclass-based generalized rewriting. *) @@ -631,7 +635,7 @@ let apply_constraint env avoid car rel prf cstr res = let eq_env x y = x == y let apply_rule hypinfo loccs : strategy = - let (nowhere_except_in,occs) = loccs in + let (nowhere_except_in,occs) = convert_occs loccs in let is_occ occ = if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in let occ = ref 0 in @@ -1007,7 +1011,7 @@ module Strategies = let lemmas flags cs : strategy = List.fold_left (fun tac (l,l2r) -> - choice tac (apply_lemma flags l l2r (false,[]))) + choice tac (apply_lemma flags l l2r AllOccurrences)) fail cs let inj_open c = (Evd.empty,c) @@ -1386,8 +1390,8 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy GLOBALIZED BY glob_strategy SUBSTITUTED BY subst_strategy - [ constr(c) ] -> [ apply_constr_expr c true all_occurrences ] - | [ "<-" constr(c) ] -> [ apply_constr_expr c false all_occurrences ] + [ constr(c) ] -> [ apply_constr_expr c true AllOccurrences ] + | [ "<-" constr(c) ] -> [ apply_constr_expr c false AllOccurrences ] | [ "subterms" rewstrategy(h) ] -> [ all_subterms h ] | [ "subterm" rewstrategy(h) ] -> [ one_subterm h ] | [ "innermost" rewstrategy(h) ] -> [ Strategies.innermost h ] @@ -1425,7 +1429,7 @@ let clsubstitute o c = (fun cl -> match cl with | Some id when is_tac id -> tclIDTAC - | _ -> cl_rewrite_clause c o all_occurrences cl) + | _ -> cl_rewrite_clause c o AllOccurrences cl) open Extraargs @@ -1438,9 +1442,9 @@ END TACTIC EXTEND setoid_rewrite [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] - -> [ cl_rewrite_clause c o all_occurrences None ] + -> [ cl_rewrite_clause c o AllOccurrences None ] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ cl_rewrite_clause c o all_occurrences (Some id)] + [ cl_rewrite_clause c o AllOccurrences (Some id)] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None] | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> @@ -1459,11 +1463,11 @@ TACTIC EXTEND GenRew | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ] | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ cl_rewrite_clause_newtac_tac c o all_occurrences (Some id) ] + [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ] | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ] | [ "rew" orient(o) glob_constr_with_bindings(c) ] -> - [ cl_rewrite_clause_newtac_tac c o all_occurrences None ] + [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ] END let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l) @@ -1899,7 +1903,7 @@ let setoid_transitivity c gl = let proof = get_transitive_proof env evm car rel in match c with | None -> eapply proof - | Some c -> apply_with_bindings (proof,Glob_term.ImplicitBindings [ c ])) + | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])) (transitivity_red true c) let setoid_symmetry_in id gl = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1dc0f6589..0d277855f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -48,6 +48,8 @@ open Extrawit open Pcoq open Compat open Evd +open Misctypes +open Locus let safe_msgnl s = try msgnl s with e -> @@ -164,7 +166,7 @@ let add_primitive_tactic s tac = atomic_mactab := Idmap.add id tac !atomic_mactab let _ = - let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in + let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in List.iter (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t))) [ "red", TacReduce(Red false,nocl); @@ -588,8 +590,9 @@ let intern_inversion_strength lf ist = function InversionUsing (intern_constr ist c, intern_hyp_list ist idl) (* Interprets an hypothesis name *) -let intern_hyp_location ist (((b,occs),id),hl) = - (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl) +let intern_hyp_location ist ((occs,id),hl) = + ((Locusops.occurrences_map (List.map (intern_or_var ist)) occs, + intern_hyp_or_metaid ist id), hl) (* Reads a pattern *) let intern_pattern ist ?(as_type=false) lfun = function @@ -764,8 +767,8 @@ let rec intern_atomic lf ist x = | TacChange (None,c,cl) -> TacChange (None, (if (cl.onhyps = None or cl.onhyps = Some []) & - (cl.concl_occs = all_occurrences_expr or - cl.concl_occs = no_occurrences_expr) + (cl.concl_occs = AllOccurrences or + cl.concl_occs = NoOccurrences) then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) | TacChange (Some p,c,cl) -> @@ -1179,8 +1182,8 @@ let interp_evaluable ist env = function interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid (* Interprets an hypothesis name *) -let interp_occurrences ist (b,occs) = - (b,interp_int_or_var_list ist occs) +let interp_occurrences ist occs = + Locusops.occurrences_map (interp_int_or_var_list ist) occs let interp_hyp_location ist gl ((occs,id),hl) = ((interp_occurrences ist occs,interp_hyp ist gl id),hl) @@ -1347,8 +1350,8 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma occl = let interp_constr_with_occurrences_and_name_as_list = interp_constr_in_compound_list - (fun c -> ((all_occurrences_expr,c),Anonymous)) - (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c + (fun c -> ((AllOccurrences,c),Anonymous)) + (function ((occs,c),Anonymous) when occs = AllOccurrences -> c | _ -> raise Not_found) (fun ist env sigma (occ_c,na) -> let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in @@ -2390,7 +2393,7 @@ and interp_atomic ist gl tac = (h_generalize_dep c_interp) | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - if clp = nowhere then + if clp = Locusops.nowhere then (* We try to fully-typechect the term *) let (sigma,c_interp) = pf_interp_constr ist gl c in tclTHEN @@ -2491,8 +2494,8 @@ and interp_atomic ist gl tac = | TacChange (None,c,cl) -> let (sigma,c_interp) = if (cl.onhyps = None or cl.onhyps = Some []) & - (cl.concl_occs = all_occurrences_expr or - cl.concl_occs = no_occurrences_expr) + (cl.concl_occs = AllOccurrences or + cl.concl_occs = NoOccurrences) then pf_interp_type ist gl c else pf_interp_constr ist gl c in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 991fbc88c..861dcb97c 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -19,6 +19,7 @@ open Genarg open Topconstr open Mod_subst open Redexpr +open Misctypes (** Values for interpretation *) type value = @@ -101,8 +102,8 @@ val intern_constr : glob_sign -> constr_expr -> glob_constr_and_expr val intern_constr_with_bindings : - glob_sign -> constr_expr * constr_expr Glob_term.bindings -> - glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings + glob_sign -> constr_expr * constr_expr bindings -> + glob_constr_and_expr * glob_constr_and_expr bindings val intern_hyp : glob_sign -> identifier Pp.located -> identifier Pp.located @@ -114,7 +115,7 @@ val subst_glob_constr_and_expr : substitution -> glob_constr_and_expr -> glob_constr_and_expr val subst_glob_with_bindings : - substitution -> glob_constr_and_expr Glob_term.with_bindings -> glob_constr_and_expr Glob_term.with_bindings + substitution -> glob_constr_and_expr with_bindings -> glob_constr_and_expr with_bindings (** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value @@ -132,10 +133,11 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr bindings -> Evd.evar_map * constr bindings -val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr Glob_term.with_bindings -> Evd.evar_map * constr Glob_term.with_bindings +val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr with_bindings -> Evd.evar_map * constr with_bindings (** Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f7b8419c9..c95486df6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -27,6 +27,8 @@ open Pattern open Matching open Genarg open Tacexpr +open Locus +open Misctypes (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -131,43 +133,6 @@ let afterHyp id gl = --Eduardo (8/8/97) *) -(* A [simple_clause] is a set of hypotheses, possibly extended with - the conclusion (conclusion is represented by None) *) - -type simple_clause = identifier option list - -(* An [clause] is the algebraic form of a - [concrete_clause]; it may refer to all hypotheses - independently of the effective contents of the current goal *) - -type clause = identifier gclause - -let allHypsAndConcl = { onhyps=None; concl_occs=all_occurrences_expr } -let allHyps = { onhyps=None; concl_occs=no_occurrences_expr } -let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr } -let onHyp id = - { onhyps=Some[((all_occurrences_expr,id),InHyp)]; - concl_occs=no_occurrences_expr } - -let simple_clause_of cl gls = - let error_occurrences () = - error "This tactic does not support occurrences selection" in - let error_body_selection () = - error "This tactic does not support body selection" in - let hyps = - match cl.onhyps with - | None -> - List.map Option.make (pf_ids_of_hyps gls) - | Some l -> - List.map (fun ((occs,id),w) -> - if occs <> all_occurrences_expr then error_occurrences (); - if w = InHypValueOnly then error_body_selection (); - Some id) l in - if cl.concl_occs = no_occurrences_expr then hyps - else - if cl.concl_occs <> all_occurrences_expr then error_occurrences () - else None :: hyps - let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl @@ -176,8 +141,12 @@ let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl -let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls -let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls +let onClause tac cl gls = + let hyps () = pf_ids_of_hyps gls in + tclMAP tac (Locusops.simple_clause_of hyps cl) gls +let onClauseLR tac cl gls = + let hyps () = pf_ids_of_hyps gls in + tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls let ifOnHyp pred tac1 tac2 id gl = if pred (id,pf_get_hyp_typ gl id) then @@ -185,52 +154,6 @@ let ifOnHyp pred tac1 tac2 id gl = else tac2 id gl - -(************************************************************************) -(* An intermediate form of occurrence clause that select components *) -(* of a definition, hypotheses and possibly the goal *) -(* (used for reduction tactics) *) -(************************************************************************) - -(* A [hyp_location] is an hypothesis together with a position, in - body if any, in type or in both *) - -type hyp_location = identifier * hyp_location_flag - -(* A [goal_location] is either an hypothesis (together with a position, in - body if any, in type or in both) or the goal *) - -type goal_location = hyp_location option - -(************************************************************************) -(* An intermediate structure for dealing with occurrence clauses *) -(************************************************************************) - -(* [clause_atom] refers either to an hypothesis location (i.e. an - hypothesis with occurrences and a position, in body if any, in type - or in both) or to some occurrences of the conclusion *) - -type clause_atom = - | OnHyp of identifier * occurrences_expr * hyp_location_flag - | OnConcl of occurrences_expr - -(* A [concrete_clause] is an effective collection of - occurrences in the hypotheses and the conclusion *) - -type concrete_clause = clause_atom list - -let concrete_clause_of cl gls = - let hyps = - match cl.onhyps with - | None -> - let f id = OnHyp (id,all_occurrences_expr,InHyp) in - List.map f (pf_ids_of_hyps gls) - | Some l -> - List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in - if cl.concl_occs = no_occurrences_expr then hyps - else - OnConcl cl.concl_occs :: hyps - (************************************************************************) (* Elimination Tacticals *) (************************************************************************) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 7c13894ec..d4cbc6e5b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -21,6 +21,8 @@ open Genarg open Tacexpr open Termops open Glob_term +open Locus +open Misctypes (** Tacticals i.e. functions from tactics to tactics. *) @@ -94,24 +96,10 @@ val onHyps : (goal sigma -> named_context) -> (** {6 Tacticals applying to goal components } *) -(** A [simple_clause] is a set of hypotheses, possibly extended with - the conclusion (conclusion is represented by None) *) - -type simple_clause = identifier option list - (** A [clause] denotes occurrences and hypotheses in a goal; in particular, it can abstractly refer to the set of hypotheses independently of the effective contents of the current goal *) -type clause = identifier gclause - -val simple_clause_of : clause -> goal sigma -> simple_clause - -val allHypsAndConcl : clause -val allHyps : clause -val onHyp : identifier -> clause -val onConcl : clause - val tryAllHyps : (identifier -> tactic) -> tactic val tryAllHypsAndConcl : (identifier option -> tactic) -> tactic @@ -121,36 +109,6 @@ val onAllHypsAndConcl : (identifier option -> tactic) -> tactic val onClause : (identifier option -> tactic) -> clause -> tactic val onClauseLR : (identifier option -> tactic) -> clause -> tactic -(** {6 An intermediate form of occurrence clause with no mention of occurrences } *) - -(** A [hyp_location] is an hypothesis together with a position, in - body if any, in type or in both *) - -type hyp_location = identifier * hyp_location_flag - -(** A [goal_location] is either an hypothesis (together with a position, in - body if any, in type or in both) or the goal *) - -type goal_location = hyp_location option - -(** {6 A concrete view of occurrence clauses } *) - -(** [clause_atom] refers either to an hypothesis location (i.e. an - hypothesis with occurrences and a position, in body if any, in type - or in both) or to some occurrences of the conclusion *) - -type clause_atom = - | OnHyp of identifier * occurrences_expr * hyp_location_flag - | OnConcl of occurrences_expr - -(** A [concrete_clause] is an effective collection of - occurrences in the hypotheses and the conclusion *) - -type concrete_clause = clause_atom list - -(** This interprets an [clause] in a given [goal] context *) -val concrete_clause_of : clause -> goal sigma -> concrete_clause - (** {6 Elimination tacticals. } *) type branch_args = { diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4ac2a5bc..7e350bfe9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -44,6 +44,9 @@ open Evarutil open Indrec open Pretype_errors open Unification +open Locus +open Locusops +open Misctypes exception Bound @@ -56,7 +59,7 @@ let rec nb_prod x = | _ -> n in count 0 x -let inj_with_occurrences e = (all_occurrences_expr,e) +let inj_with_occurrences e = (AllOccurrences,e) let dloc = dummy_loc @@ -228,11 +231,11 @@ let bind_change_occurrences occs = function let bind_red_expr_occurrences occs nbcl redexp = let has_at_clause = function - | Unfold l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l - | Pattern l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l - | Simpl (Some (occl,_)) -> occl <> all_occurrences_expr + | Unfold l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l + | Pattern l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l + | Simpl (Some (occl,_)) -> occl <> AllOccurrences | _ -> false in - if occs = all_occurrences_expr then + if occs = AllOccurrences then if nbcl > 1 && has_at_clause redexp then error_illegal_non_atomic_clause () else @@ -242,24 +245,24 @@ let bind_red_expr_occurrences occs nbcl redexp = | Unfold (_::_::_) -> error_illegal_clause () | Unfold [(occl,c)] -> - if occl <> all_occurrences_expr then + if occl <> AllOccurrences then error_illegal_clause () else Unfold [(occs,c)] | Pattern (_::_::_) -> error_illegal_clause () | Pattern [(occl,c)] -> - if occl <> all_occurrences_expr then + if occl <> AllOccurrences then error_illegal_clause () else Pattern [(occs,c)] | Simpl (Some (occl,c)) -> - if occl <> all_occurrences_expr then + if occl <> AllOccurrences then error_illegal_clause () else Simpl (Some (occs,c)) | CbvVm (Some (occl,c)) -> - if occl <> all_occurrences_expr then + if occl <> AllOccurrences then error_illegal_clause () else CbvVm (Some (occs,c)) @@ -312,7 +315,7 @@ let change_option occl t = function | None -> change_in_concl occl t let change chg c cls gl = - let cls = concrete_clause_of cls gl in + let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in tclMAP (function | OnHyp (id,occs,where) -> change_option (bind_change_occurrences occs chg) c (Some (id,where)) @@ -351,7 +354,7 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl goal = - let cl = concrete_clause_of cl goal in + let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in let tac = tclMAP (fun (where,redexp) -> reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in @@ -362,8 +365,8 @@ let reduce redexp cl goal = (* Unfolding occurrences of a constant *) let unfold_constr = function - | ConstRef sp -> unfold_in_concl [all_occurrences,EvalConstRef sp] - | VarRef id -> unfold_in_concl [all_occurrences,EvalVarRef id] + | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] + | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.") (*******************************************) @@ -1548,7 +1551,7 @@ let generalize_dep ?(with_let=false) c gl = | _ -> None else None in - let cl'' = generalize_goal gl 0 ((all_occurrences,c,body),Anonymous) cl' in + let cl'' = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) cl' in let args = Array.to_list (instance_from_named_context to_quantify_rev) in tclTHEN (apply_type cl'' (if body = None then c::args else args)) @@ -1566,7 +1569,7 @@ let generalize_gen lconstr = (occs,c,None),na) lconstr) let generalize l = - generalize_gen_let (List.map (fun c -> ((all_occurrences,c,None),Anonymous)) l) + generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) let pf_get_hyp_val gl id = let (_, b, _) = pf_get_hyp gl id in @@ -1574,7 +1577,7 @@ let pf_get_hyp_val gl id = let revert hyps gl = let lconstr = List.map (fun id -> - ((all_occurrences, mkVar id, pf_get_hyp_val gl id), Anonymous)) + ((AllOccurrences, mkVar id, pf_get_hyp_val gl id), Anonymous)) hyps in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl @@ -1621,15 +1624,16 @@ let out_arg = function let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> None - | (((b,occs),id'),hl)::_ when id=id' -> Some ((b,List.map out_arg occs),hl) + | ((occs,id'),hl)::_ when id=id' -> + Some (occurrences_map (List.map out_arg) occs, hl) | _::l -> hyp_occ l in match cls.onhyps with - None -> Some (all_occurrences,InHyp) + None -> Some (AllOccurrences,InHyp) | Some l -> hyp_occ l let occurrences_of_goal cls = - if cls.concl_occs = no_occurrences_expr then None - else Some (on_snd (List.map out_arg) cls.concl_occs) + if cls.concl_occs = NoOccurrences then None + else Some (occurrences_map (List.map out_arg) cls.concl_occs) let in_every_hyp cls = (cls.onhyps=None) @@ -1732,7 +1736,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl = | None -> depdecls | Some occ -> let newdecl = subst_closed_term_occ_decl_modulo occ test d in - if occ = (all_occurrences,InHyp) & eq_named_declaration d newdecl then + if occ = (AllOccurrences,InHyp) & eq_named_declaration d newdecl then if check_occs & not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls @@ -3056,9 +3060,9 @@ let induction_without_atomization isrec with_evars elim names lid gl = let has_selected_occurrences = function | None -> false | Some cls -> - cls.concl_occs <> all_occurrences_expr || + cls.concl_occs <> AllOccurrences || cls.onhyps <> None && List.exists (fun ((occs,_),hl) -> - occs <> all_occurrences_expr || hl <> InHyp) (Option.get cls.onhyps) + occs <> AllOccurrences || hl <> InHyp) (Option.get cls.onhyps) (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls gl = @@ -3066,7 +3070,7 @@ let clear_unselected_context id inhyps cls gl = | None -> tclIDTAC gl | Some cls -> if occur_var (pf_env gl) id (pf_concl gl) && - cls.concl_occs = no_occurrences_expr + cls.concl_occs = NoOccurrences then errorlabstrm "" (str "Conclusion must be mentioned: it depends on " ++ pr_id id ++ str "."); diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6e3c2cff4..40bcb94c9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -28,6 +28,8 @@ open Glob_term open Pattern open Termops open Unification +open Misctypes +open Locus (** Main tactics. *) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 0357fc8a3..863365800 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -29,6 +29,7 @@ open Inductiveops open Tactics open Tacticals open Ind_tables +open Misctypes (**********************************************************************) (* Generic synthesis of boolean equality *) @@ -80,21 +81,21 @@ let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = new_induct false - [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None let destruct_on_using c id = new_destruct false - [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None - (None,Some (dl,Genarg.IntroOrAndPattern [ - [dl,Genarg.IntroAnonymous]; - [dl,Genarg.IntroIdentifier id]])) + (None,Some (dl,IntroOrAndPattern [ + [dl,IntroAnonymous]; + [dl,IntroIdentifier id]])) None let destruct_on c = new_destruct false - [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))] + [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None (* reconstruct the inductive with the correct deBruijn indexes *) @@ -537,7 +538,7 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig = tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - simpl_in_hyp (freshz,InHyp); + simpl_in_hyp (freshz,Locus.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) @@ -549,11 +550,11 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). in avoid := fresht::(!avoid); (new_destruct false [Tacexpr.ElimOnConstr - (Evd.empty,((mkVar freshz,Glob_term.NoBindings)))] + (Evd.empty,((mkVar freshz,NoBindings)))] None - (None, Some (dl,Genarg.IntroOrAndPattern [[ - dl,Genarg.IntroIdentifier fresht; - dl,Genarg.IntroIdentifier freshz]])) None) gl + (None, Some (dl,IntroOrAndPattern [[ + dl,IntroIdentifier fresht; + dl,IntroIdentifier freshz]])) None) gl ]); (* Ci a1 ... an = Ci b1 ... bn @@ -667,7 +668,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] false (mkVar freshz,Glob_term.NoBindings); + Equality.inj [] false (mkVar freshz,NoBindings); intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( @@ -837,10 +838,10 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = Auto.default_auto ]); Equality.general_rewrite_bindings_in true - all_occurrences true false + Locus.AllOccurrences true false (List.hd !avoid) ((mkVar (List.hd (List.tl !avoid))), - Glob_term.NoBindings + NoBindings ) true; Equality.discr_tac false None diff --git a/toplevel/command.ml b/toplevel/command.ml index 9e21a3a76..ecc4e6995 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -31,6 +31,7 @@ open Evarutil open Evarconv open Notation open Indschemes +open Misctypes let rec under_binders env f n c = if n = 0 then f env Evd.empty c else @@ -351,7 +352,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.GType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc,GType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 21e39e0ca..5a4dbabb6 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -15,6 +15,7 @@ open Glob_term open Genarg open Vernacexpr open Ind_tables +open Misctypes (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fc51e1348..6ac321e43 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -34,6 +34,7 @@ open Redexpr open Syntax_def open Lemmas open Declaremods +open Misctypes (* Pcoq hooks *) @@ -42,7 +43,7 @@ type pcoq_hook = { solve : int -> unit; abort : string -> unit; search : searchable -> dir_path list * bool -> unit; - print_name : reference Genarg.or_by_notation -> unit; + print_name : reference or_by_notation -> unit; print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; @@ -1319,8 +1320,8 @@ let vernac_search s r = Search.search_about (List.map (on_snd interp_search_about_item) sl) r let vernac_locate = function - | LocateTerm (Genarg.AN qid) -> msgnl (print_located_qualid qid) - | LocateTerm (Genarg.ByNotation (_,ntn,sc)) -> + | LocateTerm (AN qid) -> msgnl (print_located_qualid qid) + | LocateTerm (ByNotation (_,ntn,sc)) -> ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lglob_constr) ntn sc) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index a9d384ea0..704f06fb5 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -11,6 +11,7 @@ open Term open Vernacinterp open Vernacexpr open Topconstr +open Misctypes (** Vernacular entries *) @@ -28,7 +29,7 @@ type pcoq_hook = { solve : int -> unit; abort : string -> unit; search : searchable -> dir_path list * bool -> unit; - print_name : Libnames.reference Genarg.or_by_notation -> unit; + print_name : Libnames.reference or_by_notation -> unit; print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 1882e0af2..5ccf8db88 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -26,6 +26,7 @@ open Pfedit open Refiner open Tacmach open Syntax_def +open Misctypes (* Coq interface to the Whelp query engine developed at the University of Bologna *) @@ -94,8 +95,8 @@ let url_paren f l = url_char '('; f l; url_char ')' let url_bracket f l = url_char '['; f l; url_char ']' let whelp_of_glob_sort = function - | GProp Null -> "Prop" - | GProp Pos -> "Set" + | GProp -> "Prop" + | GSet -> "Set" | GType _ -> "Type" let uri_int n = Buffer.add_string b (string_of_int n) @@ -163,7 +164,7 @@ let rec uri_of_constr c = | GLetIn (_,na,b,c) -> url_string "let "; url_of_name na; url_string "\\def "; uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, CastConv (_,t)) -> + | GCast (_,c, (CastConv t|CastVM t)) -> uri_of_constr c; url_string ":"; uri_of_constr t | GRec _ | GIf _ | GLetTuple _ | GCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint." |