diff options
49 files changed, 846 insertions, 538 deletions
@@ -48,8 +48,6 @@ library/library.cmi: lib/pp.cmi library/nametab.cmi: kernel/names.cmi library/redinfo.cmi: kernel/names.cmi kernel/term.cmi library/summary.cmi: kernel/names.cmi -parsing/as.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.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/environ.cmi kernel/evd.cmi \ @@ -96,6 +94,9 @@ pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \ kernel/term.cmi pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ kernel/term.cmi +pretyping/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi +pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/names.cmi kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ kernel/term.cmi lib/util.cmi @@ -118,9 +119,7 @@ proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi -proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi kernel/reduction.cmi kernel/term.cmi + kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ lib/util.cmi @@ -141,12 +140,12 @@ tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi tactics/pattern.cmi \ proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi tactics/tactics.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/tacmach.cmi \ - proofs/tacred.cmi tactics/tacticals.cmi kernel/term.cmi + pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ - proofs/tacred.cmi kernel/term.cmi + pretyping/tacred.cmi kernel/term.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi @@ -359,16 +358,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -parsing/as.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \ - library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ - library/global.cmi library/impargs.cmi kernel/names.cmi parsing/pcoq.cmi \ - lib/pp.cmi pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/sign.cmi \ - kernel/term.cmi lib/util.cmi toplevel/vernac.cmi parsing/as.cmi -parsing/as.cmx: parsing/ast.cmx toplevel/command.cmi parsing/coqast.cmx \ - library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ - library/global.cmx library/impargs.cmx kernel/names.cmx parsing/pcoq.cmi \ - lib/pp.cmx pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/sign.cmx \ - kernel/term.cmx lib/util.cmx toplevel/vernac.cmx parsing/as.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.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 lib/hashcons.cmx \ @@ -378,15 +367,15 @@ parsing/astterm.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi \ - parsing/astterm.cmi -parsing/astterm.cmx: parsing/ast.cmx toplevel/command.cmi parsing/coqast.cmx \ + pretyping/syntax_def.cmi kernel/term.cmi pretyping/typing.cmi \ + lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi +parsing/astterm.cmx: parsing/ast.cmx toplevel/command.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \ kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx pretyping/pretyping.cmx \ pretyping/rawterm.cmi kernel/reduction.cmx kernel/sign.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx \ - parsing/astterm.cmi + pretyping/syntax_def.cmx kernel/term.cmx pretyping/typing.cmx \ + lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ @@ -406,15 +395,17 @@ parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \ library/global.cmi library/impargs.cmi kernel/inductive.cmi \ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi + parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi \ + pretyping/syntax_def.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ + parsing/pretty.cmi parsing/pretty.cmx: pretyping/classops.cmx kernel/constant.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx library/impargs.cmx kernel/inductive.cmx \ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi + parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx \ + pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ + parsing/pretty.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ @@ -439,11 +430,11 @@ pretyping/cases.cmo: pretyping/cases.cmi pretyping/cases.cmx: pretyping/cases.cmi pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \ kernel/generic.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \ - lib/options.cmi lib/pp.cmi library/summary.cmi proofs/tacred.cmi \ + lib/options.cmi lib/pp.cmi library/summary.cmi pretyping/tacred.cmi \ kernel/term.cmi lib/util.cmi pretyping/classops.cmi pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \ kernel/generic.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \ - lib/options.cmx lib/pp.cmx library/summary.cmx proofs/tacred.cmx \ + lib/options.cmx lib/pp.cmx library/summary.cmx pretyping/tacred.cmx \ kernel/term.cmx lib/util.cmx pretyping/classops.cmi pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \ @@ -477,24 +468,24 @@ pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \ pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \ pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \ pretyping/pretype_errors.cmi -pretyping/pretyping.cmo: parsing/ast.cmi pretyping/cases.cmi \ - pretyping/classops.cmi pretyping/coercion.cmi kernel/environ.cmi \ - pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \ - kernel/generic.cmi library/indrec.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi \ - pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \ - lib/util.cmi pretyping/pretyping.cmi -pretyping/pretyping.cmx: parsing/ast.cmx pretyping/cases.cmx \ - pretyping/classops.cmx pretyping/coercion.cmx kernel/environ.cmx \ - pretyping/evarconv.cmx pretyping/evarutil.cmx kernel/evd.cmx \ - kernel/generic.cmx library/indrec.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmi \ - pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \ - lib/util.cmx pretyping/pretyping.cmi +pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \ + pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \ + pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \ + library/indrec.cmi kernel/inductive.cmi kernel/instantiate.cmi \ + kernel/names.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/rawterm.cmi pretyping/recordops.cmi kernel/reduction.cmi \ + pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ + pretyping/pretyping.cmi +pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \ + pretyping/coercion.cmx kernel/environ.cmx pretyping/evarconv.cmx \ + pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \ + library/indrec.cmx kernel/inductive.cmx kernel/instantiate.cmx \ + kernel/names.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/rawterm.cmi pretyping/recordops.cmx kernel/reduction.cmx \ + pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ + pretyping/pretyping.cmi pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \ library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ @@ -511,6 +502,20 @@ pretyping/retyping.cmx: kernel/environ.cmx kernel/generic.cmx \ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \ lib/util.cmx pretyping/retyping.cmi +pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \ + kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ + library/summary.cmi pretyping/syntax_def.cmi +pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \ + kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmi \ + library/summary.cmx pretyping/syntax_def.cmi +pretyping/tacred.cmo: kernel/closure.cmi library/declare.cmi \ + kernel/environ.cmi kernel/generic.cmi kernel/inductive.cmi \ + kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi library/redinfo.cmi \ + kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi +pretyping/tacred.cmx: kernel/closure.cmx library/declare.cmx \ + kernel/environ.cmx kernel/generic.cmx kernel/inductive.cmx \ + kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx library/redinfo.cmx \ + kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi @@ -591,29 +596,21 @@ proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacred.cmi \ + proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi \ kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx \ + proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx \ kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi -proofs/tacred.cmo: kernel/closure.cmi library/declare.cmi kernel/environ.cmi \ - kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \ - kernel/names.cmi lib/pp.cmi library/redinfo.cmi kernel/reduction.cmi \ - kernel/term.cmi lib/util.cmi proofs/tacred.cmi -proofs/tacred.cmx: kernel/closure.cmx library/declare.cmx kernel/environ.cmx \ - kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \ - kernel/names.cmx lib/pp.cmx library/redinfo.cmx kernel/reduction.cmx \ - kernel/term.cmx lib/util.cmx proofs/tacred.cmi tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \ tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \ tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ - proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacinterp.cmi tactics/auto.cmi tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ @@ -622,7 +619,7 @@ tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ tactics/pattern.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ - proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/auto.cmi tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \ @@ -696,14 +693,14 @@ tactics/tactics.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \ kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \ tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ kernel/term.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: proofs/clenv.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx library/indrec.cmx \ kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx \ tactics/pattern.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ kernel/term.cmx lib/util.cmx tactics/tactics.cmi tactics/termdn.cmo: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi \ lib/util.cmi tactics/termdn.cmi @@ -717,6 +714,20 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx proofs/logic.cmx kernel/names.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi +toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \ + parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi library/global.cmi library/indrec.cmi \ + kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ + library/library.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ + library/states.cmi pretyping/syntax_def.cmi pretyping/tacred.cmi \ + kernel/term.cmi lib/util.cmi toplevel/command.cmi +toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/constant.cmx \ + parsing/coqast.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/generic.cmx library/global.cmx library/indrec.cmx \ + kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ + library/library.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \ + library/states.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \ + kernel/term.cmx lib/util.cmx toplevel/command.cmi toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \ toplevel/errors.cmi toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \ @@ -774,25 +785,25 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ - pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \ - library/declare.cmi kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi \ - library/global.cmi library/goptions.cmi library/impargs.cmi \ - library/lib.cmi library/libobject.cmi library/library.cmi \ - proofs/macros.cmi toplevel/metasyntax.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ - lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ + toplevel/command.cmi parsing/coqast.cmi library/declare.cmi \ + kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi library/global.cmi \ + library/goptions.cmi library/impargs.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi proofs/macros.cmi \ + toplevel/metasyntax.cmi kernel/names.cmi library/nametab.cmi \ + lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ + lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ toplevel/searchisos.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \ proofs/tacmach.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ - pretyping/classops.cmx toplevel/command.cmi parsing/coqast.cmx \ - library/declare.cmx kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \ - library/global.cmx library/goptions.cmx library/impargs.cmx \ - library/lib.cmx library/libobject.cmx library/library.cmx \ - proofs/macros.cmx toplevel/metasyntax.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx \ - lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ + toplevel/command.cmx parsing/coqast.cmx library/declare.cmx \ + kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi library/global.cmx \ + library/goptions.cmx library/impargs.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx proofs/macros.cmx \ + toplevel/metasyntax.cmx kernel/names.cmx library/nametab.cmx \ + lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \ + lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ toplevel/searchisos.cmi lib/stamps.cmx library/states.cmx lib/system.cmx \ proofs/tacmach.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ @@ -47,30 +47,31 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ library/global.cmo library/states.cmo library/library.cmo \ library/nametab.cmo library/impargs.cmo library/redinfo.cmo \ - library/indrec.cmo library/declare.cmo + library/indrec.cmo library/declare.cmo library/goptions.cmo -PRETYPING=pretyping/retyping.cmo pretyping/typing.cmo \ +PRETYPING=pretyping/tacred.cmo pretyping/pretype_errors.cmo \ + pretyping/retyping.cmo pretyping/typing.cmo \ pretyping/classops.cmo pretyping/recordops.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ - pretyping/pretype_errors.cmo pretyping/coercion.cmo \ - pretyping/cases.cmo pretyping/pretyping.cmo + pretyping/coercion.cmo \ + pretyping/cases.cmo pretyping/pretyping.cmo \ + pretyping/syntax_def.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_cases.cmo\ - parsing/printer.cmo parsing/pretty.cmo \ - parsing/termast.cmo parsing/astterm.cmo \ - parsing/egrammar.cmo + parsing/extend.cmo parsing/termast.cmo \ + parsing/esyntax.cmo parsing/printer.cmo parsing/pretty.cmo \ + parsing/astterm.cmo parsing/egrammar.cmo -PROOFS=proofs/tacred.cmo \ - proofs/proof_trees.cmo proofs/logic.cmo \ - proofs/refiner.cmo proofs/evar_refiner.cmo \ +PROOFS=proofs/proof_trees.cmo proofs/logic.cmo \ + proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo \ proofs/pfedit.cmo TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ - tactics/wcclausenv.cmo tactics/tacticals.cmo \ + tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \ tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ @@ -89,10 +90,10 @@ CMX=$(CMO:.cmo=.cmx) world: minicoq coqtop.byte dev/db_printers.cmo -LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) -# $(PARSING) $(PROOFS) $(TACTICS) $(TOPLEVEL) +LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ + $(PROOFS) $(TACTICS) $(TOPLEVEL) link: $(LINK) - ocamlc -custom $(INCLUDES) -o link $(CMA) $(LINK) $(OSDEPLIBS) + ocamlc -custom $(INCLUDES) -o link dynlink.cma $(CMA) $(LINK) $(OSDEPLIBS) rm -f link lib: $(LIB) @@ -110,7 +111,7 @@ coqtop: $(CMX) $(OCAMLOPT) $(INCLUDES) -o coqtop $(CMXA) $(CMX) $(OSDEPLIBS) coqtop.byte: $(CMO) - ocamlmktop $(INCLUDES) -o coqtop.byte -custom $(CMA) \ + ocamlmktop $(INCLUDES) -o coqtop.byte -custom dynlink.cma $(CMA) \ $(CMO) $(OSDEPLIBS) # minicoq diff --git a/kernel/evd.ml b/kernel/evd.ml index cc95958bc..6853fc9c4 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -23,7 +23,7 @@ type 'a evar_info = { evar_concl : constr; evar_env : env; evar_body : evar_body; - evar_info : 'a } + evar_info : 'a option } type 'a evar_map = 'a evar_info Intmap.t diff --git a/kernel/evd.mli b/kernel/evd.mli index 1b00cddb4..e9f7818ff 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -26,7 +26,7 @@ type 'a evar_info = { evar_concl : constr; evar_env : env; evar_body : evar_body; - evar_info : 'a } + evar_info : 'a option } type 'a evar_map diff --git a/kernel/names.ml b/kernel/names.ml index e04a41f42..dd7ad6f3a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -202,6 +202,9 @@ let sp_of_wd = function | bn::dp -> make_path dp (id_of_string bn) OBJ | _ -> invalid_arg "Names.sp_of_wd" +let wd_of_sp sp = + let (sp,id,_) = repr_path sp in sp @ [string_of_id id] + let sp_ord sp1 sp2 = let (p1,id1,k) = repr_path sp1 and (p2,id2,k') = repr_path sp2 in diff --git a/kernel/names.mli b/kernel/names.mli index b3f5811e4..1ccf3c12c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -50,6 +50,7 @@ val basename : section_path -> identifier val kind_of_path : section_path -> path_kind val sp_of_wd : string list -> section_path +val wd_of_sp : section_path -> string list val path_of_string : string -> section_path val string_of_path : section_path -> string diff --git a/lib/util.ml b/lib/util.ml index 0cab4540e..e1e524cf4 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -13,6 +13,12 @@ exception UserError of string * std_ppcmds (* User errors *) let error string = raise (UserError(string,[< 'sTR string >])) let errorlabstrm l pps = raise (UserError(l,pps)) +(* raising located exceptions *) +type loc = int * int +let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) +let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) +let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) + (* Strings *) let explode s = @@ -214,6 +220,14 @@ let list_share_tails l1 l2 = in shr_rev [] (List.rev l1, List.rev l2) +let list_except_assoc e = + let rec except_e = function + | [] -> [] + | (x,_ as y)::l -> if x=e then l else y::except_e l + in + except_e + + (* Arrays *) let array_exists f v = diff --git a/lib/util.mli b/lib/util.mli index a3a20aaac..2060b7375 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -19,6 +19,12 @@ exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a +type loc = int * int + +val anomaly_loc : loc * string * std_ppcmds -> 'a +val user_err_loc : loc * string * std_ppcmds -> 'a +val invalid_arg_loc : loc * string -> 'a + (*s Strings. *) val explode : string -> string list @@ -63,6 +69,8 @@ val list_map_append : ('a -> 'b list) -> 'a list -> 'b list (* raises [Invalid_argument] if the two lists don't have the same length *) val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list +val list_except_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list + (*s Arrays. *) diff --git a/library/declare.ml b/library/declare.ml index 7dca2b1c8..2305f31ff 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -47,6 +47,7 @@ let _ = Summary.declare_summary "VARIABLE" let cache_variable (sp,(id,(ty,_,_) as vd)) = Global.push_var (id,ty); Nametab.push id sp; + declare_var_implicits id; vartab := Spmap.add sp vd !vartab let load_variable _ = @@ -69,16 +70,19 @@ let (in_variable, out_variable) = let declare_variable id ((ty,_,_) as obj) = Global.push_var (id,ty); let sp = add_leaf id CCI (in_variable (id,obj)) in - Nametab.push id sp + Nametab.push id sp; + declare_var_implicits id (* Parameters. *) let cache_parameter (sp,c) = Global.add_parameter sp c; - Nametab.push (basename sp) sp + Nametab.push (basename sp) sp; + declare_constant_implicits sp let open_parameter (sp,_) = - Nametab.push (basename sp) sp + Nametab.push (basename sp) sp; + declare_constant_implicits sp let specification_parameter obj = obj @@ -93,7 +97,8 @@ let (in_parameter, out_parameter) = let declare_parameter id c = let sp = add_leaf id CCI (in_parameter c) in Global.add_parameter sp c; - Nametab.push (basename sp) sp + Nametab.push (basename sp) sp; + declare_constant_implicits sp (* Constants. *) @@ -169,41 +174,6 @@ let declare_mind mie = push_inductive_names sp mie; declare_inductive_implicits sp -(* Syntax constants. *) - -let syntax_table = ref (Idmap.empty : constr Idmap.t) - -let _ = Summary.declare_summary - "SYNTAXCONSTANT" - { Summary.freeze_function = (fun () -> !syntax_table); - Summary.unfreeze_function = (fun ft -> syntax_table := ft); - Summary.init_function = (fun () -> syntax_table := Idmap.empty) } - -let add_syntax_constant id c = - syntax_table := Idmap.add id c !syntax_table - -let cache_syntax_constant (sp,c) = - add_syntax_constant (basename sp) c; - Nametab.push (basename sp) sp - -let open_syntax_constant (sp,_) = - Nametab.push (basename sp) sp - -let (in_syntax_constant, out_syntax_constant) = - let od = { - cache_function = cache_syntax_constant; - load_function = (fun _ -> ()); - open_function = open_syntax_constant; - specification_function = (fun x -> x) } in - declare_object ("SYNTAXCONSTANT", od) - -let declare_syntax_constant id c = - let sp = add_leaf id CCI (in_syntax_constant c) in - add_syntax_constant id c; - Nametab.push (basename sp) sp - -let out_syntax_constant id = Idmap.find id !syntax_table - (* Test and access functions. *) let is_constant sp = @@ -273,6 +243,8 @@ let global_reference_imps kind id = c, list_of_implicits (constructor_implicits ((sp,i),j)) | _ -> assert false +let global env id = global_reference CCI id + let is_global id = try let osp = Nametab.sp_of_id CCI id in diff --git a/library/declare.mli b/library/declare.mli index a8848660d..11f6b2497 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,7 +23,6 @@ type strength = type variable_declaration = constr * strength * bool val declare_variable : identifier -> variable_declaration -> unit - type constant_declaration = constant_entry * strength * bool val declare_constant : identifier -> constant_declaration -> unit @@ -33,8 +32,6 @@ val declare_mind : mutual_inductive_entry -> unit val declare_eliminations : section_path -> unit -val declare_syntax_constant : identifier -> constr -> unit - val make_strength : string list -> strength val make_strength_0 : unit -> strength val make_strength_1 : unit -> strength @@ -49,7 +46,6 @@ val is_variable : identifier -> bool val out_variable : section_path -> identifier * typed_type * strength * bool val variable_strength : identifier -> strength -val out_syntax_constant : identifier -> constr (*s It also provides a function [global_reference] to construct a global constr (a constant, an inductive or a constructor) from an identifier. @@ -61,6 +57,8 @@ val global_operator : section_path -> identifier -> sorts oper * var_context val global_reference : path_kind -> identifier -> constr val global_reference_imps : path_kind -> identifier -> constr * int list +val global : Environ.env -> identifier -> constr + val is_global : identifier -> bool val mind_path : constr -> section_path diff --git a/library/goptions.ml b/library/goptions.ml index 4f5133226..a54d0870c 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -49,7 +49,7 @@ module MakeTable = let kn = nickname A.key let _ = - if List.mem_assoc kn !param_table then + if List.mem_assoc kn !param_table then error "Sorry, this table name is already used" module MyType = struct type t = A.t let compare = Pervasives.compare end @@ -81,8 +81,8 @@ module MakeTable = Libobject.open_function = open_options; Libobject.cache_function = cache_options; Libobject.specification_function = specification_options}) in - ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), - (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) + ((fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOadd, c)) in ()), + (fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOrmv, c)) in ())) else ((fun c -> t := MySet.add c !t), (fun c -> t := MySet.remove c !t)) @@ -244,8 +244,8 @@ let set_option_value check_and_cast key v = in match info with | Sync current -> - Lib.add_anonymous_leaf - (inOptVal (key,(name,check_and_cast v current))) + let _ = Lib.add_anonymous_leaf + (inOptVal (key,(name,check_and_cast v current))) in () | Async (read,write) -> write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option" diff --git a/library/impargs.ml b/library/impargs.ml index baa993312..819873282 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -91,21 +91,36 @@ let inductive_implicits_list ind_sp = let constant_implicits_list sp = list_of_implicits (constant_implicits sp) -let implicits_of_var kind id = - failwith "TODO: implicits of vars" +(* Variables. *) + +let var_table = ref Idmap.empty + +let declare_var_implicits id = + let (_,ty) = Global.lookup_var id in + let imps = auto_implicits ty.body in + var_table := Idmap.add id imps !var_table + +let implicits_of_var _ id = + list_of_implicits (Idmap.find id !var_table) (* Registration as global tables and roolback. *) -type frozen = implicits Spmap.t +type frozen_t = implicits Spmap.t + * (implicits * implicits array) array Spmap.t + * implicits Idmap.t let init () = - constants_table := Spmap.empty + constants_table := Spmap.empty; + inductives_table := Spmap.empty; + var_table := Idmap.empty let freeze () = - !constants_table + !constants_table, !inductives_table, !var_table -let unfreeze ct = - constants_table := ct +let unfreeze (ct,it,vt) = + constants_table := ct; + inductives_table := it; + var_table := vt let _ = Summary.declare_summary "implicits" diff --git a/library/impargs.mli b/library/impargs.mli index 8659b4b40..243eb8031 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -33,5 +33,9 @@ val constructor_implicits_list : constructor_path -> int list val inductive_implicits_list : inductive_path -> int list val constant_implicits_list : section_path -> int list +val declare_var_implicits : identifier -> unit val implicits_of_var : Names.path_kind -> identifier -> int list +type frozen_t +val freeze : unit -> frozen_t +val unfreeze : frozen_t -> unit diff --git a/library/lib.ml b/library/lib.ml index ea8120787..075e0e12a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -178,6 +178,7 @@ let reset_to sp = let (after,_,_) = split_lib spf in recache_context (List.rev after) +let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix (* State and initialization. *) diff --git a/library/lib.mli b/library/lib.mli index d87c4573a..826cc12e7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -39,6 +39,7 @@ val close_section : string -> unit val make_path : identifier -> path_kind -> section_path val cwd : unit -> string list +val is_section_p : section_path -> bool val open_module : string -> unit val export_module : unit -> library_segment diff --git a/library/states.ml b/library/states.ml index d8fed1437..be1241a9a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -23,6 +23,9 @@ let (extern_state,intern_state) = (* Rollback. *) +let freeze = get_state +let unfreeze = set_state + let with_heavy_rollback f x = let sum = freeze_summaries () and flib = freeze() in diff --git a/library/states.mli b/library/states.mli index 4ac371227..46cc2f68d 100644 --- a/library/states.mli +++ b/library/states.mli @@ -9,6 +9,10 @@ val intern_state : string -> unit val extern_state : string -> unit +type state +val freeze : unit -> state +val unfreeze : state -> unit + (*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation if an exception is raised. *) diff --git a/parsing/ast.ml b/parsing/ast.ml index 75fdd346e..fa0246e32 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -52,11 +52,6 @@ let section_path sl k = make_path pa (id_of_string s) (kind_of_string k) | [] -> invalid_arg "section_path" -(* raising located exceptions *) -let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) -let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) -let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) - (* ast destructors *) let num_of_ast = function | Num(_,n) -> n diff --git a/parsing/ast.mli b/parsing/ast.mli index 37823e5ad..7a65850f0 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -9,11 +9,6 @@ open Pcoq (* Abstract syntax trees. *) -(* raising located exceptions *) -val anomaly_loc : Coqast.loc * string * std_ppcmds -> 'a -val user_err_loc : Coqast.loc * string * std_ppcmds -> 'a -val invalid_arg_loc : Coqast.loc * string -> 'a - val dummy_loc : Coqast.loc val loc : Coqast.t -> Coqast.loc diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 0c56d6f0b..e8eb9c3e4 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -128,7 +128,7 @@ let ref_from_constr = function | _ -> anomaly "Not a reference" let error_var_not_found str loc s = - Ast.user_err_loc + Util.user_err_loc (loc,str, [< 'sTR "The variable"; 'sPC; 'sTR s; 'sPC ; 'sTR "was not found"; @@ -150,7 +150,7 @@ let dbize_ref k sigma env loc s = RRef (loc,ref_from_constr c), il with UserError _ -> try - RRef (loc,ref_from_constr (Declare.out_syntax_constant id)), [] + (Syntax_def.search_syntactic_definition id, []) with Not_found -> error_var_not_found "dbize_ref" loc s @@ -389,7 +389,7 @@ let ast_adjust_consts sigma = (* locations are kept *) | _ -> anomaly "Not a reference" with UserError _ | Not_found -> try - let _ = Declare.out_syntax_constant id in + let _ = Syntax_def.search_syntactic_definition id in Node(loc,"SYNCONST",[Nvar(loc,s)]) with Not_found -> warning ("Could not globalize "^s); ast) @@ -526,3 +526,96 @@ let fconstruct_with_univ sigma sign com = (univ_sp, Constraintab.current_constraints(), c) in j *) + +open Closure +open Tacred + +(* Translation of reduction expression: we need trad because of Fold + * Moreover, reduction expressions are used both in tactics and in + * vernac. *) + +let glob_nvar com = + let s = nvar_of_ast com in + try + Nametab.sp_of_id CCI (id_of_string s) + with Not_found -> + error ("unbound variable "^s) + +let cvt_pattern sigma env = function + | Node(_,"PATTERN", Node(_,"COMMAND",[com])::nums) -> + let occs = List.map num_of_ast nums in + let c = constr_of_com sigma env com in + let j = Typing.unsafe_machine env sigma c in + (occs, j.uj_val, j.uj_type) + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") + +let cvt_unfold = function + | Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums, glob_nvar com) + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") + +let cvt_fold sigma sign = function + | Node(_,"COMMAND",[c]) -> constr_of_com sigma sign c + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") + +let flag_of_ast lf = + let beta = ref false in + let delta = ref false in + let iota = ref false in + let idents = ref (None: (sorts oper -> bool) option) in + let set_flag = function + | Node(_,"Beta",[]) -> beta := true + | Node(_,"Delta",[]) -> delta := true + | Node(_,"Iota",[]) -> iota := true + | Node(loc,"Unf",l) -> + if !delta then + if !idents = None then + let idl = List.map glob_nvar l in + idents := Some + (function + | Const sp -> List.mem sp idl + | Abst sp -> List.mem sp idl + | _ -> false) + else + user_err_loc + (loc,"flag_of_ast", + [< 'sTR"Cannot specify identifiers to unfold twice" >]) + else + user_err_loc(loc,"flag_of_ast", + [< 'sTR"Delta must be specified before" >]) + | Node(loc,"UnfBut",l) -> + if !delta then + if !idents = None then + let idl = List.map glob_nvar l in + idents := Some + (function + | Const sp -> not (List.mem sp idl) + | Abst sp -> not (List.mem sp idl) + | _ -> false) + else + user_err_loc + (loc,"flag_of_ast", + [< 'sTR"Cannot specify identifiers to unfold twice" >]) + else + user_err_loc(loc,"flag_of_ast", + [< 'sTR"Delta must be specified before" >]) + | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") + in + List.iter set_flag lf; + { r_beta = !beta; + r_iota = !iota; + r_delta = match (!delta,!idents) with + | (false,_) -> (fun _ -> false) + | (true,None) -> (fun _ -> true) + | (true,Some p) -> p } + +let redexp_of_ast sigma sign = function + | ("Red", []) -> Red + | ("Hnf", []) -> Hnf + | ("Simpl", []) -> Simpl + | ("Unfold", ul) -> Unfold (List.map cvt_unfold ul) + | ("Fold", cl) -> Fold (List.map (cvt_fold sigma sign) cl) + | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast lf) + | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast lf) + | ("Pattern",lp) -> Pattern (List.map (cvt_pattern sigma sign) lp) + | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) + diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 5bcbb943d..04da5c0e6 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -40,16 +40,16 @@ val globalize_ast : Coqast.t -> Coqast.t val type_of_com : env -> Coqast.t -> typed_type -val constr_of_com_casted : unit evar_map -> env -> Coqast.t -> constr -> +val constr_of_com_casted : 'a evar_map -> env -> Coqast.t -> constr -> constr -val constr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr -val constr_of_com : unit evar_map -> env -> Coqast.t -> constr -val constr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr +val constr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr +val constr_of_com : 'a evar_map -> env -> Coqast.t -> constr +val constr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr -val fconstr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr -val fconstr_of_com : unit evar_map -> env -> Coqast.t -> constr -val fconstr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr +val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr +val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr +val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr (* Typing with Trad, and re-checking with Mach *) (*i @@ -58,6 +58,9 @@ val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type (* Typing, re-checking with universes constraints *) val fconstruct_with_univ : - unit evar_map -> context -> Coqast.t -> unsafe_judgment + 'a evar_map -> context -> Coqast.t -> unsafe_judgment i*) + +val redexp_of_ast : + 'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 43ab29db3..0548788e6 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -312,7 +312,7 @@ GEXTEND Gram match (isMeta (nvar_of_ast id), l) with | (true, []) -> id | (false, _) -> <:ast< (CALL $id ($LIST $l)) >> - | _ -> user_err_loc + | _ -> Util.user_err_loc (loc, "G_tactic.meta_tactic", [< 'sTR"Cannot apply arguments to a meta-tactic." >]) ] ] diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 61198951d..20083b8ea 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -262,7 +262,8 @@ let print_leaf_entry with_values sep (spopt,lobj) = [< 'sTR" Syntax Macro " ; print_id id ; 'sTR sep; if with_values then - let c = out_syntax_constant id in [< prterm c >] + let c = Syntax_def.search_syntactic_definition id in + [< prrawterm c >] else [<>]; 'fNL >] | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >] @@ -428,9 +429,9 @@ let print_name name = | Not_found -> (try let (_,typ) = Global.lookup_var name in - ([< print_var str typ; - try print_impl_args (implicits_of_var CCI name) - with _ -> [<>] >]) + [< print_var str typ; + try print_impl_args (implicits_of_var CCI name) + with _ -> [<>] >] with Not_found | Invalid_argument _ -> error (str ^ " not a defined object")) | Invalid_argument _ -> error (str ^ " not a defined object") diff --git a/pretyping/cases.ml b/pretyping/cases.ml new file mode 100644 index 000000000..6abd8d6ac --- /dev/null +++ b/pretyping/cases.ml @@ -0,0 +1,5 @@ + +(* $Id$ *) + +let compile_multcase _ _ _ = failwith "compile_multcase: TODO" + diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 41b3cff69..c510299ac 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -19,10 +19,10 @@ val inh_tosort : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment val inh_ass_of_j : env -> 'a evar_defs -> unsafe_judgment -> typed_type -val inh_coerce_to : env -> unit evar_defs -> +val inh_coerce_to : env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment -val inh_cast_rel : env -> unit evar_defs -> +val inh_cast_rel : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment -val inh_apply_rel_list : bool -> env -> unit evar_defs -> +val inh_apply_rel_list : bool -> env -> 'a evar_defs -> unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) -> unsafe_judgment diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9310e5dd3..972109d2f 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -11,18 +11,18 @@ open Evarutil val reset_problems : unit -> unit -val the_conv_x : env -> unit evar_defs -> constr -> constr -> bool +val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool -val the_conv_x_leq : env -> unit evar_defs -> constr -> constr -> bool +val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool (* For debugging *) val solve_pb : - env -> unit evar_defs -> conv_pb * constr * constr -> bool + env -> 'a evar_defs -> conv_pb * constr * constr -> bool val evar_conv_x : - env -> unit evar_defs -> + env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool val evar_eqappr_x : - env -> unit evar_defs -> + env -> 'a evar_defs -> conv_pb -> constr * constr list -> constr * constr list -> bool diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 226b6ff0d..c1313ee14 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -50,7 +50,7 @@ let new_isevar_sign env sigma typ args = error "new_isevar_sign: two vars have the same name"; let newev = Evd.new_evar() in let info = { evar_concl = typ; evar_env = env; - evar_body = Evar_empty; evar_info = () } in + evar_body = Evar_empty; evar_info = None } in (Evd.add sigma newev info, mkEvar newev args) (* We don't try to guess in which sort the type should be defined, since @@ -278,7 +278,7 @@ let solve_refl conv_algo isevars c1 c2 = let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in let newev = Evd.new_evar () in let info = { evar_concl = evd.evar_concl; evar_env = nenv; - evar_body = Evar_empty; evar_info = () } in + evar_body = Evar_empty; evar_info = None } in isevars := Evd.define (Evd.add !isevars newev info) ev (mkEvar newev nargs); Some [ev] diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 501e9f28e..21f489781 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -22,7 +22,7 @@ val filter_sign : 'a * identifier list * var_context val dummy_sort : constr -val do_restrict_hyps : unit evar_map -> constr -> unit evar_map * constr +val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr type 'a evar_defs = 'a evar_map ref @@ -33,11 +33,11 @@ val ise_undefined : 'a evar_defs -> constr -> bool val ise_defined : 'a evar_defs -> constr -> bool val real_clean : - unit evar_defs -> int -> (identifier * constr) list -> constr -> constr + 'a evar_defs -> int -> (identifier * constr) list -> constr -> constr val new_isevar : - unit evar_defs -> env -> constr -> path_kind -> constr * constr -val evar_define : unit evar_defs -> constr -> constr -> int list -val solve_simple_eqn : (constr -> constr -> bool) -> unit evar_defs -> + 'a evar_defs -> env -> constr -> path_kind -> constr * constr +val evar_define : 'a evar_defs -> constr -> constr -> int list +val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs -> (conv_pb * constr * constr) -> int list option val has_undefined_isevars : 'a evar_defs -> constr -> bool @@ -59,13 +59,13 @@ val mk_tycon2 : trad_constraint -> constr -> trad_constraint (* application *) val app_dom_tycon : - env -> unit evar_defs -> trad_constraint -> trad_constraint + env -> 'a evar_defs -> trad_constraint -> trad_constraint val app_rng_tycon : env -> 'a evar_defs -> constr -> trad_constraint -> trad_constraint (* abstraction *) val abs_dom_valcon : - env -> unit evar_defs -> trad_constraint -> trad_constraint + env -> 'a evar_defs -> trad_constraint -> trad_constraint val abs_rng_tycon : env -> 'a evar_defs -> trad_constraint -> trad_constraint diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 96e97a040..05d73ffa1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -213,7 +213,7 @@ let pretype_ref loc isevars env = function let metaty = try List.assoc n !trad_metamap with Not_found -> - Ast.user_err_loc + user_err_loc (loc,"pretype", [< 'sTR "Metavariable "; 'iNT n; 'sTR "remains non instanciated" >]) in @@ -297,7 +297,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) (match loc with None -> anomaly "There is an implicit argument I cannot solve" | Some loc -> - Ast.user_err_loc + user_err_loc (loc,"pretype", [< 'sTR "Cannot infer a term for this placeholder" >])) | _ -> anomaly "tycon") diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c22653dab..97ace7b8a 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -40,22 +40,22 @@ i*) (* Raw calls to the inference machine of Trad: boolean says if we must fail * on unresolved evars, or replace them by Metas *) -val ise_resolve : bool -> unit evar_map -> (int * constr) list -> +val ise_resolve : bool -> 'a evar_map -> (int * constr) list -> env -> rawconstr -> unsafe_judgment -val ise_resolve_type : bool -> unit evar_map -> (int * constr) list -> +val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list -> env -> rawconstr -> typed_type (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says * if we must coerce to a type *) -val ise_resolve1 : bool -> unit evar_map -> env -> rawconstr -> constr +val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr -val ise_resolve_casted : unit evar_map -> env -> +val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr (* progmach.ml tries to type ill-typed terms: does not perform the conversion * test in application. *) -val ise_resolve_nocheck : unit evar_map -> (int * constr) list -> +val ise_resolve_nocheck : 'a evar_map -> (int * constr) list -> env -> rawconstr -> unsafe_judgment @@ -63,5 +63,5 @@ val ise_resolve_nocheck : unit evar_map -> (int * constr) list -> * Unused outside Trad, but useful for debugging *) val pretype : - trad_constraint -> env -> unit evar_defs -> rawconstr + trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml new file mode 100644 index 000000000..85f634405 --- /dev/null +++ b/pretyping/syntax_def.ml @@ -0,0 +1,43 @@ + +(* $Id$ *) + +open Names +open Rawterm +open Libobject +open Lib + +(* Syntactic definitions. *) + +let syntax_table = ref (Idmap.empty : rawconstr Idmap.t) + +let _ = Summary.declare_summary + "SYNTAXCONSTANT" + { Summary.freeze_function = (fun () -> !syntax_table); + Summary.unfreeze_function = (fun ft -> syntax_table := ft); + Summary.init_function = (fun () -> syntax_table := Idmap.empty) } + +let add_syntax_constant id c = + syntax_table := Idmap.add id c !syntax_table + +let cache_syntax_constant (sp,c) = + add_syntax_constant (basename sp) c; + Nametab.push (basename sp) sp + +let open_syntax_constant (sp,_) = + Nametab.push (basename sp) sp + +let (in_syntax_constant, out_syntax_constant) = + let od = { + cache_function = cache_syntax_constant; + load_function = (fun _ -> ()); + open_function = open_syntax_constant; + specification_function = (fun x -> x) } in + declare_object ("SYNTAXCONSTANT", od) + +let declare_syntactic_definition id c = + let sp = add_leaf id CCI (in_syntax_constant c) in + add_syntax_constant id c; + Nametab.push (basename sp) sp + +let search_syntactic_definition id = Idmap.find id !syntax_table + diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli new file mode 100644 index 000000000..f889f2473 --- /dev/null +++ b/pretyping/syntax_def.mli @@ -0,0 +1,15 @@ + +(* $Id$ *) + +(*i*) +open Names +open Rawterm +(*i*) + +(* Syntactic definitions. *) + +val declare_syntactic_definition : identifier -> rawconstr -> unit + +val search_syntactic_definition : identifier -> rawconstr + + diff --git a/proofs/tacred.ml b/pretyping/tacred.ml index 16ea6c589..16ea6c589 100644 --- a/proofs/tacred.ml +++ b/pretyping/tacred.ml diff --git a/proofs/tacred.mli b/pretyping/tacred.mli index a1aec82cd..a1aec82cd 100644 --- a/proofs/tacred.mli +++ b/pretyping/tacred.mli diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 80aae1182..5f6af5a8b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -56,10 +56,10 @@ let applyHead n c wc = | DOP2(Prod,c1,c2) -> let c1ty = w_type_of wc c1 in let evar = new_evar_in_sign (w_env wc) in - let (evar_sp, _) = destConst evar in + let (evar_n, _) = destEvar evar in (compose (apprec (n-1) (applist(c,[evar])) (sAPP c2 evar)) - (w_Declare evar_sp (DOP2(Cast,c1,c1ty)))) + (w_Declare evar_n (DOP2(Cast,c1,c1ty)))) wc | _ -> error "Apply_Head_Then" in @@ -243,20 +243,20 @@ and w_resrec metas evars wc = | (lhs,(DOP0(Meta k) as rhs))::t -> w_resrec ((k,lhs)::metas) t wc - | (DOPN(Const evsp,_) as evar,rhs)::t -> + | (DOPN(Evar evn,_) as evar,rhs)::t -> if w_defined_const wc evar then let (wc',metas') = w_Unify rhs evar metas wc in w_resrec metas' t wc' else (try - w_resrec metas t (w_Define evsp rhs wc) + w_resrec metas t (w_Define evn rhs wc) with UserError _ -> (match rhs with | DOPN(AppL,cl) -> (match cl.(0) with | DOPN(Const sp,_) -> let wc' = mimick_evar cl.(0) - ((Array.length cl) - 1) evsp wc in + ((Array.length cl) - 1) evn wc in w_resrec metas evars wc' | _ -> error "w_Unify") | _ -> error "w_Unify")) @@ -555,13 +555,13 @@ and clenv_resrec metas evars clenv = | ((lhs,(DOP0(Meta k) as rhs))::t,metas) -> clenv_resrec ((k,lhs)::metas) t clenv - | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) -> + | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) -> if w_defined_const clenv.hook evar then let (metas',evars') = unify_0 [] clenv.hook rhs evar in clenv_resrec (metas'@metas) (evars'@t) clenv else (try - clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv) + clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv) with UserError _ -> (match rhs with | DOPN(AppL,cl) -> @@ -569,7 +569,7 @@ and clenv_resrec metas evars clenv = | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) -> clenv_resrec metas evars (clenv_wtactic (mimick_evar cl.(0) - ((Array.length cl) - 1) evsp) + ((Array.length cl) - 1) evn) clenv) | _ -> error "w_Unify") | _ -> error "w_Unify")) @@ -857,10 +857,10 @@ let clenv_pose_dependent_evars clenv = List.fold_left (fun clenv mv -> let evar = new_evar_in_sign (w_env clenv.hook) in - let (evar_sp,_) = destConst evar in + let (evar_n,_) = destEvar evar in let tY = clenv_instance_type clenv mv in let tYty = w_type_of clenv.hook tY in - let clenv' = clenv_wtactic (w_Declare evar_sp (DOP2(Cast,tY,tYty))) + let clenv' = clenv_wtactic (w_Declare evar_n (DOP2(Cast,tY,tYty))) clenv in clenv_assign mv evar clenv') clenv @@ -909,13 +909,13 @@ and clenv_resrec metas evars clenv = | ((lhs,(DOP0(Meta k) as rhs))::t,metas) -> clenv_resrec ((k,lhs)::metas) t clenv - | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) -> + | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) -> if w_defined_const clenv.hook evar then let (metas',evars') = unify_0 [] clenv.hook rhs evar in clenv_resrec (metas'@metas) (evars'@t) clenv else (try - clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv) + clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv) with UserError _ -> (match rhs with | DOPN(AppL,cl) -> @@ -923,7 +923,7 @@ and clenv_resrec metas evars clenv = | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) -> clenv_resrec metas evars (clenv_wtactic (mimick_evar cl.(0) - ((Array.length cl) - 1) evsp) + ((Array.length cl) - 1) evn) clenv) | _ -> error "w_Unify") | _ -> error "w_Unify")) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index e63648576..e43d51966 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -61,7 +61,7 @@ let restore_decl sp evd evc = let newgoal = { evar_env = evd.evar_env; evar_concl = evd.evar_concl; evar_body = evd.evar_body; - evar_info = newctxt } in + evar_info = Some newctxt } in (rc_add evc (sp,newgoal)) @@ -114,6 +114,7 @@ let w_Focus sp wc = ids_mod (extract_decl sp) wc let w_Underlying wc = (ts_it (ids_it wc)).decls let w_type_of wc c = ctxt_type_of (ids_it wc) c let w_env wc = get_env (ids_it wc) +let w_hyps wc = var_context (get_env (ids_it wc)) let w_ORELSE wt1 wt2 wc = try wt1 wc with UserError _ -> wt2 wc let w_Declare sp c (wc:walking_constraints) = @@ -153,7 +154,7 @@ let w_Define sp c wc = let access = evars_of (ids_it wc) c in let spdecl' = { evar_env = spdecl.evar_env; evar_concl = spdecl.evar_concl; - evar_info = mt_ctxt access; + evar_info = Some (mt_ctxt access); evar_body = Evar_defined c } in (ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 47bba83fa..620c9c4b8 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -38,6 +38,7 @@ val w_Define : evar -> constr -> w_tactic val w_Underlying : walking_constraints -> evar_declarations val w_env : walking_constraints -> env +val w_hyps : walking_constraints -> var_context val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * typed_type) -> walking_constraints -> walking_constraints diff --git a/proofs/logic.ml b/proofs/logic.ml index db3a6ca18..8a0432282 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,7 +40,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | DOP0(Meta mv) -> if occur_meta conclty then error "Cannot refine to conclusions with meta-variables"; - let ctxt = goal.evar_info in + let ctxt = out_some goal.evar_info in (mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty | DOP2(Cast,t,ty) -> @@ -80,7 +80,7 @@ and mk_hdgoals sigma goal goalacc trm = match trm with | DOP2(Cast,DOP0(Meta mv),ty) -> let _ = type_of env sigma ty in - let ctxt = goal.evar_info in + let ctxt = out_some goal.evar_info in (mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty | DOPN(AppL,cl) -> @@ -217,7 +217,7 @@ let prim_refiner r sigma goal = let env = goal.evar_env in let sign = var_context env in let cl = goal.evar_concl in - let info = goal.evar_info in + let info = out_some goal.evar_info in match r with | { name = Intro; newids = [id] } -> if mem_sign sign id then error "New variable is already declared"; diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 663aedb44..8bdecdf8f 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -96,23 +96,24 @@ let lc_toList lc = Intset.elements lc (* Functions on goals *) let mk_goal ctxt env cl = - { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt } + { evar_env = env; evar_concl = cl; + evar_body = Evar_empty; evar_info = Some ctxt } (* Functions on the information associated with existential variables *) let mt_ctxt lc = { pgm = None; mimick = None; lc = lc } -let get_ctxt gl = gl.evar_info +let get_ctxt gl = out_some gl.evar_info -let get_pgm gl = gl.evar_info.pgm +let get_pgm gl = (out_some gl.evar_info).pgm let set_pgm pgm ctxt = { ctxt with pgm = pgm } -let get_mimick gl = gl.evar_info.mimick +let get_mimick gl = (out_some gl.evar_info).mimick let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc } -let get_lc gl = gl.evar_info.lc +let get_lc gl = (out_some gl.evar_info).lc (* Functions on proof trees *) @@ -225,6 +226,12 @@ let ctxt_access sigma sp = lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus +let pf_lookup_name_as_renamed hyps ccl s = + Termast.lookup_name_as_renamed (gLOB hyps) ccl s + +let pf_lookup_index_as_renamed ccl n = + Termast.lookup_index_as_renamed ccl n + (*********************************************************************) (* Pretty printing functions *) (*********************************************************************) @@ -299,7 +306,13 @@ let pr_pgm ctxt = match ctxt.pgm with let pr_ctxt ctxt = let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >] -let pr_seq {evar_env=env; evar_concl=cl; evar_info=info} = +let pr_seq evd = + let env = evd.evar_env + and cl = evd.evar_concl + and info = match evd.evar_info with + | Some i -> i + | None -> anomaly "pr_seq : info = None" + in let (x,y) as hyps = var_context env in let sign = List.rev(List.combine x y) in let pc = pr_ctxt info in diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 6e0f179b0..5e268c320 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -144,6 +144,10 @@ val get_gc : readable_constraints -> global_constraints val remap : readable_constraints -> int * goal -> readable_constraints val ctxt_access : readable_constraints -> int -> bool +val pf_lookup_name_as_renamed : + var_context -> constr -> identifier -> int option +val pf_lookup_index_as_renamed : constr -> int -> int option + (*s Pretty printing functions. *) @@ -156,15 +160,15 @@ val pr_subgoals : goal list -> std_ppcmds val pr_subgoal : int -> goal list -> std_ppcmds val pr_decl : goal -> std_ppcmds -val pr_decls : global_constraints ->std_ppcmds +val pr_decls : global_constraints -> std_ppcmds val pr_evc : readable_constraints -> std_ppcmds val prgl : goal -> std_ppcmds val pr_seq : goal -> std_ppcmds val pr_focus : local_constraints -> std_ppcmds val pr_ctxt : ctxtty -> std_ppcmds -val pr_evars : (int * goal) list -> std_ppcmds -val pr_evars_int : int -> (int * goal) list -> std_ppcmds +val pr_evars : (int * goal) list -> std_ppcmds +val pr_evars_int : int -> (int * goal) list -> std_ppcmds val pr_subgoals_existential : evar_declarations -> goal list -> std_ppcmds val ast_of_cvt_arg : tactic_arg -> Coqast.t diff --git a/proofs/refiner.ml b/proofs/refiner.ml index dac2d6a61..aeccbc094 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -177,7 +177,7 @@ let refiner = function | (Local_constraints lc) as r -> (fun goal_sigma -> let gl = goal_sigma.it in - let ctxt = gl.evar_info in + let ctxt = out_some gl.evar_info in let sg = mk_goal ctxt gl.evar_env gl.evar_concl in ({it=[sg];sigma=goal_sigma.sigma}, (fun pfl -> @@ -346,6 +346,12 @@ let tclTHEN (tac1:tactic) (tac2:tactic) (gls:goal sigma) = (repackage sigr (List.flatten gll), compose p (mapshape(List.map List.length gll)pl)) +(* tclTHENLIST [t1;..;tn] applies t1;..tn. More convenient than tclTHEN + when n is large. *) +let rec tclTHENLIST = function + | [] -> tclIDTAC + | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) + (* tclTHEN_i tac1 tac2 n gls applies the tactic tac1 to gls and applies tac2 (i+n-1) to the i_th resulting subgoal *) @@ -928,3 +934,15 @@ let print_subscript sigma sign pf = else format_print_info_script sigma sign pf +let tclINFO (tac:tactic) gls = + let (sgl,v) as res = tac gls in + begin try + let pf = v (List.map leaf (sig_it sgl)) in + let sign = var_context (sig_it gls).evar_env in + mSGNL(hOV 0 [< 'sTR" == "; + print_subscript + ((compose ts_it sig_sig) gls) sign pf >]) + with UserError _ -> + mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >]) + end; + res diff --git a/proofs/refiner.mli b/proofs/refiner.mli index fa80f4329..4d1edc7e5 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -55,6 +55,7 @@ val extract_open_proof : val tclIDTAC : tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic +val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic val tclTHENL : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic @@ -71,6 +72,7 @@ val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic +val tclINFO : tactic -> tactic (*s Tactics handling a list of goals. *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b70320b81..49315aba7 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -40,6 +40,7 @@ let sig_it = Refiner.sig_it let sig_sig = Refiner.sig_sig let project = compose ts_it sig_sig let pf_env gls = (sig_it gls).evar_env +let pf_hyps gls = var_context (sig_it gls).evar_env let pf_concl gls = (sig_it gls).evar_concl @@ -71,11 +72,18 @@ let pf_check_type gls c1 c2 = let pf_constr_of_com gls c = let evc = project gls in - Astterm.constr_of_com evc (sig_it gls).hyps c + Astterm.constr_of_com evc (sig_it gls).evar_env c let pf_constr_of_com_sort gls c = let evc = project gls in - Astterm.constr_of_com_sort evc (sig_it gls).hyps c + Astterm.constr_of_com_sort evc (sig_it gls).evar_env c + +let pf_global gls id = Declare.global (sig_it gls).evar_env id +let pf_parse_const gls = compose (pf_global gls) id_of_string + +let pf_execute gls = + let evc = project gls in + Typing.unsafe_machine (sig_it gls).evar_env evc let pf_reduction_of_redexp gls re c = reduction_of_redexp re (pf_env gls) (project gls) c @@ -91,8 +99,8 @@ let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) -let pf_conv_x = pf_reduce conv -let pf_conv_x_leq = pf_reduce conv_leq +let pf_conv_x = pf_reduce is_conv +let pf_conv_x_leq = pf_reduce is_conv_leq let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_one_step_reduce = pf_reduce one_step_reduce let pf_reduce_to_mind = pf_reduce reduce_to_mind @@ -163,6 +171,7 @@ let w_Declare_At = w_Declare_At let w_Define = w_Define let w_Underlying = w_Underlying let w_env = w_env +let w_hyps = w_hyps let w_type_of = w_type_of let w_IDTAC = w_IDTAC let w_ORELSE = w_ORELSE @@ -171,7 +180,7 @@ let ctxt_type_of = ctxt_type_of let w_defined_const wc k = defined_constant (w_env wc) k let w_const_value wc = constant_value (w_env wc) -let w_conv_x wc m n = conv (w_env wc) (w_Underlying wc) m n +let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c @@ -182,23 +191,25 @@ let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c let tclIDTAC = tclIDTAC let tclORELSE = tclORELSE -let tclTHEN = tclTHEN -let tclTHEN_i = tclTHEN_i -let tclTHENL = tclTHENL -let tclTHENS = tclTHENS -let tclTHENSI = tclTHENSI -let tclREPEAT = tclREPEAT -let tclFIRST = tclFIRST -let tclSOLVE = tclSOLVE -let tclTRY = tclTRY -let tclTHENTRY = tclTHENTRY -let tclCOMPLETE = tclCOMPLETE -let tclAT_LEAST_ONCE = tclAT_LEAST_ONCE -let tclFAIL = tclFAIL -let tclDO = tclDO -let tclPROGRESS = tclPROGRESS +let tclTHEN = tclTHEN +let tclTHENLIST = tclTHENLIST +let tclTHEN_i = tclTHEN_i +let tclTHENL = tclTHENL +let tclTHENS = tclTHENS +let tclTHENSI = tclTHENSI +let tclREPEAT = tclREPEAT +let tclFIRST = tclFIRST +let tclSOLVE = tclSOLVE +let tclTRY = tclTRY +let tclTHENTRY = tclTHENTRY +let tclCOMPLETE = tclCOMPLETE +let tclAT_LEAST_ONCE = tclAT_LEAST_ONCE +let tclFAIL = tclFAIL +let tclDO = tclDO +let tclPROGRESS = tclPROGRESS let tclWEAK_PROGRESS = tclWEAK_PROGRESS let tclNOTSAMEGOAL = tclNOTSAMEGOAL +let tclINFO = tclINFO let unTAC = unTAC @@ -266,6 +277,35 @@ let add_tactic = Refiner.add_tactic let overwriting_tactic = Refiner.overwriting_add_tactic +(* Some combinators for parsing tactic arguments. + They transform the Coqast.t arguments of the tactic into + constr arguments *) + +type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic) + +let tactic_com tac t x = tac (pf_constr_of_com x t) x + +let tactic_com_sort tac t x = tac (pf_constr_of_com_sort x t) x + +let tactic_com_list tac tl x = + let translate = pf_constr_of_com x in + tac (List.map translate tl) x + +let tactic_bind_list tac tl x = + let translate = pf_constr_of_com x in + tac (List.map (fun (b,c)->(b,translate c)) tl) x + +let tactic_com_bind_list tac (c,tl) x = + let translate = pf_constr_of_com x in + tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x + +let tactic_com_bind_list_list tac args gl = + let translate (c,tl) = + (pf_constr_of_com gl c, + List.map (fun (b,c')->(b,pf_constr_of_com gl c')) tl) in + tac (List.map translate args) gl + + (********************************************************) (* Functions for hiding the implementation of a tactic. *) (********************************************************) @@ -279,7 +319,6 @@ let overwrite_hidden_tactic s tac = overwriting_add_tactic s tac; (fun args -> vernac_tactic(s,args)) -(*** let tactic_com = fun tac t x -> tac (pf_constr_of_com x t) x @@ -427,7 +466,6 @@ let hide_cbindll_tactic s tac = in add_tactic s tacfun; fun l -> vernac_tactic(s,putconstrbinds l) -***) (* Pretty-printers *) @@ -437,8 +475,8 @@ open Printer let pr_com sigma goal com = prterm (rename_bound_var - (ids_of_sign goal.hyps) - (Trad.constr_of_com sigma goal.hyps com)) + (ids_of_sign (var_context goal.evar_env)) + (Astterm.constr_of_com sigma goal.evar_env com)) let pr_one_binding sigma goal = function | (Dep id,com) -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >] diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index fd4388876..4593e92b7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -30,7 +30,7 @@ val apply_sig_tac : val pf_concl : goal sigma -> constr val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> typed_type signature +val pf_hyps : goal sigma -> var_context val pf_untyped_hyps : goal sigma -> constr signature val pf_nth_hyp : goal sigma -> int -> identifier * constr val pf_ctxt : goal sigma -> ctxtty @@ -38,7 +38,7 @@ val pf_global : goal sigma -> identifier -> constr val pf_parse_const : goal sigma -> string -> constr val pf_type_of : goal sigma -> constr -> constr val pf_check_type : goal sigma -> constr -> constr -> constr -val pf_fexecute : goal sigma -> constr -> unsafe_judgment +val pf_execute : goal sigma -> constr -> unsafe_judgment val hnf_type_of : goal sigma -> constr -> constr val pf_constr_of_com : goal sigma -> Coqast.t -> constr @@ -48,10 +48,15 @@ val pf_get_hyp : goal sigma -> identifier -> constr val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr -val pf_reduce : 'a reduction_function -> goal sigma -> constr -> constr + + +val pf_reduce : + (env -> evar_declarations -> constr -> constr) -> + goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr -val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function +val pf_whd_betadeltaiota_stack : + goal sigma -> constr -> constr list -> constr * constr list val pf_hnf_constr : goal sigma -> constr -> constr val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr @@ -107,6 +112,7 @@ val change_constraints_pftreestate : val tclIDTAC : tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic +val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic val tclTHENL : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic @@ -172,14 +178,14 @@ val startWalk : val walking_THEN : 'a result_w_tactic -> ('a -> tactic) -> tactic val walking : w_tactic -> tactic -val w_Focusing_THEN : section_path -> 'a result_w_tactic +val w_Focusing_THEN : int -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic -val w_Declare : section_path -> constr -> w_tactic -val w_Declare_At : section_path -> section_path -> constr -> w_tactic -val w_Define : section_path -> constr -> w_tactic +val w_Declare : int -> constr -> w_tactic +val w_Declare_At : int -> int -> constr -> w_tactic +val w_Define : int -> constr -> w_tactic val w_Underlying : walking_constraints -> evar_declarations val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> context +val w_hyps : walking_constraints -> var_context val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * typed_type) -> walking_constraints -> walking_constraints @@ -199,6 +205,26 @@ val add_tactic : string -> (tactic_arg list -> tactic) -> unit val overwriting_tactic : string -> (tactic_arg list -> tactic) -> unit +(*s Transformation of tactic arguments. *) + +type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic) + +val tactic_com : (constr,Coqast.t) parse_combinator +val tactic_com_sort : (constr,Coqast.t) parse_combinator +val tactic_com_list : (constr list, Coqast.t list) parse_combinator + +val tactic_bind_list : ((bindOcc * constr) list, + (bindOcc * Coqast.t) list) parse_combinator + +val tactic_com_bind_list : + (constr * (bindOcc * constr) list, + Coqast.t * (bindOcc * Coqast.t) list) parse_combinator + +val tactic_com_bind_list_list : + ((constr * (bindOcc * constr) list) list, + (Coqast.t * (bindOcc * Coqast.t) list) list) parse_combinator + + (*s Hiding the implementation of tactics. *) val hide_tactic : diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8bf647a69..18902c7b3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3,6 +3,7 @@ open Pp open Util +open Stamps open Names open Sign open Generic @@ -97,7 +98,6 @@ let fix_noname n = let id = id_of_string (List.hd l) in fix id n -(***TODO: les versions dyn_ let dyn_mutual_fix argsl gl = match argsl with | [Integer n] -> fix_noname n gl @@ -112,7 +112,6 @@ let dyn_mutual_fix argsl gl = let (lid,ln,lar) = decomp [] [] [] lfix in mutual_fix (id::lid) (n::ln) (List.map (pf_constr_of_com gl) lar) gl | l -> bad_tactic_args "mutual_fix" l -***) let mutual_cofix = Tacmach.mutual_cofix let cofix f = mutual_cofix [f] [] @@ -122,7 +121,6 @@ let cofix_noname n = let id = id_of_string (List.hd l) in cofix id n -(***TODO let dyn_mutual_cofix argsl gl = match argsl with | [] -> cofix_noname gl @@ -137,12 +135,14 @@ let dyn_mutual_cofix argsl gl = let (lid,lar) = decomp [] [] lcofix in mutual_cofix (id::lid) (List.map (pf_constr_of_com gl) lar) gl | l -> bad_tactic_args "mutual_cofix" l -***) + (**************************************************************) (* Reduction and conversion tactics *) (**************************************************************) +type 'a tactic_reduction = env -> evar_declarations -> constr -> constr + (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a certain hypothesis *) @@ -174,13 +174,13 @@ let redin_combinator redfun = function (* Now we introduce different instances of the previous tacticals *) let change_hyp_and_check t env sigma c = - if is_conv (Global.unsafe_env()) sigma t c then + if is_conv (Global.env()) sigma t c then t else errorlabstrm "convert-check-hyp" [< 'sTR "Not convertible" >] let change_concl_and_check t env sigma c = - if is_conv_leq (Global.unsafe_env()) sigma t c then + if is_conv_leq (Global.env()) sigma t c then t else errorlabstrm "convert-check-concl" [< 'sTR "Not convertible" >] @@ -210,14 +210,12 @@ let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) let unfold_option loccname = reduct_option (unfoldn loccname) let pattern_option l = reduct_option (pattern_occs l) -(*** let dyn_change = function | [Command (com); Clause cl] -> (fun goal -> - let c = constr_of_com_sort (project goal) (pf_hyps goal) com in + let c = Astterm.constr_of_com_sort (project goal) (pf_env goal) com in in_combinator (change_in_concl c) (change_in_hyp c) cl goal) | l -> bad_tactic_args "change" l -***) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) @@ -225,15 +223,13 @@ let dyn_change = function let reduce redexp cl goal = redin_combinator (reduction_of_redexp redexp) cl goal -(*** let dyn_reduce = function | [Redexp (redn,args); Clause cl] -> (fun goal -> let redexp = - redexp_of_ast (project goal) (pf_hyps goal) (redn,args) in + Astterm.redexp_of_ast (project goal) (pf_env goal) (redn,args) in reduce redexp cl goal) | l -> bad_tactic_args "reduce" l -***) (* Unfolding occurrences of a constant *) @@ -438,7 +434,7 @@ let rec intros_rmove = function let apply_type hdcty argl gl = refine (DOPN(AppL,Array.of_list - ((DOP2(Cast,DOP0(Meta(newMETA())),hdcty))::argl))) gl + ((DOP2(Cast,DOP0(Meta(new_meta())),hdcty))::argl))) gl let apply_term hdc argl gl = refine (DOPN(AppL,Array.of_list(hdc::argl))) gl @@ -505,9 +501,9 @@ let refinew_scheme kONT clause gl = res_pf kONT clause gl let dyn_apply l = match l with - | [Command com; BINDINGS binds] -> + | [Command com; Bindings binds] -> tactic_com_bind_list apply_with_bindings (com,binds) - | [CONSTR c; CBINDINGS binds] -> + | [Constr c; Cbindings binds] -> apply_with_bindings (c,binds) | l -> bad_tactic_args "apply" l @@ -520,8 +516,8 @@ let cut_and_apply c gl = | DOP2(Prod,c1,DLAM(_,c2)) when not (dependent (Rel 1) c2) -> tclTHENS (apply_type (DOP2(Prod,c2,DLAM(Anonymous,goal_constr))) - [DOP0(Meta(newMETA()))]) - [tclIDTAC;apply_term c [DOP0(Meta(newMETA()))]] gl + [DOP0(Meta(new_meta()))]) + [tclIDTAC;apply_term c [DOP0(Meta(new_meta()))]] gl | _ -> error "Imp_elim needs a non-dependent product" let dyn_cut_and_apply = function @@ -537,7 +533,7 @@ let cut c gl = match hnf_type_of gl c with | (DOP0(Sort _)) -> apply_type (DOP2(Prod,c,DLAM(Anonymous,(pf_concl gl)))) - [DOP0(Meta (newMETA()))] gl + [DOP0(Meta (new_meta()))] gl | _ -> error "Not a proposition or a type" let dyn_cut = function @@ -577,11 +573,11 @@ let generalize_goal gl c cl = la premiere lettre du type, meme si "ci" est une constante et qu'on pourrait prendre directement son nom *) else - prod_name (Anonymous, t, cl') + prod_name (Global.env()) (Anonymous, t, cl') let generalize_dep c gl = let sign = pf_untyped_hyps gl in - let init_ids = ids_of_sign (initial_sign ()) in + let init_ids = ids_of_sign (Global.var_context()) in let rec seek ((hl,tl) as toquant) h t = if List.exists (fun id -> occur_var id t) hl or dependent c t then (h::hl,t::tl) @@ -589,7 +585,7 @@ let generalize_dep c gl = toquant in let (hl,tl) = it_sign seek ([],[]) sign in - let tothin = filter (fun id -> not (List.mem id init_ids)) hl in + let tothin = List.filter (fun id -> not (List.mem id init_ids)) hl in let tothin' = match c with | VAR id when mem_sign sign id & not (List.mem id init_ids) -> id::tothin @@ -639,7 +635,7 @@ let letin_abstract id c occ_ccl occhypl gl = try let occ = if allhyp then [] else List.assoc hyp occl in let newtyp = subst1 (VAR id) (subst_term_occ occ c typ) in - let newoccl = except_assoc hyp occl in + let newoccl = list_except_assoc hyp occl in if typ=newtyp then (accu,Some hyp) else @@ -662,7 +658,7 @@ let letin_abstract id c occ_ccl occhypl gl = (dephyps,deptyps,marks,ccl) let letin_tac with_eq name c occ_ccl occhypl gl = - let x = id_of_name_using_hdchar (pf_type_of gl c) name in + let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in let hyps = pf_untyped_hyps gl in let id = next_global_ident_away x (ids_of_sign hyps) in if mem_sign hyps id then error "New variable is already declared"; @@ -727,7 +723,7 @@ let dyn_exact cc gl = match cc with | [Command com] -> let evc = (project gl) in let concl = (pf_concl gl) in - let c = constr_of_com_casted evc (pf_hyps gl) com concl in + let c = Astterm.constr_of_com_casted evc (pf_env gl) com concl in refine c gl | l -> bad_tactic_args "exact" l @@ -795,7 +791,7 @@ let new_hyp mopt c blist g = let cut_pf = applist(thd, match mopt with - | Some m -> if m < nargs then firstn m tstack else tstack + | Some m -> if m < nargs then list_firstn m tstack else tstack | None -> tstack) in (tclTHENL (tclTHEN (kONT clause.hook) @@ -836,9 +832,9 @@ let dyn_move_dep = function let constructor_checking_bound boundopt i lbind gl = let cl = pf_concl gl in - let (mind,_,redcl) = reduce_to_mind (project gl) cl in + let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in let (x_0,x_1,args) = destMutInd mind in - let nconstr = mis_nconstr (mind_specif_of_mind mind) + let nconstr = mis_nconstr (Global.lookup_mind_specif mind) and sigma = project gl in if i=0 then error "The constructors are numbered starting from 1"; if i > nconstr then error "Not enough constructors"; @@ -856,9 +852,9 @@ let one_constructor i = (constructor_checking_bound None i) let any_constructor gl = let cl = pf_concl gl in - let (mind,_,redcl) = reduce_to_mind (project gl) cl in + let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in let (x_0,x_1,args) = destMutInd mind in - let nconstr = mis_nconstr (mind_specif_of_mind mind) + let nconstr = mis_nconstr (Global.lookup_mind_specif mind) and sigma = project gl in if nconstr = 0 then error "The type has no constructors"; tclFIRST (List.map (fun i -> one_constructor i []) @@ -950,7 +946,8 @@ let type_clenv_binding wc (c,t) lbind = let general_elim (c,lbindc) (elimc,lbindelimc) gl = let (wc,kONT) = startWalk gl in - let (_,_,t) = reduce_to_ind (project gl) (pf_type_of gl c) in + let (_,_,t) = reduce_to_ind (pf_env gl) (project gl) + (pf_type_of gl c) in let indclause = make_clenv_binding wc (c,t) lbindc in let elimt = w_type_of wc elimc in let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in @@ -960,7 +957,8 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl = * constant associated with the type. *) let default_elim (c,lbindc) gl = - let (path_name,_,t) = reduce_to_ind (project gl) (pf_type_of gl c) in + let (path_name,_,t) = reduce_to_ind (pf_env gl) (project gl) + (pf_type_of gl c) in let elimc = lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl)) in @@ -1006,7 +1004,8 @@ let simplest_elim c = default_elim (c,[]) let rec is_rec_arg indpath t = try - mind_path (fst (find_mrectype empty_evd t)) = indpath + Declare.mind_path (fst (find_mrectype (Global.env()) Evd.empty t)) + = indpath with Induc -> false @@ -1014,7 +1013,7 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) = let (lstatus,rstatus) = statuslists in let tophyp = ref None in let (l,_) = decompose_prod t in - let n = List.length (filter (fun (_,t') -> is_rec_arg indpath t') l) in + let n = List.length (List.filter (fun (_,t') -> is_rec_arg indpath t') l) in let recvarname = if n=1 then cname @@ -1060,10 +1059,10 @@ let atomize_param_of_ind hyp0 gl = error ("No such hypothesis : " ^ (string_of_id hyp0)) in let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in - let mis = mind_specif_of_mind mind in + let mis = Global.lookup_mind_specif mind in let nparams = mis_nparams mis in let argl = snd (decomp_app indtyp) in - let params = firstn nparams argl in + let params = list_firstn nparams argl in (* le gl est important pour ne pas préévaluer *) let rec atomize_one i avoid gl = if i<>nparams then @@ -1078,7 +1077,8 @@ let atomize_param_of_ind hyp0 gl = (letin_tac true (Name x) (VAR id) (Some []) []) (atomize_one (i-1) ((VAR x)::avoid)) gl | c -> - let id = id_of_name_using_hdchar (pf_type_of gl c) Anonymous in + let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) + Anonymous in let x = fresh_id [] id gl in tclTHEN (letin_tac true (Name x) c (Some []) []) @@ -1089,19 +1089,19 @@ let atomize_param_of_ind hyp0 gl = atomize_one (List.length argl) params gl let find_atomic_param_of_ind mind indtyp = - let mis = mind_specif_of_mind mind in + let mis = Global.lookup_mind_specif mind in let nparams = mis_nparams mis in let argl = snd (decomp_app indtyp) in let argv = Array.of_list argl in - let params = firstn nparams argl in - let indvars = ref [] in + let params = list_firstn nparams argl in + let indvars = ref Idset.empty in for i = nparams to (Array.length argv)-1 do match argv.(i) with | VAR id when not (List.exists (occur_var id) params) -> - indvars := add_set id !indvars + indvars := Idset.add id !indvars | _ -> () done; - !indvars + Idset.elements !indvars (* [cook_sign] builds the lists [indhyps] of hyps that must be erased, the lists of hyps to be generalize [(hdeps,tdeps)] on the @@ -1249,24 +1249,25 @@ let get_constructors varname (elimc,elimt) mind mindpath = (* Je suppose que w_type_of=type_of pour les constantes comme elimc *) (* J'espere que je ne me trompe pas *) let (hyps_of_elimt,_) = decompose_prod elimt in - let mis = mind_specif_of_mind mind in + let mis = Global.lookup_mind_specif mind in let nconstr = mis_nconstr mis in let nparam = mis_nparams mis in try - List.rev (firstn nconstr (lastn (nconstr + nparam + 1) hyps_of_elimt)) + List.rev (list_firstn nconstr + (list_lastn (nconstr + nparam + 1) hyps_of_elimt)) with Failure _ -> anomaly "induct_elim: bad elimination predicate" let induction_from_context hyp0 gl = (*test suivant sans doute inutile car protégé par le letin_tac avant appel*) - if List.mem hyp0 (ids_of_sign (initial_sign ())) then + if List.mem hyp0 (ids_of_sign (Global.var_context())) then errorlabstrm "induction" [< 'sTR "Cannot generalize a global variable" >]; let sign = pf_untyped_hyps gl in let tsign = pf_hyps gl in let tmptyp0 = pf_get_hyp gl hyp0 in let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in let indvars = find_atomic_param_of_ind mind indtyp in - let mindpath = mind_path mind in + let mindpath = Declare.mind_path mind in let elimc = lookup_eliminator tsign mindpath (suff gl (pf_concl gl)) in let elimt = pf_type_of gl elimc in let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars sign in @@ -1290,12 +1291,13 @@ let induction_with_atomization_of_ind_arg hyp0 = let new_induct c gl = match c with - | (VAR id) when not (List.mem id (ids_of_sign (initial_sign ()))) -> + | (VAR id) when not (List.mem id (ids_of_sign (Global.var_context()))) -> tclORELSE (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim)) (induction_with_atomization_of_ind_arg id) gl | _ -> - let x = id_of_name_using_hdchar (pf_type_of gl c) Anonymous in + let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) + Anonymous in let id = fresh_id [] x gl in tclTHEN (letin_tac true (Name id) c (Some []) []) @@ -1344,18 +1346,19 @@ let dyn_induct = function (* Case analysis tactics *) let general_case_analysis (c,lbindc) gl = - let (mind,_,_) = reduce_to_mind (project gl) (pf_type_of gl c) in + let env = pf_env gl in + let (mind,_,_) = reduce_to_mind env (project gl) (pf_type_of gl c) in let sigma = project gl in let sort = sort_of_goal gl in - let elim = Indrec.make_case_gen sigma mind sort in + let elim = Indrec.make_case_gen env sigma mind sort in general_elim (c,lbindc) (elim,[]) gl let simplest_case c = general_case_analysis (c,[]) let dyn_case =function - | [(CONSTR mp);(CBINDINGS mpbinds)] -> + | [Constr mp; Cbindings mpbinds] -> general_case_analysis (mp,mpbinds) - | [(COMMAND mp);(BINDINGS mpbinds)] -> + | [Command mp; Bindings mpbinds] -> tactic_com_bind_list general_case_analysis (mp,mpbinds) | l -> bad_tactic_args "case" l @@ -1366,8 +1369,8 @@ let destruct s = (tclTHEN (intros_until s) (tclLAST_HYP simplest_case)) let destruct_nodep n = (tclTHEN (intros_do n) (tclLAST_HYP simplest_case)) let dyn_destruct = function - | [(IDENTIFIER x)] -> destruct x - | [(INTEGER n)] -> destruct_nodep n + | [Identifier x] -> destruct x + | [Integer n] -> destruct_nodep n | l -> bad_tactic_args "destruct" l (* @@ -1387,7 +1390,7 @@ let elim_scheme_type elim t gl = | _ -> anomaly "elim_scheme_type" let elim_type t gl = - let (path_name,tind,t) = reduce_to_ind (project gl) t in + let (path_name,tind,t) = reduce_to_ind (pf_env gl) (project gl) t in let elimc = lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl)) in @@ -1396,24 +1399,25 @@ let elim_type t gl = | _ -> elim_scheme_type elimc tind gl let dyn_elim_type = function - | [(CONSTR c)] -> elim_type c - | [(COMMAND com)] -> tactic_com_sort elim_type com - | l -> bad_tactic_args "elim_type" l + | [Constr c] -> elim_type c + | [Command com] -> tactic_com_sort elim_type com + | l -> bad_tactic_args "elim_type" l let case_type t gl = - let (mind,_,t) = reduce_to_mind (project gl) t in + let env = pf_env gl in + let (mind,_,t) = reduce_to_mind env (project gl) t in match t with | DOP2(Prod,_,_) -> error "Not an inductive definition" | _ -> let sigma = project gl in let sort = sort_of_goal gl in - let elimc = Indrec.make_case_gen sigma mind sort in + let elimc = Indrec.make_case_gen env sigma mind sort in elim_scheme_type elimc t gl let dyn_case_type = function - | [CONSTR c] -> case_type c - | [COMMAND com] -> tactic_com case_type com - |l -> bad_tactic_args "case_type" l + | [Constr c] -> case_type c + | [Command com] -> tactic_com case_type com + | l -> bad_tactic_args "case_type" l (* Some eliminations frequently used *) @@ -1461,7 +1465,7 @@ let impE id gl = if is_imp_term (pf_hnf_constr gl t) then let (dom, _, rng) = destProd (pf_hnf_constr gl t) in (tclTHENS (cut_intro rng) - [tclIDTAC;apply_term (VAR id) [DOP0(Meta(newMETA()))]]) gl + [tclIDTAC;apply_term (VAR id) [DOP0(Meta(new_meta()))]]) gl else errorlabstrm "impE" [< 'sTR("Tactic impE expects "^(string_of_id id)^ @@ -1500,7 +1504,7 @@ let instantiate_pf_com n com pfts = with Failure _ -> error "not so many uninstantiated existential variables" in - let c = constr_of_com sigma evd.hyps com in + let c = Astterm.constr_of_com sigma evd.evar_env com in let wc' = w_Define sp c wc in let newgc = ts_mk (w_Underlying wc') in change_constraints_pftreestate newgc pfts @@ -1520,7 +1524,7 @@ let contradiction_on_hyp id gl = (* Absurd *) let absurd c gls = - let falseterm = pf_constr_of_com_sort gls (nvar "False") in + let falseterm = pf_constr_of_com_sort gls (Ast.nvar "False") in (tclTHENS (tclTHEN (elim_type falseterm) (cut c)) ([(tclTHENS @@ -1534,12 +1538,12 @@ let absurd c gls = tclIDTAC])) gls let dyn_absurd = function - | [(CONSTR c)] -> absurd c - | [(COMMAND com)] -> tactic_com_sort absurd com - | l -> bad_tactic_args "absurd" l + | [Constr c] -> absurd c + | [Command com] -> tactic_com_sort absurd com + | l -> bad_tactic_args "absurd" l let contradiction gls = - let falseterm = pf_constr_of_com_sort gls (nvar "False") in + let falseterm = pf_constr_of_com_sort gls (Ast.nvar "False") in tclTHENLIST [ intros; elim_type falseterm; assumption ] gls let dyn_contradiction = function @@ -1637,18 +1641,19 @@ let transitivity t gl = let intros_transitivity n = tclTHEN intros (transitivity n) let dyn_transitivity = function - | [(CONSTR n)] -> intros_transitivity n - | [(COMMAND n)] -> tactic_com intros_transitivity n - | l -> bad_tactic_args "transitivity" l + | [Constr n] -> intros_transitivity n + | [Command n] -> tactic_com intros_transitivity n + | l -> bad_tactic_args "transitivity" l (* tactical to save as name a subproof such that the generalisation of the current goal, abstracted with respect to the local signature, is solved by tac *) let abstract_subproof name tac gls = - let current_sign = initial_sign() + let env = Global.env() in + let current_sign = Global.var_context() and global_sign = pf_untyped_hyps gls in - let sign = Names.sign_it + let sign = Sign.sign_it (fun id typ s -> if mem_sign current_sign id then s else add_sign (id,typ) s) global_sign nil_sign @@ -1656,12 +1661,13 @@ let abstract_subproof name tac gls = let na = next_global_ident_away name (ids_of_sign global_sign) in let nas = string_of_id na in - let concl = Names.it_sign (fun t id typ -> mkNamedProd id typ t) + let concl = Sign.it_sign (fun t id typ -> mkNamedProd id typ t) (pf_concl gls) sign in - let top_goal = mkGOAL (mt_ctxt Spset.empty) current_sign concl in - let ts = {top_hyps = initial_assumptions(); - top_goal = top_goal; - top_strength = Constrtypes.NeverDischarge} + let env' = change_hyps (fun _ -> current_sign) env in + let top_goal = mk_goal (mt_ctxt Intset.empty) env' concl in + let ts = { top_hyps = (Global.env(), empty_env); + top_goal = top_goal; + top_strength = Declare.NeverDischarge } in start(nas,ts);set_proof (Some nas); begin @@ -1672,7 +1678,7 @@ let abstract_subproof name tac gls = with UserError _ as e -> (abort_cur_goal(); raise e) end; - exact (applist ((Machops.global (gLOB current_sign) na), + exact (applist ((Declare.global env' na), (List.map (fun id -> VAR(id)) (List.rev (ids_of_sign sign))))) gls @@ -1687,8 +1693,8 @@ let tclABSTRACT name_op tac gls = let dyn_tclABSTRACT = hide_tactic "ABSTRACT" (function - | [TACEXP tac] -> + | [Tacexp tac] -> tclABSTRACT None (Tacinterp.interp tac) - | [IDENTIFIER s; TACEXP tac] -> + | [Identifier s; Tacexp tac] -> tclABSTRACT (Some s) (Tacinterp.interp tac) | _ -> invalid_arg "tclABSTRACT") diff --git a/tactics/tactics.mli b/tactics/tactics.mli index db60df966..1c4287169 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -4,6 +4,7 @@ (*i*) open Names open Term +open Environ open Tacmach open Proof_trees open Reduction @@ -84,9 +85,11 @@ val dyn_exact : tactic_arg list -> tactic (*s Reduction tactics. *) -val reduct_in_hyp : 'a reduction_function -> identifier -> tactic -val reduct_option : 'a reduction_function -> identifier option -> tactic -val reduct_in_concl : 'a reduction_function -> tactic +type 'a tactic_reduction = env -> evar_declarations -> constr -> constr + +val reduct_in_hyp : 'a tactic_reduction -> identifier -> tactic +val reduct_option : 'a tactic_reduction -> identifier option -> tactic +val reduct_in_concl : 'a tactic_reduction -> tactic val change_in_concl : constr -> tactic val change_in_hyp : constr -> identifier -> tactic diff --git a/toplevel/command.ml b/toplevel/command.ml index 874d9ada8..c4f4622d7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -2,6 +2,7 @@ (* $Id$ *) open Pp +open Util open Generic open Term open Constant @@ -55,37 +56,37 @@ let definition_body_red ident n com red_option = declare_constant ident (ce',n,false) let syntax_definition ident com = - let c = constr_of_com Evd.empty (Global.env()) com in - declare_syntax_constant ident c + let c = raw_constr_of_com Evd.empty (Global.context()) com in + Syntax_def.declare_syntactic_definition ident c +(***TODO let abstraction_definition ident arity com = let c = raw_constr_of_compattern Evd.empty (Global.env()) com in machine_abstraction ident arity c - +***) (* 2| Variable definitions *) let parameter_def_var ident c = - let (sigma,(sign,fsign)) = initial_sigma_assumptions() in - machine_parameter (sign,fsign) - (id_of_string ident, constr_of_com1 true sigma sign c) + let c = constr_of_com1 true Evd.empty (Global.env()) c in + declare_parameter (id_of_string ident) c -let hypothesis_def_var is_refining ident n c = - let (sigma,(sign,fsign)) = initial_sigma_assumptions() in +let hypothesis_def_var is_refining ident n c = match n with | NeverDischarge -> parameter_def_var ident c | DischargeAt disch_sp -> - if is_section_p disch_sp then - (machine_variable (sign,fsign) - (id_of_string ident,n,false, - constr_of_com1 true sigma sign c); - if is_refining then - (mSGERRNL [< 'sTR"Warning: Variable " ; 'sTR ident ; - 'sTR" is not visible from current goals" >])) - else (mSGERRNL [< 'sTR"Warning: Declaring " ; 'sTR ident ; - 'sTR" as a parameter rather than a variable " ; - 'sTR" because it is at a global level" >]; - parameter_def_var ident c) + if Lib.is_section_p disch_sp then begin + declare_variable (id_of_string ident) + (constr_of_com1 true Evd.empty (Global.env()) c,n,false); + if is_refining then + mSGERRNL [< 'sTR"Warning: Variable " ; 'sTR ident ; + 'sTR" is not visible from current goals" >] + end else begin + mSGERRNL [< 'sTR"Warning: Declaring " ; 'sTR ident ; + 'sTR" as a parameter rather than a variable " ; + 'sTR" because it is at a global level" >]; + parameter_def_var ident c + end (* 3| Mutual Inductive definitions *) @@ -110,224 +111,222 @@ let corecursive_message = function let build_mutual lparams lnamearconstrs finite = let lrecnames = List.map (fun (x,_,_)->x) lnamearconstrs and nparams = List.length lparams - and (sigma,(sign0,fsign0)) = initial_sigma_assumptions() in - let x = Vartab.freeze() in - let mispecvec = - try + and sigma = Evd.empty + and env0 = Global.env() in + let fs = States.freeze() in + try + let mispecvec = let (ind_sign,arityl) = - List.fold_left - (fun (sign,arl) (recname,arityc,_) -> - let arity = - fconstruct_type sigma sign0 (mkProdCit lparams arityc) in - (Vartab.push recname false (arity,None) NeverDischarge - (if is_implicit_args() then IMPL_AUTO (poly_args_type arity) - else NO_IMPL); - (add_sign (recname,arity) sign, (arity::arl)))) - (sign0,[]) lnamearconstrs + List.fold_left + (fun (env,arl) (recname,arityc,_) -> + let arity = type_of_com env (mkProdCit lparams arityc) in + let env' = Environ.push_var (recname,arity) env in + declare_variable recname (arity.body,NeverDischarge,false); + (env', (arity::arl))) + (env0,[]) lnamearconstrs in - Array.of_list - (List.map2 - (fun ar (name,_,lname_constr) -> - let consconstrl = - List.map - (fun (_,constr) -> constr_of_com sigma ind_sign - (mkProdCit lparams constr)) - lname_constr - in - (name,Anonymous,ar, - put_DLAMSV_subst (List.rev lrecnames) - (Array.of_list consconstrl), - Array.of_list (List.map fst lname_constr))) - (List.rev arityl) lnamearconstrs) - -(* Expérimental -let (full_env,lpar) = - List.fold_left - (fun (env,lp) (n,t) -> - let tj = type_from_com_env env t in - (add_rel (n,tj) env, (n,tj)::lp)) - (gLOB ind_sign) lparams in (* On triche: les ind n'ont pas le droit de - figurer dans les par, mais on sait par le - calcul de arityl qu'ils ne figurent pas *) - - let lrecnames' = List.rev lrecnames in - (Array.of_list - (List.map2 - (fun ar (name,_,lname_constr) -> - let lc = - List.map - (fun (_,c) -> - it_list_i (fun i c id -> subst_varn id i c) - (nparams+1) - (constr_of_com_env sigma env c) - lrecnames') - lname_constr in - (name, Anonymous, ar, (lpar,lc), - Array.of_list (List.map fst lname_constr))) - (List.rev arityl) lnamearconstrs)) -*) - with e -> (Vartab.unfreeze x; raise e) - -in let _ = Vartab.unfreeze x - - in machine_minductive (sign0,fsign0) nparams mispecvec finite; + List.map2 + (fun ar (name,_,lname_constr) -> + let consconstrl = + List.map + (fun (_,constr) -> constr_of_com sigma ind_sign + (mkProdCit lparams constr)) + lname_constr + in + (name, ar.body, List.map fst lname_constr, + put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl))) + (List.rev arityl) lnamearconstrs + in + let mie = { + mind_entry_nparams = nparams; + mind_entry_finite = finite; + mind_entry_inds = mispecvec } + in + declare_mind mie; + States.unfreeze fs; pPNL(minductive_message lrecnames) + with e -> + States.unfreeze fs; raise e (* try to find non recursive definitions *) + +let list_chop_hd i l = match list_chop i l with + | (l1,x::l2) -> (l1,x,l2) + | _ -> assert false + let collect_non_rec = let rec searchrec lnonrec lnamerec ldefrec larrec nrec = try let i = - try_find_i + list_try_find_i (fun i f -> if List.for_all (fun def -> not (occur_var f def)) ldefrec then i else failwith "try_find_i") - 0 lnamerec in - - let (lf1,f::lf2) = chop_list i lnamerec - and (ldef1,def::ldef2) = chop_list i ldefrec - and (lar1,ar::lar2) = chop_list i larrec - and newlnv = (try (match chop_list i nrec with - (lnv1,_::lnv2) -> (lnv1@lnv2) - | _ -> []) - (* nrec=[] for cofixpoints *) - with Failure "chop_list" -> []) - in searchrec ((f,DOP2(Cast,def,body_of_type ar))::lnonrec) - (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv - with Failure "try_find_i" -> (lnonrec, (lnamerec,ldefrec,larrec,nrec)) - in searchrec [] - - + 0 lnamerec + in + let (lf1,f,lf2) = list_chop_hd i lnamerec in + let (ldef1,def,ldef2) = list_chop_hd i ldefrec in + let (lar1,ar,lar2) = list_chop_hd i larrec in + let newlnv = + try + match list_chop i nrec with + | (lnv1,_::lnv2) -> (lnv1@lnv2) + | _ -> [] (* nrec=[] for cofixpoints *) + with Failure "list_chop" -> [] + in + searchrec ((f,DOP2(Cast,def,body_of_type ar))::lnonrec) + (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv + with Failure "try_find_i" -> + (lnonrec, (lnamerec,ldefrec,larrec,nrec)) + in + searchrec [] let build_recursive lnameargsardef = - let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef - and (sigma,(sign0,_ as env)) = initial_sigma_assumptions() + and sigma = Evd.empty + and env0 = Global.env() and nv = Array.of_list (List.map (fun (_,la,_,_) -> (List.length la) -1) - lnameargsardef) in - - let x = Vartab.freeze() in + lnameargsardef) + in + let fs = States.freeze() in let (rec_sign,arityl) = - try (List.fold_left - (fun (sign,arl) (recname,lparams,arityc,_) -> - let arity = - fconstruct_type sigma sign0 (mkProdCit lparams arityc) in - (Vartab.push recname false (arity,None) NeverDischarge - (if is_implicit_args() then IMPL_AUTO (poly_args_type arity) - else NO_IMPL); - (add_sign (recname,arity) sign, (arity::arl)))) - (sign0,[]) lnameargsardef) - with e -> (Vartab.unfreeze x; raise e) in - + try + List.fold_left + (fun (env,arl) (recname,lparams,arityc,_) -> + let arity = type_of_com env (mkProdCit lparams arityc) in + declare_variable recname (arity.body,NeverDischarge,false); + (Environ.push_var (recname,arity) env, (arity::arl))) + (env0,[]) lnameargsardef + with e -> + States.unfreeze fs; raise e + in let recdef = - try (List.map (fun (_,lparams,arityc,def) -> - constr_of_com sigma rec_sign - (mkLambdaCit lparams (mkCastC(def,arityc)))) - lnameargsardef) - with e -> (Vartab.unfreeze x; raise e) in - - let _ = Vartab.unfreeze x in - + try + List.map (fun (_,lparams,arityc,def) -> + constr_of_com sigma rec_sign + (mkLambdaCit lparams (mkCastC(def,arityc)))) + lnameargsardef + with e -> + States.unfreeze fs; raise e + in + States.unfreeze fs; let (lnonrec,(lnamerec,ldefrec,larrec,nvrec)) = collect_non_rec lrecnames recdef (List.rev arityl) (Array.to_list nv) in let n = NeverDischarge in - if lnamerec <> [] then - (let recvec = [|put_DLAMSV_subst (List.rev lnamerec) - (Array.of_list ldefrec)|] in - let varrec = Array.of_list larrec in - let rec declare i = function - (fi::lf) -> - machine_constant env - ((fi,false,n), mkFixDlam (Array.of_list nvrec) i varrec recvec); - declare (i+1) lf - | _ -> () in - (* declare the recursive definitions *) - declare 0 lnamerec; pPNL(recursive_message lnamerec)); - (* The others are declared as normal definitions *) - let var_subst id = - (id,make_substituend (Machops.search_reference (gLOB sign0) id)) in - let _ = List.fold_left + if lnamerec <> [] then begin + let recvec = [|put_DLAMSV_subst (List.rev lnamerec) + (Array.of_list ldefrec)|] in + let varrec = Array.of_list larrec in + let rec declare i = function + | fi::lf -> + let ce = { const_entry_body = + mkFixDlam (Array.of_list nvrec) i varrec recvec; + const_entry_type = None } in + declare_constant fi (ce, n, false); + declare (i+1) lf + | _ -> () + in + (* declare the recursive definitions *) + declare 0 lnamerec; + pPNL(recursive_message lnamerec) + end; + (* The others are declared as normal definitions *) + let var_subst id = (id,make_substituend (global_reference CCI id)) in + let _ = + List.fold_left (fun subst (f,def) -> - machine_constant env ((f,false,n),Generic.replace_vars subst def); - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) - + let ce = { const_entry_body = Generic.replace_vars subst def; + const_entry_type = None } in + declare_constant f (ce,n,false); + warning ((string_of_id f)^" is non-recursively defined"); + (var_subst f) :: subst) (List.map var_subst lnamerec) - lnonrec in + lnonrec + in () - - let build_corecursive lnameardef = - let lrecnames = List.map (fun (f,_,_) -> f) lnameardef - and (sigma,(sign0,_ as env)) = initial_sigma_assumptions() in - - let x = Vartab.freeze() in + and sigma = Evd.empty + and env0 = Global.env() in + let fs = States.freeze() in let (rec_sign,arityl) = - try (List.fold_left - (fun (sign,arl) (recname,arityc,_) -> - let arity = fconstruct_type sigma sign0 arityc in - (Vartab.push recname false (arity,None) NeverDischarge - (if is_implicit_args() then IMPL_AUTO (poly_args_type arity) - else NO_IMPL); - (add_sign (recname,arity) sign, (arity::arl)))) - (sign0,[]) lnameardef) - with e -> (Vartab.unfreeze x; raise e) in - + try + List.fold_left + (fun (env,arl) (recname,arityc,_) -> + let arity = type_of_com env0 arityc in + declare_variable recname (arity.body,NeverDischarge,false); + (Environ.push_var (recname,arity) env, (arity::arl))) + (env0,[]) lnameardef + with e -> + States.unfreeze fs; raise e + in let recdef = - try (List.map (fun (_,arityc,def) -> - constr_of_com sigma rec_sign - (mkCastC(def,arityc))) - lnameardef) - with e -> (Vartab.unfreeze x; raise e) in - - let _ = Vartab.unfreeze x in - + try + List.map (fun (_,arityc,def) -> + constr_of_com sigma rec_sign + (mkCastC(def,arityc))) + lnameardef + with e -> + States.unfreeze fs; raise e + in + States.unfreeze fs; let (lnonrec,(lnamerec,ldefrec,larrec,_)) = collect_non_rec lrecnames recdef (List.rev arityl) [] in - let n = NeverDischarge in - - if lnamerec <> [] then - (let recvec = if lnamerec = [] then [||] - else - [|put_DLAMSV_subst (List.rev lnamerec) (Array.of_list ldefrec)|] in - - let rec declare i = function - (fi::lf) -> - machine_constant env - ((fi,false,n), mkCoFixDlam i (Array.of_list larrec) recvec); - declare (i+1) lf - | _ -> () in - - declare 0 lnamerec; pPNL(corecursive_message lnamerec)); + if lnamerec <> [] then begin + let recvec = + if lnamerec = [] then + [||] + else + [|put_DLAMSV_subst (List.rev lnamerec) (Array.of_list ldefrec)|] + in + let rec declare i = function + | fi::lf -> + let ce = { const_entry_body = + mkCoFixDlam i (Array.of_list larrec) recvec; + const_entry_type = None } in + declare_constant fi (ce,n,false); + declare (i+1) lf + | _ -> () + in + declare 0 lnamerec; + pPNL(corecursive_message lnamerec) + end; let var_subst id = - (id,make_substituend (Machops.search_reference (gLOB sign0) id)) in - let _ = List.fold_left + (id,make_substituend (global_reference CCI id)) in + let _ = + List.fold_left (fun subst (f,def) -> - machine_constant env ((f,false,n),Generic.replace_vars subst def); - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) + let ce = { const_entry_body = Generic.replace_vars subst def; + const_entry_type = None } in + declare_constant f (ce,n,false); + warning ((string_of_id f)^" is non-recursively defined"); + (var_subst f) :: subst) (List.map var_subst lnamerec) - lnonrec in + lnonrec + in () - let build_scheme lnamedepindsort = let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort - and (sigma,(sign0,fsign0)) = initial_sigma_assumptions() in + and sigma = Evd.empty + and env0 = Global.env() in let lrecspec = List.map (fun (_,dep,ind,sort) -> - let indc = constr_of_com sigma sign0 ind - and s = destSort (constr_of_com sigma sign0 sort) in - (indc,dep,s)) lnamedepindsort - and n = NeverDischarge in - let listdecl = Indrec.build_indrec sigma lrecspec in + let indc = constr_of_com sigma env0 ind + and s = destSort (constr_of_com sigma env0 sort) in + (indc,dep,s)) lnamedepindsort + in + let n = NeverDischarge in + let listdecl = Indrec.build_indrec env0 sigma lrecspec in let rec declare i = function - (fi::lf) -> machine_constant (sign0,fsign0) ((fi,false,n),listdecl.(i)); + | fi::lf -> + let ce = + { const_entry_body = listdecl.(i); const_entry_type = None } in + declare_constant fi (ce,n,false); declare (i+1) lf | _ -> () in - declare 0 lrecnames; pPNL(recursive_message lrecnames) + declare 0 lrecnames; pPNL(recursive_message lrecnames) diff --git a/toplevel/command.mli b/toplevel/command.mli index 51edb51e2..0ba5af296 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -8,11 +8,18 @@ open Declare (*i*) val definition_body : identifier -> strength -> Coqast.t -> unit + val definition_body_red : identifier -> strength -> Coqast.t -> Tacred.red_expr option -> unit + val syntax_definition : identifier -> Coqast.t -> unit + +(*i val abstraction_definition : identifier -> int array -> Coqast.t -> unit +i*) + val hypothesis_def_var : bool -> string -> strength -> Coqast.t -> unit + val parameter_def_var : string -> Coqast.t -> unit val build_mutual : diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0c3bdc576..25e29d703 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1058,6 +1058,7 @@ let _ = message ((string_of_id id) ^ " is now a syntax macro")) | _ -> bad_vernac_args "SyntaxMacro") +(*** let _ = add "ABSTRACTION" (function @@ -1072,6 +1073,7 @@ let _ = if (not(is_silent())) then message ((string_of_id id)^" is now an abstraction")) | _ -> bad_vernac_args "ABSTRACTION") +***) let _ = add "Require" @@ -1238,6 +1240,7 @@ let _ = (* Search commands *) +(*** let _ = add "Searchisos" (function @@ -1248,7 +1251,8 @@ let _ = let cc = nf_betaiota env Evd.empty c in Searchisos.type_search cc) | _ -> bad_vernac_args "Searchisos") - +***) + open Goptions let _ = |