aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend372
-rw-r--r--Makefile4
-rw-r--r--dev/vm_printers.ml4
-rw-r--r--kernel/byterun/coq_fix_code.c30
-rw-r--r--kernel/byterun/coq_instruct.h14
-rw-r--r--kernel/byterun/coq_interp.c328
-rw-r--r--kernel/byterun/coq_memory.c7
-rw-r--r--kernel/byterun/coq_memory.h1
-rw-r--r--kernel/byterun/coq_values.c3
-rw-r--r--kernel/byterun/coq_values.h13
-rw-r--r--kernel/cbytecodes.ml31
-rw-r--r--kernel/cbytecodes.mli18
-rw-r--r--kernel/cbytegen.ml347
-rw-r--r--kernel/cemitcodes.ml21
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/vconv.ml357
-rw-r--r--kernel/vconv.mli25
-rw-r--r--kernel/vm.ml749
-rw-r--r--kernel/vm.mli65
-rw-r--r--parsing/g_constr.ml410
-rw-r--r--parsing/ppconstr.ml5
-rw-r--r--pretyping/vnorm.ml271
-rw-r--r--pretyping/vnorm.mli18
-rw-r--r--proofs/redexpr.ml2
26 files changed, 1463 insertions, 1240 deletions
diff --git a/.depend b/.depend
index f762207f5..04f8de6db 100644
--- a/.depend
+++ b/.depend
@@ -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
diff --git a/Makefile b/Makefile
index a12559090..2aa10f5c6 100644
--- a/Makefile
+++ b/Makefile
@@ -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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 10:08:39 +0000