diff options
Diffstat (limited to 'plugins')
86 files changed, 1134 insertions, 889 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 6281b2675e..a09abfa193 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -12,12 +12,12 @@ let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) -let decomp_term sigma (c : Term.constr) = - Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) +let decomp_term sigma (c : Constr.t) = + Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) -let lapp c v = Term.mkApp (Lazy.force c, v) +let lapp c v = Constr.mkApp (Lazy.force c, v) -let (===) = Term.eq_constr +let (===) = Constr.equal module CoqList = struct let path = ["Init"; "Datatypes"] @@ -53,17 +53,11 @@ end module Env = struct - module ConstrHashed = struct - type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr - end - - module ConstrHashtbl = Hashtbl.Make (ConstrHashed) + module ConstrHashtbl = Hashtbl.Make (Constr) type t = (int ConstrHashtbl.t * int ref) - let add (tbl, off) (t : Term.constr) = + let add (tbl, off) (t : Constr.t) = try ConstrHashtbl.find tbl t with | Not_found -> @@ -103,7 +97,7 @@ module Bool = struct | Negb of t | Ifb of t * t * t - let quote (env : Env.t) sigma (c : Term.constr) : t = + let quote (env : Env.t) sigma (c : Constr.t) : t = let trueb = Lazy.force trueb in let falseb = Lazy.force falseb in let andb = Lazy.force andb in @@ -170,7 +164,7 @@ module Btauto = struct | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|] | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|] - let convert_env env : Term.constr = + let convert_env env : Constr.t = CoqList.of_list (Lazy.force Bool.typ) env let reify env t = lapp eval [|convert_env env; convert t|] @@ -206,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in @@ -249,7 +244,7 @@ module Btauto = struct let env = Env.to_list env in let fl = reify env fl in let fr = reify env fr in - let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in + let changed_gl = Constr.mkApp (c, [|typ; fl; fr|]) in let changed_gl = EConstr.of_constr changed_gl in Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 1828213227..ccef9ab960 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -11,14 +11,15 @@ (* Plus some e-matching and constructor handling by P. Corbineau *) open CErrors -open Util open Pp -open Goptions open Names -open Term +open Sorts +open Constr open Vars -open Tacmach open Evd +open Goptions +open Tacmach +open Util let init_size=5 @@ -154,7 +155,7 @@ let rec term_equal t1 t2 = open Hashset.Combine let rec hash_term = function - | Symb c -> combine 1 (hash_constr c) + | Symb c -> combine 1 (Constr.hash c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) @@ -215,7 +216,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -232,7 +233,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr let equal = eq_constr_nounivs - let hash = hash_constr + let hash = Constr.hash end) module Typehash = Constrhash @@ -436,9 +437,9 @@ and make_app l=function and applist_proj c l = match c with | Symb s -> applist_projection s l - | _ -> applistc (constr_of_term c) l + | _ -> Term.applistc (constr_of_term c) l and applist_projection c l = - match kind_of_term c with + match Constr.kind c with | Const c when Environ.is_projection (fst c) (Global.env()) -> let p = Projection.make (fst c) false in (match l with @@ -446,15 +447,15 @@ and applist_projection c l = let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx + Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx | hd :: tl -> - applistc (mkProj (p, hd)) tl) - | _ -> applistc c l + Term.applistc (mkProj (p, hd)) tl) + | _ -> Term.applistc c l let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in let func c = canonize_name sigma (EConstr.of_constr c) in - match kind_of_term c with + match Constr.kind c with | Const (kn,u) -> let canon_const = Constant.make1 (Constant.canonical kn) in (mkConstU (canon_const,u)) @@ -837,7 +838,7 @@ let complete_one_class state i= let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in - let typ = prod_applist _c (List.rev _args) in + let typ = Term.prod_applist _c (List.rev _args) in let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index f904aa3e68..23cd2161d7 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Term +open Constr open Names type pa_constructor = @@ -85,7 +85,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index a43a167e86..97efaced8f 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,7 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open CErrors -open Term +open Constr open Ccalgo open Pp diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 9f53123db1..a3e4501342 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,7 @@ (************************************************************************) open Ccalgo -open Term +open Constr type rule= Ax of constr diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 150319f6b9..8642df6846 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -12,7 +12,7 @@ open Evd open Names open Inductiveops open Declarations -open Term +open Constr open EConstr open Vars open Tactics @@ -76,11 +76,11 @@ let rec decompose_term env sigma t= let (mind,i_ind),u = c in let u = EInstance.kind sigma u in let canon_mind = MutInd.make1 (MutInd.canonical mind) in - let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u))) + let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> let u = EInstance.kind sigma u in let canon_const = Constant.make1 (Constant.canonical c) in - (Symb (Term.mkConstU (canon_const,u))) + (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> let canon_const kn = Constant.make1 (Constant.canonical kn) in let p' = Projection.map canon_const p in @@ -198,7 +198,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=Term.mkVar id in + let cid=Constr.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 6d3d4b7432..fb65a8639a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Constr open Context.Named.Declaration -let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) +let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx @@ -67,7 +68,7 @@ let start_deriving f suchthat lemma = let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in - let f_kn_term = Term.mkConst f_kn in + let f_kn_term = mkConst f_kn in (** In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by references to the constant [f] declared above. This substitution diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3c46d5c43b..bc84df76b7 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -7,7 +7,7 @@ (************************************************************************) open Miniml -open Term +open Constr open Declarations open Names open ModPath @@ -138,7 +138,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Mod_subst.force_constr lbody) with + (match Constr.kind (Mod_subst.force_constr lbody) with | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) @@ -146,8 +146,8 @@ let check_fix env cb i = let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal eq_constr ca1 ca2 && - Array.equal eq_constr ta1 ta2 + Array.equal Constr.equal ca1 ca2 && + Array.equal Constr.equal ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7bbb825b10..dd86177381 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,4 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a227478d0f..4ae875cd70 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -10,6 +10,7 @@ open Util open Names open Term +open Constr open Vars open Declarations open Declareops @@ -81,7 +82,7 @@ let whd_betaiotazeta t = let rec flag_of_type env t : flag = let t = whd_all env t in - match kind_of_term t with + match Constr.kind t with | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) @@ -111,14 +112,14 @@ let push_rel_assum (n, t) env = (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -145,7 +146,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kprop::s, vl @@ -153,7 +154,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -207,7 +208,7 @@ let parse_ind_args si args relmax = | [] -> Int.Map.empty | Kill _ :: s -> parse (i+1) j s | Keep :: s -> - (match kind_of_term args.(i-1) with + (match Constr.kind args.(i-1) with | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s) | _ -> parse (i+1) (j+1) s) in parse 1 1 si @@ -224,7 +225,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta c) with + match Constr.kind (whd_betaiotazeta c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -299,9 +300,9 @@ let rec extract_type env db j c args = | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown - else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args + else extract_type env db j (mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | _ -> assert false + | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -331,7 +332,7 @@ and extract_type_scheme env db c p = if Int.equal p 0 then extract_type env db 0 c [] else let c = whd_betaiotazeta c in - match kind_of_term c with + match Constr.kind c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> @@ -415,8 +416,8 @@ and extract_really_ind env kn mib = let t = snd (decompose_prod_n npar types.(j)) in let prods,head = dest_prod epar t in let nprods = List.length prods in - let args = match kind_of_term head with - | App (f,args) -> args (* [kind_of_term f = Ind ip] *) + let args = match Constr.kind head with + | App (f,args) -> args (* [Constr.kind f = Ind ip] *) | _ -> [||] in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in @@ -444,7 +445,7 @@ and extract_really_ind env kn mib = if Option.is_empty mib.mind_record then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) - let rec names_prod t = match kind_of_term t with + let rec names_prod t = match Constr.kind t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t | Cast(t,_,_) -> names_prod t @@ -503,7 +504,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in @@ -564,7 +565,7 @@ let record_constant_type env kn opt_typ = (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) let rec extract_term env mle mlt c args = - match kind_of_term c with + match Constr.kind c with | App (f,a) -> extract_term env mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> @@ -874,7 +875,7 @@ let decomp_lams_eta_n n m env c t = (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match kind_of_term c with +let rec gentypvar_ok c = match Constr.kind c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index e1d43f3405..b15b88ed2c 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -9,7 +9,7 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Term +open Constr open Declarations open Environ open Miniml diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f708307c38..28abb7f575 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -58,7 +58,6 @@ let preamble mod_name comment used_modules usf = else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ str "import qualified GHC.Base" ++ fnl () ++ - str "import qualified GHC.Prim" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "import qualified IOExts" ++ fnl () ++ @@ -78,7 +77,7 @@ let preamble mod_name comment used_modules usf = (if not usf.tunknown then mt () else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ - str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "type Any = GHC.Base.Any" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "type Any = ()" ++ fnl () ++ diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 9cbc3fd713..5d0f9c167e 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r) let pp_modname mp = str (Common.pp_module mp) +(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *) + +let infix_symbols = + ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ] +let operator_chars = + [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ] + +(* infix ops in OCaml, but disallowed by preceding grammar *) + +let builtin_infixes = + [ "::" ; "," ] + +let substring_all_opchars s start stop = + let rec check_char i = + if i >= stop then true + else + List.mem s.[i] operator_chars && check_char (i+1) + in + check_char start + let is_infix r = is_inline_custom r && (let s = find_custom r in - let l = String.length s in - l >= 2 && s.[0] == '(' && s.[l-1] == ')') + let len = String.length s in + len >= 3 && + (* parenthesized *) + (s.[0] == '(' && s.[len-1] == ')' && + let inparens = String.trim (String.sub s 1 (len - 2)) in + let inparens_len = String.length inparens in + (* either, begins with infix symbol, any remainder is all operator chars *) + (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) || + (* or, starts with #, at least one more char, all are operator chars *) + (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) || + (* or, is an OCaml built-in infix *) + (List.mem inparens builtin_infixes))) let get_infix r = let s = find_custom r in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 995d5fd19d..5903733a66 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str "Please load library " ++ pr_dirpath dp ++ str " first.") + err (str "Please load library " ++ DirPath.print dp ++ str " first.") | _ -> () end | _ -> () diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index cc93f294b3..e52e419fd3 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -180,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) -val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t +val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t val is_custom : global_reference -> bool val is_inline_custom : global_reference -> bool diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index db1a46a035..c55040df03 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -8,7 +8,7 @@ open Hipattern open Names -open Term +open Constr open EConstr open Vars open Termops @@ -39,7 +39,7 @@ exception Is_atom of constr let meta_succ m = m+1 let rec nb_prod_after n c= - match kind_of_term c with + match Constr.kind c with | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 1+(nb_prod_after 0 b) | _ -> 0 diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 106c469c62..3b6b711c0a 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Globnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 1e7da3250b..938bec25b9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -65,11 +65,14 @@ let default_intuition_tac = let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" -VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ - set_default_solver - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> let open Vernacinterp in + set_default_solver + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + ] END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index f660ba7343..d462013353 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -11,7 +11,7 @@ open Formula open Sequent open Rules open Instances -open Term +open Constr open Tacmach.New open Tacticals.New diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c2606dbe8e..3409471a7a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -24,7 +24,7 @@ open Misctypes open Context.Rel.Declaration let compare_instance inst1 inst2= - let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in + let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in match inst1,inst2 with Phantom(d1),Phantom(d2)-> (cmp d1 d2) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index d6309b057f..1a6eba8c62 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global @@ Coqlib.coq_reference "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] + [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index d8d4c1a38a..5c46f4cec2 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open EConstr open Names +open Constr +open EConstr open Globnames type tactic = unit Proofview.tactic diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 05194164b0..ea2d076ed9 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -54,13 +54,7 @@ struct (priority e1.pat) - (priority e2.pat) end -module OrderedConstr= -struct - type t=Term.constr - let compare=Term.compare -end - -type h_item = global_reference * (int*Term.constr) option +type h_item = global_reference * (int*Constr.t) option module Hitem= struct @@ -70,13 +64,13 @@ struct if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in - if c = 0 then OrderedConstr.compare c1 c2 else c + if c = 0 then Constr.compare c1 c2 else c in Option.compare cmp co1 co2 else c end -module CM=Map.Make(OrderedConstr) +module CM=Map.Make(Constr) module History=Set.Make(Hitem) diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index ca6079c8b0..7f4a6dd86a 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -10,11 +10,9 @@ open EConstr open Formula open Globnames -module OrderedConstr: Set.OrderedType with type t=Term.constr +module CM: CSig.MapS with type key=Constr.t -module CM: CSig.MapS with type key=Term.constr - -type h_item = global_reference * (int*Term.constr) option +type h_item = global_reference * (int*Constr.t) option module History: Set.S with type elt = h_item diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index d3e8aeee88..390aa8c85c 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr exception UFAIL of constr*constr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 68af1b3b63..d9e9375c0c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -12,7 +12,7 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -open Term +open Constr open Tactics open Names open Globnames @@ -27,11 +27,7 @@ qui donne le coefficient d'un terme du calcul des constructions, qui est zéro si le terme n'y est pas. *) -module Constrhash = Hashtbl.Make - (struct type t = constr - let equal = eq_constr - let hash = hash_constr - end) +module Constrhash = Hashtbl.Make(Constr) type flin = {fhom: rational Constrhash.t; fcste:rational};; @@ -84,7 +80,7 @@ let string_of_R_constant kn = | _ -> "constant_not_of_R" let rec string_of_R_constr c = - match kind_of_term c with + match Constr.kind c with Cast (c,_,_) -> string_of_R_constr c |Const (c,_) -> string_of_R_constant c | _ -> "not_of_constant" @@ -92,7 +88,7 @@ let rec string_of_R_constr c = exception NoRational let rec rational_of_constr c = - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (rational_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -125,7 +121,7 @@ exception NoLinear let rec flin_of_constr c = try( - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (flin_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -192,9 +188,9 @@ exception NoIneq let ineq1_of_constr (h,t) = let h = EConstr.Unsafe.to_constr h in let t = EConstr.Unsafe.to_constr t in - match (kind_of_term t) with + match (Constr.kind t) with | App (f,args) -> - (match kind_of_term f with + (match Constr.kind f with | Const (c,_) when Array.length args = 2 -> let t1= args.(0) in let t2= args.(1) in @@ -233,7 +229,7 @@ let ineq1_of_constr (h,t) = let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in - (match (kind_of_term t0) with + (match (Constr.kind t0) with | Const (c,_) -> (match (string_of_R_constant c) with | "R"-> @@ -438,7 +434,7 @@ let tac_use h = (* let is_ineq (h,t) = - match (kind_of_term t) with + match (Constr.kind t) with App (f,args) -> (match (string_of_R_constr f) with "Rlt" -> true @@ -479,7 +475,7 @@ let rec fourier () = (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) try - match (kind_of_term goal) with + match (Constr.kind goal) with App (f,args) -> let get = eget in (match (string_of_R_constr f) with diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fb1d923..62ca706264 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,7 +1,7 @@ open Printer open CErrors open Util -open Term +open Constr open EConstr open Vars open Namegen @@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) +let pr_leconstr_fp = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let debug_queue = Stack.create () let rec print_debug_queue e = @@ -172,7 +176,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -220,7 +224,8 @@ let find_rectype env sigma c = let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in - observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l))); + observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ + Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false @@ -233,7 +238,8 @@ exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); + observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++ + match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange; end in @@ -841,7 +847,7 @@ let build_proof | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam princ_params ); observe (str "fbody_with_full_params := " ++ - pr_leconstr fbody_with_full_params + pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 018b515170..7a9bbd92cf 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,9 @@ open Printer open CErrors -open Util open Term +open Sorts +open Util +open Constr open Vars open Namegen open Names @@ -80,7 +82,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> - match kind_of_term t with + match Constr.kind t with | Var id -> Id.Set.mem id set | _ -> false in @@ -100,13 +102,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = EConstr.Unsafe.to_constr pre_princ in let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = - match kind_of_term c with + match Constr.kind c with | Ind((u,_),_) -> MutInd.equal u rel_as_kn | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn | _ -> false in let get_fun_num c = - match kind_of_term c with + match Constr.kind c with | Ind((_,num),_) -> num | Construct(((_,num),_),_) -> num | _ -> assert false @@ -114,12 +116,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = - match kind_of_term pre_princ with + match Constr.kind pre_princ with | Rel n -> begin try match Environ.lookup_rel n env with @@ -149,12 +153,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in applistc new_f new_args, - list_union_eq eq_constr binders_to_remove_from_f binders_to_remove + list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in -(* let _ = match kind_of_term pre_princ with *) +(* let _ = match Constr.kind pre_princ with *) (* | Prod _ -> *) (* observe(str "compute_new_princ_type for "++ *) (* pr_lconstr_env env pre_princ ++ *) @@ -170,13 +174,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq - eq_constr + Constr.equal binders_to_remove_from_t (List.map pop binders_to_remove_from_b) ) @@ -189,7 +193,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin @@ -199,14 +203,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : Name.t = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq - eq_constr - (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) + Constr.equal + (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) (List.map pop binders_to_remove_from_b) ) @@ -218,12 +222,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e in - new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc + new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc in (* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) let pre_res,_ = @@ -329,7 +333,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) | Some (id) -> id,id | None -> let id_of_f = Label.to_id (Constant.label (fst f)) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort) in let names = ref [new_princ_name] in let hook = @@ -344,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in + let univs = + let poly = Flags.is_universe_polymorphism () in + Evd.const_univ_entry ~poly evd' + in + let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant name @@ -389,7 +396,7 @@ exception Not_Rec let get_funs_constant mp dp = let get_funs_constant const e : (Names.Constant.t*int) array = - match kind_of_term ((strip_lam e)) with + match Constr.kind ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> @@ -430,7 +437,7 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) then user_err Pp.(str "Not a mutal recursive block") ) l_params @@ -439,7 +446,7 @@ let get_funs_constant mp dp = let _check_bodies = try let extract_info is_first body = - match kind_of_term body with + match Constr.kind body with | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 @@ -450,7 +457,7 @@ let get_funs_constant mp dp = let check body = (* Hope this is correct *) let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then user_err Pp.(str "Not a mutal recursive block") @@ -564,7 +571,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -574,10 +581,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let t = (strip_prod_assum t) in let applied_g = List.hd (List.rev (snd (decompose_app t))) in let g = fst (decompose_app applied_g) in - if eq_constr f g + if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 2eb1b7935d..a3315f22cf 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr val generate_functional_principle : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71e..87609296bc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e8e5bfccc1..fa43536304 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,7 +1,7 @@ open Printer open Pp open Names -open Term +open Constr open Vars open Glob_term open Glob_ops @@ -378,29 +378,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let open Context.Rel.Declaration in - match decl with + let open Context.Rel.Declaration in + let sigma, _ = Pfedit.get_current_context () in + match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> - let new_t = substl ctxt t in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> - let new_t = substl ctxt t in - let new_v = substl ctxt v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ - str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) - ) + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + ) (Environ.rel_context new_env) ~init:(env,[]) ) @@ -478,7 +479,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> @@ -651,8 +652,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); @@ -683,8 +684,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); @@ -896,24 +897,24 @@ let same_raw_term rt1 rt2 = | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -922,7 +923,7 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in let open CAst in match DAst.get rt with @@ -966,7 +967,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -1011,11 +1012,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq' = DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = - match kind_of_term eq'_as_constr with + match Constr.kind eq'_as_constr with | App(_,[|_;_;ty;_|]) -> let ty = Array.to_list (snd (destApp ty)) in let ty' = snd (Util.List.chop nparam ty) in @@ -1098,7 +1099,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1114,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1133,7 +1134,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> @@ -1297,7 +1298,7 @@ let rec rebuild_return_type rt = CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) + evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 0cab5a6d35..ff0e98d00f 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -11,7 +11,7 @@ val build_inductive : Id.t list -> (* The list of function name *) *) Evd.evar_map -> - Term.pconstant list -> + Constr.pconstant list -> (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dab094f913..9e22ad3063 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,7 +1,8 @@ open CErrors +open Sorts open Util open Names -open Term +open Constr open EConstr open Pp open Indfun_common @@ -46,7 +47,7 @@ let functional_induction with_clean c princl pat = try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr (mkConst c') ) + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -74,7 +75,7 @@ let functional_induction with_clean c princl pat = (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) user_err (str "Cannot find induction principle for " - ++Printer.pr_leconstr (mkConst c') ) + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in let princ = EConstr.of_constr princ in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') @@ -841,12 +842,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list * let make_graph (f_ref:global_reference) = let c,c_body = match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) - end - | _ -> raise (UserError (None, str "Not a function reference") ) + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + let sigma, env = Pfedit.get_current_context () in + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 76fcd5ec87..5a9248d478 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,8 +1,10 @@ open Names open Pp +open Constr open Libnames open Globnames open Refiner + let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" @@ -111,7 +113,7 @@ let const_of_id id = (str "cannot find " ++ Id.print id) let def_of_const t = - match (Term.kind_of_term t) with + match Constr.kind t with Term.Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c @@ -181,7 +183,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -195,6 +199,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -204,6 +209,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise @@ -330,18 +336,18 @@ let discharge_Function (_,finfos) = is_general = finfos.is_general } -open Term - let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -349,7 +355,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in @@ -545,16 +551,16 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b -type tcc_lemma_value = +type tcc_lemma_value = | Undefined - | Value of Term.constr + | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index d41abee87e..5cc7163aa3 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -38,7 +38,7 @@ val chop_rlambda_n : int -> Glob_term.glob_constr -> val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr -val def_of_const : Term.constr -> Term.constr +val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) @@ -118,10 +118,10 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t - -type tcc_lemma_value = + +type tcc_lemma_value = | Undefined - | Value of Term.constr + | Value of Constr.t | Not_needed val funind_purify : ('a -> 'b) -> ('a -> 'b) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 93317fce1b..694c800514 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Term +open Constr open EConstr open Vars open Pp @@ -850,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 77c26f8ce6..9e2774ff32 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -18,6 +18,7 @@ open Vernacexpr open Pp open Names open Term +open Constr open Vars open Declarations open Glob_term @@ -36,19 +37,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c) (** Substitutions in constr *) let compare_constr_nosub t1 t2 = - if compare_constr (fun _ _ -> false) t1 t2 + if Constr.compare_head (fun _ _ -> false) t1 t2 then true else false let rec compare_constr' t1 t2 = if compare_constr_nosub t1 t2 then true - else (compare_constr (compare_constr') t1 t2) + else (Constr.compare_head (compare_constr') t1 t2) let rec substitterm prof t by_t in_u = if (compare_constr' (lift prof t) in_u) then (lift prof by_t) - else map_constr_with_binders succ + else Constr.map_with_binders succ (fun i -> substitterm i t by_t) prof in_u let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl @@ -89,20 +90,28 @@ let next_ident_fresh (id:Id.t) = (* comment this line to see debug msgs *) let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c) -let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prconstr c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c) + +let prconstrnl c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") + let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) let prNamedConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); msg(str ""); end let prNamedRConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc @@ -954,16 +963,16 @@ let funify_branches relinfo nfuns branch = | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind | _ -> assert false in let is_dom c = - match kind_of_term c with + match Constr.kind c with | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct | _ -> false in let _dom_i c = assert (is_dom c); - match kind_of_term c with + match Constr.kind c with | Ind((u,i)) | Construct((u,_),i) -> i | _ -> assert false in let _is_pred c shift = - match kind_of_term c with + match Constr.kind c with | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) | _ -> false in (* FIXME: *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 76f859ed72..766adfc63a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -9,7 +9,7 @@ module CVars = Vars -open Term +open Constr open EConstr open Vars open Namegen @@ -53,6 +53,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] +let pr_leconstr_rd = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let coq_init_constant s = EConstr.of_constr ( Universes.constr_of_global @@ @@ -62,14 +66,14 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = - let ce = definition_entry ~univs:ctx value (*FIXME *) in +let declare_fun f_id kind ?univs value = + let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = - match (kind_of_term t) with + match (Constr.kind t) with Const sp -> (try (match constant_opt_value_in (Global.env ()) sp with | Some c -> c @@ -137,13 +141,13 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") -let iter = function () -> (constr_of_global (delayed_force iter_ref)) +let iter_rd = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") @@ -175,8 +179,9 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f:Term.constr list -> global_reference -> Term.constr) = +let (value_f: Constr.t list -> global_reference -> Constr.t) = let open Term in + let open Constr in fun al fterm -> let rev_x_id_l = ( @@ -207,7 +212,7 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -335,7 +340,8 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p) + let _, env = Pfedit.get_current_context () in + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -453,7 +459,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -461,7 +467,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -489,8 +495,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -513,7 +519,7 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_leconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -729,7 +735,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac @@ -738,7 +744,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g @@ -851,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = @@ -989,11 +999,11 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos) + (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1039,11 +1049,12 @@ let prove_eq = travel equation_info *) let compute_terminate_type nb_args func = let open Term in + let open Constr in let open CVars in let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = - mkApp(delayed_force iter, + mkApp(delayed_force iter_rd, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: constr_of_global func::mkRel 1:: @@ -1222,8 +1233,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in - let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - sigma, List.map (Goal.V82.abstract_type sigma) sgs + let sgs,_,_,_,sigma = Proof.proof p in + sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals let build_and_l sigma l = @@ -1416,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1460,7 +1471,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference - -> Term.constr -> unit) = + -> Constr.t -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in let opacity = @@ -1468,7 +1479,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in @@ -1514,6 +1525,7 @@ let (com_eqn : int -> Id.t -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let open Term in + let open Constr in let open CVars in let env = Global.env() in let evd = ref (Evd.from_env env) in @@ -1536,7 +1548,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) (* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) (* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) - match kind_of_term eq' with + match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) | _ -> failwith "Recursive Definition (res not eq)" @@ -1548,8 +1560,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 63bbdbe7e3..50b84731b5 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,3 +1,4 @@ +open Constr (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : @@ -11,9 +12,9 @@ bool -> Constrintern.internalization_env -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (Term.pconstant -> + int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> - Term.pconstant -> - Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 89feea8dcf..bb01aca558 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 65c186a419..982fc7cc3c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -313,30 +313,51 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.universe_context_set sigma in + let poly = Flags.use_polymorphic_flag () in + let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff l2r lc n bl = - let l = Locality.LocalityFixme.consume () in - Hints.add_hints (Locality.make_module_locality l) bl +let add_hints_iff ?locality l2r lc n bl = + Hints.add_hints (Locality.make_module_locality locality) bl (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff true lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n bl; + st + end + ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff true lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n ["core"]; + st + end + ] END -VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF + +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n bl; + st + end + ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff false lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n ["core"]; + st + end + ] END (**********************************************************************) @@ -415,7 +436,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ] END VERNAC COMMAND EXTEND DeriveInversion @@ -424,7 +445,7 @@ VERNAC COMMAND EXTEND DeriveInversion -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c InProp false inv_tac ] + -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion @@ -514,7 +535,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity : bool * Term.constr -> obj = +let inTransitivity : bool * Constr.t -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); @@ -852,34 +873,12 @@ TACTIC EXTEND is_evar ] END -let has_evar sigma c = -let rec has_evar x = - match EConstr.kind sigma x with - | Evar _ -> true - | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ -> - false - | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) -> - has_evar t1 || has_evar t2 - | LetIn (_, t1, t2, t3) -> - has_evar t1 || has_evar t2 || has_evar t3 - | App (t1, ts) -> - has_evar t1 || has_evar_array ts - | Case (_, t1, t2, ts) -> - has_evar t1 || has_evar t2 || has_evar_array ts - | Fix ((_, tr)) | CoFix ((_, tr)) -> - has_evar_prec tr - | Proj (p, c) -> has_evar c -and has_evar_array x = - Array.exists has_evar x -and has_evar_prec (_, ts1, ts2) = - Array.exists has_evar ts1 || Array.exists has_evar ts2 -in -has_evar c - TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") + if Evarutil.has_undefined_evars sigma x + then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "No evars") ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 5baa0d5c1d..90a44708fc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -51,8 +51,12 @@ let eval_uconstrs ist cs = List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) ARGUMENT EXTEND auto_using TYPED AS uconstr_list @@ -186,7 +190,7 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c let glob_hints_path ist = Hints.glob_hints_path - + ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path @@ -210,10 +214,15 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] END diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 104977aef3..ed2d9da63a 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -91,7 +91,7 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) -open Term +open Constr open Proofview.Notations let rec eq_constr_mod_evars sigma x y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index c577cb2198..ebf6e450b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -232,20 +227,17 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ id = identref; ":="; te = tactic_expr -> - (id, arg_of_expr te) - | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (id, arg_of_expr (TacFun(args,te))) ] ] + [ [ (l,id) = identref; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr te) + | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + (na, arg_of_expr te) + | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: @@ -467,13 +459,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END -VERNAC COMMAND EXTEND VernacTacticNotation +VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> - [ - let l = Locality.LocalityFixme.consume () in - let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e + [ VtSideff [], VtNow ] -> + [ fun ~atts ~st -> let open Vernacinterp in + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + st ] END @@ -510,15 +502,15 @@ PRINTED BY pr_tacdef_body | [ tacdef_body(t) ] -> [ t ] END -VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ((_,r),_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater - ] -> [ - let lc = Locality.LocalityFixme.consume () in - Tacentries.register_ltac (Locality.make_module_locality lc) l + ] -> [ fun ~atts ~st -> let open Vernacinterp in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + st ] END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index fea9e837b1..f6cc3833a7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF | [ "Admit" "Obligations" ] -> [ admit_obligations None ] END -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> begin + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + end] END open Pp diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b148d962ed..ea1808a255 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) +let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst (snd ge))) +let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l @@ -239,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + st + ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + st + ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + st + ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + st + ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + st + ] END TACTIC EXTEND setoid_symmetry @@ -272,5 +291,7 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> + [ let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e467d3e2ca..e5ff473568 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,32 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -119,9 +145,9 @@ type 'a extra_genarg_printer = | Some Refl -> let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -500,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function @@ -536,15 +560,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (id,(bl,t)) = - hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) - - let pr_let_clauses recflag pr = function + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in + hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ + str " :=" ++ brk (1,1) ++ pr t) + + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -706,8 +739,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -858,7 +893,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -1003,7 +1038,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1120,10 +1155,10 @@ let pr_goal_selector ~toplevel s = let ty = EConstr.Unsafe.to_constr ty in let rec strip_ty acc n ty = if n=0 then (List.rev acc, EConstr.of_constr ty) else - match Term.kind_of_term ty with - Term.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b - | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in + match Constr.kind ty with + | Constr.Prod(na,a,b) -> + strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1175,42 +1210,77 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = - Genprint.PrinterNeedsContext (fun env sigma -> + Genprint.TopPrinterNeedsContext (fun env sigma -> h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = + let env = Global.env () in + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + in + Genprint.register_print0 wit f g h + let declare_extra_vernac_genarg_pprule wit f = - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) -let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in Miscprint.pr_intro_pattern print_constr p) -let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) -let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in Miscprint.pr_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in pr_with_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, c = match c with | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) | clear_flag,ElimOnAnonHyp n as x -> sigma, x @@ -1219,90 +1289,104 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) let make_constr_printer f c = - Genprint.PrinterNeedsContextAndLevel { + Genprint.TopPrinterNeedsContextAndLevel { Genprint.default_already_surrounded = Ppconstr.ltop; Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) + + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) (lift int); - Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); - Genprint.register_print0 wit_ident - pr_id pr_id (lift pr_id); - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) (lift pr_id); - Genprint.register_print0 + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_bindings_env ; - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 wit_open_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_destruction_arg_env ; - Genprint.register_print0 Stdarg.wit_int int int (lift int); - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); - Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); - Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5ecfaf590c..bda5774abf 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -40,12 +40,37 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_genarg_pprule_with_level : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer_with_level -> + 'b glob_extra_genarg_printer_with_level -> + 'c extra_genarg_printer_with_level -> + (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> unit diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9ae8bfe65b..5225420dc4 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -408,7 +408,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_notice (to_string ~cutoff ~filter results) + Feedback.msg_info (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 2b1106ee21..f095660638 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -13,7 +13,7 @@ open Profile_ltac open Stdarg -DECLARE PLUGIN "profile_ltac_plugin" +DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) @@ -22,7 +22,7 @@ TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END -TACTIC EXTEND stop_profiling +TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1809f0fcdb..2e14243d8a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pp open CErrors open Util +open Names open Nameops open Namegen -open Term +open Constr open EConstr open Vars open Reduction @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -426,7 +426,7 @@ let split_head = function | [] -> assert(false) let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = - pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y') + pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c = it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx) in let sk = - if sortp == InProp then - if sortc == InProp then + if sortp == Sorts.InProp then + if sortc == Sorts.InProp then if dep then case_dep_scheme_kind_from_prop else case_scheme_kind_from_prop else ( @@ -1143,7 +1143,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma = in anew_instance global binders instance [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] -let declare_relation ?(binders=[]) a aeq n refl symm trans = +let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in + let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with @@ -1884,11 +1884,11 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.const_univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1972,9 +1972,10 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then + let uctx = UState.const_univ_entry ~poly uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,UState.context uctx),None), + (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance @@ -2020,14 +2021,16 @@ let add_morphism glob binders m s n = (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2062,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in @@ -2083,8 +2086,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 63e891b455..17e7244b39 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast = type rewrite_proof = | RewPrf of constr * constr - | RewCast of Term.cast_kind + | RewCast of Constr.cast_kind type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) @@ -75,7 +75,7 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : +val declare_relation : ?locality:bool -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4d171ecbc2..9ae112d371 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -8,7 +8,7 @@ open Util open Names -open Term +open Constr open EConstr open Misctypes open Genarg @@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) (fun c -> - Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in + Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) @@ -172,8 +172,8 @@ let id_of_name = function | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> Label.to_id (Label.make "Prop") - | Type _ -> Label.to_id (Label.make "Type") + | Sorts.Prop _ -> Label.to_id (Label.make "Prop") + | Sorts.Type _ -> Label.to_id (Label.make "Type") end | _ -> fail() diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 1639736883..ccd555b615 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Id.t located * 'a gen_tactic_arg) list * + (Name.t located * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index f171fd07d7..ebffde441d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc @@ -468,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err ?loc + Nameops.Name.fold_right (fun id accu -> + if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") - else Id.Set.add name accu + else Id.Set.add id accu) name accu in List.fold_left fold Id.Set.empty lrc @@ -812,7 +813,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, id), c) :: accu + ((loc, Name id), c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fd75862c6f..32a3b53fd8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -242,9 +242,9 @@ let pr_value env v = | None -> str "a value of type" ++ spc () ++ pr_argument_type v in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -821,9 +821,9 @@ let message_of_value v = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> Ftactic.return (pr ()) - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> Ftactic.return (pr ()) + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function @@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) @@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = begin let open Genprint in match generic_val_print v with - | PrinterBasic _ -> call_debug None - | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + | TopPrinterBasic _ -> call_debug None + | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ -> Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval @@ -1380,13 +1380,38 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | VFun (_, _, _,vars,_) -> - let numargs = List.length vars in - Tacticals.New.tclZEROMSG - (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ - Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ - Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum Name.print vars ++ Pp.str ".") + | VFun (appl,_,vmap,vars,_) -> + let tactic_nm = + match appl with + UnnamedAppl -> "An unnamed user-defined tactic" + | GlbAppl apps -> + let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + match nms with + [] -> assert false + | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) + in + let numargs = List.length vars in + let givenargs = + List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in + let numgiven = List.length givenargs in + Tacticals.New.tclZEROMSG + (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ + (match numargs with + 0 -> assert false + | 1 -> + Pp.str "There is a missing argument for variable " ++ + (Name.print (List.hd vars)) + | _ -> Pp.str "There are missing arguments for variables " ++ + pr_enum Name.print vars) ++ Pp.pr_comma () ++ + match numgiven with + 0 -> + Pp.str "no arguments at all were provided." + | 1 -> + Pp.str "an argument was provided for variable " ++ + Pp.str (List.hd givenargs) ++ Pp.str "." + | _ -> + Pp.str "arguments were provided for variables " ++ + pr_enum Pp.str givenargs ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in @@ -1397,9 +1422,9 @@ and tactic_of_value ist vle = and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let fold accu ((_, id), b) = + let fold accu ((_, na), b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in - Id.Map.add id v accu + Name.fold_right (fun id -> Id.Map.add id v) na accu in let lfun = List.fold_left fold ist.lfun llc in let () = lref := lfun in @@ -1412,9 +1437,9 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, id), body) :: defs -> + | ((_, na), body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> - fold (Id.Map.add id v lfun) defs) + fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in fold ist.lfun llc diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 180fb2db40..79bf3685e2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -91,9 +91,10 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (is_global ref' t') then - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; + (let sigma, env = Pfedit.get_current_context () in + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ + pr_global ref')); ref' in subst_or_var (subst_located subst_global) @@ -120,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc9..2dd7c9a747 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e5907..e87951dd7f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index fc6781b067..cb54cac3f1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -20,6 +20,7 @@ open Pp open Mutils open Goptions open Names +open Constr (** * Debug flag @@ -580,9 +581,9 @@ struct | Ukn | BadStr of string | BadNum of int - | BadTerm of Term.constr + | BadTerm of constr | Msg of string - | Goal of (Term.constr list ) * Term.constr * parse_error + | Goal of (constr list ) * constr * parse_error let string_of_error = function | Ukn -> "ukn" @@ -983,7 +984,9 @@ struct let parse_expr sigma parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term); + then ( + let _, env = Pfedit.get_current_context () in + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); (* let constant_or_variable env term = @@ -1102,9 +1105,10 @@ struct | _ -> raise ParseError - let rconstant sigma term = + let rconstant sigma term = + let _, env = Pfedit.get_current_context () in if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1144,9 +1148,9 @@ struct let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); - match EConstr.kind sigma cstr with + if debug + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + match EConstr.kind sigma cstr with | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in @@ -1521,7 +1525,7 @@ let rec witness prover l1 l2 = let rec apply_ids t ids = match ids with | [] -> t - | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids + | i::ids -> apply_ids (mkApp(t,[| mkVar i |])) ids let coq_Node = lazy (gen_constant_in_modules "VarMap" @@ -1907,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr ff); + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; @@ -1931,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + (dump_cstr spec.typ spec.dump_coeff) ff' in + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; (* Even if it does not work, this does not mean it is not provable diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 7da4a3b829..52c6ef983d 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 @@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c1..387a525141 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 72934a15d9..559dfab524 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -8,7 +8,7 @@ open CErrors open Util -open Term +open Constr open Tactics open Coqlib @@ -204,42 +204,42 @@ else mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)] let rec parse_pos p = - match kind_of_term p with + match Constr.kind p with | App (a,[|p2|]) -> - if eq_constr a (Lazy.force pxO) then num_2 */ (parse_pos p2) + if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2) else num_1 +/ (num_2 */ (parse_pos p2)) | _ -> num_1 let parse_z z = - match kind_of_term z with + match Constr.kind z with | App (a,[|p2|]) -> - if eq_constr a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) + if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) | _ -> num_0 let parse_n z = - match kind_of_term z with + match Constr.kind z with | App (a,[|p2|]) -> parse_pos p2 | _ -> num_0 let rec parse_term p = - match kind_of_term p with + match Constr.kind p with | App (a,[|_;p2|]) -> - if eq_constr a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) - else if eq_constr a (Lazy.force ttconst) then Const (parse_z p2) - else if eq_constr a (Lazy.force ttopp) then Opp (parse_term p2) + if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) + else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2) + else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2) else Zero | App (a,[|_;p2;p3|]) -> - if eq_constr a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) - else if eq_constr a (Lazy.force ttpow) then + if Constr.equal a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) + else if Constr.equal a (Lazy.force ttpow) then Pow (parse_term p2, int_of_num (parse_n p3)) else Zero | _ -> Zero let rec parse_request lp = - match kind_of_term lp with + match Constr.kind lp with | App (_,[|_|]) -> [] | App (_,[|_;p;lp1|]) -> (parse_term p)::(parse_request lp1) diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index d6e3071aa3..e50a12a509 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val nsatz_compute : Term.constr -> unit Proofview.tactic +val nsatz_compute : Constr.t -> unit Proofview.tactic diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ff69ddefb8..8692842468 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -466,12 +466,14 @@ let destructurate_prop sigma t = | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo -let destructurate_type sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in +let nf = Tacred.simpl + +let destructurate_type env sigma t = + let is_conv = Reductionops.is_conv env sigma in + let c, args = decompose_app sigma (nf env sigma t) in match EConstr.kind sigma c, args with - | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args) - | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args) + | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) + | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) | _ -> Kufo let destructurate_term sigma t = @@ -1459,17 +1461,13 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = else (tactic,defs) -let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c - -let destructure_omega gl tac_def (id,c) = - let open Tacmach.New in - let sigma = project gl in +let destructure_omega env sigma tac_def (id,c) = if String.equal (atompart_of_id id) "State" then tac_def else try match destructurate_prop sigma c with | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end -> + when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> let t = mk_plus t1 (mk_inv t2) in normalize_equation sigma id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def @@ -1507,7 +1505,7 @@ let coq_omega = Proofview.Goal.enter begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = destructure_omega gl in + let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = @@ -1727,27 +1725,26 @@ let not_binop = function exception Undecidable -let rec decidability gl t = - let open Tacmach.New in - match destructurate_prop (project gl) t with +let rec decidability env sigma t = + match destructurate_prop sigma t with | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(And,[t1;t2]) -> mkApp (Lazy.force coq_dec_and, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Iff,[t1;t2]) -> mkApp (Lazy.force coq_dec_iff, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kimp(t1,t2) -> (* This is the only situation where it's not obvious that [t] is in Prop. The recursive call on [t2] will ensure that. *) mkApp (Lazy.force coq_dec_imp, - [| t1; t2; decidability gl t1; decidability gl t2 |]) + [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Not,[t1]) -> - mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |]) + mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type (project gl) (pf_nf gl typ) with + begin match destructurate_type env sigma typ with | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> raise Undecidable @@ -1784,15 +1781,16 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - let decidability = decidability gl in - let pf_nf = pf_nf gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in let rec loop = function | [] -> (tclTHEN nat_inject coq_omega) | LocalDef (i,body,typ) :: lit when !letin_flag -> Proofview.tclEVARMAP >>= fun sigma -> begin try - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) | Kapp(Z,_) -> let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in let hty = mk_gen_eq typ (mkVar i) body in @@ -1895,7 +1893,7 @@ let destructure_hyps = with Not_found -> loop lit) | Kapp(Eq,[typ;t1;t2]) -> if !old_style_flag then begin - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> tclTHENLIST [ (simplest_elim @@ -1912,7 +1910,7 @@ let destructure_hyps = ] | _ -> loop lit end else begin - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) @@ -1940,7 +1938,9 @@ let destructure_hyps = let destructure_goal = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let decidability = decidability gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in let rec loop t = Proofview.tclEVARMAP >>= fun sigma -> let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index e1e73b1c32..0ea8904f2c 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -104,7 +104,7 @@ open CErrors open Util open Names -open Term +open Constr open EConstr open Pattern open Patternops @@ -166,11 +166,7 @@ exchange ?1 and ?2 in the example above) *) -module ConstrSet = Set.Make( - struct - type t = Term.constr - let compare = Term.compare - end) +module ConstrSet = Set.Make(Constr) type inversion_scheme = { normal_lhs_rhs : (constr * constr_pattern) list; @@ -385,11 +381,7 @@ let rec sort_subterm gl l = | [] -> [] | h::t -> insert h (sort_subterm gl t) -module Constrhash = Hashtbl.Make - (struct type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr - end) +module Constrhash = Hashtbl.Make(Constr) let subst_meta subst c = let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index c27ac2ea44..0d491d92bd 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,14 +7,15 @@ *************************************************************************) open Names +open Constr let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = | Kvar of string - | Kapp of string * Term.constr list - | Kimp of Term.constr * Term.constr + | Kapp of string * constr list + | Kimp of constr * constr | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,27 +31,27 @@ let string_of_global r = prefix^(Names.Id.to_string (Nametab.basename_of_global r)) let destructurate t = - let c, args = Term.decompose_app t in - match Term.kind_of_term c, args with - | Term.Const (sp,_), args -> + let c, args = decompose_app t in + match Constr.kind c, args with + | Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) - | Term.Construct (csp,_) , args -> + | Construct (csp,_) , args -> Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Term.Ind (isp,_), args -> + | Ind (isp,_), args -> Kapp (string_of_global (Globnames.IndRef isp), args) - | Term.Var id, [] -> Kvar(Names.Id.to_string id) - | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body) + | Var id, [] -> Kvar(Names.Id.to_string id) + | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | _ -> Kufo exception DestConstApp let dest_const_apply t = - let f,args = Term.decompose_app t in + let f,args = decompose_app t in let ref = - match Term.kind_of_term f with - | Term.Const (sp,_) -> Globnames.ConstRef sp - | Term.Construct (csp,_) -> Globnames.ConstructRef csp - | Term.Ind (isp,_) -> Globnames.IndRef isp + match Constr.kind f with + | Const (sp,_) -> Globnames.ConstRef sp + | Construct (csp,_) -> Globnames.ConstructRef csp + | Ind (isp,_) -> Globnames.IndRef isp | _ -> raise DestConstApp in Nametab.basename_of_global ref, args @@ -129,7 +130,7 @@ let coq_O = lazy(init_constant "O") let rec mk_nat = function | 0 -> Lazy.force coq_O - | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) (* Lists *) @@ -141,47 +142,47 @@ let mkListConst c = if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] else fun _ -> Univ.Instance.empty in - fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u) + fun u -> mkConstructU (Globnames.destConstructRef r, inst u) -let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) +let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|]) let mk_list univ typ l = let rec loop = function | [] -> coq_nil univ typ | (step :: l) -> - Term.mkApp (coq_cons univ typ, [| step; loop l |]) in + mkApp (coq_cons univ typ, [| step; loop l |]) in loop l let mk_plist = - let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in - fun l -> mk_list type1lev Term.mkProp l + let type1lev = Universes.new_univ_level () in + fun l -> mk_list type1lev mkProp l let mk_list = mk_list Univ.Level.set type parse_term = - | Tplus of Term.constr * Term.constr - | Tmult of Term.constr * Term.constr - | Tminus of Term.constr * Term.constr - | Topp of Term.constr - | Tsucc of Term.constr + | Tplus of constr * constr + | Tmult of constr * constr + | Tminus of constr * constr + | Topp of constr + | Tsucc of constr | Tnum of Bigint.bigint | Tother type parse_rel = - | Req of Term.constr * Term.constr - | Rne of Term.constr * Term.constr - | Rlt of Term.constr * Term.constr - | Rle of Term.constr * Term.constr - | Rgt of Term.constr * Term.constr - | Rge of Term.constr * Term.constr + | Req of constr * constr + | Rne of constr * constr + | Rlt of constr * constr + | Rle of constr * constr + | Rgt of constr * constr + | Rge of constr * constr | Rtrue | Rfalse - | Rnot of Term.constr - | Ror of Term.constr * Term.constr - | Rand of Term.constr * Term.constr - | Rimp of Term.constr * Term.constr - | Riff of Term.constr * Term.constr + | Rnot of constr + | Ror of constr * constr + | Rand of constr * constr + | Rimp of constr * constr + | Riff of constr * constr | Rother let parse_logic_rel c = match destructurate c with @@ -196,6 +197,7 @@ let parse_logic_rel c = match destructurate c with (* Binary numbers *) +let coq_Z = lazy (bin_constant "Z") let coq_xH = lazy (bin_constant "xH") let coq_xO = lazy (bin_constant "xO") let coq_xI = lazy (bin_constant "xI") @@ -209,34 +211,34 @@ let rec mk_positive n = if Bigint.equal n Bigint.one then Lazy.force coq_xH else let (q,r) = Bigint.euclid n Bigint.two in - Term.mkApp + mkApp ((if Bigint.equal r Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), [| mk_positive q |]) let mk_N = function | 0 -> Lazy.force coq_N0 - | n -> Term.mkApp (Lazy.force coq_Npos, + | n -> mkApp (Lazy.force coq_Npos, [| mk_positive (Bigint.of_int n) |]) module type Int = sig - val typ : Term.constr Lazy.t - val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool - val plus : Term.constr Lazy.t - val mult : Term.constr Lazy.t - val opp : Term.constr Lazy.t - val minus : Term.constr Lazy.t - - val mk : Bigint.bigint -> Term.constr - val parse_term : Term.constr -> parse_term - val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel + val typ : constr Lazy.t + val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool + val plus : constr Lazy.t + val mult : constr Lazy.t + val opp : constr Lazy.t + val minus : constr Lazy.t + + val mk : Bigint.bigint -> constr + val parse_term : constr -> parse_term + val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel (* check whether t is built only with numbers and + * - *) - val get_scalar : Term.constr -> Bigint.bigint option + val get_scalar : constr -> Bigint.bigint option end module Z : Int = struct -let typ = lazy (bin_constant "Z") +let typ = coq_Z let plus = lazy (z_constant "Z.add") let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") @@ -266,9 +268,9 @@ let recognize_Z t = let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 else if Bigint.is_strictly_pos n then - Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) else - Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) let mk = mk_Z @@ -284,14 +286,9 @@ let parse_term t = (match recognize_Z t with Some t -> Tnum t | None -> Tother) | _ -> Tother -let pf_nf gl c = - EConstr.Unsafe.to_constr - (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) - let is_int_typ gl t = - match destructurate (pf_nf gl t) with - | Kapp("Z",[]) -> true - | _ -> false + Tacmach.New.pf_apply Reductionops.is_conv gl + (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) let parse_rel gl t = match destructurate t with diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 80e00e4e14..5ba063d9d0 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -8,116 +8,117 @@ (** Coq objects used in romega *) +open Constr (* from Logic *) -val coq_refl_equal : Term.constr lazy_t -val coq_and : Term.constr lazy_t -val coq_not : Term.constr lazy_t -val coq_or : Term.constr lazy_t -val coq_True : Term.constr lazy_t -val coq_False : Term.constr lazy_t -val coq_I : Term.constr lazy_t +val coq_refl_equal : constr lazy_t +val coq_and : constr lazy_t +val coq_not : constr lazy_t +val coq_or : constr lazy_t +val coq_True : constr lazy_t +val coq_False : constr lazy_t +val coq_I : constr lazy_t (* from ReflOmegaCore/ZOmega *) -val coq_t_int : Term.constr lazy_t -val coq_t_plus : Term.constr lazy_t -val coq_t_mult : Term.constr lazy_t -val coq_t_opp : Term.constr lazy_t -val coq_t_minus : Term.constr lazy_t -val coq_t_var : Term.constr lazy_t - -val coq_proposition : Term.constr lazy_t -val coq_p_eq : Term.constr lazy_t -val coq_p_leq : Term.constr lazy_t -val coq_p_geq : Term.constr lazy_t -val coq_p_lt : Term.constr lazy_t -val coq_p_gt : Term.constr lazy_t -val coq_p_neq : Term.constr lazy_t -val coq_p_true : Term.constr lazy_t -val coq_p_false : Term.constr lazy_t -val coq_p_not : Term.constr lazy_t -val coq_p_or : Term.constr lazy_t -val coq_p_and : Term.constr lazy_t -val coq_p_imp : Term.constr lazy_t -val coq_p_prop : Term.constr lazy_t - -val coq_s_bad_constant : Term.constr lazy_t -val coq_s_divide : Term.constr lazy_t -val coq_s_not_exact_divide : Term.constr lazy_t -val coq_s_sum : Term.constr lazy_t -val coq_s_merge_eq : Term.constr lazy_t -val coq_s_split_ineq : Term.constr lazy_t - -val coq_direction : Term.constr lazy_t -val coq_d_left : Term.constr lazy_t -val coq_d_right : Term.constr lazy_t - -val coq_e_split : Term.constr lazy_t -val coq_e_extract : Term.constr lazy_t -val coq_e_solve : Term.constr lazy_t - -val coq_interp_sequent : Term.constr lazy_t -val coq_do_omega : Term.constr lazy_t - -val mk_nat : int -> Term.constr -val mk_N : int -> Term.constr +val coq_t_int : constr lazy_t +val coq_t_plus : constr lazy_t +val coq_t_mult : constr lazy_t +val coq_t_opp : constr lazy_t +val coq_t_minus : constr lazy_t +val coq_t_var : constr lazy_t + +val coq_proposition : constr lazy_t +val coq_p_eq : constr lazy_t +val coq_p_leq : constr lazy_t +val coq_p_geq : constr lazy_t +val coq_p_lt : constr lazy_t +val coq_p_gt : constr lazy_t +val coq_p_neq : constr lazy_t +val coq_p_true : constr lazy_t +val coq_p_false : constr lazy_t +val coq_p_not : constr lazy_t +val coq_p_or : constr lazy_t +val coq_p_and : constr lazy_t +val coq_p_imp : constr lazy_t +val coq_p_prop : constr lazy_t + +val coq_s_bad_constant : constr lazy_t +val coq_s_divide : constr lazy_t +val coq_s_not_exact_divide : constr lazy_t +val coq_s_sum : constr lazy_t +val coq_s_merge_eq : constr lazy_t +val coq_s_split_ineq : constr lazy_t + +val coq_direction : constr lazy_t +val coq_d_left : constr lazy_t +val coq_d_right : constr lazy_t + +val coq_e_split : constr lazy_t +val coq_e_extract : constr lazy_t +val coq_e_solve : constr lazy_t + +val coq_interp_sequent : constr lazy_t +val coq_do_omega : constr lazy_t + +val mk_nat : int -> constr +val mk_N : int -> constr (** Precondition: the type of the list is in Set *) -val mk_list : Term.constr -> Term.constr list -> Term.constr -val mk_plist : Term.types list -> Term.types +val mk_list : constr -> constr list -> constr +val mk_plist : types list -> types (** Analyzing a coq term *) (* The generic result shape of the analysis of a term. One-level depth, except when a number is found *) type parse_term = - Tplus of Term.constr * Term.constr - | Tmult of Term.constr * Term.constr - | Tminus of Term.constr * Term.constr - | Topp of Term.constr - | Tsucc of Term.constr + Tplus of constr * constr + | Tmult of constr * constr + | Tminus of constr * constr + | Topp of constr + | Tsucc of constr | Tnum of Bigint.bigint | Tother (* The generic result shape of the analysis of a relation. One-level depth. *) type parse_rel = - Req of Term.constr * Term.constr - | Rne of Term.constr * Term.constr - | Rlt of Term.constr * Term.constr - | Rle of Term.constr * Term.constr - | Rgt of Term.constr * Term.constr - | Rge of Term.constr * Term.constr + Req of constr * constr + | Rne of constr * constr + | Rlt of constr * constr + | Rle of constr * constr + | Rgt of constr * constr + | Rge of constr * constr | Rtrue | Rfalse - | Rnot of Term.constr - | Ror of Term.constr * Term.constr - | Rand of Term.constr * Term.constr - | Rimp of Term.constr * Term.constr - | Riff of Term.constr * Term.constr + | Rnot of constr + | Ror of constr * constr + | Rand of constr * constr + | Rimp of constr * constr + | Riff of constr * constr | Rother (* A module factorizing what we should now about the number representation *) module type Int = sig (* the coq type of the numbers *) - val typ : Term.constr Lazy.t + val typ : constr Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool + val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool (* the operations on the numbers *) - val plus : Term.constr Lazy.t - val mult : Term.constr Lazy.t - val opp : Term.constr Lazy.t - val minus : Term.constr Lazy.t + val plus : constr Lazy.t + val mult : constr Lazy.t + val opp : constr Lazy.t + val minus : constr Lazy.t (* building a coq number *) - val mk : Bigint.bigint -> Term.constr + val mk : Bigint.bigint -> constr (* parsing a term (one level, except if a number is found) *) - val parse_term : Term.constr -> parse_term + val parse_term : constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel + val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : Term.constr -> Bigint.bigint option + val get_scalar : constr -> Bigint.bigint option end (* Currently, we only use Z numbers *) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 661485aeeb..54ff44fbd3 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -27,8 +28,6 @@ let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) let (>>) = Tacticals.New.tclTHEN -let mkApp = Term.mkApp - (* \section{Types} \subsection{How to walk in a term} To represent how to get to a proposition. Only choice points are @@ -68,14 +67,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq (it could contains some [Term.Var] but no [Term.Rel]). So no need to lift when breaking or creating arrows. *) type oproposition = - Pequa of Term.constr * oequation (* constr = copy of the Coq formula *) + Pequa of constr * oequation (* constr = copy of the Coq formula *) | Ptrue | Pfalse | Pnot of oproposition | Por of int * oproposition * oproposition | Pand of int * oproposition * oproposition | Pimp of int * oproposition * oproposition - | Pprop of Term.constr + | Pprop of constr (* The equations *) and oequation = { @@ -102,9 +101,9 @@ and oequation = { type environment = { (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : Term.constr list; + mutable terms : constr list; (* La meme chose pour les propositions *) - mutable props : Term.constr list; + mutable props : constr list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) real_indices : int IntHtbl.t; @@ -184,8 +183,9 @@ let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" | t :: l -> + let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in @@ -219,7 +219,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i calcul des variables utiles. *) let add_reified_atom t env = - try List.index0 Term.eq_constr t env.terms + try List.index0 Constr.equal t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -237,7 +237,7 @@ let set_reified_atom v t env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try List.index0 Term.eq_constr t env.props + try List.index0 Constr.equal t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -560,7 +560,7 @@ let reify_hyp env gl i = | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> let d = EConstr.Unsafe.to_constr d in let dummy = Lazy.force coq_True in - let p = mk_equation env ctxt dummy Eq (Term.mkVar i) d in + let p = mk_equation env ctxt dummy Eq (mkVar i) d in i,Defined,p | LocalDef (_,_,t) | LocalAssum (_,t) -> let t = EConstr.Unsafe.to_constr t in @@ -1012,7 +1012,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (fun id -> match Id.Map.find id reified_hyps with | Defined,p -> - reified_of_proposition env p, mk_refl (Term.mkVar id) + reified_of_proposition env p, mk_refl (mkVar id) | Assumed,p -> reified_of_proposition env (maximize_prop useful_equa_ids p), EConstr.mkVar id diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 9f02388c39..150c253a7a 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -13,6 +13,7 @@ open Ltac_plugin open CErrors open Util open Term +open Constr open Tacmach open Proof_search open Context.Named.Declaration @@ -82,7 +83,7 @@ let make_atom atom_env term= let term = EConstr.Unsafe.to_constr term in try let (_,i)= - List.find (fun (t,_)-> eq_constr term t) atom_env.env + List.find (fun (t,_)-> Constr.equal term t) atom_env.env in Atom i with Not_found -> let i=atom_env.next in diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index bec18f6df8..b2285a4a11 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -10,7 +10,7 @@ type atom_env= {mutable next:int; - mutable env:(Term.constr*int) list} + mutable env:(Constr.t*int) list} val make_form : atom_env -> Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 447acb9057..8e4d8b0d34 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -41,9 +41,12 @@ Ltac Ss_to_add f acc := | _ => constr:((acc + f)%nat) end. +(* For internal use only *) +Local Definition protected_to_nat := N.to_nat. + Ltac natprering := match goal with - |- context C [S ?p] => + |- context C [S ?p] => match p with O => fail 1 (* avoid replacing 1 with 1+0 ! *) | p => match isnatcst p with @@ -52,9 +55,19 @@ Ltac natprering := fold v; natprering end end - | _ => idtac + | _ => change N.to_nat with protected_to_nat + end. + +Ltac natpostring := + match goal with + | |- context [N.to_nat ?x] => + let v := eval cbv in (N.to_nat x) in + change (N.to_nat x) with v; + natpostring + | _ => change protected_to_nat with N.to_nat end. Add Ring natr : natSRth - (morphism nat_morph_N, constants [natcst], preprocess [natprering]). + (morphism nat_morph_N, constants [natcst], + preprocess [natprering], postprocess [natpostring]). diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 05ab8ab326..a7d6d5bb20 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) ) !from_name ] END @@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) ) !field_from_name ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b8fae2494f..e3e749b754 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -10,7 +10,7 @@ open Ltac_plugin open Pp open Util open Names -open Term +open Constr open EConstr open Vars open CClosure @@ -58,13 +58,13 @@ let rec mk_clos_but f_map subs t = match f_map (global_of_constr_nofail t) with | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> - (match kind_of_term t with + (match Constr.kind t with App(f,args) -> mk_clos_app_but f_map subs f args 0 | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t | _ -> mk_atom t) and mk_clos_app_but f_map subs f args n = - let open Term in + let open Constr in if n >= Array.length args then mk_atom(mkApp(f, args)) else let fargs, args' = Array.chop n args in @@ -150,13 +150,14 @@ let ic_unsafe c = (*FIXME remove *) let sigma = Evd.from_env env in EConstr.of_constr (fst (Constrintern.interp_constr env sigma c)) -let decl_constant na ctx c = - let open Term in - let vars = Univops.universes_of_constr c in - let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in +let decl_constant na univs c = + let open Constr in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in + let univs = Univops.restrict_universe_context univs vars in + let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true - ~univs:(Univ.ContextSet.to_context ctx) c), + (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) (* Calling a global tactic *) @@ -220,7 +221,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) + Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -344,13 +345,7 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -let pr_constr c = pr_econstr c - -module M = struct - type t = Term.constr - let compare = Term.compare -end -module Cmap = Map.Make(M) +module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" @@ -372,7 +367,7 @@ let find_ring_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) | [] -> assert false let add_entry (sp,_kn) e = @@ -395,7 +390,7 @@ let subst_th (subst,th) = let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && - Term.eq_constr set' th.ring_setoid && + Constr.equal set' th.ring_setoid && ext' == th.ring_ext && morph' == th.ring_morph && th' == th.ring_th && @@ -533,19 +528,19 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ + str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); + pr_econstr_env env !evd mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) @@ -865,7 +860,7 @@ let find_field_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) | [] -> assert false let add_field_entry (sp,_kn) e = @@ -933,7 +928,7 @@ let field_equality evd r inv req = inv_m_lem let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = - let open Term in + let open Constr in check_required_library (cdir@["Field_tac"]); let (sigma,fth) = ic fth in let env = Global.env() in diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index d37582bd79..c26fcc8d1f 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Libnames open Constrexpr open Tacexpr diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f7e0a5d936..8493dbdbb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -12,6 +12,7 @@ open Util open Names open Evd open Term +open Constr open Termops open Printer open Locusops @@ -239,7 +240,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c)); + ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); (sigma, (sigma, c)) @@ -465,7 +466,6 @@ let ssrevaltac ist gtac = (* but stripping global ones. We use the variable names to encode the *) (* the number of dependencies, so that the transformation is reversible. *) -open Term let env_size env = List.length (Environ.named_context env) let pf_concl gl = EConstr.Unsafe.to_constr (pf_concl gl) @@ -491,23 +491,23 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in nf_evar sigma t in - let rec put evlist c = match kind_of_term c with + let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else let n = max 0 (Array.length a - nenv) in let t = abs_evar n k in (k, (n, t)) :: put evlist t - | _ -> fold_constr put evlist c in + | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, EConstr.of_constr c0,[], ucst else let rec lookup k i = function | [] -> 0, 0 | (k', (n, _)) :: evl -> if k = k' then i, n else lookup k (i + 1) evl in - let rec get i c = match kind_of_term c with + let rec get i c = match Constr.kind c with | Evar (ev, a) -> let j, n = lookup ev i evlist in - if j = 0 then map_constr (get i) c else if n = 0 then mkRel j else + if j = 0 then Constr.map (get i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k))) - | _ -> map_constr_with_binders ((+) 1) get i c in + | _ -> Constr.map_with_binders ((+) 1) get i c in let rec loop c i = function | (_, (n, t)) :: evl -> loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl @@ -539,7 +539,7 @@ module Intset = Evar.Set let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); - pp(lazy(str"c0= " ++ Printer.pr_constr c0)); + pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0)); let sigma0 = project gl in let c0 = nf_evar sigma0 (nf_evar sigma c0) in let nenv = env_size (pf_env gl) in @@ -551,7 +551,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in nf_evar sigma0 (nf_evar sigma t) in - let rec put evlist c = match kind_of_term c with + let rec put evlist c = match Constr.kind c with | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else let n = max 0 (Array.length a - nenv) in @@ -560,12 +560,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) = (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t - | _ -> fold_constr put evlist c in + | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") - (fun (k,_) -> str(Evd.string_of_existential k)) evlist)); + (fun (k,_) -> Evar.print k) evlist)); let evplist = let depev = List.fold_left (fun evs (_,(_,t,_)) -> let t = EConstr.of_constr t in @@ -588,17 +588,17 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec lookup k i = function | [] -> 0, 0 | (k', (n,_,_)) :: evl -> if k = k' then i,n else lookup k (i + 1) evl in - let rec get evlist i c = match kind_of_term c with + let rec get evlist i c = match Constr.kind c with | Evar (ev, a) -> let j, n = lookup ev i evlist in - if j = 0 then map_constr (get evlist i) c else if n = 0 then mkRel j else + if j = 0 then Constr.map (get evlist i) c else if n = 0 then mkRel j else mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k))) - | _ -> map_constr_with_binders ((+) 1) (get evlist) i c in + | _ -> Constr.map_with_binders ((+) 1) (get evlist) i c in let rec app extra_args i c = match decompose_app c with | hd, args when isRel hd && destRel hd = i -> let j = destRel hd in mkApp (mkRel j, Array.of_list (List.map (Vars.lift (i-1)) extra_args @ args)) - | _ -> map_constr_with_binders ((+) 1) (app extra_args) i c in + | _ -> Constr.map_with_binders ((+) 1) (app extra_args) i c in let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in @@ -645,7 +645,7 @@ let pf_abs_cterm gl n c0 = let c0 = EConstr.Unsafe.to_constr c0 in let noargs = [|0|] in let eva = Array.make n noargs in - let rec strip i c = match kind_of_term c with + let rec strip i c = match Constr.kind c with | App (f, a) when isRel f -> let j = i - destRel f in if j >= n || eva.(j) = noargs then mkApp (f, Array.map (strip i) a) else @@ -653,8 +653,8 @@ let pf_abs_cterm gl n c0 = let nd = Array.length dp - 1 in let mkarg k = strip i a.(if k < nd then dp.(k + 1) - j else k + dp.(0)) in mkApp (f, Array.init (Array.length a - dp.(0)) mkarg) - | _ -> map_constr_with_binders ((+) 1) strip i c in - let rec strip_ndeps j i c = match kind_of_term c with + | _ -> Constr.map_with_binders ((+) 1) strip i c in + let rec strip_ndeps j i c = match Constr.kind c with | Prod (x, t, c1) when i < j -> let dl, c2 = strip_ndeps j (i + 1) c1 in if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else @@ -665,7 +665,7 @@ let pf_abs_cterm gl n c0 = if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else i :: dl, mkLetIn (x, strip i b, strip i t, c2) | _ -> [], strip i c in - let rec strip_evars i c = match kind_of_term c with + let rec strip_evars i c = match Constr.kind c with | Lambda (x, t1, c1) when i < n -> let na = nb_evar_deps x in let dl, t2 = strip_ndeps (i + na) i t1 in @@ -760,7 +760,7 @@ let clear_with_wilds wilds clr0 gl = let id = NamedDecl.get_id nd in if List.mem id clr || not (List.mem id wilds) then clr else let vars = Termops.global_vars_set_of_decl (pf_env gl) (project gl) nd in - let occurs id' = Idset.mem id' vars in + let occurs id' = Id.Set.mem id' vars in if List.exists occurs clr then id :: clr else clr in Proofview.V82.of_tactic (Tactics.clear (Context.Named.fold_inside extend_clr ~init:clr0 (Tacmach.pf_hyps gl))) gl @@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in - pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); + pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = @@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = compose_lam (let xs,y = List.chop (n-1) l in y @ xs) (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) in - pp(lazy(str"after: " ++ Printer.pr_constr oc)); + pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error @@ -1203,7 +1203,7 @@ let genclrtac cl cs clr = let gentac ist gen gl = (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr c)); + ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 2eadd5f26c..c399451941 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -190,7 +190,7 @@ val pf_merge_uc_of : val constr_name : evar_map -> EConstr.t -> Name.t val pf_type_of : Goal.goal Evd.sigma -> - Term.constr -> Goal.goal Evd.sigma * Term.types + Constr.constr -> Goal.goal Evd.sigma * Constr.types val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types @@ -220,7 +220,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : Globnames.global_reference -> Goal.goal Evd.sigma -> - Term.constr * Goal.goal Evd.sigma + Constr.constr * Goal.goal Evd.sigma val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t @@ -232,7 +232,7 @@ val new_tmp_id : val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Goal.goal Evd.sigma -> - evar_map * Term.constr -> int * Term.constr + evar_map * Constr.constr -> int * Constr.constr val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 26b5c57675..4e0b44a44d 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma = if not (EConstr.eq_constr sigma t t') then loop ctx t' else errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ - str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in + str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in let n_elim_args = Context.Rel.nhyps ctx in let is_rec_elim = @@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr c)); + ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr | Some (c, _, _,gl) -> true, gl | None -> errorstrm Pp.(str"Unable to apply the eliminator to the term"++ - spc()++pr_econstr c++spc()++str"or to unify it's type with"++ - pr_econstr inf_arg_ty) in + spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++ + pr_econstr_env env (project gl) inf_arg_ty) in ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 95ca6f49ad..bd9633afbd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -11,13 +11,14 @@ open Ltac_plugin open Util open Names +open Term +open Constr open Vars open Locus open Printer open Globnames open Termops open Tacinterp -open Term open Ssrmatching_plugin open Ssrmatching @@ -76,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -85,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term ist gl t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -108,7 +109,7 @@ let congrtac ((n, t), ty) ist gl = let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -246,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)), + ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -266,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl = | Proj _ when same_proj sigma0 c t -> body env t c | Const f -> aux (body env c c) | App (f, a) -> aux (EConstr.mkApp (body env f f, a)) - | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++ - str" contains no " ++ pr_econstr t ++ str" even after unfolding") + | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++ + str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding") in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c) else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in @@ -316,7 +317,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* such a generic Leibnitz equation -- short of inspecting the type *) (* of the elimination lemmas. *) -let rec strip_prod_assum c = match Term.kind_of_term c with +let rec strip_prod_assum c = match Constr.kind c with | Prod (_, _, c') -> strip_prod_assum c' | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c) | Cast (c', _, _) -> strip_prod_assum c' @@ -341,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = Term.destConst elim in + let elim, _ = destConst elim in let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in @@ -351,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* We check the proof is well typed *) let sigma, proof_ty = try Typing.type_of env sigma proof with _ -> raise PRtype_error in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl with _ -> @@ -373,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) | _ -> anomaly "rewrite rule not an application" in - errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++ - (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty)) + errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++ + (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; let is_construct_ref sigma c r = @@ -390,12 +391,12 @@ let rwcltac cl rdx dir sr gl = let gl = pf_unsafe_merge_uc ucst gl in let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr))); + ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty)); + ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in @@ -410,7 +411,7 @@ let rwcltac cl rdx dir sr gl = let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) - ++ str " to " ++ pr_econstr r2) in + ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in @@ -604,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in - let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in Feedback.msg_info Pp.(str"BEGIN INSTANCES"); try while true do diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index d01bdc1b9e..5c1b399a80 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,11 +8,12 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Pp open Names +open Constr open Tacmach open Ssrmatching_plugin.Ssrmatching - open Ssrprinters open Ssrcommon open Ssrtacticals @@ -30,9 +31,6 @@ let ssrposetac ist (id, (_, t)) gl = let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) -open Pp -open Term - let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in @@ -59,10 +57,10 @@ let rec is_Evar_or_CastedMeta sigma x = (EConstr.isCast sigma x && is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x))) let occur_existential_or_casted_meta c = - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Not_found | Cast (m,_,_) when isMeta m -> raise Not_found - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Not_found -> true open Printer @@ -71,29 +69,30 @@ let examine_abstract id gl = let gl, tid = pfe_type_of gl id in let abstract, gl = pf_mkSsrConst "abstract" gl in let sigma = project gl in + let env = pf_env gl in if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then - errorstrm(strbrk"not an abstract constant: "++pr_econstr id); + errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id); let _, args_id = EConstr.destApp sigma tid in if Array.length args_id <> 3 then - errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id); + errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id); if not (is_Evar_or_CastedMeta sigma args_id.(2)) then - errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used"); + errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used"); tid, args_id let pf_find_abstract_proof check_lock gl abstract_n = let fire gl t = EConstr.Unsafe.to_constr (Reductionops.nf_evar (project gl) (EConstr.of_constr t)) in let abstract, gl = pf_mkSsrConst "abstract" gl in let l = Evd.fold_undefined (fun e ei l -> - match kind_of_term ei.Evd.evar_concl with + match Constr.kind ei.Evd.evar_concl with | App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta (fire gl ty) && is_Evar_or_CastedMeta (project gl) (EConstr.of_constr @@ fire gl lock))) && - Term.eq_constr hd (EConstr.Unsafe.to_constr abstract) && Term.eq_constr n abstract_n -> e::l + Constr.equal hd (EConstr.Unsafe.to_constr abstract) && Constr.equal n abstract_n -> e::l | _ -> l) (project gl) [] in match l with | [e] -> e - | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++ strbrk" not found in the evar map exactly once. "++ strbrk"Did you tamper with it?") @@ -204,7 +203,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -270,7 +269,7 @@ let ssrabstract ist gens (*last*) gl = let gl, proof = let pf_unify_HO gl a b = try pf_unify_HO gl a b - with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++ + with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++ strbrk" cannot abstract this goal. Did you generalize it?") in let find_hole p t = match EConstr.kind (project gl) t with @@ -286,10 +285,10 @@ let ssrabstract ist gens (*last*) gl = let p = mkApp (proj2,[|ty;concl;p|]) in let concl = mkApp(prod,[|ty; concl|]) in pf_unify_HO gl concl t, p - | App(hd, [|left; right|]) when Term.eq_constr hd prod -> + | App(hd, [|left; right|]) when Term.Constr.equal hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) - | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++ strbrk" has an unexpected shape. Did you tamper with it?") in find_hole @@ -360,14 +359,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Sort _, [] -> EConstr.Vars.subst_vars s ct | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) - | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function | [] -> c | t::ts as args -> match EConstr.kind sigma c with | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args) - | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac ~ist pats in let tacigens = @@ -395,8 +394,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Some id -> if pats = [] then Tacticals.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++pr_econstr ct)); + ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); + ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); Tacticals.tclTHENS (basecuttac "ssr_have" ct) [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in "ssr_have", diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 023778fdbf..6c325cce43 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl = (* Utils of local interest only *) let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in - ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in + ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in let protectC, gl = pf_mkSsrConst "protect_term" gl in let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in let eq = EConstr.of_constr eq in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7b591feada..46403aef3c 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function | (fk, h), (_, (_, Some c)) -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | (fk, h), (_, (c, None)) -> - pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) + pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706d..4b2fab6d19 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs let pp_term gl t = - let t = Reductionops.nf_evar (project gl) t in pr_econstr t + let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t (* FIXME *) (* terms are pre constr, the kind is parsing/printing flag to distinguish diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 507b4631b0..4f530a0aec 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -9,7 +9,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Names -open Term +module CoqConstr = Constr +open CoqConstr open Termops open Constrexpr open Constrexpr_ops @@ -73,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -85,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> @@ -157,11 +158,14 @@ let declare_one_prenex_implicit locality f = | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] -VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF | [ "Prenex" "Implicits" ne_global_list(fl) ] - -> [ let locality = - Locality.make_section_locality (Locality.LocalityFixme.consume ()) in - List.iter (declare_one_prenex_implicit locality) fl ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + let locality = Locality.make_section_locality atts.locality in + List.iter (declare_one_prenex_implicit locality) fl; + st + ] END (* Vernac grammar visibility patch *) @@ -342,7 +346,7 @@ let coerce_search_pattern_to_sort hpat = let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern hpat') in + pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = try @@ -358,13 +362,13 @@ let coerce_search_pattern_to_sort hpat = let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () + errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path let interp_head_pat hpat = let filter_head, p = coerce_search_pattern_to_sort hpat in - let rec loop c = match kind_of_term c with + let rec loop c = match CoqConstr.kind c with | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' @@ -467,10 +471,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref c = match DAst.get c with +let pr_rawhintref c = + let _, env = Pfedit.get_current_context () in + match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr c + pr_glob_constr_env env f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c @@ -545,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d )) + Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), + ((Loc.tag s),None),(d ))) ]]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 50fe94f7c9..d6dbad7a95 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -18,10 +18,13 @@ let frozen_lexer = CLexer.get_keyword_state () ;; open Ltac_plugin open Names open Pp -open Pcoq open Genarg open Stdarg open Term +module CoqConstr = Constr +open CoqConstr +open Pcoq +open Pcoq.Constr open Vars open Libnames open Tactics @@ -35,10 +38,8 @@ open Evd open Tacexpr open Tacinterp open Pretyping -open Constr open Ppconstr open Printer - open Globnames open Misctypes open Decl_kinds @@ -73,7 +74,7 @@ let pp s = !pp_ref s (** Utils {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = - match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] + match kind c with App (f, a) -> f, a | _ -> c, [| |] (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -99,7 +100,6 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr @@ -325,7 +325,7 @@ let unif_FO env ise p c = let nf_open_term sigma0 ise c = let c = EConstr.Unsafe.to_constr c in let s = ise and s' = ref sigma0 in - let rec nf c' = match kind_of_term c' with + let rec nf c' = match kind c' with | Evar ex -> begin try nf (existential_value s ex) with _ -> let k, a = ex in let a' = Array.map nf a in @@ -333,7 +333,7 @@ let nf_open_term sigma0 ise c = s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); mkEvar (k, a') end - | _ -> map_constr nf c' in + | _ -> map nf c' in let copy_def k evi () = if evar_body evi != Evd.Evar_empty then () else match Evd.evar_body (Evd.find s k) with @@ -365,7 +365,7 @@ let pf_unify_HO gl t1 t2 = re_sig si sigma (* This is what the definition of iter_constr should be... *) -let iter_constr_LR f c = match kind_of_term c with +let iter_constr_LR f c = match kind c with | Evar (k, a) -> Array.iter f a | Cast (cc, _, t) -> f cc; f t | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b @@ -396,7 +396,7 @@ let inv_dir = function L2R -> R2L | R2L -> L2R type pattern_class = | KpatFixed | KpatConst - | KpatEvar of existential_key + | KpatEvar of Evar.t | KpatLet | KpatLam | KpatRigid @@ -418,26 +418,27 @@ let all_ok _ _ = true let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 -let isRigid c = match kind_of_term c with +let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = - if isEvar c then hole_var else map_constr wipe_evar c in - pr_constr (wipe_evar c0) + if isEvar c then hole_var else map wipe_evar c in + let sigma, env = Pfedit.get_current_context () in + pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = let ise = ref ise0 in let sigma = ref ise0 in let nenv = env_size env + if hack then 1 else 0 in - let rec put c = match kind_of_term c with + let rec put c = match kind c with | Evar (k, a as ex) -> begin try put (existential_value !sigma ex) with NotInstantiatedEvar -> - if Evd.mem sigma0 k then map_constr put c else + if Evd.mem sigma0 k then map put c else let evi = Evd.find !sigma k in let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in let abs_dc (d, c) = function @@ -452,7 +453,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = sigma := Evd.define k (applistc (mkMeta m) a) !sigma; put (existential_value !sigma ex) end - | _ -> map_constr put c in + | _ -> map put c in let c1 = put c0 in !ise, c1 (* Compile a match pattern from a term; t is the term to fill. *) @@ -462,7 +463,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in - match kind_of_term f with + match kind f with | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else @@ -490,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = (* kind and arity for Proj and Flex patterns. *) let ungen_upat lhs (sigma, uc, t) u = let f, a = safeDestApp lhs in - let k = match kind_of_term f with + let k = match kind f with | Var _ | Ind _ | Construct _ -> KpatFixed | Const _ -> KpatConst | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k @@ -502,14 +503,14 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in - let nargs_of_proj t = match kind_of_term t with + let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be the number of arguments including the projected *) | _ -> assert false in - try match kind_of_term f with + try match kind f with | Prod _ -> na Prod_cs - | Sort s -> na (Sort_cs (family_of_sort s)) + | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) @@ -517,22 +518,22 @@ let nb_cs_proj_args pc f u = with Not_found -> -1 let isEvar_k k f = - match kind_of_term f with Evar (k', _) -> k = k' | _ -> false + match kind f with Evar (k', _) -> k = k' | _ -> false let nb_args c = - match kind_of_term c with App (_, a) -> Array.length a | _ -> 0 + match kind c with App (_, a) -> Array.length a | _ -> 0 let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a) let splay_app ise = - let rec loop c a = match kind_of_term c with + let rec loop c a = match kind c with | App (f, a') -> loop f (Array.append a' a) | Cast (c', _, _) -> loop c' a | Evar ex -> (try loop (existential_value ise ex) a with _ -> c, a) | _ -> c, a in - fun c -> match kind_of_term c with + fun c -> match kind c with | App (f, a) -> loop f a | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] @@ -541,8 +542,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when Term.eq_constr u.up_f f -> na - | KpatFixed when Term.eq_constr u.up_f f -> na + | KpatConst when equal u.up_f f -> na + | KpatFixed when equal u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -554,7 +555,7 @@ let filter_upat i0 f n u fpats = if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats -let eq_prim_proj c t = match kind_of_term t with +let eq_prim_proj c t = match kind t with | Proj(p,_) -> Constant.equal (Projection.constant p) c | _ -> false @@ -562,13 +563,13 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> Term.eq_constr u.up_f f - | KpatFixed -> Term.eq_constr u.up_f f + | KpatConst -> equal u.up_f f + | KpatFixed -> equal u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f | KpatRigid -> isRigid f - | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f + | KpatProj pc -> equal f (mkConst pc) || eq_prim_proj pc f | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats @@ -741,13 +742,13 @@ let mk_tpattern_matcher ?(all_instances=false) let x, pv, t, pb = destLetIn u.up_f in let env' = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in - let match_let f = match kind_of_term f with + let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> Term.eq_constr u.up_f - | KpatConst -> Term.eq_constr u.up_f + | KpatFixed -> equal u.up_f + | KpatConst -> equal u.up_f | KpatLam -> fun c -> - (match kind_of_term c with + (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c | _ -> false) | _ -> unif_EQ env sigma u.up_f in @@ -778,8 +779,8 @@ let rec uniquize = function let t1 = nf_evar sigma1 t1 in let f1 = nf_evar sigma1 f1 in let a1 = Array.map (nf_evar sigma1) a1 in - not (Term.eq_constr t t1 && - Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + not (equal t t1 && + equal f f1 && CArray.for_all2 equal a a1) in x :: uniquize (List.filter neq xs) in ((fun env c h ~k -> @@ -1018,7 +1019,7 @@ let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind let interp_ssrterm _ gl t = Tacmach.project gl, t @@ -1100,7 +1101,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let decodeG t f g = decode ist (mkG t) f g in let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in let cleanup_XinE h x rp sigma = - let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in + let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) let ctx = pf_hyps gl in let len = Context.Named.length ctx in @@ -1115,11 +1116,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = with Not_found -> ref (Some x), fun _ -> () in let sigma0 = project gl in let new_evars = - let rec aux acc t = match kind_of_term t with + let rec aux acc t = match kind t with | Evar (k,_) -> if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else (update k; k::acc) - | _ -> fold_constr aux acc t in + | _ -> CoqConstr.fold aux acc t in aux [] (nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> @@ -1202,7 +1203,7 @@ let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;; let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;; let id_of_pattern = function - | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None) + | _, T t -> (match kind t with Var id -> Some id | _ -> None) | _ -> None (* The full occurrence set *) @@ -1214,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c - | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in @@ -1222,7 +1223,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in sigma, e_body in let ex_value hole = - match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in + match kind hole with Evar (e,_) -> e | _ -> assert false in let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in @@ -1414,7 +1415,7 @@ let () = let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in -(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) +(* not (equal lhs (Evarutil.nf_evar ise rhs)) in *) let env, sigma, concl = pf_env gl, project gl, pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma0, cpat = interp_cpattern ist gl arg None in @@ -1423,7 +1424,8 @@ let ssrinstancesof ist arg gl = let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8e2a1a7176..8ab666f7ea 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -6,7 +6,7 @@ open Genarg open Tacexpr open Environ open Evd -open Term +open Constr (** ******** Small Scale Reflection pattern matching facilities ************* *) |