aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend187
-rw-r--r--contrib/extraction/common.ml73
-rw-r--r--contrib/extraction/common.mli4
-rw-r--r--contrib/extraction/extract_env.ml23
-rw-r--r--contrib/extraction/extraction.ml351
-rw-r--r--contrib/extraction/extraction.mli9
-rw-r--r--contrib/extraction/haskell.ml56
-rw-r--r--contrib/extraction/miniml.mli39
-rw-r--r--contrib/extraction/mlutil.ml23
-rw-r--r--contrib/extraction/ocaml.ml121
-rw-r--r--contrib/extraction/table.ml146
-rw-r--r--contrib/extraction/table.mli44
-rw-r--r--contrib/extraction/test_extraction.v2
13 files changed, 483 insertions, 595 deletions
diff --git a/.depend b/.depend
index d8deee0351..e6539d98a7 100644
--- a/.depend
+++ b/.depend
@@ -38,10 +38,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/univ.cmi
kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/names.cmi kernel/term.cmi kernel/univ.cmi
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi
kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi
kernel/names.cmi: lib/pp.cmi lib/predicate.cmi
kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
kernel/univ.cmi
@@ -61,9 +61,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/bignat.cmi: lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
-lib/rtree.cmi: lib/pp.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -93,6 +90,9 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi
library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
kernel/sign.cmi lib/util.cmi
library/summary.cmi: library/libnames.cmi kernel/names.cmi
+lib/rtree.cmi: lib/pp.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
lib/util.cmi
@@ -304,20 +304,20 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
library/libnames.cmi kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi
contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
kernel/term.cmi interp/topconstr.cmi lib/util.cmi
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
- pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi \
contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
kernel/sign.cmi kernel/term.cmi
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+ pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
contrib/correctness/ptype.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
@@ -373,7 +373,8 @@ contrib/extraction/ocaml.cmi: library/libnames.cmi \
contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi
contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
lib/pp.cmi
-contrib/extraction/table.cmi: library/libnames.cmi kernel/names.cmi
+contrib/extraction/table.cmi: library/libnames.cmi \
+ contrib/extraction/miniml.cmi kernel/names.cmi
contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
proofs/tacmach.cmi
contrib/interface/dad.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
@@ -546,6 +547,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/modops.cmi
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+ kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -554,12 +561,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi kernel/modops.cmi
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
- kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -642,34 +643,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
lib/hashcons.cmx: lib/hashcons.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/pp_control.cmo: lib/pp_control.cmi
lib/pp_control.cmx: lib/pp_control.cmi
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/predicate.cmo: lib/predicate.cmi
lib/predicate.cmx: lib/predicate.cmi
lib/profile.cmo: lib/profile.cmi
lib/profile.cmx: lib/profile.cmi
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -772,6 +763,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
lib/system.cmx library/states.cmi
library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi
library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
toplevel/vernacexpr.cmo
@@ -1754,10 +1755,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
lib/util.cmx tactics/wcclausenv.cmi
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/gallina.cmo: tools/gallina_lexer.cmo
tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1962,14 +1963,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi
toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi
-toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \
- kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
- library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \
- toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
- kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
- library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
- toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2030,6 +2023,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
+ library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \
+ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
+ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
+ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi
contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi
contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -2050,6 +2051,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx lib/util.cmx
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+ contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+ contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+ contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+ contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2066,18 +2079,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
- contrib/correctness/past.cmi contrib/correctness/penv.cmi \
- contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
- contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
- kernel/univ.cmi contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
- contrib/correctness/past.cmi contrib/correctness/penv.cmx \
- contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
- contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
- kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2303,20 +2304,18 @@ contrib/correctness/pwp.cmx: kernel/environ.cmx library/global.cmx \
kernel/reduction.cmx pretyping/reductionops.cmx kernel/term.cmx \
pretyping/termops.cmx lib/util.cmx contrib/correctness/pwp.cmi
contrib/extraction/common.cmo: library/declaremods.cmi \
- contrib/extraction/extraction.cmi contrib/extraction/haskell.cmi \
- library/lib.cmi library/libnames.cmi library/libobject.cmi \
- contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
- library/nameops.cmi kernel/names.cmi library/nametab.cmi \
- contrib/extraction/ocaml.cmi lib/pp.cmi lib/pp_control.cmi \
- parsing/printer.cmi contrib/extraction/scheme.cmi \
+ contrib/extraction/haskell.cmi library/lib.cmi library/libnames.cmi \
+ library/libobject.cmi contrib/extraction/miniml.cmi \
+ contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
+ library/nametab.cmi contrib/extraction/ocaml.cmi lib/pp.cmi \
+ lib/pp_control.cmi parsing/printer.cmi contrib/extraction/scheme.cmi \
contrib/extraction/table.cmi lib/util.cmi contrib/extraction/common.cmi
contrib/extraction/common.cmx: library/declaremods.cmx \
- contrib/extraction/extraction.cmx contrib/extraction/haskell.cmx \
- library/lib.cmx library/libnames.cmx library/libobject.cmx \
- contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
- library/nameops.cmx kernel/names.cmx library/nametab.cmx \
- contrib/extraction/ocaml.cmx lib/pp.cmx lib/pp_control.cmx \
- parsing/printer.cmx contrib/extraction/scheme.cmx \
+ contrib/extraction/haskell.cmx library/lib.cmx library/libnames.cmx \
+ library/libobject.cmx contrib/extraction/miniml.cmi \
+ contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
+ library/nametab.cmx contrib/extraction/ocaml.cmx lib/pp.cmx \
+ lib/pp_control.cmx parsing/printer.cmx contrib/extraction/scheme.cmx \
contrib/extraction/table.cmx lib/util.cmx contrib/extraction/common.cmi
contrib/extraction/extract_env.cmo: contrib/extraction/common.cmi \
kernel/declarations.cmi library/declare.cmi \
@@ -2333,7 +2332,7 @@ contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \
contrib/extraction/table.cmx lib/util.cmx \
contrib/extraction/extract_env.cmi
contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
- pretyping/evd.cmi library/global.cmi lib/gmap.cmi kernel/inductive.cmi \
+ pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \
pretyping/inductiveops.cmi library/libnames.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
@@ -2341,7 +2340,7 @@ contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
library/summary.cmi contrib/extraction/table.cmi kernel/term.cmi \
pretyping/termops.cmi lib/util.cmi contrib/extraction/extraction.cmi
contrib/extraction/extraction.cmx: kernel/declarations.cmx kernel/environ.cmx \
- pretyping/evd.cmx library/global.cmx lib/gmap.cmx kernel/inductive.cmx \
+ pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \
pretyping/inductiveops.cmx library/libnames.cmx \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
@@ -2358,13 +2357,15 @@ contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \
contrib/extraction/extract_env.cmx interp/genarg.cmx parsing/pcoq.cmx \
lib/pp.cmx contrib/extraction/table.cmx toplevel/vernacexpr.cmx \
toplevel/vernacinterp.cmx
-contrib/extraction/haskell.cmo: contrib/extraction/miniml.cmi \
- contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
- contrib/extraction/ocaml.cmi lib/pp.cmi lib/util.cmi \
+contrib/extraction/haskell.cmo: library/libnames.cmi \
+ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
+ library/nameops.cmi kernel/names.cmi contrib/extraction/ocaml.cmi \
+ lib/pp.cmi parsing/printer.cmi lib/util.cmi \
contrib/extraction/haskell.cmi
-contrib/extraction/haskell.cmx: contrib/extraction/miniml.cmi \
- contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
- contrib/extraction/ocaml.cmx lib/pp.cmx lib/util.cmx \
+contrib/extraction/haskell.cmx: library/libnames.cmx \
+ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
+ library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \
+ lib/pp.cmx parsing/printer.cmx lib/util.cmx \
contrib/extraction/haskell.cmi
contrib/extraction/mlutil.cmo: library/libnames.cmi \
contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \
@@ -2376,11 +2377,11 @@ contrib/extraction/mlutil.cmx: library/libnames.cmx \
contrib/extraction/mlutil.cmi
contrib/extraction/ocaml.cmo: library/libnames.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
- library/nameops.cmi kernel/names.cmi lib/pp.cmi \
+ library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
contrib/extraction/table.cmi lib/util.cmi contrib/extraction/ocaml.cmi
contrib/extraction/ocaml.cmx: library/libnames.cmx \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
- library/nameops.cmx kernel/names.cmx lib/pp.cmx \
+ library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
contrib/extraction/table.cmx lib/util.cmx contrib/extraction/ocaml.cmi
contrib/extraction/scheme.cmo: library/libnames.cmi \
contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
@@ -2391,16 +2392,16 @@ contrib/extraction/scheme.cmx: library/libnames.cmx \
library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \
lib/pp.cmx lib/util.cmx contrib/extraction/scheme.cmi
contrib/extraction/table.cmo: kernel/declarations.cmi kernel/environ.cmi \
- library/global.cmi lib/gmap.cmi library/goptions.cmi library/lib.cmi \
- library/libnames.cmi library/libobject.cmi library/nameops.cmi \
- kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
- parsing/printer.cmi kernel/reduction.cmi library/summary.cmi \
+ library/global.cmi library/goptions.cmi library/lib.cmi \
+ library/libnames.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
+ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+ lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi library/summary.cmi \
kernel/term.cmi lib/util.cmi contrib/extraction/table.cmi
contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \
- library/global.cmx lib/gmap.cmx library/goptions.cmx library/lib.cmx \
- library/libnames.cmx library/libobject.cmx library/nameops.cmx \
- kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
- parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \
+ library/global.cmx library/goptions.cmx library/lib.cmx \
+ library/libnames.cmx library/libobject.cmx contrib/extraction/miniml.cmi \
+ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+ lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \
kernel/term.cmx lib/util.cmx contrib/extraction/table.cmi
contrib/field/field.cmo: toplevel/cerrors.cmi interp/constrintern.cmi \
library/declare.cmi parsing/egrammar.cmi pretyping/evd.cmi \
@@ -2612,6 +2613,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx contrib/interface/ctast.cmx \
tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \
pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2636,14 +2645,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
pretyping/termops.cmx contrib/interface/translate.cmx \
pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
contrib/interface/showproof.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
- parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
- parsing/printer.cmi contrib/interface/translate.cmi \
- contrib/interface/vtp.cmi contrib/interface/xlate.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
- parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
- parsing/printer.cmx contrib/interface/translate.cmx \
- contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2812,12 +2813,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx lib/util.cmx
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi
contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -2872,8 +2873,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
contrib/xml/xml.cmx
contrib/xml/unshare.cmo: contrib/xml/unshare.cmi
contrib/xml/unshare.cmx: contrib/xml/unshare.cmi
-contrib/xml/xml.cmo: contrib/xml/xml.cmi
-contrib/xml/xml.cmx: contrib/xml/xml.cmi
contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -2900,6 +2899,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
tactics/tauto.cmo: parsing/grammar.cma
tactics/tauto.cmx: parsing/grammar.cma
tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index bfe693c64b..28f560d96b 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -19,6 +19,8 @@ open Miniml
open Mlutil
open Ocaml
+(*s Get all references used in one [ml_decl list]. *)
+
module Orefset = struct
type t = { set : Refset.t ; list : global_reference list }
let empty = { set = Refset.empty ; list = [] }
@@ -31,58 +33,12 @@ end
type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
-let add_down o r = o.down <- Orefset.add r o.down
-let add_up o r = o.up <- Orefset.add r o.up
-let lang_add_type o r = if lang () = Haskell then add_up o r else add_down o r
-
-(*s Get all references used in one [ml_decl] list. *)
-
-let mltype_get_references o t =
- let rec get_rec = function
- | Tglob (r,l) -> lang_add_type o r; List.iter get_rec l
- | Tarr (a,b) -> get_rec a; get_rec b
- | _ -> ()
- in get_rec t
-
-let ast_get_references o a =
- let rec get_rec a =
- ast_iter get_rec a;
- match a with
- | MLglob r -> add_down o r
- | MLcons (r,_) -> add_up o r
- | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> add_up o r) v
- | MLcast (_,t) -> mltype_get_references o t
- | _ -> ()
- in get_rec a
-
-let ip_of_indref = function
- | IndRef ip -> ip
- | _ -> assert false
-
let decl_get_references ld =
let o = { up = Orefset.empty ; down = Orefset.empty } in
- let one_decl = function
- | Dind (l,_) ->
- List.iter (fun (_,r,l) ->
- lang_add_type o r;
- (try
- List.iter (add_down o) (find_proj (ip_of_indref r))
- with Not_found -> ());
- List.iter (fun (r,l) ->
- add_up o r;
- List.iter (mltype_get_references o) l) l) l
- | Dtype (r,_,t) -> lang_add_type o r; mltype_get_references o t
- | Dterm (r,a,t) ->
- add_down o r; ast_get_references o a; mltype_get_references o t
- | Dfix(rv,c,t) ->
- Array.iter (add_down o) rv;
- Array.iter (ast_get_references o) c;
- Array.iter (mltype_get_references o) t
- | DcustomTerm (r,_) -> add_down o r
- | DcustomType (r,_) -> lang_add_type o r
- in
- List.iter one_decl ld;
- o
+ let do_term r = o.down <- Orefset.add r o.down in
+ let do_cons r = o.up <- Orefset.add r o.up in
+ let do_type = if lang () = Haskell then do_cons else do_term in
+ List.iter (decl_iter_references do_term do_cons do_type) ld; o
(*S Modules considerations. *)
@@ -229,17 +185,6 @@ let preamble prm = match lang () with
| Haskell -> Haskell.preamble prm
| Scheme -> Scheme.preamble prm
| Toplevel -> (fun _ _ -> mt ())
-
-let pp_comment s = match lang () with
- | Haskell -> str "-- " ++ s ++ fnl ()
- | Scheme -> str ";" ++ s ++ fnl ()
- | Ocaml | Toplevel -> str "(* " ++ s ++ str " *)" ++ fnl ()
-
-let pp_logical_ind r =
- pp_comment (Printer.pr_global r ++ str " : logical inductive")
-
-let pp_singleton_ind r =
- pp_comment (Printer.pr_global r ++ str " : singleton inductive constructor")
(*S Extraction to a file. *)
@@ -263,12 +208,6 @@ let extract_to_file f prm decls =
decl_type_search Tdummy decls,
decl_type_search Tunknown decls) in
pp_with ft (preamble prm used_modules print_dummys);
- if not prm.modular then begin
- List.iter (fun r -> pp_with ft (pp_logical_ind r))
- (List.filter Extraction.decl_is_logical_ind prm.to_appear);
- List.iter (fun r -> pp_with ft (pp_singleton_ind r))
- (List.filter Extraction.decl_is_singleton prm.to_appear);
- end;
begin try
List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
with e ->
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 2f420b8ad1..fb2291edfa 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -19,10 +19,6 @@ val long_module : global_reference -> dir_path
val create_mono_renamings : ml_decl list -> unit
val set_keywords : unit -> unit
-val pp_logical_ind : global_reference -> std_ppcmds
-
-val pp_singleton_ind : global_reference -> std_ppcmds
-
val pp_decl : unit -> ml_decl -> std_ppcmds
val segment_contents : Lib.library_segment -> global_reference list
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9d1808a76d..7d19fa68d7 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -179,8 +179,7 @@ let check_r m sm r =
let check_decl m sm = function
| Dterm (r,_,_) -> check_r m sm r
| Dtype (r,_,_) -> check_r m sm r
- | Dind ((_,r,_)::_, _) -> check_r m sm r
- | Dind ([],_) -> ()
+ | Dind (kn,_) -> check_r m sm (IndRef (kn,0))
| DcustomTerm (r,_) -> check_r m sm r
| DcustomType (r,_) -> check_r m sm r
| Dfix(rv,_,_) -> Array.iter (check_r m sm) rv
@@ -280,13 +279,13 @@ and visit_ast m eenv a =
in
visit a
-and visit_inductive m eenv inds =
- let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in
- let visit_ind (_,_,cl) = List.iter visit_constructor cl in
- List.iter visit_ind inds
+and visit_inductive m eenv ind =
+ let visit_constructor tl = List.iter (visit_type m eenv) tl in
+ let visit_packet p = Array.iter visit_constructor p.ip_types in
+ Array.iter visit_packet ind.ind_packets
and visit_decl m eenv = function
- | Dind (inds,_) -> visit_inductive m eenv inds
+ | Dind (_,ind) -> visit_inductive m eenv ind
| Dtype (_,_,t) -> visit_type m eenv t
| Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
| Dfix (_,c,t) ->
@@ -333,8 +332,7 @@ let print_user_extract r =
let decl_in_r r0 = function
| Dterm (r,_,_) -> r = r0
| Dtype (r,_,_) -> r = r0
- | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
- | Dind ([],_) -> false
+ | Dind (kn, _) -> kn = kn_of_r r0
| DcustomTerm (r,_) -> r = r0
| DcustomType (r,_) -> r = r0
| Dfix (rv,_,_) -> array_exists ((=) r0) rv
@@ -343,10 +341,6 @@ let extraction qid =
let r = Nametab.global qid in
if is_ml_extraction r then
print_user_extract r
- else if decl_is_logical_ind r then
- msgnl (pp_logical_ind r)
- else if decl_is_singleton r then
- msgnl (pp_singleton_ind r)
else
let prm =
{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
@@ -404,8 +398,7 @@ let extraction_file f vl =
let decl_in_m m = function
| Dterm (r,_,_) -> m = long_module r
| Dtype (r,_,_) -> m = long_module r
- | Dind ((_,r,_)::_, _) -> m = long_module r
- | Dind ([],_) -> false
+ | Dind (kn,_) -> m = long_module (IndRef (kn,0))
| DcustomTerm (r,_) -> m = long_module r
| DcustomType (r,_) -> m = long_module r
| Dfix (rv,_,_) -> m = long_module rv.(0)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 76b4133aba..6e1cdcfccb 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -29,7 +29,17 @@ open Table
open Mlutil
(*i*)
-(*S Extraction results. *)
+exception I of inductive_info
+
+let none = Evd.empty
+
+let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
+
+let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
+
+let is_axiom kn = (Global.lookup_constant kn).const_body = None
+
+(*S Generation of flags and signatures. *)
(* The type [flag] gives us information about any Coq term:
\begin{itemize}
@@ -51,77 +61,6 @@ type scheme = TypeScheme | Default
type flag = info * scheme
-(* The [signature] type is used to know how many arguments a CIC
- object expects, and what these arguments will become in the ML
- object. *)
-
-(* Convention: outmost lambda/product gives the head of the list,
- and [true] means that the argument is to be kept. *)
-
-type signature = bool list
-
-(* The [ind_extraction_result] is used to save the extraction of
- an inductive type. In the informative case, it stores a signature
- and a type variable list. *)
-
-type ind_extraction_result = signature * identifier list
-
-(* For an informative constructor, the [cons_extraction_result]
- contains the list of the types of its arguments and the number of
- parameters to discard. *)
-
-type cons_extraction_result = ml_type list * int
-
-(*S Tables to keep the extraction results. *)
-
-let visited_inductive = ref KNset.empty
-let visit_inductive k = visited_inductive := KNset.add k !visited_inductive
-let already_visited_inductive k = KNset.mem k !visited_inductive
-
-let inductive_table =
- ref (Gmap.empty : (inductive, ind_extraction_result) Gmap.t)
-let add_inductive i e = inductive_table := Gmap.add i e !inductive_table
-let lookup_inductive i = Gmap.find i !inductive_table
-
-let constructor_table =
- ref (Gmap.empty : (constructor, cons_extraction_result) Gmap.t)
-let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
-let lookup_constructor c = Gmap.find c !constructor_table
-
-let cst_term_table = ref (KNmap.empty : ml_decl KNmap.t)
-let add_cst_term kn d = cst_term_table := KNmap.add kn d !cst_term_table
-let lookup_cst_term kn = KNmap.find kn !cst_term_table
-
-let cst_type_table = ref (KNmap.empty : ml_schema KNmap.t)
-let add_cst_type kn s = cst_type_table := KNmap.add kn s !cst_type_table
-let lookup_cst_type kn = KNmap.find kn !cst_type_table
-
-(* Tables synchronization. *)
-
-let freeze () =
- !visited_inductive, !inductive_table,
- !constructor_table, !cst_term_table, !cst_type_table
-
-let unfreeze (vi,it,ct,te,ty) =
- visited_inductive := vi; inductive_table := it; constructor_table := ct;
- cst_term_table := te; cst_type_table := ty
-
-let _ = declare_summary "Extraction tables"
- { freeze_function = freeze;
- unfreeze_function = unfreeze;
- init_function = (fun () -> ());
- survive_section = true }
-
-(*S Generation of flags and signatures. *)
-
-let none = Evd.empty
-
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
-
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
-
-let is_axiom kn = (Global.lookup_constant kn).const_body = None
-
(*s [flag_of_type] transforms a type [t] into a [flag].
Really important function. *)
@@ -251,8 +190,8 @@ let rec extract_type env db j c args =
(* There are two kinds of informative axioms here, *)
(* - the types that should be realized via [Extract Constant] *)
(* - the type schemes that are not realizable (yet). *)
- if args = [] then error_axiom kn
- else error_axiom_scheme kn
+ if args = [] then error_axiom (ConstRef kn)
+ else error_axiom_scheme (ConstRef kn)
| Const kn ->
let body = constant_value env kn in
let mlt1 = extract_type env db j (applist (body, args)) [] in
@@ -266,9 +205,9 @@ let rec extract_type env db j c args =
(* reduction. Try to find the shortest correct answer. *)
if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1
| None -> mlt1)
- | Ind kni ->
- let si = fst (extract_inductive kni) in
- extract_type_app env db (IndRef kni,si) args
+ | Ind ((kn,i) as ip) ->
+ let s = (extract_inductive kn).ind_packets.(i).ip_sign in
+ extract_type_app env db (IndRef ip,s) args
| Case _ | Fix _ | CoFix _ -> Tunknown
| _ -> assert false
@@ -320,78 +259,71 @@ and extract_type_scheme env db c p =
(*S Extraction of an inductive type. *)
-(* [extract_inductive] answers a [ind_extraction_result] in
- case of an informative inductive, and raises [Not_found] otherwise *)
-
-and extract_inductive ((kn,_) as i) =
- if not (already_visited_inductive kn) then extract_mib kn;
- lookup_inductive i
-
-(* [extract_constructor] answers a [cons_extraction_result] in
- case of an informative constructor, and raises [Not_found] otherwise *)
-
-and extract_constructor (((kn,_),_) as c) =
- if not (already_visited_inductive kn) then extract_mib kn;
- lookup_constructor c
-
-(* The real job: *)
-
-and extract_mib kn =
- visit_inductive kn;
- add_recursors kn;
- let env = Global.env () in
- let (mib,mip) = Global.lookup_inductive (kn,0) in
- (* Everything concerning parameters. *)
- (* We do that first, since they are common to all the [mib]. *)
- let params_nb = mip.mind_nparams in
- let params_env = push_rel_context mip.mind_params_ctxt env in
- (* First pass: we store inductive signatures together with *)
- (* their type var list. *)
- for i = 0 to mib.mind_ntypes - 1 do
- let mip = snd (Global.lookup_inductive (kn,i)) in
- if mip.mind_sort <> (Prop Null) then
- let ip = (kn,i) in
- let s,vl = type_sign_vl env mip.mind_nf_arity in
- add_inductive ip (s,vl);
- done;
- (* Second pass: we extract constructors *)
- for i = 0 to mib.mind_ntypes - 1 do
- let ip = (kn,i) in
- let mip = snd (Global.lookup_inductive ip) in
- if mip.mind_sort <> (Prop Null) then
- let s = fst (lookup_inductive ip) in
- let types = arities_of_constructors env ip in
- for j = 0 to Array.length types - 1 do
- let t = snd (decompose_prod_n params_nb types.(j)) in
- let args = match kind_of_term (snd (decompose_prod t)) with
- | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
- | _ -> [||]
+and extract_inductive kn =
+ try lookup_ind kn with Not_found ->
+ add_recursors kn;
+ let env = Global.env () in
+ let (mib,mip) = Global.lookup_inductive (kn,0) in
+ (* Everything concerning parameters. *)
+ (* We do that first, since they are common to all the [mib]. *)
+ let npar = mip.mind_nparams in
+ let epar = push_rel_context mip.mind_params_ctxt env in
+ (* First pass: we store inductive signatures together with *)
+ (* their type var list. *)
+ let packets =
+ Array.map
+ (fun mip ->
+ let b = mip.mind_sort <> (Prop Null) in
+ let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in
+ let t = Array.make (Array.length mip.mind_nf_lc) [] in
+ { ip_logical = (not b); ip_sign = s; ip_vars = v; ip_types = t })
+ mib.mind_packets
+ in
+ add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets};
+ (* Second pass: we extract constructors *)
+ for i = 0 to mib.mind_ntypes - 1 do
+ let p = packets.(i) in
+ if not p.ip_logical then
+ let types = arities_of_constructors env (kn,i) in
+ for j = 0 to Array.length types - 1 do
+ let t = snd (decompose_prod_n npar types.(j)) in
+ let args = match kind_of_term (snd (decompose_prod t)) with
+ | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+ | _ -> [||]
+ in
+ let dbmap = parse_ind_args p.ip_sign args (nb_prod t + npar) in
+ let db = db_from_ind dbmap npar in
+ p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
+ done
+ done;
+ (* Third pass: we determine special cases. *)
+ let ind_info =
+ try
+ if not mib.mind_finite then raise (I Coinductive);
+ if mib.mind_ntypes <> 1 then raise (I Standard);
+ let p = packets.(0) in
+ if p.ip_logical then raise (I Standard);
+ if Array.length p.ip_types <> 1 then raise (I Standard);
+ let typ = p.ip_types.(0) in
+ let l = List.filter (type_neq mlt_env Tdummy) typ in
+ if List.length l = 1 && not (type_mem_kn kn (List.hd l))
+ then raise (I Singleton);
+ if l = [] then raise (I Standard);
+ let projs =
+ try (find_structure (kn,0)).s_PROJ
+ with Not_found -> raise (I Standard);
in
- let dbmap = parse_ind_args s args (nb_prod t + params_nb) in
- let db = db_from_ind dbmap params_nb in
- let l = extract_type_cons params_env db dbmap t (params_nb+1) in
- add_constructor (ip,j+1) (l,params_nb)
- done
- done;
- (* Record tables: *)
- if mib.mind_ntypes = 1 then
- let ip = (kn,0) in
- let mip = snd (Global.lookup_inductive ip) in
- if (mip.mind_sort <> (Prop Null))
- && (Array.length mip.mind_consnames = 1)
- && not (is_singleton_inductive ip)
- then try
- let typs = fst (lookup_constructor (ip,1)) in
- let s = List.map (type_neq mlt_env Tdummy) typs in
- if not (List.mem true s) then raise Not_found;
- let projs = (find_structure ip).s_PROJ in
- assert (List.length s = List.length projs);
- let check (_,o) = match o with
- | None -> raise Not_found
- | Some kn -> ConstRef kn
- in
- add_record ip (List.map check (List.filter fst (List.combine s projs)))
- with Not_found -> ()
+ let s = List.map (type_neq mlt_env Tdummy) l in
+ let check (_,o) = match o with
+ | None -> raise (I Standard)
+ | Some kn -> ConstRef kn
+ in
+ add_record kn (List.map check (List.filter fst (List.combine s projs)));
+ raise (I Record)
+ with (I info) -> info
+ in
+ let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
+ add_ind kn i; i
(*s [extract_type_cons] extracts the type of an inductive
constructor toward the corresponding list of ML types. *)
@@ -411,29 +343,11 @@ and extract_type_cons env db dbmap c i =
(extract_type env db 0 t []) :: l
| _ -> []
-(*s Looking for informative singleton case, i.e. an inductive with one
- constructor which has one informative argument. This dummy case will
- be simplified. *)
-
-and is_singleton_inductive ip =
- let (mib,mip) = Global.lookup_inductive ip in
- mib.mind_finite &&
- (mib.mind_ntypes = 1) &&
- (Array.length mip.mind_consnames = 1) &&
- try
- let l =
- List.filter (type_neq mlt_env Tdummy) (fst (extract_constructor (ip,1)))
- in List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l))
- with Not_found -> false
-
-and is_singleton_constructor ((kn,i),_) =
- is_singleton_inductive (kn,i)
-
(*s Recording the ML type abbreviation of a Coq type scheme constant. *)
and mlt_env r = match r with
| ConstRef kn ->
- (try match lookup_cst_term kn with
+ (try match lookup_term kn with
| Dtype (_,vl,mlt) -> Some mlt
| _ -> None
with Not_found ->
@@ -449,7 +363,7 @@ and mlt_env r = match r with
let s,vl = type_sign_vl env typ in
let db = db_from_sign s in
let t = extract_type_scheme env db body (List.length s)
- in add_cst_term kn (Dtype (r, vl, t)); Some t
+ in add_term kn (Dtype (r, vl, t)); Some t
| _ -> None))
| _ -> None
@@ -461,12 +375,12 @@ let type_expunge = type_expunge mlt_env
(*s Extraction of the type of a constant. *)
let record_constant_type kn =
- try lookup_cst_type kn
+ try lookup_type kn
with Not_found ->
let env = Global.env () in
let mlt = extract_type env [] 1 (constant_type env kn) [] in
let schema = (type_maxvar mlt, mlt)
- in add_cst_type kn schema; schema
+ in add_type kn schema; schema
(*S Extraction of a term. *)
@@ -603,14 +517,16 @@ and extract_cst_app env mle mlt kn args =
they are fixed, and thus are not used for the computation.
\end{itemize} *)
-and extract_cons_app env mle mlt ((ip,_) as cp) args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
(* First, we build the type of the constructor, stored in small pieces. *)
- let types, params_nb = extract_constructor cp in
- let types = List.map type_expand types in
- let nb_tvar = List.length (snd (extract_inductive ip)) in
- let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in
+ let mi = extract_inductive kn in
+ let params_nb = mi.ind_nparams in
+ let oi = mi.ind_packets.(i) in
+ let nb_tvars = List.length oi.ip_vars
+ and types = List.map type_expand oi.ip_types.(j-1) in
+ let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
- let type_cons = instantiation (nb_tvar, type_cons) in
+ let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
let s = List.map ((<>) Tdummy) types in
let ls = List.length s in
@@ -624,7 +540,7 @@ and extract_cons_app env mle mlt ((ip,_) as cp) args =
(* If stored and expected types differ, then magic! *)
let magic = needs_magic (type_cons, type_head) in
let head mla =
- if is_singleton_constructor cp then
+ if mi.ind_info = Singleton then
put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *)
else put_magic_if magic (MLcons (ConstructRef cp, mla))
in
@@ -643,7 +559,7 @@ and extract_cons_app env mle mlt ((ip,_) as cp) args =
(*S Extraction of a case. *)
-and extract_case env mle (ip,c,br) mlt =
+and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* [br]: bodies of each branch (in functional form) *)
(* [ni]: number of arguments without parameters in each branch *)
let ni = mis_constr_nargs ip in
@@ -665,8 +581,10 @@ and extract_case env mle (ip,c,br) mlt =
snd (case_expunge s e)
end
else
- let nb_tvar = List.length (snd (extract_inductive ip)) in
- let metas = Array.init nb_tvar new_meta in
+ let mi = extract_inductive kn in
+ let params_nb = mi.ind_nparams in
+ let oi = mi.ind_packets.(i) in
+ let metas = Array.init (List.length oi.ip_vars) new_meta in
(* The extraction of the head. *)
let type_head = Tglob (IndRef ip, Array.to_list metas) in
let a = extract_term env mle type_head c [] in
@@ -674,14 +592,14 @@ and extract_case env mle (ip,c,br) mlt =
let extract_branch i =
(* The types of the arguments of the corresponding constructor. *)
let f t = type_subst_vect metas (type_expand t) in
- let l = List.map f (fst (extract_constructor (ip,i+1))) in
+ let l = List.map f oi.ip_types.(i) in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
(ConstructRef (ip,i+1), List.rev ids, e)
in
- if is_singleton_inductive ip then
+ if mi.ind_info = Singleton then
begin
(* Informative singleton case: *)
(* [match c with C i -> t] becomes [let i = c' in t'] *)
@@ -733,11 +651,11 @@ let extract_constant kn r =
| None -> (* A logical axiom is risky, an informative one is fatal. *)
(match flag_of_type env typ with
| (Info,TypeScheme) ->
- if isSort typ then error_axiom kn
- else error_axiom_scheme kn
- | (Info,Default) -> error_axiom kn
- | (Logic,TypeScheme) -> warning_axiom kn; Dtype (r, [], Tdummy)
- | (Logic,Default) -> warning_axiom kn; Dterm (r, MLdummy, Tdummy))
+ if isSort typ then error_axiom r
+ else error_axiom_scheme r
+ | (Info,Default) -> error_axiom r
+ | (Logic,TypeScheme) -> warning_axiom r; Dtype (r, [], Tdummy)
+ | (Logic,Default) -> warning_axiom r; Dterm (r, MLdummy, Tdummy))
| Some l_body ->
(match flag_of_type env typ with
| (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
@@ -774,42 +692,18 @@ let extract_constant kn r =
Dtype (r, vl, t))
let extract_constant_cache kn r =
- try lookup_cst_term kn
+ try lookup_term kn
with Not_found ->
let d = extract_constant kn r
- in add_cst_term kn d; d
-
-(*s From an inductive to a ML declaration. *)
-
-let extract_inductive_declaration kn =
- if not (already_visited_inductive kn) then extract_mib kn;
- let ip = (kn,0) in
- if is_singleton_inductive ip then
- let t =
- List.hd (List.filter (type_neq Tdummy) (fst (lookup_constructor (ip,1))))
- and vl = snd (lookup_inductive ip) in
- Dtype (IndRef ip,vl,t)
- else
- let mib = Global.lookup_mind kn in
- let one_ind ip n =
- iterate_for (-n) (-1)
- (fun j l ->
- let cp = (ip,-j) in
- let mlt = fst (lookup_constructor cp) in
- (ConstructRef cp, List.filter (type_neq Tdummy) mlt)::l) []
- in
- let l =
- iterate_for (1 - mib.mind_ntypes) 0
- (fun i acc ->
- let ip = (kn,-i) in
- let nc = Array.length mib.mind_packets.(-i).mind_consnames in
- try
- let vl = snd (lookup_inductive ip) in
- (vl, IndRef ip, one_ind ip nc) :: acc
- with Not_found -> acc)
- []
- in
- Dind (l, not mib.mind_finite)
+ in add_term kn d; d
+
+let extract_inductive_declaration kn =
+ let ind = extract_inductive kn in
+ let f l = List.filter (type_neq Tdummy) l in
+ let packets =
+ Array.map (fun p -> { p with ip_types = Array.map f p.ip_types })
+ ind.ind_packets
+ in Dind (kn,{ ind with ind_packets = packets })
(*s From a global reference to a ML declaration. *)
@@ -819,19 +713,4 @@ let extract_declaration r = match r with
| ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
| VarRef kn -> error_section ()
-(*s Check if a global reference corresponds to a logical inductive. *)
-
-let decl_is_logical_ind = function
- | IndRef ip -> (try ignore (extract_inductive ip); false with _ -> true)
- | ConstructRef cp ->
- (try ignore (extract_constructor cp); false with _ -> true)
- | _ -> false
-
-(*s Check if a global reference corresponds to the constructor of
- a singleton inductive. *)
-
-let decl_is_singleton = function
- | ConstructRef cp -> is_singleton_constructor cp
- | _ -> false
-
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b8e74961b8..268a68692f 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -17,12 +17,3 @@ open Miniml
val extract_declaration : global_reference -> ml_decl
-(*s Check whether a global reference corresponds to a logical inductive. *)
-
-val decl_is_logical_ind : global_reference -> bool
-
-(*s Check if a global reference corresponds to the constructor of
- a singleton inductive. *)
-
-val decl_is_singleton : global_reference -> bool
-
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 149b9967cb..81ec48767a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -14,6 +14,7 @@ open Pp
open Util
open Names
open Nameops
+open Libnames
open Miniml
open Mlutil
open Ocaml
@@ -176,7 +177,25 @@ and pp_function env f t =
(*s Pretty-printing of inductive types declaration. *)
-let pp_one_inductive (pl,name,cl) =
+let pp_comment s = str "-- " ++ s ++ fnl ()
+
+let pp_logical_ind ip packet =
+ pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+ pp_comment (str "with constructors : " ++
+ prvect_with_sep spc Printer.pr_global
+ (Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types))
+
+let pp_singleton kn packet =
+ let l = rename_tvars keywords packet.ip_vars in
+ let l' = List.rev l in
+ hov 0 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++
+ prlist_with_sep spc pr_id l ++
+ (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
+ pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+ pp_comment (str "singleton inductive, whose constructor was " ++
+ Printer.pr_global (ConstructRef ((kn,0),1))))
+
+let pp_one_ind ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
(pp_global r ++
@@ -186,25 +205,32 @@ let pp_one_inductive (pl,name,cl) =
prlist_with_sep
(fun () -> (str " ")) (pp_type true (List.rev pl)) l))
in
- (str (if cl = [] then "type " else "data ") ++
- pp_global name ++ str " " ++
- prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
- (if pl = [] then (mt ()) else (str " ")) ++
- if cl = [] then str "= () -- empty inductive"
- else
- (v 0 (str "= " ++
- prlist_with_sep (fun () -> (fnl () ++ str " | "))
- pp_constructor cl)))
+ str (if cv = [||] then "type " else "data ") ++
+ pp_global (IndRef ip) ++ str " " ++
+ prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
+ (if pl = [] then mt () else str " ") ++
+ if cv = [||] then str "= () -- empty inductive"
+ else
+ (v 0 (str "= " ++
+ prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor
+ (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
-let pp_inductive il =
- (prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ())
+let rec pp_ind kn i ind =
+ if i >= Array.length ind.ind_packets then mt ()
+ else
+ let ip = (kn,i) in
+ let p = ind.ind_packets.(i) in
+ if p.ip_logical then
+ pp_logical_ind ip p ++ pp_ind kn (i+1) ind
+ else
+ pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ pp_ind kn (i+1) ind
+
(*s Pretty-printing of a declaration. *)
let pp_decl = function
- | Dind ([], _) -> mt ()
- | Dind (i, _) ->
- hov 0 (pp_inductive i)
+ | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0)
+ | Dind (kn,i) -> hov 0 (pp_ind kn 0 i)
| Dtype (r, l, t) ->
let l = rename_tvars keywords l in
let l' = List.rev l in
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 199bb9e0cc..6f56f36e30 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -15,6 +15,15 @@ open Util
open Names
open Libnames
+(* The [signature] type is used to know how many arguments a CIC
+ object expects, and what these arguments will become in the ML
+ object. *)
+
+(* Convention: outmost lambda/product gives the head of the list,
+ and [true] means that the argument is to be kept. *)
+
+type signature = bool list
+
(*s ML type expressions. *)
type ml_type =
@@ -27,7 +36,7 @@ type ml_type =
| Tunknown
| Tcustom of string
-and ml_meta = { id : int; mutable contents : ml_type option}
+and ml_meta = { id : int; mutable contents : ml_type option }
(* ML type schema.
The integer is the number of variable in the schema. *)
@@ -36,11 +45,28 @@ type ml_schema = int * ml_type
(*s ML inductive types. *)
-type ml_one_ind =
- identifier list * global_reference * (global_reference * ml_type list) list
+type inductive_info = Record | Singleton | Coinductive | Standard
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
+ If the inductive is logical ([ip_logical = false]), then all other fields
+ are unused. Otherwise,
+ [ip_sign] is a signature concerning the arguments of the inductive,
+ [ip_vars] contains the names of the type variables surviving in ML,
+ [ip_types] contains the ML types of all constructors.
+*)
-type ml_ind =
- ml_one_ind list * bool (* cofix *)
+type ml_ind_packet = {
+ ip_logical : bool;
+ ip_sign : signature;
+ ip_vars : identifier list;
+ ip_types : (ml_type list) array }
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type ml_ind = {
+ ind_info : inductive_info;
+ ind_nparams : int;
+ ind_packets : ml_ind_packet array }
(*s ML terms. *)
@@ -59,11 +85,10 @@ type ml_ast =
| MLmagic of ml_ast
| MLcustom of string
-
(*s ML declarations. *)
type ml_decl =
- | Dind of ml_ind
+ | Dind of kernel_name * ml_ind
| Dtype of global_reference * identifier list * ml_type
| Dterm of global_reference * ml_ast * ml_type
| DcustomTerm of global_reference * string
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 07df294b51..07bf98aeea 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -409,10 +409,9 @@ let rec type_search t = function
let decl_type_search t l =
let one_decl = function
- | Dind(l,_) ->
- List.iter (fun (_,_,l) ->
- (List.iter (fun (_,l) ->
- List.iter (type_search t) l) l)) l
+ | Dind (_,{ind_packets=p}) ->
+ Array.iter
+ (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
| Dterm (_,_,u) -> type_search t u
| Dfix (_,_,v) -> Array.iter (type_search t) v
| Dtype (_,_,u) -> type_search t u
@@ -1205,19 +1204,19 @@ let ast_iter_references do_term do_cons do_type a =
| MLcast (_,t) -> type_iter_references do_type t
| _ -> ()
in iter a
-
+
let decl_iter_references do_term do_cons do_type =
let type_iter = type_iter_references do_type
and ast_iter = ast_iter_references do_term do_cons do_type in
- let cons_iter (r,l) = do_cons r; List.iter type_iter l in
- let ind_iter (_,r,l) =
- do_type r;
- (try List.iter do_term (find_proj ((kn_of_r r),0))
- with Not_found -> ());
- List.iter cons_iter l
+ let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in
+ let packet_iter ip p =
+ do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in
+ let ind_iter kn ind =
+ if ind.ind_info = Record then List.iter do_term (find_projections kn);
+ Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
in
function
- | Dind (l,_) -> List.iter ind_iter l
+ | Dind (kn,ind) -> ind_iter kn ind
| Dtype (r,_,t) -> do_type r; type_iter t
| Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
| Dfix(rv,c,t) ->
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2e81a52c9e..f168c57b80 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -198,7 +198,7 @@ let rec pp_expr par env args =
(hov 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
spc () ++ str "in") ++
spc () ++ hov 0 pp_a2))
- | MLglob r when is_proj r && args <> [] ->
+ | MLglob r when is_projection r && args <> [] ->
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
| MLglob r ->
@@ -210,13 +210,13 @@ let rec pp_expr par env args =
else pp_global r
| MLcons (r,args') ->
(try
- let projs = find_proj (kn_of_r r, 0) in
+ let projs = find_projections (kn_of_r r) in
pp_record_pat (projs, List.map (pp_expr true env []) args')
with Not_found ->
assert (args=[]);
let tuple = pp_tuple (pp_expr true env []) args' in
if Refset.mem r !cons_cofix then
- pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++ str ")")
+ pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
else pp_par par (pp_global r ++ spc () ++ tuple))
| MLcase (t, pv) ->
let r,_,_ = pv.(0) in
@@ -226,7 +226,7 @@ let rec pp_expr par env args =
(pp_expr false env [] t)
in
let record =
- try ignore (find_proj (kn_of_r r, 0)); true with Not_found -> false
+ try ignore (find_projections (kn_of_r r)); true with Not_found -> false
in
if Array.length pv = 1 && not record then
let s1,s2 = pp_one_pat env pv.(0) in
@@ -269,7 +269,7 @@ and pp_one_pat env (r,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
let expr = pp_expr (expr_needs_par t) env' [] t in
try
- let projs = find_proj (kn_of_r r,0) in
+ let projs = find_projections (kn_of_r r) in
pp_record_pat (projs, List.rev_map pr_id ids), expr
with Not_found ->
let args =
@@ -340,64 +340,79 @@ let pp_Dfix env (p,c,t) =
let pp_parameters l =
(pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-let pp_one_ind prefix (pl,name,cl) =
+let pp_one_ind prefix ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
- (pp_global r ++
- match l with
- | [] -> (mt ())
- | _ -> (str " of " ++
- prlist_with_sep
- (fun () -> (spc () ++ str "* "))
- (pp_type true pl) l))
+ hov 2 (str " | " ++ pp_global r ++
+ match l with
+ | [] -> mt ()
+ | _ -> (str " of " ++
+ prlist_with_sep
+ (fun () -> spc () ++ str "* ") (pp_type true pl) l))
in
- (pp_parameters pl ++ str prefix ++ pp_global name ++ str " =" ++
- if cl = [] then str " unit (* empty inductive *)"
- else (fnl () ++
- v 0 (str " | " ++
- prlist_with_sep (fun () -> (fnl () ++ str " | "))
- (fun c -> hov 2 (pp_constructor c)) cl)))
-
-let pp_ind il =
- str "type " ++
- prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "") il
- ++ fnl ()
-
-let pp_record ip pl l =
- let pl = rename_tvars keywords pl in
- str "type " ++ pp_parameters pl ++ pp_global (IndRef ip) ++ str " = { "++
+ pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++
+ if cv = [||] then str " unit (* empty inductive *)"
+ else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
+ (Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
+
+let pp_comment s = str "(* " ++ s ++ str " *)" ++ fnl ()
+
+let pp_logical_ind ip packet =
+ pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+ pp_comment (str "with constructors : " ++
+ prvect_with_sep spc Printer.pr_global
+ (Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types))
+
+let pp_singleton kn packet =
+ let l = rename_tvars keywords packet.ip_vars in
+ hov 0 (str "type " ++ spc () ++ pp_parameters l ++
+ pp_global (IndRef (kn,0)) ++ spc () ++ str "=" ++ spc () ++
+ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
+ pp_comment (str "singleton inductive, whose constructor was " ++
+ Printer.pr_global (ConstructRef ((kn,0),1))))
+
+let pp_record kn packet =
+ let l = List.combine (find_projections kn) packet.ip_types.(0) in
+ let projs = find_projections kn in
+ let pl = rename_tvars keywords packet.ip_vars in
+ str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
- (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l)
+ (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l)
++ str " }" ++ fnl ()
-let pp_coind_preamble (pl,name,_) =
+let pp_coind ip pl =
+ let r = IndRef ip in
let pl = rename_tvars keywords pl in
- pp_parameters pl ++ pp_global name ++ str " = " ++
- pp_parameters pl ++ str "__" ++ pp_global name ++ str " Lazy.t"
-
-let pp_coind il =
- str "type " ++
- prlist_with_sep (fun () -> fnl () ++ str "and ") pp_coind_preamble il ++
- fnl () ++ str "and " ++
- prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "__") il ++
- fnl ()
+ pp_parameters pl ++ pp_global r ++ str " = " ++
+ pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
+
+let rec pp_ind co first kn i ind =
+ if i >= Array.length ind.ind_packets then mt ()
+ else
+ let ip = (kn,i) in
+ let p = ind.ind_packets.(i) in
+ if p.ip_logical then
+ pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
+ else
+ str (if first then "type " else "and ") ++
+ (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++
+ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+ fnl () ++ pp_ind co false kn (i+1) ind
(*s Pretty-printing of a declaration. *)
let pp_decl = function
- | Dind ([], _) -> mt ()
- | Dind (i, true) ->
- List.iter
- (fun (_,_,l) ->
- List.iter (fun (r,_) ->
- cons_cofix := Refset.add r !cons_cofix) l) i;
- hov 0 (pp_coind i)
- | Dind ([vl, IndRef ip, [_,l]] as i, _) ->
- (try
- let projs = find_proj ip in
- hov 0 (pp_record ip vl (List.combine projs l))
- with Not_found -> hov 0 (pp_ind i))
- | Dind (i,_) -> hov 0 (pp_ind i)
+ | Dind (kn,i) as d ->
+ (match i.ind_info with
+ | Singleton -> pp_singleton kn i.ind_packets.(0)
+ | Record -> pp_record kn i.ind_packets.(0)
+ | Coinductive ->
+ let nop _ = ()
+ and add r = cons_cofix := Refset.add r !cons_cofix in
+ decl_iter_references nop add nop d;
+ hov 0 (pp_ind true true kn 0 i)
+ | Standard ->
+ hov 0 (pp_ind false true kn 0 i))
| Dtype (r, l, t) ->
let l = rename_tvars keywords l in
hov 0 (str "type" ++ spc () ++ pp_parameters l ++
@@ -407,7 +422,7 @@ let pp_decl = function
(* We compute renamings of [rv] before asking [empty_env ()]... *)
let ppv = Array.map pp_global rv in
hov 0 (pp_Dfix (empty_env ()) (ppv,defs,typs))
- | Dterm (r, a, t) when is_proj r ->
+ | Dterm (r, a, t) when is_projection r ->
let e = pp_global r in
(pp_val e t ++
hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl()))
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 75c70fd7f2..223bc77b38 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -17,32 +17,48 @@ open Goptions
open Libnames
open Util
open Pp
+open Miniml
+(*S Warning and Error messages. *)
-(*s Warning and Error messages. *)
-
-let error_axiom_scheme kn =
- errorlabstrm "axiom_scheme_message"
+let error_axiom_scheme r =
+ errorlabstrm "Extraction"
(str "Extraction cannot accept the type scheme axiom " ++ spc () ++
- Printer.pr_global (ConstRef kn) ++ spc () ++ str ".")
+ Printer.pr_global r ++ spc () ++ str ".")
-let error_axiom kn =
- errorlabstrm "axiom_message"
+let error_axiom r =
+ errorlabstrm "Extraction"
(str "You must specify an extraction for axiom" ++ spc () ++
- Printer.pr_global (ConstRef kn) ++ spc () ++ str "first.")
+ Printer.pr_global r ++ spc () ++ str "first.")
-let warning_axiom kn =
+let warning_axiom r =
Options.if_verbose warn
(str "This extraction depends on logical axiom" ++ spc () ++
- Printer.pr_global (ConstRef kn) ++ str "." ++ spc() ++
+ Printer.pr_global r ++ str "." ++ spc() ++
str "Having false logical axiom in the environment when extracting" ++
spc () ++ str "may lead to incorrect or non-terminating ML terms.")
let error_section () =
- errorlabstrm "section_message"
+ errorlabstrm "Extraction"
(str "You can't do that within a section. Close it and try again.")
-(*s AutoInline parameter *)
+let error_constant r =
+ errorlabstrm "Extraction"
+ (Printer.pr_global r ++ spc () ++ str "is not a constant.")
+
+let error_type_scheme r =
+ errorlabstrm "Extraction"
+ (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.")
+
+let error_inductive r =
+ errorlabstrm "Extraction"
+ (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+
+let error_nb_cons () =
+ errorlabstrm "Extraction" (str "Not the right number of constructors.")
+
+
+(*S Extraction AutoInline *)
let auto_inline_ref = ref true
@@ -55,7 +71,8 @@ let _ = declare_bool_option
optread = auto_inline;
optwrite = (:=) auto_inline_ref}
-(*s Optimize parameter *)
+
+(*S Extraction Optimize *)
let optim_ref = ref true
@@ -68,18 +85,8 @@ let _ = declare_bool_option
optread = optim;
optwrite = (:=) optim_ref}
-(*s Auxiliary functions *)
-let is_constant r = match r with
- | ConstRef _ -> true
- | _ -> false
-
-let check_constant r =
- if (is_constant r) then r
- else errorlabstrm "extract_constant"
- (Printer.pr_global r ++ spc () ++ str "is not a constant.")
-
-(*s Target Language *)
+(*S Extraction Lang *)
type lang = Ocaml | Haskell | Scheme | Toplevel
@@ -102,7 +109,8 @@ let _ = declare_summary "Extraction Lang"
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
-(*s Table for custom inlining *)
+
+(*S Extraction Inline/NoInline *)
let empty_inline_table = (Refset.empty,Refset.empty)
@@ -138,14 +146,15 @@ let _ = declare_summary "Extraction Inline"
let extraction_inline b l =
if Lib.sections_are_opened () then error_section ();
- let refs = List.map (fun x -> check_constant (Nametab.global x)) l in
+ let refs = List.map Nametab.global l in
+ List.iter (function ConstRef _ -> () | r -> error_constant r) refs;
Lib.add_anonymous_leaf (inline_extraction (b,refs))
(*s Printing part *)
let print_extraction_inline () =
let (i,n)= !inline_table in
- let i'= Refset.filter is_constant i in
+ let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
msg
(str "Extraction Inline:" ++ fnl () ++
Refset.fold
@@ -167,7 +176,8 @@ let (reset_inline,_) =
let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
-(*s Table for direct ML extractions. *)
+
+(*S Extract Constant/Inductive. *)
type kind = Term | Type | Ind | Construct
@@ -176,15 +186,11 @@ let check_term_or_type r = match r with
let env = Global.env () in
let typ = Environ.constant_type env sp in
let typ = Reduction.whd_betadeltaiota env typ in
- (match kind_of_term typ with
- | Sort _ -> (r,Type)
- | _ -> if not (Reduction.is_arity env typ) then (r,Term)
- else errorlabstrm "extract_constant"
- (Printer.pr_global r ++ spc () ++
- str "is a type scheme, not a type."))
- | _ -> errorlabstrm "extract_constant"
- (Printer.pr_global r ++ spc () ++ str "is not a constant.")
-
+ if isSort typ then (r,Type)
+ else if Reduction.is_arity env typ then error_type_scheme r
+ else (r,Term)
+ | _ -> error_constant r
+
let empty_extractions = (Refmap.empty, Refset.empty)
let extractions = ref empty_extractions
@@ -222,7 +228,6 @@ let _ = declare_summary "ML extractions"
init_function = (fun () -> extractions := empty_extractions);
survive_section = true }
-
(*s Grammar entries. *)
let extract_constant_inline inline r s =
@@ -237,8 +242,7 @@ let extract_inductive r (s,l) =
| IndRef ((kn,i) as ip) ->
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets.(i).mind_consnames in
- if n <> List.length l then
- error "Not the right number of constructors.";
+ if n <> List.length l then error_nb_cons ();
Lib.add_anonymous_leaf (inline_extraction (true,[g]));
Lib.add_anonymous_leaf (in_ml_extraction (g,Ind,s));
list_iter_i
@@ -246,31 +250,26 @@ let extract_inductive r (s,l) =
let g = ConstructRef (ip,succ j) in
Lib.add_anonymous_leaf (inline_extraction (true,[g]));
Lib.add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
- | _ ->
- errorlabstrm "extract_inductive"
- (Printer.pr_global g ++ spc () ++ str "is not an inductive type.")
+ | _ -> error_inductive g
-(*s Record Inductive tables. *)
-let record_type_table =
- ref (Gmap.empty : (inductive, global_reference list) Gmap.t)
+(*S The other tables: constants, inductives, records, ... *)
-let record_proj_table = ref Refset.empty
+(*s Constants tables. *)
-let add_record i l =
- record_type_table := Gmap.add i l !record_type_table;
- record_proj_table := List.fold_right Refset.add l !record_proj_table
+let terms = ref (KNmap.empty : ml_decl KNmap.t)
+let add_term kn d = terms := KNmap.add kn d !terms
+let lookup_term kn = KNmap.find kn !terms
-let find_proj i = Gmap.find i !record_type_table
+let types = ref (KNmap.empty : ml_schema KNmap.t)
+let add_type kn s = types := KNmap.add kn s !types
+let lookup_type kn = KNmap.find kn !types
-let is_proj r = Refset.mem r !record_proj_table
+(*s Inductives table. *)
-let _ = declare_summary "Extraction Record tables"
- { freeze_function = (fun () -> !record_type_table,!record_proj_table);
- unfreeze_function =
- (fun (x,y) -> record_type_table := x; record_proj_table := y);
- init_function = (fun () -> ());
- survive_section = true }
+let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let add_ind kn m = inductives := KNmap.add kn m !inductives
+let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
@@ -291,9 +290,32 @@ let is_recursor = function
| ConstRef kn -> KNset.mem kn !recursors
| _ -> false
-let _ = declare_summary "Extraction Recursors table"
- { freeze_function = (fun () -> !recursors);
- unfreeze_function = (fun x -> recursors := x);
- init_function = (fun () -> ());
+(*s Record tables. *)
+
+let records = ref (KNmap.empty : global_reference list KNmap.t)
+let projs = ref Refset.empty
+
+let add_record kn l =
+ records := KNmap.add kn l !records;
+ projs := List.fold_right Refset.add l !projs
+
+let find_projections kn = KNmap.find kn !records
+let is_projection r = Refset.mem r !projs
+
+(*s Tables synchronization. *)
+
+let freeze () = !terms, !types, !inductives, !recursors, !records, !projs
+
+let unfreeze (te,ty,id,re,rd,pr) =
+ terms:=te; types:=ty; inductives:=id; recursors:=re; records:=rd; projs:=pr
+
+let _ = declare_summary "Extraction tables"
+ { freeze_function = freeze;
+ unfreeze_function = unfreeze;
+ init_function = (fun () -> ());
survive_section = true }
+
+
+
+
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 3ffb74ac4b..e6495add6e 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -10,16 +10,18 @@
open Names
open Libnames
+open Miniml
(*s Warning and Error messages. *)
+val error_axiom_scheme : global_reference -> 'a
+val error_axiom : global_reference -> 'a
+val warning_axiom : global_reference -> unit
val error_section : unit -> 'a
-
-val error_axiom_scheme : kernel_name -> 'a
-
-val error_axiom : kernel_name -> 'a
-
-val warning_axiom : kernel_name -> unit
+val error_constant : global_reference -> 'a
+val error_type_scheme : global_reference -> 'a
+val error_inductive : global_reference -> 'a
+val error_nb_cons : unit -> 'a
(*s AutoInline parameter *)
@@ -32,46 +34,46 @@ val optim : unit -> bool
(*s Target language. *)
type lang = Ocaml | Haskell | Scheme | Toplevel
-
val lang : unit -> lang
(*s Table for custom inlining *)
val to_inline : global_reference -> bool
-
val to_keep : global_reference -> bool
(*s Table for direct ML extractions. *)
val is_ml_extraction : global_reference -> bool
-
val find_ml_extraction : global_reference -> string
-
val ml_extractions : unit -> Refset.t
-
val ml_type_extractions : unit -> (global_reference * string) list
-
val ml_term_extractions : unit -> (global_reference * string) list
(*s Extraction commands. *)
val extraction_language : lang -> unit
-
val extraction_inline : bool -> reference list -> unit
-
val print_extraction_inline : unit -> unit
-
val reset_extraction_inline : unit -> unit
-
val extract_constant_inline : bool -> reference -> string -> unit
-
val extract_inductive : reference -> string * string list -> unit
-(*s some tables. *)
+(*s Some table-related operations *)
+
+val add_term : kernel_name -> ml_decl -> unit
+val lookup_term : kernel_name -> ml_decl
-val add_record : inductive -> global_reference list -> unit
-val find_proj : inductive -> global_reference list
-val is_proj : global_reference -> bool
+val add_type : kernel_name -> ml_schema -> unit
+val lookup_type : kernel_name -> ml_schema
+
+val add_ind : kernel_name -> ml_ind -> unit
+val lookup_ind : kernel_name -> ml_ind
val add_recursors : kernel_name -> unit
val is_recursor : global_reference -> bool
+
+val add_record : kernel_name -> global_reference list -> unit
+val find_projections : kernel_name -> global_reference list
+val is_projection : global_reference -> bool
+
+
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 33e832af43..8c706cdf80 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -293,7 +293,7 @@ type 'x truc =
Definition test24:= (sigT Set [a:Set](option a)).
Extraction test24.
-(* type test24 = (unit, Obj.t option) sigT *)
+(* type test24 = (__, __ option) sigT *)
(** Coq term non strongly-normalizable after extraction *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 11:47:56 +0000