diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-22 17:42:45 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-22 17:42:45 +0000 |
commit | fff07f8260867740f1f8d8b09bd26baa5f99e5c6 (patch) | |
tree | c222eddef1770307a3d097faa8d928228ef61629 | |
parent | 66b674a1d41d9349f4c64543eda5ef005617e3a0 (diff) |
- Ajout d'un cast vm dans la syntaxe : x <: t
Part contre ces cas sont detruis dans les "Definition"
(pas dans les "Lemma") je comprends pas ou ils sont enlev'e...
Si une id'ee ...
- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.
- Meilleur compilation des coinductifs, on utilise maintenant vraimment
du lazy.
- Enfin un peu plus de doc dans le code de la vm.
Benjamin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 372 | ||||
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | dev/vm_printers.ml | 4 | ||||
-rw-r--r-- | kernel/byterun/coq_fix_code.c | 30 | ||||
-rw-r--r-- | kernel/byterun/coq_instruct.h | 14 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 328 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.c | 7 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.h | 1 | ||||
-rw-r--r-- | kernel/byterun/coq_values.c | 3 | ||||
-rw-r--r-- | kernel/byterun/coq_values.h | 13 | ||||
-rw-r--r-- | kernel/cbytecodes.ml | 31 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 18 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 347 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 21 | ||||
-rw-r--r-- | kernel/inductive.ml | 4 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
-rw-r--r-- | kernel/vconv.ml | 357 | ||||
-rw-r--r-- | kernel/vconv.mli | 25 | ||||
-rw-r--r-- | kernel/vm.ml | 749 | ||||
-rw-r--r-- | kernel/vm.mli | 65 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 10 | ||||
-rw-r--r-- | parsing/ppconstr.ml | 5 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 271 | ||||
-rw-r--r-- | pretyping/vnorm.mli | 18 | ||||
-rw-r--r-- | proofs/redexpr.ml | 2 |
26 files changed, 1463 insertions, 1240 deletions
@@ -79,8 +79,8 @@ kernel/type_errors.cmi: kernel/term.cmi kernel/names.cmi kernel/environ.cmi kernel/typeops.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi kernel/environ.cmi kernel/entries.cmi kernel/univ.cmi: lib/pp.cmi kernel/names.cmi -kernel/vconv.cmi: kernel/vm.cmi kernel/term.cmi kernel/reduction.cmi \ - kernel/names.cmi kernel/environ.cmi +kernel/vconv.cmi: kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ + kernel/environ.cmi kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi lib/bigint.cmi: lib/pp.cmi @@ -222,6 +222,8 @@ pretyping/termops.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ pretyping/typing.cmi: kernel/term.cmi pretyping/evd.cmi kernel/environ.cmi pretyping/unification.cmi: kernel/term.cmi pretyping/evd.cmi \ kernel/environ.cmi +pretyping/vnorm.cmi: kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ + kernel/environ.cmi proofs/clenvtac.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ proofs/proof_type.cmi kernel/names.cmi pretyping/evd.cmi \ pretyping/clenv.cmi @@ -555,10 +557,10 @@ ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ lib/options.cmi library/nametab.cmi kernel/names.cmi toplevel/mltop.cmi \ library/library.cmi library/libnames.cmi library/lib.cmi ide/ideutils.cmi \ - tactics/hipattern.cmi library/global.cmi pretyping/evd.cmi \ - pretyping/evarutil.cmi kernel/environ.cmi kernel/declarations.cmi \ - toplevel/coqtop.cmi config/coq_config.cmi toplevel/cerrors.cmi \ - ide/coq.cmi + tactics/hipattern.cmi library/goptions.cmi library/global.cmi \ + pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ + kernel/declarations.cmi toplevel/coqtop.cmi config/coq_config.cmi \ + toplevel/cerrors.cmi ide/coq.cmi ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ toplevel/vernac.cmx lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx lib/system.cmx \ @@ -566,10 +568,10 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ lib/options.cmx library/nametab.cmx kernel/names.cmx toplevel/mltop.cmx \ library/library.cmx library/libnames.cmx library/lib.cmx ide/ideutils.cmx \ - tactics/hipattern.cmx library/global.cmx pretyping/evd.cmx \ - pretyping/evarutil.cmx kernel/environ.cmx kernel/declarations.cmx \ - toplevel/coqtop.cmx config/coq_config.cmx toplevel/cerrors.cmx \ - ide/coq.cmi + tactics/hipattern.cmx library/goptions.cmx library/global.cmx \ + pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ + kernel/declarations.cmx toplevel/coqtop.cmx config/coq_config.cmx \ + toplevel/cerrors.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi ide/find_phrase.cmo: ide/ideutils.cmi @@ -848,14 +850,14 @@ kernel/univ.cmo: lib/util.cmi lib/pp.cmi kernel/names.cmi lib/hashcons.cmi \ kernel/univ.cmi kernel/univ.cmx: lib/util.cmx lib/pp.cmx kernel/names.cmx lib/hashcons.cmx \ kernel/univ.cmi -kernel/vconv.cmo: kernel/vm.cmi lib/util.cmi kernel/univ.cmi kernel/term.cmi \ - kernel/reduction.cmi kernel/names.cmi kernel/inductive.cmi \ - kernel/environ.cmi kernel/declarations.cmi kernel/csymtable.cmi \ - kernel/conv_oracle.cmi kernel/closure.cmi kernel/vconv.cmi -kernel/vconv.cmx: kernel/vm.cmx lib/util.cmx kernel/univ.cmx kernel/term.cmx \ - kernel/reduction.cmx kernel/names.cmx kernel/inductive.cmx \ - kernel/environ.cmx kernel/declarations.cmx kernel/csymtable.cmx \ - kernel/conv_oracle.cmx kernel/closure.cmx kernel/vconv.cmi +kernel/vconv.cmo: kernel/vm.cmi kernel/univ.cmi kernel/term.cmi \ + kernel/reduction.cmi kernel/names.cmi kernel/environ.cmi \ + kernel/declarations.cmi kernel/csymtable.cmi kernel/conv_oracle.cmi \ + kernel/closure.cmi kernel/vconv.cmi +kernel/vconv.cmx: kernel/vm.cmx kernel/univ.cmx kernel/term.cmx \ + kernel/reduction.cmx kernel/names.cmx kernel/environ.cmx \ + kernel/declarations.cmx kernel/csymtable.cmx kernel/conv_oracle.cmx \ + kernel/closure.cmx kernel/vconv.cmi kernel/vm.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \ kernel/conv_oracle.cmi kernel/cbytecodes.cmi kernel/vm.cmi kernel/vm.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \ @@ -1550,6 +1552,14 @@ pretyping/unification.cmx: lib/util.cmx pretyping/typing.cmx \ pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \ library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ kernel/environ.cmx pretyping/unification.cmi +pretyping/vnorm.cmo: kernel/vm.cmi kernel/vconv.cmi lib/util.cmi \ + kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ + kernel/inductive.cmi kernel/environ.cmi kernel/declarations.cmi \ + pretyping/vnorm.cmi +pretyping/vnorm.cmx: kernel/vm.cmx kernel/vconv.cmx lib/util.cmx \ + kernel/term.cmx kernel/reduction.cmx kernel/names.cmx \ + kernel/inductive.cmx kernel/environ.cmx kernel/declarations.cmx \ + pretyping/vnorm.cmi proofs/clenvtac.cmo: lib/util.cmi pretyping/unification.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi proofs/refiner.cmi \ @@ -1626,14 +1636,14 @@ proofs/proof_type.cmx: lib/util.cmx kernel/term.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx pretyping/pattern.cmx library/nametab.cmx \ kernel/names.cmx library/libnames.cmx interp/genarg.cmx pretyping/evd.cmx \ kernel/environ.cmx proofs/proof_type.cmi -proofs/redexpr.cmo: kernel/vconv.cmi lib/util.cmi kernel/typeops.cmi \ +proofs/redexpr.cmo: pretyping/vnorm.cmi lib/util.cmi kernel/typeops.cmi \ kernel/term.cmi pretyping/tacred.cmi library/summary.cmi \ pretyping/reductionops.cmi pretyping/rawterm.cmi lib/pp.cmi \ library/nametab.cmi kernel/names.cmi library/libnames.cmi \ library/global.cmi kernel/environ.cmi kernel/declarations.cmi \ kernel/csymtable.cmi kernel/conv_oracle.cmi kernel/closure.cmi \ proofs/redexpr.cmi -proofs/redexpr.cmx: kernel/vconv.cmx lib/util.cmx kernel/typeops.cmx \ +proofs/redexpr.cmx: pretyping/vnorm.cmx lib/util.cmx kernel/typeops.cmx \ kernel/term.cmx pretyping/tacred.cmx library/summary.cmx \ pretyping/reductionops.cmx pretyping/rawterm.cmx lib/pp.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ @@ -2298,44 +2308,46 @@ toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \ kernel/term.cmi tactics/tactics.cmi parsing/tactic_printer.cmi \ proofs/tactic_debug.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo lib/system.cmi interp/syntax_def.cmi \ - library/states.cmi tactics/setoid_replace.cmi parsing/search.cmi \ - kernel/safe_typing.cmi interp/reserve.cmi pretyping/reductionops.cmi \ - proofs/redexpr.cmi pretyping/recordops.cmi toplevel/record.cmi \ - pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ - parsing/printmod.cmi parsing/printer.cmi pretyping/pretyping.cmi \ - parsing/prettyp.cmi lib/pp_control.cmi lib/pp.cmi proofs/pfedit.cmi \ - lib/options.cmi interp/notation.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi interp/modintern.cmi toplevel/mltop.cmi \ - toplevel/metasyntax.cmi library/library.cmi library/libnames.cmi \ - library/lib.cmi pretyping/inductiveops.cmi library/impargs.cmi \ - library/goptions.cmi library/global.cmi pretyping/evd.cmi \ - pretyping/evarutil.cmi kernel/environ.cmi kernel/entries.cmi \ - pretyping/detyping.cmi library/declaremods.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ - toplevel/command.cmi pretyping/classops.cmi toplevel/class.cmi \ - tactics/autorewrite.cmi tactics/auto.cmi toplevel/vernacentries.cmi + library/states.cmi kernel/sign.cmi tactics/setoid_replace.cmi \ + parsing/search.cmi kernel/safe_typing.cmi interp/reserve.cmi \ + pretyping/reductionops.cmi proofs/redexpr.cmi pretyping/recordops.cmi \ + toplevel/record.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ + proofs/proof_trees.cmi parsing/printmod.cmi parsing/printer.cmi \ + pretyping/pretyping.cmi parsing/prettyp.cmi lib/pp_control.cmi lib/pp.cmi \ + proofs/pfedit.cmi lib/options.cmi interp/notation.cmi library/nametab.cmi \ + kernel/names.cmi library/nameops.cmi interp/modintern.cmi \ + toplevel/mltop.cmi toplevel/metasyntax.cmi library/library.cmi \ + library/libnames.cmi library/lib.cmi pretyping/inductiveops.cmi \ + library/impargs.cmi library/goptions.cmi library/global.cmi \ + pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ + kernel/entries.cmi pretyping/detyping.cmi library/declaremods.cmi \ + kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \ + interp/constrextern.cmi toplevel/command.cmi pretyping/classops.cmi \ + toplevel/class.cmi tactics/autorewrite.cmi tactics/auto.cmi \ + toplevel/vernacentries.cmi toplevel/vernacentries.cmx: kernel/vm.cmx toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx kernel/vconv.cmx lib/util.cmx kernel/univ.cmx \ kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx parsing/tactic_printer.cmx \ proofs/tactic_debug.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx lib/system.cmx interp/syntax_def.cmx \ - library/states.cmx tactics/setoid_replace.cmx parsing/search.cmx \ - kernel/safe_typing.cmx interp/reserve.cmx pretyping/reductionops.cmx \ - proofs/redexpr.cmx pretyping/recordops.cmx toplevel/record.cmx \ - pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ - parsing/printmod.cmx parsing/printer.cmx pretyping/pretyping.cmx \ - parsing/prettyp.cmx lib/pp_control.cmx lib/pp.cmx proofs/pfedit.cmx \ - lib/options.cmx interp/notation.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx interp/modintern.cmx toplevel/mltop.cmx \ - toplevel/metasyntax.cmx library/library.cmx library/libnames.cmx \ - library/lib.cmx pretyping/inductiveops.cmx library/impargs.cmx \ - library/goptions.cmx library/global.cmx pretyping/evd.cmx \ - pretyping/evarutil.cmx kernel/environ.cmx kernel/entries.cmx \ - pretyping/detyping.cmx library/declaremods.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \ - toplevel/command.cmx pretyping/classops.cmx toplevel/class.cmx \ - tactics/autorewrite.cmx tactics/auto.cmx toplevel/vernacentries.cmi + library/states.cmx kernel/sign.cmx tactics/setoid_replace.cmx \ + parsing/search.cmx kernel/safe_typing.cmx interp/reserve.cmx \ + pretyping/reductionops.cmx proofs/redexpr.cmx pretyping/recordops.cmx \ + toplevel/record.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + proofs/proof_trees.cmx parsing/printmod.cmx parsing/printer.cmx \ + pretyping/pretyping.cmx parsing/prettyp.cmx lib/pp_control.cmx lib/pp.cmx \ + proofs/pfedit.cmx lib/options.cmx interp/notation.cmx library/nametab.cmx \ + kernel/names.cmx library/nameops.cmx interp/modintern.cmx \ + toplevel/mltop.cmx toplevel/metasyntax.cmx library/library.cmx \ + library/libnames.cmx library/lib.cmx pretyping/inductiveops.cmx \ + library/impargs.cmx library/goptions.cmx library/global.cmx \ + pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ + kernel/entries.cmx pretyping/detyping.cmx library/declaremods.cmx \ + kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \ + interp/constrextern.cmx toplevel/command.cmx pretyping/classops.cmx \ + toplevel/class.cmx tactics/autorewrite.cmx tactics/auto.cmx \ + toplevel/vernacentries.cmi toplevel/vernacexpr.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi interp/ppextend.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi library/goptions.cmi \ @@ -2848,9 +2860,9 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \ toplevel/cerrors.cmx contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ - tactics/tactics.cmi tactics/tacticals.cmi proofs/tactic_debug.cmi \ - pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ - kernel/sign.cmi pretyping/reductionops.cmi contrib/recdef/recdef.cmo \ + tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \ + proofs/tacmach.cmi tactics/tacinterp.cmi kernel/sign.cmi \ + pretyping/reductionops.cmi contrib/recdef/recdef.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ lib/pp.cmi proofs/pfedit.cmi lib/options.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ @@ -2862,9 +2874,9 @@ contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ contrib/funind/functional_principles_proofs.cmi contrib/funind/functional_principles_proofs.cmx: lib/util.cmx \ pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \ - tactics/tactics.cmx tactics/tacticals.cmx proofs/tactic_debug.cmx \ - pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ - kernel/sign.cmx pretyping/reductionops.cmx contrib/recdef/recdef.cmx \ + tactics/tactics.cmx tactics/tacticals.cmx pretyping/tacred.cmx \ + proofs/tacmach.cmx tactics/tacinterp.cmx kernel/sign.cmx \ + pretyping/reductionops.cmx contrib/recdef/recdef.cmx \ pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ lib/pp.cmx proofs/pfedit.cmx lib/options.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ @@ -2906,20 +2918,22 @@ contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \ parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ kernel/mod_subst.cmi library/libobject.cmi library/libnames.cmi \ - library/lib.cmi library/global.cmi pretyping/evd.cmi \ - pretyping/evarutil.cmi kernel/entries.cmi library/declare.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \ - kernel/closure.cmi contrib/funind/indfun_common.cmi + library/lib.cmi library/impargs.cmi library/goptions.cmi \ + library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ + kernel/entries.cmi library/declare.cmi kernel/declarations.cmi \ + library/decl_kinds.cmo interp/coqlib.cmi kernel/closure.cmi \ + contrib/funind/indfun_common.cmi contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/term.cmx library/summary.cmx proofs/refiner.cmx \ pretyping/reductionops.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ kernel/mod_subst.cmx library/libobject.cmx library/libnames.cmx \ - library/lib.cmx library/global.cmx pretyping/evd.cmx \ - pretyping/evarutil.cmx kernel/entries.cmx library/declare.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \ - kernel/closure.cmx contrib/funind/indfun_common.cmi + library/lib.cmx library/impargs.cmx library/goptions.cmx \ + library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ + kernel/entries.cmx library/declare.cmx kernel/declarations.cmx \ + library/decl_kinds.cmx interp/coqlib.cmx kernel/closure.cmx \ + contrib/funind/indfun_common.cmi contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ @@ -2977,63 +2991,63 @@ contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ contrib/funind/invfun.cmo: toplevel/vernacentries.cmi lib/util.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tauto.cmo tactics/tactics.cmi tactics/tacticals.cmi \ - proofs/tactic_debug.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ - proofs/tacexpr.cmo kernel/sign.cmi lib/rtree.cmi \ - pretyping/reductionops.cmi pretyping/rawterm.cmi parsing/printer.cmi \ - parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi kernel/names.cmi \ - library/nameops.cmi library/libnames.cmi tactics/inv.cmi \ - kernel/inductive.cmi pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi tactics/hiddentac.cmi library/global.cmi \ - interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \ - kernel/environ.cmi kernel/entries.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/coqlib.cmi toplevel/command.cmi \ - kernel/closure.cmi toplevel/cerrors.cmi + proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ + kernel/sign.cmi lib/rtree.cmi pretyping/reductionops.cmi \ + pretyping/rawterm.cmi parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi \ + proofs/pfedit.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi tactics/inv.cmi kernel/inductive.cmi \ + pretyping/indrec.cmi contrib/funind/indfun_common.cmi \ + tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ + kernel/entries.cmi kernel/declarations.cmi library/decl_kinds.cmo \ + interp/coqlib.cmi toplevel/command.cmi kernel/closure.cmi \ + toplevel/cerrors.cmi contrib/funind/invfun.cmx: toplevel/vernacentries.cmx lib/util.cmx \ pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tauto.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - proofs/tactic_debug.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ - proofs/tacexpr.cmx kernel/sign.cmx lib/rtree.cmx \ - pretyping/reductionops.cmx pretyping/rawterm.cmx parsing/printer.cmx \ - parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx kernel/names.cmx \ - library/nameops.cmx library/libnames.cmx tactics/inv.cmx \ - kernel/inductive.cmx pretyping/indrec.cmx \ - contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \ - interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \ - kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/coqlib.cmx toplevel/command.cmx \ - kernel/closure.cmx toplevel/cerrors.cmx -contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \ - tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \ - parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi pretyping/inductiveops.cmi \ + proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ + kernel/sign.cmx lib/rtree.cmx pretyping/reductionops.cmx \ + pretyping/rawterm.cmx parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx \ + proofs/pfedit.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx tactics/inv.cmx kernel/inductive.cmx \ + pretyping/indrec.cmx contrib/funind/indfun_common.cmx \ + tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ + kernel/entries.cmx kernel/declarations.cmx library/decl_kinds.cmx \ + interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \ + toplevel/cerrors.cmx +contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi \ + parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi \ + library/nameops.cmi library/libnames.cmi pretyping/inductiveops.cmi \ contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \ interp/coqlib.cmi contrib/funind/rawtermops.cmi -contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \ - tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \ - parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx pretyping/inductiveops.cmx \ +contrib/funind/rawtermops.cmx: lib/util.cmx pretyping/rawterm.cmx \ + parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx \ + library/nameops.cmx library/libnames.cmx pretyping/inductiveops.cmx \ contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \ interp/coqlib.cmx contrib/funind/rawtermops.cmi contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ - pretyping/typing.cmi interp/topconstr.cmi kernel/term.cmi \ - proofs/tactic_debug.cmi tactics/tacinterp.cmi lib/system.cmi \ + pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tacinterp.cmi lib/system.cmi kernel/sign.cmi \ kernel/reduction.cmi contrib/funind/rawtermops.cmi pretyping/rawterm.cmi \ - parsing/printer.cmi parsing/ppvernac.cmi parsing/ppconstr.cmi lib/pp.cmi \ - lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \ - pretyping/inductiveops.cmi kernel/inductive.cmi \ - contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \ - pretyping/evd.cmi kernel/declarations.cmi interp/coqlib.cmi \ + parsing/printer.cmi pretyping/pretyping.cmi parsing/ppvernac.cmi \ + parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \ + library/nameops.cmi library/libnames.cmi pretyping/inductiveops.cmi \ + kernel/inductive.cmi contrib/funind/indfun_common.cmi library/impargs.cmi \ + library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ + pretyping/detyping.cmi kernel/declarations.cmi interp/coqlib.cmi \ interp/constrextern.cmi toplevel/command.cmi toplevel/cerrors.cmi \ contrib/funind/rawterm_to_relation.cmi contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - pretyping/typing.cmx interp/topconstr.cmx kernel/term.cmx \ - proofs/tactic_debug.cmx tactics/tacinterp.cmx lib/system.cmx \ + pretyping/typing.cmx interp/topconstr.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tacinterp.cmx lib/system.cmx kernel/sign.cmx \ kernel/reduction.cmx contrib/funind/rawtermops.cmx pretyping/rawterm.cmx \ - parsing/printer.cmx parsing/ppvernac.cmx parsing/ppconstr.cmx lib/pp.cmx \ - lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \ - pretyping/inductiveops.cmx kernel/inductive.cmx \ - contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \ - pretyping/evd.cmx kernel/declarations.cmx interp/coqlib.cmx \ + parsing/printer.cmx pretyping/pretyping.cmx parsing/ppvernac.cmx \ + parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx kernel/names.cmx \ + library/nameops.cmx library/libnames.cmx pretyping/inductiveops.cmx \ + kernel/inductive.cmx contrib/funind/indfun_common.cmx library/impargs.cmx \ + library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ + pretyping/detyping.cmx kernel/declarations.cmx interp/coqlib.cmx \ interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ contrib/funind/rawterm_to_relation.cmi contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ @@ -3991,96 +4005,74 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/compatibility.h \ - /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /user/jforest/home//lib/ocaml/caml/config.h \ - /user/jforest/home//lib/ocaml/caml/fail.h \ - /user/jforest/home//lib/ocaml/caml/mlvalues.h \ - /user/jforest/home//lib/ocaml/caml/misc.h \ - /user/jforest/home//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /user/jforest/home//lib/ocaml/caml/alloc.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h @@ -91,7 +91,7 @@ UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values COQOPTS=$(GLOB) $(COQ_XML) $(VM) $(UNBOXEDVALUES) TIME= # is "'time -p'" to get compilation time of .v -BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS) +BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS) ########################################################################### @@ -141,7 +141,7 @@ LIBRARY=\ PRETYPING=\ pretyping/termops.cmo pretyping/evd.cmo \ - pretyping/reductionops.cmo pretyping/inductiveops.cmo \ + pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \ pretyping/retyping.cmo pretyping/cbv.cmo \ pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ pretyping/tacred.cmo \ diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c037eca7c..1e1144895 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -65,8 +65,6 @@ and ppatom a = print_string (string_of_kn sp); print_string ","; print_int i; print_string ")" - | Afix_app _ -> print_vfix_app () - | Aswitch _ -> print_vswith() and ppwhd whd = match whd with @@ -74,9 +72,7 @@ and ppwhd whd = | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() - | Vfix_app _ -> print_vfix_app() | Vcofix _ -> print_string "cofix" - | Vcofix_app _ -> print_string "cofix_app" | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4616580df..70648b44b 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -27,31 +27,31 @@ void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= - arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]= - arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]= - arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]= - arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= + arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= + arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= + arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= + arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= + arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= + arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0; + arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]= - arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]= - arity[GRAB]=arity[COGRAB]= - arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]= - arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]= - arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]= - arity[ACCUMULATECOND]= 1; + arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= + arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= + arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= + arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= + arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= + arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[SWITCH]=0; + arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; } #endif /* THREADED_CODE */ @@ -150,7 +150,7 @@ value coq_tcode_of_code (value code, value size) { block_size = sizes >> 16; sizes = const_size + block_size; for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; }; - } else if (instr == CLOSUREREC) { + } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) { uint32 i, n; COPY32(q,p); p++; /* ndefs */ n = 3 + 2*(*q); /* ndefs, nvars, start, typlbls,lbls*/ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index d3b07526f..89616c5f3 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -22,18 +22,20 @@ enum instructions { PUSH_RETADDR, APPLY, APPLY1, APPLY2, APPLY3, APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, COGRAB, - CLOSURE, CLOSUREREC, + RETURN, RESTART, GRAB, GRABREC, + CLOSURE, CLOSUREREC, CLOSURECOFIX, OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, PUSHOFFSETCLOSURE, GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, - FORCE, SWITCH, PUSHFIELD, + MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, + SWITCH, PUSHFIELDS, + GETFIELD0, GETFIELD1, GETFIELD, + SETFIELD0, SETFIELD1, SETFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, ACCUMULATECOND, STOP + ACCUMULATE, ACCUMULATECOND, + MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP }; #endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8bfe78ebe..180e2b011 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */ # define Next break #endif -/* #define _COQ_DEBUG_ */ +/*#define _COQ_DEBUG_ */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) @@ -164,7 +164,7 @@ value coq_interprete #else opcode_t curr_instr; #endif - print_instr("Enter Interpreter"); + print_instr("Enter Interpreter"); if (coq_pc == NULL) { /* Interpreter is initializing */ print_instr("Interpreter is initializing"); #ifdef THREADED_CODE @@ -383,6 +383,17 @@ value coq_interprete coq_extra_args = 2; goto check_stacks; } + /* Stack checks */ + + check_stacks: + print_instr("check_stacks"); + if (sp < coq_stack_threshold) { + coq_sp = sp; + realloc_coq_stack(Coq_stack_threshold); + sp = coq_sp; + } + Next; + /* Fall through CHECK_SIGNALS */ Instruct(APPTERM) { int nargs = *pc++; @@ -438,6 +449,7 @@ value coq_interprete Instruct(RETURN) { print_instr("RETURN"); + print_int(*pc); sp += *pc++; if (coq_extra_args > 0) { coq_extra_args--; @@ -485,30 +497,6 @@ value coq_interprete Next; } - Instruct(COGRAB){ - int required = *pc++; - print_instr("COGRAB"); - if(forcable == Val_true) { - print_instr("true"); - /* L'instruction précédante est FORCE */ - if (coq_extra_args > 0) coq_extra_args--; - pc++; - forcable = Val_false; - } else { /* L'instruction précédante est APPLY */ - mlsize_t num_args, i; - num_args = 1 + coq_extra_args; /* arg1 + extra args */ - Alloc_small(accu, num_args + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i]; - Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ - sp += num_args; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - Next; - } Instruct(GRABREC) { int rec_pos = *pc++; /* commence a zero */ print_instr("GRABREC"); @@ -607,7 +595,59 @@ value coq_interprete accu = accu + 2 * start * sizeof(value); Next; } - + + Instruct(CLOSURECOFIX){ + int nfunc = *pc++; + int nvars = *pc++; + int start = *pc++; + int i, j , size; + value * p; + print_instr("CLOSURECOFIX"); + if (nvars > 0) *--sp = accu; + /* construction du vecteur de type */ + Alloc_small(accu, nfunc, 0); + for(i = 0; i < nfunc; i++) { + Field(accu,i) = (value)(pc+pc[i]); + } + pc += nfunc; + *--sp=accu; + + /* Creation des blocks accumulate */ + for(i=0; i < nfunc; i++) { + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = Val_int(1); + *--sp=accu; + } + /* creation des fonction cofix */ + + p = sp; + size = nfunc + nvars + 2; + for (i=0; i < nfunc; i++) { + + Alloc_small(accu, size, Closure_tag); + Code_val(accu) = pc+pc[i]; + for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j]; + Field(accu, size - 1) = p[nfunc]; + for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j]; + *--sp = accu; + /* creation du block contenant le cofix */ + + Alloc_small(accu,1, ATOM_COFIX_TAG); + Field(accu, 0) = sp[0]; + *sp = accu; + /* mise a jour du block accumulate */ + caml_modify(&Field(p[i], 1),*sp); + sp++; + } + pc += nfunc; + accu = p[start]; + sp = p + nfunc + 1 + nvars; + print_instr("ici4"); + Next; + } + + Instruct(PUSHOFFSETCLOSURE) { print_instr("PUSHOFFSETCLOSURE"); *--sp = accu; @@ -644,7 +684,7 @@ value coq_interprete /* Access to global variables */ Instruct(PUSHGETGLOBAL) { - print_instr("PUSHGETGLOBAL"); + print_instr("PUSH"); *--sp = accu; } /* Fallthrough */ @@ -703,38 +743,27 @@ value coq_interprete accu = block; Next; } + Instruct(MAKEBLOCK4) { + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK4"); + Alloc_small(block, 4, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + Field(block, 3) = sp[2]; + sp += 3; + accu = block; + Next; + } /* Access to components of blocks */ - -/* Branches and conditional branches */ - Instruct(FORCE) { - print_instr("FORCE"); - if (Is_block(accu) && Tag_val(accu) == Closure_tag) { - forcable = Val_true; - /* On pousse l'addresse de retour et l'argument */ - sp -= 3; - sp[0] = (value) (pc - 1); - sp[1] = coq_env; - sp[2] = Val_long(coq_extra_args); - /* On evalue le cofix */ - coq_extra_args = 0; - pc = Code_val(accu); - coq_env = accu; - goto check_stacks; - } else { - if (Is_block(accu)) print_int(Tag_val(accu)); - else print_instr("Not a block"); - } - Next; - } - - Instruct(SWITCH) { uint32 sizes = *pc++; print_instr("SWITCH"); - print_int(sizes); + print_int(sizes & 0xFFFF); if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); @@ -748,68 +777,56 @@ value coq_interprete } Next; } - Instruct(PUSHFIELD){ + + Instruct(PUSHFIELDS){ int i; int size = *pc++; - print_instr("PUSHFIELD"); + print_instr("PUSHFIELDS"); sp -= size; for(i=0;i<size;i++)sp[i] = Field(accu,i); Next; } - - Instruct(MAKESWITCHBLOCK) { - mlsize_t sz; - int i, annot; - code_t typlbl,swlbl; - print_instr("MAKESWITCHBLOCK"); - typlbl = (code_t)pc + *pc; - pc++; - swlbl = (code_t)pc + *pc; - pc++; - annot = *pc++; - sz = *pc++; - *--sp = accu; - *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ - if (sz == 0) accu = Atom(0); - else { - Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { - for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; - }else{ - for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; - } - } - *--sp = accu; - /* On cree le zipper switch */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; - /* On cree l'atome */ - Alloc_small(accu, 2, ATOM_SWITCH_TAG); - Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; - sp++;sp[0] = accu; - /* On cree l'accumulateur */ - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu,1) = *sp++; + + Instruct(GETFIELD0){ + print_instr("GETFIELD0"); + accu = Field(accu, 0); Next; } - /* Stack checks */ - - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; + Instruct(GETFIELD1){ + print_instr("GETFIELD1"); + accu = Field(accu, 1); + Next; } - Next; - /* Fall through CHECK_SIGNALS */ + Instruct(GETFIELD){ + print_instr("GETFIELD"); + accu = Field(accu, *pc); + pc++; + Next; + } + + Instruct(SETFIELD0){ + print_instr("SETFIELD0"); + caml_modify(&Field(accu, 0),*sp); + sp++; + Next; + } + + Instruct(SETFIELD1){ + print_instr("SETFIELD1"); + caml_modify(&Field(accu, 1),*sp); + sp++; + Next; + } + + Instruct(SETFIELD){ + print_instr("SETFIELD"); + caml_modify(&Field(accu, *pc),*sp); + sp++; pc++; + Next; + } + /* Integer constants */ Instruct(CONST0){ @@ -854,14 +871,7 @@ value coq_interprete Next; } -/* Debugging and machine control */ - - Instruct(STOP){ - print_instr("STOP"); - coq_sp = sp; - return accu; - } - + /* Special operations for reduction of open term */ Instruct(ACCUMULATECOND) { int i, num; print_instr("ACCUMULATECOND"); @@ -869,7 +879,7 @@ value coq_interprete pc++; if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) { /* printf ("false\n"); - printf ("tag = %d", Tag_val(Field(accu,1))); */ + printf ("tag = %d", Tag_val(Field(accu,1))); */ num = Wosize_val(coq_env); for(i = 2; i < num; i++) *--sp = Field(accu,i); coq_extra_args = coq_extra_args + (num - 2); @@ -881,7 +891,7 @@ value coq_interprete }; /* printf ("true\n"); */ } - + Instruct(ACCUMULATE) { mlsize_t i, size; print_instr("ACCUMULATE"); @@ -896,7 +906,86 @@ value coq_interprete sp += 3; Next; } - + Instruct(MAKESWITCHBLOCK) { + print_instr("MAKESWITCHBLOCK"); + *--sp = accu; + accu = Field(accu,1); + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: + { + mlsize_t i, nargs; + print_instr("COFIX_TAG"); + sp-=2; + pc++; + sp[0] = (value) (pc + *pc); + sp[1] = coq_env; + coq_env = Field(accu,0); + accu = sp[2]; + sp[2] = Val_long(coq_extra_args); + nargs = Wosize_val(accu) - 2; + sp -= nargs; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; + print_int(nargs); + coq_extra_args = nargs; + pc = Code_val(coq_env); + goto check_stacks; + } + case ATOM_COFIXEVALUATED_TAG: + { + print_instr("COFIX_EVAL_TAG"); + accu = Field(accu,1); + pc++; + pc = pc + *pc; + sp++; + Next; + } + default: + { + mlsize_t sz; + int i, annot; + code_t typlbl,swlbl; + print_instr("MAKESWITCHBLOCK"); + + typlbl = (code_t)pc + *pc; + pc++; + swlbl = (code_t)pc + *pc; + pc++; + annot = *pc++; + sz = *pc++; + *--sp=Field(coq_global_data, annot); + /* On sauve la pile */ + if (sz == 0) accu = Atom(0); + else { + Alloc_small(accu, sz, Default_tag); + if (Field(*sp, 2) == Val_true) { + for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; + }else{ + for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; + } + } + *--sp = accu; + /* On cree le zipper switch */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; + Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; + Field(accu, 4) = coq_env; + sp++;sp[0] = accu; + /* On cree l'atome */ + Alloc_small(accu, 2, ATOM_SWITCH_TAG); + Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; + sp++;sp[0] = accu; + /* On cree l'accumulateur */ + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = *sp++; + } + } + Next; + } + + + Instruct(MAKEACCU) { int i; print_instr("MAKEACCU"); @@ -921,6 +1010,15 @@ value coq_interprete Next; } +/* Debugging and machine control */ + + Instruct(STOP){ + print_instr("STOP"); + coq_sp = sp; + return accu; + } + + #ifndef THREADED_CODE default: /*fprintf(stderr, "%d\n", *pc);*/ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index db6aacb92..bfcb6812c 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -34,7 +34,6 @@ int drawinstr; long coq_saved_sp_offset; value * coq_sp; -value forcable; /* Some predefined pointer code */ code_t accumulate; @@ -135,7 +134,6 @@ value init_coq_vm(value unit) /* ML */ init_coq_atom_tbl(40); /* Initialing the interpreter */ coq_all_transp = 0; - forcable = Val_false; init_coq_interpreter(); /* Some predefined pointer code */ @@ -266,8 +264,9 @@ value coq_set_drawinstr(value unit) return Val_unit; } -value coq_set_forcable (value unit) + +value coq_print_pointer(value p) { - forcable = Val_true; + printf("pointer = %X\n", p); return Val_unit; } diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 7c96e684e..0d866dc76 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -43,7 +43,6 @@ extern int drawinstr; /* interp state */ extern value * coq_sp; -extern value forcable; /* Some predefined pointer code */ extern code_t accumulate; diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index baf3ab090..34b885e8f 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -27,8 +27,7 @@ value coq_kind_of_closure(value v) { if (Is_instruction(c, GRAB)) return Val_int(0); if (Is_instruction(c, RESTART)) {is_app = 1; c++;} if (Is_instruction(c, GRABREC)) return Val_int(1+is_app); - if (Is_instruction(c, COGRAB)) return Val_int(3+is_app); - if (Is_instruction(c, MAKEACCU)) return Val_int(5); + if (Is_instruction(c, MAKEACCU)) return Val_int(3); return Val_int(0); } diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a186d62aa..48fba64bf 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,11 +14,20 @@ #include "alloc.h" #include "mlvalues.h" +#define Default_tag 0 +#define Accu_tag 0 + + + +#define ATOM_ID_TAG 0 +#define ATOM_IDDEF_TAG 1 +#define ATOM_INDUCTIVE_TAG 2 #define ATOM_FIX_TAG 3 #define ATOM_SWITCH_TAG 4 +#define ATOM_COFIX_TAG 5 +#define ATOM_COFIXEVALUATED_TAG 6 + -#define Accu_tag 0 -#define Default_tag 0 /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 499554746..a9b16f29c 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -3,6 +3,14 @@ open Term type tag = int +let id_tag = 0 +let iddef_tag = 1 +let ind_tag = 2 +let fix_tag = 3 +let switch_tag = 4 +let cofix_tag = 5 +let cofix_evaluated_tag = 6 + type structured_constant = | Const_sorts of sorts | Const_ind of inductive @@ -39,18 +47,20 @@ type instruction = | Krestart | Kgrab of int (* number of arguments *) | Kgrabrec of int (* rec arg *) - | Kcograb of int (* number of arguments *) | Kclosure of Label.t * int (* label, number of free variables *) | Kclosurerec of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix of int * int * Label.t array * Label.t array + (* nb fv, init, lbl types, lbl bodies *) | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kforce | Kswitch of Label.t array * Label.t array (* consts,blocks *) - | Kpushfield of int + | Kpushfields of int + | Kfield of int + | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes @@ -79,7 +89,6 @@ let rec instruction ppf = function | Krestart -> fprintf ppf "\trestart" | Kgrab n -> fprintf ppf "\tgrab %i" n | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n - | Kcograb n -> fprintf ppf "\tcograb %i" n | Kclosure(lbl, n) -> fprintf ppf "\tclosure L%i, %i" lbl n | Kclosurerec(fv,init,lblt,lblb) -> @@ -89,7 +98,13 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - (* nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix (fv,init,lblt,lblb) -> + fprintf ppf "\tclosurecofix"; + fprintf ppf " %i , %i, " fv init; + print_string "types = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; + print_string " bodies = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" @@ -98,13 +113,13 @@ let rec instruction ppf = function | Kmakeprod -> fprintf ppf "\tmakeprod" | Kmakeswitchblock(lblt,lbls,_,sz) -> fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz - | Kforce -> fprintf ppf "\tforce" | Kswitch(lblc,lblb) -> fprintf ppf "\tswitch"; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kpushfield n -> - fprintf ppf "\tpushfield %i" n + | Kpushfields n -> fprintf ppf "\tpushfields %i" n + | Ksetfield n -> fprintf ppf "\tsetfield %i" n + | Kfield n -> fprintf ppf "\tgetfield %i" n | Kstop -> fprintf ppf "\tstop" | Ksequence (c1,c2) -> fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index a996f7505..215b6ad4a 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -3,6 +3,14 @@ open Term type tag = int +val id_tag : tag +val iddef_tag : tag +val ind_tag : tag +val fix_tag : tag +val switch_tag : tag +val cofix_tag : tag +val cofix_evaluated_tag : tag + type structured_constant = | Const_sorts of sorts | Const_ind of inductive @@ -37,21 +45,24 @@ type instruction = | Krestart | Kgrab of int (* number of arguments *) | Kgrabrec of int (* rec arg *) - | Kcograb of int (* number of arguments *) | Kclosure of Label.t * int (* label, number of free variables *) | Kclosurerec of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix of int * int * Label.t array * Label.t array + (* nb fv, init, lbl types, lbl bodies *) | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kforce | Kswitch of Label.t array * Label.t array (* consts,blocks *) - | Kpushfield of int + | Kpushfields of int + | Kfield of int + | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes + and bytecodes = instruction list type fv_elem = FVnamed of identifier | FVrel of int @@ -59,3 +70,4 @@ type fv_elem = FVnamed of identifier | FVrel of int type fv = fv_elem array val draw_instr : bytecodes -> unit + diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 041e0795d..e1f89fadb 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -6,35 +6,161 @@ open Term open Declarations open Pre_env -(*i Compilation des variables + calcul des variables libres *) -(* Representation des environnements machines : *) -(*[t0|C0| ... |tc|Cc| ... |t(nbr-1)|C(nbr-1)| fv1 | fv1 | .... | fvn] *) -(* ^<----------offset---------> *) - - -type fv = fv_elem list - -type vm_env = {size : int; fv_rev : fv} - (* size = n; fv_rev = [fvn; ... ;fv1] *) - -type t = { - nb_stack : int; (* nbre de variables sur la pile *) - in_stack : int list; (* position dans la pile *) - nb_rec : int; (* nbre de fonctions mutuellement recursives = - nbr *) - pos_rec : int; (* position de la fonction courante = c *) - offset : int; - in_env : vm_env ref - } - -let empty_fv = {size= 0; fv_rev = []} +(* Compilation des variables + calcul des variables libres *) + +(* Dans la machine virtuel il n'y a pas de difference entre les *) +(* fonctions et leur environnement *) + +(* Representation de l'environnements des fonctions : *) +(* [clos_t | code | fv1 | fv2 | ... | fvn ] *) +(* ^ *) +(* l'offset pour l'acces au variable libre est 1 (il faut passer le *) +(* pointeur de code). *) +(* Lors de la compilation, les variables libres sont stock'ees dans *) +(* [in_env] dans l'ordre inverse de la representation machine, ceci *) +(* permet de rajouter des nouvelles variables dans l'environnememt *) +(* facilement. *) +(* Les arguments de la fonction arrive sur la pile dans l'ordre de *) +(* l'application : f arg1 ... argn *) +(* - la pile est alors : *) +(* arg1 : ... argn : extra args : return addr : ... *) +(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn *) +(* [n], [argn] par le de Bruijn [1] *) + +(* Representation des environnements des points fix mutuels : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^<----------offset---------> *) +(* type = [Ct1 | .... | Ctn] *) +(* Ci est le code correspondant au corps du ieme point fix *) +(* Lors de l'evaluation d'un point fix l'environnement est un pointeur *) +(* sur la position correspondante a son code. *) +(* Dans le corps de chaque point fix le de Bruijn [nbr] represente, *) +(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le *) +(* nbr-ieme. *) +(* L'acces a ces variables se fait par l'instruction [Koffsetclosure] *) +(* (decalage de l'environnement) *) + +(* Ceci permet de representer tout les point fix mutuels en un seul bloc *) +(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des *) +(* types des points fixes, ils sont utilises pour tester la conversion *) +(* Leur environnement d'execution est celui du dernier point fix : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^ *) + + +(* Representation des cofix mutuels : *) +(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) +(* ... *) +(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) +(* *) +(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* ... *) +(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* Les block [ai] sont des fonctions qui accumulent leurs arguments : *) +(* ai arg1 argp ---> *) +(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) +(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation, *) +(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp] *) +(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de *) +(* l'evaluation : *) +(* ai' <-- *) +(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) +(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *) +(* fois l'application d'un cofix (evaluation lazy) *) +(* De plus elle permet de creer facilement des cycles quand les cofix ne *) +(* n'ont pas d'aruments, ex: *) +(* cofix one := cons 1 one *) +(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) +(* fcofix1 = [clos_t | code | a1] *) +(* Quand on force l'evaluation de [a1] le resultat est *) +(* [cons_t | 1 | a1] *) +(* [a1] est mis a jour : *) +(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) +(* Le cycle est cree ... *) + +(* On conserve la fct de cofix pour la conversion *) + +type vm_env = { + size : int; (* longueur de la liste [n] *) + fv_rev : fv_elem list (* [fvn; ... ;fv1] *) + } + +let empty_fv = { size= 0; fv_rev = [] } + +type comp_env = { + nb_stack : int; (* nbre de variables sur la pile *) + in_stack : int list; (* position dans la pile *) + nb_rec : int; (* nbre de fonctions mutuellement *) + (* recursives = nbr *) + pos_rec : instruction list; (* instruction d'acces pour les variables *) + (* de point fix ou de cofix *) + offset : int; + in_env : vm_env ref + } let fv r = !(r.in_env) + +let empty_comp_env ()= + { nb_stack = 0; + in_stack = []; + nb_rec = 0; + pos_rec = []; + offset = 0; + in_env = ref empty_fv; + } + +(*i Creation functions for comp_env *) -(* [add_param n] rend la liste [sz+1;sz+2;...;sz+n] *) let rec add_param n sz l = if n = 0 then l else add_param (n - 1) sz (n+sz::l) + +let comp_env_fun arity = + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = ref empty_fv + } + + +let comp_env_type rfv = + { nb_stack = 0; + in_stack = []; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = rfv + } + +let comp_env_fix ndef curr_pos arity rfv = + let prec = ref [] in + for i = ndef downto 1 do + prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec + done; + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = ndef; + pos_rec = !prec; + offset = 2 * (ndef - curr_pos - 1)+1; + in_env = rfv + } + +let comp_env_cofix ndef arity rfv = + let prec = ref [] in + for i = 1 to ndef do + prec := Kenvacc i :: !prec + done; + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = ndef; + pos_rec = !prec; + offset = ndef+1; + in_env = rfv + } (* [push_param ] ajoute les parametres de fonction dans la pile *) let push_param n sz r = @@ -42,33 +168,16 @@ let push_param n sz r = nb_stack = r.nb_stack + n; in_stack = add_param n sz r.in_stack } -(* [push_local e sz] ajoute une nouvelle variable dans la pile a la position *) +(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *) +(* position [sz] *) let push_local sz r = { r with nb_stack = r.nb_stack + 1; in_stack = (sz + 1) :: r.in_stack } -(* Table de relocation initiale *) -let empty () = - { nb_stack = 0; in_stack = []; - nb_rec = 0;pos_rec = 0; - offset = 0; in_env = ref empty_fv } -let init_fun arity = - { nb_stack = arity; in_stack = add_param arity 0 []; - nb_rec = 0; pos_rec = 0; - offset = 1; in_env = ref empty_fv } - -let init_type ndef rfv = - { nb_stack = 0; in_stack = []; - nb_rec = 0; pos_rec = 0; - offset = 2*(ndef-1)+1; in_env = rfv } - -let init_fix ndef pos_rec arity rfv = - { nb_stack = arity; in_stack = add_param arity 0 []; - nb_rec = ndef; pos_rec = pos_rec; - offset = 2 * (ndef - pos_rec - 1)+1; in_env = rfv} +(*i Compilation of variables *) let find_at el l = let rec aux n = function | [] -> raise Not_found @@ -87,24 +196,27 @@ let pos_named id r = let pos_rel i r sz = if i <= r.nb_stack then Kacc(sz - (List.nth r.in_stack (i-1))) - else if i <= r.nb_stack + r.nb_rec - then Koffsetclosure (2 * (r.nb_rec + r.nb_stack - r.pos_rec - i)) - else - let db = FVrel(i - r.nb_stack - r.nb_rec) in - let env = !(r.in_env) in - try Kenvacc(r.offset + env.size - (find_at db env.fv_rev)) - with Not_found -> - let pos = env.size in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; - Kenvacc(r.offset + pos) - + else + let i = i - r.nb_stack in + if i <= r.nb_rec then + try List.nth r.pos_rec (i-1) + with _ -> assert false + else + let i = i - r.nb_rec in + let db = FVrel(i) in + let env = !(r.in_env) in + try Kenvacc(r.offset + env.size - (find_at db env.fv_rev)) + with Not_found -> + let pos = env.size in + r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + Kenvacc(r.offset + pos) (*i Examination of the continuation *) -(* Discard all instructions up to the next label. - This function is to be applied to the continuation before adding a - non-terminating instruction (branch, raise, return, appterm) - in front of it. *) +(* Discard all instructions up to the next label. *) +(* This function is to be applied to the continuation before adding a *) +(* non-terminating instruction (branch, raise, return, appterm) *) +(* in front of it. *) let rec discard_dead_code cont = cont (*function @@ -113,9 +225,9 @@ let rec discard_dead_code cont = cont | _ :: cont -> discard_dead_code cont *) -(* Return a label to the beginning of the given continuation. - If the sequence starts with a branch, use the target of that branch - as the label, thus avoiding a jump to a jump. *) +(* Return a label to the beginning of the given continuation. *) +(* If the sequence starts with a branch, use the target of that branch *) +(* as the label, thus avoiding a jump to a jump. *) let label_code = function | Klabel lbl :: _ as cont -> (lbl, cont) @@ -138,7 +250,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation ****) +(* Extention of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function @@ -150,15 +262,41 @@ let add_grab arity lbl cont = if arity = 1 then Klabel lbl :: cont else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont - -(* Environnement global *****) +let add_grabrec rec_arg arity lbl cont = + if arity = 1 then + Klabel lbl :: Kgrabrec 0 :: Krestart :: cont + else + Krestart :: Klabel lbl :: Kgrabrec rec_arg :: + Krestart :: Kgrab (arity - 1) :: cont + +(* continuation of a cofix *) + +let cont_cofix arity = + (* accu = res *) + (* stk = ai::args::ra::... *) + (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *) + [ Kpush; + Kpush; (* stk = res::res::ai::args::ra::... *) + Kacc 2; + Kfield 1; + Kfield 0; + Kmakeblock(2, cofix_evaluated_tag); + Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*) + Kacc 2; + Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *) + (* stk = res::ai::args::ra::... *) + Kacc 0; (* accu = res *) + Kreturn (arity+2) ] + + +(*i Global environment global *) let global_env = ref empty_env let set_global_env env = global_env := env -(* Code des fermetures ****) +(* Code des fermetures *) let fun_code = ref [] let init_fun_code () = fun_code := [] @@ -259,6 +397,14 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont +let rec compile_fv reloc l sz cont = + match l with + | [] -> cont + | [fvn] -> compile_fv_elem reloc fvn sz cont + | fvn :: tl -> + compile_fv_elem reloc fvn sz + (Kpush :: compile_fv reloc tl (sz + 1) cont) + (* compilation des constantes *) let rec get_allias env kn = @@ -271,8 +417,8 @@ let rec get_allias env kn = let rec compile_constr reloc c sz cont = match kind_of_term c with - | Meta _ -> raise (Invalid_argument "Cbytegen.gen_lam : Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.gen_lam : Evar") + | Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta") + | Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar") | Cast(c,_,_) -> compile_constr reloc c sz cont @@ -294,7 +440,7 @@ let rec compile_constr reloc c sz cont = | Lambda _ -> let params, body = decompose_lam c in let arity = List.length params in - let r_fun = init_fun arity in + let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in let cont_fun = compile_constr r_fun body arity [Kreturn arity] in @@ -314,11 +460,11 @@ let rec compile_constr reloc c sz cont = let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in (* Compilation des types *) - let rtype = init_type ndef rfv in + let env_type = comp_env_type rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code - (compile_constr rtype type_bodies.(i) 0 [Kstop]) in + (compile_constr env_type type_bodies.(i) 0 [Kstop]) in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -326,18 +472,12 @@ let rec compile_constr reloc c sz cont = for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in - let rbody = init_fix ndef i arity rfv in + let env_body = comp_env_fix ndef i arity rfv in let cont1 = - compile_constr rbody body arity [Kreturn arity] in + compile_constr env_body body arity [Kreturn arity] in let lbl = Label.create () in lbl_bodies.(i) <- lbl; - let fcode = - if arity = 1 then - Klabel lbl :: Kgrabrec 0 :: Krestart :: cont1 - else - Krestart :: Klabel lbl :: Kgrabrec rec_args.(i) :: - Krestart :: Kgrab (arity - 1) :: cont1 - in + let fcode = add_grabrec rec_args.(i) arity lbl cont1 in fun_code := [Ksequence(fcode,!fun_code)] done; let fv = !rfv in @@ -346,15 +486,15 @@ let rec compile_constr reloc c sz cont = | CoFix(init,(_,type_bodies,rec_bodies)) -> let ndef = Array.length type_bodies in - let rfv = ref empty_fv in let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in (* Compilation des types *) - let rtype = init_type ndef rfv in + let rfv = ref empty_fv in + let env_type = comp_env_type rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code - (compile_constr rtype type_bodies.(i) 0 [Kstop]) in + (compile_constr env_type type_bodies.(i) 0 [Kstop]) in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -362,21 +502,18 @@ let rec compile_constr reloc c sz cont = for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in - let rbody = init_fix ndef i arity rfv in + let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in - let cont1 = - compile_constr rbody body arity [Kreturn(arity)] in + compile_constr env_body body (arity+1) (cont_cofix arity) in let cont2 = - if arity <= 1 then cont1 else Kgrab (arity - 1) :: cont1 in - let cont3 = - Krestart :: Klabel lbl :: Kcograb arity :: Krestart :: cont2 in - fun_code := [Ksequence(cont3,!fun_code)]; - lbl_bodies.(i) <- lbl + add_grab (arity+1) lbl cont1 in + lbl_bodies.(i) <- lbl; + fun_code := [Ksequence(cont2,!fun_code)]; done; let fv = !rfv in compile_fv reloc fv.fv_rev sz - (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) + (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) | Case(ci,t,a,branchs) -> let ind = ci.ci_ind in @@ -418,12 +555,12 @@ let rec compile_constr reloc c sz cont = let lbl_b,code_b = label_code( if nargs = arity then - Kpushfield arity :: + Kpushfields arity :: compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in - Kpushfield arity :: + Kpushfields arity :: compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c)) in @@ -436,17 +573,8 @@ let rec compile_constr reloc c sz cont = | Klabel lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - let cont_a = if mib.mind_finite then code_sw else Kforce :: code_sw in - compile_constr reloc a sz cont_a - -and compile_fv reloc l sz cont = - match l with - | [] -> cont - | [fvn] -> compile_fv_elem reloc fvn sz cont - | fvn :: tl -> - compile_fv_elem reloc fvn sz - (Kpush :: compile_fv reloc tl (sz + 1) cont) - + compile_constr reloc a sz code_sw + and compile_str_cst reloc sc sz cont = match sc with | Bconstr c -> compile_constr reloc c sz cont @@ -465,9 +593,18 @@ let compile env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); - let reloc = empty () in + let reloc = empty_comp_env () in let init_code = compile_constr reloc c 0 [Kstop] in let fv = List.rev (!(reloc.in_env).fv_rev) in +(* draw_instr init_code; + draw_instr !fun_code; + Format.print_string "fv = "; + List.iter (fun v -> + match v with + | FVnamed id -> Format.print_string ((string_of_id id)^"; ") + | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format + .print_string "\n"; + Format.print_flush(); *) init_code,!fun_code, Array.of_list fv let compile_constant_body env body opaque boxed = diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index cccb18443..71a9aa0eb 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -149,8 +149,6 @@ let emit_instr = function out opGRAB; out_int n | Kgrabrec(rec_arg) -> out opGRABREC; out_int rec_arg - | Kcograb n -> - out opCOGRAB; out_int n | Kclosure(lbl, n) -> out opCLOSURE; out_int n; out_label lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> @@ -160,6 +158,13 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_types; let org = !out_position in Array.iter (out_label_with_orig org) lbl_bodies + | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> + out opCLOSURECOFIX;out_int (Array.length lbl_bodies); + out_int nfv; out_int init; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_types; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q | Kconst((Const_b0 i)) -> @@ -178,16 +183,20 @@ let emit_instr = function out opMAKESWITCHBLOCK; out_label typlbl; out_label swlbl; slot_for_annot annot;out_int sz - | Kforce -> - out opFORCE | Kswitch (tbl_const, tbl_block) -> out opSWITCH; out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block - | Kpushfield n -> - out opPUSHFIELD;out_int n + | Kpushfields n -> + out opPUSHFIELDS;out_int n + | Kfield n -> + if n <= 1 then out (opGETFIELD0+n) + else (out opGETFIELD;out_int n) + | Ksetfield n -> + if n <= 1 then out (opSETFIELD0+n) + else (out opSETFIELD;out_int n) | Kstop -> out opSTOP | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr") diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a6a605d2d..2e2bcafce 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -30,8 +30,8 @@ let lookup_mind_specif env (kn,tyi) = let find_rectype env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match kind_of_term t with - | Ind ind -> (ind, l) - | _ -> raise Not_found + | Ind ind -> (ind, l) + | _ -> raise Not_found let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 0f05ffc6b..deca20a6b 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -35,6 +35,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body val lookup_mind_specif : env -> inductive -> mind_specif (*s Functions to build standard types related to inductive *) +val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list val type_of_inductive : mind_specif -> types @@ -49,6 +50,7 @@ val arities_of_constructors : inductive -> mind_specif -> types array (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array + (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c63762f54..90317d531 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -131,7 +131,7 @@ let hcons_constant_body cb = let add_constant dir l decl senv = check_label l senv.labset; - let kn = make_con senv.modinfo.modpath dir l in + let kn = make_con senv.modinfo.modpath dir l in let cb = match decl with | ConstantEntry ce -> translate_constant senv.env kn ce diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 653f8978c..7115097e4 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -17,7 +17,7 @@ let val_of_constr env c = let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> nargs args1 = nargs args2 - | Zfix _, Zfix _ -> true + | Zfix(f1,args1), Zfix(f2,args2) -> nargs args1 = nargs args2 | Zswitch _, Zswitch _ -> true | _ , _ -> false @@ -42,8 +42,9 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let rec conv_val pb k v1 v2 cu = - if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu +let rec conv_val pb k v1 v2 cu = + if v1 == v2 then cu + else conv_whd pb k (whd_val v1) (whd_val v2) cu and conv_whd pb k whd1 whd2 cu = match whd1, whd2 with @@ -52,21 +53,14 @@ and conv_whd pb k whd1 whd2 cu = let cu = conv_val CONV k (dom p1) (dom p2) cu in conv_fun pb k (codom p1) (codom p2) cu | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu - | Vfix f1, Vfix f2 -> conv_fix k f1 f2 cu - | Vfix_app fa1, Vfix_app fa2 -> - let f1 = fix fa1 in - let args1 = args_of_fix fa1 in - let f2 = fix fa2 in - let args2 = args_of_fix fa2 in - conv_arguments k args1 args2 (conv_fix k f1 f2 cu) - | Vcofix cf1, Vcofix cf2 -> - conv_cofix k cf1 cf2 cu - | Vcofix_app cfa1, Vcofix_app cfa2 -> - let cf1 = cofix cfa1 in - let args1 = args_of_cofix cfa1 in - let cf2 = cofix cfa2 in - let args2 = args_of_cofix cfa2 in - conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) + | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu + | Vfix (f1,Some args1), Vfix(f2,Some args2) -> + if nargs args1 <> nargs args2 then raise NotConvertible + else conv_arguments k args1 args2 (conv_fix k f1 f2 cu) + | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu + | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) -> + if nargs args1 <> nargs args2 then raise NotConvertible + else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if i1 = i2 then cu else raise NotConvertible | Vconstr_block b1, Vconstr_block b2 -> @@ -111,8 +105,6 @@ and conv_atom pb k a1 stk1 a2 stk2 cu = conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu | _, Aiddef(ik2,v2) -> conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu - | Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ -> - Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work" | _, _ -> raise NotConvertible and conv_stack k stk1 stk2 cu = @@ -120,22 +112,17 @@ and conv_stack k stk1 stk2 cu = | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) - | Zfix fa1 :: stk1, Zfix fa2 :: stk2 -> - let f1 = fix fa1 in - let args1 = args_of_fix fa1 in - let f2 = fix fa2 in - let args2 = args_of_fix fa2 in + | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack k stk1 stk2 (conv_arguments k args1 args2 (conv_fix k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> - if eq_tbl sw1 sw2 then + if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in let rcu = ref (conv_val CONV k vt1 vt2 cu) in let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in for i = 0 to Array.length b1 - 1 do rcu := - conv_val CONV (k + fst b1.(i)) - (snd b1.(i)) (snd b2.(i)) !rcu + conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu done; conv_stack k stk1 stk2 !rcu else raise NotConvertible @@ -151,24 +138,20 @@ and conv_fix k f1 f2 cu = if f1 == f2 then cu else if check_fix f1 f2 then - let tf1 = types_of_fix f1 in - let tf2 = types_of_fix f2 in + let bf1, tf1 = reduce_fix k f1 in + let bf2, tf2 = reduce_fix k f2 in let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in - let bf1 = bodies_of_fix k f1 in - let bf2 = bodies_of_fix k f2 in - conv_vect (conv_fun CONV (k + (fix_ndef f1))) bf1 bf2 cu + conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu else raise NotConvertible and conv_cofix k cf1 cf2 cu = if cf1 == cf2 then cu else if check_cofix cf1 cf2 then - let tcf1 = types_of_cofix cf1 in - let tcf2 = types_of_cofix cf2 in + let bcf1, tcf1 = reduce_cofix k cf1 in + let bcf2, tcf2 = reduce_cofix k cf2 in let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in - let bcf1 = bodies_of_cofix k cf1 in - let bcf2 = bodies_of_cofix k cf2 in - conv_vect (conv_val CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu + conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible and conv_arguments k args1 args2 cu = @@ -255,302 +238,4 @@ let set_use_vm b = let use_vm _ = !use_vm -(*******************************************) -(* Calcul de la forme normal d'un terme *) -(*******************************************) - -let crazy_type = mkSet - -let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in - if name = Anonymous then (Name (id_of_string "x"),dom,codom) - else res - -exception Find_at of int - -(* rend le numero du constructeur correspondant au tag [tag], - [cst] = true si c'est un constructeur constant *) - -let invert_tag cst tag reloc_tbl = - try - for j = 0 to Array.length reloc_tbl - 1 do - let tagj,arity = reloc_tbl.(j) in - if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then - raise (Find_at j) - else () - done;raise Not_found - with Find_at j -> (j+1) - (* Argggg, ces constructeurs de ... qui commencent a 1*) - -(* Build the substitution that replaces Rels by the appropriate - inductives *) -let ind_subst mind mib = - let ntypes = mib.mind_ntypes in - let make_Ik k = mkInd (mind,ntypes-k-1) in - Util.list_tabulate make_Ik ntypes - -(* Instantiate inductives and parameters in constructor type - in normal form *) -let constructor_instantiate mind mib params ctyp = - let si = ind_subst mind mib in - let ctyp1 = substl si ctyp in - let nparams = Array.length params in - if nparams = 0 then ctyp1 - else - let _,ctyp2 = decompose_prod_n nparams ctyp1 in - let sp = List.rev (Array.to_list params) in substl sp ctyp2 - -let destApplication t = - try destApp t - with _ -> t,[||] - -let construct_of_constr_const env tag typ = - let cind,params = destApplication (whd_betadeltaiota env typ) in - let ind = destInd cind in - let (_,mip) = Inductive.lookup_mind_specif env ind in - let rtbl = mip.mind_reloc_tbl in - let i = invert_tag true tag rtbl in - mkApp(mkConstruct(ind,i), params) - -let find_rectype typ = - let cind,args = destApplication typ in - let ind = destInd cind in - ind, args - -let construct_of_constr_block env tag typ = - let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let nparams = mib.mind_nparams in - let rtbl = mip.mind_reloc_tbl in - let i = invert_tag false tag rtbl in - let params = Array.sub allargs 0 nparams in - let specif = mip.mind_nf_lc in - let ctyp = constructor_instantiate mind mib params specif.(i-1) in - (mkApp(mkConstruct(ind,i), params), ctyp) - -let constr_type_of_idkey env idkey = - match idkey with - | ConstKey cst -> - let ty = (lookup_constant cst env).const_type in - mkConst cst, ty - | VarKey id -> - let (_,_,ty) = lookup_named id env in - mkVar id, ty - | RelKey i -> - let n = (nb_rel env - i) in - let (_,_,ty) = lookup_rel n env in - mkRel n, lift n ty - -let type_of_ind env ind = - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif - -let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl = - (* [build_one_branch i cty] construit le type de la ieme branche (commence - a 0) et les lambda correspondant aux realargs *) - let build_one_branch i cty = - let typi = constructor_instantiate mind mib params cty in - let decl,indapp = Term.decompose_prod typi in - let ind,cargs = find_rectype indapp in - let nparams = Array.length params in - let carity = snd (rtbl.(i)) in - let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in - let codom = - let papp = mkApp(p,crealargs) in - if dep then - let cstr = ith_constructor_of_inductive ind (i+1) in - let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in - mkApp(papp,[|dep_cstr|]) - else papp - in - decl, codom - in Array.mapi build_one_branch mip.mind_nf_lc - -(* La fonction de normalisation *) - -let rec nf_val env v t = nf_whd env (whd_val v) t - -and nf_whd env whd typ = - match whd with - | Vsort s -> mkSort s - | Vprod p -> - let dom = nf_val env (dom p) crazy_type in - let name = Name (id_of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in - let codom = nf_val (push_rel (name,None,dom) env) vc crazy_type in - mkProd(name,dom,codom) - | Vfun f -> nf_fun env f typ - | Vfix f -> nf_fix env f - | Vfix_app fa -> - let f = fix fa in - let vargs = args_of_fix fa in - let fd = nf_fix env f in - let (_,i),(_,ta,_) = destFix fd in - let t = ta.(i) in - let _, args = nf_args env vargs t in - mkApp(fd,args) - | Vcofix cf -> nf_cofix env cf - | Vcofix_app cfa -> - let cf = cofix cfa in - let vargs = args_of_cofix cfa in - let cfd = nf_cofix env cf in - let i,(_,ta,_) = destCoFix cfd in - let t = ta.(i) in - let _, args = nf_args env vargs t in - mkApp(cfd,args) - | Vconstr_const n -> construct_of_constr_const env n typ - | Vconstr_block b -> - let capp,ctyp = construct_of_constr_block env (btag b) typ in - let args = nf_bargs env b ctyp in - mkApp(capp,args) - | Vatom_stk(Aid idkey, stk) -> - let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk - | Vatom_stk(Aiddef(idkey,v), stk) -> - nf_whd env (whd_stack v stk) typ - | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind) stk - | Vatom_stk(_,stk) -> assert false - -and nf_stk env c t stk = - match stk with - | [] -> c - | Zapp vargs :: stk -> - let t, args = nf_args env vargs t in - nf_stk env (mkApp(c,args)) t stk - | Zfix fa :: stk -> - let f = fix fa in - let vargs = args_of_fix fa in - let fd = nf_fix env f in - let (_,i),(_,ta,_) = destFix fd in - let tf = ta.(i) in - let typ, args = nf_args env vargs tf in - let _,_,codom = decompose_prod env typ in - nf_stk env (mkApp(mkApp(fd,args),[|c|])) (subst1 c codom) stk - | Zswitch sw :: stk -> - let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let nparams = mib.mind_nparams in - let params,realargs = Util.array_chop nparams allargs in - (* calcul du predicat du case, - [dep] indique si c'est un case dependant *) - let dep,p = - let dep = ref false in - let rec nf_predicate env v pT = - match whd_val v, kind_of_term pT with - | Vfun f, Prod _ -> - let k = nb_rel env in - let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env pT in - let body = - nf_predicate (push_rel (name,None,dom) env) vb codom in - mkLambda(name,dom,body) - | Vfun f, _ -> - dep := true; - let k = nb_rel env in - let vb = body_of_vfun k f in - let name = Name (id_of_string "c") in - let n = mip.mind_nrealargs in - let rargs = Array.init n (fun i -> mkRel (n-i)) in - let dom = mkApp(mkApp(mkInd ind,params),rargs) in - let body = - nf_val (push_rel (name,None,dom) env) vb crazy_type in - mkLambda(name,dom,body) - | _, _ -> nf_val env v crazy_type - in - let aux = - nf_predicate env (type_of_switch sw) - (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params)) - in - !dep,aux in - (* Calcul du type des branches *) - let btypes = - build_branches_type ind mib mip params dep p mip.mind_reloc_tbl in - (* calcul des branches *) - let bsw = branch_of_switch (nb_rel env) sw in - let mkbranch i (n,v) = - let decl,codom = btypes.(i) in - let env = - List.fold_right - (fun (name,t) env -> push_rel (name,None,t) env) decl env in - let b = nf_val env v codom in - compose_lam decl b - in - let branchs = Array.mapi mkbranch bsw in - let tcase = - if dep then mkApp(mkApp(p, params), [|c|]) - else mkApp(p, params) - in - let ci = case_info sw in - nf_stk env (mkCase(ci, p, c, branchs)) tcase stk - -and nf_args env vargs t = - let t = ref t in - let len = nargs vargs in - let targs = - Array.init len - (fun i -> - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (arg vargs i) dom in - t := subst1 c codom; c) in - !t,targs - -and nf_bargs env b t = - let t = ref t in - let len = bsize b in - let args = Array.create len crazy_type in - for i = 0 to len - 1 do - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in - args.(i) <- c; - t := subst1 c codom - done; - args -(* Array.init len - (fun i -> - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in - t := subst1 c codom; c) *) - -and nf_fun env f typ = - let k = nb_rel env in - let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env typ in - let body = nf_val (push_rel (name,None,dom) env) vb codom in - mkLambda(name,dom,body) - -and nf_fix env f = - let init = fix_init f in - let rec_args = rec_args f in - let ndef = fix_ndef f in - let vt = types_of_fix f in - let ft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in - let k = nb_rel env in - let vb = bodies_of_fix k f in - let env = push_rec_types (name,ft,ft) env in - let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in - mkFix ((rec_args,init),(name,ft,fb)) - -and nf_cofix env cf = - let init = cofix_init cf in - let ndef = cofix_ndef cf in - let vt = types_of_cofix cf in - let cft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in - let k = nb_rel env in - let vb = bodies_of_cofix k cf in - let env = push_rec_types (name,cft,cft) env in - let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in - mkCoFix (init,(name,cft,cfb)) - -let cbv_vm env c t = - let transp = transp_values () in - if not transp then set_transp_values true; - let v = val_of_constr env c in - let c = nf_val env v t in - if not transp then set_transp_values false; - c - diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 4aed5d05f..551615aa5 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,28 +19,5 @@ val use_vm : unit -> bool val set_use_vm : bool -> unit val vconv : conv_pb -> types conversion_function -(***********************************************************************) -(*s Reduction functions *) -val cbv_vm : env -> constr -> types -> constr - - - - - -val nf_val : env -> values -> types -> constr - -val nf_whd : env -> Vm.whd -> types -> constr - -val nf_stk : env -> constr -> types -> Vm.stack -> constr - -val nf_args : env -> Vm.arguments -> types -> types * constr array - -val nf_bargs : env -> Vm.vblock -> types -> constr array - -val nf_fun : env -> Vm.vfun -> types -> constr - -val nf_fix : env -> Vm.vfix -> constr - -val nf_cofix : env -> Vm.vcofix -> constr +val val_of_constr : env -> constr -> values - diff --git a/kernel/vm.ml b/kernel/vm.ml index c8be979e0..8fd8af74e 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,20 +1,16 @@ -open Obj open Names open Term open Conv_oracle open Cbytecodes - external set_drawinstr : unit -> unit = "coq_set_drawinstr" (******************************************) (* Fonctions en plus du module Obj ********) (******************************************) -external offset_closure : t -> int -> t = "coq_offset_closure" -external offset : t -> int = "coq_offset" -let first o = (offset_closure o (offset o)) -let last o = (field o (size o - 1)) +external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" +external offset : Obj.t -> int = "coq_offset" let accu_tag = 0 @@ -34,8 +30,10 @@ external set_transp_values : bool -> unit = "coq_set_transp_value" (*******************************************) type tcode -let tcode_of_obj v = ((obj v):tcode) -let fun_code v = tcode_of_obj (field (repr v) 0) +let tcode_of_obj v = ((Obj.obj v):tcode) +let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) + + external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" @@ -63,155 +61,26 @@ let popstop_code i = end let stop = popstop_code 0 - + (******************************************************) (* Types de donnees abstraites et fonctions associees *) (******************************************************) (* Values of the abstract machine *) -let val_of_obj v = ((obj v):values) -let crasy_val = (val_of_obj (repr 0)) - - -(* Functions *) -type vfun -(* v = [Tc | c | fv1 | ... | fvn ] *) -(* ^ *) -(* [Tc | (Restart : c) | v | a1 | ... an] *) -(* ^ *) +let val_of_obj v = ((Obj.obj v):values) +let crasy_val = (val_of_obj (Obj.repr 0)) -(* Products *) +(* Abstract data *) type vprod -(* [0 | dom : codom] *) -(* ^ *) -let dom : vprod -> values = fun p -> val_of_obj (field (repr p) 0) -let codom : vprod -> vfun = fun p -> (obj (field (repr p) 1)) - -(* Arguments *) -type arguments -(* arguments = [_ | _ | _ | a1 | ... | an] *) -(* ^ *) -let nargs : arguments -> int = fun args -> (size (repr args)) - 2 - -let unsafe_arg : arguments -> int -> values = - fun args i -> val_of_obj (field (repr args) (i+2)) - -let arg args i = - if 0 <= i && i < (nargs args) then unsafe_arg args i - else raise (Invalid_argument - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i))) - -(* Fixpoints *) +type vfun type vfix +type vcofix +type vblock +type arguments -(* [Tc|c0|Ti|c1|...|Ti|cn|fv1|...|fvn| [ct0|...|ctn]] *) -(* ^ *) -type vfix_block - -let fix_init : vfix -> int = fun vf -> (offset (repr vf)/2) - -let block_of_fix : vfix -> vfix_block = fun vf -> obj (first (repr vf)) - -let fix_block_type : vfix_block -> tcode array = - fun fb -> (obj (last (repr fb))) - -let fix_block_ndef : vfix_block -> int = - fun fb -> size (last (repr fb)) - -let fix_ndef vf = fix_block_ndef (block_of_fix vf) - -let unsafe_fb_code : vfix_block -> int -> tcode = - fun fb i -> tcode_of_obj (field (repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = block_of_fix vf in - let size = fix_block_ndef fb in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = fix_init f1, fix_init f2 in - (* Verification du point de depart *) - if i1 = i2 then - let fb1,fb2 = block_of_fix f1, block_of_fix f2 in - let n = fix_block_ndef fb1 in - (* Verification du nombre de definition *) - if n = fix_block_ndef fb2 then - (* Verification des arguments recursifs *) - try - for i = 0 to n - 1 do - if not (unsafe_rec_arg fb1 i = unsafe_rec_arg fb2 i) then - raise FALSE - done; - true - with FALSE -> false - else false - else false - -(* Partials applications of Fixpoints *) -type vfix_app -let fix : vfix_app -> vfix = - fun vfa -> ((obj (field (repr vfa) 1)):vfix) -let args_of_fix : vfix_app -> arguments = - fun vfa -> ((magic vfa) : arguments) - -(* CoFixpoints *) -type vcofix -type vcofix_block -let cofix_init : vcofix -> int = fun vcf -> (offset (repr vcf)/2) - -let block_of_cofix : vcofix -> vcofix_block = fun vcf -> obj (first (repr vcf)) - -let cofix_block_ndef : vcofix_block -> int = - fun fb -> size (last (repr fb)) - -let cofix_ndef vcf= cofix_block_ndef (block_of_cofix vcf) - -let cofix_block_type : vcofix_block -> tcode array = - fun cfb -> (obj (last (repr cfb))) - -let check_cofix cf1 cf2 = - cofix_init cf1 = cofix_init cf2 && - cofix_ndef cf1 = cofix_ndef cf2 - -let cofix_arity c = int_tcode c 1 - -let unsafe_cfb_code : vcofix_block -> int -> tcode = - fun cfb i -> tcode_of_obj (field (repr cfb) (2 * i)) - -(* Partials applications of CoFixpoints *) -type vcofix_app -let cofix : vcofix_app -> vcofix = - fun vcfa -> ((obj (field (repr vcfa) 1)):vcofix) -let args_of_cofix : vcofix_app -> arguments = - fun vcfa -> ((magic vcfa) : arguments) - -(* Blocks *) -type vblock (* la representation Ocaml *) -let btag : vblock -> int = fun b -> tag (repr b) -let bsize : vblock -> int = fun b -> size (repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then - val_of_obj (field (repr b) i) - else raise (Invalid_argument "Vm.bfield") - -(* Accumulators and atoms *) - -type accumulator -(* [Ta | accumulate | at | a1 | ... | an ] *) - -type inv_rel_key = int - -type id_key = inv_rel_key tableKey - +type vm_env type vstack = values array -type vm_env - type vswitch = { sw_type_code : tcode; sw_code : tcode; @@ -220,138 +89,148 @@ type vswitch = { sw_env : vm_env } -(* Ne pas changer ce type sans modifier le code C *) +(* Representation des types abstraits: *) +(* + Les produits : *) +(* - vprod = 0_[ dom | codom] *) +(* dom : values, codom : vfun *) +(* *) +(* + Les fonctions ont deux representations possibles : *) +(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *) +(* C:tcode, fvi : values *) +(* Remarque : il n'y a pas de difference entre la fct et son *) +(* environnement. *) +(* - Application partielle : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* *) +(* + Les points fixes : *) +(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* Remarque il n'y a qu'un seul block pour representer tout les *) +(* points fixes d'une declaration mutuelle, chaque point fixe *) +(* pointe sur la position de son code dans le block. *) +(* - L'application partielle d'un point fixe suit le meme schema *) +(* que celui des fonctions *) +(* Remarque seul les points fixes qui n'ont pas encore recu leur *) +(* argument recursif sont encode de cette maniere (si l'argument *) +(* recursif etait un constructeur le point fixe se serait reduit *) +(* sinon il est represente par un accumulateur) *) +(* *) +(* + Les cofix sont expliques dans cbytegen.ml *) +(* *) +(* + Les vblock encodent les constructeurs (non constant) de caml, *) +(* la difference est que leur tag commence a 1 (0 est reserve pour les *) +(* accumulateurs : accu_tag) *) +(* *) +(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *) +(* *) +(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation des [accu] : tag_[....] *) +(* -- tag <= 2 : encodage du type atom *) +(* -- 3_[accu|fix_app] : un point fixe bloque par un accu *) +(* -- 4_[accu|vswitch] : un case bloque par un accu *) +(* -- 5_[fcofix] : une fonction de cofix *) +(* -- 6_[fcofix|val] : une fonction de cofix, val represente *) +(* la valeur de la reduction de la fct applique a arg1 ... argn *) +(* Le type [arguments] est utiliser de maniere abstraite comme un *) +(* tableau, il represente la structure de donnee suivante : *) +(* tag[ _ | _ |v1|... | vn] *) +(* Generalement le 1er champs est un pointeur de code *) + +(* Ne pas changer ce type sans modifier le code C, *) +(* en particulier le fichier "coq_values.h" *) type atom = | Aid of id_key | Aiddef of id_key * values | Aind of inductive - | Afix_app of accumulator * vfix_app - | Aswitch of accumulator * vswitch - -let atom_of_accu : accumulator -> atom = - fun a -> ((obj (field (repr a) 1)) : atom) - -let args_of_accu : accumulator -> arguments = - fun a -> ((magic a) : arguments) - -let nargs_of_accu a = nargs (args_of_accu a) (* Les zippers *) type zipper = | Zapp of arguments - | Zfix of vfix_app + | Zfix of vfix*arguments (* Peut-etre vide *) | Zswitch of vswitch type stack = zipper list +type to_up = values + type whd = | Vsort of sorts | Vprod of vprod | Vfun of vfun - | Vfix of vfix - | Vfix_app of vfix_app - | Vcofix of vcofix - | Vcofix_app of vcofix_app + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack -(* Les atomes sont forcement Aid Aiddef Aind *) - -(**********************************************) -(* Constructeurs ******************************) -(**********************************************) -(* obj_of_atom : atom -> t *) -let obj_of_atom : atom -> t = - fun a -> - let res = Obj.new_block accu_tag 2 in - set_field res 0 (repr accumulate); - set_field res 1 (repr a); - res - -(* obj_of_str_const : structured_constant -> t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_b0 tag -> repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = new_block tag len in - for i = 0 to len - 1 do - set_field res i (obj_of_str_const args.(i)) - done; - res - -let val_of_obj o = ((obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let idkey_tbl = Hashtbl.create 31 - -let val_of_idkey key = - try Hashtbl.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - Hashtbl.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) -let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) - -let val_of_named id = val_of_idkey (VarKey id) -let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) - -let val_of_constant c = val_of_idkey (ConstKey c) -let val_of_constant_def n c v = - let res = Obj.new_block accu_tag 2 in - set_field res 0 (repr (mkAccuCond n)); - set_field res 1 (repr (Aiddef(ConstKey c, v))); - val_of_obj res - - (*************************************************) (* Destructors ***********************************) (*************************************************) - let rec whd_accu a stk = let stk = - if nargs_of_accu a = 0 then stk - else Zapp (args_of_accu a) :: stk in - let at = atom_of_accu a in - match at with - | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk) - | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk) - | Aswitch(a,sw) -> whd_accu a (Zswitch sw :: stk) + if Obj.size a = 2 then stk + else Zapp (Obj.obj a) :: stk in + let at = Obj.field a 1 in + match Obj.tag at with + | i when i <= 2 -> + Vatom_stk(Obj.magic at, stk) + | 3 (* fix_app tag *) -> + let fa = Obj.field at 1 in + let zfix = + Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + whd_accu (Obj.field at 0) (zfix :: stk) + | 4 (* switch tag *) -> + let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in + whd_accu (Obj.field at 0) (zswitch :: stk) + | 5 (* cofix_tag *) -> + begin match stk with + | [] -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + Vcofix(vcfx, to_up, None) + | [Zapp args] -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + Vcofix(vcfx, to_up, Some args) + | _ -> assert false + end + | 6 (* cofix_evaluated_tag *) -> + begin match stk with + | [] -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + Vcofix(vcofix, res, None) + | [Zapp args] -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + Vcofix(vcofix, res, Some args) + | _ -> assert false + end + | _ -> assert false -external kind_of_closure : t -> int = "coq_kind_of_closure" +external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" let whd_val : values -> whd = fun v -> - let o = repr v in - if is_int o then Vconstr_const (obj o) + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) else - let tag = tag o in + let tag = Obj.tag o in if tag = accu_tag then - if is_accumulate (fun_code o) then whd_accu (obj o) [] + ( + if Obj.size o = 1 then Obj.obj o (* sort *) else - if size o = 1 then Vsort(obj (field o 0)) - else Vprod(obj o) + if is_accumulate (fun_code o) then whd_accu o [] + else (Vprod(Obj.obj o))) else - if tag = closure_tag || tag = infix_tag then - match kind_of_closure o with - | 0 -> Vfun(obj o) - | 1 -> Vfix(obj o) - | 2 -> Vfix_app(obj o) - | 3 -> Vcofix(obj o) - | 4 -> Vcofix_app(obj o) - | 5 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work" - else Vconstr_block(obj o) + if tag = Obj.closure_tag || tag = Obj.infix_tag then + ( match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work") + else Vconstr_block(Obj.obj o) @@ -359,7 +238,6 @@ let whd_val : values -> whd = (* La machine abstraite *************************) (************************************************) - (* gestion de la pile *) external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" @@ -371,6 +249,17 @@ external push_vstack : vstack -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" + + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else raise (Invalid_argument + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i))) + let apply_arguments vf vargs = let n = nargs vargs in if n = 0 then vf @@ -378,7 +267,7 @@ let apply_arguments vf vargs = begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (magic vf) (n - 1) + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end let apply_vstack vf vstk = @@ -388,80 +277,130 @@ let apply_vstack vf vstk = begin push_ra stop; push_vstack vstk; - interprete (fun_code vf) vf (magic vf) (n - 1) + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end -let apply_fix_app vfa arg = - let vf = fix vfa in - let vargs = args_of_fix vfa in - push_ra stop; - push_val arg; - push_arguments vargs; - interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs) - -external set_forcable : unit -> unit = "coq_set_forcable" -let force_cofix v = - match whd_val v with - | Vcofix _ | Vcofix_app _ -> - push_ra stop; - set_forcable (); - interprete (fun_code v) (magic v) (magic v) 0 - | _ -> v - -let apply_switch sw arg = - let arg = force_cofix arg in - let tc = sw.sw_annot.tailcall in - if tc then - (push_ra stop;push_vstack sw.sw_stk) - else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); - interprete sw.sw_code arg sw.sw_env 0 +(**********************************************) +(* Constructeurs ******************************) +(**********************************************) -let is_accu v = - is_block (repr v) && tag (repr v) = accu_tag && - fun_code v == accumulate +let obj_of_atom : atom -> Obj.t = + fun a -> + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr accumulate); + Obj.set_field res 1 (Obj.repr a); + res -let rec whd_stack v stk = - match stk with - | [] -> whd_val v - | Zapp a :: stkt -> whd_stack (apply_arguments v a) stkt - | Zfix fa :: stkt -> - if is_accu v then whd_accu (magic v) stk - else whd_stack (apply_fix_app fa v) stkt - | Zswitch sw :: stkt -> - if is_accu v then whd_accu (magic v) stk - else whd_stack (apply_switch sw v) stkt +(* obj_of_str_const : structured_constant -> Obj.t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> Obj.repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_b0 tag -> Obj.repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = Obj.new_block tag len in + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) + done; + res -let rec force_whd v stk = - match whd_stack v stk with - | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk - | res -> res +let val_of_obj o = ((Obj.obj o) : values) - +let val_of_str_const str = val_of_obj (obj_of_str_const str) -(* Function *) -external closure_arity : vfun -> int = "coq_closure_arity" +let val_of_atom a = val_of_obj (obj_of_atom a) + +let idkey_tbl = Hashtbl.create 31 + +let val_of_idkey key = + try Hashtbl.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + Hashtbl.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) +let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) + +let val_of_named id = val_of_idkey (VarKey id) +let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) + +let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_constant_def n c v = + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr (mkAccuCond n)); + Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v))); + val_of_obj res -(* [apply_rel v k arity] applique la valeurs [v] aux arguments - [k],[k+1], ... , [k+arity-1] *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) +(*************************************************) +(** Operations pour la manipulation des donnees **) +(*************************************************) + + +(* Functions over products *) + +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) + +(* Functions over vfun *) + +external closure_arity : vfun -> int = "coq_closure_arity" + let body_of_vfun k vf = let vargs = mkrel_vstack k 1 in - apply_vstack (magic vf) vargs + apply_vstack (Obj.magic vf) vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in - assert (0 <= arity && arity < Sys.max_array_length); + assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_vstack (magic vf1) vargs in - let v2 = apply_vstack (magic vf2) vargs in + let v1 = apply_vstack (Obj.magic vf1) vargs in + let v2 = apply_vstack (Obj.magic vf2) vargs in arity, v1, v2 - + +(* Functions over fixpoint *) + +let first o = (offset_closure o (offset o)) +let last o = (Obj.field o (Obj.size o - 1)) + +let current_fix vf = offset (Obj.repr vf) / 2 + +let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 -(* Fix *) +let rec_args vf = + let fb = first (Obj.repr vf) in + let size = Obj.size (last fb) in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = current_fix f1, current_fix f2 in + (* Verification du point de depart *) + if i1 = i2 then + let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in + let n = Obj.size (last fb1) in + (* Verification du nombre de definition *) + if n = Obj.size (last fb2) then + (* Verification des arguments recursifs *) + try + for i = 0 to n - 1 do + if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i + then raise FALSE + done; + true + with FALSE -> false + else false + else false + +(* Functions over vfix *) external atom_rel : unit -> atom array = "get_coq_atom_tbl" external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" @@ -486,69 +425,89 @@ let relaccu_code i = !relaccu_tbl.(i) end -let jump_grabrec c = offset_tcode c 2 -let jump_grabrecrestart c = offset_tcode c 3 - -let bodies_of_fix k vf = - let fb = block_of_fix vf in - let ndef = fix_block_ndef fb in +let reduce_fix k vf = + let fb = first (Obj.repr vf) in + (* calcul des types *) + let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let ndef = Array.length fc_typ in + let et = offset_closure fb (2*(ndef - 1)) in + let ftyp = + Array.map + (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in (* Construction de l' environnement des corps des points fixes *) - let e = dup (repr fb) in + let e = Obj.dup fb in for i = 0 to ndef - 1 do - set_field e (2 * i) (repr (relaccu_code (k + i))) + Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) done; let fix_body i = + let jump_grabrec c = offset_tcode c 2 in let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block closure_tag 2 in - set_field res 0 (repr c); - set_field res 1 (offset_closure e (2*i)); - ((obj res) : vfun) - in Array.init ndef fix_body - -let types_of_fix vf = - let fb = block_of_fix vf in - let type_code = fix_block_type fb in - let type_val c = interprete c crasy_val (magic fb) 0 in - Array.map type_val type_code - + let res = Obj.new_block Obj.closure_tag 2 in + Obj.set_field res 0 (Obj.repr c); + Obj.set_field res 1 (offset_closure e (2*i)); + ((Obj.obj res) : vfun) in + (Array.init ndef fix_body, ftyp) -(* CoFix *) -let jump_cograb c = offset_tcode c 2 -let jump_cograbrestart c = offset_tcode c 3 - -let bodies_of_cofix k vcf = - let cfb = block_of_cofix vcf in - let ndef = cofix_block_ndef cfb in - (* Construction de l' environnement des corps des cofix *) - let e = dup (repr cfb) in +(* Functions over vcofix *) + +let get_fcofix vcf i = + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + | Vcofix(vcfi, _, _) -> vcfi + | _ -> assert false + +let current_cofix vcf = + let ndef = Obj.size (last (Obj.repr vcf)) in + let rec find_cofix pos = + if pos < ndef then + if get_fcofix vcf pos == vcf then pos + else find_cofix (pos+1) + else raise Not_found in + try find_cofix 0 + with _ -> assert false + +let check_cofix vcf1 vcf2 = + (current_cofix vcf1 = current_cofix vcf2) && + (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + +external print_point : Obj.t -> unit = "coq_print_pointer" + +let reduce_cofix k vcf = + let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let ndef = Array.length fc_typ in + let ftyp = + Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in + (* Construction de l'environnement des corps des cofix *) + + let max = k + ndef - 1 in + let e = Obj.dup (Obj.repr vcf) in for i = 0 to ndef - 1 do - set_field e (2 * i) (repr (relaccu_code (k + i))) + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) done; + let cofix_body i = - let c = unsafe_cfb_code cfb i in - let arity = int_tcode c 1 in - if arity = 0 then - begin - push_ra stop; - interprete (jump_cograbrestart c) crasy_val - (obj (offset_closure e (2*i))) 0 - end - else - let res = Obj.new_block closure_tag 2 in - set_field res 0 (repr (jump_cograb c)); - set_field res 1 (offset_closure e (2*i)); - ((obj res) : values) - in Array.init ndef cofix_body - -let types_of_cofix vcf = - let cfb = block_of_cofix vcf in - let type_code = cofix_block_type cfb in - let type_val c = interprete c crasy_val (magic cfb) 0 in - Array.map type_val type_code - -(* Switch *) - -let eq_tbl sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + let vcfi = get_fcofix vcf i in + let c = Obj.field (Obj.repr vcfi) 0 in + Obj.set_field e 0 c; + let atom = Obj.new_block cofix_tag 1 in + let self = Obj.new_block accu_tag 2 in + Obj.set_field self 0 (Obj.repr accumulate); + Obj.set_field self 1 (Obj.repr atom); + apply_vstack (Obj.obj e) [|Obj.obj self|] in + (Array.init ndef cofix_body, ftyp) + + +(* Functions over vblock *) + +let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) +let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) + else raise (Invalid_argument "Vm.bfield") + + +(* Functions over vswitch *) + +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci @@ -557,15 +516,22 @@ let type_of_switch sw = interprete sw.sw_type_code crasy_val sw.sw_env 0 let branch_arg k (tag,arity) = - if arity = 0 then ((magic tag):values) + if arity = 0 then ((Obj.magic tag):values) else - let b = new_block tag arity in + let b = Obj.new_block tag arity in for i = 0 to arity - 1 do - set_field b i (repr (val_of_rel (k+i))) + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) done; val_of_obj b - - + +let apply_switch sw arg = + let tc = sw.sw_annot.tailcall in + if tc then + (push_ra stop;push_vstack sw.sw_stk) + else + (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + interprete sw.sw_code arg sw.sw_env 0 + let branch_of_switch k sw = let eval_branch (_,arity as ta) = let arg = branch_arg k ta in @@ -573,27 +539,62 @@ let branch_of_switch k sw = (arity, v) in Array.map eval_branch sw.sw_annot.rtbl - - - - - - - - - - - - - - - - + +(* Evaluation *) +let is_accu v = + let o = Obj.repr v in + Obj.is_block o && Obj.tag o = accu_tag && + fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag +let rec whd_stack v stk = + match stk with + | [] -> whd_val v + | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt + | Zfix (f,args) :: stkt -> + let o = Obj.repr v in + if Obj.is_block o && Obj.tag o = accu_tag then + whd_accu (Obj.repr v) stk + else + let v', stkt = + match stkt with + | Zapp args' :: stkt -> + push_ra stop; + push_arguments args'; + push_val v; + push_arguments args; + let v' = + interprete (fun_code f) (Obj.magic f) (Obj.magic f) + (nargs args+ nargs args') in + v', stkt + | _ -> + push_ra stop; + push_val v; + push_arguments args; + let v' = + interprete (fun_code f) (Obj.magic f) (Obj.magic f) + (nargs args) in + v', stkt + in + whd_stack v' stkt + | Zswitch sw :: stkt -> + let o = Obj.repr v in + if Obj.is_block o && Obj.tag o = accu_tag then + if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk + else + let to_up = + match whd_accu (Obj.repr v) [] with + | Vcofix (_, to_up, _) -> to_up + | _ -> assert false in + whd_stack (apply_switch sw to_up) stkt + else whd_stack (apply_switch sw v) stkt +let rec force_whd v stk = + match whd_stack v stk with + | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk + | res -> res diff --git a/kernel/vm.mli b/kernel/vm.mli index b5fd9b9db..279ac9370 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -13,45 +13,41 @@ type tcode (* Les valeurs ***********) -type accumulator type vprod type vfun type vfix -type vfix_app type vcofix -type vcofix_app type vblock type vswitch type arguments +type atom = + | Aid of id_key + | Aiddef of id_key * values + | Aind of inductive + +(* Les zippers *) + type zipper = | Zapp of arguments - | Zfix of vfix_app + | Zfix of vfix*arguments (* Peut-etre vide *) | Zswitch of vswitch type stack = zipper list - -type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive - | Afix_app of accumulator * vfix_app - | Aswitch of accumulator * vswitch +type to_up type whd = | Vsort of sorts | Vprod of vprod | Vfun of vfun - | Vfix of vfix - | Vfix_app of vfix_app - | Vcofix of vcofix - | Vcofix_app of vcofix_app + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack - -(* Constructors *) + +(** Constructors *) val val_of_str_const : structured_constant -> values val val_of_rel : int -> values @@ -63,44 +59,43 @@ val val_of_named_def : identifier -> values -> values val val_of_constant : constant -> values val val_of_constant_def : int -> constant -> values -> values -(* Destructors *) +(** Destructors *) val whd_val : values -> whd +(* Arguments *) +val nargs : arguments -> int +val arg : arguments -> int -> values + (* Product *) val dom : vprod -> values val codom : vprod -> vfun + (* Function *) val body_of_vfun : int -> vfun -> values val decompose_vfun2 : int -> vfun -> vfun -> int * values * values + (* Fix *) -val fix : vfix_app -> vfix -val args_of_fix : vfix_app -> arguments -val fix_init : vfix -> int -val fix_ndef : vfix -> int -val rec_args : vfix -> int array +val current_fix : vfix -> int val check_fix : vfix -> vfix -> bool -val bodies_of_fix : int -> vfix -> vfun array -val types_of_fix : vfix -> values array +val rec_args : vfix -> int array +val reduce_fix : int -> vfix -> vfun array * values array + (* bodies , types *) + (* CoFix *) -val cofix : vcofix_app -> vcofix -val args_of_cofix : vcofix_app -> arguments -val cofix_init : vcofix -> int -val cofix_ndef : vcofix -> int +val current_cofix : vcofix -> int val check_cofix : vcofix -> vcofix -> bool -val bodies_of_cofix : int -> vcofix -> values array -val types_of_cofix : vcofix -> values array +val reduce_cofix : int -> vcofix -> values array * values array + (* bodies , types *) (* Block *) val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values + (* Switch *) -val eq_tbl : vswitch -> vswitch -> bool +val check_switch : vswitch -> vswitch -> bool val case_info : vswitch -> case_info val type_of_switch : vswitch -> values val branch_of_switch : int -> vswitch -> (int * values) array -(* Arguments *) -val nargs : arguments -> int -val arg : arguments -> int -> values (* Evaluation *) val whd_stack : values -> stack -> whd diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 641abe2f7..9c8632a6d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -155,8 +155,14 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ] + [ c1 = operconstr; "<:"; c2 = binder_constr -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; "<:"; c2 = SELF -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; ":";c2 = binder_constr -> + CCast(loc,c1, CastConv DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> + CCast(loc,c1, CastConv DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 92b07e08b..ea4a26308 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -566,8 +566,9 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_rawsort s, latom - | CCast (_,a,_,b) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), + | CCast (_,a,k,b) -> + let s = match k with CastConv VMcast -> "<:" | _ -> ":" in + hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), lcast | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml new file mode 100644 index 000000000..fb05661d7 --- /dev/null +++ b/pretyping/vnorm.ml @@ -0,0 +1,271 @@ +open Names +open Declarations +open Term +open Environ +open Inductive +open Reduction +open Vm + +(*******************************************) +(* Calcul de la forme normal d'un terme *) +(*******************************************) + +let crazy_type = mkSet + +let decompose_prod env t = + let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + if name = Anonymous then (Name (id_of_string "x"),dom,codom) + else res + +exception Find_at of int + +(* rend le numero du constructeur correspondant au tag [tag], + [cst] = true si c'est un constructeur constant *) + +let invert_tag cst tag reloc_tbl = + try + for j = 0 to Array.length reloc_tbl - 1 do + let tagj,arity = reloc_tbl.(j) in + if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then + raise (Find_at j) + else () + done;raise Not_found + with Find_at j -> (j+1) + (* Argggg, ces constructeurs de ... qui commencent a 1*) + +let find_rectype_a env c = + let (t, l) = + let t = whd_betadeltaiota env c in + try destApp t with _ -> (t,[||]) in + match kind_of_term t with + | Ind ind -> (ind, l) + | _ -> raise Not_found + +(* Instantiate inductives and parameters in constructor type *) +let build_type_constructor mind mib params ctyp = + let si = ind_subst mind mib in + let ctyp1 = substl si ctyp in + let nparams = Array.length params in + if nparams = 0 then ctyp1 + else + let _,ctyp2 = decompose_prod_n nparams ctyp1 in + let sp = List.rev (Array.to_list params) in substl sp ctyp2 + +let construct_of_constr_const env tag typ = + let ind,params = find_rectype env typ in + let (_,mip) = lookup_mind_specif env ind in + let i = invert_tag true tag mip.mind_reloc_tbl in + applistc (mkConstruct(ind,i)) params + +let construct_of_constr_block env tag typ = + let (mind,_ as ind), allargs = find_rectype_a env typ in + let (mib,mip) = lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let i = invert_tag false tag mip.mind_reloc_tbl in + let params = Array.sub allargs 0 nparams in + let specif = mip.mind_nf_lc in + let ctyp = build_type_constructor mind mib params specif.(i-1) in + (mkApp(mkConstruct(ind,i), params), ctyp) + +let constr_type_of_idkey env idkey = + match idkey with + | ConstKey cst -> + mkConst cst, (lookup_constant cst env).const_type + | VarKey id -> + let (_,_,ty) = lookup_named id env in + mkVar id, ty + | RelKey i -> + let n = (nb_rel env - i) in + let (_,_,ty) = lookup_rel n env in + mkRel n, lift n ty + +let type_of_ind env ind = + type_of_inductive (Inductive.lookup_mind_specif env ind) + +let build_branches_type env (mind,_ as _ind) mib mip params dep p = + let rtbl = mip.mind_reloc_tbl in + (* [build_one_branch i cty] construit le type de la ieme branche (commence + a 0) et les lambda correspondant aux realargs *) + let build_one_branch i cty = + let typi = build_type_constructor mind mib params cty in + let decl,indapp = Term.decompose_prod typi in + let ind,cargs = find_rectype_a env indapp in + let nparams = Array.length params in + let carity = snd (rtbl.(i)) in + let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in + let codom = + let papp = mkApp(p,crealargs) in + if dep then + let cstr = ith_constructor_of_inductive ind (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in + mkApp(papp,[|dep_cstr|]) + else papp + in + decl, codom + in Array.mapi build_one_branch mip.mind_nf_lc + +let build_case_type dep p realargs c = + if dep then mkApp(mkApp(p, realargs), [|c|]) + else mkApp(p, realargs) + +(* La fonction de normalisation *) + +let rec nf_val env v t = nf_whd env (whd_val v) t + +and nf_vtype env v = nf_val env v crazy_type + +and nf_whd env whd typ = + match whd with + | Vsort s -> mkSort s + | Vprod p -> + let dom = nf_vtype env (dom p) in + let name = Name (id_of_string "x") in + let vc = body_of_vfun (nb_rel env) (codom p) in + let codom = nf_vtype (push_rel (name,None,dom) env) vc in + mkProd(name,dom,codom) + | Vfun f -> nf_fun env f typ + | Vfix(f,None) -> nf_fix env f + | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs) + | Vcofix(cf,_,None) -> nf_cofix env cf + | Vcofix(cf,_,Some vargs) -> + let cfd = nf_cofix env cf in + let i,(_,ta,_) = destCoFix cfd in + let t = ta.(i) in + let _, args = nf_args env vargs t in + mkApp(cfd,args) + | Vconstr_const n -> construct_of_constr_const env n typ + | Vconstr_block b -> + let capp,ctyp = construct_of_constr_block env (btag b) typ in + let args = nf_bargs env b ctyp in + mkApp(capp,args) + | Vatom_stk(Aid idkey, stk) -> + let c,typ = constr_type_of_idkey env idkey in + nf_stk env c typ stk + | Vatom_stk(Aiddef(idkey,v), stk) -> + nf_whd env (whd_stack v stk) typ + | Vatom_stk(Aind ind, stk) -> + nf_stk env (mkInd ind) (type_of_ind env ind) stk + +and nf_stk env c t stk = + match stk with + | [] -> c + | Zapp vargs :: stk -> + let t, args = nf_args env vargs t in + nf_stk env (mkApp(c,args)) t stk + | Zfix (f,vargs) :: stk -> + let fa, typ = nf_fix_app env f vargs in + let _,_,codom = decompose_prod env typ in + nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk + | Zswitch sw :: stk -> + let (mind,_ as ind),allargs = find_rectype_a env t in + let (mib,mip) = Inductive.lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let params,realargs = Util.array_chop nparams allargs in + let pT = + hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in + let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in + (* Calcul du type des branches *) + let btypes = build_branches_type env ind mib mip params dep p in + (* calcul des branches *) + let bsw = branch_of_switch (nb_rel env) sw in + let mkbranch i (n,v) = + let decl,codom = btypes.(i) in + let env = + List.fold_right + (fun (name,t) env -> push_rel (name,None,t) env) decl env in + let b = nf_val env v codom in + compose_lam decl b + in + let branchs = Array.mapi mkbranch bsw in + let tcase = build_case_type dep p realargs c in + let ci = case_info sw in + nf_stk env (mkCase(ci, p, c, branchs)) tcase stk + +and nf_predicate env ind mip params v pT = + match whd_val v, kind_of_term pT with + | Vfun f, Prod _ -> + let k = nb_rel env in + let vb = body_of_vfun k f in + let name,dom,codom = decompose_prod env pT in + let dep,body = + nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in + dep, mkLambda(name,dom,body) + | Vfun f, _ -> + let k = nb_rel env in + let vb = body_of_vfun k f in + let name = Name (id_of_string "c") in + let n = mip.mind_nrealargs in + let rargs = Array.init n (fun i -> mkRel (n-i)) in + let dom = mkApp(mkApp(mkInd ind,params),rargs) in + let body = nf_vtype (push_rel (name,None,dom) env) vb in + true, mkLambda(name,dom,body) + | _, _ -> false, nf_val env v crazy_type + +and nf_args env vargs t = + let t = ref t in + let len = nargs vargs in + let args = + Array.init len + (fun i -> + let _,dom,codom = decompose_prod env !t in + let c = nf_val env (arg vargs i) dom in + t := subst1 c codom; c) in + !t,args + +and nf_bargs env b t = + let t = ref t in + let len = bsize b in + let args = + Array.init len + (fun i -> + let _,dom,codom = decompose_prod env !t in + let c = nf_val env (bfield b i) dom in + t := subst1 c codom; c) in + args + +and nf_fun env f typ = + let k = nb_rel env in + let vb = body_of_vfun k f in + let name,dom,codom = decompose_prod env typ in + let body = nf_val (push_rel (name,None,dom) env) vb codom in + mkLambda(name,dom,body) + +and nf_fix env f = + let init = current_fix f in + let rec_args = rec_args f in + let k = nb_rel env in + let vb, vt = reduce_fix k f in + let ndef = Array.length vt in + let ft = Array.map (fun v -> nf_val env v crazy_type) vt in + let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in + let env = push_rec_types (name,ft,ft) env in + let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in + mkFix ((rec_args,init),(name,ft,fb)) + +and nf_fix_app env f vargs = + let fd = nf_fix env f in + let (_,i),(_,ta,_) = destFix fd in + let t = ta.(i) in + let t, args = nf_args env vargs t in + mkApp(fd,args),t + +and nf_cofix env cf = + let init = current_cofix cf in + let k = nb_rel env in + let vb,vt = reduce_cofix k cf in + let ndef = Array.length vt in + let cft = Array.map (fun v -> nf_val env v crazy_type) vt in + let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in + let env = push_rec_types (name,cft,cft) env in + let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in + mkCoFix (init,(name,cft,cfb)) + +let cbv_vm env c t = + let transp = transp_values () in + if not transp then set_transp_values true; + let v = Vconv.val_of_constr env c in + let c = nf_val env v t in + if not transp then set_transp_values false; + c + diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli new file mode 100644 index 000000000..2ea94bfb0 --- /dev/null +++ b/pretyping/vnorm.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i*) +open Names +open Term +open Environ +open Reduction +(*i*) + +(*s Reduction functions *) +val cbv_vm : env -> constr -> types -> constr + diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6f49ee735..c69d1be36 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open RedFlags (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in - Vconv.cbv_vm env c ctyp + Vnorm.cbv_vm env c ctyp let set_opaque_const sp = |