diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 18:10:57 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 18:10:57 +0000 |
| commit | 1f96d480842a1206a9334d0c8b1b6cc4647066ef (patch) | |
| tree | 9fc22a20d49bcefca1d863aee9d36c5fab03334f | |
| parent | 6c7f6fa6c215e5e28fcf23bf28ccb9db543709ba (diff) | |
Transparent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
52 files changed, 922 insertions, 655 deletions
@@ -15,7 +15,7 @@ kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/univ.cmi kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ kernel/sign.cmi kernel/term.cmi -kernel/names.cmi: lib/pp.cmi +kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/safe_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \ @@ -47,15 +47,17 @@ library/libobject.cmi: kernel/names.cmi library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi lib/system.cmi library/nametab.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi +library/opaque.cmi: kernel/closure.cmi kernel/environ.cmi kernel/names.cmi \ + kernel/safe_typing.cmi library/summary.cmi: kernel/names.cmi lib/system.cmi: lib/pp.cmi lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi -parsing/astterm.cmi: parsing/coqast.cmi kernel/declarations.cmi \ - kernel/environ.cmi kernel/evd.cmi library/impargs.cmi kernel/names.cmi \ - library/nametab.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \ - kernel/sign.cmi kernel/term.cmi +parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ + library/impargs.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \ + kernel/term.cmi parsing/coqast.cmi: lib/dyn.cmi kernel/names.cmi parsing/coqlib.cmi: kernel/names.cmi pretyping/pattern.cmi kernel/term.cmi parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ @@ -170,10 +172,9 @@ tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \ kernel/term.cmi tactics/setoid_replace.cmi: proofs/proof_type.cmi kernel/term.cmi tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi -tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi \ - kernel/declarations.cmi kernel/names.cmi pretyping/pattern.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi +tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \ + pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \ @@ -349,8 +350,10 @@ kernel/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/instantiate.cmi -kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi -kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi +kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ + kernel/names.cmi +kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ + kernel/names.cmi kernel/reduction.cmo: kernel/closure.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ @@ -421,6 +424,8 @@ lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/predicate.cmo: lib/predicate.cmi +lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \ @@ -480,17 +485,25 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \ library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \ library/libobject.cmi library/library.cmo: kernel/environ.cmi library/global.cmi library/lib.cmi \ - library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - library/summary.cmi lib/system.cmi lib/util.cmi library/library.cmi + library/libobject.cmi kernel/names.cmi library/nametab.cmi \ + lib/options.cmi lib/pp.cmi library/summary.cmi lib/system.cmi \ + lib/util.cmi library/library.cmi library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \ - library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - library/summary.cmx lib/system.cmx lib/util.cmx library/library.cmi + library/libobject.cmx kernel/names.cmx library/nametab.cmx \ + lib/options.cmx lib/pp.cmx library/summary.cmx lib/system.cmx \ + lib/util.cmx library/library.cmi library/nametab.cmo: kernel/declarations.cmi library/libobject.cmi \ kernel/names.cmi lib/pp.cmi library/summary.cmi kernel/term.cmi \ lib/util.cmi library/nametab.cmi library/nametab.cmx: kernel/declarations.cmx library/libobject.cmx \ kernel/names.cmx lib/pp.cmx library/summary.cmx kernel/term.cmx \ lib/util.cmx library/nametab.cmi +library/opaque.cmo: kernel/closure.cmi kernel/declarations.cmi \ + kernel/environ.cmi library/global.cmi kernel/names.cmi \ + library/summary.cmi kernel/term.cmi lib/util.cmi library/opaque.cmi +library/opaque.cmx: kernel/closure.cmx kernel/declarations.cmx \ + kernel/environ.cmx library/global.cmx kernel/names.cmx \ + library/summary.cmx kernel/term.cmx lib/util.cmx library/opaque.cmi library/states.cmo: library/lib.cmi library/library.cmi library/summary.cmi \ lib/system.cmi library/states.cmi library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ @@ -511,24 +524,22 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi -parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \ - library/impargs.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ - pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - pretyping/retyping.cmi kernel/sign.cmi pretyping/syntax_def.cmi \ - kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ - parsing/astterm.cmi -parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx \ - kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \ - library/impargs.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ - pretyping/pretyping.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - pretyping/retyping.cmx kernel/sign.cmx pretyping/syntax_def.cmx \ - kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ - parsing/astterm.cmi +parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ + kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ + library/global.cmi library/impargs.cmi kernel/names.cmi \ + library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ + pretyping/pretype_errors.cmi pretyping/pretyping.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \ + parsing/termast.cmi pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi +parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ + kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ + library/global.cmx library/impargs.cmx kernel/names.cmx \ + library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ + pretyping/pretype_errors.cmx pretyping/pretyping.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \ + kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \ + parsing/termast.cmx pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi kernel/names.cmi \ parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx kernel/names.cmx \ @@ -793,12 +804,12 @@ pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \ library/summary.cmx lib/util.cmx pretyping/syntax_def.cmi pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/inductive.cmi kernel/instantiate.cmi \ - kernel/names.cmi lib/pp.cmi kernel/reduction.cmi library/summary.cmi \ - kernel/term.cmi lib/util.cmi pretyping/tacred.cmi + kernel/names.cmi library/opaque.cmi lib/pp.cmi kernel/reduction.cmi \ + library/summary.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/inductive.cmx kernel/instantiate.cmx \ - kernel/names.cmx lib/pp.cmx kernel/reduction.cmx library/summary.cmx \ - kernel/term.cmx lib/util.cmx pretyping/tacred.cmi + kernel/names.cmx library/opaque.cmx lib/pp.cmx kernel/reduction.cmx \ + library/summary.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi @@ -889,20 +900,20 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ lib/dyn.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \ lib/gmap.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \ - proofs/pfedit.cmi lib/pp.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi + library/nametab.cmi library/opaque.cmi lib/options.cmi \ + pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi library/summary.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \ parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ lib/dyn.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \ lib/gmap.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \ - proofs/pfedit.cmx lib/pp.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx proofs/tactic_debug.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi + library/nametab.cmx library/opaque.cmx lib/options.cmx \ + pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/sign.cmx library/summary.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \ kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \ kernel/evd.cmi library/global.cmi kernel/instantiate.cmi proofs/logic.cmi \ @@ -1356,8 +1367,8 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \ library/impargs.cmi library/lib.cmi library/library.cmi \ toplevel/metasyntax.cmi toplevel/mltop.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ - lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \ + library/nametab.cmi library/opaque.cmi lib/options.cmi proofs/pfedit.cmi \ + lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ parsing/search.cmi library/states.cmi pretyping/syntax_def.cmi \ @@ -1372,8 +1383,8 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \ library/impargs.cmx library/lib.cmx library/library.cmx \ toplevel/metasyntax.cmx toplevel/mltop.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ - lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \ + library/nametab.cmx library/opaque.cmx lib/options.cmx proofs/pfedit.cmx \ + lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ parsing/search.cmx library/states.cmx pretyping/syntax_def.cmx \ @@ -1649,14 +1660,14 @@ contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/evd.cmi library/global.cmi lib/gmap.cmi \ kernel/inductive.cmi kernel/instantiate.cmi contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi \ - kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi contrib/extraction/extraction.cmi + kernel/reduction.cmi pretyping/retyping.cmi library/summary.cmi \ + kernel/term.cmi lib/util.cmi contrib/extraction/extraction.cmi contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \ kernel/environ.cmx kernel/evd.cmx library/global.cmx lib/gmap.cmx \ kernel/inductive.cmx kernel/instantiate.cmx contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \ - kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi + kernel/reduction.cmx pretyping/retyping.cmx library/summary.cmx \ + kernel/term.cmx lib/util.cmx contrib/extraction/extraction.cmi contrib/extraction/haskell.cmo: kernel/environ.cmi library/global.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ kernel/names.cmi contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi \ @@ -71,7 +71,8 @@ CONFIG=config/coq_config.cmo LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \ - lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo + lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ + lib/predicate.cmo KERNEL=kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \ @@ -82,7 +83,8 @@ KERNEL=kernel/names.cmo kernel/univ.cmo \ LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \ library/lib.cmo library/goptions.cmo \ - library/global.cmo library/library.cmo library/states.cmo \ + library/global.cmo library/opaque.cmo \ + library/library.cmo library/states.cmo \ library/impargs.cmo library/indrec.cmo library/declare.cmo PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \ @@ -147,8 +149,8 @@ INTERFACE=contrib/interface/vtp.cmo \ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \ lib/util.cmo lib/dyn.cmo lib/gmap.cmo lib/gmapl.cmo \ - lib/hashcons.cmo lib/profile.cmo library/libobject.cmo \ - library/summary.cmo kernel/names.cmo \ + lib/predicate.cmo lib/hashcons.cmo lib/profile.cmo \ + library/libobject.cmo library/summary.cmo kernel/names.cmo \ parsing/lexer.cmo parsing/coqast.cmo \ parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo \ @@ -162,7 +164,7 @@ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \ kernel/instantiate.cmo kernel/closure.cmo kernel/reduction.cmo \ kernel/inductive.cmo kernel/type_errors.cmo kernel/typeops.cmo \ kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo \ - library/global.cmo \ + library/global.cmo library/opaque.cmo \ library/library.cmo lib/options.cmo library/indrec.cmo \ library/impargs.cmo pretyping/retyping.cmo library/declare.cmo \ pretyping/cbv.cmo pretyping/tacred.cmo pretyping/classops.cmo \ @@ -702,7 +704,7 @@ ML4FILES += parsing/lexer.ml4 parsing/q_coqast.ml4 \ parsing/g_prim.ml4 parsing/pcoq.ml4 GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \ - lib/hashcons.cmo kernel/names.cmo \ + lib/hashcons.cmo lib/predicate.cmo kernel/names.cmo \ parsing/coqast.cmo parsing/lexer.cmo \ parsing/pcoq.cmo parsing/q_coqast.cmo parsing/g_prim.cmo diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v index 5cdd5eacd..9e5f95439 100644 --- a/contrib/field/Field_Theory.v +++ b/contrib/field/Field_Theory.v @@ -58,10 +58,7 @@ Proof. Elim (eq_nat_dec n n0);Intro y. Left; Rewrite y; Auto. Right;Red;Intro;Inversion H;Auto. -Save. - -Transparent Peano_dec.eq_nat_dec. -Transparent eqExprA_O. +Defined. Definition eq_nat_dec := Eval Compute in Peano_dec.eq_nat_dec. Definition eqExprA := Eval Compute in eqExprA_O. diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 926ca7951..61bd3353f 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -109,8 +109,10 @@ let _ = let field g = let evc = project g and env = pf_env g in - let typ = constr_of_Constr (interp_tacarg (evc,env,[],[],Some g,get_debug ()) - <:tactic< + let ist = { evc=evc; env=env; lfun=[]; lmatch=[]; + goalopt=Some g; debug=get_debug () } in + let typ = constr_of_Constr (interp_tacarg ist + <:tactic< Match Context With | [|-(eq ?1 ? ?)] -> ?1 | [|-(eqT ?1 ? ?)] -> ?1>>) in diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index e4c852f7f..4e069c11c 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -389,7 +389,7 @@ let inspect n = sp, Lib.Leaf lobj -> (match sp, object_tag lobj with _, "VARIABLE" -> - let ((_, _, v), _, _) = get_variable sp in + let ((_, _, v), _) = get_variable sp in add_search2 (Nametab.locate (qualid_of_sp sp)) v | sp, ("CONSTANT"|"PARAMETER") -> let {const_type=typ} = Global.lookup_constant sp in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 6f1be02fb..00259ef99 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -170,7 +170,7 @@ let constant_to_ast_list sp = errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];; let variable_to_ast_list sp = - let ((id, c, v), _, _) = get_variable sp in + let ((id, c, v), _) = get_variable sp in let l = implicits_of_var sp in (match c with None -> diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index 3d29e0503..45ad93aba 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -75,9 +75,8 @@ Definition log_inf_correct1 := Definition log_inf_correct2 := [p:positive](proj2 ? ? (log_inf_correct p)). -(***TODO: retablir les commandes Opaque / Transparent Opaque log_inf_correct1 log_inf_correct2. -***) + Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3116bd49b..f4b75583c 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -847,7 +847,7 @@ let print_object lobj id sp dn fv env = let hyps = string_list_of_named_context_list hyps in print_mutual_inductive packs fv hyps env inner_types | "VARIABLE" -> - let (_,(varentry,_,_)) = Declare.out_variable lobj in + let (_,(varentry,_)) = Declare.out_variable lobj in begin match varentry with Declare.SectionLocalDef body -> diff --git a/kernel/closure.ml b/kernel/closure.ml index f41993673..82847ae15 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -58,6 +58,11 @@ type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of section_path +type transparent_state = Idpred.t * Sppred.t + +let all_opaque = (Idpred.empty, Sppred.empty) +let all_transparent = (Idpred.full, Sppred.full) + module type RedFlagsSig = sig type reds type red_kind @@ -66,12 +71,12 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant_path -> red_kind - val fCONSTBUT : constant_path -> red_kind + val fCONST : section_path -> red_kind val fVAR : identifier -> red_kind - val fVARBUT : identifier -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds + val red_sub : reds -> red_kind -> reds + val red_add_transparent : reds -> transparent_state -> reds val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_get_const : reds -> bool * evaluable_global_reference list @@ -86,84 +91,84 @@ module RedFlags = (struct type reds = { r_beta : bool; r_delta : bool; - r_const : bool * constant_path list * identifier list; + r_const : transparent_state; r_zeta : bool; r_evar : bool; r_iota : bool } type red_kind = BETA | DELTA | EVAR | IOTA | ZETA - | CONST of constant_path | CONSTBUT of constant_path - | VAR of identifier | VARBUT of identifier + | CONST of constant_path | VAR of identifier let fBETA = BETA let fDELTA = DELTA let fEVAR = EVAR let fIOTA = IOTA let fZETA = ZETA let fCONST sp = CONST sp - let fCONSTBUT sp = CONSTBUT sp - let fVAR id = VAR id - let fVARBUT id = VARBUT id + let fVAR id = VAR id let no_red = { r_beta = false; r_delta = false; - r_const = false,[],[]; + r_const = all_opaque; r_zeta = false; r_evar = false; r_iota = false } let red_add red = function | BETA -> { red with r_beta = true } - | DELTA -> - (match red.r_const with - | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags" - | _ -> { red with r_const = true,[],[]; r_delta = true }) + | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST sp -> - let (oldallbut,l1,l2) = red.r_const in - if oldallbut then error "Conflict in the reduction flags" - else { red with r_const = false, list_union [sp] l1, l2 } - | CONSTBUT sp -> - (match red.r_const with - | (false,_::_,_ | false,_,_::_ | true,[],[]) -> - error "Conflict in the reduction flags" - | (_,l1,l2) -> { red with r_const = true, list_union [sp] l1, l2 }) + let (l1,l2) = red.r_const in + { red with r_const = l1, Sppred.add sp l2 } | IOTA -> { red with r_iota = true } | EVAR -> { red with r_evar = true } | ZETA -> { red with r_zeta = true } | VAR id -> - let (oldallbut,l1,l2) = red.r_const in - if oldallbut then error "Conflict in the reduction flags" - else { red with r_const = false, l1, list_union [id] l2 } - | VARBUT id -> - (match red.r_const with - | (false,_::_,_ | false,_,_::_ | true,[],[]) -> - error "Conflict in the reduction flags" - | (_,l1,l2) -> { red with r_const = true, l1, list_union [id] l2 }) + let (l1,l2) = red.r_const in + { red with r_const = Idpred.add id l1, l2 } + + let red_sub red = function + | BETA -> { red with r_beta = false } + | DELTA -> { red with r_delta = false } + | CONST sp -> + let (l1,l2) = red.r_const in + { red with r_const = l1, Sppred.remove sp l2 } + | IOTA -> { red with r_iota = false } + | EVAR -> { red with r_evar = false } + | ZETA -> { red with r_zeta = false } + | VAR id -> + let (l1,l2) = red.r_const in + { red with r_const = Idpred.remove id l1, l2 } + + let red_add_transparent red tr = + { red with r_const = tr } let mkflags = List.fold_left red_add no_red let red_set red = function | BETA -> incr_cnt red.r_beta beta | CONST sp -> - let (b,l,_) = red.r_const in - let c = List.mem sp l in - incr_cnt ((b & not c) or (c & not b)) delta + let (_,l) = red.r_const in + let c = Sppred.mem sp l in + incr_cnt c delta | VAR id -> (* En attendant d'avoir des sp pour les Var *) - let (b,_,l) = red.r_const in - let c = List.mem id l in - incr_cnt ((b & not c) or (c & not b)) delta + let (l,_) = red.r_const in + let c = Idpred.mem id l in + incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | EVAR -> incr_cnt red.r_zeta evar | IOTA -> incr_cnt red.r_iota iota | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta - | (CONSTBUT _ | VARBUT _) -> (* Not for internal use *) - failwith "not implemented" let red_get_const red = - let b,l1,l2 = red.r_const in - let l1' = List.map (fun x -> EvalConstRef x) l1 in - let l2' = List.map (fun x -> EvalVarRef x) l2 in - b, l1' @ l2' + let p1,p2 = red.r_const in + let (b1,l1) = Idpred.elements p1 in + let (b2,l2) = Sppred.elements p2 in + if b1=b2 then + let l1' = List.map (fun x -> EvalVarRef x) l1 in + let l2' = List.map (fun x -> EvalConstRef x) l2 in + (b1, l1' @ l2') + else error "unrepresentable pair of predicate" end : RedFlagsSig) @@ -376,13 +381,13 @@ let red_under (md,r) rk = type 'a table_key = | ConstBinding of constant - | EvarBinding of (existential * 'a subs) + | EvarBinding of existential | VarBinding of identifier | FarRelBinding of int type ('a, 'b) infos = { i_flags : flags; - i_repr : ('a, 'b) infos -> 'a subs -> constr -> 'a; + i_repr : ('a, 'b) infos -> constr -> 'a; i_env : env; i_evc : 'b evar_map; i_rels : int * (int * constr) list; @@ -396,15 +401,15 @@ let ref_value_cache info ref = Some (Hashtbl.find info.i_tab ref) with Not_found -> try - let body,subs = + let body = match ref with | FarRelBinding n -> - let (s,l) = info.i_rels in lift n (List.assoc (s-n) l), ESID 0 - | VarBinding id -> List.assoc id info.i_vars, ESID 0 - | EvarBinding (evc,subs) -> existential_value info.i_evc evc, subs - | ConstBinding cst -> constant_value info.i_env cst, ESID 0 + let (s,l) = info.i_rels in lift n (List.assoc (s-n) l) + | VarBinding id -> List.assoc id info.i_vars + | EvarBinding evc -> existential_value info.i_evc evc + | ConstBinding cst -> constant_value info.i_env cst in - let v = info.i_repr info subs body in + let v = info.i_repr info body in Hashtbl.add info.i_tab ref v; Some v with @@ -579,7 +584,7 @@ and fterm = and freference = (* only vars as args of FConst ... exploited for caching *) | FConst of section_path * fconstr array - | FEvar of (existential * fconstr subs) + | FEvar of existential_key * fconstr array | FVar of identifier | FFarRel of int (* index in the rel_context part of _initial_ environment *) @@ -679,9 +684,9 @@ let mk_clos_deep clos_fun env t = | IsConst (sp,v) -> { norm = Red; term = FFlex (FConst (sp,Array.map (clos_fun env) v)) } - | IsEvar (_,v as ev) -> + | IsEvar (n,v) -> { norm = Red; - term = FFlex (FEvar (ev, env)) } + term = FFlex (FEvar (n, Array.map (clos_fun env) v)) } | IsMutCase (ci,p,c,v) -> { norm = Red; @@ -733,9 +738,8 @@ let rec to_constr constr_fun lfts v = mkCast (constr_fun lfts a, constr_fun lfts b) | FFlex (FConst (op,ve)) -> mkConst (op, Array.map (constr_fun lfts) ve) - | FFlex (FEvar ((n,args),env)) -> - let f a = constr_fun lfts (mk_clos env a) in - mkEvar (n, Array.map f args) + | 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) -> @@ -985,10 +989,11 @@ let rec knr info m stk = (match ref_value_cache info (ConstBinding cst) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FFlex(FEvar ev) when can_red info stk fEVAR -> + | FFlex(FEvar (n,args)) when can_red info stk fEVAR -> (* In the case of evars, if it is not defined, then we do not set the flag to Norm, because it may be instantiated later on *) - (match ref_value_cache info (EvarBinding ev) with + let evar = (n, Array.map term_of_fconstr args) in + (match ref_value_cache info (EvarBinding evar) with Some v -> kni info v stk | None -> (m,stk)) | FFlex(FVar id) when can_red info stk (fVAR id) -> @@ -1065,8 +1070,8 @@ and down_then_up info m stk = Array.map (kl info) fbds),bds,e) | FFlex(FConst(sp,args)) -> FFlex(FConst(sp, Array.map (kl info) args)) - | FFlex(FEvar((i,args),e)) -> - FFlex(FEvar((i,args),e)) + | FFlex(FEvar(i,args)) -> + FFlex(FEvar(i, Array.map (kl info) args)) | t -> t in {norm=Norm;term=nt} in (* Precondition: m.norm = Norm *) @@ -1089,13 +1094,15 @@ let inject = mk_clos (ESID 0) type 'a clos_infos = (fconstr, 'a) infos let create_clos_infos flgs env sigma = - create (fun _ -> mk_clos) 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) - | FEvar ev -> ref_value_cache info (EvarBinding ev) + | FEvar (n,v) -> + let evar = (n, Array.map (norm_val info) v) in + ref_value_cache info (EvarBinding evar) | FVar id -> ref_value_cache info (VarBinding id) | FFarRel p -> ref_value_cache info (FarRelBinding p) diff --git a/kernel/closure.mli b/kernel/closure.mli index b7ded4a9f..5c8662420 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -32,6 +32,11 @@ type evaluable_global_reference = Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) +type transparent_state = Idpred.t * Sppred.t + +val all_opaque : transparent_state +val all_transparent : transparent_state + (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -47,10 +52,8 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant_path -> red_kind - val fCONSTBUT : constant_path -> red_kind + val fCONST : section_path -> red_kind val fVAR : identifier -> red_kind - val fVARBUT : identifier -> red_kind (* No reduction at all *) val no_red : reds @@ -58,6 +61,12 @@ module type RedFlagsSig = sig (* Adds a reduction kind to a set *) val red_add : reds -> red_kind -> reds + (* Removes a reduction kind to a set *) + val red_sub : reds -> red_kind -> reds + + (* Adds a reduction kind to a set *) + val red_add_transparent : reds -> transparent_state -> reds + (* Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds @@ -104,7 +113,7 @@ val unfold_flags : evaluable_global_reference -> flags type 'a table_key = | ConstBinding of constant - | EvarBinding of (existential * 'a subs) + | EvarBinding of existential | VarBinding of identifier | FarRelBinding of int @@ -113,7 +122,7 @@ val ref_value_cache: ('a,'b) infos -> 'a table_key -> 'a option val info_flags: ('a,'b) infos -> flags val infos_under: ('a,'b) infos -> ('a,'b) infos val create: - (('a,'b) infos -> 'a subs -> constr -> 'a) -> + (('a,'b) infos -> constr -> 'a) -> flags -> env -> 'b evar_map -> ('a,'b) infos (***********************************************************************) @@ -174,7 +183,7 @@ type fterm = and freference = | FConst of section_path * fconstr array - | FEvar of (existential * fconstr subs) + | FEvar of existential_key * fconstr array | FVar of identifier | FFarRel of int diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 28f26a3af..f75128148 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -21,7 +21,7 @@ type constant_body = { const_type : types; const_hyps : section_context; const_constraints : constraints; - mutable const_opaque : bool } + const_opaque : bool } let is_defined cb = match cb.const_body with Some _ -> true | _ -> false @@ -31,8 +31,9 @@ let is_opaque cb = cb.const_opaque (*s Global and local constant declaration. *) type constant_entry = { - const_entry_body : constr; - const_entry_type : constr option } + const_entry_body : constr; + const_entry_type : constr option; + const_entry_opaque : bool } type local_entry = | LocalDef of constr diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ff002230f..e7c88f6f4 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -26,17 +26,16 @@ type constant_body = { const_type : types; const_hyps : section_context; (* New: younger hyp at top *) const_constraints : constraints; - mutable const_opaque : bool } + const_opaque : bool } val is_defined : constant_body -> bool -val is_opaque : constant_body -> bool - (*s Global and local constant declaration. *) type constant_entry = { - const_entry_body : constr; - const_entry_type : constr option } + const_entry_body : constr; + const_entry_type : constr option; + const_entry_opaque : bool } type local_entry = | LocalDef of constr diff --git a/kernel/environ.ml b/kernel/environ.ml index 77b96d30c..a34191a3e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -331,7 +331,7 @@ let make_all_name_different env = (* Constants *) let defined_constant env sp = is_defined (lookup_constant sp env) -let opaque_constant env sp = is_opaque (lookup_constant sp env) +let opaque_constant env sp = (lookup_constant sp env).const_opaque (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant env sp = @@ -353,16 +353,6 @@ let evaluable_rel_decl env n = with Not_found -> false -(*s Opaque / Transparent switching *) - -let set_opaque env sp = - let cb = lookup_constant sp env in - cb.const_opaque <- true - -let set_transparent env sp = - let cb = lookup_constant sp env in - cb.const_opaque <- false - (*s Modules (i.e. compiled environments). *) type compiled_env = { diff --git a/kernel/environ.mli b/kernel/environ.mli index 45c2d1130..2a778b76e 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -164,11 +164,6 @@ val evaluable_constant : env -> constant_path -> bool val evaluable_named_decl : env -> identifier -> bool val evaluable_rel_decl : env -> int -> bool -(*s Opaque / Transparent switching *) - -val set_opaque : env -> constant_path -> unit -val set_transparent : env -> constant_path -> unit - (*s Modules. *) type compiled_env diff --git a/kernel/names.ml b/kernel/names.ml index b3a4ccba5..3d72326ed 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -145,6 +145,7 @@ module IdOrdered = module Idset = Set.Make(IdOrdered) module Idmap = Map.Make(IdOrdered) +module Idpred = Predicate.Make(IdOrdered) let atompart_of_id id = fst (repr_ident id) let index_of_id id = snd (repr_ident id) @@ -310,7 +311,7 @@ module SpOrdered = end module Spset = Set.Make(SpOrdered) - +module Sppred = Predicate.Make(SpOrdered) module Spmap = Map.Make(SpOrdered) (* Special references for inductive objects *) diff --git a/kernel/names.mli b/kernel/names.mli index 6e2739590..5af331075 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -40,8 +40,9 @@ val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier (* Identifiers sets and maps *) -module Idset : Set.S with type elt = identifier -module Idmap : Map.S with type key = identifier +module Idset : Set.S with type elt = identifier +module Idpred : Predicate.S with type elt = identifier +module Idmap : Map.S with type key = identifier val lift_ident : identifier -> identifier val next_ident_away_from : identifier -> identifier list -> identifier @@ -106,7 +107,9 @@ val sp_ord : section_path -> section_path -> int (* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *) val is_dirpath_prefix_of : dir_path -> dir_path -> bool -module Spmap : Map.S with type key = section_path +module Spset : Set.S with type elt = section_path +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 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index dd76eee74..d7a57e2d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -266,7 +266,7 @@ let safe_infer_declaration env = function type local_names = (identifier * variable_path) list -let add_global_declaration sp env locals (body,typ,cst) = +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 @@ -285,22 +285,24 @@ let add_global_declaration sp env locals (body,typ,cst) = const_type = typ; const_hyps = sp_hyps; const_constraints = cst; - const_opaque = false } + const_opaque = op } in Environ.add_constant sp cb env' let add_parameter sp t locals env = - add_global_declaration sp env locals (safe_infer_declaration env (Assum t)) + add_global_declaration + sp env locals (safe_infer_declaration env (Assum t)) false -let add_constant_with_value sp body typ locals env = +let add_constant sp ce locals env = + let { const_entry_body = body; + const_entry_type = typ; + const_entry_opaque = op } = ce in let body' = match typ with | None -> body | Some ty -> mkCast (body, ty) in - add_global_declaration sp env locals (safe_infer_declaration env (Def body')) - -let add_constant sp ce locals env = - add_constant_with_value sp ce.const_entry_body ce.const_entry_type locals env + add_global_declaration + sp env locals (safe_infer_declaration env (Def body')) op let add_discharged_constant sp r locals env = let (body,typ,cst) = Cooking.cook_constant env r in @@ -464,9 +466,6 @@ let rec pop_named_decls idl env = | [] -> env | id::l -> pop_named_decls l (Environ.pop_named_decl id env) -let set_opaque = Environ.set_opaque -let set_transparent = Environ.set_transparent - let export = export let import = import diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ff1a8131d..90c6e2466 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -67,9 +67,6 @@ val lookup_constant : section_path -> safe_environment -> constant_body val lookup_mind : section_path -> safe_environment -> mutual_inductive_body val lookup_mind_specif : inductive -> safe_environment -> inductive_instance -val set_opaque : safe_environment -> section_path -> unit -val set_transparent : safe_environment -> section_path -> unit - val export : safe_environment -> dir_path -> compiled_env val import : compiled_env -> safe_environment -> safe_environment diff --git a/lib/predicate.ml b/lib/predicate.ml new file mode 100644 index 000000000..1b2ef443b --- /dev/null +++ b/lib/predicate.ml @@ -0,0 +1,99 @@ +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Library General Public License. *) +(* *) +(***********************************************************************) + +(* $Id$ *) + +(* Sets over ordered types *) + +module type OrderedType = + sig + type t + val compare: t -> t -> int + end + +module type S = + sig + type elt + type t + val empty: t + val full: t + val is_empty: t -> bool + val is_full: t -> bool + val mem: elt -> t -> bool + val singleton: elt -> t + val add: elt -> t -> t + val remove: elt -> t -> t + val union: t -> t -> t + val inter: t -> t -> t + val diff: t -> t -> t + val complement: t -> t + val equal: t -> t -> bool + val subset: t -> t -> bool + val elements: t -> bool * elt list + end + +module Make(Ord: OrderedType) = + struct + module EltSet = Set.Make(Ord) + + (* when bool is false, the denoted set is the complement of + the given set *) + type elt = Ord.t + type t = bool * EltSet.t + + let elements (b,s) = (b, EltSet.elements s) + + let empty = (false,EltSet.empty) + let full = (true,EltSet.empty) + + (* assumes the set is infinite *) + let is_empty (b,s) = not b & EltSet.is_empty s + let is_full (b,s) = b & EltSet.is_empty s + + let mem x (b,s) = + if b then not (EltSet.mem x s) else EltSet.mem x s + + let singleton x = (false,EltSet.singleton x) + + let add x (b,s) = + if b then (b,EltSet.remove x s) + else (b,EltSet.add x s) + + let remove x (b,s) = + if b then (b,EltSet.add x s) + else (b,EltSet.remove x s) + + let complement (b,s) = (not b, s) + + let union s1 s2 = + match (s1,s2) with + ((false,p1),(false,p2)) -> (false,EltSet.union p1 p2) + | ((true,n1),(true,n2)) -> (true,EltSet.inter n1 n2) + | ((false,p1),(true,n2)) -> (true,EltSet.diff n2 p1) + | ((true,n1),(false,p2)) -> (true,EltSet.diff n1 p2) + + let inter s1 s2 = + complement (union (complement s1) (complement s2)) + + let diff s1 s2 = inter s1 (complement s2) + + let subset s1 s2 = + match (s1,s2) with + ((false,p1),(false,p2)) -> EltSet.subset p1 p2 + | ((true,n1),(true,n2)) -> EltSet.subset n2 n1 + | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2) + | ((true,_),(false,_)) -> false + + let equal (b1,s1) (b2,s2) = + b1=b2 & EltSet.equal s1 s2 + + end diff --git a/lib/predicate.mli b/lib/predicate.mli new file mode 100644 index 000000000..73e4ecce9 --- /dev/null +++ b/lib/predicate.mli @@ -0,0 +1,69 @@ + +(* $Id$ *) + +(* Module [Pred]: sets over infinite ordered types with complement. *) + +(* This module implements the set data structure, given a total ordering + function over the set elements. All operations over sets + are purely applicative (no side-effects). + The implementation uses the Set library. *) + +module type OrderedType = + sig + type t + val compare: t -> t -> int + end + (* The input signature of the functor [Pred.Make]. + [t] is the type of the set elements. + [compare] is a total ordering function over the set elements. + This is a two-argument function [f] such that + [f e1 e2] is zero if the elements [e1] and [e2] are equal, + [f e1 e2] is strictly negative if [e1] is smaller than [e2], + and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + Example: a suitable ordering function is + the generic structural comparison function [compare]. *) + +module type S = + sig + type elt + (* The type of the set elements. *) + type t + (* The type of sets. *) + val empty: t + (* The empty set. *) + val full: t + (* The whole type. *) + val is_empty: t -> bool + (* Test whether a set is empty or not. *) + val is_full: t -> bool + (* Test whether a set contains the whole type or not. *) + val mem: elt -> t -> bool + (* [mem x s] tests whether [x] belongs to the set [s]. *) + val singleton: elt -> t + (* [singleton x] returns the one-element set containing only [x]. *) + val add: elt -> t -> t + (* [add x s] returns a set containing all elements of [s], + plus [x]. If [x] was already in [s], [s] is returned unchanged. *) + val remove: elt -> t -> t + (* [remove x s] returns a set containing all elements of [s], + except [x]. If [x] was not in [s], [s] is returned unchanged. *) + val union: t -> t -> t + val inter: t -> t -> t + val diff: t -> t -> t + val complement: t -> t + (* Union, intersection, difference and set complement. *) + val equal: t -> t -> bool + (* [equal s1 s2] tests whether the sets [s1] and [s2] are + equal, that is, contain equal elements. *) + val subset: t -> t -> bool + (* [subset s1 s2] tests whether the set [s1] is a subset of + the set [s2]. *) + val elements: t -> bool * elt list + (* Gives a finite representation of the predicate: if the + boolean is false, then the predicate is given in extension. + if it is true, then the complement is given *) + end + +module Make(Ord: OrderedType): (S with type elt = Ord.t) + (* Functor building an implementation of the set structure + given a totally ordered type. *) diff --git a/library/declare.ml b/library/declare.ml index d2e451dd9..b10658466 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -63,20 +63,19 @@ let make_strength_2 () = if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2) else NeverDischarge + (* Section variables. *) type section_variable_entry = | SectionLocalDef of constr | SectionLocalAssum of constr -type sticky = bool - -type variable_declaration = section_variable_entry * strength * sticky +type variable_declaration = section_variable_entry * strength type checked_section_variable = constr option * types * Univ.constraints type checked_variable_declaration = - checked_section_variable * strength * sticky + checked_section_variable * strength let vartab = ref ((Spmap.empty, []) : @@ -91,7 +90,7 @@ let _ = Summary.declare_summary "VARIABLE" Summary.init_function = (fun () -> vartab := (Spmap.empty, [])); Summary.survive_section = false } -let cache_variable (sp,(id,(d,str,sticky))) = +let cache_variable (sp,(id,(d,str))) = (* Constr raisonne sur les noms courts *) if List.mem_assoc id (current_section_context ()) then errorlabstrm "cache_variable" @@ -101,7 +100,7 @@ let cache_variable (sp,(id,(d,str,sticky))) = | SectionLocalDef c -> Global.push_named_def (id,c) in Nametab.push 0 (restrict_path 0 sp) (VarRef sp); - vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str,sticky)) m, sp::l) + vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str)) m, sp::l) let (in_variable, out_variable) = let od = { @@ -160,9 +159,7 @@ type constant_declaration_type = | ConstantEntry of constant_entry | ConstantRecipe of Cooking.recipe -type opacity = bool - -type constant_declaration = constant_declaration_type * strength * opacity +type constant_declaration = constant_declaration_type * strength let csttab = ref (Spmap.empty : strength Spmap.t) @@ -172,7 +169,7 @@ let _ = Summary.declare_summary "CONSTANT" Summary.init_function = (fun () -> csttab := Spmap.empty); Summary.survive_section = false } -let cache_constant (sp,(cdt,stre,op)) = +let cache_constant (sp,(cdt,stre)) = if Nametab.exists_cci sp then errorlabstrm "cache_constant" [< pr_id (basename sp); 'sTR " already exists" >] ; @@ -190,12 +187,11 @@ let cache_constant (sp,(cdt,stre,op)) = (* All qualifications of Theorem, Lemma & Definition are visible *) Nametab.push 0 sp (ConstRef sp) | NotDeclare -> assert false); - if op then Global.set_opaque sp; csttab := Spmap.add sp stre !csttab (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant (sp,(ce,stre,op)) = +let load_constant (sp,(ce,stre)) = if Nametab.exists_cci sp then errorlabstrm "cache_constant" [< pr_id (basename sp); 'sTR " already exists" >] ; @@ -203,16 +199,17 @@ let load_constant (sp,(ce,stre,op)) = Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp) (* Opening means making the name without its module qualification available *) -let open_constant (sp,(_,stre,_)) = +let open_constant (sp,(_,stre)) = let n = depth_of_strength stre in Nametab.push n (restrict_path n sp) (ConstRef sp) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry { const_entry_body = mkProp; - const_entry_type = None } + const_entry_type = None; + const_entry_opaque = false } -let export_constant (ce,stre,op) = Some (dummy_constant_entry,stre,op) +let export_constant (ce,stre) = Some (dummy_constant_entry,stre) let (in_constant, out_constant) = let od = { @@ -227,7 +224,8 @@ let hcons_constant_declaration = function | (ConstantEntry ce, stre) -> (ConstantEntry { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = option_app hcons1_constr ce.const_entry_type }, + const_entry_type = option_app hcons1_constr ce.const_entry_type; + const_entry_opaque = ce.const_entry_opaque }, stre) | cd -> cd @@ -328,17 +326,17 @@ let constant_or_parameter_strength sp = try constant_strength sp with Not_found -> NeverDischarge let get_variable sp = - let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in + let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in (* let (c,ty) = Global.lookup_named id in*) - ((id,c,ty),str,sticky) + ((id,c,ty),str) let get_variable_with_constraints sp = - let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in + let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in (* let (c,ty) = Global.lookup_named id in*) - ((id,c,ty),cst,str,sticky) + ((id,c,ty),cst,str) let variable_strength sp = - let _,(_,str,_) = Spmap.find sp (fst !vartab) in str + let _,(_,str) = Spmap.find sp (fst !vartab) in str (* Global references. *) @@ -570,8 +568,11 @@ let declare_one_elimination mispec = let c = instantiate_inductive_section_params c (fst (mis_inductive mispec)) in let _ = declare_constant (id_of_string na) - (ConstantEntry { const_entry_body = c; const_entry_type = None }, - NeverDischarge,false) in + (ConstantEntry + { const_entry_body = c; + const_entry_type = None; + const_entry_opaque = false }, + NeverDischarge) in Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >] in let env = Global.env () in diff --git a/library/declare.mli b/library/declare.mli index 8d5744ad2..5563ebe9e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -33,9 +33,7 @@ type section_variable_entry = | SectionLocalDef of constr | SectionLocalAssum of constr -type sticky = bool - -type variable_declaration = section_variable_entry * strength * sticky +type variable_declaration = section_variable_entry * strength val declare_variable : identifier -> variable_declaration -> variable_path @@ -43,9 +41,7 @@ type constant_declaration_type = | ConstantEntry of constant_entry | ConstantRecipe of Cooking.recipe -type opacity = bool - -type constant_declaration = constant_declaration_type * strength * opacity +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 @@ -78,9 +74,9 @@ val constant_strength : constant_path -> strength val constant_or_parameter_strength : constant_path -> strength val out_variable : Libobject.obj -> identifier * variable_declaration -val get_variable : variable_path -> named_declaration * strength * sticky +val get_variable : variable_path -> named_declaration * strength val get_variable_with_constraints : - variable_path -> named_declaration * Univ.constraints * strength * sticky + variable_path -> named_declaration * Univ.constraints * strength val variable_strength : variable_path -> strength val find_section_variable : identifier -> variable_path val last_section_hyps : dir_path -> identifier list diff --git a/library/global.ml b/library/global.ml index 9dc5cdcd7..1f509bcde 100644 --- a/library/global.ml +++ b/library/global.ml @@ -61,9 +61,6 @@ let lookup_constant sp = lookup_constant sp !global_env let lookup_mind sp = lookup_mind sp !global_env let lookup_mind_specif c = lookup_mind_specif c !global_env -let set_opaque sp = set_opaque !global_env sp -let set_transparent sp = set_transparent !global_env sp - let export s = export !global_env s let import cenv = global_env := import cenv !global_env diff --git a/library/global.mli b/library/global.mli index 0d0db36ce..a9cda1289 100644 --- a/library/global.mli +++ b/library/global.mli @@ -48,9 +48,6 @@ val lookup_constant : section_path -> constant_body val lookup_mind : section_path -> mutual_inductive_body val lookup_mind_specif : inductive -> inductive_instance -val set_opaque : section_path -> unit -val set_transparent : section_path -> unit - val export : dir_path -> compiled_env val import : compiled_env -> unit diff --git a/library/opaque.ml b/library/opaque.ml new file mode 100644 index 000000000..26d2798b1 --- /dev/null +++ b/library/opaque.ml @@ -0,0 +1,60 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Util +open Names +open Closure +open Summary +open Term +open Declarations +(*i*) + +let tr_state = ref all_transparent + +let state () = !tr_state + +let _ = + declare_summary "Transparent constants and variables" + { freeze_function = state; + unfreeze_function = (fun ts -> tr_state := ts); + init_function = (fun () -> tr_state := all_transparent); + survive_section = false } + +let is_evaluable env ref = + match ref with + EvalConstRef sp -> + let (ids,sps) = !tr_state in + Sppred.mem sp sps & + let cb = Environ.lookup_constant sp env in + cb.const_body <> None & not cb.const_opaque + | EvalVarRef id -> + let (ids,sps) = !tr_state in + Idpred.mem id ids & + Environ.lookup_named_value id env <> None + +(* Modifying this state *) +let set_opaque_const sp = + let (ids,sps) = !tr_state in + tr_state := (ids, Sppred.remove sp sps) +let set_transparent_const sp = + let (ids,sps) = !tr_state in + let cb = Global.lookup_constant sp in + if cb.const_body <> None & cb.const_opaque then + error ("Cannot make "^Global.string_of_global (ConstRef sp)^ + " transparent because it was declared opaque."); + tr_state := (ids, Sppred.add sp sps) + +let set_opaque_var id = + let (ids,sps) = !tr_state in + tr_state := (Idpred.remove id ids, sps) +let set_transparent_var id = + let (ids,sps) = !tr_state in + tr_state := (Idpred.add id ids, sps) diff --git a/library/opaque.mli b/library/opaque.mli new file mode 100644 index 000000000..47427a67b --- /dev/null +++ b/library/opaque.mli @@ -0,0 +1,30 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Names +open Closure +open Safe_typing +open Environ +(*i*) + +(* The current set of transparent constants and variables *) +val state : unit -> transparent_state + +(* returns true if the global reference has a definition and that is + has not been set opaque *) +val is_evaluable : env -> evaluable_global_reference -> bool + +(* Modifying this state *) +val set_opaque_const : section_path -> unit +val set_transparent_const : section_path -> unit + +val set_opaque_var : identifier -> unit +val set_transparent_var : identifier -> unit diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 7e48d545a..0d527647b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -18,7 +18,7 @@ open Vernac_ GEXTEND Gram GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list stringarg ne_stringarg_list constrarg sortarg tacarg - ne_qualidarg_list qualidarg qualidconstarg commentarg + ne_qualidarg_list qualidarg commentarg commentarg_list; identarg: @@ -34,9 +34,6 @@ GEXTEND Gram [ [ q = qualidarg; l = ne_qualidarg_list -> q::l | q = qualidarg -> [q] ] ] ; - qualidconstarg: - [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST $l)) >> ] ] - ; numarg: [ [ n = Prim.number -> n | "-"; n = Prim.number -> Num (loc, ( - Ast.num_of_ast n)) ] ] diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4132727e2..ea227c112 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -61,9 +61,6 @@ GEXTEND Gram [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST $l)) >> | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ] ; - qualidconstarg: - [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST $l)) >> ] ] - ; pure_numarg: [ [ n = Prim.number -> n | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n)) @@ -107,9 +104,6 @@ GEXTEND Gram ne_qualidarg_list: [ [ l = LIST1 qualidarg -> l ] ] ; - ne_qualidconstarg_list: - [ [ l = LIST1 qualidconstarg -> l ] ] - ; pattern_occ: [ [ nl = LIST1 pure_numarg; c = constrarg -> <:ast< (PATTERN $c ($LIST $nl)) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b325dbba9..3bec62837 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -339,9 +339,9 @@ GEXTEND Gram | IDENT "End"; id = identarg -> <:ast< (EndSection $id) >> (* Transparent and Opaque *) - | IDENT "Transparent"; l = ne_qualidconstarg_list -> + | IDENT "Transparent"; l = ne_qualidarg_list -> <:ast< (TRANSPARENT ($LIST $l)) >> - | IDENT "Opaque"; l = ne_qualidconstarg_list -> + | IDENT "Opaque"; l = ne_qualidarg_list -> <:ast< (OPAQUE ($LIST $l)) >> (* Coercions *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 05bf62b99..540e1fab0 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -300,7 +300,6 @@ module Tactic = let idmeta_arg = gec "idmeta_arg" let idmetahyp = gec "idmetahyp" let qualidarg = gec "qualidarg" - let qualidconstarg = gec "qualidconstarg" let input_fun = gec "input_fun" let lconstrarg = gec "lconstrarg" let let_clause = gec "let_clause" @@ -316,7 +315,6 @@ module Tactic = let ne_hyp_list = gec_list "ne_hyp_list" let ne_idmetahyp_list = gec_list "ne_idmetahyp_list" let ne_qualidarg_list = gec_list "ne_qualidarg_list" - let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list" let ne_pattern_list = gec_list "ne_pattern_list" let clause_pattern = gec "clause_pattern" let one_intropattern = gec "one_intropattern" @@ -363,7 +361,6 @@ module Vernac_ = let identarg = gec "identarg" let ne_identarg_list = gec_list "ne_identarg_list" let qualidarg = gec "qualidarg" - let qualidconstarg = gec "qualidconstarg" let commentarg = gec "commentarg" let commentarg_list = gec_list "commentarg_list" let ne_qualidarg_list = gec_list "ne_qualidarg_list" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2f9c69b2e..3b55171b7 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -121,7 +121,6 @@ module Tactic : val idmeta_arg : Coqast.t Gram.Entry.e val idmetahyp : Coqast.t Gram.Entry.e val qualidarg : Coqast.t Gram.Entry.e - val qualidconstarg : Coqast.t Gram.Entry.e val input_fun : Coqast.t Gram.Entry.e val intropattern : Coqast.t Gram.Entry.e val lconstrarg : Coqast.t Gram.Entry.e @@ -138,7 +137,6 @@ module Tactic : val ne_hyp_list : Coqast.t list Gram.Entry.e val ne_idmetahyp_list : Coqast.t list Gram.Entry.e val ne_qualidarg_list : Coqast.t list Gram.Entry.e - val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e val ne_intropattern : Coqast.t Gram.Entry.e val ne_pattern_list : Coqast.t list Gram.Entry.e val clause_pattern : Coqast.t Gram.Entry.e @@ -172,7 +170,6 @@ module Vernac_ : val identarg : Coqast.t Gram.Entry.e val ne_identarg_list : Coqast.t list Gram.Entry.e val qualidarg : Coqast.t Gram.Entry.e - val qualidconstarg : Coqast.t Gram.Entry.e val commentarg : Coqast.t Gram.Entry.e val commentarg_list : Coqast.t list Gram.Entry.e val ne_qualidarg_list : Coqast.t list Gram.Entry.e diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 322a61af7..109172af4 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -259,7 +259,7 @@ let print_mutual sp = implicit_args_msg sp mipv >]) *) let print_section_variable sp = - let (d,_,_) = get_variable sp in + let (d,_) = get_variable sp in let l = implicits_of_var sp in [< print_named_decl d; print_impl_args l; 'fNL >] @@ -473,7 +473,7 @@ let print_local_context () = | [] -> [< >] | (sp,Lib.Leaf lobj)::rest -> if "VARIABLE" = object_tag lobj then - let (d,_,_) = get_variable sp in + let (d,_) = get_variable sp in [< print_var_rec rest; print_named_decl d >] else diff --git a/parsing/search.ml b/parsing/search.ml index 530dd48f0..f9ad43abe 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -53,7 +53,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = match object_tag lobj with | "VARIABLE" -> (try - let ((idc,_,typ),_,_) = get_variable sp in + let ((idc,_,typ),_) = get_variable sp in if (head_const typ) = const then fn (VarRef sp) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 6f91ac5b8..77370dedc 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -236,7 +236,9 @@ let rec norm_head info env t stack = let normt = (sp,Array.map (cbv_norm_term info env) vars) in norm_head_ref 0 info env stack (ConstBinding normt) - | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env)) + | IsEvar (ev,args) -> + let evar = (ev, Array.map (cbv_norm_term info env) args) in + norm_head_ref 0 info env stack (EvarBinding evar) | IsLetIn (x, b, t, c) -> (* zeta means letin are contracted; delta without zeta means we *) @@ -283,8 +285,8 @@ and norm_head_ref k info env stack normt = and make_constr_ref n info = function | FarRelBinding p -> mkRel (n+p) | VarBinding id -> mkVar id - | EvarBinding ((ev,args),env) -> - mkEvar (ev,Array.map (cbv_norm_term info env) args) + | EvarBinding (ev,args) -> + mkEvar (ev,Array.map (cbv_norm_term info (ESID 0)) args) | ConstBinding cst -> mkConst cst (* cbv_stack_term performs weak reduction on constr t under the subs @@ -403,7 +405,7 @@ type 'a cbv_infos = (cbv_value, 'a) infos (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = create - (fun old_info s c -> cbv_stack_term old_info TOP s c) + (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c) flgs env sigma diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ab0938985..cc907ac7a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -19,13 +19,24 @@ open Closure open Instantiate open Cbv +exception Elimconst +exception Redelimination + +let check_transparency env ref = + match ref with + EvalConst (sp,_) -> Opaque.is_evaluable env (EvalConstRef sp) + | EvalVar id -> Opaque.is_evaluable env (EvalVarRef id) + | _ -> false + +let isEvalRef env x = + Instantiate.isEvalRef x & + let ref = Instantiate.destEvalRef x in + check_transparency env ref + (************************************************************************) (* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick *) (* is to reuse the name of the function after reduction of the fixpoint *) -exception Elimconst -exception Redelimination - type constant_evaluation = | EliminationFix of int * (int * (int * constr) list * int) | EliminationMutualFix of @@ -171,7 +182,7 @@ let compute_consteval_mutual_fix sigma env ref = let new_minarg = max (minarg'+minarg-nargs) minarg' in EliminationMutualFix (new_minarg,ref,(refs,infos)) | _ -> assert false) - | _ when isEvalRef c' -> + | _ when isEvalRef env c' -> (* Forget all \'s and args and do as if we had started with c' *) let ref = destEvalRef c' in (match reference_opt_value sigma env ref with @@ -310,15 +321,15 @@ let special_red_case env whfun (ci, p, c, lf) = let (constr, cargs) = whfun s in match kind_of_term constr with | IsConst (sp,args as cst) -> - (match constant_opt_value env cst with - | Some gvalue -> - if reducible_mind_case gvalue then - reduce_mind_case_use_function cst env - {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs; - mci=ci; mlf=lf} - else - redrec (gvalue, cargs) - | None -> raise Redelimination) + (if not (Opaque.is_evaluable env (EvalConstRef sp)) then + raise Redelimination; + let gvalue = constant_value env cst in + if reducible_mind_case gvalue then + reduce_mind_case_use_function cst env + {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs; + mci=ci; mlf=lf} + else + redrec (gvalue, cargs)) | _ -> if reducible_mind_case constr then reduce_mind_case @@ -329,8 +340,8 @@ let special_red_case env whfun (ci, p, c, lf) = in redrec (c, empty_stack) + let rec red_elim_const env sigma ref largs = - if not (evaluable_reference sigma env ref) then raise Redelimination; match reference_eval sigma env ref with | EliminationCases n when stack_args_size largs >= n -> let c = reference_value sigma env ref in @@ -376,17 +387,18 @@ and construct_const env sigma = | IsLetIn (n,b,t,c) -> stacklam hnfstack [b] c stack | IsMutCase (ci,p,c,lf) -> hnfstack - (special_red_case env (construct_const env sigma) (ci,p,c,lf), stack) + (special_red_case env + (construct_const env sigma) (ci,p,c,lf), stack) | IsMutConstruct _ -> s | IsCoFix _ -> s | IsFix fix -> (match reduce_fix hnfstack fix stack with | Reduced s' -> hnfstack s' | NotReducible -> raise Redelimination) - | _ when isEvalRef x -> + | _ when isEvalRef env x -> let ref = destEvalRef x in (try - hnfstack (red_elim_const env sigma ref stack) + hnfstack (red_elim_const env sigma ref stack) with Redelimination -> (match reference_opt_value sigma env ref with | Some cval -> @@ -423,10 +435,11 @@ let internal_red_product env sigma c = | IsProd (x,a,b) -> mkProd (x, a, redrec (push_rel_assum (x,a) env) b) | IsLetIn (x,a,b,t) -> redrec env (subst1 a t) | IsMutCase (ci,p,d,lf) -> simpfun (mkMutCase (ci,p,redrec env d,lf)) - | _ when isEvalRef x -> + | _ when isEvalRef env x -> (* TO DO: re-fold fixpoints after expansion *) (* to get true one-step reductions *) - (match reference_opt_value sigma env (destEvalRef x) with + let ref = destEvalRef x in + (match reference_opt_value sigma env ref with | None -> raise Redelimination | Some c -> c) | _ -> raise Redelimination @@ -460,11 +473,11 @@ let hnf_constr env sigma c = (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with | Reduced s' -> redrec s' | NotReducible -> app_stack s) - | _ when isEvalRef x -> + | _ when isEvalRef env x -> let ref = destEvalRef x in (try - let (c',lrest) = red_elim_const env sigma ref largs in - redrec (c', lrest) + let (c',lrest) = red_elim_const env sigma ref largs in + redrec (c', lrest) with Redelimination -> match reference_opt_value sigma env ref with | Some c -> @@ -499,7 +512,7 @@ let whd_nf env sigma c = (match reduce_fix nf_app fix stack with | Reduced s' -> nf_app s' | NotReducible -> s) - | _ when isEvalRef c -> + | _ when isEvalRef env c -> (try nf_app (red_elim_const env sigma (destEvalRef c) stack) with Redelimination -> @@ -609,14 +622,17 @@ let rec substlin env name n ol c = | (IsRel _|IsMeta _|IsVar _|IsSort _ |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c) - -let unfold env sigma name = - clos_norm_flags (unfold_flags name) env sigma let string_of_evaluable_ref = function | EvalVarRef id -> string_of_id id | EvalConstRef sp -> string_of_path sp +let unfold env sigma name = + if Opaque.is_evaluable env name then + clos_norm_flags (unfold_flags name) env sigma + else + error (string_of_evaluable_ref name^" is opaque") + (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. @@ -719,10 +735,12 @@ let one_step_reduce env sigma c = | Reduced s' -> s' | NotReducible -> raise NotStepReducible) | IsCast (c,_) -> redrec (c,largs) - | _ when isEvalRef x -> - let ref = destEvalRef x in + | _ when isEvalRef env x -> + let ref = + try destEvalRef x + with Redelimination -> raise NotStepReducible in (try - red_elim_const env sigma ref largs + red_elim_const env sigma ref largs with Redelimination -> match reference_opt_value sigma env ref with | Some d -> d, largs diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b1cf3764e..1dfc55973 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -177,7 +177,9 @@ let cook_proof () = and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in (ident, - ({ const_entry_body = pfterm; const_entry_type = Some concl }, + ({ const_entry_body = pfterm; + const_entry_type = Some concl; + const_entry_opaque = true }, strength)) (*********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 3ca4ea654..0ea59eea2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -89,7 +89,7 @@ val resume_proof : identifier -> unit val suspend_proof : unit -> unit -(*s [cook_proof ()] turns the current proof (assumed completed) +(*s [cook_proof opacity] turns the current proof (assumed completed) into a constant with its name and strength; it fails if there is no current proof of if it is not completed *) diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 846344210..098c2568e 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -48,9 +48,14 @@ type value = | VRec of value ref (* Signature for interpretation: val_interp and interpretation functions *) + and interp_sign = - enamed_declarations * Environ.env * (identifier * value) list * - (int * constr) list * goal sigma option * debug_info + { evc : enamed_declarations; + env : Environ.env; + lfun : (identifier * value) list; + lmatch : (int * constr) list; + goalopt : goal sigma option; + debug : debug_info } (* For tactic_of_value *) exception NotTactic @@ -132,6 +137,14 @@ let rec constr_list goalopt = function | _::tl -> constr_list goalopt tl | [] -> [] +let interp_constr ist c ocl = + interp_constr_gen ist.evc ist.env + (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl + +let interp_openconstr ist c ocl = + interp_openconstr_gen ist.evc ist.env + (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl + (* For user tactics *) let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t), (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml" @@ -150,13 +163,13 @@ let r_goalopt = ref None let r_debug = ref DebugOn (* Updates the references with the current environment *) -let env_update (evc,env,lfun,lmatch,goalopt,debug) = - r_evc := evc; - r_env := env; - r_lfun := lfun; - r_lmatch := lmatch; - r_goalopt := goalopt; - r_debug := debug +let env_update ist = + r_evc := ist.evc; + r_env := ist.env; + r_lfun := ist.lfun; + r_lmatch := ist.lmatch; + r_goalopt := ist.goalopt; + r_debug := ist.debug (* Table of interpretation functions *) let interp_tab = @@ -192,19 +205,22 @@ let glob_const_nvar loc env qid = | [],id -> (* lookup_value may raise Not_found *) (match Environ.lookup_named_value id env with - | Some _ -> EvalVarRef id + | Some _ -> + let v = EvalVarRef id in + if Opaque.is_evaluable env v then v + else error ("variable "^(string_of_id id)^" is opaque") | None -> error ((string_of_id id)^ " does not denote an evaluable constant")) | _ -> raise Not_found with Not_found -> try - match Nametab.locate qid with - | ConstRef sp when Environ.evaluable_constant (Global.env ()) sp -> - EvalConstRef sp - | VarRef sp when - Environ.evaluable_named_decl (Global.env ()) (basename sp) -> - EvalVarRef (basename sp) + let ev = (match Nametab.locate qid with + | ConstRef sp -> EvalConstRef sp + | VarRef sp -> EvalVarRef (basename sp) | _ -> error ((Nametab.string_of_qualid qid) ^ + " does not denote an evaluable constant")) in + if Opaque.is_evaluable env ev then ev + else error ((Nametab.string_of_qualid qid) ^ " does not denote an evaluable constant") with Not_found -> Nametab.error_global_not_found_loc loc qid @@ -447,8 +463,9 @@ let set_debug pos = debug := pos (* Gives the state of debug *) let get_debug () = !debug + (* Interprets any expression *) -let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = +let rec val_interp ist ast = (* mSGNL [<print_ast ast>]; *) (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *) @@ -456,137 +473,119 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = let value_interp debug = match ast with | Node(_,"APP",l) -> - let fv = val_interp (evc,env,lfun,lmatch,goalopt,debug) (List.hd l) - and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt,debug)) - (List.tl l) in - app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast - | Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) - | Node(_,"REC",l) -> - rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast l + let fv = val_interp ist (List.hd l) + and largs = List.map (val_interp ist) (List.tl l) in + app_interp ist fv largs ast + | Node(_,"FUN",l) -> VFun (ist.lfun,read_fun (List.hd l),List.nth l 1) + | Node(_,"REC",l) -> rec_interp ist ast l | Node(_,"LET",[Node(_,"LETDECL",l);u]) -> - let addlfun=letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in - val_interp (evc,env,addlfun@lfun,lmatch,goalopt,debug) u + let addlfun=letin_interp ist ast l in + val_interp { ist with lfun=addlfun@ist.lfun } u | Node(_,"LETCUT",[Node(_,"LETDECL",l)]) -> - VTactic (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast l) - | Node(_,"MATCHCONTEXT",lmr) -> - match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr - | Node(_,"MATCH",lmr) -> - match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr + VTactic (letcut_interp ist ast l) + | Node(_,"MATCHCONTEXT",lmr) -> match_context_interp ist ast lmr + | Node(_,"MATCH",lmr) -> match_interp ist ast lmr | Node(_,"IDTAC",[]) -> VTactic tclIDTAC | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0) | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n)) | Node(_,"PROGRESS",[tac]) -> - VTactic (tclPROGRESS (tac_interp lfun lmatch debug tac)) + VTactic (tclPROGRESS (tactic_interp ist tac)) | Node(_,"TACTICLIST",l) -> - VTactic (interp_semi_list tclIDTAC lfun lmatch debug l) + VTactic (interp_semi_list tclIDTAC ist.lfun ist.lmatch ist.debug l) | Node(_,"DO",[n;tac]) -> - VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch debug tac)) - | Node(_,"TRY",[tac]) -> - VTactic (tclTRY (tac_interp lfun lmatch debug tac)) - | Node(_,"INFO",[tac]) -> - VTactic (tclINFO (tac_interp lfun lmatch debug tac)) - | Node(_,"REPEAT",[tac]) -> - VTactic (tclREPEAT (tac_interp lfun lmatch debug tac)) + VTactic (tclDO (num_of_ast n) (tactic_interp ist tac)) + | Node(_,"TRY",[tac]) -> VTactic (tclTRY (tactic_interp ist tac)) + | Node(_,"INFO",[tac]) -> VTactic (tclINFO (tactic_interp ist tac)) + | Node(_,"REPEAT",[tac]) -> VTactic (tclREPEAT (tactic_interp ist tac)) | Node(_,"ORELSE",[tac1;tac2]) -> - VTactic (tclORELSE (tac_interp lfun lmatch debug tac1) - (tac_interp lfun lmatch debug tac2)) - | Node(_,"FIRST",l) -> - VTactic (tclFIRST (List.map (tac_interp lfun lmatch debug) l)) + VTactic (tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2)) + | Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tactic_interp ist) l)) | Node(_,"TCLSOLVE",l) -> - VTactic (tclSOLVE (List.map (tac_interp lfun lmatch debug) l)) + VTactic (tclSOLVE (List.map (tactic_interp ist) l)) | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> - val_interp (evc,env,lfun,lmatch,goalopt,debug) - (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l)) + val_interp ist + (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l)) | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> - VFTactic ([],(interp_atomic opn)) + VFTactic ([],(interp_atomic opn)) | Node(_,"VOID",[]) -> VVoid | Nvar(_,s) -> - (try (unrec (List.assoc s lfun)) - with | Not_found -> - (try (vcontext_interp goalopt (lookup s)) - with | Not_found -> VArg (Identifier s))) + (try (unrec (List.assoc s ist.lfun)) + with | Not_found -> + (try (vcontext_interp ist.goalopt (lookup s)) + with | Not_found -> VArg (Identifier s))) | Node(_,"QUALIDARG",[Nvar(_,s)]) -> - (try (make_qid (unrec (List.assoc s lfun))) - with | Not_found -> - VArg (Qualid (qid_interp (evc,env,lfun,lmatch,goalopt,debug) ast))) + (try (make_qid (unrec (List.assoc s ist.lfun))) + with | Not_found -> + VArg (Qualid (qid_interp ist ast))) | Node(_,"QUALIDARG",_) | Node(_,"QUALIDMETA",_) -> - VArg (Qualid (qid_interp (evc,env,lfun,lmatch,goalopt,debug) ast)) + VArg (Qualid (qid_interp ist ast)) | Str(_,s) -> VArg (Quoted_string s) | Num(_,n) -> VArg (Integer n) - | Node(_,"COMMAND",[c]) -> - com_interp (evc,env,lfun,lmatch,goalopt,debug) c - | Node(_,"CASTEDCOMMAND",[c]) -> - cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) c - | Node(_,"CASTEDOPENCOMMAND",[c]) -> - cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) c + | Node(_,"COMMAND",[c]) -> com_interp ist c + | Node(_,"CASTEDCOMMAND",[c]) -> cast_com_interp ist c + | Node(_,"CASTEDOPENCOMMAND",[c]) -> cast_opencom_interp ist c | Node(_,"BINDINGS",astl) -> - VArg (Cbindings (List.map (bind_interp - (evc,env,lfun,lmatch,goalopt,debug)) astl)) + VArg (Cbindings (List.map (bind_interp ist) astl)) | Node(_,"REDEXP",[Node(_,redname,args)]) -> - VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) - (redname,args))) + VArg (Redexp (redexp_of_ast ist (redname,args))) | Node(_,"CLAUSE",cl) -> - VArg (Clause (List.map (clause_interp - (evc,env,lfun,lmatch,goalopt,debug)) cl)) + VArg (Clause (List.map (clause_interp ist) cl)) | Node(_,"TACTIC",[ast]) -> - VArg (Tac ((tac_interp lfun lmatch debug ast),ast)) + VArg (Tac ((tactic_interp ist ast),ast)) (*Remains to treat*) | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> - VArg ((Fixexp (s,n,c))) + VArg ((Fixexp (s,n,c))) | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> - VArg ((Cofixexp (s,c))) + VArg ((Cofixexp (s,c))) (*End of Remains to treat*) | Node(_,"INTROPATTERN", [ast]) -> - VArg ((Intropattern (cvt_intro_pattern - (evc,env,lfun,lmatch,goalopt,debug) ast))) + VArg ((Intropattern (cvt_intro_pattern ist ast))) | Node(_,"LETPATTERNS",astl) -> - VArg (Letpatterns (List.fold_left (cvt_letpattern - (evc,env,lfun,lmatch,goalopt,debug)) (None,[]) astl)) + VArg (Letpatterns (List.fold_left (cvt_letpattern ist) (None,[]) astl)) | Node(loc,s,l) -> - (try - ((look_for_interp s) (evc,env,lfun,lmatch,goalopt,debug) ast) - with + (try + ((look_for_interp s) ist ast) + with Not_found -> - val_interp (evc,env,lfun,lmatch,goalopt,debug) - (Node(dummy_loc,"APPTACTIC",[ast]))) + val_interp ist (Node(dummy_loc,"APPTACTIC",[ast]))) | Dynamic(_,t) -> - env_update (evc,env,lfun,lmatch,goalopt,debug); - let f = (ocamlOut t) in - Obj.magic (val_interp (evc,env,lfun,lmatch,goalopt,debug) (f ())) + env_update ist; + let f = (ocamlOut t) in + Obj.magic (val_interp ist (f ())) | _ -> - anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR - "Unrecognizable ast: "; print_ast ast>]) in - if debug = DebugOn then - match debug_prompt goalopt ast with + anomaly_loc (Ast.loc ast, "Tacinterp.val_interp", + [<'sTR "Unrecognizable ast: "; print_ast ast>]) in + if ist.debug = DebugOn then + match debug_prompt ist.goalopt ast with | Exit -> VTactic tclIDTAC | v -> value_interp v else value_interp debug (* Interprets an application node *) -and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast = +and app_interp ist fv largs ast = match fv with | VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) | VFun(olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then if lval=[] then - val_interp (evc,env,(olfun@newlfun),lmatch,goalopt,debug) body + val_interp { ist with lfun=olfun@newlfun } body else - app_interp (evc,env,lfun,lmatch,goalopt,debug) (val_interp (evc,env, - (olfun@newlfun),lmatch,goalopt,debug) body) lval ast + app_interp ist + (val_interp {ist with lfun=olfun@newlfun } body) lval ast else VFun(olfun@newlfun,lvar,body) | _ -> - user_err_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR - "Illegal tactic application: "; print_ast ast>]) + user_err_loc (Ast.loc ast, "Tacinterp.app_interp", + [<'sTR"Illegal tactic application: "; print_ast ast>]) (* Interprets recursive expressions *) -and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function +and rec_interp ist ast = function | [Node(_,"RECCLAUSE",_)] as l -> let (name,var,body) = List.hd (read_rec_clauses l) and ve = ref VVoid in - let newve = VFun(lfun@[(name,VRec ve)],read_fun var,body) in + let newve = VFun(ist.lfun@[(name,VRec ve)],read_fun var,body) in begin ve:=newve; !ve @@ -596,45 +595,40 @@ and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in let lenv = List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) lrc lref [] in - let lve = List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun - var,body))) lrc in + let lve = List.map (fun (name,var,body) -> + (name,VFun(ist.lfun@lenv,read_fun var,body))) lrc in begin List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; - val_interp (evc,env,(lfun@lve),lmatch,goalopt,debug) u + val_interp { ist with lfun=ist.lfun@lve } u end | _ -> - anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR - "Rec not well formed: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp", + [<'sTR"Rec not well formed: "; print_ast ast>]) (* Interprets the clauses of a Let *) -and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function +and let_interp ist ast = function | [] -> [] | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> - (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t):: - (let_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) + (id,val_interp ist t)::(let_interp ist ast tl) | _ -> - anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR - "Let not well formed: "; print_ast ast>]) + anomaly_loc (Ast.loc ast, "Tacinterp.let_interp", + [<'sTR"Let not well formed: "; print_ast ast>]) (* Interprets the clauses of a LetCutIn *) -and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function +and letin_interp ist ast = function | [] -> [] | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> - (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t):: - (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) + (id,val_interp ist t):: (letin_interp ist ast tl) | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl -> - let typ = - constr_of_Constr (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt,debug) com)) - and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce in + let typ = constr_of_Constr (unvarg (val_interp ist com)) + and tac = val_interp ist tce in (match tac with | VArg (Constr csr) -> - (id,VArg (Constr (mkCast (csr,typ)))):: - (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) + (id,VArg (Constr (mkCast (csr,typ))))::(letin_interp ist ast tl) | VArg (Identifier id) -> (try - (id,VArg (Constr (mkCast (constr_of_id id goalopt,typ)))):: - (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) + (id,VArg (Constr (mkCast (constr_of_id id ist.goalopt,typ)))):: + (letin_interp ist ast tl) with | Not_found -> errorlabstrm "Tacinterp.letin_interp" [< 'sTR "Term or tactic expected" >]) @@ -642,7 +636,7 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function (try let t = tactic_of_value tac in let ndc = - (match goalopt with + (match ist.goalopt with | None -> Global.named_context () | Some g -> pf_hyps g) in start_proof id NeverDischarge ndc typ; @@ -650,8 +644,7 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function let (_,({const_entry_body = pft; const_entry_type = _},_)) = cook_proof () in delete_proof id; - (id,VArg (Constr (mkCast (pft,typ)))):: - (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) + (id,VArg (Constr (mkCast (pft,typ))))::(letin_interp ist ast tl) with | NotTactic -> delete_proof id; errorlabstrm "Tacinterp.letin_interp" @@ -661,15 +654,13 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function [<'sTR "LetIn not well formed: "; print_ast ast>]) (* Interprets the clauses of a LetCut *) -and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function +and letcut_interp ist ast = function | [] -> tclIDTAC | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl -> - let typ = - constr_of_Constr (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt,debug) com)) - and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce + let typ = constr_of_Constr (unvarg (val_interp ist com)) + and tac = val_interp ist tce and (ndc,ccl) = - match goalopt with + match ist.goalopt with | None -> errorlabstrm "Tacinterp.letcut_interp" [< 'sTR "Do not use Let for toplevel definitions, use Lemma, ... instead" >] @@ -679,19 +670,20 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function let cutt = interp_atomic "Cut" [Constr typ] and exat = interp_atomic "Exact" [Constr csr] in tclTHENS cutt [tclTHEN (introduction id) - (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] + (letcut_interp ist ast tl);exat] (* let lic = mkLetIn (Name id,csr,typ,ccl) in let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) - (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) + (letcut_interp ist ast tl))*) | VArg (Identifier ir) -> (try let cutt = interp_atomic "Cut" [Constr typ] - and exat = interp_atomic "Exact" [Constr (constr_of_id ir goalopt)] in + and exat = + interp_atomic "Exact" [Constr (constr_of_id ir ist.goalopt)] in tclTHENS cutt [tclTHEN (introduction id) - (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] + (letcut_interp ist ast tl);exat] with | Not_found -> errorlabstrm "Tacinterp.letin_interp" [< 'sTR "Term or tactic expected" >]) @@ -706,12 +698,12 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function let cutt = interp_atomic "Cut" [Constr typ] and exat = interp_atomic "Exact" [Constr pft] in tclTHENS cutt [tclTHEN (introduction id) - (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] + (letcut_interp ist ast tl);exat] (* let lic = mkLetIn (Name id,pft,typ,ccl) in let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) - (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) + (letcut_interp ist ast tl))*) with | NotTactic -> delete_proof id; errorlabstrm "Tacinterp.letcut_interp" @@ -721,38 +713,40 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function "LetCut not well formed: "; print_ast ast>]) (* Interprets the Match Context expressions *) -and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = +and match_context_interp ist ast lmr = (* let goal = (match goalopt with | None -> errorlabstrm "Tacinterp.apply_match_context" [< 'sTR "No goal available" >] | Some g -> g) in*) - let rec apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal nocc (id,c) + let rec apply_goal_sub ist goal nocc (id,c) csr mt mhyps hyps = try let (lgoal,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in if mhyps = [] then - eval_with_fail (val_interp - (evc,env,lctxt@lfun,lgoal@lmatch,Some goal,debug)) mt goal + eval_with_fail + (val_interp + { ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch; + goalopt=Some goal}) + mt goal else - apply_hyps_context evc env (lctxt@lfun) lmatch goal debug mt lgoal - mhyps hyps + apply_hyps_context {ist with goalopt=Some goal} mt lgoal mhyps hyps with | (FailError _) as e -> raise e | NextOccurrence _ -> raise No_match | No_match | _ -> - apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal (nocc + 1) (id,c) + apply_goal_sub ist goal (nocc + 1) (id,c) csr mt mhyps hyps in - let rec apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal = + let rec apply_match_context ist goal = function | (All t)::tl -> (try - eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal,debug)) t + eval_with_fail (val_interp {ist with goalopt=Some goal }) t goal with No_match | _ -> - apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl) + apply_match_context ist goal tl) | (Pat (mhyps,mgoal,mt))::tl -> let hyps = make_hyps (List.rev (pf_hyps goal)) and concl = pf_concl goal in @@ -761,23 +755,20 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = (try (let lgoal = apply_matching mg concl in begin - db_matched_concl debug env concl; + db_matched_concl ist.debug ist.env concl; if mhyps = [] then eval_with_fail (val_interp - (evc,env,lfun,lgoal@lmatch,Some goal,debug)) mt goal + {ist with lmatch=lgoal@ist.lmatch; goalopt=Some goal}) mt goal else - apply_hyps_context evc env lfun lmatch goal debug mt lgoal mhyps + apply_hyps_context { ist with goalopt=Some goal} mt lgoal mhyps hyps end) - with | No_match | _ -> - apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl) + with | No_match | _ -> apply_match_context ist goal tl) | Subterm (id,mg) -> (try - apply_goal_sub (evc,env,lfun,lmatch,goalopt,debug) goal 0 (id,mg) - concl mt mhyps hyps + apply_goal_sub ist goal 0 (id,mg) concl mt mhyps hyps with - | No_match | _ -> - apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal tl)) + | No_match | _ -> apply_match_context ist goal tl)) | _ -> errorlabstrm "Tacinterp.apply_match_context" [<'sTR "No matching clauses for Match Context">] in @@ -785,14 +776,15 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = (fun goal -> let evc = project goal and env = pf_env goal in - apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal - (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in + apply_match_context ist goal + (read_match_context_rule ist.evc ist.env + (constr_list ist.goalopt ist.lfun) lmr)) in -(* (fun (evc,env,lfun,lmatch,goalopt,debug) goal -> - apply_match_context (evc,env,lfun,lmatch,goalopt,debug) goal +(* (fun ist goal -> + apply_match_context ist goal (read_match_context_rule evc env (constr_list goalopt lfun) lmr)) in*) - (match goalopt with + (match ist.goalopt with | None -> VContext app_wo_goal | Some g -> app_wo_goal g) @@ -800,43 +792,44 @@ and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = (constr_list goalopt lfun) lmr)*) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch - mhyps hyps = - let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun - lmatch mhyps lhyps_mhyp lhyps_rest noccopt = +and apply_hyps_context ist mt lgmatch mhyps hyps = + let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp + lhyps_rest noccopt = + let goal = match ist.goalopt with Some g -> g | _ -> assert false in match mhyps with | hd::tl -> let (lid,lc,lm,newlhyps,hyp_match,noccopt) = apply_one_mhyp_context lmatch hd lhyps_mhyp noccopt in begin - db_matched_hyp debug env hyp_match; + db_matched_hyp ist.debug ist.env hyp_match; (try if tl = [] then - eval_with_fail (val_interp (evc,env,(lfun@lid@lc@lfun_glob), - (lmatch@lm@lmatch_glob),Some goal,debug)) mt goal + eval_with_fail + (val_interp {ist with lfun=lfun@lid@lc@ist.lfun; + lmatch=lmatch@lm@ist.lmatch; + goalopt=Some goal}) + mt goal else let nextlhyps = List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) [] lhyps_rest in - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt + apply_hyps_context_rec ist mt (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None with | (FailError _) as e -> raise e | _ -> (match noccopt with | None -> - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun + apply_hyps_context_rec ist mt lfun lmatch mhyps newlhyps lhyps_rest None | Some nocc -> - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun - lmatch mhyps (hyp_match::newlhyps) lhyps_rest (Some (nocc + - 1)))) + apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps + (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1)))) end | [] -> anomalylabstrm "apply_hyps_context_rec" [<'sTR "Empty list should not occur" >] in - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps - hyps hyps None + apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None (* Interprets a VContext value *) and vcontext_interp goalopt = function @@ -847,78 +840,81 @@ and vcontext_interp goalopt = function | v -> v (* Interprets the Match expressions *) -and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = - let rec apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) nocc (id,c) csr +and match_interp ist ast lmr = + let rec apply_sub_match ist nocc (id,c) csr mt = - match goalopt with + match ist.goalopt with | None -> (try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug) mt + val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} mt with | NextOccurrence _ -> raise No_match) | Some g -> (try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - eval_with_fail (val_interp - (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug)) mt g + eval_with_fail (val_interp { ist with lfun=lctxt@ist.lfun; + lmatch=lm@ist.lmatch}) + mt g with | NextOccurrence n -> raise No_match | (FailError _) as e -> raise e - | _ -> - apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) (nocc + 1) (id,c) - csr mt) + | _ -> apply_sub_match ist (nocc + 1) (id,c) csr mt) in - let rec apply_match (evc,env,lfun,lmatch,goalopt,debug) csr = function + let rec apply_match ist csr = function | (All t)::_ -> - (match goalopt with + (match ist.goalopt with | None -> - (try val_interp (evc,env,lfun,lmatch,goalopt,debug) t - with | No_match | _ -> - apply_match (evc,env,lfun,lmatch,goalopt,debug) csr []) + (try val_interp ist t + with | No_match | _ -> apply_match ist csr []) | Some g -> (try - eval_with_fail (val_interp (evc,env,lfun,lmatch,goalopt,debug)) t g + eval_with_fail (val_interp ist) t g with | (FailError _) as e -> raise e - | _ -> apply_match (evc,env,lfun,lmatch,goalopt,debug) csr [])) + | _ -> apply_match ist csr [])) | (Pat ([],mp,mt))::tl -> (match mp with | Term c -> - (match goalopt with + (match ist.goalopt with | None -> (try val_interp - (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug) mt + { ist with lmatch=(apply_matching c csr)@ist.lmatch } mt with | No_match | _ -> - apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl) + apply_match ist csr tl) | Some g -> (try eval_with_fail (val_interp - (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug)) mt g + { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g with | (FailError _) as e -> raise e - | _ -> apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl)) + | _ -> apply_match ist csr tl)) | Subterm (id,c) -> (try - apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) 0 (id,c) csr mt + apply_sub_match ist 0 (id,c) csr mt with | No_match -> - apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl)) + apply_match ist csr tl)) | _ -> errorlabstrm "Tacinterp.apply_match" [<'sTR "No matching clauses for Match">] in let csr = - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) - (List.hd lmr))) - and ilr = read_match_rule evc env (constr_list goalopt lfun) (List.tl lmr) in - apply_match (evc,env,lfun,lmatch,goalopt,debug) csr ilr + constr_of_Constr (unvarg (val_interp ist (List.hd lmr))) + and ilr = read_match_rule + ist.evc ist.env (constr_list ist.goalopt ist.lfun) (List.tl lmr) in + apply_match ist csr ilr + +and tactic_interp ist ast g = + tac_interp ist.lfun ist.lmatch ist.debug ast g (* Interprets tactic expressions *) and tac_interp lfun lmatch debug ast g = let evc = project g and env = pf_env g in - try tactic_of_value (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) g + let ist = { evc=evc; env=env; lfun=lfun; lmatch=lmatch; + goalopt=Some g; debug=debug } in + try tactic_of_value (val_interp ist ast) g with | NotTactic -> errorlabstrm "Tacinterp.tac_interp" [<'sTR "Interpretation gives a non-tactic value">] @@ -945,60 +941,54 @@ and interp_semi_list acc lfun lmatch debug = function | [] -> acc (* Interprets bindings for tactics *) -and bind_interp (evc,env,lfun,lmatch,goalopt,debug) = function +and bind_interp ist = function | Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> (NoDep n,constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[c]))))) + ist (Node(loc,"COMMAND",[c]))))) | Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> (Dep (id_of_Identifier (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) + ist (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) (Node(loc1,"COMMAND",[c]))))) + ist (Node(loc1,"COMMAND",[c]))))) | Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> (Com,constr_of_Constr (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt,debug) + (val_interp ist (Node(loc,"COMMAND",[c]))))) | x -> errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; print_ast x>] (* Interprets a COMMAND expression (in case of failure, returns Command) *) -and com_interp (evc,env,lfun,lmatch,goalopt,debug) = function +and com_interp ist = function | Node(_,"EVAL",[c;rtc]) -> - let redexp = unredexp (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) rtc)) in - VArg (Constr ((reduction_of_redexp redexp) env evc - (interp_constr_gen evc env (constr_list goalopt lfun) - lmatch c None))) + let redexp = unredexp (unvarg (val_interp ist rtc)) in + VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc + (interp_constr ist c None))) | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast -> (try - let ic = - interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None - and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in + let ic = interp_constr ist c None + and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in VArg (Constr (subst_meta [-1,ic] ctxt)) with | Not_found -> errorlabstrm "com_interp" [<'sTR "Unbound context identifier"; print_ast ast>]) - | c -> - VArg (Constr - (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None)) + | c -> VArg (Constr (interp_constr ist c None)) (* Interprets a CASTEDCOMMAND expression *) -and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com = - match goalopt with +and cast_com_interp ist com = + match ist.goalopt with | Some gl -> (match com with | Node(_,"EVAL",[c;rtc]) -> let redexp = unredexp (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) rtc)) in - VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen - evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl))))) + ist rtc)) in + VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc + (interp_constr ist c (Some (pf_concl gl))))) | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast -> (try - let ic = - interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None - and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in + let ic = interp_constr ist c None + and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in begin wARNING [<'sTR "Cannot pre-constrain the context expression with goal">]; @@ -1009,26 +999,25 @@ and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com = errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier"; print_ast ast>]) | c -> - VArg (Constr (interp_constr_gen evc env (constr_list goalopt lfun) - lmatch c (Some (pf_concl gl))))) + VArg (Constr (interp_constr ist c (Some (pf_concl gl))))) | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] (* Interprets a CASTEDOPENCOMMAND expression *) -and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com = - match goalopt with +and cast_opencom_interp ist com = + match ist.goalopt with | Some gl -> (match com with | Node(_,"EVAL",[c;rtc]) -> let redexp = unredexp (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) rtc)) in - VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen - evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl))))) + ist rtc)) in + VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc + (interp_constr ist c (Some (pf_concl gl))))) | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast -> (try - let ic = - interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None - and ctxt = constr_of_Constr_context (unvarg (List.assoc s lfun)) in + let ic = interp_constr ist c None + and ctxt = + constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in begin wARNING [<'sTR "Cannot pre-constrain the context expression with goal">]; @@ -1040,76 +1029,68 @@ and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com = print_ast ast>]) | c -> VArg - (OpenConstr (interp_openconstr_gen evc env (constr_list goalopt lfun) - lmatch c (Some (pf_concl gl))))) + (OpenConstr (interp_openconstr ist c (Some (pf_concl gl))))) | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] (* Interprets a qualified name. This can be a metavariable to be injected *) -and qid_interp (evc,env,lfun,lmatch,goalopt,debug) = function +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 lmatch)) + Nametab.qualid_of_sp (path_of_const (List.assoc n ist.lmatch)) | ast -> anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR "Unrecognizable qualid ast: "; print_ast ast>]) -and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function +and cvt_pattern ist = function | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> let occs = List.map num_of_ast nums and csr = constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[com])))) in - let jdt = Typing.unsafe_machine env evc csr in + ist (Node(loc,"COMMAND",[com])))) in + let jdt = Typing.unsafe_machine ist.env ist.evc csr in (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") -and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function +and cvt_unfold ist = function | Node(_,"UNFOLD", com::nums) -> - let qid = - qualid_of_Qualid - (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) com)) in - (List.map num_of_ast nums,glob_const_nvar loc env qid) + let qid = qualid_of_Qualid (unvarg (val_interp ist com)) in + (List.map num_of_ast nums,glob_const_nvar loc ist.env qid) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") (* Interprets the arguments of Fold *) -and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function +and cvt_fold ist = function | Node(_,"COMMAND",[c]) as ast -> - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) - ast)) + constr_of_Constr (unvarg (val_interp ist ast)) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") (* Interprets the reduction flags *) -and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = +and flag_of_ast ist lf = let rec add_flag red = function | [] -> red | Node(_,"Beta",[])::lf -> add_flag (red_add red fBETA) lf + | Node(_,"Delta",[])::Node(loc,"Unf",l)::lf -> + let red = red_add_transparent (red_add red fDELTA) all_opaque in + let red = + List.fold_right + (fun v red -> + match glob_const_nvar loc ist.env (qid_interp ist v) with + | EvalVarRef id -> red_add red (fVAR id) + | EvalConstRef sp -> red_add red (fCONST sp)) l red + in add_flag red lf + | Node(_,"Delta",[])::Node(loc,"UnfBut",l)::lf -> + let red = red_add red fDELTA in + let red = red_add_transparent red (Opaque.state()) in + let red = + List.fold_right + (fun v red -> + match glob_const_nvar loc ist.env (qid_interp ist v) with + | EvalVarRef id -> red_sub red (fVAR id) + | EvalConstRef sp -> red_sub red (fCONST sp)) l red + in add_flag red lf | Node(_,"Delta",[])::lf -> - (match lf with - | Node(loc,"Unf",l)::lf -> - let idl= - List.fold_right - (fun v red -> - match glob_const_nvar loc env - (qid_interp (evc,env,lfun,lmatch,goalopt,debug) v) with - | EvalVarRef id -> red_add red (fVAR id) - | EvalConstRef sp -> red_add red (fCONST sp)) l red - in add_flag idl lf -(* -(id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l - in add_flag (red_add red (CONST idl)) lf -*) - | Node(loc,"UnfBut",l)::lf -> - let idl= - List.fold_right - (fun v red -> - match glob_const_nvar loc env - (qid_interp (evc,env,lfun,lmatch,goalopt,debug)v) with - | EvalVarRef id -> red_add red (fVARBUT id) - | EvalConstRef sp -> red_add red (fCONSTBUT sp)) l red - in add_flag idl lf - - | _ -> add_flag (red_add red fDELTA) lf) + let red = red_add red fDELTA in + let red = red_add_transparent red (Opaque.state()) in + add_flag red lf | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf | Node(_,"Evar",[])::lf -> add_flag (red_add red fEVAR) lf @@ -1122,47 +1103,37 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = add_flag no_red lf; (* Interprets a reduction expression *) -and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function +and redexp_of_ast ist = function | ("Red", []) -> Red false | ("Hnf", []) -> Hnf | ("Simpl", []) -> Simpl - | ("Unfold", ul) -> - Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt,debug)) ul) - | ("Fold", cl) -> - Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt,debug)) cl) - | ("Cbv",lf) -> - Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf) - | ("Lazy",lf) -> - Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf) - | ("Pattern",lp) -> - Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt,debug)) lp) + | ("Unfold", ul) -> Unfold (List.map (cvt_unfold ist) ul) + | ("Fold", cl) -> Fold (List.map (cvt_fold ist) cl) + | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast ist lf) + | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast ist lf) + | ("Pattern",lp) -> Pattern (List.map (cvt_pattern ist) lp) | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) (* Interprets the patterns of Intro *) -and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function +and cvt_intro_pattern ist = function | Node(_,"WILDCAR", []) -> WildPat | Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> - IdPat (id_of_Identifier (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s))))) + IdPat (id_of_Identifier (unvarg (val_interp ist (Nvar (loc,s))))) | Node(_,"DISJPATTERN", l) -> - DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) - l) + DisjPat (List.map (cvt_intro_pattern ist) l) | Node(_,"CONJPATTERN", l) -> - ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) - l) + ConjPat (List.map (cvt_intro_pattern ist) l) | Node(_,"LISTPATTERN", l) -> - ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) - l) + ListPat (List.map (cvt_intro_pattern ist) l) | x -> errorlabstrm "cvt_intro_pattern" - [<'sTR "Not the expected form for an introduction pattern!"; print_ast - x>] + [<'sTR "Not the expected form for an introduction pattern!";'fNL; + print_ast x>] (* Interprets a pattern of Let *) -and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function +and cvt_letpattern ist (o,l) = function | Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> - (o,(id_of_Identifier (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) + (o,(id_of_Identifier (unvarg (val_interp ist (Nvar (loc,s)))),List.map num_of_ast nums)::l) | Node(_,"CCLPATTERN", nums) -> if o <> None then @@ -1200,7 +1171,10 @@ let bad_tactic_args s = let (inMD,outMD) = let add (na,td) = mactab := Gmap.add na td !mactab in let cache_md (_,(na,td)) = - let ve=val_interp (Evd.empty,Global.env (),[],[],None,get_debug ()) td + let ve=val_interp + {evc=Evd.empty;env=Global.env ();lfun=[]; + lmatch=[]; goalopt=None; debug=get_debug ()} + td in add (na,ve) in declare_object ("TAC-DEFINITION", {cache_function = cache_md; diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index f6be50869..41b105f7b 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -31,8 +31,12 @@ type value = (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = - enamed_declarations * Environ.env * (identifier * value) list * - (int * constr) list * goal sigma option * debug_info + { evc : enamed_declarations; + env : Environ.env; + lfun : (identifier * value) list; + lmatch : (int * constr) list; + goalopt : goal sigma option; + debug : debug_info } (* Gives the constr corresponding to a CONSTR [tactic_arg] *) val constr_of_Constr : tactic_arg -> constr diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a52f24b0e..c8d1c4370 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -88,9 +88,9 @@ let _ = vinterp_add "HintRewrite" let lcsr = List.map (function | Node(loc,"CONSTR",l) -> - constr_of_Constr (interp_tacarg - (evc,env,[],[],None,Tactic_debug.DebugOff) - (Node(loc,"COMMAND",l))) + let ist = { evc=evc; env=env; lfun=[]; lmatch=[]; + goalopt=None; debug=Tactic_debug.DebugOff } in + constr_of_Constr (interp_tacarg ist (Node(loc,"COMMAND",l))) | _ -> bad_vernac_args "HintRewrite") lcom in add_rew_rules (string_of_id id) (List.map (fun csr -> (csr,ort = "LR",t)) lcsr)) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index f7bf462dc..31dddc038 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -236,8 +236,10 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in let _ = declare_constant name - (ConstantEntry { const_entry_body = invProof; const_entry_type = None }, - NeverDischarge,false) + (ConstantEntry { const_entry_body = invProof; + const_entry_type = None; + const_entry_opaque = false }, + NeverDischarge) in () (* open Pfedit *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index cc18b64c1..10dcee8d7 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -229,12 +229,14 @@ let add_setoid a aeq th = let eq_ext_name2 = gen_eq_lem_name () in let _ = Declare.declare_constant eq_ext_name ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph; - Declarations.const_entry_type = None}), - Declare.NeverDischarge,true) in + Declarations.const_entry_type = None; + Declarations.const_entry_opaque = true}), + Declare.NeverDischarge) in let _ = Declare.declare_constant eq_ext_name2 ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph2; - Declarations.const_entry_type = None}), - Declare.NeverDischarge,true) in + Declarations.const_entry_type = None; + Declarations.const_entry_opaque = true}), + Declare.NeverDischarge) in let eqmorph = (current_constant eq_ext_name) in let eqmorph2 = (current_constant eq_ext_name2) in (Lib.add_anonymous_leaf @@ -452,8 +454,9 @@ let add_morphism lem_name (m,profil) = let lem2_name = add_suffix lem_name "2" in let _ = Declare.declare_constant lem2_name ((Declare.ConstantEntry {Declarations.const_entry_body = lem_2; - Declarations.const_entry_type = None}), - Declare.NeverDischarge,true) in + Declarations.const_entry_type = None; + Declarations.const_entry_opaque = true}), + Declare.NeverDischarge) in let lem2 = (current_constant lem2_name) in (Lib.add_anonymous_leaf (morphism_to_obj (m, diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 18cb8ee50..11c82f518 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1823,7 +1823,7 @@ let abstract_subproof name tac gls = with e when catchable_exception e -> (delete_current_proof(); raise e) in (* Faudrait un peu fonctionnaliser cela *) - let sp = Declare.declare_constant na (ConstantEntry const,strength,true) in + let sp = Declare.declare_constant na (ConstantEntry const,strength) in let newenv = Global.env() in Declare.constr_of_reference Evd.empty newenv (ConstRef sp) in diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index d847a060d..694351b67 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -15,17 +15,17 @@ Proof. NewInduction n. Auto. Left; Exists n; Auto. -Qed. +Defined. Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}. Proof. NewInduction n; NewInduction m; Auto. Elim (IHn m); Auto. -Qed. +Defined. Hints Resolve O_or_S eq_nat_dec : arith. Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. -Qed. +Defined. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 14f331930..645f4b0d7 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -139,17 +139,20 @@ Section Logic_lemmas. Theorem sym_eq : (eq ? x y) -> (eq ? y x). Proof. Induction 1; Trivial. - Qed. + Defined. + Opaque sym_eq. Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z). Proof. Induction 2; Trivial. - Qed. + Defined. + Opaque trans_eq. Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)). Proof. Induction 1; Trivial. - Qed. + Defined. + Opaque f_equal. Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)). Proof. diff --git a/toplevel/class.ml b/toplevel/class.ml index 3fb0f67a5..9696557c1 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -344,8 +344,9 @@ let build_id_coercion idf_opt source = let constr_entry = (* Cast is necessary to express [val_f] is identity *) ConstantEntry { const_entry_body = mkCast (val_f, typ_f); - const_entry_type = None } in - let sp = declare_constant idf (constr_entry,NeverDischarge,false) in + const_entry_type = None; + const_entry_opaque = false } in + let sp = declare_constant idf (constr_entry,NeverDischarge) in ConstRef sp (* diff --git a/toplevel/command.ml b/toplevel/command.ml index f290d684b..5b3e3a59d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -37,26 +37,26 @@ let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) (* 1| Constant definitions *) -let constant_entry_of_com (com,comtypopt) = +let constant_entry_of_com (com,comtypopt,opacity) = let sigma = Evd.empty in let env = Global.env() in match comtypopt with None -> { const_entry_body = interp_constr sigma env com; - const_entry_type = None } + const_entry_type = None; + const_entry_opaque = opacity } | Some comtyp -> let typ = interp_type sigma env comtyp in { const_entry_body = interp_casted_constr sigma env com typ; - const_entry_type = Some typ } + const_entry_type = Some typ; + const_entry_opaque = opacity } let red_constant_entry ce = function | None -> ce | Some red -> let body = ce.const_entry_body in - { const_entry_body = - reduction_of_redexp red (Global.env()) Evd.empty body; - const_entry_type = - ce.const_entry_type } + { ce with const_entry_body = + reduction_of_redexp red (Global.env()) Evd.empty body } let constr_of_constr_entry ce = match ce.const_entry_type with @@ -64,21 +64,21 @@ let constr_of_constr_entry ce = | Some t -> mkCast (ce.const_entry_body, t) let declare_global_definition ident ce n local = - let sp = declare_constant ident (ConstantEntry ce,n,false) in + let sp = declare_constant ident (ConstantEntry ce,n) in if local then wARNING [< pr_id ident; 'sTR" is declared as a global definition" >]; if_verbose message ((string_of_id ident) ^ " is defined"); ConstRef sp let definition_body_red red_option ident (local,n) com comtypeopt = - let ce = constant_entry_of_com (com,comtypeopt) in + let ce = constant_entry_of_com (com,comtypeopt,false) in let ce' = red_constant_entry ce red_option in match n with | NeverDischarge -> declare_global_definition ident ce' n local | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let c = constr_of_constr_entry ce' in - let sp = declare_variable ident (SectionLocalDef c,n,false) in + let sp = declare_variable ident (SectionLocalDef c,n) in if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; @@ -118,7 +118,7 @@ let hypothesis_def_var is_refining ident n c = | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in - let sp = declare_variable ident (SectionLocalAssum t,n,false) in + let sp = declare_variable ident (SectionLocalAssum t,n) in if_verbose message ((string_of_id ident) ^ " is assumed"); if is_refining then mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; @@ -271,7 +271,7 @@ let build_recursive lnameargsardef = let raw_arity = mkProdCit lparams arityc in let arity = interp_type sigma env0 raw_arity in let _ = declare_variable recname - (SectionLocalAssum arity, NeverDischarge, false) in + (SectionLocalAssum arity, NeverDischarge) in (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> @@ -299,8 +299,9 @@ let build_recursive lnameargsardef = (Array.map (fun id -> Name id) namerec, arrec, recvec)); - const_entry_type = None } in - let sp = declare_constant fi (ConstantEntry ce, n, false) in + const_entry_type = None; + const_entry_opaque = false } in + let sp = declare_constant fi (ConstantEntry ce, n) in (ConstRef sp) in (* declare the recursive definitions *) @@ -312,8 +313,9 @@ let build_recursive lnameargsardef = List.fold_left (fun subst (f,def) -> let ce = { const_entry_body = replace_vars subst def; - const_entry_type = None } in - let _ = declare_constant f (ConstantEntry ce,n,false) in + const_entry_type = None; + const_entry_opaque = false } in + let _ = declare_constant f (ConstantEntry ce,n) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -333,7 +335,7 @@ let build_corecursive lnameardef = let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in let arity = arj.utj_val in let _ = declare_variable recname - (SectionLocalAssum arj.utj_val,NeverDischarge,false) in + (SectionLocalAssum arj.utj_val,NeverDischarge) in (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> @@ -360,9 +362,10 @@ let build_corecursive lnameardef = mkCoFix (i, (Array.map (fun id -> Name id) namerec, arrec, recvec)); - const_entry_type = None } + const_entry_type = None; + const_entry_opaque = false } in - let sp = declare_constant fi (ConstantEntry ce,n,false) in + let sp = declare_constant fi (ConstantEntry ce,n) in (ConstRef sp) in let lrefrec = Array.mapi declare namerec in @@ -372,8 +375,9 @@ let build_corecursive lnameardef = List.fold_left (fun subst (f,def) -> let ce = { const_entry_body = replace_vars subst def; - const_entry_type = None } in - let _ = declare_constant f (ConstantEntry ce,n,false) in + const_entry_type = None; + const_entry_opaque = false } in + let _ = declare_constant f (ConstantEntry ce,n) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -406,8 +410,10 @@ let build_scheme lnamedepindsort = let n = NeverDischarge in let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = - let ce = { const_entry_body = decl; const_entry_type = None } in - let sp = declare_constant fi (ConstantEntry ce,n,false) in + let ce = { const_entry_body = decl; + const_entry_type = None; + const_entry_opaque = false } in + let sp = declare_constant fi (ConstantEntry ce,n) in ConstRef sp :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in @@ -434,14 +440,18 @@ let apply_tac_not_declare id pft = function Pfedit.delete_current_proof (); Pfedit.by (tclTHENS cutt [introduction id;exat]) -let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) - strength = +let save id const strength = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in begin match strength with | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity -> let c = constr_of_constr_entry const in - let _ = declare_variable id (SectionLocalDef c,strength,opacity) in () + let _ = declare_variable id (SectionLocalDef c,strength) + in () | NeverDischarge | DischargeAt _ -> - let _ = declare_constant id (ConstantEntry const,strength,opacity)in () + let _ = declare_constant id (ConstantEntry const,strength) + in () | NotDeclare -> apply_tac_not_declare id pft tpo end; if not (strength = NotDeclare) then @@ -452,7 +462,8 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) let save_named opacity = let id,(const,strength) = Pfedit.cook_proof () in - save opacity id const strength + let const = { const with const_entry_opaque = opacity } in + save id const strength let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then @@ -463,13 +474,15 @@ let check_anonymity id save_ident = let save_anonymous opacity save_ident = let id,(const,strength) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; - save opacity save_ident const strength + save save_ident const strength let save_anonymous_with_strength strength opacity save_ident = let id,(const,_) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; - save opacity save_ident const strength + save save_ident const strength let get_current_context () = try Pfedit.get_current_goal_context () diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 819df64e0..61db7f6c6 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -162,9 +162,9 @@ let inductive_message inds = type opacity = bool type discharge_operation = - | Variable of identifier * section_variable_entry * strength * bool * bool + | Variable of identifier * section_variable_entry * strength * bool | Parameter of identifier * constr * bool - | Constant of section_path * recipe * strength * opacity * bool + | 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) @@ -181,7 +181,7 @@ let process_object oldenv dir sec_sp let tag = object_tag lobj in match tag with | "VARIABLE" -> - let ((id,c,t),cst,stre,sticky) = get_variable_with_constraints sp in + let ((id,c,t),cst,stre) = get_variable_with_constraints sp in (* VARIABLE means local (entry Variable/Hypothesis/Local and are *) (* always discharged *) (* @@ -227,7 +227,7 @@ let process_object oldenv dir sec_sp let r = { d_from = cb; d_modlist = work_alist; d_abstract = ids_to_discard } in - let op = Constant (newsp,r,stre,cb.const_opaque,imp) in + let op = Constant (newsp,r,stre,imp) in (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) | "INDUCTIVE" -> @@ -281,15 +281,15 @@ let process_item oldenv dir sec_sp acc = function | (_,_) -> acc let process_operation = function - | Variable (id,expmod_a,stre,sticky,imp) -> + | Variable (id,expmod_a,stre,imp) -> (* Warning:parentheses needed to get a side-effect from with_implicits *) - let _ = with_implicits imp (declare_variable id) (expmod_a,stre,sticky) in + let _ = with_implicits imp (declare_variable id) (expmod_a,stre) in () | Parameter (spid,typ,imp) -> let _ = with_implicits imp (declare_parameter spid) typ in constant_message spid - | Constant (sp,r,stre,opa,imp) -> - with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre,opa); + | Constant (sp,r,stre,imp) -> + with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre); constant_message (basename sp) | Inductive (mie,imp) -> let _ = with_implicits imp declare_mind mie in diff --git a/toplevel/record.ml b/toplevel/record.ml index 13b2891ec..a146264ed 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -117,9 +117,11 @@ let declare_projections indsp coers fields = let name = try let proj = instantiate_inductive_section_params proj indsp in - let cie = { const_entry_body = proj; const_entry_type = None} in + let cie = { const_entry_body = proj; + const_entry_type = None; + const_entry_opaque = false } in let sp = - declare_constant fi (ConstantEntry cie,NeverDischarge,false) + declare_constant fi (ConstantEntry cie,NeverDischarge) in Some sp with Type_errors.TypeError (k,ctx,te) -> begin warning_or_error coe (BadTypedProj (fi,k,ctx,te)); diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 71740fbd9..3094fbacb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -643,23 +643,26 @@ let _ = (fun id_list () -> List.iter (function - | VARG_CONSTANT sp -> Global.set_transparent sp + | VARG_QUALID qid -> + (match locate_qualid dummy_loc qid with + | ConstRef sp -> Opaque.set_transparent_const sp + | VarRef sp -> Opaque.set_transparent_var (basename sp) + | _ -> error + "cannot set an inductive type or a constructor as transparent") | _ -> bad_vernac_args "TRANSPARENT") id_list) -let warning_opaque s = - if_verbose warning - ("This command turns the constants which depend on the definition/proof -of "^s^" un-re-checkable until the next \"Transparent "^s^"\" command.") - let _ = add "OPAQUE" (fun id_list () -> List.iter (function - | VARG_CONSTANT sp -> - warning_opaque (Global.string_of_global (ConstRef sp)); - Global.set_opaque sp + | VARG_QUALID qid -> + (match locate_qualid dummy_loc qid with + | ConstRef sp -> Opaque.set_opaque_const sp + | VarRef sp -> Opaque.set_opaque_var (basename sp) + | _ -> error + "cannot set an inductive type or a constructor as opaque") | _ -> bad_vernac_args "OPAQUE") id_list) diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 3d170e6be..0b32cd141 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -32,7 +32,6 @@ type vernac_arg = | VARG_NUMBERLIST of int list | VARG_IDENTIFIER of identifier | VARG_QUALID of Nametab.qualid - | VARG_CONSTANT of constant_path | VCALL of string * vernac_arg list | VARG_CONSTR of Coqast.t | VARG_CONSTRLIST of Coqast.t list @@ -85,12 +84,6 @@ let rec cvt_varg ast = | Nvar(_,id) -> VARG_IDENTIFIER id | Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p) - | Node(loc,"QUALIDCONSTARG",p) -> - let q = Astterm.interp_qualid p in - let sp = - try Nametab.locate_constant q - with Not_found -> Nametab.error_global_constant_not_found_loc loc q - in VARG_CONSTANT sp | Str(_,s) -> VARG_STRING s | Id(_,s) -> VARG_STRING s | Num(_,n) -> VARG_NUMBER n @@ -112,7 +105,9 @@ let rec cvt_varg ast = | Node(_,"ASTLIST",al) -> VARG_ASTLIST al | Node(_,"TACTIC_ARG",[targ]) -> let (evc,env)= Command.get_current_context () in - VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None,get_debug ()) targ) + let ist = { evc=evc; env=env; lfun=[]; lmatch=[]; + goalopt=None; debug=get_debug ()} in + VARG_TACTIC_ARG (interp_tacarg ist targ) | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg", [< 'sTR "Unrecognizable ast node of vernac arg:"; diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index ed068d167..2aa45f322 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -28,7 +28,6 @@ type vernac_arg = | VARG_NUMBERLIST of int list | VARG_IDENTIFIER of identifier | VARG_QUALID of Nametab.qualid - | VARG_CONSTANT of constant_path | VCALL of string * vernac_arg list | VARG_CONSTR of Coqast.t | VARG_CONSTRLIST of Coqast.t list |