diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
88 files changed, 785 insertions, 946 deletions
@@ -337,13 +337,11 @@ kernel/indtypes.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx lib/options.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/typeops.cmx lib/util.cmx kernel/indtypes.cmi kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ - kernel/instantiate.cmi kernel/names.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ - kernel/inductive.cmi + kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/inductive.cmi kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ - kernel/instantiate.cmx kernel/names.cmx kernel/reduction.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ - kernel/inductive.cmi + kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/inductive.cmi kernel/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/instantiate.cmi @@ -461,13 +459,13 @@ library/goptions.cmx: library/global.cmx library/lib.cmx \ library/impargs.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/evd.cmi library/global.cmi kernel/inductive.cmi library/lib.cmi \ library/libobject.cmi kernel/names.cmi kernel/reduction.cmi \ - kernel/sign.cmi library/summary.cmi kernel/term.cmi kernel/typeops.cmi \ - lib/util.cmi library/impargs.cmi + library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ + library/impargs.cmi library/impargs.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/evd.cmx library/global.cmx kernel/inductive.cmx library/lib.cmx \ library/libobject.cmx kernel/names.cmx kernel/reduction.cmx \ - kernel/sign.cmx library/summary.cmx kernel/term.cmx kernel/typeops.cmx \ - lib/util.cmx library/impargs.cmi + library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ + library/impargs.cmi library/indrec.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/indtypes.cmi kernel/inductive.cmi kernel/instantiate.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ @@ -1005,25 +1003,25 @@ tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \ pretyping/evarutil.cmi kernel/evd.cmi lib/explore.cmi proofs/logic.cmi \ kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \ - kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi lib/util.cmi + proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi lib/util.cmi tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \ pretyping/evarutil.cmx kernel/evd.cmx lib/explore.cmx proofs/logic.cmx \ kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \ - kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx lib/util.cmx -tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi tactics/hiddentac.cmi \ - tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi lib/util.cmi tactics/elim.cmi -tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx tactics/hiddentac.cmx \ - tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx kernel/reduction.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx lib/util.cmx tactics/elim.cmi + kernel/term.cmx lib/util.cmx +tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \ + tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi lib/util.cmi tactics/elim.cmi +tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx kernel/environ.cmx \ + tactics/hiddentac.cmx tactics/hipattern.cmx kernel/inductive.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx lib/util.cmx tactics/elim.cmi tactics/eqdecide.cmo: tactics/auto.cmi parsing/coqlib.cmi \ tactics/equality.cmi library/global.cmi tactics/hiddentac.cmi \ tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \ @@ -1568,9 +1566,9 @@ contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \ toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ contrib/correctness/psyntax.cmi -contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \ - kernel/evd.cmi library/global.cmi kernel/names.cmi lib/options.cmi \ - contrib/correctness/past.cmi pretyping/pattern.cmi \ +contrib/correctness/ptactic.cmo: library/declare.cmi kernel/environ.cmi \ + tactics/equality.cmi kernel/evd.cmi library/global.cmi kernel/names.cmi \ + lib/options.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \ contrib/correctness/pcic.cmi contrib/correctness/pdb.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ contrib/correctness/perror.cmi proofs/pfedit.cmi \ @@ -1583,9 +1581,9 @@ contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ contrib/correctness/ptactic.cmi -contrib/correctness/ptactic.cmx: library/declare.cmx tactics/equality.cmx \ - kernel/evd.cmx library/global.cmx kernel/names.cmx lib/options.cmx \ - contrib/correctness/past.cmi pretyping/pattern.cmx \ +contrib/correctness/ptactic.cmx: library/declare.cmx kernel/environ.cmx \ + tactics/equality.cmx kernel/evd.cmx library/global.cmx kernel/names.cmx \ + lib/options.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \ contrib/correctness/pcic.cmx contrib/correctness/pdb.cmx \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ contrib/correctness/perror.cmx proofs/pfedit.cmx \ @@ -1618,28 +1616,30 @@ contrib/correctness/ptyping.cmx: parsing/ast.cmx parsing/astterm.cmx \ contrib/correctness/ptype.cmi contrib/correctness/putil.cmx \ kernel/reduction.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ contrib/correctness/ptyping.cmi -contrib/correctness/putil.cmo: parsing/coqlib.cmi kernel/names.cmi \ - contrib/correctness/past.cmi pretyping/pattern.cmi \ - contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/prename.cmi \ - parsing/printer.cmi contrib/correctness/ptype.cmi kernel/term.cmi \ - lib/util.cmi contrib/correctness/putil.cmi -contrib/correctness/putil.cmx: parsing/coqlib.cmx kernel/names.cmx \ - contrib/correctness/past.cmi pretyping/pattern.cmx \ - contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/prename.cmx \ - parsing/printer.cmx contrib/correctness/ptype.cmi kernel/term.cmx \ - lib/util.cmx contrib/correctness/putil.cmi -contrib/correctness/pwp.cmo: kernel/evd.cmi library/global.cmi \ - kernel/names.cmi contrib/correctness/past.cmi \ +contrib/correctness/putil.cmo: parsing/coqlib.cmi kernel/environ.cmi \ + library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \ + pretyping/pattern.cmi contrib/correctness/peffect.cmi \ + contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \ + contrib/correctness/prename.cmi parsing/printer.cmi \ + contrib/correctness/ptype.cmi kernel/term.cmi lib/util.cmi \ + contrib/correctness/putil.cmi +contrib/correctness/putil.cmx: parsing/coqlib.cmx kernel/environ.cmx \ + library/global.cmx kernel/names.cmx contrib/correctness/past.cmi \ + pretyping/pattern.cmx contrib/correctness/peffect.cmx \ + contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx lib/pp.cmx \ + contrib/correctness/prename.cmx parsing/printer.cmx \ + contrib/correctness/ptype.cmi kernel/term.cmx lib/util.cmx \ + contrib/correctness/putil.cmi +contrib/correctness/pwp.cmo: kernel/environ.cmi kernel/evd.cmi \ + library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi \ contrib/correctness/pmonad.cmi contrib/correctness/prename.cmi \ contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \ contrib/correctness/putil.cmi kernel/reduction.cmi kernel/term.cmi \ lib/util.cmi contrib/correctness/pwp.cmi -contrib/correctness/pwp.cmx: kernel/evd.cmx library/global.cmx \ - kernel/names.cmx contrib/correctness/past.cmi \ +contrib/correctness/pwp.cmx: kernel/environ.cmx kernel/evd.cmx \ + library/global.cmx kernel/names.cmx contrib/correctness/past.cmi \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx \ contrib/correctness/pmonad.cmx contrib/correctness/prename.cmx \ diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index c885242bd..936c39d56 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -146,8 +146,8 @@ let coq_constant d s = make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI let bool_sp = coq_constant ["Init"; "Datatypes"] "bool" -let coq_true = mkMutConstruct (((bool_sp,0),1), [||]) -let coq_false = mkMutConstruct (((bool_sp,0),2), [||]) +let coq_true = mkMutConstruct ((bool_sp,0),1) +let coq_false = mkMutConstruct ((bool_sp,0),2) let constant s = let id = id_of_string s in diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index 6a7a70cf3..d4c3494a8 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -122,6 +122,7 @@ let eq_pattern = let (loop_ids : tactic) = fun gl -> let rec arec hyps gl = + let env = pf_env gl in let concl = pf_concl gl in match hyps with | [] -> tclIDTAC gl @@ -135,7 +136,7 @@ let (loop_ids : tactic) = fun gl -> match pf_matches gl eq_pattern (body_of_type a) with | [_; _,varphi; _] when isVar varphi -> let phi = destVar varphi in - if occur_var phi concl then + if Environ.occur_var env phi concl then tclTHEN (rewriteLR (mkVar id)) (arec al) gl else arec al gl diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml index 29caf3107..de5d2da7d 100644 --- a/contrib/correctness/ptyping.ml +++ b/contrib/correctness/ptyping.ml @@ -107,10 +107,10 @@ let effect_app ren env f args = * Also returns its variables *) let state_coq_ast sign a = + let env = Global.env_of_context sign in let j = - let env = Global.env_of_context sign in reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in - let ids = global_vars j.uj_val in + let ids = global_vars env j.uj_val in j.uj_val, j.uj_type, ids (* [is_pure p] tests wether the program p is an expression or not. *) diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index e227a4459..73d1778ac 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -14,6 +14,7 @@ open Util open Names open Term open Pattern +open Environ open Pmisc open Ptype @@ -61,10 +62,10 @@ let is_mutable_in_env env id = let now_vars env c = Util.map_succeed (function id -> if is_mutable_in_env env id then id else failwith "caught") - (global_vars c) + (global_vars (Global.env()) c) let make_before_after c = - let ids = global_vars c in + let ids = global_vars (Global.env()) c in let al = Util.map_succeed (function id -> @@ -98,18 +99,18 @@ let make_assoc_list ren env on_prime ids = [] ids let apply_pre ren env c = - let ids = global_vars c.p_value in + let ids = global_vars (Global.env()) c.p_value in let al = make_assoc_list ren env current_var ids in { p_assert = c.p_assert; p_name = c.p_name; p_value = subst_in_constr al c.p_value } let apply_assert ren env c = - let ids = global_vars c.a_value in + let ids = global_vars (Global.env()) c.a_value in let al = make_assoc_list ren env current_var ids in { a_name = c.a_name; a_value = subst_in_constr al c.a_value } let apply_post ren env before c = - let ids = global_vars c.a_value in + let ids = global_vars (Global.env()) c.a_value in let al = make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in { a_name = c.a_name; a_value = subst_in_constr al c.a_value } diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml index b00f5c38f..1381bdf92 100644 --- a/contrib/correctness/pwp.ml +++ b/contrib/correctness/pwp.ml @@ -13,6 +13,7 @@ open Util open Names open Term +open Environ open Pmisc open Ptype @@ -53,7 +54,7 @@ let update_post env top ef c = l else l) - [] (global_vars c) + [] (global_vars (Global.env()) c) in subst_in_constr al c @@ -110,7 +111,7 @@ let create_bool_post c = let is_bool = function | TypePure c -> (match kind_of_term (strip_outer_cast c) with - | IsMutInd (op,_) -> Global.string_of_global (IndRef op) = "bool" + | IsMutInd op -> Global.string_of_global (IndRef op) = "bool" | _ -> false) | _ -> false diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index cd6160b2a..93e8d4cf5 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -138,9 +138,9 @@ let _ = let c = Astterm.interp_constr Evd.empty (Global.env()) ast in match kind_of_term c with (* If it is a global reference, then output the declaration *) - | IsConst (sp,_) -> extract_reference (ConstRef sp) - | IsMutInd (ind,_) -> extract_reference (IndRef ind) - | IsMutConstruct (cs,_) -> extract_reference (ConstructRef cs) + | IsConst sp -> extract_reference (ConstRef sp) + | IsMutInd ind -> extract_reference (IndRef ind) + | IsMutConstruct cs -> extract_reference (ConstructRef cs) (* Otherwise, output the ML type or expression *) | _ -> match extract_constr (Global.env()) [] c with diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 8f70b560f..f5b28598c 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -262,7 +262,7 @@ type inductive_extraction_result = | Iprop let inductive_extraction_table = - ref (Gmap.empty : (inductive_path, inductive_extraction_result) Gmap.t) + ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t) let add_inductive_extraction i e = inductive_extraction_table := Gmap.add i e !inductive_extraction_table @@ -274,7 +274,7 @@ type constructor_extraction_result = | Cprop let constructor_extraction_table = - ref (Gmap.empty : (constructor_path, constructor_extraction_result) Gmap.t) + ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t) let add_constructor_extraction c e = constructor_extraction_table := Gmap.add c e !constructor_extraction_table @@ -358,13 +358,13 @@ and extract_type_rec_info env c vl args = | None -> let id = id_of_name (fst (lookup_rel_type n env)) in Tmltype (Tvar id, [], vl)) - | IsConst (sp,a) when args = [] && is_ml_extraction (ConstRef sp) -> + | IsConst sp when args = [] && is_ml_extraction (ConstRef sp) -> Tmltype (Tglob (ConstRef sp), [], vl) - | IsConst (sp,a) when is_axiom sp -> + | IsConst sp when is_axiom sp -> let id = next_ident_away (basename sp) vl in Tmltype (Tvar id, [], id :: vl) - | IsConst (sp,a) -> - let t = constant_type env none (sp,a) in + | IsConst sp -> + let t = constant_type env none sp in if is_arity env none t then (match extract_constant sp with | Emltype (Miniml.Tarity,_,_) -> Tarity @@ -375,9 +375,9 @@ and extract_type_rec_info env c vl args = else (* We can't keep as ML type abbreviation a CIC constant *) (* which type is not an arity: we reduce this constant. *) - let cvalue = constant_value env (sp,a) in + let cvalue = constant_value env sp in extract_type_rec_info env (applist (cvalue, args)) vl [] - | IsMutInd (spi,_) -> + | IsMutInd spi -> (match extract_inductive spi with |Iml (si,vli) -> extract_type_app env (IndRef spi,si,vli) vl args @@ -520,11 +520,11 @@ and extract_term_info_with_type env ctx c t = extract_term_info env' (false :: ctx) c2) | IsRel n -> MLrel (renum_db ctx n) - | IsConst (sp,_) -> + | IsConst sp -> MLglob (ConstRef sp) | IsApp (f,a) -> extract_app env ctx f a - | IsMutConstruct (cp,_) -> + | IsMutConstruct cp -> abstract_constructor cp | IsMutCase ((_,(ip,_,_,_,_)),_,c,br) -> extract_case env ctx ip c br @@ -577,7 +577,7 @@ and abstract_constructor cp = (* Extraction of a case *) and extract_case env ctx ip c br = - let mis = Global.lookup_mind_specif (ip,[||]) in + let mis = Global.lookup_mind_specif ip in let ni = Array.map List.length (mis_recarg mis) in (* [ni]: number of arguments without parameters in each branch *) (* [br]: bodies of each branch (in functional form) *) @@ -756,7 +756,7 @@ and extract_constructor (((sp,_),_) as c) = and is_singleton_inductive (sp,_) = let mib = Global.lookup_mind sp in (mib.mind_ntypes = 1) && - let mis = build_mis ((sp,0),[||]) mib in + let mis = build_mis (sp,0) mib in (mis_nconstr mis = 1) && match extract_constructor ((sp,0),1) with | Cml ([mlt],_,_)-> (try parse_ml_type sp mlt; true with Found_sp -> false) @@ -775,7 +775,7 @@ and extract_mib sp = let genv = Global.env () in (* Everything concerning parameters. We do that first, since they are common to all the [mib]. *) - let mis = build_mis ((sp,0),[||]) mib in + let mis = build_mis (sp,0) mib in let nb = mis_nparams mis in let rb = mis_params_ctxt mis in let env = push_rels rb genv in @@ -789,7 +789,7 @@ and extract_mib sp = let vl0 = iterate_for 0 (mib.mind_ntypes - 1) (fun i vl -> let ip = (sp,i) in - let mis = build_mis (ip,[||]) mib in + let mis = build_mis ip mib in if (mis_sort mis) = (Prop Null) then begin add_inductive_extraction ip Iprop; vl end else begin @@ -808,7 +808,7 @@ and extract_mib sp = iterate_for 0 (mib.mind_ntypes - 1) (fun i vl -> let ip = (sp,i) in - let mis = build_mis (ip,[||]) mib in + let mis = build_mis ip mib in if mis_sort mis = Prop Null then begin for j = 1 to mis_nconstr mis do add_constructor_extraction (ip,j) Cprop @@ -832,7 +832,7 @@ and extract_mib sp = (* Third pass: we update the type variables list in the inductives table *) for i = 0 to mib.mind_ntypes-1 do let ip = (sp,i) in - let mis = build_mis (ip,[||]) mib in + let mis = build_mis ip mib in match lookup_inductive_extraction ip with | Iprop -> () | Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l)); @@ -840,7 +840,7 @@ and extract_mib sp = (* Fourth pass: we update also in the constructors table *) for i = 0 to mib.mind_ntypes-1 do let ip = (sp,i) in - let mis = build_mis (ip,[||]) mib in + let mis = build_mis ip mib in for j = 1 to mis_nconstr mis do let cp = (ip,j) in match lookup_constructor_extraction cp with @@ -880,7 +880,7 @@ and extract_inductive_declaration sp = iterate_for (1 - mib.mind_ntypes) 0 (fun i acc -> let ip = (sp,-i) in - let mis = build_mis (ip,[||]) mib in + let mis = build_mis ip mib in match lookup_inductive_extraction ip with | Iprop -> acc | Iml (_,vl) -> diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 49706bbd3..652a96910 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -76,7 +76,7 @@ let pf_parse_constr gl s = let rec string_of_constr c = match kind_of_term c with IsCast (c,t) -> string_of_constr c - |IsConst (c,l) -> string_of_path c + |IsConst c -> string_of_path c |IsVar(c) -> string_of_id c | _ -> "not_of_constant" ;; @@ -86,7 +86,7 @@ let rec rational_of_constr c = | IsCast (c,t) -> (rational_of_constr c) | IsApp (c,args) -> (match kind_of_term c with - IsConst (c,l) -> + IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.Ropp" -> rop (rational_of_constr args.(0)) @@ -106,7 +106,7 @@ let rec rational_of_constr c = (rational_of_constr args.(1)) | _ -> failwith "not a rational") | _ -> failwith "not a rational") - | IsConst (c,l) -> + | IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.R1" -> r1 |"Coq.Reals.Rdefinitions.R0" -> r0 @@ -120,7 +120,7 @@ let rec flin_of_constr c = | IsCast (c,t) -> (flin_of_constr c) | IsApp (c,args) -> (match kind_of_term c with - IsConst (c,l) -> + IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.Ropp" -> flin_emult (rop r1) (flin_of_constr args.(0)) @@ -152,7 +152,7 @@ let rec flin_of_constr c = (rinv b))) |_->assert false) |_ -> assert false) - | IsConst (c,l) -> + | IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.R1" -> flin_one () |"Coq.Reals.Rdefinitions.R0" -> flin_zero () @@ -187,7 +187,7 @@ let ineq1_of_constr (h,t) = let t1= args.(0) in let t2= args.(1) in (match kind_of_term f with - IsConst (c,l) -> + IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h; htype="Rlt"; @@ -218,13 +218,13 @@ let ineq1_of_constr (h,t) = (flin_of_constr t1); hstrict=false}] |_->assert false) - | IsMutInd ((sp,i),l) -> + | IsMutInd (sp,i) -> (match (string_of_path sp) with "Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in (match (kind_of_term t0) with - IsConst (c,l) -> + IsConst c -> (match (string_of_path c) with "Coq.Reals.Rdefinitions.R"-> [{hname=h; diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index aa158f841..50aebb917 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -737,7 +737,7 @@ let rec nsortrec vl x = | IsMutCase(_,x,t,a) -> nsortrec vl x | IsCast(x,t)-> nsortrec vl t - | IsConst((c,_)) -> nsortrec vl (lookup_constant c vl).const_type + | IsConst c -> nsortrec vl (lookup_constant c vl).const_type | _ -> nsortrec vl (type_of vl Evd.empty x) ;; let nsort x = diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index d56f92cfa..d12f868ac 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -177,9 +177,9 @@ let dest_const_apply t = let f,args = get_applist t in let ref = match kind_of_term f with - | IsConst (sp,_) -> ConstRef sp - | IsMutConstruct (csp,_) -> ConstructRef csp - | IsMutInd (isp,_) -> IndRef isp + | IsConst sp -> ConstRef sp + | IsMutConstruct csp -> ConstructRef csp + | IsMutInd isp -> IndRef isp | _ -> raise Destruct in basename (Global.sp_of_global ref), args @@ -193,12 +193,12 @@ type result = let destructurate t = let c, args = get_applist t in match kind_of_term c, args with - | IsConst (sp,_), args -> + | IsConst sp, args -> Kapp (string_of_id (basename (Global.sp_of_global (ConstRef sp))),args) - | IsMutConstruct (csp,_) , args -> + | IsMutConstruct csp , args -> Kapp (string_of_id (basename (Global.sp_of_global (ConstructRef csp))), args) - | IsMutInd (isp,_), args -> + | IsMutInd isp, args -> Kapp (string_of_id (basename (Global.sp_of_global (IndRef isp))),args) | IsVar id,[] -> Kvar(string_of_id id) | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 10ca06b78..b87ec5861 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -200,9 +200,9 @@ let decomp_term c = kind_of_term (strip_outer_cast c) let compute_lhs typ i nargsi = match kind_of_term typ with - | IsMutInd((sp,0),args) -> + | IsMutInd(sp,0) -> let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkMutConstruct (((sp,0),i+1), args), argsi) + mkApp (mkMutConstruct ((sp,0),i+1), argsi) | _ -> i_can't_do_that () (*s This function builds the pattern from the RHS. Recursive calls are diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index 37fb01a4c..173c44356 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -18,14 +18,14 @@ type result = let destructurate t = let c, args = Reduction.whd_stack t in match Term.kind_of_term c, args with - | Term.IsConst (sp,_), args -> + | Term.IsConst sp, args -> Kapp (Names.string_of_id (Names.basename (Global.sp_of_global (Term.ConstRef sp))),args) - | Term.IsMutConstruct (csp,_) , args -> + | Term.IsMutConstruct csp , args -> Kapp (Names.string_of_id (Names.basename (Global.sp_of_global (Term.ConstructRef csp))), args) - | Term.IsMutInd (isp,_), args -> + | Term.IsMutInd isp, args -> Kapp (Names.string_of_id (Names.basename (Global.sp_of_global (Term.IndRef isp))),args) | Term.IsVar id,[] -> Kvar(Names.string_of_id id) @@ -40,9 +40,9 @@ let dest_const_apply t = let f,args = Reduction.whd_stack t in let ref = match Term.kind_of_term f with - | Term.IsConst (sp,_) -> Term.ConstRef sp - | Term.IsMutConstruct (csp,_) -> Term.ConstructRef csp - | Term.IsMutInd (isp,_) -> Term.IndRef isp + | Term.IsConst sp -> Term.ConstRef sp + | Term.IsMutConstruct csp -> Term.ConstructRef csp + | Term.IsMutInd isp -> Term.IndRef isp | _ -> raise Destruct in Names.basename (Global.sp_of_global ref), args diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index f4b75583c..d79e43813 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -414,16 +414,16 @@ let print_term inner_types l env csr = (fun x i -> [< (term_display idradix false l env x); i >]) t [<>]) >] ) - | T.IsConst (sp,_) -> + | T.IsConst sp -> X.xml_empty "CONST" (add_sort_attribute false ["uri",(uri_of_path sp Constant) ; "id", next_id]) - | T.IsMutInd ((sp,i),_) -> + | T.IsMutInd (sp,i) -> X.xml_empty "MUTIND" ["uri",(uri_of_path sp Inductive) ; "noType",(string_of_int i) ; "id", next_id] - | T.IsMutConstruct (((sp,i),j),_) -> + | T.IsMutConstruct ((sp,i),j) -> X.xml_empty "MUTCONSTRUCT" (add_sort_attribute false ["uri",(uri_of_path sp Inductive) ; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 51334029e..bc7a0b836 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -99,13 +99,12 @@ let constr_display csr = ^(term_display t)^","^(term_display c)^")" | IsApp (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" | IsEvar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")" - | IsConst (c,l) -> "Const("^(string_of_path c)^","^(array_display l)^")" - | IsMutInd ((sp,i),l) -> - "MutInd(("^(string_of_path sp)^","^(string_of_int i)^")," - ^(array_display l)^")" - | IsMutConstruct (((sp,i),j),l) -> - "MutConstruct((("^(string_of_path sp)^","^(string_of_int i)^")," - ^(string_of_int j)^"),"^(array_display l)^")" + | IsConst c -> "Const("^(string_of_path c)^")" + | IsMutInd (sp,i) -> + "MutInd("^(string_of_path sp)^","^(string_of_int i)^")" + | IsMutConstruct ((sp,i),j) -> + "MutConstruct(("^(string_of_path sp)^","^(string_of_int i)^")," + ^(string_of_int j)^")" | IsMutCase (ci,p,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display bl)^")" @@ -180,24 +179,19 @@ let print_pure_constr csr = | IsEvar (e,l) -> print_string "Evar#"; print_int e; print_string "{"; Array.iter (fun x -> print_space (); box_display x) l; print_string"}" - | IsConst (c,l) -> print_string "Cons("; + | IsConst c -> print_string "Cons("; sp_display c; - print_string "){"; - Array.iter (fun x -> print_space (); box_display x) l; - print_string"}" - | IsMutInd ((sp,i),l) -> + print_string ")" + | IsMutInd (sp,i) -> print_string "Ind("; sp_display sp; print_string ","; print_int i; - print_string "){"; - Array.iter (fun x -> print_space (); box_display x) l; - print_string"}" - | IsMutConstruct (((sp,i),j),l) -> + print_string ")" + | IsMutConstruct ((sp,i),j) -> print_string "Constr("; sp_display sp; print_string ","; - print_int i; print_string ","; print_int j; print_string ")"; - Array.iter (fun x -> print_space (); box_display x) l; + print_int i; print_string ","; print_int j; print_string ")" | IsMutCase (ci,p,c,bl) -> open_vbox 0; print_string "<"; box_display p; print_string ">"; diff --git a/kernel/closure.ml b/kernel/closure.ml index 82847ae15..283b60e28 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -97,7 +97,7 @@ module RedFlags = (struct r_iota : bool } type red_kind = BETA | DELTA | EVAR | IOTA | ZETA - | CONST of constant_path | VAR of identifier + | CONST of constant | VAR of identifier let fBETA = BETA let fDELTA = DELTA let fEVAR = EVAR @@ -566,8 +566,8 @@ and fterm = | FAtom of constr | FCast of fconstr * fconstr | FFlex of freference - | FInd of inductive_path * fconstr array - | FConstruct of constructor_path * fconstr array + | FInd of inductive + | FConstruct of constructor | FApp of fconstr * fconstr array | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs @@ -583,7 +583,7 @@ and fterm = and freference = (* only vars as args of FConst ... exploited for caching *) - | FConst of section_path * fconstr array + | FConst of constant | FEvar of existential_key * fconstr array | FVar of identifier | FFarRel of int (* index in the rel_context part of _initial_ environment *) @@ -677,13 +677,13 @@ let mk_clos_deep clos_fun env t = | IsApp (f,v) -> { norm = Red; term = FApp (clos_fun env f, Array.map (clos_fun env) v) } - | IsMutInd (sp,v) -> - { norm = Cstr; term = FInd (sp, Array.map (clos_fun env) v) } - | IsMutConstruct (sp,v) -> - { norm = Cstr; term = FConstruct (sp,Array.map (clos_fun env) v)} - | IsConst (sp,v) -> + | IsMutInd sp -> + { norm = Norm; term = FInd sp } + | IsMutConstruct sp -> + { norm = Norm; term = FConstruct sp } + | IsConst sp -> { norm = Red; - term = FFlex (FConst (sp,Array.map (clos_fun env) v)) } + term = FFlex (FConst sp) } | IsEvar (n,v) -> { norm = Red; term = FFlex (FEvar (n, Array.map (clos_fun env) v)) } @@ -736,14 +736,11 @@ let rec to_constr constr_fun lfts v = | _ -> assert false) | FCast (a,b) -> mkCast (constr_fun lfts a, constr_fun lfts b) - | FFlex (FConst (op,ve)) -> - mkConst (op, Array.map (constr_fun lfts) ve) + | FFlex (FConst op) -> mkConst op | FFlex (FEvar (n,args)) -> mkEvar (n, Array.map (constr_fun lfts) args) - | FInd (op,ve) -> - mkMutInd (op, Array.map (constr_fun lfts) ve) - | FConstruct (op,ve) -> - mkMutConstruct (op, Array.map (constr_fun lfts) ve) + | FInd op -> mkMutInd op + | FConstruct op -> mkMutConstruct op | FCases (ci,p,c,ve) -> mkMutCase (ci, constr_fun lfts p, constr_fun lfts c, @@ -984,9 +981,8 @@ let rec knr info m stk = (match get_arg m stk with (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s | (None,s) -> (m,s)) - | FFlex(FConst(sp,args)) when can_red info stk (fCONST sp) -> - let cst = (sp, Array.map term_of_fconstr args) in - (match ref_value_cache info (ConstBinding cst) with + | FFlex(FConst sp) when can_red info stk (fCONST sp) -> + (match ref_value_cache info (ConstBinding sp) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) | FFlex(FEvar (n,args)) when can_red info stk fEVAR -> @@ -1004,7 +1000,7 @@ let rec knr info m stk = (match ref_value_cache info (FarRelBinding k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct((sp,c),args) when can_red info stk fIOTA -> + | FConstruct(ind,c) when can_red info stk fIOTA -> (match strip_update_shift_app m stk with (depth, args, Zcase(((*cn*) npar,_),_,br)::s) -> assert (npar>=0); @@ -1061,15 +1057,9 @@ and down_then_up info m stk = FLetIn(na, kl info a, kl info b, kl info c, f, e) | FProd(na,dom,rng,f,e) -> FProd(na, kl info dom, kl info rng, f, e) - | FInd(ind,args) -> - FInd(ind, Array.map (kl info) args) - | FConstruct(c,args) -> - FConstruct(c, Array.map (kl info) args) | FCoFix(n,(na,ftys,fbds),bds,e) -> FCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds),bds,e) - | FFlex(FConst(sp,args)) -> - FFlex(FConst(sp, Array.map (kl info) args)) | FFlex(FEvar(i,args)) -> FFlex(FEvar(i, Array.map (kl info) args)) | t -> t in @@ -1097,9 +1087,7 @@ let create_clos_infos flgs env sigma = create (fun _ -> inject) flgs env sigma let unfold_reference info = function - | FConst (op,v) -> - let cst = (op, Array.map (norm_val info) v) in - ref_value_cache info (ConstBinding cst) + | FConst op -> ref_value_cache info (ConstBinding op) | FEvar (n,v) -> let evar = (n, Array.map (norm_val info) v) in ref_value_cache info (EvarBinding evar) diff --git a/kernel/closure.mli b/kernel/closure.mli index 5c8662420..16de949af 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -166,8 +166,8 @@ type fterm = | FAtom of constr | FCast of fconstr * fconstr | FFlex of freference - | FInd of inductive_path * fconstr array - | FConstruct of constructor_path * fconstr array + | FInd of inductive + | FConstruct of constructor | FApp of fconstr * fconstr array | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs @@ -182,7 +182,7 @@ type fterm = | FLOCKED and freference = - | FConst of section_path * fconstr array + | FConst of constant | FEvar of existential_key * fconstr array | FVar of identifier | FFarRel of int diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1bccf60f6..79420e040 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -20,37 +20,21 @@ open Reduction (*s Cooking the constants. *) -type modification_action = ABSTRACT | ERASE - type 'a modification = | NOT_OCCUR - | DO_ABSTRACT of 'a * modification_action list + | DO_ABSTRACT of 'a * constr array | DO_REPLACE of constant_body type work_list = - (section_path * section_path modification) list - * (inductive_path * inductive_path modification) list - * (constructor_path * constructor_path modification) list + (constant * constant modification) list + * (inductive * inductive modification) list + * (constructor * constructor modification) list type recipe = { d_from : constant_body; d_abstract : identifier list; d_modlist : work_list } -let rec modif_length = function - | ABSTRACT :: l -> 1 + modif_length l - | ERASE :: l -> modif_length l - | [] -> 0 - -let interp_modif absfun mkfun (sp,modif) cl = - let rec interprec = function - | ([], cl) -> mkfun (sp, Array.of_list cl) - | (ERASE::tlm, c::cl) -> interprec (tlm,cl) - | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c - | _ -> assert false - in - interprec (modif, Array.to_list cl) - let failure () = anomalylabstrm "generic__modify_opers" [< 'sTR"An oper which was never supposed to appear has just appeared" ; @@ -61,7 +45,7 @@ let failure () = 'sPC ; 'sTR"is broken - this function is an internal system" ; 'sPC ; 'sTR"for internal system use only" >] -let modify_opers replfun absfun (constl,indl,cstrl) = +let modify_opers replfun (constl,indl,cstrl) = let rec substrec c = let op, cl = splay_constr c in let cl' = Array.map substrec cl in @@ -69,51 +53,51 @@ let modify_opers replfun absfun (constl,indl,cstrl) = | OpMutCase (n,(spi,a,b,c,d) as oper) -> (try match List.assoc spi indl with - | DO_ABSTRACT (spi',modif) -> - let n' = modif_length modif + n in + | DO_ABSTRACT (spi',abs_vars) -> + let n' = Array.length abs_vars + n in gather_constr (OpMutCase (n',(spi',a,b,c,d)),cl') | _ -> raise Not_found with | Not_found -> gather_constr (op,cl')) | OpMutInd spi -> + assert (Array.length cl=0); (try (match List.assoc spi indl with | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',modif) -> - assert (List.length modif <= Array.length cl); - interp_modif absfun mkMutInd (oper',modif) cl' + | DO_ABSTRACT (oper',abs_vars) -> + mkApp (mkMutInd oper', abs_vars) | DO_REPLACE _ -> assert false) with - | Not_found -> mkMutInd (spi,cl')) + | Not_found -> mkMutInd spi) | OpMutConstruct spi -> + assert (Array.length cl=0); (try (match List.assoc spi cstrl with | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',modif) -> - assert (List.length modif <= Array.length cl); - interp_modif absfun mkMutConstruct (oper',modif) cl' + | DO_ABSTRACT (oper',abs_vars) -> + mkApp (mkMutConstruct oper', abs_vars) | DO_REPLACE _ -> assert false) with - | Not_found -> mkMutConstruct (spi,cl')) + | Not_found -> mkMutConstruct spi) | OpConst sp -> + assert (Array.length cl=0); (try (match List.assoc sp constl with | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',modif) -> - assert (List.length modif <= Array.length cl); - interp_modif absfun mkConst (oper',modif) cl' + | DO_ABSTRACT (oper',abs_vars) -> + mkApp (mkConst oper', abs_vars) | DO_REPLACE cb -> substrec (replfun sp cb cl')) with - | Not_found -> mkConst (sp,cl')) + | Not_found -> mkConst sp) | _ -> gather_constr (op, cl') in if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec -let expmod_constr oldenv modlist c = +let expmod_constr modlist c = let sigma = Evd.empty in let simpfun = if modlist = ([],[],[]) then fun x -> x else nf_betaiota in @@ -130,22 +114,20 @@ let expmod_constr oldenv modlist c = instantiate_constr cb.const_hyps body (Array.to_list args) | None -> assert false in - let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in + let c' = + modify_opers expfun modlist c in match kind_of_term c' with | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ) | _ -> simpfun c' -let expmod_type oldenv modlist c = - type_app (expmod_constr oldenv modlist) c +let expmod_type modlist c = + type_app (expmod_constr modlist) c let abstract_constant ids_to_abs hyps (body,typ) = let abstract_once ((hyps,body,typ) as sofar) id = match hyps with | (hyp,c,t as decl)::rest when hyp = id -> - let body' = match body with - | None -> None - | Some c -> Some (mkNamedLambda_or_LetIn decl c) - in + let body' = option_app (mkNamedLambda_or_LetIn decl) body in let typ' = mkNamedProd_wo_LetIn decl typ in (rest, body', typ') | _ -> @@ -157,9 +139,9 @@ let abstract_constant ids_to_abs hyps (body,typ) = let cook_constant env r = let cb = r.d_from in - let typ = expmod_type env r.d_modlist cb.const_type in - let body = option_app (expmod_constr env r.d_modlist) cb.const_body in + let typ = expmod_type r.d_modlist cb.const_type in + let body = option_app (expmod_constr r.d_modlist) cb.const_body in let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in - let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in + let hyps = map_named_context (expmod_constr r.d_modlist) hyps in let body,typ = abstract_constant r.d_abstract hyps (body,typ) in (body, typ, cb.const_constraints, cb.const_opaque) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 48f4dfc83..3cd03fc9a 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,17 +16,15 @@ open Univ (*s Cooking the constants. *) -type modification_action = ABSTRACT | ERASE - type 'a modification = | NOT_OCCUR - | DO_ABSTRACT of 'a * modification_action list + | DO_ABSTRACT of 'a * constr array | DO_REPLACE of constant_body type work_list = - (section_path * section_path modification) list - * (inductive_path * inductive_path modification) list - * (constructor_path * constructor_path modification) list + (constant * constant modification) list + * (inductive * inductive modification) list + * (constructor * constructor modification) list type recipe = { d_from : constant_body; @@ -38,7 +36,7 @@ val cook_constant : (*s Utility functions used in module [Discharge]. *) -val expmod_constr : env -> work_list -> constr -> constr -val expmod_type : env -> work_list -> types -> types +val expmod_constr : work_list -> constr -> constr +val expmod_type : work_list -> types -> types diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f75128148..47f65d4a3 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -45,7 +45,7 @@ type recarg = | Param of int | Norec | Mrec of int - | Imbr of inductive_path * recarg list + | Imbr of inductive * recarg list type one_inductive_body = { mind_consnames : identifier array; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index e7c88f6f4..735f6f141 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -47,7 +47,7 @@ type recarg = | Param of int | Norec | Mrec of int - | Imbr of inductive_path * (recarg list) + | Imbr of inductive * (recarg list) (* [mind_typename] is the name of the inductive; [mind_arity] is the arity generalized over global parameters; [mind_lc] is the list diff --git a/kernel/environ.ml b/kernel/environ.ml index a34191a3e..98f54337f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -214,6 +214,112 @@ let lookup_constant sp env = let lookup_mind sp env = Spmap.find sp env.env_globals.env_inductives + +(* Lookup of section variables *) +let lookup_constant_variables c env = + let cmap = lookup_constant c env in + Sign.instance_from_section_context cmap.const_hyps + +let lookup_inductive_variables (sp,i) env = + let mis = lookup_mind sp env in + Sign.instance_from_section_context mis.mind_hyps + +let lookup_constructor_variables (ind,_) env = + lookup_inductive_variables ind env + +(* Returns the list of global variables in a term *) + +let vars_of_global env constr = + match kind_of_term constr with + IsVar id -> [id] + | IsConst sp -> + List.map destVar + (Array.to_list (lookup_constant_variables sp env)) + | IsMutInd ind -> + List.map destVar + (Array.to_list (lookup_inductive_variables ind env)) + | IsMutConstruct cstr -> + List.map destVar + (Array.to_list (lookup_constructor_variables cstr env)) + | _ -> [] + +let rec global_varsl env l constr = + let l = vars_of_global env constr @ l in + fold_constr (global_varsl env) l constr + +let global_vars env = global_varsl env [] + +let global_vars_decl env = function + | (_, None, t) -> global_vars env t + | (_, Some c, t) -> (global_vars env c)@(global_vars env t) + +let global_vars_set env constr = + let rec filtrec acc c = + let vl = vars_of_global env c in + let acc = List.fold_right Idset.add vl acc in + fold_constr filtrec acc c + in + filtrec Idset.empty constr + + +exception Occur + +let occur_in_global env id constr = + let vars = vars_of_global env constr in + if List.mem id vars then raise Occur + +let occur_var env s c = + let rec occur_rec c = + occur_in_global env s c; + iter_constr occur_rec c + in + try occur_rec c; false with Occur -> true + +let occur_var_in_decl env hyp (_,c,typ) = + match c with + | None -> occur_var env hyp (body_of_type typ) + | Some body -> + occur_var env hyp (body_of_type typ) || + occur_var env hyp body + +(* [keep_hyps sign ids] keeps the part of the signature [sign] which + contains the variables of the set [ids], and recursively the variables + contained in the types of the needed variables. *) + +let rec keep_hyps env needed = function + | (id,copt,t as d) ::sign when Idset.mem id needed -> + let globc = + match copt with + | None -> Idset.empty + | Some c -> global_vars_set env c in + let needed' = + Idset.union (global_vars_set env (body_of_type t)) + (Idset.union globc needed) in + d :: (keep_hyps env needed' sign) + | _::sign -> keep_hyps env needed sign + | [] -> [] + +(* This renames bound variables with fresh and distinct names *) +(* in such a way that the printer doe not generate new names *) +(* and therefore that printed names are the intern names *) +(* In this way, tactics such as Induction works well *) + +let rec rename_bound_var env l c = + match kind_of_term c with + | IsProd (Name s,c1,c2) -> + if dependent (mkRel 1) c2 then + let s' = next_ident_away s (global_vars env c2@l) in + let env' = push_rel (Name s',None,c1) env in + mkProd (Name s', c1, rename_bound_var env' (s'::l) c2) + else + let env' = push_rel (Name s,None,c1) env in + mkProd (Name s, c1, rename_bound_var env' l c2) + | IsProd (Anonymous,c1,c2) -> + let env' = push_rel (Anonymous,None,c1) env in + mkProd (Anonymous, c1, rename_bound_var env' l c2) + | IsCast (c,t) -> mkCast (rename_bound_var env l c, t) + | x -> c + (* First character of a constr *) let lowercase_first_char id = String.lowercase (first_char id) @@ -244,15 +350,15 @@ let hdchar env c = | IsLetIn (_,_,_,c) -> hdrec (k+1) c | IsCast (c,_) -> hdrec k c | IsApp (f,l) -> hdrec k f - | IsConst (sp,_) -> + | IsConst sp -> let c = lowercase_first_char (basename sp) in if c = "?" then "y" else c - | IsMutInd ((sp,i) as x,_) -> + | IsMutInd ((sp,i) as x) -> if i=0 then lowercase_first_char (basename sp) else lowercase_first_char (id_of_global env (IndRef x)) - | IsMutConstruct ((sp,i) as x,_) -> + | IsMutConstruct ((sp,i) as x) -> lowercase_first_char (id_of_global env (ConstructRef x)) | IsVar id -> lowercase_first_char id | IsSort s -> sort_hdchar s diff --git a/kernel/environ.mli b/kernel/environ.mli index 2a778b76e..761f196c0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -104,12 +104,18 @@ val lookup_rel_value : int -> env -> constr option (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) -val lookup_constant : constant_path -> env -> constant_body +val lookup_constant : constant -> env -> constant_body (* Looks up in the context of global inductive names *) (* raises [Not_found] if the required path is not found *) val lookup_mind : section_path -> env -> mutual_inductive_body +(* Looks up the array of section variables used by a global (constant, + inductive or constructor). *) +val lookup_constant_variables : constant -> env -> constr array +val lookup_inductive_variables : inductive -> env -> constr array +val lookup_constructor_variables : constructor -> env -> constr array + (*s Miscellanous *) val sp_of_global : env -> global_reference -> section_path @@ -158,12 +164,30 @@ val it_mkNamedProd_wo_LetIn : constr -> named_context -> constr val lambda_create : env -> types * constr -> constr val prod_create : env -> types * constr -> constr -val defined_constant : env -> constant_path -> bool -val evaluable_constant : env -> constant_path -> bool +val defined_constant : env -> constant -> bool +val evaluable_constant : env -> constant -> bool val evaluable_named_decl : env -> identifier -> bool val evaluable_rel_decl : env -> int -> bool +(*s Ocurrence of section variables. *) +(* [(occur_var id c)] returns [true] if variable [id] occurs free + in c, [false] otherwise *) +val occur_var : env -> identifier -> constr -> bool +val occur_var_in_decl : env -> identifier -> named_declaration -> bool + +(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *) +val global_vars : env -> constr -> identifier list + +(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR + id] in declaration [d] (type and body if any) *) +val global_vars_decl : env -> named_declaration -> identifier list +val global_vars_set : env -> constr -> Idset.t + +val keep_hyps : env -> Idset.t -> named_context -> named_context + +val rename_bound_var : env -> identifier list -> constr -> constr + (*s Modules. *) type compiled_env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index c28055ae6..47e56e3b0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -189,13 +189,13 @@ let listrec_mconstr env ntypes hyps nparams i indlc = else Norec else raise (IllFormedInd (LocalNonPos n)) - | IsMutInd (ind_sp,a) -> - if array_for_all (noccur_between n ntypes) a - && List.for_all (noccur_between n ntypes) largs + | IsMutInd ind_sp -> + if List.for_all (noccur_between n ntypes) largs then Norec - else Imbr(ind_sp,imbr_positive env n (ind_sp,a) largs) + else Imbr(ind_sp,imbr_positive env n ind_sp largs) | err -> - if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs + if noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs then Norec else raise (IllFormedInd (LocalNonPos n)) @@ -315,9 +315,9 @@ let is_recursive listind = let abstract_inductive ntypes hyps (par,np,id,arity,cnames,issmall,isunit,lc) = let args = instance_from_named_context (List.rev hyps) in let nhyps = List.length hyps in - let nparams = List.length args in (* nparams = nhyps - nb(letin) *) + let nparams = Array.length args in (* nparams = nhyps - nb(letin) *) let new_refs = - list_tabulate (fun k -> applist(mkRel (k+nhyps+1),args)) ntypes in + list_tabulate (fun k -> appvect(mkRel (k+nhyps+1),args)) ntypes in let abs_constructor b = it_mkNamedProd_or_LetIn (substl new_refs b) hyps in let lc' = Array.map abs_constructor lc in let arity' = it_mkNamedProd_or_LetIn arity hyps in @@ -329,14 +329,15 @@ let cci_inductive locals env env_ar kind finite inds cst = let ids = List.fold_left (fun acc (_,_,_,ar,_,_,_,lc) -> - Idset.union (global_vars_set (body_of_type ar)) + Idset.union (global_vars_set env (body_of_type ar)) (Array.fold_left - (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc) + (fun acc c -> + Idset.union (global_vars_set env (body_of_type c)) acc) acc lc)) Idset.empty inds in - let hyps = keep_hyps ids (named_context env) in + let hyps = keep_hyps env ids (named_context env) in let inds' = if Options.immediate_discharge then List.map (abstract_inductive ntypes hyps) inds diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index f5a6ca236..93bfb5454 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -49,7 +49,7 @@ val mind_check_wellformed : env -> mutual_inductive_entry -> unit (* [cci_inductive] checks positivity and builds an inductive body *) val cci_inductive : - (identifier * variable_path) list -> env -> env -> path_kind -> bool -> + (identifier * variable) list -> env -> env -> path_kind -> bool -> (Sign.rel_context * int * identifier * types * identifier list * bool * bool * types array) list -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b52822514..6cd04f76f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -21,12 +21,11 @@ type inductive_instance = { mis_sp : section_path; mis_mib : mutual_inductive_body; mis_tyi : int; - mis_args : constr array; mis_mip : one_inductive_body } -let build_mis ((sp,tyi),args) mib = - { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args; +let build_mis (sp,tyi) mib = + { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_mip = mind_nth_type_packet mib tyi } let mis_ntypes mis = mis.mis_mib.mind_ntypes @@ -47,28 +46,18 @@ let mis_consnames mis = mis.mis_mip.mind_consnames let mis_conspaths mis = let dir = dirpath mis.mis_sp in Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames -let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args) +let mis_inductive mis = (mis.mis_sp,mis.mis_tyi) let mis_finite mis = mis.mis_mip.mind_finite let mis_typed_nf_lc mis = let sign = mis.mis_mib.mind_hyps in -(* let args = Array.to_list mis.mis_args in *) - Array.map (fun t -> (* Instantiate.instantiate_type sign*) t (*args*)) - mis.mis_mip.mind_nf_lc + mis.mis_mip.mind_nf_lc let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis) let mis_user_lc mis = let sign = mis.mis_mib.mind_hyps in -(*i - let at = mind_user_lc mis.mis_mip in - if Array.length mis.mis_args = 0 then at - else - let args = Array.to_list mis.mis_args in - Array.map (fun t -> Instantiate.instantiate_constr sign t args) at -i*) - Array.map (fun t -> (*Instantiate.instantiate_type sign*) t (*args*)) - (mind_user_lc mis.mis_mip) + (mind_user_lc mis.mis_mip) (* gives the vector of constructors and of types of constructors of an inductive definition @@ -78,10 +67,9 @@ let mis_type_mconstructs mispec = let specif = Array.map body_of_type (mis_user_lc mispec) and ntypes = mis_ntypes mispec and nconstr = mis_nconstr mispec in - let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) - and make_Ck k = mkMutConstruct - (((mispec.mis_sp,mispec.mis_tyi),k+1), - mispec.mis_args) in + let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) + and make_Ck k = + mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in (Array.init nconstr make_Ck, Array.map (substl (list_tabulate make_Ik ntypes)) specif) @@ -89,7 +77,7 @@ let mis_nf_constructor_type i mispec = let specif = mis_nf_lc mispec and ntypes = mis_ntypes mispec and nconstr = mis_nconstr mispec in - let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in + let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in if i > nconstr then error "Not enough constructors in the type"; substl (list_tabulate make_Ik ntypes) specif.(i-1) @@ -97,22 +85,17 @@ let mis_constructor_type i mispec = let specif = mis_user_lc mispec and ntypes = mis_ntypes mispec and nconstr = mis_nconstr mispec in - let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in + let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in if i > nconstr then error "Not enough constructors in the type"; substl (list_tabulate make_Ik ntypes) specif.(i-1) let mis_arity mis = - let hyps = mis.mis_mib.mind_hyps - in let ar = mind_user_arity mis.mis_mip - in if Array.length mis.mis_args = 0 then ar - else let largs = Array.to_list mis.mis_args in - Instantiate.instantiate_type hyps ar largs + let hyps = mis.mis_mib.mind_hyps in + mind_user_arity mis.mis_mip let mis_nf_arity mis = - let hyps = mis.mis_mib.mind_hyps - in if Array.length mis.mis_args = 0 then mis.mis_mip.mind_nf_arity - else let largs = Array.to_list mis.mis_args in - Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs + let hyps = mis.mis_mib.mind_hyps in + mis.mis_mip.mind_nf_arity let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt (* @@ -124,31 +107,13 @@ let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt let mis_sort mispec = mispec.mis_mip.mind_sort -let liftn_inductive_instance n depth mis = { - mis_sp = mis.mis_sp; - mis_mib = mis.mis_mib; - mis_tyi = mis.mis_tyi; - mis_args = Array.map (liftn n depth) mis.mis_args; - mis_mip = mis.mis_mip -} - -let lift_inductive_instance n = liftn_inductive_instance n 1 - -let substnl_ind_instance l n mis = { - mis_sp = mis.mis_sp; - mis_mib = mis.mis_mib; - mis_tyi = mis.mis_tyi; - mis_args = Array.map (substnl l n) mis.mis_args; - mis_mip = mis.mis_mip -} - (* [inductive_family] = [inductive_instance] applied to global parameters *) type inductive_family = IndFamily of inductive_instance * constr list type inductive_type = IndType of inductive_family * constr list -let liftn_inductive_family n d (IndFamily (mis, params)) = - IndFamily (liftn_inductive_instance n d mis, List.map (liftn n d) params) +let liftn_inductive_family n d (IndFamily (mis,params)) = + IndFamily (mis, List.map (liftn n d) params) let lift_inductive_family n = liftn_inductive_family n 1 let liftn_inductive_type n d (IndType (indf, realargs)) = @@ -156,7 +121,7 @@ let liftn_inductive_type n d (IndType (indf, realargs)) = let lift_inductive_type n = liftn_inductive_type n 1 let substnl_ind_family l n (IndFamily (mis,params)) = - IndFamily (substnl_ind_instance l n mis, List.map (substnl l n) params) + IndFamily (mis, List.map (substnl l n) params) let substnl_ind_type l n (IndType (indf,realargs)) = IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs) @@ -198,12 +163,9 @@ let make_default_case_info mis = (*s Useful functions *) -let inductive_path_of_constructor_path (ind_sp,i) = ind_sp -let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i) - -let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args) -let index_of_constructor ((ind_sp,i),args) = i -let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) +let inductive_of_constructor (ind_sp,i) = ind_sp +let index_of_constructor (ind_sp,i) = i +let ith_constructor_of_inductive ind_sp i = (ind_sp,i) exception Induc @@ -222,19 +184,19 @@ let find_mrectype env sigma c = let find_inductive env sigma c = let (t, l) = whd_betadeltaiota_stack env sigma c in match kind_of_term t with - | IsMutInd ((sp,i),_ as ind) + | IsMutInd ((sp,i) as ind) when mind_type_finite (lookup_mind sp env) i -> (ind, l) | _ -> raise Induc let find_coinductive env sigma c = let (t, l) = whd_betadeltaiota_stack env sigma c in match kind_of_term t with - | IsMutInd ((sp,i),_ as ind) + | IsMutInd ((sp,i) as ind) when not (mind_type_finite (lookup_mind sp env) i) -> (ind, l) | _ -> raise Induc (* raise Induc if not an inductive type *) -let lookup_mind_specif ((sp,tyi),args as ind) env = +let lookup_mind_specif ((sp,tyi) as ind) env = build_mis ind (lookup_mind sp env) let find_rectype env sigma ty = @@ -253,7 +215,7 @@ type constructor_summary = { } let lift_constructor n cs = { - cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt)); + cs_cstr = cs.cs_cstr; cs_params = List.map (lift n) cs.cs_params; cs_nargs = cs.cs_nargs; cs_args = lift_rel_context n cs.cs_args; diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c8f49ed61..2aee7f420 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -67,10 +67,10 @@ type inductive_family = IndFamily of inductive_instance * constr list val make_ind_family : inductive_instance * constr list -> inductive_family val dest_ind_family : inductive_family -> inductive_instance * constr list -val liftn_inductive_family : int -> int -> inductive_family -> inductive_family -val lift_inductive_family : int -> inductive_family -> inductive_family -val substnl_ind_family : constr list -> int -> inductive_family - -> inductive_family +val liftn_inductive_family : + int -> int -> inductive_family -> inductive_family +val lift_inductive_family : + int -> inductive_family -> inductive_family (*s [inductive_type] = [inductive_family] applied to ``real'' parameters *) type inductive_type = IndType of inductive_family * constr list @@ -90,10 +90,6 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val ith_constructor_of_inductive : inductive -> int -> constructor -val inductive_path_of_constructor_path : constructor_path -> inductive_path -val ith_constructor_path_of_inductive_path : - inductive_path -> int -> constructor_path - (*s This type gathers useful informations about some instance of a constructor relatively to some implicit context (the current one) diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index a92de9e60..c1e864523 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -61,23 +61,20 @@ let instantiate_type sign tty args = (* Constants. *) (* constant_type gives the type of a constant *) -let constant_type env sigma (sp,args) = +let constant_type env sigma sp = let cb = lookup_constant sp env in - (* TODO: check args *) -(* instantiate_type cb.const_hyps *) cb.const_type (*(Array.to_list args)*) + cb.const_type type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -let constant_value env (sp,args) = +let constant_value env sp = let cb = lookup_constant sp env in if cb.const_opaque then raise (NotEvaluableConst Opaque); match cb.const_body with - | Some body -> - instantiate_constr cb.const_hyps body (Array.to_list args) - | None -> - raise (NotEvaluableConst NoBody) + | Some body -> body + | None -> raise (NotEvaluableConst NoBody) let constant_opt_value env cst = try Some (constant_value env cst) @@ -133,7 +130,7 @@ let destEvalRef c = match kind_of_term c with | _ -> anomaly "Not an evaluable reference" let evaluable_reference sigma env = function - | EvalConst (sp,_) -> evaluable_constant env sp + | EvalConst sp -> evaluable_constant env sp | EvalVar id -> evaluable_named_decl env id | EvalRel n -> evaluable_rel_decl env n | EvalEvar (ev,_) -> Evd.is_defined sigma ev diff --git a/kernel/names.ml b/kernel/names.ml index 3d72326ed..811672ba3 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -316,11 +316,11 @@ module Spmap = Map.Make(SpOrdered) (* Special references for inductive objects *) -type variable_path = section_path -type constant_path = section_path -type inductive_path = section_path * int -type constructor_path = inductive_path * int -type mutual_inductive_path = section_path +type variable = section_path +type constant = section_path +type inductive = section_path * int +type constructor = inductive * int +type mutual_inductive = section_path (* Hash-consing of name objects *) module Hname = Hashcons.Make( diff --git a/kernel/names.mli b/kernel/names.mli index 5af331075..cdf8c8c83 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -112,11 +112,11 @@ module Sppred : Predicate.S with type elt = section_path module Spmap : Map.S with type key = section_path (*s Specific paths for declarations *) -type variable_path = section_path -type constant_path = section_path -type inductive_path = section_path * int -type constructor_path = inductive_path * int -type mutual_inductive_path = section_path +type variable = section_path +type constant = section_path +type inductive = section_path * int +type constructor = inductive * int +type mutual_inductive = section_path (* Hash-consing *) val hcons_names : unit -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5c0a4fa63..734187a9c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -201,7 +201,7 @@ let contract_cofix (bodynum,(types,names,bodies as typedbodies)) = let reduce_mind_case mia = match kind_of_term mia.mconstr with - | IsMutConstruct (ind_sp,i as cstr_sp, args) -> + | IsMutConstruct (ind_sp,i as cstr_sp) -> (* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in applist (mia.mlf.(i-1),real_cargs) @@ -574,17 +574,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv = let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in convert_stacks infos lft1 lft2 v1 v2 u3 - | (FInd (op1,cl1), FInd(op2,cl2)) -> - if op1 = op2 then - let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in - convert_stacks infos lft1 lft2 v1 v2 u1 + | (FInd op1, FInd op2) -> + if op1 = op2 + then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | (FConstruct (op1,cl1), FConstruct(op2,cl2)) -> + | (FConstruct op1, FConstruct op2) -> if op1 = op2 - then - let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in - convert_stacks infos lft1 lft2 v1 v2 u1 + then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1c7d5e17f..6eba04182 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -264,14 +264,15 @@ let safe_infer_declaration env = function let (j,cst) = safe_infer env t in None, assumption_of_judgment env Evd.empty j, cst -type local_names = (identifier * variable_path) list +type local_names = (identifier * variable) list let add_global_declaration sp env locals (body,typ,cst) op = let env' = add_constraints cst env in let ids = match body with - | None -> global_vars_set typ - | Some b -> Idset.union (global_vars_set b) (global_vars_set typ) in - let hyps = keep_hyps ids (named_context env) in + | None -> global_vars_set env typ + | Some b -> + Idset.union (global_vars_set env b) (global_vars_set env typ) in + let hyps = keep_hyps env ids (named_context env) in let body, typ = if Options.immediate_discharge then option_app (fun c -> it_mkNamedLambda_or_LetIn c hyps) body, @@ -312,8 +313,9 @@ let add_discharged_constant sp r locals env = add_parameter sp typ locals (* Bricolage avant poubelle *) env' | Some c -> (* let c = hcons1_constr c in *) - let ids = Idset.union (global_vars_set c) (global_vars_set typ) in - let hyps = keep_hyps ids (named_context env') in + let ids = + Idset.union (global_vars_set env c) (global_vars_set env typ) in + let hyps = keep_hyps env ids (named_context env') in let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in let cb = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 90c6e2466..23a970b49 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -45,7 +45,7 @@ val check_and_push_named_def : identifier * constr -> safe_environment -> (constr option * types * constraints) * safe_environment -type local_names = (identifier * variable_path) list +type local_names = (identifier * variable) list val add_parameter : section_path -> constr -> local_names -> safe_environment -> safe_environment diff --git a/kernel/sign.ml b/kernel/sign.ml index 573d6f809..0d7168c00 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -43,10 +43,12 @@ let pop_named_decl id = function | (id',_,_) :: sign -> assert (id = id'); sign | [] -> assert false let ids_of_named_context = List.map (fun (id,_,_) -> id) -let rec instance_from_named_context = function - | (id,None,_) :: sign -> mkVar id :: instance_from_named_context sign - | _ :: sign -> instance_from_named_context sign - | [] -> [] +let instance_from_named_context sign = + let rec inst_rec = function + | (id,None,_) :: sign -> mkVar id :: inst_rec sign + | _ :: sign -> inst_rec sign + | [] -> [] in + Array.of_list (inst_rec sign) let map_named_context = map let rec mem_named_context id = function | (id',_,_) :: _ when id=id' -> true @@ -59,15 +61,17 @@ let it_named_context_quantifier f = List.fold_left (fun c d -> f d c) (*s Signatures of ordered section variables *) -type section_declaration = variable_path * constr option * constr +type section_declaration = variable * constr option * constr type section_context = section_declaration list -let rec instance_from_section_context = function - | (sp,None,_) :: sign -> - mkVar (basename sp) :: instance_from_section_context sign - | _ :: sign -> instance_from_section_context sign - | [] -> [] +let instance_from_section_context sign = + let rec inst_rec = function + | (sp,None,_) :: sign -> mkVar (basename sp) :: inst_rec sign + | _ :: sign -> inst_rec sign + | [] -> [] in + Array.of_list (inst_rec sign) let instance_from_section_context x = - if Options.immediate_discharge then [] else instance_from_section_context x + if Options.immediate_discharge then [||] + else instance_from_section_context x (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) @@ -156,23 +160,6 @@ let instantiate_sign sign args = in instrec (sign,args) -(* [keep_hyps sign ids] keeps the part of the signature [sign] which - contains the variables of the set [ids], and recursively the variables - contained in the types of the needed variables. *) - -let rec keep_hyps needed = function - | (id,copt,t as d) ::sign when Idset.mem id needed -> - let globc = - match copt with - | None -> Idset.empty - | Some c -> global_vars_set c in - let needed' = - Idset.union (global_vars_set (body_of_type t)) - (Idset.union globc needed) in - d :: (keep_hyps needed' sign) - | _::sign -> keep_hyps needed sign - | [] -> [] - (*************************) (* Names environments *) (*************************) diff --git a/kernel/sign.mli b/kernel/sign.mli index 6180906cb..dd5aba6c6 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -40,15 +40,14 @@ val it_named_context_quantifier : (named_declaration -> constr -> constr) -> constr -> named_context -> constr val instantiate_sign : named_context -> constr list -> (identifier * constr) list -val keep_hyps : Idset.t -> named_context -> named_context -val instance_from_named_context : named_context -> constr list +val instance_from_named_context : named_context -> constr array (*s Signatures of ordered section variables *) -type section_declaration = variable_path * constr option * constr +type section_declaration = variable * constr option * constr type section_context = section_declaration list -val instance_from_section_context : section_context -> constr list +val instance_from_section_context : section_context -> constr array (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) diff --git a/kernel/term.ml b/kernel/term.ml index 8b276c068..e79fd5fb3 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -24,7 +24,7 @@ type existential_key = int type pattern_source = DefaultPat of int | RegularPat type case_style = PrintLet | PrintIf | PrintCases type case_printing = - inductive_path * identifier array * int + inductive * identifier array * int * case_style option * pattern_source array type case_info = int * case_printing @@ -62,9 +62,9 @@ let family_of_sort = function type global_reference = | VarRef of section_path - | ConstRef of constant_path - | IndRef of inductive_path - | ConstructRef of constructor_path + | ConstRef of constant + | IndRef of inductive + | ConstructRef of constructor (********************************************************************) (* Constructions as implemented *) @@ -80,9 +80,6 @@ module type InternalSig = sig type constr type existential = existential_key * constr array -type constant = section_path * constr array -type constructor = constructor_path * constr array -type inductive = inductive_path * constr array type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -143,9 +140,6 @@ struct (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr existential = existential_key * 'constr array -type 'constr constant = constant_path * 'constr array -type 'constr constructor = constructor_path * 'constr array -type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = name array * 'types array * 'constr array type ('constr, 'types) fixpoint = @@ -170,9 +164,9 @@ type ('constr, 'types) kind_of_term = | IsLetIn of name * 'constr * 'types * 'constr | IsApp of 'constr * 'constr array | IsEvar of 'constr existential - | IsConst of 'constr constant - | IsMutInd of 'constr inductive - | IsMutConstruct of 'constr constructor + | IsConst of constant + | IsMutInd of inductive + | IsMutConstruct of constructor | IsMutCase of case_info * 'constr * 'constr * 'constr array | IsFix of ('constr, 'types) fixpoint | IsCoFix of ('constr, 'types) cofixpoint @@ -180,9 +174,6 @@ type ('constr, 'types) kind_of_term = type constr = (constr,constr) kind_of_term type existential = existential_key * constr array -type constant = constant_path * constr array -type constructor = constructor_path * constr array -type inductive = inductive_path * constr array type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -204,10 +195,9 @@ let comp_term t1 t2 = n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 | IsApp (c1,l1), IsApp (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2 | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2 - | IsConst (c1,l1), IsConst (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2 - | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2 - | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) -> - c1 == c2 & array_for_all2 (==) l1 l2 + | IsConst c1, IsConst c2 -> c1 == c2 + | IsMutInd c1, IsMutInd c2 -> c1 == c2 + | IsMutConstruct c1, IsMutConstruct c2 -> c1 == c2 | IsMutCase (ci1,p1,c1,bl1), IsMutCase (ci2,p2,c2,bl2) -> ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2 | IsFix (ln1,(lna1,tl1,bl1)), IsFix (ln2,(lna2,tl2,bl2)) -> @@ -233,10 +223,9 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t = | IsLetIn (na,b,t,c) -> IsLetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c) | IsApp (c,l) -> IsApp (sh_rec c, Array.map sh_rec l) | IsEvar (e,l) -> IsEvar (e, Array.map sh_rec l) - | IsConst (c,l) -> IsConst (sh_sp c, Array.map sh_rec l) - | IsMutInd ((sp,i),l) -> IsMutInd ((sh_sp sp,i), Array.map sh_rec l) - | IsMutConstruct (((sp,i),j),l) -> - IsMutConstruct (((sh_sp sp,i),j), Array.map sh_rec l) + | IsConst c -> IsConst (sh_sp c) + | IsMutInd (sp,i) -> IsMutInd (sh_sp sp,i) + | IsMutConstruct ((sp,i),j) -> IsMutConstruct ((sh_sp sp,i),j) | IsMutCase (ci,p,c,bl) -> (* TO DO: extract ind_sp *) IsMutCase (ci, sh_rec p, sh_rec c, Array.map sh_rec bl) | IsFix (ln,(lna,tl,bl)) -> @@ -465,17 +454,9 @@ let isApp c = match kind_of_term c with IsApp _ -> true | _ -> false (* Destructs a constant *) let destConst c = match kind_of_term c with - | IsConst (sp, a as r) -> r + | IsConst sp -> sp | _ -> invalid_arg "destConst" -let path_of_const c = match kind_of_term c with - | IsConst (sp,_) -> sp - | _ -> anomaly "path_of_const called with bad args" - -let args_of_const c = match kind_of_term c with - | IsConst (_,args) -> args - | _ -> anomaly "args_of_const called with bad args" - let isConst c = match kind_of_term c with IsConst _ -> true | _ -> false (* Destructs an existential variable *) @@ -491,28 +472,12 @@ let num_of_evar c = match kind_of_term c with let destMutInd c = match kind_of_term c with | IsMutInd (sp, a as r) -> r | _ -> invalid_arg "destMutInd" - -let op_of_mind c = match kind_of_term c with - | IsMutInd (ind_sp,_) -> ind_sp - | _ -> anomaly "op_of_mind called with bad args" - -let args_of_mind c = match kind_of_term c with - | IsMutInd (_,args) -> args - | _ -> anomaly "args_of_mind called with bad args" (* Destructs a constructor *) let destMutConstruct c = match kind_of_term c with | IsMutConstruct (sp, a as r) -> r | _ -> invalid_arg "dest" -let op_of_mconstr c = match kind_of_term c with - | IsMutConstruct (sp,_) -> sp - | _ -> anomaly "op_of_mconstr called with bad args" - -let args_of_mconstr c = match kind_of_term c with - | IsMutConstruct (_,args) -> args - | _ -> anomaly "args_of_mconstr called with bad args" - let isMutConstruct c = match kind_of_term c with IsMutConstruct _ -> true | _ -> false @@ -571,16 +536,14 @@ let rec strip_head_cast c = match kind_of_term c with the usual representation of the constructions; it is not recursive *) let fold_constr f acc c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> acc + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> acc | IsCast (c,t) -> f (f acc c) t | IsProd (_,t,c) -> f (f acc t) c | IsLambda (_,t,c) -> f (f acc t) c | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c | IsApp (c,l) -> Array.fold_left f (f acc c) l | IsEvar (_,l) -> Array.fold_left f acc l - | IsConst (_,l) -> Array.fold_left f acc l - | IsMutInd (_,l) -> Array.fold_left f acc l - | IsMutConstruct (_,l) -> Array.fold_left f acc l | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl | IsFix (_,(lna,tl,bl)) -> let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in @@ -597,16 +560,14 @@ let fold_constr f acc c = match kind_of_term c with each binder traversal; it is not recursive *) let fold_constr_with_binders g f n acc c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> acc + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> acc | IsCast (c,t) -> f n (f n acc c) t | IsProd (_,t,c) -> f (g n) (f n acc t) c | IsLambda (_,t,c) -> f (g n) (f n acc t) c | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c | IsApp (c,l) -> Array.fold_left (f n) (f n acc c) l | IsEvar (_,l) -> Array.fold_left (f n) acc l - | IsConst (_,l) -> Array.fold_left (f n) acc l - | IsMutInd (_,l) -> Array.fold_left (f n) acc l - | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | IsFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in @@ -622,16 +583,14 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with not specified *) let iter_constr f c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> () + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> () | IsCast (c,t) -> f c; f t | IsProd (_,t,c) -> f t; f c | IsLambda (_,t,c) -> f t; f c | IsLetIn (_,b,t,c) -> f b; f t; f c | IsApp (c,l) -> f c; Array.iter f l | IsEvar (_,l) -> Array.iter f l - | IsConst (_,l) -> Array.iter f l - | IsMutInd (_,l) -> Array.iter f l - | IsMutConstruct (_,l) -> Array.iter f l | IsMutCase (_,p,c,bl) -> f p; f c; Array.iter f bl | IsFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | IsCoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -643,16 +602,14 @@ let iter_constr f c = match kind_of_term c with subterms are processed is not specified *) let iter_constr_with_binders g f n c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> () + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> () | IsCast (c,t) -> f n c; f n t | IsProd (_,t,c) -> f n t; f (g n) c | IsLambda (_,t,c) -> f n t; f (g n) c | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c | IsApp (c,l) -> f n c; Array.iter (f n) l | IsEvar (_,l) -> Array.iter (f n) l - | IsConst (_,l) -> Array.iter (f n) l - | IsMutInd (_,l) -> Array.iter (f n) l - | IsMutConstruct (_,l) -> Array.iter (f n) l | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl | IsFix (_,(_,tl,bl)) -> Array.iter (f n) tl; @@ -666,16 +623,14 @@ let iter_constr_with_binders g f n c = match kind_of_term c with not specified *) let map_constr f c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> c | IsCast (c,t) -> mkCast (f c, f t) | IsProd (na,t,c) -> mkProd (na, f t, f c) | IsLambda (na,t,c) -> mkLambda (na, f t, f c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) | IsApp (c,l) -> mkApp (f c, Array.map f l) | IsEvar (e,l) -> mkEvar (e, Array.map f l) - | IsConst (c,l) -> mkConst (c, Array.map f l) - | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) - | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl) | IsFix (ln,(lna,tl,bl)) -> mkFix (ln,(lna,Array.map f tl,Array.map f bl)) @@ -689,16 +644,14 @@ let map_constr f c = match kind_of_term c with subterms are processed is not specified *) let map_constr_with_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c) | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al) | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) - | IsConst (c,al) -> mkConst (c, Array.map (f l) al) - | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) - | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) | IsFix (ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in @@ -714,16 +667,14 @@ let map_constr_with_binders g f l c = match kind_of_term c with and the order with which subterms are processed is not specified *) let map_constr_with_named_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al) | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) - | IsConst (c,al) -> mkConst (c, Array.map (f l) al) - | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) - | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) | IsFix (ln,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in @@ -765,7 +716,8 @@ let array_map_left_pair f a g b = end let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> c | IsCast (c,t) -> let c' = f l c in mkCast (c', f l t) | IsProd (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c) | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c) @@ -774,9 +726,6 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with | IsApp (c,al) -> let c' = f l c in mkApp (c', array_map_left (f l) al) | IsEvar (e,al) -> mkEvar (e, array_map_left (f l) al) - | IsConst (c,al) -> mkConst (c, array_map_left (f l) al) - | IsMutInd (c,al) -> mkMutInd (c, array_map_left (f l) al) - | IsMutConstruct (c,al) -> mkMutConstruct (c, array_map_left (f l) al) | IsMutCase (ci,p,c,bl) -> let p' = f l p in let c' = f l c in mkMutCase (ci, p', c', array_map_left (f l) bl) @@ -791,16 +740,14 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with (* strong *) let map_constr_with_full_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c + | (IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsConst _ | IsMutInd _ + | IsMutConstruct _) -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c) | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al) | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) - | IsConst (c,al) -> mkConst (c, Array.map (f l) al) - | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) - | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) | IsFix (ln,(lna,tl,bl)) -> let l' = @@ -837,10 +784,9 @@ let compare_constr f t1 t2 = f h1 h2 & List.for_all2 f l1 l2 else false | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | IsConst (c1,l1), IsConst (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2 - | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2 - | IsMutConstruct (c1,l1), IsMutConstruct (c2,l2) -> - c1 = c2 & array_for_all2 f l1 l2 + | IsConst c1, IsConst c2 -> c1 = c2 + | IsMutInd c1, IsMutInd c2 -> c1 = c2 + | IsMutConstruct c1, IsMutConstruct c2 -> c1 = c2 | IsMutCase (_,p1,c1,bl1), IsMutCase (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 | IsFix (ln1,(_,tl1,bl1)), IsFix (ln2,(_,tl2,bl2)) -> @@ -1421,25 +1367,6 @@ let le_kind_implicit k1 k2 = (k1=mkImplicit) or (isprop k1) or (k2=mkImplicit) or (is_Type k2) -(* Returns the list of global variables in a term *) - -let rec global_varsl l constr = match kind_of_term constr with - | IsVar id -> id::l - | _ -> fold_constr global_varsl l constr - -let global_vars = global_varsl [] - -let global_vars_decl = function - | (_, None, t) -> global_vars t - | (_, Some c, t) -> (global_vars c)@(global_vars t) - -let global_vars_set constr = - let rec filtrec acc c = match kind_of_term c with - | IsVar id -> Idset.add id acc - | _ -> fold_constr filtrec acc c - in - filtrec Idset.empty constr - (* Rem: end of import from old module Generic *) (* Various occurs checks *) @@ -1448,7 +1375,7 @@ let global_vars_set constr = * false otherwise *) let occur_const s c = let rec occur_rec c = match kind_of_term c with - | IsConst (sp,_) when sp=s -> raise Occur + | IsConst sp when sp=s -> raise Occur | _ -> iter_constr occur_rec c in try occur_rec c; false with Occur -> true @@ -1460,18 +1387,6 @@ let occur_evar n c = in try occur_rec c; false with Occur -> true -let occur_var s c = - let rec occur_rec c = match kind_of_term c with - | IsVar id when id=s -> raise Occur - | _ -> iter_constr occur_rec c - in - try occur_rec c; false with Occur -> true - -let occur_var_in_decl hyp (_,c,typ) = - match c with - | None -> occur_var hyp (body_of_type typ) - | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body - (***************************************) (* alpha and eta conversion functions *) (***************************************) @@ -1529,23 +1444,6 @@ let eta_eq_constr = in aux -(* This renames bound variables with fresh and distinct names *) -(* in such a way that the printer doe not generate new names *) -(* and therefore that printed names are the intern names *) -(* In this way, tactics such as Induction works well *) - -let rec rename_bound_var l c = - match kind_of_term c with - | IsProd (Name s,c1,c2) -> - if dependent (mkRel 1) c2 then - let s' = next_ident_away s (global_vars c2@l) in - mkProd (Name s', c1, rename_bound_var (s'::l) c2) - else - mkProd (Name s, c1, rename_bound_var l c2) - | IsProd (Anonymous,c1,c2) -> mkProd (Anonymous, c1, rename_bound_var l c2) - | IsCast (c,t) -> mkCast (rename_bound_var l c, t) - | x -> c - (***************************) (* substitution functions *) (***************************) @@ -1789,10 +1687,10 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpApp | OpConst of constant_path + | OpApp | OpConst of constant | OpEvar of existential_key - | OpMutInd of inductive_path - | OpMutConstruct of constructor_path + | OpMutInd of inductive + | OpMutConstruct of constructor | OpMutCase of case_info | OpRec of fix_kind * name array @@ -1806,10 +1704,10 @@ let splay_constr c = match kind_of_term c with | IsLambda (x, t1, t2) -> OpLambda x, [|t1;t2|] | IsLetIn (x, b, t1, t2) -> OpLetIn x, [|b;t1;t2|] | IsApp (f,a) -> OpApp, Array.append [|f|] a - | IsConst (sp, a) -> OpConst sp, a + | IsConst sp -> OpConst sp,[||] | IsEvar (sp, a) -> OpEvar sp, a - | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, l - | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, l + | IsMutInd ind_sp -> OpMutInd ind_sp,[||] + | IsMutConstruct cstr_sp -> OpMutConstruct cstr_sp, [||] | IsMutCase (ci,p,c,bl) -> OpMutCase ci, Array.append [|p;c|] bl | IsFix (fi,(lna,tl,bl)) -> OpRec (RFix fi,lna), Array.append tl bl | IsCoFix (fi,(lna,tl,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl @@ -1824,10 +1722,10 @@ let gather_constr = function | OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2) | OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2) | OpApp, v -> let f = v.(0) and a = array_tl v in mkApp (f, a) - | OpConst sp, a -> mkConst (sp, a) + | OpConst sp, [||] -> mkConst sp | OpEvar sp, a -> mkEvar (sp, a) - | OpMutInd ind_sp, l -> mkMutInd (ind_sp, l) - | OpMutConstruct cstr_sp, l -> mkMutConstruct (cstr_sp, l) + | OpMutInd ind_sp, [||] -> mkMutInd ind_sp + | OpMutConstruct cstr_sp, [||] -> mkMutConstruct cstr_sp | OpMutCase ci, v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) @@ -1849,10 +1747,10 @@ let splay_constr_with_binders c = match kind_of_term c with | IsLambda (x, t1, t2) -> OpLambda x, [x,None,t1], [|t2|] | IsLetIn (x, b, t1, t2) -> OpLetIn x, [x,Some b,t1], [|t2|] | IsApp (f,v) -> OpApp, [], Array.append [|f|] v - | IsConst (sp, a) -> OpConst sp, [], a + | IsConst sp -> OpConst sp, [], [||] | IsEvar (sp, a) -> OpEvar sp, [], a - | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, [], l - | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, [], l + | IsMutInd ind_sp -> OpMutInd ind_sp, [], [||] + | IsMutConstruct cstr_sp -> OpMutConstruct cstr_sp, [], [||] | IsMutCase (ci,p,c,bl) -> let v = Array.append [|p;c|] bl in OpMutCase ci, [], v | IsFix (fi,(na,tl,bl)) -> @@ -1878,10 +1776,10 @@ let gather_constr_with_binders = function | OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2) | OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2) | OpApp, [], v -> let f = v.(0) and a = array_tl v in mkApp (f, a) - | OpConst sp, [], a -> mkConst (sp, a) + | OpConst sp, [], [||] -> mkConst sp | OpEvar sp, [], a -> mkEvar (sp, a) - | OpMutInd ind_sp, [], l -> mkMutInd (ind_sp, l) - | OpMutConstruct cstr_sp, [], l -> mkMutConstruct (cstr_sp, l) + | OpMutInd ind_sp, [], [||] -> mkMutInd ind_sp + | OpMutConstruct cstr_sp, [], [||] -> mkMutConstruct cstr_sp | OpMutCase ci, [], v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) diff --git a/kernel/term.mli b/kernel/term.mli index ca0bae838..248d57227 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -41,7 +41,7 @@ type existential_key = int type pattern_source = DefaultPat of int | RegularPat type case_style = PrintLet | PrintIf | PrintCases type case_printing = - inductive_path * identifier array * int + inductive * identifier array * int * case_style option * pattern_source array (* the integer is the number of real args, needed for reduction *) type case_info = int * case_printing @@ -52,9 +52,6 @@ sig (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr existential = existential_key * 'constr array -type 'constr constant = constant_path * 'constr array -type 'constr constructor = constructor_path * 'constr array -type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = name array * 'types array * 'constr array type ('constr, 'types) fixpoint = @@ -71,9 +68,9 @@ end type global_reference = | VarRef of section_path - | ConstRef of constant_path - | IndRef of inductive_path - | ConstructRef of constructor_path + | ConstRef of constant + | IndRef of inductive + | ConstructRef of constructor (*s*******************************************************************) (* The type of constructions *) @@ -121,17 +118,14 @@ type ('constr, 'types) kind_of_term = | IsLetIn of name * 'constr * 'types * 'constr | IsApp of 'constr * 'constr array | IsEvar of 'constr existential - | IsConst of 'constr constant - | IsMutInd of 'constr inductive - | IsMutConstruct of 'constr constructor + | IsConst of constant + | IsMutInd of inductive + | IsMutConstruct of constructor | IsMutCase of case_info * 'constr * 'constr * 'constr array | IsFix of ('constr, 'types) fixpoint | IsCoFix of ('constr, 'types) cofixpoint type existential = existential_key * constr array -type constant = constant_path * constr array -type constructor = constructor_path * constr array -type inductive = inductive_path * constr array type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -327,10 +321,8 @@ i*) val destApplication : constr -> constr * constr array (* Destructs a constant *) -val destConst : constr -> constant_path * constr array +val destConst : constr -> constant val isConst : constr -> bool -val path_of_const : constr -> constant_path -val args_of_const : constr -> constr array (* Destructs an existential variable *) val destEvar : constr -> existential_key * constr array @@ -338,14 +330,10 @@ val num_of_evar : constr -> existential_key (* Destructs a (co)inductive type *) val destMutInd : constr -> inductive -val op_of_mind : constr -> inductive_path -val args_of_mind : constr -> constr array (* Destructs a constructor *) val destMutConstruct : constr -> constructor val isMutConstruct : constr -> bool -val op_of_mconstr : constr -> constructor_path -val args_of_mconstr : constr -> constr array (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) val destCase : constr -> case_info * constr * constr * constr array @@ -479,14 +467,6 @@ val subst1 : constr -> constr -> constr val substl_decl : constr list -> named_declaration -> named_declaration val subst1_decl : constr -> named_declaration -> named_declaration -(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *) -val global_vars : constr -> identifier list - -(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR - id] in declaration [d] (type and body if any) *) -val global_vars_decl : named_declaration -> identifier list - -val global_vars_set : constr -> Idset.t val replace_vars : (identifier * constr) list -> constr -> constr val subst_var : identifier -> constr -> constr @@ -518,25 +498,18 @@ val occur_existential : constr -> bool (* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs in c, [false] otherwise *) -val occur_const : constant_path -> constr -> bool +val occur_const : constant -> constr -> bool (* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs in c, [false] otherwise *) val occur_evar : existential_key -> constr -> bool -(* [(occur_var id c)] returns [true] if variable [id] occurs free - in c, [false] otherwise *) -val occur_var : identifier -> constr -> bool - -val occur_var_in_decl : identifier -> named_declaration -> bool - (* [dependent M N] is true iff M is eq\_constr with a subterm of N M is appropriately lifted through abstractions of N *) val dependent : constr -> constr -> bool (* strips head casts and flattens head applications *) val strip_head_cast : constr -> constr -val rename_bound_var : identifier list -> constr -> constr val eta_reduce_head : constr -> constr val eq_constr : constr -> constr -> bool val eta_eq_constr : constr -> constr -> bool @@ -566,10 +539,10 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpApp | OpConst of constant_path + | OpApp | OpConst of constant | OpEvar of existential_key - | OpMutInd of inductive_path - | OpMutConstruct of constructor_path + | OpMutInd of inductive + | OpMutConstruct of constructor | OpMutCase of case_info | OpRec of fix_kind * name array diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4342b5793..e8e8f35b9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -460,7 +460,7 @@ let check_term env mind_recvec f = Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b) | Imbr((sp,i) as ind_sp,lrc) -> let sprecargs = - mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in + mis_recargs (lookup_mind_specif ind_sp env) in let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) in crec env' n' ((1,lc)::lst') (lr,b) @@ -589,7 +589,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = anomaly "check_subterm_rec_meta: Bad occurrence of recursive call" | _ -> raise (FixGuardError NotEnoughAbstractionInFixBody) in let (env',c,d) = check_occur env 1 def in - let ((sp,tyi),_ as mind, largs) = + let ((sp,tyi) as mind, largs) = try find_inductive env' sigma c with Induc -> raise (FixGuardError RecursionNotOnInductiveType) in let mind_recvec = mis_recargs (lookup_mind_specif mind env') in @@ -690,17 +690,14 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsLetIn (x,a,b,c) -> anomaly "check_rec_call: should have been reduced" - | IsMutInd (_,la) -> - (array_for_all (check_rec_call env n lst) la) && + | IsMutInd _ -> (List.for_all (check_rec_call env n lst) l) - | IsMutConstruct (_,la) -> - (array_for_all (check_rec_call env n lst) la) && + | IsMutConstruct _ -> (List.for_all (check_rec_call env n lst) l) - | IsConst (sp,la) as c -> + | IsConst sp -> (try - (array_for_all (check_rec_call env n lst) la) && (List.for_all (check_rec_call env n lst) l) with (FixGuardError _ ) as e -> if evaluable_constant env sp then @@ -791,7 +788,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = raise (CoFixGuardError (CodomainNotInductiveType b)) in let (mind, _) = codomain_is_coind env deftype in - let ((sp,tyi),_) = mind in + let (sp,tyi) = mind in let lvlra = mis_recargs (lookup_mind_specif mind env) in let vlra = lvlra.(tyi) in let rec check_rec_call env alreadygrd n vlra t = @@ -815,9 +812,9 @@ let check_guard_rec_meta env sigma nbfix def deftype = else error "check_guard_rec_meta: ???" (* ??? *) - | IsMutConstruct ((_,i as cstr_sp),l) -> + | IsMutConstruct (_,i as cstr_sp) -> let lra =vlra.(i-1) in - let mI = inductive_of_constructor (cstr_sp,l) in + let mI = inductive_of_constructor cstr_sp in let mis = lookup_mind_specif mI env in let _,realargs = list_chop (mis_nparams mis) args in let rec process_args_of_constr l lra = @@ -835,8 +832,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = (process_args_of_constr lr lrar) | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> - let mis = - lookup_mind_specif (ind_sp,[||]) env in + let mis = lookup_mind_specif ind_sp env in let sprecargs = mis_recargs mis in let lc = (Array.map (List.map @@ -934,6 +930,9 @@ let control_only_guard env sigma = let rec control_rec c = match kind_of_term c with | IsRel _ | IsVar _ -> () | IsSort _ | IsMeta _ -> () + | IsMutInd _ -> () + | IsMutConstruct _ -> () + | IsConst _ -> () | IsCoFix (_,(_,tys,bds) as cofix) -> check_cofix env sigma cofix; Array.iter control_rec tys; @@ -943,9 +942,6 @@ let control_only_guard env sigma = Array.iter control_rec tys; Array.iter control_rec bds; | IsMutCase(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b - | IsMutInd (_,cl) -> Array.iter control_rec cl - | IsMutConstruct (_,cl) -> Array.iter control_rec cl - | IsConst (_,cl) -> Array.iter control_rec cl | IsEvar (_,cl) -> Array.iter control_rec cl | IsApp (_,cl) -> Array.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 diff --git a/library/declare.ml b/library/declare.ml index b10658466..19c7323c9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -459,18 +459,17 @@ let constr_of_reference _ _ ref = if Options.immediate_discharge then match ref with | VarRef sp -> mkVar (basename sp) - | ConstRef sp -> mkConst (sp,[||]) - | ConstructRef sp -> mkMutConstruct (sp,[||]) - | IndRef sp -> mkMutInd (sp,[||]) + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkMutConstruct sp + | IndRef sp -> mkMutInd sp else let hyps = context_of_global_reference ref in let hyps0 = current_section_context () in - let args = instance_from_section_context hyps in let body = match ref with | VarRef sp -> mkVar (basename sp) - | ConstRef sp -> mkConst (sp,Array.of_list args) - | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args) - | IndRef sp -> mkMutInd (sp,Array.of_list args) + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkMutConstruct sp + | IndRef sp -> mkMutInd sp in find_common_hyps_then_abstract body hyps0 hyps @@ -565,7 +564,7 @@ let declare_one_elimination mispec = let mindstr = string_of_id (mis_typename mispec) in let declare na c = (* Hack to get const_hyps right in the declaration *) - let c = instantiate_inductive_section_params c (fst (mis_inductive mispec)) + let c = instantiate_inductive_section_params c (mis_inductive mispec) in let _ = declare_constant (id_of_string na) (ConstantEntry @@ -594,16 +593,15 @@ let declare_eliminations sp = if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then error ("Declarations of elimination scheme outside the section "^ "of the inductive definition is not implemented"); *) - let ctxt = instance_from_section_context mib.mind_hyps in for i = 0 to Array.length mib.mind_packets - 1 do if mind_type_finite mib i then - let mispec = Global.lookup_mind_specif ((sp,i), Array.of_list ctxt) in + let mispec = Global.lookup_mind_specif (sp,i) in declare_one_elimination mispec done (* Look up function for the default elimination constant *) -let lookup_eliminator env (ind_sp,_) s = +let lookup_eliminator env ind_sp s = let path = path_of_inductive_path ind_sp in let dir, base,k = repr_path path in let id = add_suffix base (elimination_suffix s) in diff --git a/library/declare.mli b/library/declare.mli index 5563ebe9e..6918c99db 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -35,7 +35,7 @@ type section_variable_entry = type variable_declaration = section_variable_entry * strength -val declare_variable : identifier -> variable_declaration -> variable_path +val declare_variable : identifier -> variable_declaration -> variable type constant_declaration_type = | ConstantEntry of constant_entry @@ -46,20 +46,20 @@ type constant_declaration = constant_declaration_type * strength (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> constant_path +val declare_constant : identifier -> constant_declaration -> constant -val redeclare_constant : constant_path -> constant_declaration -> unit +val redeclare_constant : constant -> constant_declaration -> unit -val declare_parameter : identifier -> constr -> constant_path +val declare_parameter : identifier -> constr -> constant (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block *) -val declare_mind : mutual_inductive_entry -> mutual_inductive_path +val declare_mind : mutual_inductive_entry -> mutual_inductive (* [declare_eliminations sp] declares elimination schemes associated to the mutual inductive block refered by [sp] *) -val declare_eliminations : mutual_inductive_path -> unit +val declare_eliminations : mutual_inductive -> unit val out_inductive : Libobject.obj -> mutual_inductive_entry @@ -70,15 +70,15 @@ val make_strength_2 : unit -> strength (*s Corresponding test and access functions. *) val is_constant : section_path -> bool -val constant_strength : constant_path -> strength -val constant_or_parameter_strength : constant_path -> strength +val constant_strength : constant -> strength +val constant_or_parameter_strength : constant -> strength val out_variable : Libobject.obj -> identifier * variable_declaration -val get_variable : variable_path -> named_declaration * strength +val get_variable : variable -> named_declaration * strength val get_variable_with_constraints : - variable_path -> named_declaration * Univ.constraints * strength -val variable_strength : variable_path -> strength -val find_section_variable : identifier -> variable_path + variable -> named_declaration * Univ.constraints * strength +val variable_strength : variable -> strength +val find_section_variable : identifier -> variable val last_section_hyps : dir_path -> identifier list (*s [global_reference k id] returns the object corresponding to @@ -90,7 +90,7 @@ val last_section_hyps : dir_path -> identifier list given environment instead of looking in the current global environment. *) val context_of_global_reference : global_reference -> section_context -val instantiate_inductive_section_params : constr -> inductive_path -> constr +val instantiate_inductive_section_params : constr -> inductive -> constr val implicit_section_args : global_reference -> section_path list val extract_instance : global_reference -> constr array -> constr array @@ -110,8 +110,8 @@ val construct_reference : Environ.env -> path_kind -> identifier -> constr val is_global : identifier -> bool -val path_of_inductive_path : inductive_path -> mutual_inductive_path -val path_of_constructor_path : constructor_path -> mutual_inductive_path +val path_of_inductive_path : inductive -> mutual_inductive +val path_of_constructor_path : constructor -> mutual_inductive (* Look up function for the default elimination constant *) val elimination_suffix : sorts_family -> string diff --git a/library/impargs.ml b/library/impargs.ml index d71acd70f..63351392e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -126,7 +126,7 @@ let constant_implicits_list sp = implicit arguments of the constructors. *) module Inductive_path = struct - type t = inductive_path + type t = inductive let compare (spx,ix) (spy,iy) = let c = ix - iy in if c = 0 then sp_ord spx spy else c end @@ -136,7 +136,7 @@ module Indmap = Map.Make(Inductive_path) let inductives_table = ref Indmap.empty module Construtor_path = struct - type t = constructor_path + type t = constructor let compare (indx,ix) (indy,iy) = let c = ix - iy in if c = 0 then Inductive_path.compare indx indy else c end @@ -269,18 +269,15 @@ let context_of_global_reference = function | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps let type_of_global r = - let args = - Array.of_list - (Sign.instance_from_section_context (context_of_global_reference r)) in match r with | VarRef sp -> lookup_named_type (basename sp) (Global.env ()) | ConstRef sp -> - Typeops.type_of_constant (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_constant (Global.env ()) Evd.empty sp | IndRef sp -> - Typeops.type_of_inductive (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_inductive (Global.env ()) Evd.empty sp | ConstructRef sp -> - Typeops.type_of_constructor (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_constructor (Global.env ()) Evd.empty sp let check_range n i = if i<1 or i>n then error ("Bad argument number: "^(string_of_int i)) diff --git a/library/impargs.mli b/library/impargs.mli index 9b8d0616d..ceaa30cdf 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -33,9 +33,9 @@ val compute_implicits : env -> 'a Evd.evar_map -> types -> implicits_list (*s Computation of implicits (done using the global environment). *) -val declare_var_implicits : variable_path -> unit -val declare_constant_implicits : constant_path -> unit -val declare_mib_implicits : mutual_inductive_path -> unit +val declare_var_implicits : variable -> unit +val declare_constant_implicits : constant -> unit +val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : global_reference -> unit (* Manual declaration of which arguments are expected implicit *) @@ -43,15 +43,15 @@ val declare_manual_implicits : global_reference -> implicits_list -> unit (*s Access to already computed implicits. *) -val constructor_implicits_list : constructor_path -> implicits_list -val inductive_implicits_list : inductive_path -> implicits_list -val constant_implicits_list : constant_path -> implicits_list +val constructor_implicits_list : constructor -> implicits_list +val inductive_implicits_list : inductive -> implicits_list +val constant_implicits_list : constant -> implicits_list -val implicits_of_var : variable_path -> implicits_list +val implicits_of_var : variable -> implicits_list -val is_implicit_constant : constant_path -> bool -val is_implicit_inductive_definition : inductive_path -> bool -val is_implicit_var : variable_path -> bool +val is_implicit_constant : constant -> bool +val is_implicit_inductive_definition : inductive -> bool +val is_implicit_var : variable -> bool val implicits_of_global : global_reference -> implicits_list diff --git a/library/indrec.ml b/library/indrec.ml index 96a188da7..36ce4f783 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -319,7 +319,7 @@ let mis_make_indrec env sigma listdepkind mispec = it_mkLambda_or_LetIn_name env (lambda_create env (build_dependent_inductive - (lift_inductive_family nrec indf), + (lift_inductive_family nrec indf), mkMutCase (make_default_case_info mispeci, mkRel (dect+j+1), mkRel 1, branches))) (Sign.lift_rel_context nrec lnames) @@ -443,13 +443,13 @@ let check_arities listdepkind = let build_mutual_indrec env sigma = function | (mind,dep,s)::lrecspec -> - let ((sp,tyi),_) = mind in + let (sp,tyi) = mind in let mispec = lookup_mind_specif mind env in let listdepkind = (mispec, dep,s):: (List.map (function (mind',dep',s') -> - let ((sp',_),_) = mind' in + let (sp',_) = mind' in if sp=sp' then (lookup_mind_specif mind' env,dep',s') else diff --git a/library/nametab.mli b/library/nametab.mli index 7d0f164f9..f34895bef 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -70,7 +70,7 @@ val extended_locate : qualid -> extended_global_reference val locate_obj : qualid -> section_path -val locate_constant : qualid -> constant_path +val locate_constant : qualid -> constant val locate_section : qualid -> dir_path (* [exists sp] tells if [sp] is already bound to a cci term *) diff --git a/parsing/astterm.ml b/parsing/astterm.ml index bfd4e6685..81fdc9229 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -156,7 +156,7 @@ let ids_of_ctxt ctxt = ctxt) type pattern_qualid_kind = - | IsConstrPat of loc * (constructor_path * identifier list) + | IsConstrPat of loc * constructor | IsVarPat of loc * identifier let maybe_constructor env = function @@ -164,8 +164,7 @@ let maybe_constructor env = function let qid = interp_qualid l in (try match kind_of_term (global_qualified_reference qid) with - | IsMutConstruct ((spi,j),cl) -> - IsConstrPat (loc,((spi,j),ids_of_ctxt cl)) + | IsMutConstruct c -> IsConstrPat (loc,c) | _ -> (match maybe_variable l with | Some s -> @@ -183,13 +182,13 @@ let maybe_constructor env = function (* This may happen in quotations *) | Node(loc,"MUTCONSTRUCT",[sp;Num(_,ti);Num(_,n)]) -> (* Buggy: needs to compute the context *) - IsConstrPat (loc,(((ast_to_sp sp,ti),n),[])) + IsConstrPat (loc,((ast_to_sp sp,ti),n)) | Path(loc,sp) -> (match absolute_reference sp with - | ConstructRef (spi,j) -> - IsConstrPat (loc,((spi,j),[])) - | _ -> error ("Unknown absolute constructor name: "^(string_of_path sp))) + | ConstructRef c -> IsConstrPat (loc,c) + | _ -> + error ("Unknown absolute constructor name: "^(string_of_path sp))) | Node(loc,("CONST"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) -> user_err_loc (loc,"ast_to_pattern", diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index ab9153705..7c6dad215 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -105,9 +105,7 @@ let print_constructors envpar names types = in hV 0 [< 'sTR " "; pc >] let build_inductive sp tyi = - let ctxt = context_of_global_reference (IndRef (sp,tyi)) in - let ctxt = Array.of_list (instance_from_section_context ctxt) in - let mis = Global.lookup_mind_specif ((sp,tyi),ctxt) in + let mis = Global.lookup_mind_specif (sp,tyi) in let params = mis_params_ctxt mis in let args = extended_rel_list 0 params in let indf = make_ind_family (mis,args) in @@ -460,13 +458,13 @@ let print_opaque_name qid = try let x = global_qualified_reference qid in match kind_of_term x with - | IsConst (sp,_ as cst) -> - let cb = Global.lookup_constant sp in + | IsConst cst -> + let cb = Global.lookup_constant cst in if is_defined cb then - print_constant true " = " sp + print_constant true " = " cst else error "not a defined constant" - | IsMutInd ((sp,_),_) -> + | IsMutInd (sp,_) -> print_mutual sp | IsMutConstruct cstr -> let ty = Typeops.type_of_constructor env sigma cstr in diff --git a/parsing/printer.ml b/parsing/printer.ml index b1d85e53a..2d01371a5 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -123,9 +123,9 @@ let pr_constructor env cstr = open Pattern let pr_ref_label = function (* On triche sur le contexte *) - | ConstNode sp -> pr_constant (Global.env()) (sp,[||]) - | IndNode sp -> pr_inductive (Global.env()) (sp,[||]) - | CstrNode sp -> pr_constructor (Global.env()) (sp,[||]) + | ConstNode sp -> pr_constant (Global.env()) sp + | IndNode sp -> pr_inductive (Global.env()) sp + | CstrNode sp -> pr_constructor (Global.env()) sp | VarNode id -> pr_id id let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t) diff --git a/parsing/search.ml b/parsing/search.ml index f9ad43abe..e0dc3b7a4 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -68,7 +68,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = (Name mip.mind_typename, None, mip.mind_nf_arity)) mib.mind_packets in (match kind_of_term const with - | IsMutInd ((sp',tyi) as indsp,_) -> + | IsMutInd ((sp',tyi) as indsp) -> if sp=sp' then print_constructors indsp fn env (mind_nth_type_packet mib tyi) @@ -92,7 +92,7 @@ let rec head c = | _ -> c let constr_to_section_path c = match kind_of_term c with - | IsConst (sp,_) -> sp + | IsConst sp -> sp | _ -> raise No_section_path let xor a b = (a or b) & (not (a & b)) diff --git a/parsing/termast.ml b/parsing/termast.ml index 922c09d28..d84c5e952 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -116,12 +116,12 @@ let ast_of_qualid p = let rec ast_of_cases_pattern = function (* loc is thrown away for printing *) | PatVar (loc,Name id) -> nvar id | PatVar (loc,Anonymous) -> nvar wildcard - | PatCstr(loc,(cstrsp,_),args,Name id) -> + | PatCstr(loc,cstrsp,args,Name id) -> let args = List.map ast_of_cases_pattern args in ope("PATTAS", [nvar id; ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)]) - | PatCstr(loc,(cstrsp,_),args,Anonymous) -> + | PatCstr(loc,cstrsp,args,Anonymous) -> ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp) :: List.map ast_of_cases_pattern args) @@ -303,11 +303,9 @@ let ast_of_constr at_top env t = ast_of_raw (Detyping.detype avoid (names_of_rel_context env) t') -let ast_of_constant env (sp,ids) = +let ast_of_constant env sp = let a = ast_of_constant_ref sp in - if !print_arguments then - ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) - else a + a let ast_of_existential env (ev,ids) = let a = ast_of_existential_ref ev in @@ -315,17 +313,13 @@ let ast_of_existential env (ev,ids) = ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) else a -let ast_of_constructor env (cstr_sp,ids) = +let ast_of_constructor env cstr_sp = let a = ast_of_constructor_ref cstr_sp in - if !print_arguments then - ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) - else a + a -let ast_of_inductive env (ind_sp,ids) = +let ast_of_inductive env ind_sp = let a = ast_of_inductive_ref ind_sp in - if !print_arguments then - ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) - else a + a let decompose_binder_pattern = function | PProd(na,ty,c) -> Some (BProd,na,ty,c) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ee1d2ae52..ac9777a14 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -30,7 +30,7 @@ open Evarconv type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor_path * int + | WrongNumargConstructor of constructor * int | WrongPredicateArity of constr * constr * constr | NeedsInversion of constr * constr | UnusedClause of cases_pattern list @@ -68,7 +68,7 @@ let norec_branch_scheme env isevars cstr = | [] -> mkExistential isevars env in crec env (List.rev cstr.cs_args) -let rec_branch_scheme env isevars ((sp,j),_) recargs cstr = +let rec_branch_scheme env isevars (sp,j) recargs cstr = let rec crec env (args,recargs) = match args, recargs with | (name,None,c as d)::rea,(ra::reca) -> @@ -182,16 +182,6 @@ let mssg_this_case_cannot_occur () = "This pattern-matching is not exhaustive." (* Utils *) - -let ids_of_ctxt ids = - try Array.to_list (Array.map destVar ids) - with _ -> anomaly "Context of constructor is not built from Var" -let ctxt_of_ids ids = Array.of_list (List.map mkVar ids) -let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids) -let rawconstructor_of_constructor (cstr_sp,ctxt) = (cstr_sp,ids_of_ctxt ctxt) -let inductive_of_rawconstructor c = - inductive_of_constructor (constructor_of_rawconstructor c) - let make_anonymous_patvars = list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous)) @@ -266,7 +256,7 @@ type alias_constr = type alias_builder = | AliasLeaf of constr - | AliasConstructor of alias_constr * (constructor_path * identifier list) + | AliasConstructor of alias_constr * constructor type history_partial_result = | HistoryArg of (constr * cases_pattern) @@ -490,10 +480,10 @@ let pattern_status pats = (* Well-formedness tests *) (* Partial check on patterns *) -let check_constructor loc ((_,j as cstr_sp,ids),args) mind cstrs = +let check_constructor loc (_,j as cstr_sp) mind cstrs args = (* Check it is constructor of the right type *) - if inductive_path_of_constructor_path cstr_sp <> fst mind - then error_bad_constructor_loc loc (cstr_sp,ctxt_of_ids ids) mind; + if inductive_of_constructor cstr_sp <> mind + then error_bad_constructor_loc loc cstr_sp mind; (* Check the constructor has the right number of args *) let nb_args_constr = cstrs.(j-1).cs_nargs in if List.length args <> nb_args_constr @@ -503,8 +493,8 @@ let check_all_variables typ mat = List.iter (fun eqn -> match current_pattern eqn with | PatVar (_,id) -> () - | PatCstr (loc,(cstr_sp,ids),_,_) -> - error_bad_pattern_loc loc (cstr_sp,ctxt_of_ids ids) typ) + | PatCstr (loc,cstr_sp,_,_) -> + error_bad_pattern_loc loc cstr_sp typ) mat let check_unused_pattern env eqn = @@ -1048,9 +1038,9 @@ let group_equations mind current cstrs mat = let rest = {rest with tag = lower_pattern_status rest.tag} in brs.(i-1) <- (args, rest) :: brs.(i-1) done - | PatCstr(loc,((ind_sp,i),ids as cstr),largs,alias) -> + | PatCstr(loc,((ind_sp,i) as cstr),largs,alias) -> (* This is a regular clause *) - check_constructor loc (cstr,largs) mind cstrs; + check_constructor loc cstr mind cstrs largs; only_default := false; brs.(i-1) <- (largs,rest) :: brs.(i-1)) mat () in (brs,!only_default) @@ -1087,8 +1077,7 @@ let build_branch current pb eqns const_info = DepAlias (applist (mkMutConstruct const_info.cs_cstr, params)) in let history = push_history_pattern const_info.cs_nargs - (AliasConstructor - (partialci, rawconstructor_of_constructor const_info.cs_cstr)) + (AliasConstructor (partialci, const_info.cs_cstr)) pb.history in (* We find matching clauses *) @@ -1350,7 +1339,7 @@ let coerce_row typing_fun isevars env cstropt tomatch = let typ = body_of_type j.uj_type in let t = match cstropt with | Some (cloc,(cstr,_ as c)) -> - (let tyi = inductive_of_rawconstructor c in + (let tyi = inductive_of_constructor c in try let indtyp = inh_coerce_to_ind isevars env typ tyi in IsInd (typ,find_rectype env (evars_of isevars) typ) @@ -1358,8 +1347,7 @@ let coerce_row typing_fun isevars env cstropt tomatch = (* 2 cases : Not the right inductive or not an inductive at all *) try let mind,_ = find_mrectype env (evars_of isevars) typ in - error_bad_constructor_loc cloc - (constructor_of_rawconstructor c) mind + error_bad_constructor_loc cloc c mind with Induc -> error_case_not_inductive_loc (loc_of_rawconstr tomatch) CCI env (evars_of isevars) j) @@ -1381,7 +1369,7 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl = let build_expected_arity env isevars isdep tomatchl = let cook n = function | _,IsInd (_,IndType(indf,_)) -> - let indf' = lift_inductive_family n indf in + let indf' = lift_inductive_family n indf in Some (build_dependent_inductive indf', fst (get_arity indf')) | _,NotInd _ -> None in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7e5fda903..e44bda7d2 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -21,7 +21,7 @@ open Evarutil type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor_path * int + | WrongNumargConstructor of constructor * int | WrongPredicateArity of constr * constr * constr | NeedsInversion of constr * constr | UnusedClause of cases_pattern list diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 77370dedc..c4f5b13a4 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -34,8 +34,7 @@ open Esubst * FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under * the substitution S, and then applied to args. Here again, * weak reduction. - * CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th - * inductive type sp. + * CONSTR(c,args) is the constructor [c] applied to [args]. * * Note that any term has not an equivalent in cbv_value: for example, * a product (x:A)B must be in normal form because only VAL may @@ -49,7 +48,7 @@ type cbv_value = | LAM of name * constr * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value list | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of int * inductive_path * cbv_value array * cbv_value list + | CONSTR of constructor * cbv_value list (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) @@ -64,9 +63,8 @@ let rec shift_value n = function FIXP (fix,subs_shft (n,s), List.map (shift_value n) args) | COFIXP (cofix,s,args) -> COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args) - | CONSTR (i,spi,vars,args) -> - CONSTR (i, spi, Array.map (shift_value n) vars, - List.map (shift_value n) args) + | CONSTR (c,args) -> + CONSTR (c, List.map (shift_value n) args) (* Contracts a fixpoint: given a fixpoint and a substitution, @@ -142,7 +140,7 @@ let red_allowed_ref flags stack = function | FarRelBinding _ -> red_allowed flags stack fDELTA | VarBinding id -> red_allowed flags stack (fVAR id) | EvarBinding _ -> red_allowed flags stack fEVAR - | ConstBinding (sp,_) -> red_allowed flags stack (fCONST sp) + | ConstBinding sp -> red_allowed flags stack (fCONST sp) (* Transfer application lists from a value to the stack * useful because fixpoints may be totally applied in several times @@ -151,7 +149,7 @@ let strip_appl head stack = match head with | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack) | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack) - | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack) + | CONSTR (c,app) -> (CONSTR(c,[]), stack_app app stack) | _ -> (head, stack) @@ -232,9 +230,8 @@ let rec norm_head info env t stack = | IsVar id -> norm_head_ref 0 info env stack (VarBinding id) - | IsConst (sp,vars) -> - let normt = (sp,Array.map (cbv_norm_term info env) vars) in - norm_head_ref 0 info env stack (ConstBinding normt) + | IsConst sp -> + norm_head_ref 0 info env stack (ConstBinding sp) | IsEvar (ev,args) -> let evar = (ev, Array.map (cbv_norm_term info env) args) in @@ -262,13 +259,10 @@ let rec norm_head info env t stack = | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack) | IsFix fix -> (FIXP(fix,env,[]), stack) | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack) - | IsMutConstruct ((spi,i),vars) -> - (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack) + | IsMutConstruct c -> (CONSTR(c, []), stack) (* neutral cases *) - | (IsSort _ | IsMeta _) -> (VAL(0, t), stack) - | IsMutInd (sp,vars) -> - (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack) + | (IsSort _ | IsMeta _ | IsMutInd _) -> (VAL(0, t), stack) | IsProd (x,t,c) -> (VAL(0, mkProd (x, cbv_norm_term info env t, cbv_norm_term info (subs_lift env) c)), @@ -317,17 +311,13 @@ and cbv_stack_term info stack env t = (* constructor in a Case -> IOTA (use red_under because we know there is a Case) *) - | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk))) + | (CONSTR((sp,n),_), APP(args,CASE(_,br,(arity,_),env,stk))) when red_under (info_flags info) fIOTA -> -(* - let ncargs = arity.(n-1) in - let real_args = list_lastn ncargs args in -*) let real_args = snd (list_chop arity args) in cbv_stack_term info (stack_app real_args stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA ( " " )*) - | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk)) + | (CONSTR((_,n),_), CASE(_,br,_,env,stk)) when red_under (info_flags info) fIOTA -> cbv_stack_term info stk env br.(n-1) @@ -335,7 +325,7 @@ and cbv_stack_term info stack env t = | (head, TOP) -> head | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) - | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl) + | (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl) (* definitely a value *) | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk) @@ -390,9 +380,9 @@ and cbv_norm_value info = function (* reduction under binders *) Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds))) (List.map (cbv_norm_value info) args) - | CONSTR (n,spi,vars,args) -> + | CONSTR (c,args) -> applistc - (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars)) + (mkMutConstruct c) (List.map (cbv_norm_value info) args) (* with profiling *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 7271a3c0b..d78711137 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -33,7 +33,7 @@ type cbv_value = | LAM of name * constr * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value list | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list + | CONSTR of constructor * cbv_value list val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 556dbd334..5a88e62dc 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -22,24 +22,24 @@ open Rawterm (* usage qque peu general: utilise aussi dans record *) type cte_typ = - | NAM_Section_Variable of variable_path - | NAM_Constant of constant_path - | NAM_Inductive of inductive_path - | NAM_Constructor of constructor_path + | NAM_Section_Variable of variable + | NAM_Constant of constant + | NAM_Inductive of inductive + | NAM_Constructor of constructor let cte_of_constr c = match kind_of_term c with - | IsConst (sp,_) -> ConstRef sp - | IsMutInd (ind_sp,_) -> IndRef ind_sp - | IsMutConstruct (cstr_cp,_) -> ConstructRef cstr_cp + | IsConst sp -> ConstRef sp + | IsMutInd ind_sp -> IndRef ind_sp + | IsMutConstruct cstr_cp -> ConstructRef cstr_cp | IsVar id -> VarRef (Declare.find_section_variable id) | _ -> raise Not_found type cl_typ = | CL_SORT | CL_FUN - | CL_SECVAR of variable_path - | CL_CONST of constant_path - | CL_IND of inductive_path + | CL_SECVAR of variable + | CL_CONST of constant + | CL_IND of inductive type cl_info_typ = { cl_strength : strength; @@ -203,8 +203,8 @@ let _ = let constructor_at_head t = let rec aux t' = match kind_of_term t' with | IsVar id -> CL_SECVAR (find_section_variable id),0 - | IsConst (sp,_) -> CL_CONST sp,0 - | IsMutInd (ind_sp,_) -> CL_IND ind_sp,0 + | IsConst sp -> CL_CONST sp,0 + | IsMutInd ind_sp -> CL_IND ind_sp,0 | IsProd (_,_,c) -> CL_FUN,0 | IsLetIn (_,_,_,c) -> aux c | IsSort _ -> CL_SORT,0 diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 4b5261647..019644e20 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -20,9 +20,9 @@ open Declare type cl_typ = | CL_SORT | CL_FUN - | CL_SECVAR of variable_path - | CL_CONST of constant_path - | CL_IND of inductive_path + | CL_SECVAR of variable + | CL_CONST of constant + | CL_IND of inductive (* This is the type of infos for declared classes *) type cl_info_typ = { diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2aada52ee..b4df53b8a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -46,10 +46,10 @@ let occur_rel p env id = let occur_id env id0 c = let rec occur n c = match kind_of_term c with | IsVar id when id=id0 -> raise Occur - | IsConst (sp, _) when basename sp = id0 -> raise Occur - | IsMutInd (ind_sp, _) + | IsConst sp when basename sp = id0 -> raise Occur + | IsMutInd ind_sp when basename (path_of_inductive_path ind_sp) = id0 -> raise Occur - | IsMutConstruct (cstr_sp, _) + | IsMutConstruct cstr_sp when basename (path_of_constructor_path cstr_sp) = id0 -> raise Occur | IsRel p when p>n & occur_rel (p-n) env id0 -> raise Occur | _ -> iter_constr_with_binders succ occur n c @@ -99,18 +99,18 @@ let used_of = global_vars_and_consts (* Tools for printing of Cases *) let encode_inductive ref = - let (indsp,_ as ind) = + let indsp = match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with - | IsMutInd (indsp,args) -> (indsp,args) + | IsMutInd indsp -> indsp | _ -> errorlabstrm "indsp_of_id" - [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >] - in - let mis = Global.lookup_mind_specif ind in + [< 'sTR ((Global.string_of_global ref)^ + " is not an inductive type") >] in + let mis = Global.lookup_mind_specif indsp in let constr_lengths = Array.map List.length (mis_recarg mis) in (indsp,constr_lengths) let constr_nargs indsp = - let mis = Global.lookup_mind_specif (indsp,[||] (* ?? *)) in + let mis = Global.lookup_mind_specif indsp in let nparams = mis_nparams mis in Array.map (fun t -> List.length (fst (decompose_prod_assum t)) - nparams) (mis_nf_lc mis) @@ -138,7 +138,7 @@ module PrintingCasesMake = val title : string end) -> struct - type t = inductive_path * int array + type t = inductive * int array let encode = encode_inductive let check (_,lc) = if not (Test.test lc) then @@ -292,15 +292,14 @@ let rec detype avoid env t = | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c | IsApp (f,args) -> RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args) - | IsConst (sp,cl) -> - detype_reference avoid env (ConstRef sp) cl + | IsConst sp -> RRef (dummy_loc, ConstRef sp) | IsEvar (ev,cl) -> let f = REvar (dummy_loc, ev) in RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl)) - | IsMutInd (ind_sp,cl) -> - detype_reference avoid env (IndRef ind_sp) cl - | IsMutConstruct (cstr_sp,cl) -> - detype_reference avoid env (ConstructRef cstr_sp) cl + | IsMutInd ind_sp -> + RRef (dummy_loc, IndRef ind_sp) + | IsMutConstruct cstr_sp -> + RRef (dummy_loc, ConstructRef cstr_sp) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in @@ -312,8 +311,7 @@ let rec detype avoid env t = else Some (detype avoid env p) in let constructs = - Array.init (Array.length considl) - (fun i -> ((indsp,i+1),[] (* on triche *))) in + Array.init (Array.length considl) (fun i -> (indsp,i+1)) in let eqnv = array_map3 (detype_eqn avoid env) constructs consnargsl bl in let eqnl = Array.to_list eqnv in @@ -330,20 +328,6 @@ let rec detype avoid env t = | IsFix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef | IsCoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef -and detype_reference avoid env ref args = - let args = - try Array.to_list (extract_instance ref args) - with Not_found -> (* May happen in debugger *) - if Array.length args = 0 then [] - else - let m = "<<Cannot split "^(string_of_int (Array.length args))^ - " arguments>>" in - (mkVar (id_of_string m))::(Array.to_list args) - in - let f = RRef (dummy_loc, ref) in - if args = [] then f - else RApp (dummy_loc, f, List.map (detype avoid env) args) - and detype_fix avoid env fixkind (names,tys,bodies) = let lfi = Array.map (fun id -> next_name_away id avoid) names in let def_avoid = Array.to_list lfi@avoid in @@ -353,7 +337,7 @@ and detype_fix avoid env fixkind (names,tys,bodies) = Array.map (detype def_avoid def_env) bodies) -and detype_eqn avoid env constr_id construct_nargs branch = +and detype_eqn avoid env constr construct_nargs branch = let make_pat x avoid env b ids = if not (force_wildcard ()) or (dependent (mkRel 1) b) then let id = next_name_away_with_default "x" x avoid in @@ -364,7 +348,7 @@ and detype_eqn avoid env constr_id construct_nargs branch = let rec buildrec ids patlist avoid env n b = if n=0 then (dummy_loc, ids, - [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)], + [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], detype avoid env b) else match kind_of_term b with diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f40ad4dc0..e221e4945 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -241,14 +241,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (let c = nf_evar (evars_of isevars) c1 in evar_conv_x (push_rel_assum (n,c) env) isevars pbty c'1 c'2) - | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> + | IsMutInd sp1, IsMutInd sp2 -> sp1=sp2 - & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 - | IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) -> + | IsMutConstruct sp1, IsMutConstruct sp2 -> sp1=sp2 - & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 | IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) -> diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 66125bfeb..54e67e401 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -46,9 +46,9 @@ let rec occur_meta_pattern = function | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false type constr_label = - | ConstNode of section_path - | IndNode of inductive_path - | CstrNode of constructor_path + | ConstNode of constant + | IndNode of inductive + | CstrNode of constructor | VarNode of identifier exception BoundPattern;; @@ -74,9 +74,9 @@ let rec head_pattern_bound t = | PCoFix _ -> anomaly "head_pattern_bound: not a type" let head_of_constr_reference c = match kind_of_term c with - | IsConst (sp,_) -> ConstNode sp - | IsMutConstruct (sp,_) -> CstrNode sp - | IsMutInd (sp,_) -> IndNode sp + | IsConst sp -> ConstNode sp + | IsMutConstruct sp -> CstrNode sp + | IsMutInd sp -> IndNode sp | IsVar id -> VarNode id | _ -> anomaly "Not a rigid reference" @@ -311,9 +311,9 @@ let rec pattern_of_constr t = | IsProd (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) | IsLambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) | IsApp (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a) - | IsConst (sp,ctxt) -> pattern_of_ref (ConstRef sp) ctxt - | IsMutInd (sp,ctxt) -> pattern_of_ref (IndRef sp) ctxt - | IsMutConstruct (sp,ctxt) -> pattern_of_ref (ConstructRef sp) ctxt + | IsConst sp -> PRef (ConstRef sp) + | IsMutInd sp -> PRef (IndRef sp) + | IsMutConstruct sp -> PRef (ConstructRef sp) | IsEvar (n,ctxt) -> if ctxt = [||] then PEvar n else PApp (PEvar n, Array.map pattern_of_constr ctxt) @@ -323,8 +323,3 @@ let rec pattern_of_constr t = | IsFix f -> PFix f | IsCoFix _ -> error "pattern_of_constr: (co)fix currently not supported" - -and pattern_of_ref ref inst = - let args = Declare.extract_instance ref inst in - let f = PRef ref in - if args = [||] then f else PApp (f, Array.map pattern_of_constr args) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 91dd32ba3..42b680820 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -34,9 +34,9 @@ type constr_pattern = val occur_meta_pattern : constr_pattern -> bool type constr_label = - | ConstNode of section_path - | IndNode of inductive_path - | CstrNode of constructor_path + | ConstNode of constant + | IndNode of inductive + | CstrNode of constructor | VarNode of identifier val label_of_ref : global_reference -> constr_label diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cb9e0abd6..2cb322bea 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -221,7 +221,7 @@ let rec pretype tycon env isevars lvar lmeta = function sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in let args = instance_from_named_context hyps in - let c = mkEvar (ev, Array.of_list args) in + let c = mkEvar (ev, args) in let j = (Retyping.get_judgment_of env (evars_of isevars) c) in inh_conv_coerce_to_tycon loc env isevars j tycon diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index a46a3f8b5..c8c91a945 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -23,17 +23,16 @@ type loc = int * int (* the last argument of PatCstr is a possible alias ident for the pattern *) type cases_pattern = | PatVar of loc * name - | PatCstr of - loc * (constructor_path * identifier list) * cases_pattern list * name + | PatCstr of loc * constructor * cases_pattern list * name type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn type 'ctxt reference = - | RConst of section_path * 'ctxt - | RInd of inductive_path * 'ctxt - | RConstruct of constructor_path * 'ctxt + | RConst of constant * 'ctxt + | RInd of inductive * 'ctxt + | RConstruct of constructor * 'ctxt | RVar of identifier | REVar of int * 'ctxt diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 22492a6cc..336b3ffa1 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -22,17 +22,16 @@ type loc = int * int (* the last argument of PatCstr is a possible alias ident for the pattern *) type cases_pattern = | PatVar of loc * name - | PatCstr of - loc * (constructor_path * identifier list) * cases_pattern list * name + | PatCstr of loc * constructor * cases_pattern list * name type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn type 'ctxt reference = - | RConst of section_path * 'ctxt - | RInd of inductive_path * 'ctxt - | RConstruct of constructor_path * 'ctxt + | RConst of constant * 'ctxt + | RInd of inductive * 'ctxt + | RConstruct of constructor * 'ctxt | RVar of identifier | REVar of int * 'ctxt diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cabdaa62c..c3c295428 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -34,7 +34,7 @@ type struc_typ = { s_PARAM : int; s_PROJ : section_path option list } -let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref) +let sTRUCS = (ref [] : (inductive * struc_typ) list ref) let add_new_struc1 x = sTRUCS:=x::(!sTRUCS) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 25e024a6c..3684bb228 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -29,11 +29,11 @@ type struc_typ = { s_PROJ : section_path option list } val add_new_struc : - inductive_path * identifier * int * section_path option list -> unit + inductive * identifier * int * section_path option list -> unit (* [find_structure isp] returns the infos associated to inductive path [isp] if it corresponds to a structure, otherwise fails with [Not_found] *) -val find_structure : inductive_path -> struc_typ +val find_structure : inductive -> struc_typ type obj_typ = { o_DEF : constr; @@ -47,8 +47,8 @@ val add_new_objdef : Term.constr list * Term.constr list -> unit -val inStruc : inductive_path * struc_typ -> obj -val outStruc : obj -> inductive_path * struc_typ +val inStruc : inductive * struc_typ -> obj +val outStruc : obj -> inductive * struc_typ val inObjDef1 : section_path -> obj val outObjDef1 : obj -> section_path diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index cc907ac7a..7d1564a8c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -24,7 +24,7 @@ exception Redelimination let check_transparency env ref = match ref with - EvalConst (sp,_) -> Opaque.is_evaluable env (EvalConstRef sp) + EvalConst sp -> Opaque.is_evaluable env (EvalConstRef sp) | EvalVar id -> Opaque.is_evaluable env (EvalVarRef id) | _ -> false @@ -128,8 +128,8 @@ let invert_name labs l na0 env sigma ref = function let refi = match ref with | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) - | EvalConst (sp,args) -> - Some (EvalConst (make_path (dirpath sp) id CCI, args)) in + | EvalConst sp -> + Some (EvalConst (make_path (dirpath sp) id CCI)) in match refi with | None -> None | Some ref -> @@ -298,9 +298,9 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = let subbodies = list_tabulate make_Fi nbodies in substl subbodies bodies.(bodynum) -let reduce_mind_case_use_function (sp,args) env mia = +let reduce_mind_case_use_function sp env mia = match kind_of_term mia.mconstr with - | IsMutConstruct(ind_sp,i as cstr_sp, args) -> + | IsMutConstruct(ind_sp,i as cstr_sp) -> let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in applist (mia.mlf.(i-1), real_cargs) | IsCoFix (_,(names,_,_) as cofix) -> @@ -308,9 +308,9 @@ let reduce_mind_case_use_function (sp,args) env mia = match names.(i) with | Name id -> let sp = make_path (dirpath sp) id (kind_of_path sp) in - (match constant_opt_value env (sp,args) with + (match constant_opt_value env sp with | None -> None - | Some _ -> Some (mkConst (sp,args))) + | Some _ -> Some (mkConst sp)) | Anonymous -> None in let cofix_def = contract_cofix_use_function build_fix_name cofix in mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) @@ -320,8 +320,8 @@ let special_red_case env whfun (ci, p, c, lf) = let rec redrec s = let (constr, cargs) = whfun s in match kind_of_term constr with - | IsConst (sp,args as cst) -> - (if not (Opaque.is_evaluable env (EvalConstRef sp)) then + | IsConst cst -> + (if not (Opaque.is_evaluable env (EvalConstRef cst)) then raise Redelimination; let gvalue = constant_value env cst in if reducible_mind_case gvalue then @@ -528,14 +528,14 @@ let nf env sigma c = strong whd_nf env sigma c * ol is the occurence list to find. *) let rec substlin env name n ol c = match kind_of_term c with - | IsConst (sp,_ as const) when EvalConstRef sp = name -> + | IsConst const when EvalConstRef const = name -> if List.hd ol = n then try (n+1, List.tl ol, constant_value env const) with NotEvaluableConst _ -> errorlabstrm "substlin" - [< pr_sp sp; 'sTR " is not a defined constant" >] + [< pr_sp const; 'sTR " is not a defined constant" >] else ((n+1), ol, c) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index b519968a3..79c73d2d5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -386,13 +386,17 @@ let mk_clenv_hnf_constr_type_of wc t = mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t)) let mk_clenv_rename_from wc (c,t) = - mk_clenv_from wc (c,rename_bound_var [] t) + mk_clenv_from wc (c,rename_bound_var (w_env wc) [] t) + +let mk_clenv_rename_from_n wc n (c,t) = + mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t) let mk_clenv_rename_type_of wc t = - mk_clenv_from wc (t,rename_bound_var [] (w_type_of wc t)) + mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t)) let mk_clenv_rename_hnf_constr_type_of wc t = - mk_clenv_from wc (t,rename_bound_var [] (w_hnf_constr wc (w_type_of wc t))) + mk_clenv_from wc + (t,rename_bound_var (w_env wc) [] (w_hnf_constr wc (w_type_of wc t))) let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t) @@ -1068,7 +1072,7 @@ let make_clenv_binding_apply wc n (c,t) lbind = let clause = mk_clenv_from_n wc n (c,t) in clenv_constrain_missing_args largs clause else if lcomargs = 0 then - let clause = mk_clenv_rename_from wc (c,t) in + let clause = mk_clenv_rename_from_n wc n (c,t) in clenv_match_args lbind clause else errorlabstrm "make_clenv_bindings" diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 20eae8111..3b3ce56ea 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -62,7 +62,9 @@ val unify_0 : val collect_metas : constr -> int list val mk_clenv : 'a -> constr -> 'a clausenv val mk_clenv_from : 'a -> constr * constr -> 'a clausenv -val mk_clenv_rename_from : 'a -> constr * constr -> 'a clausenv +val mk_clenv_from_n : 'a -> int -> constr * constr -> 'a clausenv +val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv +val mk_clenv_rename_from_n : wc -> int -> constr * constr -> wc clausenv val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv val mk_clenv_printable_type_of : wc -> constr -> wc clausenv val mk_clenv_type_of : wc -> constr -> wc clausenv diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 9e9d6c8fb..0256dd600 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -125,7 +125,7 @@ let w_env wc = get_env (ids_it wc) let w_hyps wc = named_context (get_env (ids_it wc)) let w_ORELSE wt1 wt2 wc = try wt1 wc with e when catchable_exception e -> wt2 wc -let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp +let w_defined_const wc sp = defined_constant (w_env wc) sp let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k let w_const_value wc = constant_value (w_env wc) let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n diff --git a/proofs/logic.ml b/proofs/logic.ml index 22751eaf9..58fb85240 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -202,10 +202,11 @@ let split_sign hfrom hto l = splitrec [] false l let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = + let env = Global.env() in let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = if toleft - then occur_var_in_decl hyp2 d - else occur_var_in_decl hyp d2 + then occur_var_in_decl env hyp2 d + else occur_var_in_decl env hyp d2 in let rec moverec first middle = function | [] -> error ("No such hypothesis : " ^ (string_of_id hto)) @@ -260,9 +261,11 @@ let apply_to_hyp2 env id f = if (not !check) || !found then env' else error "No such assumption" let global_vars_set_of_var = function - | (_,None,t) -> global_vars_set (body_of_type t) + | (_,None,t) -> global_vars_set (Global.env()) (body_of_type t) | (_,Some c,t) -> - Idset.union (global_vars_set (body_of_type t)) (global_vars_set c) + let env =Global.env() in + Idset.union (global_vars_set env (body_of_type t)) + (global_vars_set env c) let check_backward_dependencies sign d = if not (Idset.for_all @@ -272,9 +275,10 @@ let check_backward_dependencies sign d = error "Can't introduce at that location: free variable conflict" let check_forward_dependencies id tail = + let env = Global.env() in List.iter (function (id',_,_ as decl) -> - if occur_var_in_decl id decl then + if occur_var_in_decl env id decl then error ((string_of_id id) ^ " is used in the hypothesis " ^ (string_of_id id'))) tail @@ -529,7 +533,7 @@ let prim_refiner r sigma goal = | { name = Thin; hypspecs = ids } -> let clear_aux sign id = - if !check && occur_var id cl then + if !check && occur_var env id cl then error ((string_of_id id) ^ " is used in the conclusion."); remove_hyp sign id in diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index ca67f7306..a77fb84a0 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -107,7 +107,7 @@ let make_qid = function | VArg (Identifier id) -> VArg (Qualid (make_qualid [] id)) | VArg (Constr c) -> (match (kind_of_term c) with - | IsConst _ -> VArg (Qualid (qualid_of_sp (path_of_const c))) + | IsConst cst -> VArg (Qualid (qualid_of_sp cst)) | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >]) | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >] @@ -1057,7 +1057,7 @@ and cast_opencom_interp ist com = and qid_interp ist = function | Node(loc,"QUALIDARG",p) -> interp_qualid p | Node(loc,"QUALIDMETA",[Num(_,n)]) -> - Nametab.qualid_of_sp (path_of_const (List.assoc n ist.lmatch)) + Nametab.qualid_of_sp (destConst(List.assoc n ist.lmatch)) | ast -> anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR "Unrecognizable qualid ast: "; print_ast ast>]) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5c1a2c876..8a05e0989 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -276,7 +276,7 @@ let mutual_cofix lf lar pf = let rename_bound_var_goal gls = let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in let ids = ids_of_named_context sign in - convert_concl (rename_bound_var ids cl) gls + convert_concl (rename_bound_var (Global.env()) ids cl) gls (***************************************) @@ -481,7 +481,7 @@ open Pp open Printer let pr_com sigma goal com = - prterm (rename_bound_var + prterm (rename_bound_var (Global.env()) (ids_of_named_context goal.evar_hyps) (Astterm.interp_constr sigma (Evarutil.evar_env goal) com)) diff --git a/tactics/auto.ml b/tactics/auto.ml index 742a6ad23..088e7636a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -378,10 +378,9 @@ let _ = begin try let env = Global.env() and sigma = Evd.empty in - let (isp, _ as rectype) = - destMutInd (Declare.global_qualified_reference qid) in + let isp = destMutInd (Declare.global_qualified_reference qid) in let conspaths = - mis_conspaths (Global.lookup_mind_specif rectype) in + mis_conspaths (Global.lookup_mind_specif isp) in let hyps = Declare.implicit_section_args (IndRef isp) in let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in let lcons = diff --git a/tactics/elim.ml b/tactics/elim.ml index ffdc962a1..dc0393b06 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -12,6 +12,7 @@ open Pp open Util open Names open Term +open Environ open Reduction open Inductive open Proof_type @@ -160,7 +161,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHyp (fun id gls -> let idty = pf_type_of gls (mkVar id) in - let fvty = global_vars idty in + let fvty = global_vars (pf_env gls) idty in let possible_bring_ids = (List.tl (nLastHyps (abs_j - abs_i) gls)) @bargs.assums in diff --git a/tactics/equality.ml b/tactics/equality.ml index c2c21d9fd..e497fb114 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -273,7 +273,7 @@ let find_eq_pattern aritysort sort = *) exception DiscrFound of - (constructor_path * int) list * constructor_path * constructor_path + (constructor * int) list * constructor * constructor let find_positions env sigma t1 t2 = let rec findrec posn t1 t2 = @@ -281,7 +281,7 @@ let find_positions env sigma t1 t2 = let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with - | IsMutConstruct (sp1,_), IsMutConstruct (sp2,_) -> + | IsMutConstruct sp1, IsMutConstruct sp2 -> (* both sides are constructors, so either we descend, or we can discriminate here. *) if sp1 = sp2 then @@ -1192,7 +1192,7 @@ let rec eq_mod_rel l_meta t0 t1 = let is_hd_const c = match kind_of_term c with | IsApp (f,args) -> (match kind_of_term f with - | IsConst (c,_) -> Some (c, args) + | IsConst c -> Some (c, args) |_ -> None) | _ -> None @@ -1218,7 +1218,7 @@ let sub_term_with_unif cref ceq = | OpApp, cl -> begin let f, args = destApplication u in match kind_of_term f with - | IsConst (sp,_) when sp = hdsp -> begin + | IsConst sp when sp = hdsp -> begin try (array_fold_left2 eq_mod_rel l_meta args t_args, nb_occ+1) with NotEqModRel -> Array.fold_left diff --git a/tactics/inv.ml b/tactics/inv.ml index 3fbe8e8ee..15e8ee6b3 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -189,7 +189,9 @@ let rec dependent_hyps id idlist sign = | [] -> [] | (id1::l) -> let id1ty = snd (lookup_named id1 sign) in - if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l + if occur_var (Global.env()) id (body_of_type id1ty) + then id1::dep_rec l + else dep_rec l in dep_rec idlist @@ -201,8 +203,9 @@ let generalizeRewriteIntros tac depids id gls = gls let var_occurs_in_pf gl id = - occur_var id (pf_concl gl) or - List.exists (fun (_,t) -> occur_var id t) (pf_hyps_types gl) + let env = pf_env gl in + occur_var env id (pf_concl gl) or + List.exists (fun (_,t) -> occur_var env id t) (pf_hyps_types gl) let split_dep_and_nodep idl gl = (List.filter (var_occurs_in_pf gl) idl, diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 31dddc038..f6b2ba06f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -83,14 +83,15 @@ let no_inductive_inconstr env constr = *) -let thin_ids (hyps,vars) = +let thin_ids env (hyps,vars) = fst (List.fold_left (fun ((ids,globs) as sofar) (id,c,a) -> if List.mem id globs then match c with - | None -> (id::ids,(global_vars a)@globs) - | Some body -> (id::ids,(global_vars body)@(global_vars a)@globs) + | None -> (id::ids,(global_vars env a)@globs) + | Some body -> + (id::ids,(global_vars env body)@(global_vars env a)@globs) else sofar) ([],vars) hyps) @@ -167,7 +168,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = pty,goal else let i = mkAppliedInd ind in - let ivars = global_vars i in + let ivars = global_vars env i in let revargs,ownsign = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> @@ -201,7 +202,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = in assert (list_subset - (global_vars invGoal) + (global_vars env invGoal) (ids_of_named_context (named_context invEnv))); (* errorlabstrm "lemma_inversion" @@ -252,7 +253,7 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op = let gl = nth_goal_of_pftreestate n pts in let t = pf_get_hyp_typ gl id in let env = pf_env gl and sigma = project gl in - let fv = global_vars t in + let fv = global_vars env t in (* Pourquoi ??? let thin_ids = thin_ids (hyps,fv) in if not(list_subset thin_ids fv) then diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 10dcee8d7..d19c67c18 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -292,9 +292,9 @@ let check_is_dependent t n = let gen_lem_name m = match kind_of_term m with | IsVar id -> add_suffix id "_ext" - | IsConst (sp, _) -> add_suffix (basename sp) "_ext" - | IsMutInd ((sp, i), _) -> add_suffix (basename sp) ((string_of_int i)^"_ext") - | IsMutConstruct (((sp,i),j), _) -> add_suffix + | IsConst sp -> add_suffix (basename sp) "_ext" + | IsMutInd (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext") + | IsMutConstruct ((sp,i),j) -> add_suffix (basename sp) ((string_of_int i)^(string_of_int i)^"_ext") | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">] @@ -617,9 +617,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with let al = [|hh; cc|] in let a = [|hhm; ccm|] in let fleche_constr = (Lazy.force coq_fleche) in - let fleche_cp = (match (kind_of_term fleche_constr) with - | (IsConst (cp,_)) -> cp - | _ -> assert false) in + let fleche_cp = destConst fleche_constr in let new_concl = (mkApp (fleche_constr, al)) in if is_r then diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 168cd94e1..d9919b7e0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -298,7 +298,7 @@ let case_sign ity i = analrec [] recarg.(i-1) let elim_sign ity i = - let (_,j),_ = ity in + let (_,j) = ity in let rec analrec acc = function | (Param(_)::rest) -> analrec (false::acc) rest | (Norec::rest) -> analrec (false::acc) rest @@ -346,7 +346,7 @@ let general_elim_then_using | _ -> let name_elim = match kind_of_term elim with - | IsConst (sp,_) -> string_of_path sp + | IsConst sp -> string_of_path sp | IsVar id -> string_of_id id | _ -> "\b" in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 441cb2aad..e7673944e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -58,12 +58,12 @@ let get_pairs_from_bindings = List.map pair_from_binding let rec string_head_bound x = match kind_of_term x with - | IsConst _ -> string_of_id (basename (path_of_const x)) - | IsMutInd (ind_sp,args) -> - let mispec = Global.lookup_mind_specif (ind_sp,args) in + | IsConst cst -> string_of_id (basename cst) + | IsMutInd ind_sp -> + let mispec = Global.lookup_mind_specif ind_sp in string_of_id (mis_typename mispec) - | IsMutConstruct ((ind_sp,i),args) -> - let mispec = Global.lookup_mind_specif (ind_sp,args) in + | IsMutConstruct (ind_sp,i) -> + let mispec = Global.lookup_mind_specif ind_sp in string_of_id (mis_consnames mispec).(i-1) | IsVar id -> string_of_id id | _ -> raise Bound @@ -469,7 +469,7 @@ let move_to_rhyp rhyp gl = | (hyp,c,typ) as ht :: rest -> if Some hyp = rhyp then lastfixed - else if List.exists (occur_var_in_decl hyp) depdecls then + else if List.exists (occur_var_in_decl (pf_env gl) hyp) depdecls then get_lhyp lastfixed (ht::depdecls) rest else get_lhyp (Some hyp) depdecls rest @@ -660,10 +660,11 @@ let generalize_goal gl c cl = prod_name (Global.env()) (Anonymous, t, cl') let generalize_dep c gl = + let env = pf_env gl in let sign = pf_hyps gl in let init_ids = ids_of_named_context (Global.named_context()) in let rec seek toquant d = - if List.exists (fun (id,_,_) -> occur_var_in_decl id d) toquant + if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant or dependent_in_decl c d then d::toquant else @@ -680,7 +681,7 @@ let generalize_dep c gl = in let cl' = List.fold_right mkNamedProd_or_LetIn to_quantify (pf_concl gl) in let cl'' = generalize_goal gl c cl' in - let args = instance_from_named_context to_quantify in + let args = Array.to_list (instance_from_named_context to_quantify) in tclTHEN (apply_type cl'' (c::args)) (thin (List.rev tothin')) @@ -769,7 +770,7 @@ let letin_tac with_eq name c occs gl = let (depdecls,marks,ccl)= letin_abstract id c occs gl in let t = pf_type_of gl c in let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in - let args = instance_from_named_context depdecls in + let args = Array.to_list (instance_from_named_context depdecls) in let newcl = mkNamedLetIn id c t tmpcl in (* if with_eq then @@ -1076,7 +1077,7 @@ let default_elim (c,lbindc) gl = let elimc = try lookup_eliminator env ind s with Not_found -> - let dir, base,k = repr_path (path_of_inductive_path (fst ind)) in + let dir, base,k = repr_path (path_of_inductive_path ind) in let id = make_elimination_ident base s in errorlabstrm "default_elim" [< 'sTR "Cannot find the elimination combinator :"; @@ -1129,7 +1130,7 @@ comes from a canonically generated one *) let rec is_rec_arg env sigma indpath t = try - let ((ind_sp,_),_) = find_mrectype env sigma t in + let (ind_sp,_) = find_mrectype env sigma t in Declare.path_of_inductive_path ind_sp = indpath with Induc -> false @@ -1211,7 +1212,7 @@ let atomize_param_of_ind hyp0 gl = let argl = snd (decomp_app indtyp) in let c = List.nth argl (i-1) in match kind_of_term c with - | IsVar id when not (List.exists (occur_var id) avoid) -> + | IsVar id when not (List.exists (occur_var (pf_env gl) id) avoid) -> atomize_one (i-1) ((mkVar id)::avoid) gl | IsVar id -> let x = fresh_id [] id gl in @@ -1239,7 +1240,8 @@ let find_atomic_param_of_ind mind indtyp = let indvars = ref Idset.empty in for i = nparams to (Array.length argv)-1 do match kind_of_term argv.(i) with - | IsVar id when not (List.exists (occur_var id) params) -> + | IsVar id + when not (List.exists (occur_var (Global.env()) id) params) -> indvars := Idset.add id !indvars | _ -> () done; @@ -1323,8 +1325,9 @@ let cook_sign hyp0 indvars env = indhyps := hyp::!indhyps; rhyp end else - if (List.exists (fun id -> occur_var_in_decl id decl) allindhyps - or List.exists (fun (id,_,_) -> occur_var_in_decl id decl) !decldeps) + if (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps + or List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) + !decldeps) then begin decldeps := decl::!decldeps; if !before then diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 4de0a8e46..6672e56c4 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -51,8 +51,8 @@ let constr_val_discr t = let c, l = decomp t in match kind_of_term c with (* IsConst _,_) -> Some(TERM c,l) *) - | IsMutInd (ind_sp,_) -> Some(IndNode ind_sp,l) - | IsMutConstruct (cstr_sp,_) -> Some(CstrNode cstr_sp,l) + | IsMutInd ind_sp -> Some(IndNode ind_sp,l) + | IsMutConstruct cstr_sp -> Some(CstrNode cstr_sp,l) (* Ici, comment distinguer SectionVarNode de VarNode ?? *) | IsVar id -> Some(VarNode id,l) | _ -> None diff --git a/toplevel/class.ml b/toplevel/class.ml index 9696557c1..50c0f33e0 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -182,31 +182,18 @@ let check_target clt = function (* decomposition de constr vers coe_typ *) -(* t provient de global_reference donc pas de Cast, pas de App *) -let coe_of_reference t = - match kind_of_term t with - | IsConst (sp,l) -> (Array.to_list l), ConstRef sp - | IsMutInd (ind_sp,l) -> (Array.to_list l), IndRef ind_sp - | IsMutConstruct (cstr_sp,l) -> (Array.to_list l), ConstructRef cstr_sp - | IsVar id -> - let sp = - try find_section_variable id - with Not_found -> anomaly "Not a reference" - in [], VarRef sp - | _ -> anomaly "Not a reference" - let constructor_at_head1 t = let rec aux t' = match kind_of_term t' with - | IsConst (sp,l) -> t',[],(Array.to_list l),CL_CONST sp,0 - | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0 - | IsVar id -> t',[],[],CL_SECVAR (find_section_variable id),0 + | IsConst sp -> t',[],CL_CONST sp,0 + | IsMutInd ind_sp -> t',[],CL_IND ind_sp,0 + | IsVar id -> t',[],CL_SECVAR (find_section_variable id),0 | IsCast (c,_) -> aux c | IsApp(f,args) -> - let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args - | IsProd (_,_,_) -> t',[],[],CL_FUN,0 + let t',_,l,_ = aux f in t',Array.to_list args,l,Array.length args + | IsProd (_,_,_) -> t',[],CL_FUN,0 | IsLetIn (_,_,_,c) -> aux c - | IsSort _ -> t',[],[],CL_SORT,0 + | IsSort _ -> t',[],CL_SORT,0 | _ -> raise Not_found in aux (collapse_appl t) @@ -254,21 +241,21 @@ la liste des variables dont depend la classe source let get_source lp source = match source with | None -> - let (v1,lv1,l,cl1,p1) = + let (v1,lv1,cl1,p1) = match lp with | [] -> raise Not_found | t1::_ -> try constructor_at_head1 t1 with _ -> raise Not_found in - (cl1,p1,v1,lv1,1,l) + (cl1,p1,v1,lv1,1) | Some cl -> let rec aux n = function | [] -> raise Not_found | t1::lt -> try - let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in - if cl1 = cl then cl1,p1,v1,lv1,n,l + let v1,lv1,cl1,p1 = constructor_at_head1 t1 in + if cl1 = cl then cl1,p1,v1,lv1,n else aux (n+1) lt with _ -> aux (n + 1) lt in aux 1 lp @@ -277,7 +264,7 @@ let get_target t ind = if (ind > 1) then CL_FUN,0,t else - let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2 + let v2,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2 let prods_of t = let rec aux acc d = match kind_of_term d with @@ -360,19 +347,15 @@ booleen "coercion identite'?" lorque source est None alors target est None aussi. *) -let add_new_coercion_core idf stre source target isid = +let add_new_coercion_core coef stre source target isid = let env = Global.env () in - let v = constr_of_reference Evd.empty env idf in + let v = constr_of_reference Evd.empty env coef in let vj = Retyping.get_judgment_of env Evd.empty v in - (* coef, c'est idf non ? - let f_vardep,coef = coe_of_reference v in - *) - let coef = idf in if coercion_exists coef then raise (CoercionError AlreadyExists); let lp = prods_of (vj.uj_type) in let llp = List.length lp in if llp <= 1 then raise (CoercionError NotACoercion); - let (cls,ps,vs,lvs,ind,s_vardep) = + let (cls,ps,vs,lvs,ind) = try get_source (List.tl lp) source with Not_found -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 5b3e3a59d..b93cc8b6a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -227,13 +227,13 @@ let list_chop_hd i l = match list_chop i l with | (l1,x::l2) -> (l1,x,l2) | _ -> assert false -let collect_non_rec = +let collect_non_rec env = let rec searchrec lnonrec lnamerec ldefrec larrec nrec = try let i = list_try_find_i (fun i f -> - if List.for_all (fun def -> not (occur_var f def)) ldefrec + if List.for_all (fun def -> not (occur_var env f def)) ldefrec then i else failwith "try_find_i") 0 lnamerec in @@ -288,7 +288,7 @@ let build_recursive lnameargsardef = in States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,nvrec)) = - collect_non_rec lrecnames recdef arityl (Array.to_list nv) in + collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in @@ -352,7 +352,7 @@ let build_corecursive lnameardef = in States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,_)) = - collect_non_rec lrecnames recdef arityl [] in + collect_non_rec env0 lrecnames recdef arityl [] in let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in diff --git a/toplevel/command.mli b/toplevel/command.mli index 3c1d52b6a..63456e33b 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -35,7 +35,7 @@ i*) val hypothesis_def_var : bool -> identifier -> strength -> Coqast.t -> global_reference -val parameter_def_var : identifier -> Coqast.t -> constant_path +val parameter_def_var : identifier -> Coqast.t -> constant val build_mutual : (identifier * Coqast.t) list -> diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 61db7f6c6..9b634bf08 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -32,16 +32,15 @@ let recalc_sp dir sp = let (_,spid,k) = repr_path sp in Names.make_path dir spid k let rec find_var id = function - | [] -> raise Not_found + | [] -> false | (sp,b,_)::l -> if basename sp = id then b=None else find_var id l let build_abstract_list hyps ids_to_discard = - map_succeed - (fun id -> - try - if find_var id hyps then ABSTRACT else failwith "caugth" - with Not_found -> failwith "caugth") - ids_to_discard + let l = + List.fold_left + (fun vars id -> if find_var id hyps then mkVar id::vars else vars) + [] ids_to_discard in + Array.of_list l (* Discharge of inductives is done here (while discharge of constants is done by the kernel for efficiency). *) @@ -61,7 +60,7 @@ let abstract_inductive ids_to_abs hyps inds = (np,tname,arity',cnames,lc')) inds in - (inds',ABSTRACT) in + inds' in let abstract_one_def id c inds = List.map (function (np,tname,arity,cnames,lc) -> @@ -69,22 +68,21 @@ let abstract_inductive ids_to_abs hyps inds = let lc' = List.map (replace_vars [id, c]) lc in (np,tname,arity',cnames,lc')) inds in - let abstract_once ((hyps,inds,modl) as sofar) id = + let abstract_once ((hyps,inds,vars) as sofar) id = match hyps with | (hyp,None,t as d)::rest when id = hyp -> - let (inds',modif) = abstract_one_assum hyp t inds in - (rest, inds', modif::modl) + let inds' = abstract_one_assum hyp t inds in + (rest, inds', mkVar id::vars) | (hyp,Some b,t as d)::rest when id = hyp -> let inds' = abstract_one_def hyp b inds in - (rest, inds', modl) - | _ -> sofar - in - let (_,inds',revmodl) = + (rest, inds', vars) + | _ -> sofar in + let (_,inds',vars) = List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in let inds'' = List.map (fun (nparams,a,arity,c,lc) -> - let nparams' = nparams + (List.length revmodl) in + let nparams' = nparams + (List.length vars) in let params, short_arity = decompose_prod_n_assum nparams' arity in let shortlc = List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in @@ -102,7 +100,7 @@ let abstract_inductive ids_to_abs hyps inds = mind_entry_consnames = c; mind_entry_lc = shortlc }) inds' in - (inds'', List.rev revmodl) + (inds'', Array.of_list vars) let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = assert (Array.length mib.mind_packets > 0); @@ -111,8 +109,8 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = array_map_to_list (fun mip -> let nparams = mip.mind_nparams in - let arity = expmod_type oldenv modlist (mind_user_arity mip) in - let lc = Array.map (expmod_type oldenv modlist) (mind_user_lc mip) in + let arity = expmod_type modlist (mind_user_arity mip) in + let lc = Array.map (expmod_type modlist) (mind_user_lc mip) in (nparams, mip.mind_typename, arity, @@ -121,15 +119,15 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = mib.mind_packets in let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) mib.mind_hyps in - let hyps' = map_named_context (expmod_constr oldenv modlist) hyps in - let (inds',modl) = abstract_inductive ids_to_discard hyps' inds in + let hyps' = map_named_context (expmod_constr modlist) hyps in + let (inds',abs_vars) = abstract_inductive ids_to_discard hyps' inds in let lmodif_one_mind i = let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in - (((osecsp,i), DO_ABSTRACT ((nsecsp,i),modl)), + (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)), list_tabulate (function j -> let j' = j + 1 in - (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),modl))) + (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars))) nbc) in let indmodifs,cstrmodifs = @@ -167,8 +165,8 @@ type discharge_operation = | Constant of section_path * recipe * strength * bool | Inductive of mutual_inductive_entry * bool | Class of cl_typ * cl_info_typ - | Struc of inductive_path * (unit -> struc_typ) - | Objdef of constant_path + | Struc of inductive * (unit -> struc_typ) + | Objdef of constant | Coercion of coercion_entry | Require of module_reference | Constraints of Univ.constraints @@ -204,7 +202,7 @@ let process_object oldenv dir sec_sp ids_to_discard,work_alist) *) - | "CONSTANT" | "PARAMETER" -> + | ("CONSTANT" | "PARAMETER") -> (* CONSTANT/PARAMETER means never discharge (though visibility *) (* may vary) *) let stre = constant_or_parameter_strength sp in @@ -215,20 +213,20 @@ let process_object oldenv dir sec_sp (ops, ids_to_discard, (constl,indl,cstrl)) else *) - let cb = Environ.lookup_constant sp oldenv in - let imp = is_implicit_constant sp in - let newsp = match stre with - | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp - | _ -> recalc_sp dir sp in - let mods = - let modl = build_abstract_list cb.const_hyps ids_to_discard in - [ (sp, DO_ABSTRACT(newsp,modl)) ] - in - let r = { d_from = cb; - d_modlist = work_alist; - d_abstract = ids_to_discard } in - let op = Constant (newsp,r,stre,imp) in - (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) + let cb = Environ.lookup_constant sp oldenv in + let imp = is_implicit_constant sp in + let newsp = match stre with + | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp + | _ -> recalc_sp dir sp in + let mods = + let abs_vars = build_abstract_list cb.const_hyps ids_to_discard in + [ (sp, DO_ABSTRACT(newsp,abs_vars)) ] + in + let r = { d_from = cb; + d_modlist = work_alist; + d_abstract = ids_to_discard } in + let op = Constant (newsp,r,stre,imp) in + (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) | "INDUCTIVE" -> let mib = Environ.lookup_mind sp oldenv in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index d044232b6..69eb5f2a6 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -477,7 +477,7 @@ let explain_bad_constructor ctx cstr ind = 'sTR "is expected" >] let explain_wrong_numarg_of_constructor ctx cstr n = - let pc = pr_constructor ctx (cstr,[||]) in + let pc = pr_constructor ctx cstr in [<'sTR "The constructor "; pc; 'sTR " expects " ; if n = 0 then [< 'sTR "no argument.">] else [< 'iNT n ; 'sTR " arguments.">] diff --git a/toplevel/record.ml b/toplevel/record.ml index a146264ed..87cb11b61 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -82,7 +82,7 @@ let warning_or_error coe err = (* We build projections *) let declare_projections indsp coers fields = - let mispec = Global.lookup_mind_specif (indsp,[||]) in + let mispec = Global.lookup_mind_specif indsp in let paramdecls = Inductive.mis_params_ctxt mispec in let paramdecls = List.map (fun (na,b,t) -> match na with Name id -> (id,b,t) | _ -> assert false) @@ -96,8 +96,9 @@ let declare_projections indsp coers fields = List.fold_left2 (fun (sp_projs,ids_not_ok,subst) coe (fi,optci,ti) -> let fv_ti = match optci with - | Some ci -> global_vars ci (* Type is then meaningless *) - | None -> global_vars ti in + | Some ci -> + global_vars (Global.env()) ci (* Type is then meaningless *) + | None -> global_vars (Global.env()) ti in let bad_projs = (list_intersect ids_not_ok fv_ti) in if bad_projs <> [] then begin warning_or_error coe (MissingProj (fi,bad_projs)); diff --git a/toplevel/record.mli b/toplevel/record.mli index 9039dfc7d..0791c1a87 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -19,7 +19,7 @@ open Sign [coers]; it returns the absolute names of projections *) val declare_projections : - inductive_path -> bool list -> named_context -> constant_path option list + inductive -> bool list -> named_context -> constant option list val definition_structure : bool * identifier * (identifier * Coqast.t) list * diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 2c158ba31..ac4642722 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -48,7 +48,7 @@ let objdef_declare ref = let v = constr_of_reference Evd.empty env ref in let vc = match kind_of_term v with - | IsConst (sp,l as cst) -> + | IsConst cst -> (match constant_opt_value env cst with | Some vc -> vc | None -> objdef_err ref) @@ -60,7 +60,7 @@ let objdef_declare ref = let { s_PARAM = p; s_PROJ = lpj } = (try (find_structure (match kind_of_term f with - | IsMutConstruct ((indsp,1),_) -> indsp + | IsMutConstruct (indsp,1) -> indsp | _ -> objdef_err ref)) with _ -> objdef_err ref) in let params, projs = |