diff options
| -rw-r--r-- | .depend | 265 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | contrib/extraction/Extraction.v | 30 | ||||
| -rw-r--r-- | contrib/extraction/common.ml | 43 | ||||
| -rw-r--r-- | contrib/extraction/common.mli | 9 | ||||
| -rw-r--r-- | contrib/extraction/extract_env.ml | 181 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 241 | ||||
| -rw-r--r-- | contrib/extraction/extraction.mli | 4 | ||||
| -rw-r--r-- | contrib/extraction/haskell.ml | 20 | ||||
| -rw-r--r-- | contrib/extraction/miniml.mli | 10 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 127 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.mli | 12 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 19 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 46 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 6 | ||||
| -rw-r--r-- | contrib/extraction/test/Makefile.haskell | 2 | ||||
| -rwxr-xr-x | contrib/extraction/test/extract.haskell | 2 |
17 files changed, 541 insertions, 478 deletions
@@ -25,9 +25,6 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.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 kernel/declarations.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ @@ -48,6 +45,9 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi library/summary.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 kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -203,6 +203,7 @@ tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi +toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ kernel/names.cmi library/nametab.cmi kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ @@ -211,7 +212,6 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ pretyping/tacred.cmi kernel/term.cmi toplevel/coqinit.cmi: kernel/names.cmi toplevel/discharge.cmi: kernel/names.cmi -toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \ @@ -226,18 +226,18 @@ toplevel/recordobj.cmi: library/nametab.cmi 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/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.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 @@ -276,7 +276,8 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/term.cmi contrib/extraction/common.cmi: contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi + contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \ + lib/pp.cmi contrib/extraction/extraction.cmi: kernel/environ.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \ kernel/term.cmi @@ -319,18 +320,16 @@ config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx -dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \ - toplevel/cerrors.cmi pretyping/evd.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \ - proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ - pretyping/termops.cmi kernel/univ.cmi -dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \ - toplevel/cerrors.cmx pretyping/evd.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \ - proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ - pretyping/termops.cmx kernel/univ.cmx +dev/top_printers.cmo: parsing/ast.cmi toplevel/cerrors.cmi proofs/clenv.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/refiner.cmi kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi kernel/univ.cmi +dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/refiner.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx kernel/univ.cmx kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ kernel/closure.cmi @@ -429,34 +428,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: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ @@ -533,6 +522,16 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi +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/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ @@ -1205,18 +1204,20 @@ tactics/inv.cmo: proofs/clenv.cmi parsing/coqlib.cmi tactics/elim.cmi \ kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \ library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \ kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi tactics/wcclausenv.cmi tactics/inv.cmi + proofs/proof_type.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + tactics/wcclausenv.cmi tactics/inv.cmi tactics/inv.cmx: proofs/clenv.cmx parsing/coqlib.cmx tactics/elim.cmx \ kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \ library/global.cmx pretyping/inductiveops.cmx library/nameops.cmx \ kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi + proofs/proof_type.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + tactics/wcclausenv.cmx tactics/inv.cmi tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ @@ -1306,10 +1307,10 @@ tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi \ proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - tactics/tactics.cmi + pretyping/reductionops.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ @@ -1317,10 +1318,10 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx \ proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - tactics/tactics.cmi + pretyping/reductionops.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \ tactics/hipattern.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ @@ -1349,14 +1350,24 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.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/coqdep_lexer.cmo: config/coq_config.cmi tools/coqdep_lexer.cmx: config/coq_config.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 \ + kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi \ + pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \ + kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi +toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ + kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx \ + pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \ + kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi kernel/inductive.cmi library/lib.cmi \ @@ -1403,14 +1414,14 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \ library/nameops.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ lib/system.cmx toplevel/toplevel.cmx toplevel/vernac.cmx \ toplevel/coqinit.cmi -toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ - toplevel/cerrors.cmi library/lib.cmi library/library.cmi \ +toplevel/coqtop.cmo: toplevel/cerrors.cmi config/coq_config.cmi \ + toplevel/coqinit.cmi library/lib.cmi library/library.cmi \ toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \ library/states.cmi lib/system.cmi toplevel/toplevel.cmi \ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi -toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ - toplevel/cerrors.cmx library/lib.cmx library/library.cmx \ +toplevel/coqtop.cmx: toplevel/cerrors.cmx config/coq_config.cmx \ + toplevel/coqinit.cmx library/lib.cmx library/library.cmx \ toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ @@ -1433,16 +1444,6 @@ toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ lib/pp.cmx toplevel/recordobj.cmx pretyping/recordops.cmx \ kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/discharge.cmi -toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ - kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \ - kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi -toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ - kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \ - kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi @@ -1535,16 +1536,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.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/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1589,6 +1580,28 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.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/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi library/global.cmi \ kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \ @@ -1603,18 +1616,6 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/typeops.cmx lib/util.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 \ @@ -1673,11 +1674,11 @@ contrib/correctness/pextract.cmx: parsing/ast.cmx pretyping/evd.cmx \ toplevel/vernacinterp.cmx contrib/correctness/pextract.cmi contrib/correctness/pmisc.cmo: parsing/coqast.cmi library/declare.cmi \ pretyping/evarutil.cmi library/global.cmi library/nameops.cmi \ - kernel/names.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi \ + kernel/names.cmi lib/options.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi \ contrib/correctness/pmisc.cmi contrib/correctness/pmisc.cmx: parsing/coqast.cmx library/declare.cmx \ pretyping/evarutil.cmx library/global.cmx library/nameops.cmx \ - kernel/names.cmx lib/pp.cmx kernel/term.cmx lib/util.cmx \ + kernel/names.cmx lib/options.cmx lib/pp.cmx kernel/term.cmx lib/util.cmx \ contrib/correctness/pmisc.cmi contrib/correctness/pmlize.cmo: parsing/coqlib.cmi pretyping/evd.cmi \ library/global.cmi kernel/names.cmi contrib/correctness/past.cmi \ @@ -1831,20 +1832,22 @@ contrib/correctness/pwp.cmx: kernel/environ.cmx library/global.cmx \ contrib/correctness/putil.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/global.cmi \ +contrib/extraction/common.cmo: library/declare.cmi \ + contrib/extraction/extraction.cmi library/global.cmi \ contrib/extraction/haskell.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/table.cmi \ pretyping/termops.cmi lib/util.cmi contrib/extraction/common.cmi -contrib/extraction/common.cmx: library/global.cmx \ +contrib/extraction/common.cmx: library/declare.cmx \ + contrib/extraction/extraction.cmx library/global.cmx \ contrib/extraction/haskell.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/table.cmx \ pretyping/termops.cmx lib/util.cmx contrib/extraction/common.cmi contrib/extraction/extract_env.cmo: parsing/astterm.cmi \ - contrib/extraction/common.cmi pretyping/evd.cmi \ + contrib/extraction/common.cmi library/declare.cmi pretyping/evd.cmi \ contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \ @@ -1852,7 +1855,7 @@ contrib/extraction/extract_env.cmo: parsing/astterm.cmi \ kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \ contrib/extraction/extract_env.cmi contrib/extraction/extract_env.cmx: parsing/astterm.cmx \ - contrib/extraction/common.cmx pretyping/evd.cmx \ + contrib/extraction/common.cmx library/declare.cmx pretyping/evd.cmx \ contrib/extraction/extraction.cmx library/global.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \ @@ -1884,13 +1887,13 @@ contrib/extraction/haskell.cmx: contrib/extraction/miniml.cmi \ library/nametab.cmx contrib/extraction/ocaml.cmx lib/options.cmx \ lib/pp.cmx kernel/term.cmx lib/util.cmx contrib/extraction/haskell.cmi contrib/extraction/mlutil.cmo: kernel/declarations.cmi \ - contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi lib/pp.cmi parsing/printer.cmi \ + contrib/extraction/miniml.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi \ contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \ contrib/extraction/mlutil.cmi contrib/extraction/mlutil.cmx: kernel/declarations.cmx \ - contrib/extraction/miniml.cmi kernel/names.cmx library/nametab.cmx \ - lib/options.cmx lib/pp.cmx parsing/printer.cmx \ + contrib/extraction/miniml.cmi library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx \ contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \ contrib/extraction/mlutil.cmi contrib/extraction/ocaml.cmo: contrib/extraction/miniml.cmi \ @@ -1966,13 +1969,14 @@ contrib/interface/blast.cmx: parsing/astterm.cmx tactics/auto.cmx \ toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ contrib/interface/blast.cmi contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ - parsing/astterm.cmi contrib/interface/blast.cmi pretyping/classops.cmi \ - toplevel/command.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \ - contrib/interface/dad.cmi contrib/interface/debug_tac.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - toplevel/cerrors.cmi pretyping/evd.cmi library/global.cmi \ - contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \ + parsing/astterm.cmi contrib/interface/blast.cmi toplevel/cerrors.cmi \ + pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \ + contrib/interface/ctast.cmo contrib/interface/dad.cmi \ + contrib/interface/debug_tac.cmi kernel/declarations.cmi \ + library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ + library/global.cmi contrib/interface/history.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi \ + toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \ contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi contrib/interface/pbp.cmi proofs/pfedit.cmi \ lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \ @@ -1985,13 +1989,14 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ contrib/interface/vtp.cmi contrib/interface/xlate.cmi contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ - parsing/astterm.cmx contrib/interface/blast.cmx pretyping/classops.cmx \ - toplevel/command.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \ - contrib/interface/dad.cmx contrib/interface/debug_tac.cmx \ - kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - toplevel/cerrors.cmx pretyping/evd.cmx library/global.cmx \ - contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \ + parsing/astterm.cmx contrib/interface/blast.cmx toplevel/cerrors.cmx \ + pretyping/classops.cmx toplevel/command.cmx parsing/coqast.cmx \ + contrib/interface/ctast.cmx contrib/interface/dad.cmx \ + contrib/interface/debug_tac.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ + library/global.cmx contrib/interface/history.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx \ + toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \ contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx contrib/interface/pbp.cmx proofs/pfedit.cmx \ lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \ @@ -2023,12 +2028,12 @@ contrib/interface/dad.cmx: parsing/astterm.cmx contrib/interface/ctast.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/dad.cmi -contrib/interface/debug_tac.cmo: parsing/ast.cmi parsing/coqast.cmi \ - toplevel/cerrors.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ +contrib/interface/debug_tac.cmo: parsing/ast.cmi toplevel/cerrors.cmi \ + parsing/coqast.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ lib/util.cmi contrib/interface/debug_tac.cmi -contrib/interface/debug_tac.cmx: parsing/ast.cmx parsing/coqast.cmx \ - toplevel/cerrors.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ +contrib/interface/debug_tac.cmx: parsing/ast.cmx toplevel/cerrors.cmx \ + parsing/coqast.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ lib/util.cmx contrib/interface/debug_tac.cmi contrib/interface/history.cmo: contrib/interface/paths.cmi \ @@ -2054,14 +2059,14 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ contrib/interface/name_to_ast.cmi contrib/interface/parse.cmo: contrib/interface/ascent.cmi \ - config/coq_config.cmi contrib/interface/ctast.cmo toplevel/cerrors.cmi \ + toplevel/cerrors.cmi config/coq_config.cmi contrib/interface/ctast.cmo \ parsing/esyntax.cmi library/libobject.cmi library/library.cmi \ contrib/interface/line_parser.cmi toplevel/metasyntax.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \ lib/pp.cmi lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \ contrib/interface/xlate.cmi contrib/interface/parse.cmx: contrib/interface/ascent.cmi \ - config/coq_config.cmx contrib/interface/ctast.cmx toplevel/cerrors.cmx \ + toplevel/cerrors.cmx config/coq_config.cmx contrib/interface/ctast.cmx \ parsing/esyntax.cmx library/libobject.cmx library/library.cmx \ contrib/interface/line_parser.cmx toplevel/metasyntax.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \ @@ -2087,6 +2092,14 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.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: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -2107,14 +2120,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.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 \ @@ -2211,8 +2216,6 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ parsing/printer.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/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi library/nameops.cmi \ @@ -2233,6 +2236,8 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.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 kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/correctness/psyntax.cmo: parsing/grammar.cma contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo @@ -210,8 +210,8 @@ EXTRACTIONCMO=contrib/extraction/table.cmo\ contrib/extraction/mlutil.cmo\ contrib/extraction/ocaml.cmo \ contrib/extraction/haskell.cmo \ - contrib/extraction/common.cmo \ contrib/extraction/extraction.cmo \ + contrib/extraction/common.cmo \ contrib/extraction/extract_env.cmo CORRECTNESSCMO=contrib/correctness/pmisc.cmo \ diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index b51d683ac..e18e48efd 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -17,25 +17,27 @@ Grammar vernac vernac : ast := (* Monolithic extraction to a file *) | extr_file [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] - -> [ (ExtractionFile "ocaml" $f ($LIST $l)) ] -| haskell_extr_file - [ "Haskell" "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] - -> [ (ExtractionFile "haskell" $f ($LIST $l)) ] + -> [ (ExtractionFile $f ($LIST $l)) ] (* Modular extraction (one Coq module = one ML module) *) | extr_module [ "Extraction" "Module" identarg($m) "." ] - -> [ (ExtractionModule "ocaml" $m) ] -| haskell_extr_module - [ "Haskell" "Extraction" "Module" identarg($m) "." ] - -> [ (ExtractionModule "haskell" $m) ] + -> [ (ExtractionModule $m) ] | rec_extr_module [ "Recursive" "Extraction" "Module" identarg($m) "." ] - -> [ (RecursiveExtractionModule "ocaml" $m) ] -| rec_haskell_extr_module - [ "Haskell" "Recursive" "Extraction" "Module" identarg($m) "." ] - -> [ (RecursiveExtractionModule "haskell" $m) ] + -> [ (RecursiveExtractionModule $m) ] +(* Target Language *) + +| extraction_ocaml + [ "Extraction" "Language" "Ocaml" "." ] + -> [ (ExtractionLangOcaml) ] +| extraction_haskell + [ "Extraction" "Language" "Haskell" "." ] + -> [ (ExtractionLangHaskell) ] +| extraction_toplevel + [ "Extraction" "Language" "Toplevel" "." ] + -> [ (ExtractionLangToplevel) ] (* Custom inlining directives *) | inline_constant @@ -54,7 +56,6 @@ Grammar vernac vernac : ast := [ "Reset" "Extraction" "Inline" "."] -> [ (ResetExtractionInline) ] - (* Overriding of a Coq object by an ML one *) | extract_constant [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] @@ -81,4 +82,5 @@ with idorstring_list: ast list := with idorstring : ast := ids_ident [ identarg($id) ] -> [ $id ] | ids_string [ stringarg($s) ] -> [ $s ] -.
\ No newline at end of file +. + diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 7dba81ff2..130868591 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -14,6 +14,7 @@ open Nameops open Miniml open Table open Mlutil +open Extraction open Ocaml open Nametab open Util @@ -25,12 +26,6 @@ let current_module = ref (id_of_string "") let is_construct = function ConstructRef _ -> true | _ -> false -let sp_of_r r = match r with - | ConstRef sp -> sp - | IndRef (sp,_) -> sp - | ConstructRef ((sp,_),_) -> sp - | _ -> assert false - let qualid_of_dirpath d = let dir,id = split_dirpath d in make_qualid dir id @@ -142,7 +137,6 @@ let cache r f = (*s Renaming issues at toplevel *) module ToplevelParams = struct - let toplevel = true let globals () = Idset.empty let rename_global r _ = Termops.id_of_global (Global.env()) r let pp_global r _ _ = Printer.pr_global r @@ -152,8 +146,6 @@ end module MonoParams = struct - let toplevel = false - let globals () = !global_ids let rename_global_id id = @@ -179,8 +171,6 @@ end module ModularParams = struct - let toplevel = false - let globals () = !global_ids let clash r id = @@ -220,7 +210,6 @@ module ModularParams = struct end - module ToplevelPp = Ocaml.Make(ToplevelParams) module OcamlMonoPp = Ocaml.Make(MonoParams) @@ -229,19 +218,27 @@ module OcamlModularPp = Ocaml.Make(ModularParams) module HaskellMonoPp = Haskell.Make(MonoParams) module HaskellModularPp = Haskell.Make(ModularParams) +let pp_comment s = match lang () with + | Haskell -> str "-- " ++ s ++ fnl () + | Ocaml | Toplevel -> str "(* " ++ s ++ str " *)" ++ fnl () + +let pp_logical_ind r = + pp_comment (Printer.pr_global r ++ str " : logical inductive") (*s Extraction to a file. *) let extract_to_file f prm decls = - let preamble,keyw = match prm.lang with + let preamble,keyw = match lang () with | Ocaml -> Ocaml.preamble,Ocaml.keywords | Haskell -> Haskell.preamble,Haskell.keywords + | _ -> assert false in - let pp_decl = match prm.lang,prm.modular with + let pp_decl = match lang (),prm.modular with | Ocaml, false -> OcamlMonoPp.pp_decl | Ocaml, _ -> OcamlModularPp.pp_decl | Haskell, false -> HaskellMonoPp.pp_decl | Haskell, _ -> HaskellModularPp.pp_decl + | _ -> assert false in let used_modules = if prm.modular then Idset.remove prm.mod_name (decl_get_modules decls) @@ -252,17 +249,22 @@ let extract_to_file f prm decls = Hashtbl.clear renamings; keywords := keyw; global_ids := keyw; - let cout = open_out f in + let cout = match f with + | None -> stdout + | Some f -> open_out f in let ft = Pp_control.with_output_to cout in + if not prm.modular then + List.iter (fun r -> pp_with ft (pp_logical_ind r)) + (List.filter declaration_is_logical_ind prm.to_appear); pp_with ft (preamble prm used_modules (decl_print_prop decls)); begin try List.iter (fun d -> msgnl_with ft (pp_decl d)) decls with e -> - pp_flush_with ft (); close_out cout; raise e + pp_flush_with ft (); if f <> None then close_out cout; raise e end; pp_flush_with ft (); - close_out cout; + if f <> None then close_out cout; (*i (* names resolution *) @@ -276,3 +278,10 @@ let extract_to_file f prm decls = pp_flush_with ft (); close_out cout; i*) + + + + + + + diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 98d91cd71..6835d2e97 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -8,19 +8,22 @@ (*i $Id$ i*) +open Pp open Miniml open Mlutil open Names open Nametab module ToplevelPp : Mlpp - -val sp_of_r : global_reference -> section_path +module OcamlMonoPp : Mlpp +module HaskellMonoPp : Mlpp val is_long_module : dir_path -> global_reference -> bool val short_module : global_reference -> identifier +val pp_logical_ind : global_reference -> std_ppcmds + val extract_to_file : - string -> extraction_params -> ml_decl list -> unit + string option -> extraction_params -> ml_decl list -> unit diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 361eac76f..9838a79f0 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -138,7 +138,7 @@ and visit_type m eenv t = | Tglob r -> visit_reference m eenv r | Tapp l -> List.iter visit l | Tarr (t1,t2) -> visit t1; visit t2 - | Tvar _ | Texn _ | Tprop | Tarity -> () + | Tvar _ | Tprop | Tarity -> () in visit t @@ -165,12 +165,9 @@ and visit_inductive m eenv inds = List.iter visit_ind inds and visit_decl m eenv = function - | Dtype (inds,_) -> - visit_inductive m eenv inds - | Dabbrev (_,_,t) -> - visit_type m eenv t - | Dglob (_,a) -> - visit_ast m eenv a + | Dtype (inds,_) -> visit_inductive m eenv inds + | Dabbrev (_,_,t) -> visit_type m eenv t + | Dglob (_,a) -> visit_ast m eenv a | Dcustom _ -> () (*s Recursive extracted environment for a list of reference: we just @@ -195,16 +192,8 @@ let modules_extract_env m = vernacular command is \verb!Extraction! [term]. Whenever [term] is a global, its definition is displayed. *) -let refs_set_of_list l = List.fold_right Refset.add l Refset.empty - let decl_of_refs refs = List.map extract_declaration (extract_env refs) -let local_optimize refs = - let prm = - { lang = Ocaml ; toplevel = true; modular = false; - mod_name = id_of_string ""; to_appear = refs} in - optimize prm (decl_of_refs refs) - let print_user_extract r = msgnl (str "User defined extraction:" ++ spc () ++ str (find_ml_extraction r) ++ fnl ()) @@ -216,15 +205,35 @@ let decl_in_r r0 = function | Dtype ([],_) -> false | Dcustom (r,_) -> r = r0 +let pp_decl d = match lang () with + | Ocaml -> OcamlMonoPp.pp_decl d + | Haskell -> HaskellMonoPp.pp_decl d + | Toplevel -> ToplevelPp.pp_decl d + +let pp_ast a = match lang () with + | Ocaml -> OcamlMonoPp.pp_ast a + | Haskell -> HaskellMonoPp.pp_ast a + | Toplevel -> ToplevelPp.pp_ast a + +let pp_type t = match lang () with + | Ocaml -> OcamlMonoPp.pp_type t + | Haskell -> HaskellMonoPp.pp_type t + | Toplevel -> ToplevelPp.pp_type t + let extract_reference r = if is_ml_extraction r then print_user_extract r else - let d = list_last (local_optimize [r]) in - msgnl (ToplevelPp.pp_decl - (if (decl_in_r r d) || d = Dtype([],true) || d = Dtype([],false) - then d - else List.find (decl_in_r r) (local_optimize [r]))) + if declaration_is_logical_ind r then + msgnl (pp_logical_ind r) + else + let prm = + { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in + let decls = optimize prm (decl_of_refs [r]) in + let d = list_last decls in + let d = if (decl_in_r r d) then d + else List.find (decl_in_r r) decls + in msgnl (pp_decl d) let _ = vinterp_add "Extraction" @@ -240,59 +249,53 @@ let _ = (* Otherwise, output the ML type or expression *) | _ -> match extract_constr (Global.env()) c with - | Emltype (t,_,_) -> msgnl (ToplevelPp.pp_type t) - | Emlterm a -> msgnl (ToplevelPp.pp_ast (normalize a))) + | Emltype (t,_,_) -> msgnl (pp_type t) + | Emlterm a -> msgnl (pp_ast (normalize a))) | _ -> assert false) (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) +let mono_extraction (f,m) vl = + let refs = refs_of_vargl vl in + let prm = {modular=false; mod_name = m; to_appear= refs} in + let decls = decl_of_refs refs in + let decls = add_ml_decls prm decls in + let decls = optimize prm decls in + extract_to_file f prm decls + let _ = vinterp_add "ExtractionRec" - (fun vl () -> - let rl = refs_of_vargl vl in - let ml_rl = List.filter is_ml_extraction rl in - let rl = List.filter (fun x -> not (is_ml_extraction x)) rl in - let dl = local_optimize rl in - List.iter print_user_extract ml_rl ; - List.iter (fun d -> msgnl (ToplevelPp.pp_decl d)) dl) + (fun vl () -> mono_extraction (None,id_of_string "Main") vl) (*s Extraction to a file (necessarily recursive). The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. We just call [extract_to_file] on the saturated environment. *) -let lang_to_lang = function - | "ocaml" -> Ocaml - | "haskell" -> Haskell - | _ -> assert false - -let lang_suffix = function +let lang_suffix () = match lang () with | Ocaml -> "ml" | Haskell -> "hs" + | Toplevel -> assert false -let filename f lang = - let s = lang_suffix lang in - if Filename.check_suffix f s then f,id_of_string (Filename.chop_suffix f s) - else f^"."^s,id_of_string f +let filename f = + let s = lang_suffix () in + if Filename.check_suffix f s then Some f,id_of_string (Filename.chop_suffix f s) + else Some (f^"."^s),id_of_string f + +let lang_error () = + errorlabstrm "extraction_language" + (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." + ++ fnl () ++ + str "You should use Extraction Language Ocaml or Haskell before.") let _ = vinterp_add "ExtractionFile" (function - | VARG_STRING lang :: VARG_STRING f :: vl -> + | VARG_STRING f :: vl -> (fun () -> - let lang = lang_to_lang lang in - let f,m = filename f lang in - let refs = refs_of_vargl vl in - let prm = {lang=lang; - toplevel=false; - modular=false; - mod_name = m; - to_appear= refs} in - let decls = decl_of_refs refs in - let decls = add_ml_decls prm decls in - let decls = optimize prm decls in - extract_to_file f prm decls) + if lang () = Toplevel then lang_error () + else mono_extraction (filename f) vl) | _ -> assert false) (*s Extraction of a module. The vernacular command is @@ -305,29 +308,27 @@ let decl_in_m m = function | Dtype ([],_) -> false | Dcustom (r,_) -> is_long_module m r -let module_file_name m = function +let module_file_name m = match lang () with | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml" | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs" + | Toplevel -> assert false let _ = vinterp_add "ExtractionModule" (function - | [VARG_STRING lang; VARG_IDENTIFIER m] -> + | [VARG_IDENTIFIER m] -> (fun () -> - let lang = lang_to_lang lang in - let dir_m = module_of_id m in - let f = module_file_name m lang in - let prm = {lang=lang; - toplevel=false; - modular=true; - mod_name= m; - to_appear= []} in - let rl = extract_module dir_m in - let decls = optimize prm (decl_of_refs rl) in - let decls = add_ml_decls prm decls in - check_one_module dir_m decls; - let decls = List.filter (decl_in_m dir_m) decls in - extract_to_file f prm decls) + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let f = module_file_name m in + let prm = {modular=true; mod_name=m; to_appear=[]} in + let rl = extract_module dir_m in + let decls = optimize prm (decl_of_refs rl) in + let decls = add_ml_decls prm decls in + check_one_module dir_m decls; + let decls = List.filter (decl_in_m dir_m) decls in + extract_to_file (Some f) prm decls) | _ -> assert false) (*s Recursive Extraction of all the modules [M] depends on. @@ -336,30 +337,24 @@ let _ = let _ = vinterp_add "RecursiveExtractionModule" (function - | [VARG_STRING lang; VARG_IDENTIFIER m] -> + | [VARG_IDENTIFIER m] -> (fun () -> - let lang = lang_to_lang lang in - let dir_m = module_of_id m in - let modules,refs = - modules_extract_env dir_m in - check_modules modules; - let dummy_prm = {lang=lang; - toplevel=false; - modular=true; - mod_name=m; - to_appear= []} in - let decls = optimize dummy_prm (decl_of_refs refs) in - let decls = add_ml_decls dummy_prm decls in - Dirset.iter - (fun m -> - let short_m = snd (split_dirpath m) in - let f = module_file_name short_m lang in - let prm = {lang=lang; - toplevel=false; - modular=true; - mod_name=short_m; - to_appear= []} in - let decls = List.filter (decl_in_m m) decls in - if decls <> [] then extract_to_file f prm decls) - modules) + if lang () = Toplevel then lang_error () + else + let dir_m = module_of_id m in + let modules,refs = + modules_extract_env dir_m in + check_modules modules; + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let decls = optimize dummy_prm (decl_of_refs refs) in + let decls = add_ml_decls dummy_prm decls in + Dirset.iter + (fun m -> + let short_m = snd (split_dirpath m) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + let decls = List.filter (decl_in_m m) decls in + if decls <> [] then extract_to_file (Some f) prm decls) + modules) | _ -> assert false) + diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 4de693eb0..a52000341 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -242,6 +242,47 @@ let decompose_lam_eta n env c = let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in (rb, e) +(*s TODO commentaires *) + +let prop_abstract_1 f = + let rec abs rels i = function + | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels) + | (_,Arity) :: l -> abs rels i l + | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l) + | (Logic,_) :: l -> MLlam (prop_name, abs rels (succ i) l) + in abs [] 1 + +let prop_abstract_2 f = + let rec abs rels i = function + | [] -> f i (List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels) + | (_,Arity) :: l -> abs rels i l + | (Info,_) :: l -> MLlam (anonymous, abs (MLrel i :: rels) (succ i) l) + | (Logic,_) :: l -> MLlam (prop_name, abs (MLprop :: rels) (succ i) l) + in abs [] 1 + + +(*s Abstraction of an constant. *) + +let abstract_const sp s = + if List.mem default s then + prop_abstract_1 (fun a -> MLapp(MLglob (ConstRef sp), a)) s + else MLglob (ConstRef sp) + +(*s The opposite function. *) + +let eta_expanse_w_prop e s = + let s = List.filter (function (_,NotArity) -> true | _ -> false) s in + let ids,e = collect_lams e in + let m = List.length ids in + assert (m <= (List.length s)); + let _,s = list_chop m s in + let core = if s <> [] then + prop_abstract_2 (fun i a -> MLapp (ml_lift (i-1) e,a)) s + else e + in let new_e = named_lams core ids in + try + let new_e,_,_ = kill_prop_aux new_e in new_e + with Impossible -> new_e (*s Error message when extraction ends on an axiom. *) @@ -283,15 +324,20 @@ let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table let constant_table = ref (Gmap.empty : (section_path, extraction_result) Gmap.t) +let signature_table = + ref (Gmap.empty : (section_path, signature) Gmap.t) + (* Tables synchronization. *) let freeze () = - !inductive_extraction_table, !constructor_extraction_table, !constant_table + !inductive_extraction_table, !constructor_extraction_table, + !constant_table, !signature_table -let unfreeze (it,cst,ct) = +let unfreeze (it,cst,ct,st) = inductive_extraction_table := it; constructor_extraction_table := cst; - constant_table := ct + constant_table := ct; + signature_table := st let _ = declare_summary "Extraction tables" { freeze_function = freeze; @@ -515,6 +561,14 @@ and signature_rec env c args = | Var _ -> section_message () | _ -> assert false +(*s signature of a section path *) + +and signature_of_sp sp typ = + try + Gmap.find sp !signature_table + with Not_found -> + let s = signature (Global.env()) typ in + signature_table := Gmap.add sp s !signature_table; s (*s Extraction of a term. Precondition: [c] has a type which is not an arity. @@ -570,11 +624,11 @@ and extract_term_info_wt env ctx c t = | Rel n -> MLrel (renum_db ctx n) | Const sp -> - MLglob (ConstRef sp) + abstract_const sp (signature_of_sp sp t) | App (f,a) -> extract_app env ctx f a | Construct cp -> - abstract_constructor cp + abstract_constructor cp (signature_of_constructor cp) | Case ({ci_ind=ip},_,c,br) -> extract_case env ctx ip c br | Fix ((_,i),recd) -> @@ -586,9 +640,8 @@ and extract_term_info_wt env ctx c t = | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false | Var _ -> section_message () - -(* Abstraction of an inductive constructor: +(*s Abstraction of an inductive constructor: \begin{itemize} \item In ML, contructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, @@ -601,22 +654,16 @@ and extract_term_info_wt env ctx c t = produces: [fun ]$p_1 \ldots p_n ~ x_1 \ldots x_n $[-> C(]$x_{i_1},\ldots, x_{i_k}$[)]. - This ML term will be reduced later on when applied, see [mlutil.ml]. *) - -and abstract_constructor cp = - let s,n = signature_of_constructor cp in - let rec abstract rels i = function - | [] -> - let rels = List.rev_map (fun x -> MLrel (i-x)) rels in - MLcons (ConstructRef cp, rels) - | (Info,NotArity) :: l -> - MLlam (id_of_name Anonymous, abstract (i :: rels) (succ i) l) - | (Logic,NotArity) :: l -> - MLlam (id_of_name Anonymous, abstract rels (succ i) l) - | (_,Arity) :: l -> - abstract rels i l - in - anonym_lams (ml_lift n (abstract [] 1 s)) n + This ML term will be reduced later on when applied, see [mlutil.ml]. + + In the special case of a informative singleton inductive, [C] is identity *) + +and abstract_constructor cp (s,n) = + let f = if is_singleton_constructor cp then + function [x] -> x | _ -> assert false + else + fun a -> MLcons (ConstructRef cp, a) + in anonym_lams (ml_lift n (prop_abstract_1 f s)) n (* Extraction of a case *) @@ -644,24 +691,31 @@ and extract_case env ctx ip c br = in (ConstructRef cp, ids, e') in - (* [c] has an inductive type, not an arity type *) - (match extract_term env ctx c with - | Rmlterm a -> - MLcase (a, Array.mapi extract_branch br) - | Rprop -> - (* Logical singleton case: *) - if Array.length br = 0 then - MLcase (MLprop, [||]) (* to be recognize later on as an empty case *) - else begin - (* [match c with C i j k -> t] becomes [t'] *) - assert (Array.length br = 1); - let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in - let env' = push_rels_assum rb env in - (* We know that all arguments are logic. *) - let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in - extract_constr_to_term env' ctx' e - end) - + if br = [||] then + MLexn "absurd case" + else + (* [c] has an inductive type, not an arity type *) + match extract_term env ctx c with + | Rmlterm a when is_singleton_inductive ip -> + (* Informative singleton case: *) + (* [match c with C i -> t] becomes [let i = c' in t'] *) + assert (Array.length br = 1); + let (_,ids,e') = extract_branch 0 br.(0) in + assert (List.length ids = 1); + MLletin (List.hd ids,a,e') + | Rmlterm a -> + (* Standard case: we apply [extract_branch]. *) + MLcase (a, Array.mapi extract_branch br) + | Rprop -> + (* Logical singleton case: *) + (* [match c with C i j k -> t] becomes [t'] *) + assert (Array.length br = 1); + let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in + let env' = push_rels_assum rb env in + (* We know that all arguments are logic. *) + let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in + extract_constr_to_term env' ctx' e + (* Extraction of a (co)-fixpoint *) @@ -772,25 +826,15 @@ and extract_constant sp = | (Logic,NotArity) -> Emlterm MLprop (* Axiom? I don't mind! *) | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[])) (* Idem *) | Some body -> - let e = extract_constr_wt env body typ in - let e = eta_expanse e typ in - constant_table := Gmap.add sp e !constant_table; + let e = match extract_constr_wt env body typ with + | Emlterm MLprop as e -> e + | Emlterm MLarity as e -> e + | Emlterm a -> + Emlterm (eta_expanse_w_prop a (signature_of_sp sp typ)) + | e -> e + in constant_table := Gmap.add sp e !constant_table; e -(*s Eta-expansion to bypass ML type inference limitations (due to possible - polymorphic references, the ML type system does not generalize all - type variables that could be generalized). *) - -and eta_expanse ec typ = match ec with - | Emlterm (MLlam _) -> ec - | Emlterm (MLfix _) -> ec - | Emlterm a -> - (match extract_type (Global.env()) typ with - | Tmltype (Tarr _, _) -> - Emlterm (MLlam (anonymous, MLapp (a, [MLrel 1]))) - | _ -> ec) - | _ -> ec - (*s Extraction of an inductive. *) and extract_inductive ((sp,_) as i) = @@ -805,6 +849,22 @@ and signature_of_constructor cp = match extract_constructor cp with | Cprop -> assert false | Cml (_,s,n) -> (s,n) +(* 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 ind = + let (mib,mip) = Global.lookup_inductive ind in + mib.mind_finite && + (mib.mind_ntypes = 1) && + (Array.length mip.mind_consnames = 1) && + match extract_constructor (ind,1) with + | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt) + | _ -> false + +and is_singleton_constructor ((sp,i),_) = + is_singleton_inductive (sp,i) + and extract_mib sp = let ind = (sp,0) in if not (Gmap.mem ind !inductive_extraction_table) then begin @@ -873,7 +933,7 @@ and extract_mib sp = | Iprop -> () | Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l)); done; - (* Fourth pass: we update also in the constructors table *) + (* Fourth pass: we also update the constructors table *) for i = 0 to mib.mind_ntypes-1 do let ip = (sp,i) in for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do @@ -890,28 +950,40 @@ and extract_mib sp = and extract_inductive_declaration sp = extract_mib sp; - let mib = Global.lookup_mind sp in - let one_ind ip n = - iterate_for (-n) (-1) - (fun j l -> - let cp = (ip,-j) in - match lookup_constructor_extraction cp with - | Cprop -> assert false - | Cml (t,_,_) -> (ConstructRef cp, t)::l) [] - in - let l = - iterate_for (1 - mib.mind_ntypes) 0 - (fun i acc -> - let ip = (sp,-i) in - let nc = Array.length mib.mind_packets.(-i).mind_consnames in - match lookup_inductive_extraction ip with - | Iprop -> acc - | Iml (_,vl) -> - (List.rev vl, IndRef ip, one_ind ip nc) :: acc) - [] - in - Dtype (l, not mib.mind_finite) - + let ip = (sp,0) in + if is_singleton_inductive ip then + let t = match lookup_constructor_extraction (ip,1) with + | Cml ([t],_,_)-> t + | _ -> assert false + in + let vl = match lookup_inductive_extraction ip with + | Iml (_,vl) -> vl + | _ -> assert false + in + Dabbrev (IndRef ip,vl,t) + else + let mib = Global.lookup_mind sp in + let one_ind ip n = + iterate_for (-n) (-1) + (fun j l -> + let cp = (ip,-j) in + match lookup_constructor_extraction cp with + | Cprop -> assert false + | Cml (t,_,_) -> (ConstructRef cp, t)::l) [] + in + let l = + iterate_for (1 - mib.mind_ntypes) 0 + (fun i acc -> + let ip = (sp,-i) in + let nc = Array.length mib.mind_packets.(-i).mind_consnames in + match lookup_inductive_extraction ip with + | Iprop -> acc + | Iml (_,vl) -> + (List.rev vl, IndRef ip, one_ind ip nc) :: acc) + [] + in + Dtype (l, not mib.mind_finite) + (*s Extraction of a global reference i.e. a constant or an inductive. *) let extract_declaration r = match r with @@ -922,3 +994,10 @@ let extract_declaration r = match r with | IndRef (sp,_) -> extract_inductive_declaration sp | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp | VarRef _ -> assert false + +(*s Check whether a global reference corresponds to a logical inductive. *) + +let declaration_is_logical_ind = function + | IndRef ip -> extract_inductive ip = Iprop + | ConstructRef cp -> extract_constructor cp = Cprop + | _ -> false diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index 39f8d08b7..87f97641c 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -37,3 +37,7 @@ val extract_constr : env -> constr -> extraction_result (*s ML declaration corresponding to a Coq reference. *) val extract_declaration : global_reference -> ml_decl + +(*s Check whether a global reference corresponds to a logical inductive. *) + +val declaration_is_logical_ind : global_reference -> bool diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 7abccdf5d..53c1b4bc5 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -87,7 +87,6 @@ let rec pp_type par ren t = (open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2 ++ close_par par) | Tglob r -> pp_type_global r - | Texn s -> (str ("() -- " ^ s) ++ fnl ()) | Tprop -> str "Prop" | Tarity -> str "Arity" in @@ -234,21 +233,22 @@ let pp_one_inductive (pl,name,cl) = (fun () -> (str " ")) (pp_type true ren) l)) in (str (if cl = [] then "type " else "data ") ++ - pp_type_global name ++ str " " ++ - prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++ - (if pl = [] then (mt ()) else (str " ")) ++ - (v 0 (str "= " ++ - prlist_with_sep (fun () -> (fnl () ++ str " | ")) - pp_constructor cl))) - + pp_type_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))) + let pp_inductive il = (prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ()) (*s Pretty-printing of a declaration. *) let pp_decl = function - | Dtype ([], _) -> - (mt ()) + | Dtype ([], _) -> mt () | Dtype (i, _) -> hov 0 (pp_inductive i) | Dabbrev (r, l, t) -> diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 7c72bde37..60d5baf40 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -22,7 +22,6 @@ type ml_type = | Tapp of ml_type list | Tarr of ml_type * ml_type | Tglob of global_reference - | Texn of string | Tprop | Tarity @@ -56,24 +55,17 @@ type ml_decl = | Dglob of global_reference * ml_ast | Dcustom of global_reference * string -(*s Target language. *) - -type lang = Ocaml | Haskell - (*s Pretty-printing of MiniML in a given concrete syntax is parameterized by a function [pp_global] that pretty-prints global references. The resulting pretty-printer is a module of type [Mlpp] providing functions to print types, terms and declarations. *) type extraction_params = - { lang : lang; - toplevel : bool; - modular : bool; + { modular : bool; mod_name : identifier; to_appear : global_reference list } module type Mlpp_param = sig - val toplevel : bool val globals : unit -> Idset.t (* the bool arg is: should we rename in uppercase or not ? *) val rename_global : global_reference -> bool -> identifier diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index d516bb369..52798cb58 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -39,6 +39,19 @@ let get_tvars t = | a -> s in Idset.elements (get_rec Idset.empty t) +(*s Does a section path occur in a ML type ? *) + +let sp_of_r r = match r with + | ConstRef sp -> sp + | IndRef (sp,_) -> sp + | ConstructRef ((sp,_),_) -> sp + | _ -> assert false + +let rec type_mem_sp sp = function + | Tglob r when (sp_of_r r)=sp -> true + | Tapp l -> List.exists (type_mem_sp sp) l + | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b) + | _ -> false (*s In an ML type, update the arguments to all inductive types [(sp,_)] *) @@ -52,25 +65,6 @@ let rec update_args sp vl = function Tarr (update_args sp vl a, update_args sp vl b) | a -> a -(*s Informative singleton optimization *) - -(* We simplify informative singleton inductive, i.e. an inductive with one - constructor which has one informative argument. *) - -let rec type_mem r0 = function - | Tglob r when r=r0 -> true - | Tapp l -> List.exists (type_mem r0) l - | Tarr (a,b) -> (type_mem r0 a) || (type_mem r0 b) - | _ -> false - -let singletons = ref Refset.empty - -let is_singleton r = Refset.mem r !singletons - -let add_singleton r = singletons:= Refset.add r !singletons - -let clear_singletons () = singletons:= Refset.empty - (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns the list [idn;...;id1] and the term [t]. *) @@ -309,7 +303,7 @@ let check_constant_case br = then raise Impossible done; cst -(* TODO: il faudrait verifier si dans chaque branche on a _ et non pas +(* TODO: il faudrait verifier si dans chaque branche on a [_] et non pas seulement dans la premiere (Coercion Prop < Type). *) let rec permut_case_fun br acc = @@ -367,12 +361,6 @@ let rec simpl o = function simpl o f | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) - | MLcons (r,[t]) when is_singleton r -> simpl o t - (* Informative singleton *) - | MLcase (e,[||]) -> - MLexn "absurd case" - | MLcase (e,[|r,[i],c|]) when is_singleton r -> (* Informative singleton *) - simpl o (MLletin (i,e,c)) | MLcase (e,br) -> let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in simpl_case o br (simpl o e) @@ -432,25 +420,6 @@ and simpl_case o br e = (*s Local [prop] elimination. *) (* Try to eliminate as many [prop] as possible inside an [ml_ast]. *) -(*i -(* Index of the first [prop] lambda *) - -let rec first_prop_rank = function - | MLlam(id,_) when id=prop_name -> 1 - | MLlam(_,t) -> succ (first_prop_rank t) - | _ -> raise Impossible - -(* Minimal number of args after [Rel p] *) - -let min_nb_args p m t = - let rec minrec n m = function - | MLrel i when i=n+p -> 0 - | MLapp(f,a) -> - let m = List.fold_left (minrec n) m a in - if f=(MLrel (n+p)) then min (List.length a) m else m - | a -> ast_fold_lift minrec n m a - in minrec 0 m t -i*) (* Given the names of the variables, build a substitution array. *) let rels_to_kill ids = @@ -504,8 +473,8 @@ let kill_prop_args t0 ids m t = in killrec 0 t let kill_prop_aux c = - let m = nb_lams c in let ids,c = collect_lams c in + let m = List.length ids in let ids' = List.filter ((<>) prop_name) ids in let diff = m - List.length ids' in if ids' = [] || diff = 0 then raise Impossible; @@ -553,8 +522,6 @@ and kill_prop_fix i fi c = done; c,ids,m - - let normalize a = if (optim()) then kill_prop (simpl true a) else simpl false a @@ -730,7 +697,8 @@ let manual_expand_list = List.map (fun s -> path_of_string ("Coq.Init."^s)) [ "Specif.sigS_rect" ; "Specif.sigS_rec" ; "Datatypes.prod_rect" ; "Datatypes.prod_rec"; - "Wf.Acc_rec" ; "Wf.well_founded_induction" ] + "Wf.Acc_rec" ; "Wf.Acc_rect" ; + "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ] let manual_expand = function | ConstRef sp -> List.mem sp manual_expand_list @@ -743,12 +711,12 @@ let manual_expand = function we are free to act (AutoInline is set) \end{itemize} *) -let expand strict_lang r t = +let expand r t = (not (to_keep r)) (* The user DOES want to keep it *) && ((to_inline r) (* The user DOES want to expand it *) || - (auto_inline () && strict_lang && + (auto_inline () && lang () <> Haskell && ((manual_expand r) || expansion_test t))) (*s Optimization *) @@ -764,11 +732,6 @@ let subst_glob_decl r m = function | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t') | d -> d -let warning_expansion r = - warn (hov 0 (str "The constant" ++ spc () ++ - Printer.pr_global r ++ - spc () ++ str "is expanded.")) - let print_ml_decl prm (r,_) = not (to_inline r) || List.mem r prm.to_appear @@ -778,20 +741,7 @@ let add_ml_decls prm decls = let l = List.map (fun (r,s)-> Dcustom (r,s)) l in (List.rev l @ decls) -let strict_language = (=) Ocaml - -let rec empty_ind = function - | [] -> [],[] - | t :: q -> let l,l' = empty_ind q in - (match t with - | ids,r,[] -> Dabbrev (r,ids,Texn "empty inductive") :: l,l' - | _ -> l,t::l') - -let global_kill_prop r0 ids m = function - | Dglob(r,e) -> Dglob (r,kill_prop_args (MLglob r0) ids m e) - | d -> d - -let rec optim prm = function +let rec optimize prm = function | [] -> [] | ( Dabbrev (r,_,Tarity) | @@ -799,40 +749,19 @@ let rec optim prm = function Dglob(r,MLarity) | Dglob(r,MLprop) ) as d :: l -> if List.mem r prm.to_appear then - d :: (optim prm l) - else optim prm l + d :: (optimize prm l) + else optimize prm l | Dglob (r,t) :: l -> let t = normalize t in - let t,l = - try - let t,ids,m = kill_prop_aux t in - t,(List.map (global_kill_prop r ids m) l) - (* TODO: options & modularité? *) - with Impossible -> (t,l) in - let b = expand (strict_language prm.lang) r t in + let b = expand r t in let l = if b then - begin - if not (prm.toplevel) then if_verbose warning_expansion r; - List.map (subst_glob_decl r t) l - end + List.map (subst_glob_decl r t) l else l in if (not b || prm.modular || List.mem r prm.to_appear) then let t = optimize_fix t in - Dglob (r,t) :: (optim prm l) + Dglob (r,t) :: (optimize prm l) else - optim prm l - | (Dtype ([],_) | Dabbrev _ | Dcustom _) as d :: l -> - d :: (optim prm l) - | Dtype ([ids,r,[r0,[t0]]],false) :: l when not (type_mem r t0) -> - (* Detection of informative singleton. *) - add_singleton r0; - Dabbrev (r, ids, t0) :: (optim prm l) - | Dtype(il,b) :: l -> - (* Detection of empty inductives. *) - let l1,l2 = empty_ind il in - if l2 = [] then l1 @ (optim prm l) - else l1 @ (Dtype(l2,b) :: (optim prm l)) - - -let optimize prm l = clear_singletons(); optim prm l + optimize prm l + | d :: l -> d :: (optimize prm l) + diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index 1b8166b58..02257be77 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -28,15 +28,19 @@ val collect_lams : ml_ast -> identifier list * ml_ast val anonym_lams : ml_ast -> int -> ml_ast +val named_lams : ml_ast -> identifier list -> ml_ast + (*s Utility functions over ML types. [update_args sp vl t] puts [vl] as arguments behind every inductive types [(sp,_)]. *) +val sp_of_r : global_reference -> section_path + +val type_mem_sp : section_path -> ml_type -> bool + val get_tvars : ml_type -> identifier list val update_args : section_path -> ml_type list -> ml_type -> ml_type -val clear_singletons : unit -> unit - (*s Utility functions over ML terms. [occurs n t] checks whether [Rel n] occurs (freely) in [t]. [ml_lift] is de Bruijn lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *) @@ -65,3 +69,7 @@ val add_ml_decls : val optimize : extraction_params -> ml_decl list -> ml_decl list +exception Impossible + +val kill_prop_aux : ml_ast -> ml_ast * identifier list * int + diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 5dcbc4667..b385bd619 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -158,7 +158,6 @@ let rec pp_type par ren t = (open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2 ++ close_par par) | Tglob r -> pp_type_global r - | Texn s -> str ("unit (* " ^ s ^ " *)") | Tprop -> str "prop" | Tarity -> str "arity" in @@ -347,11 +346,13 @@ let pp_one_ind prefix (pl,name,cl) = (fun () -> (spc () ++ str "* ")) (pp_type true ren) l)) in (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ - (fnl () ++ - v 0 (str " " ++ - prlist_with_sep (fun () -> (fnl () ++ str " | ")) - (fun c -> hov 2 (pp_constructor c)) cl))) - + (* TODO: possible clash with Coq unit *) + 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 @@ -373,11 +374,9 @@ let pp_coind il = (*s Pretty-printing of a declaration. *) let pp_decl = function - | Dtype ([], _) -> - if P.toplevel then hov 0 (str " prop (* Logic inductive *)" ++ fnl ()) - else (mt ()) + | Dtype ([], _) -> mt () | Dtype (i, cofix) -> - if cofix && (not P.toplevel) then begin + if cofix then begin List.iter (fun (_,_,l) -> List.iter (fun (r,_) -> diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 2eca006c7..0cafb9460 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -82,6 +82,38 @@ let reference_of_varg = function let refs_of_vargl = List.map reference_of_varg +(*s Target Language *) + +type lang = Ocaml | Haskell | Toplevel + +let lang_ref = ref Ocaml + +let lang () = !lang_ref + +let (extraction_language,_) = + declare_object ("Extraction Lang", + {cache_function = (fun (_,l) -> lang_ref := l); + load_function = (fun (_,l) -> lang_ref := l); + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) }) + +let _ = declare_summary "Extraction Lang" + { freeze_function = (fun () -> !lang_ref); + unfreeze_function = ((:=) lang_ref); + init_function = (fun () -> lang_ref := Ocaml); + survive_section = true } + +let _ = + vinterp_add "ExtractionLangOcaml" + (fun _ () -> add_anonymous_leaf (extraction_language Ocaml)) + +let _ = + vinterp_add "ExtractionLangHaskell" + (fun _ () -> add_anonymous_leaf (extraction_language Haskell)) + +let _ = + vinterp_add "ExtractionLangToplevel" + (fun _ () -> add_anonymous_leaf (extraction_language Toplevel)) (*s Table for custom inlining *) @@ -100,7 +132,6 @@ let add_inline_entries b l = (List.fold_right (f b) l i), (List.fold_right (f (not b)) l k) - (*s Registration of operations for rollback. *) let (inline_extraction,_) = @@ -137,12 +168,13 @@ let print_inline () = let i'= Refset.filter is_constant i in msg (str "Extraction Inline:" ++ fnl () ++ - Refset.fold - (fun r p -> (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++ - str "Extraction NoInline:" ++ fnl () ++ - Refset.fold - (fun r p -> (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ()) -) + Refset.fold + (fun r p -> + (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++ + str "Extraction NoInline:" ++ fnl () ++ + Refset.fold + (fun r p -> + (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ())) let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index ff47bcede..a6cde3c5f 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -30,6 +30,12 @@ val check_constant : global_reference -> global_reference val refs_of_vargl : vernac_arg list -> global_reference list +(*s Target language. *) + +type lang = Ocaml | Haskell | Toplevel + +val lang : unit -> lang + (*s Table for custom inlining *) val to_inline : global_reference -> bool diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell index 8dc8d0166..ddc6ab4fb 100644 --- a/contrib/extraction/test/Makefile.haskell +++ b/contrib/extraction/test/Makefile.haskell @@ -45,7 +45,7 @@ $(HS): hs2v ./extract.haskell $@ clean: - rm -f theories/*/*.* + rm -f theories/*/*.h* theories/*/*.o # diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell index ef98a62ed..84cde78d4 100755 --- a/contrib/extraction/test/extract.haskell +++ b/contrib/extraction/test/extract.haskell @@ -5,7 +5,7 @@ d=`dirname $vfile` n=`basename $vfile .v` cat custom/all > /tmp/extr$$.v if [ -e custom/$n ]; then cat custom/$n >> /tmp/extr$$.v; fi -echo "Cd \"$d\". Haskell Extraction Module $n. " >> /tmp/extr$$.v +echo "Cd \"$d\". Extraction Language Haskell. Extraction Module $n. " >> /tmp/extr$$.v ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v out=$? rm -f /tmp/extr$$.v |