aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend115
-rw-r--r--Makefile14
-rw-r--r--dev/changements.txt7
-rw-r--r--kernel/names.ml5
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/term.ml6
-rw-r--r--kernel/term.mli10
-rw-r--r--kernel/typeops.ml4
-rw-r--r--kernel/typeops.mli4
-rw-r--r--library/impargs.ml13
-rw-r--r--library/impargs.mli11
-rw-r--r--parsing/astterm.ml225
-rw-r--r--parsing/astterm.mli20
-rw-r--r--parsing/g_command.ml469
-rw-r--r--parsing/g_vernac.ml418
-rw-r--r--parsing/pcoq.ml45
-rw-r--r--parsing/pcoq.mli19
-rw-r--r--parsing/pretty.ml76
-rw-r--r--parsing/pretty.mli8
-rw-r--r--parsing/termast.ml1203
-rw-r--r--parsing/termast.mli11
-rwxr-xr-xpretyping/classops.ml71
-rw-r--r--pretyping/classops.mli6
-rw-r--r--pretyping/pretyping.ml9
-rw-r--r--pretyping/pretyping.mli3
-rw-r--r--pretyping/rawterm.mli9
-rw-r--r--pretyping/typing.ml4
-rw-r--r--toplevel/vernacentries.ml2
29 files changed, 1036 insertions, 918 deletions
diff --git a/.depend b/.depend
index 31deddb79..b12c2d82a 100644
--- a/.depend
+++ b/.depend
@@ -18,7 +18,6 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi \
kernel/names.cmi: lib/pp.cmi
kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi
-kernel/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi
kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \
kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi
@@ -40,7 +39,7 @@ library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
kernel/inductive.cmi kernel/names.cmi kernel/safe_typing.cmi \
kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
library/goptions.cmi: kernel/names.cmi
-library/impargs.cmi: kernel/names.cmi kernel/term.cmi
+library/impargs.cmi: kernel/inductive.cmi kernel/names.cmi kernel/term.cmi
library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
kernel/names.cmi kernel/term.cmi
library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi
@@ -49,6 +48,8 @@ library/library.cmi: lib/pp.cmi
library/nametab.cmi: kernel/names.cmi
library/redinfo.cmi: kernel/names.cmi kernel/term.cmi
library/summary.cmi: kernel/names.cmi
+parsing/as.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
parsing/pcoq.cmi lib/pp.cmi
parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -67,9 +68,11 @@ parsing/pretty.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \
kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
kernel/term.cmi
parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
- kernel/sign.cmi kernel/term.cmi
-parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \
- kernel/term.cmi
+ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \
+ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+ kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi
pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
library/libobject.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi
pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
@@ -91,6 +94,8 @@ pretyping/rawterm.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \
library/libobject.cmi library/library.cmi kernel/names.cmi \
kernel/term.cmi
+pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ kernel/term.cmi
pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi
proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
kernel/term.cmi lib/util.cmi
@@ -296,8 +301,6 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
kernel/names.cmx library/nametab.cmx kernel/reduction.cmx kernel/sign.cmx \
library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
library/declare.cmi
-library/discharge.cmo: library/declare.cmi library/discharge.cmi
-library/discharge.cmx: library/declare.cmx library/discharge.cmi
library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -356,6 +359,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
+parsing/as.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+ library/global.cmi library/impargs.cmi kernel/names.cmi parsing/pcoq.cmi \
+ lib/pp.cmi pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ kernel/term.cmi lib/util.cmi toplevel/vernac.cmi parsing/as.cmi
+parsing/as.cmx: parsing/ast.cmx toplevel/command.cmi parsing/coqast.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+ library/global.cmx library/impargs.cmx kernel/names.cmx parsing/pcoq.cmi \
+ lib/pp.cmx pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/sign.cmx \
+ kernel/term.cmx lib/util.cmx toplevel/vernac.cmx parsing/as.cmi
parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi
parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -388,20 +401,20 @@ parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi
parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi
parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi
-parsing/pretty.cmo: kernel/constant.cmi library/declare.cmi \
- kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
- library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
- library/lib.cmi library/libobject.cmi library/library.cmi \
- kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
- kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi \
- lib/util.cmi parsing/pretty.cmi
-parsing/pretty.cmx: kernel/constant.cmx library/declare.cmx \
- kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
- library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
- library/lib.cmx library/libobject.cmx library/library.cmx \
- kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
- kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx \
- lib/util.cmx parsing/pretty.cmi
+parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+ library/global.cmi library/impargs.cmi kernel/inductive.cmi \
+ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \
+ library/library.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+ parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi
+parsing/pretty.cmx: pretyping/classops.cmx kernel/constant.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+ library/global.cmx library/impargs.cmx kernel/inductive.cmx \
+ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \
+ library/library.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+ parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi
parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -415,29 +428,31 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
kernel/generic.cmi library/global.cmi library/goptions.cmi \
library/impargs.cmi kernel/inductive.cmi kernel/names.cmi \
- library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi parsing/termast.cmi
+ library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/univ.cmi lib/util.cmi parsing/termast.cmi
parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
kernel/generic.cmx library/global.cmx library/goptions.cmx \
library/impargs.cmx kernel/inductive.cmx kernel/names.cmx \
- library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx parsing/termast.cmi
+ library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmi kernel/sign.cmx \
+ kernel/term.cmx kernel/univ.cmx lib/util.cmx parsing/termast.cmi
+pretyping/cases.cmo: pretyping/cases.cmi
+pretyping/cases.cmx: pretyping/cases.cmi
pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
kernel/generic.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
- lib/options.cmi lib/pp.cmi parsing/printer.cmi library/summary.cmi \
- proofs/tacred.cmi kernel/term.cmi lib/util.cmi pretyping/classops.cmi
+ lib/options.cmi lib/pp.cmi library/summary.cmi proofs/tacred.cmi \
+ kernel/term.cmi lib/util.cmi pretyping/classops.cmi
pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
kernel/generic.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \
- lib/options.cmx lib/pp.cmx parsing/printer.cmx library/summary.cmx \
- proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi
+ lib/options.cmx lib/pp.cmx library/summary.cmx proofs/tacred.cmx \
+ kernel/term.cmx lib/util.cmx pretyping/classops.cmi
pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \
- pretyping/recordops.cmi kernel/reduction.cmi kernel/retyping.cmi \
+ pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
pretyping/coercion.cmi
pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
pretyping/evarconv.cmx kernel/evd.cmx kernel/generic.cmx kernel/names.cmx \
- pretyping/recordops.cmx kernel/reduction.cmx kernel/retyping.cmi \
+ pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \
kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
pretyping/coercion.cmi
pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \
@@ -462,22 +477,22 @@ pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \
pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \
pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \
pretyping/pretype_errors.cmi
-pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \
- pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \
- pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
- library/indrec.cmi kernel/inductive.cmi kernel/instantiate.cmi \
- pretyping/multcase.cmi kernel/names.cmi lib/pp.cmi \
+pretyping/pretyping.cmo: parsing/ast.cmi pretyping/cases.cmi \
+ pretyping/classops.cmi pretyping/coercion.cmi kernel/environ.cmi \
+ pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+ kernel/generic.cmi library/indrec.cmi kernel/inductive.cmi \
+ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
- pretyping/recordops.cmi kernel/reduction.cmi kernel/retyping.cmi \
+ pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
lib/util.cmi pretyping/pretyping.cmi
-pretyping/pretyping.cmx: parsing/ast.cmx pretyping/classops.cmx \
- pretyping/coercion.cmx kernel/environ.cmx pretyping/evarconv.cmx \
- pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \
- library/indrec.cmx kernel/inductive.cmx kernel/instantiate.cmx \
- pretyping/multcase.cmi kernel/names.cmx lib/pp.cmx \
+pretyping/pretyping.cmx: parsing/ast.cmx pretyping/cases.cmx \
+ pretyping/classops.cmx pretyping/coercion.cmx kernel/environ.cmx \
+ pretyping/evarconv.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+ kernel/generic.cmx library/indrec.cmx kernel/inductive.cmx \
+ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
pretyping/pretype_errors.cmx pretyping/rawterm.cmi \
- pretyping/recordops.cmx kernel/reduction.cmx kernel/retyping.cmi \
+ pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \
kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
lib/util.cmx pretyping/pretyping.cmi
pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \
@@ -488,6 +503,14 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \
library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \
library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
pretyping/recordops.cmi
+pretyping/retyping.cmo: kernel/environ.cmi kernel/generic.cmi \
+ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \
+ kernel/reduction.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \
+ lib/util.cmi pretyping/retyping.cmi
+pretyping/retyping.cmx: kernel/environ.cmx kernel/generic.cmx \
+ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \
+ kernel/reduction.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \
+ lib/util.cmx pretyping/retyping.cmi
pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi
@@ -707,11 +730,13 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \
library/lib.cmi library/libobject.cmi library/library.cmi \
- parsing/pcoq.cmi lib/pp.cmi library/summary.cmi toplevel/metasyntax.cmi
+ parsing/pcoq.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
+ toplevel/metasyntax.cmi
toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmi \
library/lib.cmx library/libobject.cmx library/library.cmx \
- parsing/pcoq.cmi lib/pp.cmx library/summary.cmx toplevel/metasyntax.cmi
+ parsing/pcoq.cmi lib/pp.cmx library/summary.cmx lib/util.cmx \
+ toplevel/metasyntax.cmi
toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \
kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \
diff --git a/Makefile b/Makefile
index c46f30851..7d51977c2 100644
--- a/Makefile
+++ b/Makefile
@@ -49,16 +49,18 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
library/indrec.cmo library/declare.cmo
-PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \
- pretyping/evarutil.cmo pretyping/evarconv.cmo \
+PRETYPING=pretyping/retyping.cmo pretyping/typing.cmo \
+ pretyping/classops.cmo pretyping/recordops.cmo \
+ pretyping/evarutil.cmo pretyping/evarconv.cmo \
pretyping/pretype_errors.cmo pretyping/coercion.cmo \
- pretyping/multcase.cmo pretyping/pretyping.cmo
+ pretyping/cases.cmo pretyping/pretyping.cmo
PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
- parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\
- parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo \
- parsing/egrammar.cmo
+ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_cases.cmo\
+ parsing/printer.cmo parsing/pretty.cmo \
+ parsing/termast.cmo parsing/astterm.cmo \
+ parsing/egrammar.cmo
PROOFS=proofs/tacred.cmo \
proofs/proof_trees.cmo proofs/logic.cmo \
diff --git a/dev/changements.txt b/dev/changements.txt
index 0e0ae4f1c..80698a0be 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -46,7 +46,8 @@ Changements dans les fonctions :
rev_append -> List.rev_append
Termenv
- mind_specif_of_mind -> Global.lookup_mind_specif
+ mind_specif_of_mind -> Global.lookup_mind_specif
+ ou Environ.lookup_mind_specif si on a un env sous la main
mis_arity -> instantiate_arity
mis_lc -> instantiate_lc
@@ -54,8 +55,8 @@ Changements dans les fonctions :
gentermpr -> gen_pr_term
Typing, Machops
- type_of_type -> type_of_sort
- fcn_proposition -> type_of_type
+ type_of_type -> judge_of_type
+ fcn_proposition -> judge_of_prop_contents
Changements dans les grammaires
diff --git a/kernel/names.ml b/kernel/names.ml
index 316e0735a..e04a41f42 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -224,6 +224,11 @@ module Spset = Set.Make(SpOrdered)
module Spmap = Map.Make(SpOrdered)
+(* Special references for inductive objects *)
+
+type inductive_path = section_path * int
+type constructor_path = inductive_path * int
+
(* Hash-consing of name objects *)
module Hident = Hashcons.Make(
struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 541e4f61a..b3f5811e4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -70,6 +70,9 @@ val sp_gt : section_path * section_path -> bool
module Spset : Set.S with type elt = section_path
module Spmap : Map.S with type key = section_path
+type inductive_path = section_path * int
+type constructor_path = inductive_path * int
+
(* Hash-consing *)
val hcons_names : unit ->
(section_path -> section_path) * (section_path -> section_path) *
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 04d63da8f..8f1ad3787 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -89,10 +89,10 @@ let rec execute mf env cstr =
(make_judge cofix larv.(i), cst)
| IsSort (Prop c) ->
- (make_judge_of_prop_contents c, cst0)
+ (judge_of_prop_contents c, cst0)
| IsSort (Type u) ->
- make_judge_of_type u
+ judge_of_type u
| IsAppL (f,args) ->
let (j,cst1) = execute mf env f in
diff --git a/kernel/term.ml b/kernel/term.ml
index 1a5c74e68..38dbc3765 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -20,8 +20,8 @@ type 'a oper =
(* DOPN *)
| AppL | Const of section_path | Abst of section_path
| Evar of int
- | MutInd of section_path * int
- | MutConstruct of (section_path * int) * int
+ | MutInd of inductive_path
+ | MutConstruct of constructor_path
| MutCase of case_info
| Fix of int array * int
| CoFix of int
@@ -30,7 +30,7 @@ type 'a oper =
(* an extra slot, for putting in whatever sort of
operator we need for whatever sort of application *)
-and case_info = (section_path * int) option
+and case_info = inductive_path option
(* Sorts. *)
diff --git a/kernel/term.mli b/kernel/term.mli
index b84925860..6e7101ad3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -17,14 +17,14 @@ type 'a oper =
| Cast | Prod | Lambda
| AppL | Const of section_path | Abst of section_path
| Evar of int
- | MutInd of section_path * int
- | MutConstruct of (section_path * int) * int
+ | MutInd of inductive_path
+ | MutConstruct of constructor_path
| MutCase of case_info
| Fix of int array * int
| CoFix of int
| XTRA of string
-and case_info = (section_path * int) option
+and case_info = inductive_path option
(*s The sorts of CCI. *)
@@ -287,13 +287,13 @@ val args_of_abst : constr -> constr array
(* Destructs a (co)inductive type *)
val destMutInd : constr -> section_path * int * constr array
-val op_of_mind : constr -> section_path * int
+val op_of_mind : constr -> inductive_path
val args_of_mind : constr -> constr array
val ci_of_mind : constr -> case_info
(* Destructs a constructor *)
val destMutConstruct : constr -> section_path * int * int * constr array
-val op_of_mconstr : constr -> (section_path * int) * int
+val op_of_mconstr : constr -> constructor_path
val args_of_mconstr : constr -> constr array
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0824c192c..706646245 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -357,13 +357,13 @@ let judge_of_set =
uj_type = DOP0(Sort type_0);
uj_kind = DOP0(Sort type_1) }
-let make_judge_of_prop_contents = function
+let judge_of_prop_contents = function
| Null -> judge_of_prop
| Pos -> judge_of_set
(* Type of Type(i). *)
-let make_judge_of_type u =
+let judge_of_type u =
let (uu,uuu,c) = super_super u in
{ uj_val = DOP0 (Sort (Type u));
uj_type = DOP0 (Sort (Type uu));
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index b935efd8c..a271dc9ec 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -42,9 +42,9 @@ val type_case_branches :
env -> 'a evar_map -> constr -> constr -> constr -> constr
-> constr * constr array * constr
-val make_judge_of_prop_contents : contents -> unsafe_judgment
+val judge_of_prop_contents : contents -> unsafe_judgment
-val make_judge_of_type : universe -> unsafe_judgment * constraints
+val judge_of_type : universe -> unsafe_judgment * constraints
val abs_rel :
env -> 'a evar_map -> name -> typed_type -> unsafe_judgment
diff --git a/library/impargs.ml b/library/impargs.ml
index cd9a5ef4e..baa993312 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -82,13 +82,14 @@ let constructor_implicits ((sp,i),j) =
let imps = Spmap.find sp !inductives_table in
(snd imps.(i)).(pred j)
-let mconstr_implicits mc =
- let (sp, i, j, _) = destMutConstruct mc in
- list_of_implicits (constructor_implicits ((sp,i),j))
+let constructor_implicits_list constr_sp =
+ list_of_implicits (constructor_implicits constr_sp)
-let mind_implicits m =
- let (sp,i,_) = destMutInd m in
- list_of_implicits (inductive_implicits (sp,i))
+let inductive_implicits_list ind_sp =
+ list_of_implicits (inductive_implicits ind_sp)
+
+let constant_implicits_list sp =
+ list_of_implicits (constant_implicits sp)
let implicits_of_var kind id =
failwith "TODO: implicits of vars"
diff --git a/library/impargs.mli b/library/impargs.mli
index 8a598ef7e..8659b4b40 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -4,6 +4,7 @@
(*i*)
open Names
open Term
+open Inductive
(*i*)
(* Implicit arguments. Here we store the implicit arguments. Notice that we
@@ -25,10 +26,12 @@ val declare_constant_manual_implicits : section_path -> int list -> unit
val constant_implicits : section_path -> implicits
val declare_inductive_implicits : section_path -> unit
-val inductive_implicits : section_path * int -> implicits
-val constructor_implicits : (section_path * int) * int -> implicits
+val inductive_implicits : inductive_path -> implicits
+val constructor_implicits : constructor_path -> implicits
+
+val constructor_implicits_list : constructor_path -> int list
+val inductive_implicits_list : inductive_path -> int list
+val constant_implicits_list : section_path -> int list
-val mconstr_implicits : constr -> int list
-val mind_implicits : constr -> int list
val implicits_of_var : Names.path_kind -> identifier -> int list
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index d06be7d62..0c56d6f0b 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -65,127 +65,9 @@ let check_number_of_pattern loc n l =
if n<>(List.length l) then
user_err_loc (loc,"check_number_of_pattern",mssg_number_of_patterns n l)
-(* absolutize_eqn replaces pattern variables that are global. This
- * means that we are going to remove the pattern abstractions that
- * correspond to constructors.
- * Warning: Names that are global but do not correspond to
- * constructors are considered non-known_global. E.g. if nat appears
- * in a pattern is considered as a variable name. known_global should
- * be refined in order to consider known_global names only those that
- * correspond to constructors of inductive types.
- *)
-(*
-let is_constructor = function
- DOPN(MutConstruct((sp,tyi),i),cl)-> true | _ ->false
-
-let is_known_constructor k env id =
- let srch =
- match k with
- CCI -> Machops.search_reference
- | FW -> Machops.search_freference
- | _ -> anomaly "known_global" in
- try is_constructor (srch env id)
- with (Not_found | UserError _) ->
- (try is_constructor (Environ.search_synconst k id)
- with Not_found -> false)
-
-
-let rec abs_eqn k env avoid = function
- (v::ids, Slam(_,ona,t)) ->
- let id = id_of_string (Ast.id_of_ast v) in
- if is_known_constructor k env id
- then abs_eqn k env avoid (ids, subst1 (VAR id) t)
- else
- let id' = if is_underscore id then id else next_ident_away id avoid in
- let (nids,nt) = abs_eqn k env (id'::avoid) (ids,t) in
- (id'::nids, DLAM(na,nt))
- | ([],t) -> ([],t)
- | _ -> assert false
-
-
-let rec absolutize_eqn absrec k env = function
- DOP1(XTRA("LAMEQN",ids),lam_eqn) ->
- let gids = ids_of_sign (get_globals env) in
- let (nids,neqn) = abs_eqn k env gids (ids, lam_eqn) in
- let uplid = filter is_uppercase_var nids in
- let _ = if uplid <> [] then warning_uppercase uplid in
- DOP1(XTRA("LAMEQN",nids), absrec neqn)
- | _ -> anomalylabstrm "absolutize_eqn" (mal_formed_mssg())
-
-*)
(****************************************************************)
(* Arguments normally implicit in the "Implicit Arguments mode" *)
(* but explicitely given *)
-(*
-let dest_explicit_arg = function
- (DOP1(XTRA ("!", [Num(_,j)]), t)) -> (j,t)
- | _ -> raise Not_found
-
-let is_explicit_arg = function
- (DOP1(XTRA ("!", [Num(_,j)]), t)) -> true
- | _ -> false
-
-let explicitize_appl l args =
- let rec aux n l args acc =
- match (l,args) with
- (i::l',a::args') ->
- if i=n
- then try let j,a' = dest_explicit_arg a in
- if j > i
- then aux (n+1) l' args (mkExistential::acc)
- else if j = i
- then aux (n+1) l' args' (a'::acc)
- else error "Bad explicitation number"
- with Not_found -> aux (n+1) l' args (mkExistential::acc)
- else if is_explicit_arg a then error "Bad explicitation number"
- else aux (n+1) l args' (a::acc)
- | ([],_) -> (List.rev acc)@args
- | (_,[]) -> (List.rev acc)
-in aux 1 l args []
-
-
-let absolutize k sigma env constr =
- let rec absrec env constr = match constr with
- VAR id -> fst (absolutize_var_with_impl k sigma env id)
- | Rel _ as t -> t
- | DOP1(XTRA ("!", [Num _]), _) -> error "Bad explicitation number"
- | DOPN(AppL,cl) -> (* Detect implicit args occurrences *)
- let cl1 = Array.to_list cl in
- let f = List.hd cl1 in
- let args = List.tl cl1 in
- begin match f with
- VAR id ->
- let (c, impargs) = absolutize_var_with_impl k sigma env id in
- let newargs = explicitize_appl impargs args in
- mkAppList c (List.map (absrec env) newargs)
- | DOPN((Const _ | MutInd _ | MutConstruct _) as op, _) ->
- let id = id_of_global op in
- let (c, impargs) = search_ref_with_impl k env id in
- let newargs = explicitize_appl impargs args in
- mkAppList c (List.map (absrec env) newargs)
- | (DOP1(XTRA ("!",[]), t)) ->
- mkAppList (absrec env t) (List.map (absrec env) args)
- | _ -> mkAppL (Array.map (absrec env) cl)
- end
-
- (* Pattern branches have a special absolutization *)
- | DOP1(XTRA("LAMEQN",_),_) as eqn -> absolutize_eqn (absrec env) k env eqn
-
- | DOP0 _ as t -> t
- | DOP1(oper,c) -> DOP1(oper,absrec env c)
- | DOP2(oper,c1,c2) -> DOP2(oper,absrec env c1,absrec env c2)
- | DOPN(oper,cl) -> DOPN(oper,Array.map (absrec env) cl)
- | DOPL(oper,cl) -> DOPL(oper,List.map (absrec env) cl)
- | DLAM(na,c) -> DLAM(na,absrec (add_rel (na,()) env) c)
- | DLAMV(na,cl) -> DLAMV(na,Array.map (absrec (add_rel (na,()) env)) cl)
-
- in absrec env constr
-
-
-(* Fonctions exportées *)
-let absolutize_cci sigma env constr = absolutize CCI sigma env constr
-let absolutize_fw sigma env constr = absolutize FW sigma env constr
-*)
let dbize_sp = function
| Path(loc,sl,s) ->
@@ -196,62 +78,6 @@ let dbize_sp = function
[< 'sTR"malformed section-path" >]))
| ast -> anomaly_loc(Ast.loc ast,"Astterm.dbize_sp",
[< 'sTR"not a section-path" >])
-(*
-let dbize_op loc opn pl cl =
- match (opn,pl,cl) with
- ("META",[Num(_,n)], []) -> DOP0(Meta n)
- | ("XTRA",(Str(_,s))::tlpl,_) when (multcase_kw s) ->
- DOPN(XTRA(s,tlpl),Array.of_list cl)
- | ("XTRA",(Str(_,s))::tlpl,[]) -> DOP0(XTRA(s,tlpl))
- | ("XTRA",(Str(_,s))::tlpl,[c]) -> DOP1(XTRA(s,tlpl),c)
- | ("XTRA",(Str(_,s))::tlpl,[c1;c2]) -> DOP2(XTRA(s,tlpl),c1,c2)
- | ("XTRA",(Str(_,s))::tlpl,_) -> DOPN(XTRA(s,tlpl), Array.of_list cl)
-
- | ("PROP", [Id(_,s)], []) ->
- (try RSort(Prop (contents_of_str s))
- with Invalid_argument s -> anomaly_loc (loc,"Astterm.dbize_op",
- [< 'sTR s >]))
- | ("TYPE", [], []) -> RSort(Type(dummy_univ))
-
- | ("IMPLICIT", [], []) -> DOP0(Implicit)
- | ("CAST", [], [c1;c2]) -> DOP2(Cast,c1,c2)
-
- | ("CONST", [sp], _) -> DOPN(Const (dbize_sp sp),Array.of_list cl)
- | ("ABST", [sp], _) ->
- (try global_abst (dbize_sp sp) (Array.of_list cl)
- with
- Failure _ | Invalid_argument _ ->
- anomaly_loc(loc,"Astterm.dbize_op",
- [< 'sTR"malformed abstraction" >])
- | Not_found -> user_err_loc(loc,"Astterm.dbize_op",
- [< 'sTR"Unbound abstraction" >]))
- | ("MUTIND", [sp;Num(_,tyi)], _) ->
- DOPN(MutInd (dbize_sp sp, tyi),Array.of_list cl)
-
- | ("MUTCASE", [], p::c::l) -> mkMutCase None p c l
-
- | ("MUTCONSTRUCT", [sp;Num(_,tyi);Num(_,n)], _) ->
- DOPN(MutConstruct ((dbize_sp sp, tyi),n),Array.of_list cl)
-
- | ("SQUASH",[],[_]) -> user_err_loc
- (loc,"Astterm.dbize_op",
- [< 'sTR "Unrecognizable braces expression." >])
-
- | (op,_,_) -> anomaly_loc
- (loc,"Astterm.dbize_op",
- [< 'sTR "Unrecognizable constr operator: "; 'sTR op >])
-
-
-let split_params =
- let rec sprec acc = function
- (Id _ as p)::l -> sprec (p::acc) l
- | (Str _ as p)::l -> sprec (p::acc) l
- | (Num _ as p)::l -> sprec (p::acc) l
- | (Path _ as p)::l -> sprec (p::acc) l
- | l -> (List.rev acc,l)
- in sprec []
-
-*)
let is_underscore id = (id = "_")
@@ -526,49 +352,11 @@ let dbize k sigma =
in
dbrec
-(*
-let dbize_kind ... =
- let c =
- try dbize k sigma env com
- with e ->
- wrap_error
- (Ast.loc com, "dbize_kind",
- [< 'sTR"During conversion from explicit-names to" ; 'sPC ;
- 'sTR"debruijn-indices" >], e,
- [< 'sTR"Perhaps the input is malformed" >]) in
-
- let c =
- try absolutize k sigma env c
- with e ->
- wrap_error
- (Ast.loc com, "Astterm.dbize_kind",
- [< 'sTR"During the relocation of global references," >], e,
- [< 'sTR"Perhaps the input is malformed" >])
- in c
-
-*)
-
let dbize_cci sigma env com = dbize CCI sigma env com
let dbize_fw sigma env com = dbize FW sigma env com
(* constr_of_com takes an environment of typing assumptions,
- * and translates a command to a constr.
-
-let raw_constr_of_com sigma env com =
- let c = dbize_cci sigma (unitize_env env) com in
- try Sosub.soexecute c
- with Failure _|UserError _ -> error_sosub_execute CCI com
-
-let raw_fconstr_of_com sigma env com =
- let c = dbize_fw sigma (unitize_env env) com in
- try Sosub.soexecute c
- with Failure _|UserError _ -> error_sosub_execute FW com
-
-let raw_constr_of_compattern sigma env com =
- let c = dbize_cci sigma (unitize_env env) com in
- try Sosub.try_soexecute c
- with Failure _|UserError _ -> error_sosub_execute CCI com
- *)
+ * and translates a command to a constr. *)
let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env env) com
@@ -707,16 +495,10 @@ let fconstr_of_com_sort sigma sign com =
let constr_of_com_casted sigma env com typ =
let sign = context env in
- let c = raw_constr_of_com sigma sign com in
- let isevars = ref sigma in
- try
- let j = unsafe_machine
- (mk_tycon (nf_ise1 sigma typ)) false isevars [] env c in
- (j_apply (process_evars true !isevars) j).uj_val
- with e ->
- Stdpp.raise_with_loc (Ast.loc com) e
+ ise_resolve_casted sigma env typ (raw_constr_of_com sigma sign com)
(* Typing with Trad, and re-checking with Mach *)
+(* Should be done in two passes by library commands ...
let fconstruct_type sigma sign com =
let c = constr_of_com1 true sigma sign com in
Mach.fexecute_type sigma sign c
@@ -743,3 +525,4 @@ let fconstruct_with_univ sigma sign com =
let (_,j) = with_universes (Mach.fexecute sigma sign)
(univ_sp, Constraintab.current_constraints(), c) in
j
+*)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 0b19d3b9c..5bcbb943d 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -40,22 +40,24 @@ val globalize_ast : Coqast.t -> Coqast.t
val type_of_com : env -> Coqast.t -> typed_type
-val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
+val constr_of_com_casted : unit evar_map -> env -> Coqast.t -> constr ->
constr
-val constr_of_com1 : bool -> 'c evar_map -> env -> Coqast.t -> constr
-val constr_of_com : 'c evar_map -> env -> Coqast.t -> constr
-val constr_of_com_sort : 'c evar_map -> env -> Coqast.t -> constr
+val constr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr
+val constr_of_com : unit evar_map -> env -> Coqast.t -> constr
+val constr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com1 : bool -> 'c evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com : 'c evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com_sort : 'c evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com1 : bool -> unit evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com : unit evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com_sort : unit evar_map -> env -> Coqast.t -> constr
(* Typing with Trad, and re-checking with Mach *)
-
+(*i
val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type
(* Typing, re-checking with universes constraints *)
val fconstruct_with_univ :
- 'c evar_map -> context -> Coqast.t -> unsafe_judgment
+ unit evar_map -> context -> Coqast.t -> unsafe_judgment
+
+i*)
diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4
index f820ef44b..7a0bab447 100644
--- a/parsing/g_command.ml4
+++ b/parsing/g_command.ml4
@@ -2,7 +2,6 @@
(* $Id$ *)
open Pcoq
-
open Command
GEXTEND Gram
@@ -23,7 +22,7 @@ GEXTEND Gram
| c1 = command -> [c1] ] ]
;
command0:
- [ [ "?" -> <:ast< (XTRA "ISEVAR") >>
+ [ [ "?" -> <:ast< (ISEVAR) >>
| "?"; n = Prim.number -> <:ast< (META $n) >>
| "["; id1 = IDENT; ":"; c = command; c2 = abstraction_tail ->
<:ast< (LAMBDALIST $c [$id1]$c2) >>
@@ -32,9 +31,9 @@ GEXTEND Gram
<:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >>
| "["; id1 = IDENT; ","; idl = ne_ident_comma_list;
c = abstraction_tail ->
- <:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]($SLAM $idl $c)) >>
+ <:ast< (LAMBDALIST (ISEVAR) [$id1]($SLAM $idl $c)) >>
| "["; id1 = IDENT; c = abstraction_tail ->
- <:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]$c) >>
+ <:ast< (LAMBDALIST (ISEVAR) [$id1]$c) >>
| "["; id1 = IDENT; "="; c = command; "]"; c2 = command ->
<:ast< (ABST #Core#let.cci $c [$id1]$c2) >>
| "<<"; id1 = IDENT; ">>"; c = command -> <:ast< [$id1]$c >>
@@ -52,10 +51,12 @@ GEXTEND Gram
let id2 = Ast.coerce_to_var "lc2" lc2 in
<:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
| "("; lc1 = lcommand; ")" -> lc1
+(*
| "("; lc1 = lcommand; ")"; "@"; "["; cl = ne_command_list; "]" ->
<:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
- | "Prop" -> <:ast< (PROP {Null}) >>
- | "Set" -> <:ast< (PROP {Pos}) >>
+*)
+ | "Prop" -> <:ast< (PROP) >>
+ | "Set" -> <:ast< (SET) >>
| "Type" -> <:ast< (TYPE) >>
| IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
<:ast< (FIX $id ($LIST $fbinders)) >>
@@ -67,35 +68,35 @@ GEXTEND Gram
[ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_command; ">>" -> c
| "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with";
cl = ne_command_list; "end" ->
- <:ast< (XTRA "REC" $l1 $c ($LIST $cl)) >>
+ <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >>
| "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with"; "end"
->
- <:ast< (XTRA "REC" $l1 $c) >>
+ <:ast< (CASE "REC" $l1 $c) >>
| "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of";
cl = ne_command_list; "end" ->
- <:ast< (MUTCASE $l1 $c ($LIST $cl)) >>
+ <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >>
| "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of"; "end" ->
- <:ast< (MUTCASE $l1 $c) >>
+ <:ast< (CASE "NOREC" $l1 $c) >>
| IDENT "Case"; c = command; "of"; cl = ne_command_list; "end" ->
- <:ast< (XTRA "MLCASE" "NOREC" $c ($LIST $cl)) >>
+ <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >>
| IDENT "Case"; c = command; "of"; "end" ->
- <:ast< (XTRA "MLCASE" "NOREC" $c) >>
+ <:ast< (CASE "NOREC" "SYNTH" $c) >>
| IDENT "Match"; c = command; "with"; cl = ne_command_list; "end" ->
- <:ast< (XTRA "MLCASE" "REC" $c ($LIST $cl)) >>
+ <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >>
| IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = command; "in"; c1 = command ->
- <:ast< (XTRA "MLCASE" "NOREC" $c (LAMBDALIST (XTRA "ISEVAR")
+ <:ast< (MLCASE "NOREC" $c (LAMBDALIST (ISEVAR)
($SLAM $b $c1))) >>
| IDENT "let"; id1 = IDENT ; "="; c = command; "in";
c1 = command -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>
| IDENT "if"; c1 = command; IDENT "then"; c2 = command;
IDENT "else"; c3 = command ->
- <:ast< ( XTRA "MLCASE" "NOREC" $c1 $c2 $c3) >>
+ <:ast< ( MLCASE "NOREC" $c1 $c2 $c3) >>
(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *)
| "<"; l1 = lcommand; ">";
IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = command; "in"; c1 = command ->
- <:ast< (MUTCASE $l1 $c (LAMBDALIST (XTRA "ISEVAR") ($SLAM $b $c1))) >>
+ <:ast< (MUTCASE $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
| "<"; l1 = lcommand; ">";
IDENT "if"; c1 = command; IDENT "then";
c2 = command; IDENT "else"; c3 = command ->
@@ -132,7 +133,7 @@ GEXTEND Gram
;
command10:
[ [ "!"; f = IDENT; args = ne_command9_list ->
- <:ast< (APPLIST (XTRA "!" ($VAR $f)) ($LIST $args)) >>
+ <:ast< (APPLISTEXPL ($VAR $f) ($LIST $args)) >>
| f = command9; args = ne_command91_list ->
<:ast< (APPLIST $f ($LIST $args)) >>
| f = command9 -> f ] ]
@@ -149,9 +150,29 @@ GEXTEND Gram
[ [ id = binder; ";"; idl = ne_binder_list -> id::idl
| id = binder -> [id] ] ]
;
- command91:
+ weak_binder:
+ [ [ idl = ne_ident_comma_list; c = type_option ->
+ <:ast< (BINDER $c ($LIST $idl)) >> ] ]
+ ;
+ ne_weak_binder_list:
+ [ [ id = weak_binder; ";"; idl = ne_weak_binder_list -> id::idl
+ | id = weak_binder -> [id] ] ]
+ ;
+ type_option:
+ [ [ ":"; c = command -> c
+ | -> <:ast< (ISEVAR) >> ] ]
+ ;
+(* parameters:
+ [ [ "["; bl = ne_binder_semi_list; "]" -> $bl ] ]
+ ;
+ parameters_list:
+ [ [
+ <:ast< (BINDERLIST ($LIST $bl)) >>
+ | -> <:ast< (BINDERLIST) >> ] ]
+ ;
+*) command91:
[ [ n = Prim.number; "!"; c1 = command9 ->
- <:ast< (XTRA "!" $n $c1) >>
+ <:ast< (EXPL $n $c1) >>
| c1 = command9 -> c1 ] ]
;
ne_command91_list:
@@ -165,7 +186,7 @@ GEXTEND Gram
fixbinder:
[ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = command;
":="; def = command -> <:ast< (NUMFDECL $id $recarg $type_ $def) >>
- | id = ident; "["; idl = ne_binder_list; "]"; ":"; type_ = command;
+ | id = ident; "["; idl = ne_weak_binder_list; "]"; ":"; type_ = command;
":="; def = command ->
<:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ]
;
@@ -186,7 +207,7 @@ GEXTEND Gram
":"; c = command; c2 = abstraction_tail ->
<:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >>
| ";"; idl = ne_ident_comma_list; c2 = abstraction_tail ->
- <:ast< (LAMBDALIST (XTRA "ISEVAR") ($SLAM $idl $c2)) >>
+ <:ast< (LAMBDALIST (ISEVAR) ($SLAM $idl $c2)) >>
| "]"; c = command -> c ] ]
;
product_tail:
@@ -194,7 +215,9 @@ GEXTEND Gram
":"; c = command; c2 = product_tail ->
<:ast< (PRODLIST $c ($SLAM $idl $c2)) >>
| ";"; idl = ne_ident_comma_list; c2 = product_tail ->
- <:ast< (PRODLIST (XTRA "ISEVAR") ($SLAM $idl $c2)) >>
+ <:ast< (PRODLIST (ISEVAR) ($SLAM $idl $c2)) >>
| ")"; c = command -> c ] ]
;
-END
+END;;
+
+(* $Id$ *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5d2679407..e43c9ed0a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -72,7 +72,7 @@ GEXTEND Gram
-> <:ast< (VERNACARGLIST $id $c $indpar $lidcom) >> ] ]
;
onerec:
- [ [ id = identarg; "["; idl = ne_binder_semi_list; "]"; ":"; c = comarg;
+ [ [ id = identarg; "["; idl = ne_binder_list; "]"; ":"; c = comarg;
":="; def = comarg ->
<:ast< (VERNACARGLIST $id (BINDERLIST ($LIST $idl)) $c $def) >> ] ]
;
@@ -123,12 +123,12 @@ GEXTEND Gram
[ [ IDENT "Induction"; IDENT "for" -> <:ast< "DEP" >>
| IDENT "Minimality"; IDENT "for" -> <:ast< "NODEP" >> ] ]
;
- ne_binder_semi_list:
- [ [ id = binder; ";"; idl = ne_binder_semi_list -> id :: idl
+ ne_binder_list:
+ [ [ id = binder; ";"; idl = ne_binder_list -> id :: idl
| id = binder -> [id] ] ]
;
indpar:
- [ [ "["; bl = ne_binder_semi_list; "]" ->
+ [ [ "["; bl = ne_binder_list; "]" ->
<:ast< (BINDERLIST ($LIST $bl)) >>
| -> <:ast< (BINDERLIST) >> ] ]
;
@@ -253,13 +253,13 @@ GEXTEND Gram
(LAMBDALIST $c [$id1]($SLAM $idl $t)))) >>
- | hyp = hyp_tok; bl = ne_binder_semi_list; "." ->
+ | hyp = hyp_tok; bl = ne_binder_list; "." ->
<:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = hyps_tok; bl = ne_binder_semi_list; "." ->
+ | hyp = hyps_tok; bl = ne_binder_list; "." ->
<:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = param_tok; bl = ne_binder_semi_list; "." ->
+ | hyp = param_tok; bl = ne_binder_list; "." ->
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = params_tok; bl = ne_binder_semi_list; "." ->
+ | hyp = params_tok; bl = ne_binder_list; "." ->
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
| IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
":="; c = comarg; "." ->
@@ -285,7 +285,7 @@ GEXTEND Gram
c = rec_constr; "{"; fs = fields; "}"; "." ->
<:ast< (RECORD "COERCION" $name $ps (COMMAND $s) $c $fs) >>
- | IDENT "Mutual"; "["; bl = ne_binder_semi_list; "]" ; f = finite_tok;
+ | IDENT "Mutual"; "["; bl = ne_binder_list; "]" ; f = finite_tok;
indl = block_old_style; "." ->
<:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
(VERNACARGLIST ($LIST $indl))) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b1c80bd3e..873d52cbb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -255,6 +255,9 @@ module Command =
let simple_pattern2 = Gram.Entry.create "Command.simple_pattern2"
let simple_pattern_list =
Gram.Entry.create "Command.simple_pattern_list"
+ let type_option = gec "type_option"
+ let weak_binder = gec "weak_binder"
+ let ne_weak_binder_list = gec_list "ne_weak_binder"
let ucommand = snd (get_univ "command")
end
@@ -355,7 +358,7 @@ module Vernac =
let lvernac = gec_list "lvernac"
let meta_binding = gec "meta_binding"
let meta_binding_list = gec_list "meta_binding_list"
- let ne_binder_semi_list = gec_list "ne_binder_semi_list"
+ let ne_binder_list = gec_list "ne_binder_list"
let ne_comarg_list = gec_list "ne_comarg_list"
let ne_identarg_comma_list = gec_list "ne_identarg_comma_list"
let identarg_list = gec_list "identarg_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5bd9a31da..de8c7128e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -81,21 +81,24 @@ module Command :
val ident : Coqast.t Gram.Entry.e
val lassoc_command4 : Coqast.t Gram.Entry.e
val lcommand : Coqast.t Gram.Entry.e
- val lsimple_pattern : (string list * Coqast.t) Gram.Entry.e
+ val lsimple_pattern : Coqast.t Gram.Entry.e
val ne_binder_list : Coqast.t list Gram.Entry.e
val ne_command91_list : Coqast.t list Gram.Entry.e
val ne_command9_list : Coqast.t list Gram.Entry.e
val ne_command_list : Coqast.t list Gram.Entry.e
val ne_eqn_list : Coqast.t list Gram.Entry.e
val ne_ident_comma_list : Coqast.t list Gram.Entry.e
- val ne_pattern_list : (string list * Coqast.t list) Gram.Entry.e
- val pattern : (string list * Coqast.t) Gram.Entry.e
- val pattern_list : (string list * Coqast.t list) Gram.Entry.e
+ val ne_pattern_list : Coqast.t list Gram.Entry.e
+ val pattern : Coqast.t Gram.Entry.e
+ val pattern_list : Coqast.t list Gram.Entry.e
val product_tail : Coqast.t Gram.Entry.e
val raw_command : Coqast.t Gram.Entry.e
- val simple_pattern : (string list * Coqast.t) Gram.Entry.e
- val simple_pattern2 : (string list * Coqast.t) Gram.Entry.e
- val simple_pattern_list : (string list * Coqast.t list) Gram.Entry.e
+ val simple_pattern : Coqast.t Gram.Entry.e
+ val simple_pattern2 : Coqast.t Gram.Entry.e
+ val simple_pattern_list : Coqast.t list Gram.Entry.e
+ val type_option : Coqast.t Gram.Entry.e
+ val weak_binder : Coqast.t Gram.Entry.e
+ val ne_weak_binder_list : Coqast.t list Gram.Entry.e
end
module Tactic :
@@ -172,7 +175,7 @@ module Vernac :
val lvernac : Coqast.t list Gram.Entry.e
val meta_binding : Coqast.t Gram.Entry.e
val meta_binding_list : Coqast.t list Gram.Entry.e
- val ne_binder_semi_list : Coqast.t list Gram.Entry.e
+ val ne_binder_list : Coqast.t list Gram.Entry.e
val ne_comarg_list : Coqast.t list Gram.Entry.e
val ne_identarg_comma_list : Coqast.t list Gram.Entry.e
val ne_identarg_list : Coqast.t list Gram.Entry.e
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 35e37290b..c482dd15e 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -46,7 +46,7 @@ let print_typed_value_in_env env (trm,typ) =
[< term0 (gLOB sign) trm ; 'fNL ;
'sTR " : "; term0 (gLOB sign) typ ; 'fNL >]
-let print_typed_value x = print_typed_value_in_env (Global.env()) x
+let print_typed_value x = print_typed_value_in_env (Global.env ()) x
let print_recipe = function
| Some c -> prterm c
@@ -500,7 +500,7 @@ let fprint_judge {uj_val=trm;uj_type=typ} =
let unfold_head_fconst =
let rec unfrec = function
- | DOPN(Const _,_) as k -> constant_value (Global.env()) k
+ | DOPN(Const _,_) as k -> constant_value (Global.env ()) k
| DOP2(Lambda,t,DLAM(na,b)) -> DOP2(Lambda,t,DLAM(na,unfrec b))
| DOPN(AppL,v) -> DOPN(AppL,array_cons (unfrec (array_hd v)) (array_tl v))
| x -> x
@@ -661,3 +661,75 @@ let inspect depth =
in
let items = List.rev (inspectrec depth [] (Lib.contents_after None)) in
print_context false items
+
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml *)
+
+open Classops
+
+let string_of_strength = function
+ | NeverDischarge -> "(global)"
+ | DischargeAt sp -> "(disch@"^(string_of_path sp)
+
+let print_coercion_value v = prterm v.cOE_VALUE.uj_val
+
+let print_index_coercion c =
+ let _,v = coercion_info_from_index c in
+ print_coercion_value v
+
+let print_class i =
+ let cl,x = class_info_from_index i in
+ [< 'sTR x.cL_STR >]
+
+let print_path ((i,j),p) =
+ [< 'sTR"[";
+ prlist_with_sep (fun () -> [< 'sTR"; " >])
+ (fun c -> print_index_coercion c) p;
+ 'sTR"] : "; print_class i; 'sTR" >-> ";
+ print_class j >]
+
+let print_graph () =
+ [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >]
+
+let print_classes () =
+ [< prlist_with_sep pr_spc
+ (fun (_,(cl,x)) ->
+ [< 'sTR x.cL_STR (*; 'sTR(string_of_strength x.cL_STRE) *) >])
+ (!cLASSES) >]
+
+let print_coercions () =
+ [< prlist_with_sep pr_spc
+ (fun (_,(_,v)) -> [< print_coercion_value v >]) (!cOERCIONS) >]
+
+let cl_of_id id =
+ match string_of_id id with
+ | "FUNCLASS" -> CL_FUN
+ | "SORTCLASS" -> CL_SORT
+ | _ -> let v = Declare.global_reference CCI id in
+ let cl,_ = constructor_at_head v in
+ cl
+
+let index_cl_of_id id =
+ try
+ let cl = cl_of_id id in
+ let i,_=class_info cl in
+ i
+ with _ ->
+ errorlabstrm "index_cl_of_id"
+ [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+
+let print_path_between ids idt =
+ let i = (index_cl_of_id ids) in
+ let j = (index_cl_of_id idt) in
+ let p =
+ try
+ lookup_path_between (i,j)
+ with _ ->
+ errorlabstrm "index_cl_of_id"
+ [< 'sTR"No path between ";'sTR(string_of_id ids);
+ 'sTR" and ";'sTR(string_of_id ids) >]
+ in
+ print_path ((i,j),p)
+
+(*************************************************************************)
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 0691f0a01..93c270716 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -44,6 +44,14 @@ val print_extraction : unit -> std_ppcmds
val print_extracted_vars : unit -> std_ppcmds
i*)
+(* Pretty-printing functions for classes and coercions *)
+val print_graph : unit -> std_ppcmds
+val print_classes : unit -> std_ppcmds
+val print_coercions : unit -> std_ppcmds
+val print_path_between : identifier -> identifier -> std_ppcmds
+
+
val crible : (string -> unit assumptions -> constr -> unit) -> identifier ->
unit
val inspect : int -> std_ppcmds
+
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 040cd82ce..aadf51142 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -13,33 +13,57 @@ open Declare
open Impargs
open Coqast
open Ast
+open Rawterm
-(* Different strategies for renaming of bound variables *)
+(* In this file, we translate constr to ast, in order to print constr *)
-module type RenamingStrategy = sig
- type used_idents = identifier list
- val concrete_name : used_idents -> unit assumptions -> name -> constr
- -> identifier option * used_idents
- val used_of : constr -> used_idents
- val ids_of_env : unit assumptions -> used_idents
-end
+(**********************************************************************)
+(* conversion of references *)
-(* Ancienne version de renommage des variables (avant Dec 98) *)
-
-module WeakRenamingStrategy = struct
-
- type used_idents = identifier list
-
- let concrete_name l n c =
- if n = Anonymous then (None,l)
- else
- let fresh_id = next_name_away n l in
- if dependent (Rel 1) c then (Some fresh_id, fresh_id::l) else (None,l)
- let used_of = global_vars
- let ids_of_env env =
- map_succeed
- (function (Name id,_) -> id | _ -> failwith "caught") (get_rels env)
-end
+let ids_of_ctxt cl =
+ List.map (
+ function
+ (VAR id) -> id
+ | (Rel n) ->
+ warning "ids_of_ctxt: rel";
+ id_of_string ("REL "^(string_of_int n))
+ | _-> anomaly"ids_of_ctxt")
+ (Array.to_list cl)
+
+let ast_of_ident id = nvar (string_of_id id)
+
+let ast_of_constructor (((sp,tyi),n),ids) =
+ ope("MUTCONSTRUCT",
+ (path_section dummy_loc sp)::(num tyi)::(num n)
+ ::(List.map ast_of_ident ids))
+
+let ast_of_mutind ((sp,tyi),ids) =
+ ope("MUTIND",
+ (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
+
+let ast_of_ref = function
+ | RConst (sp,idl) ->
+ ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl))
+ | RAbst (sp) ->
+ ope("ABST", (path_section dummy_loc sp)
+ ::(List.map ast_of_ident (* on triche *) []))
+ | RInd (ind,idl) -> ast_of_mutind(ind,idl)
+ | RConstruct (cstr,idl) -> ast_of_constructor (cstr,idl)
+ | RVar id -> nvar (string_of_id id)
+ | REVar (sp,idl) ->
+ ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl))
+ | RMeta n -> ope("META",[num n])
+
+(**********************************************************************)
+(* conversion of patterns *)
+
+let rec ast_of_pattern = function (* loc is thrown away for printing *)
+ PatVar (loc,Name id) -> nvar (string_of_id id)
+ | PatVar (loc,Anonymous) -> nvar "_"
+ | PatCstr(loc,cstr,args) ->
+ ope("PATTCONSTRUCT",
+ (ast_of_constructor cstr)::List.map ast_of_pattern args)
+ | PatAs(loc,id,p) -> ope("PATTAS",[nvar (string_of_id id); ast_of_pattern p])
(* Nouvelle version de renommage des variables (DEC 98) *)
(* This is the algorithm to display distinct bound variables
@@ -53,78 +77,86 @@ end
il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
mais f et f0 contribue à la liste des variables à éviter (en supposant
que les noms f et f0 ne sont pas déjà pris)
- Intérêt : noms homogènes dans un but avant et après Intro *)
-
-module StrongRenamingStrategy = struct
-
- type used_idents = identifier list
-
- let occur_id env id0 c =
- let rec occur n = function
- | VAR id -> id=id0
- | DOPN (Const sp,cl) ->
- (basename sp = id0) or (array_exists (occur n) cl)
- | DOPN (Abst sp,cl) ->
- (basename sp = id0) or (array_exists (occur n) cl)
- | DOPN (MutInd _, cl) as t ->
- (basename (mind_path t) = id0) or (array_exists (occur n) cl)
- | DOPN (MutConstruct _, cl) as t ->
- (basename (mind_path t) = id0) or (array_exists (occur n) cl)
- | DOPN(_,cl) -> array_exists (occur n) cl
- | DOP1(_,c) -> occur n c
- | DOP2(_,c1,c2) -> (occur n c1) or (occur n c2)
- | DOPL(_,cl) -> List.exists (occur n) cl
- | DLAM(_,c) -> occur (n+1) c
- | DLAMV(_,v) -> array_exists (occur (n+1)) v
- | Rel p ->
- p > n &
- (try (fst (lookup_rel (p-n) env) = Name id0)
- with Not_found -> false) (* Unbound indice : may happen in debug *)
- | DOP0 _ -> false
- in
- occur 1 c
-
- let next_name_not_occuring name l env t =
- let rec next id =
- if List.mem id l or occur_id env id t then next (lift_ident id) else id
- in match name with
- | Name id -> next id
- | Anonymous -> id_of_string "_"
-
- let concrete_name l env n c =
+ Intérêt : noms homogènes dans un but avant et après Intro
+*)
+
+type used_idents = identifier list
+
+(*
+ let concrete_name (lo,l as ll) n c =
if n = Anonymous then
if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"
- else (None,l)
+ else (None,ll)
else
- let fresh_id = next_name_not_occuring n l env c in
+ let l' = match lo with None -> l | Some l0 -> l0@l in
+ let fresh_id = next_name_away n l' in
let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
- (idopt, fresh_id::l)
-
- (* Returns the list of global variables and constants in a term *)
- let global_vars_and_consts t =
- let rec collect acc = function
- | VAR id -> id::acc
- | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
- | DOPN (Abst sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
- | DOPN (MutInd _, cl) as t ->
- (basename (mind_path t))::(Array.fold_left collect acc cl)
- | DOPN (MutConstruct _, cl) as t ->
- (basename (mind_path t))::(Array.fold_left collect acc cl)
- | DOPN(_,cl) -> Array.fold_left collect acc cl
- | DOP1(_,c) -> collect acc c
- | DOP2(_,c1,c2) -> collect (collect acc c1) c2
- | DOPL(_,cl) -> List.fold_left collect acc cl
- | DLAM(_,c) -> collect acc c
- | DLAMV(_,v) -> Array.fold_left collect acc v
- | _ -> acc
- in
- list_uniquize (collect [] t)
-
- let used_of = global_vars_and_consts
- let ids_of_env = Sign.ids_of_env
-end
+ (idopt, (lo,fresh_id::l))
+*)
+
+let occur_id env id0 c =
+ let rec occur n = function
+ VAR id -> id=id0
+ | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
+ | DOPN (Abst sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
+ | DOPN (MutInd _, cl) as t ->
+ (basename (mind_path t) = id0) or (array_exists (occur n) cl)
+| DOPN (MutConstruct _, cl) as t ->
+ (basename (mind_path t) = id0) or (array_exists (occur n) cl)
+| DOPN(_,cl) -> array_exists (occur n) cl
+| DOP1(_,c) -> occur n c
+| DOP2(_,c1,c2) -> (occur n c1) or (occur n c2)
+| DOPL(_,cl) -> List.exists (occur n) cl
+| DLAM(_,c) -> occur (n+1) c
+| DLAMV(_,v) -> array_exists (occur (n+1)) v
+| Rel p ->
+ p>n &
+ (try (fst (lookup_rel (p-n) env) = Name id0)
+ with Not_found -> false) (* Unbound indice : may happen in debug *)
+| DOP0 _ -> false
+ in occur 1 c;;
+
+let next_name_not_occuring name l env t =
+ let rec next id =
+ if List.mem id l or occur_id env id t then next (lift_ident id) else id
+ in match name with
+ | Name id -> next id
+ | Anonymous -> id_of_string "_"
+
+let concrete_name l env n c =
+ if n = Anonymous then
+ if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"
+ else (None,l)
+ else
+ let fresh_id = next_name_not_occuring n l env c in
+ let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
+ (idopt, fresh_id::l)
+
+ (* Returns the list of global variables and constants in a term *)
+let global_vars_and_consts t =
+ let rec collect acc = function
+ VAR id -> id::acc
+ | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
+ | DOPN (Abst sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
+ | DOPN (MutInd _, cl) as t ->
+ (basename (mind_path t))::(Array.fold_left collect acc cl)
+ | DOPN (MutConstruct _, cl) as t ->
+ (basename (mind_path t))::(Array.fold_left collect acc cl)
+ | DOPN(_,cl) -> Array.fold_left collect acc cl
+ | DOP1(_,c) -> collect acc c
+ | DOP2(_,c1,c2) -> collect (collect acc c1) c2
+ | DOPL(_,cl) -> List.fold_left collect acc cl
+ | DLAM(_,c) -> collect acc c
+ | DLAMV(_,v) -> Array.fold_left collect acc v
+ | _ -> acc
+ in
+ list_uniquize (collect [] t);;
+let used_of = global_vars_and_consts
+let ids_of_env = Sign.ids_of_env
+
+(****************************************************************************)
(* Tools for printing of Cases *)
(* These functions implement a light form of Termenv.mind_specif_of_mind *)
(* specially for handle Cases printing; they respect arities but not typing *)
@@ -135,30 +167,30 @@ let indsp_of_id id =
with Not_found -> error ("Cannot find reference "^(string_of_id id))
in
match oper with
- | MutInd(sp,tyi) -> (sp,tyi)
- | _ -> errorlabstrm "indsp_of_id"
- [< 'sTR ((string_of_id id)^" is not an inductive type") >]
+ MutInd(sp,tyi) -> (sp,tyi)
+ | _ -> errorlabstrm "indsp_of_id"
+ [< 'sTR ((string_of_id id)^" is not an inductive type") >];;
let mind_specif_of_mind_light (sp,tyi) =
let mib = Global.lookup_mind sp in
(mib,mind_nth_type_packet mib tyi)
let rec remove_indtypes = function
- | (1, DLAMV(_,cl)) -> cl
+ (1, DLAMV(_,cl)) -> cl
| (n, DLAM (_,c)) -> remove_indtypes (n-1, c)
- | _ -> anomaly "remove_indtypes: bad list of constructors"
-
+ | _ -> anomaly "remove_indtypes: bad list of constructors";;
+
let rec remove_params n t =
- if n = 0 then t
+ if n=0 then t
else match t with
- | DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c
- | DOP2(Cast,c,_) -> remove_params n c
- | _ -> anomaly "remove_params : insufficiently quantified"
+ DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c
+ | DOP2(Cast,c,_) -> remove_params n c
+ | _ -> anomaly "remove_params : insufficiently quantified";;
let rec get_params = function
- | DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c)
+ DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c)
| DOP2(Cast,c,_) -> get_params c
- | _ -> []
+ | _ -> [];;
let lc_of_lmis (mib,mip) =
let lc = remove_indtypes (mib.mind_ntypes,mip.mind_lc) in
@@ -210,11 +242,11 @@ module PrintingCasesIf =
let title = "Types leading to pretty-printing of Cases using a `if' form: "
let member_message id = function
| true ->
- "Cases on elements of " ^ (string_of_id id)
- ^ " are printed using a `if' form"
+ "Cases on elements of " ^ (string_of_id id)
+ ^ " are printed using a `if' form"
| false ->
- "Cases on elements of " ^ (string_of_id id)
- ^ " are not printed using `if' form"
+ "Cases on elements of " ^ (string_of_id id)
+ ^ " are not printed using `if' form"
end)
module PrintingCasesLet =
@@ -226,11 +258,11 @@ module PrintingCasesLet =
"Types leading to a pretty-printing of Cases using a `let' form:"
let member_message id = function
| true ->
- "Cases on elements of " ^ (string_of_id id)
- ^ " are printed using a `let' form"
+ "Cases on elements of " ^ (string_of_id id)
+ ^ " are printed using a `let' form"
| false ->
- "Cases on elements of " ^ (string_of_id id)
- ^ " are not printed using a `let' form"
+ "Cases on elements of " ^ (string_of_id id)
+ ^ " are not printed using a `let' form"
end)
module PrintingIf = Goptions.MakeTable(PrintingCasesIf)
@@ -238,12 +270,12 @@ module PrintingLet = Goptions.MakeTable(PrintingCasesLet)
(* Options for printing or not wildcard and synthetisable types *)
-open Goptions
+open Goptions;;
let wildcard_value = ref true
let force_wildcard () = !wildcard_value
-let _ =
+let _ =
declare_async_bool_option
{ optasyncname = "the forced wildcard option";
optasynckey = SecondaryTable ("Printing","Wildcard");
@@ -265,94 +297,88 @@ let _ =
let print_implicits = ref false
+(**************************************************)
(* The main translation function is bdize_depcast *)
-module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
-
- (* pour les implicites *)
-
- (* l est ordonne'ee (croissant), ne garder que les elements <= n *)
- let filter_until n l =
- let rec aux = function
- | [] -> []
- | i::l -> if i > n then [] else i::(aux l)
- in
- aux l
-
- (* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes,
- la 2eme est la plus longue se'quence commencant par n,
- la 1ere contient les autres elements *)
-
- let rec div_implicits n =
- function
- | [] -> [],[]
- | i::l ->
- if i = n then
- let l1,l2=(div_implicits (n-1) l) in l1,i::l2
- else
- i::l,[]
-
- let bdize_app c al =
- let impl =
- match c with
- | DOPN(MutConstruct _,_) -> mconstr_implicits c
- | DOPN(MutInd _,_) -> mind_implicits c
- | DOPN(Const sp,_) -> list_of_implicits (constant_implicits sp)
- | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
- | _ -> []
- in
- if impl = [] then
- ope("APPLIST", al)
- else if !print_implicits then
- ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
+(* pour les implicites *)
+
+(* l est ordonne'ee (croissant), ne garder que les elements <= n *)
+let filter_until n l =
+let rec aux = function
+ [] -> []
+ | i::l -> if i > n then []
+ else i::(aux l)
+in aux l;;
+
+(* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes,
+ la 2eme est la plus longue se'quence commencant par n,
+ la 1ere contient les autres elements *)
+
+let rec div_implicits n =
+ function [] -> [],[]
+ | i::l -> if i = n then let l1,l2=(div_implicits (n-1) l) in l1,i::l2
+ else i::l,[];;
+
+let bdize_app c al =
+ let impl =
+ match c with
+ DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp
+ | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp
+ | DOPN(Const sp,_) -> constant_implicits_list sp
+ | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+ | _ -> []
+ in
+ if impl = []
+ then ope("APPLIST", al)
+ else if !print_implicits
+ then ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
else
let largs = List.length al - 1 in
let impl = List.rev (filter_until largs impl) in
let impl1,impl2=div_implicits largs impl in
let al1 = Array.of_list al in
- List.iter
- (fun i -> al1.(i) <-
- ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
- impl2;
- List.iter
- (fun i -> al1.(i) <-
- ope("XTRA",[str "!"; num i; al1.(i)]))
- impl1;
- al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
- ope("APPLIST",Array.to_list al1)
-
- type optioncast = WithCast | WithoutCast
-
- (* [reference_tree p] pre-computes the variables and de bruijn occurring
- in a term to avoid a O(n2) factor when computing dependent each time *)
-
- type ref_tree = NODE of (int list * identifier list) * ref_tree list
-
- let combine l =
- let rec combine_rec = function
- | [] -> [],[]
- | NODE ((a,b),_)::l ->
- let a',b' = combine_rec l in (list_union a a',list_union b b')
- in
- NODE (combine_rec l,l)
-
- let rec reference_tree p = function
- | VAR id -> NODE (([],[id]),[])
- | Rel n -> NODE (([n-p],[]),[])
- | DOP0 op -> NODE (([],[]),[])
- | DOP1(op,c) -> reference_tree p c
- | DOP2(op,c1,c2) -> combine [reference_tree p c1;reference_tree p c2]
- | DOPN(op,cl) -> combine (List.map (reference_tree p) (Array.to_list cl))
- | DOPL(op,cl) -> combine (List.map (reference_tree p) cl)
- | DLAM(na,c) -> reference_tree (p+1) c
- | DLAMV(na,cl) ->
- combine (List.map (reference_tree (p+1))(Array.to_list cl))
-
- (* Auxiliary function for MutCase printing *)
- (* [computable] tries to tell if the predicate typing the result is
- inferable *)
-
- let computable p k =
+ List.iter
+ (fun i -> al1.(i) <-
+ ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
+ impl2;
+ List.iter
+ (fun i -> al1.(i) <-
+ ope("XTRA",[str "!"; num i; al1.(i)]))
+ impl1;
+ al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
+ ope("APPLIST",Array.to_list al1)
+
+type optioncast = WithCast | WithoutCast;;
+
+(* [reference_tree p] pre-computes the variables and de bruijn occurring
+ in a term to avoid a O(n2) factor when computing dependent each time *)
+
+type ref_tree =
+ NODE of (int list * identifier list) * ref_tree list
+
+let combine l =
+ let rec combine_rec = function
+ | [] -> [],[]
+ | NODE ((a,b),_)::l ->
+ let a',b' = combine_rec l in (list_union a a',list_union b b')
+ in
+ NODE (combine_rec l,l)
+
+let rec reference_tree p = function
+ VAR id -> NODE (([],[id]),[])
+ | Rel n -> NODE (([n-p],[]),[])
+ | DOP0 op -> NODE (([],[]),[])
+ | DOP1(op,c) -> reference_tree p c
+ | DOP2(op,c1,c2) -> combine [reference_tree p c1;reference_tree p c2]
+ | DOPN(op,cl) -> combine (List.map (reference_tree p) (Array.to_list cl))
+ | DOPL(op,cl) -> combine (List.map (reference_tree p) cl)
+ | DLAM(na,c) -> reference_tree (p+1) c
+ | DLAMV(na,cl) -> combine (List.map (reference_tree (p+1))(Array.to_list cl))
+
+(* Auxiliary function for MutCase printing *)
+(* [computable] tries to tell if the predicate typing the result is inferable*)
+
+let computable p k =
(* We first remove as many lambda as the arity, then we look
if it remains a lambda for a dependent elimination. This function
works for normal eta-expanded term. For non eta-expanded or
@@ -376,299 +402,514 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
| _ -> false
in striprec (k,p)
- (* Main translation function from constr -> ast *)
-
- let bdize_depcast opcast at_top env t =
- let init_avoid = if at_top then Strategy.ids_of_env env else [] in
- let rec bdrec avoid env t =
- match collapse_appl t with
- (* Not well-formed constructions *)
- | DLAM(na,c) ->
- (match Strategy.concrete_name avoid env na c with
- | (Some id,avoid') ->
- slam(Some (string_of_id id),
- bdrec avoid' (add_rel (Name id,()) env) c)
- | (None,avoid') -> slam(None,bdrec avoid' env (pop c)))
- | DLAMV(na,cl) ->
- if not(array_exists (dependent (Rel 1)) cl) then
- slam(None,ope("V$", array_map_to_list
- (fun c -> bdrec avoid env (pop c)) cl))
- else
- let id = next_name_away na avoid in
- slam(Some (string_of_id id),
- ope("V$", array_map_to_list
- (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
-
- (* Well-formed constructions *)
- | regular_constr ->
- (match kind_of_term regular_constr with
- | IsRel n ->
- (try match fst(lookup_rel n env) with
- | Name id -> nvar (string_of_id id)
- | Anonymous -> raise Not_found
- with Not_found -> ope("REL",[num n]))
- (* TODO: Change this to subtract the current depth *)
- | IsMeta n -> ope("META",[num n])
- | IsVar id -> nvar (string_of_id id)
- | IsXtra s ->
- ope("XTRA",[str s])
- | IsSort s ->
- (match s with
- | Prop c -> ope("PROP",[ide (str_of_contents c)])
- | Type u -> ope("TYPE",[path_section dummy_loc u.u_sp;
- num u.u_num]))
- (* TODO??? | IsImplicit -> ope("IMPLICIT",[]) *)
- | IsCast (c1,c2) ->
- if opcast = WithoutCast then
- bdrec avoid env c1
- else
- ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
- | IsProd (Anonymous,ty,c) ->
- (* Anonymous product are never factorized *)
- ope("PROD",[bdrec [] env ty;
- slam(None,bdrec avoid env (pop c))])
- | IsProd (Name _ as na,ty,c) ->
- let (n,a) = factorize_binder 1 avoid env Prod na ty c in
- (* PROD et PRODLIST doivent être distingués à cause du cas
- non dépendant, pour isoler l'implication;
- peut-être un constructeur ARROW serait-il
- plus justifié ? *)
- let oper = if n=1 then "PROD" else "PRODLIST" in
- ope(oper,[bdrec [] env ty;a])
- | IsLambda (na,ty,c) ->
- let (_,a) = factorize_binder 1 avoid env Lambda na ty c in
- (* LAMBDA et LAMBDALIST se comportent pareil *)
- ope("LAMBDALIST",[bdrec [] env ty;a])
- | IsAppL (f,args) ->
- bdize_app f (List.map (bdrec avoid env) (f::args))
-
- | IsConst (sp,cl) ->
- ope("CONST",((path_section dummy_loc sp)::
- (array_map_to_list (bdrec avoid env) cl)))
- | IsEvar (_,cl) ->
- ope("ISEVAR",(array_map_to_list (bdrec avoid env) cl))
- | IsAbst (sp,cl) ->
- ope("ABST",((path_section dummy_loc sp)::
- (array_map_to_list (bdrec avoid env) cl)))
- | IsMutInd (sp,tyi,cl) ->
- ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
- (array_map_to_list (bdrec avoid env) cl)))
- | IsMutConstruct (sp,tyi,n,cl) ->
- ope("MUTCONSTRUCT",
- ((path_section dummy_loc sp)::(num tyi)::(num n)::
- (array_map_to_list (bdrec avoid env) cl)))
- | IsMutCase (annot,p,c,bl) ->
- let synth_type = synthetize_type () in
- let tomatch = bdrec avoid env c in
- begin match annot with
- | None ->
- (* Pas d'annotation --> affichage avec vieux Case *)
- let pred = bdrec avoid env p in
- let bl' = array_map_to_list (bdrec avoid env) bl in
- ope("MUTCASE",pred::tomatch::bl')
- | Some indsp ->
- let (mib,mip as lmis) =
- mind_specif_of_mind_light indsp in
- let lc = lc_of_lmis lmis in
- let lcparams = Array.map get_params lc in
- let k =
- (nb_prod mip.mind_arity.body) - mib.mind_nparams in
- let pred =
- if synth_type & computable p k & lcparams <> [||]
- then ope("XTRA", [str "SYNTH"])
- else bdrec avoid env p
- in
- if PrintingIf.active indsp then
- ope("FORCEIF", [ pred; tomatch;
- bdrec avoid env bl.(0);
- bdrec avoid env bl.(1) ])
- else
- let idconstructs = mip.mind_consnames in
- let asttomatch =
- ope("XTRA",[str "TOMATCH"; tomatch]) in
- let eqnv =
- array_map3 (bdize_eqn avoid env) idconstructs
- lcparams bl in
- let eqnl = Array.to_list eqnv in
- let tag =
- if PrintingLet.active indsp then
- "FORCELET"
- else
- "MULTCASE"
- in
- ope("XTRA", (str tag)::pred::asttomatch::eqnl)
- end
-
- | IsFix (nv,n,cl,lfn,vt) ->
- let lfi =
- List.map (fun na -> next_name_away na avoid) lfn in
- let def_env =
- List.fold_left
- (fun env id -> add_rel (Name id,()) env) env lfi in
- let def_avoid = lfi@avoid in
- let f = List.nth lfi n in
- let rec split_lambda binds env avoid = function
- (0, t) ->
- binds,bdrec avoid env t
- | (n, DOP2(Cast,t,_)) ->
- split_lambda binds env avoid (n,t)
- | (n, DOP2(Lambda,t,DLAM(na,b))) ->
- let ast = bdrec avoid env t in
- let id = next_name_away na avoid in
- let ast_of_bind =
- ope("BINDER",[ast;nvar (string_of_id id)]) in
- let new_env = add_rel (Name id,()) env in
- split_lambda (ast_of_bind::binds)
- new_env (id::avoid) (n-1,b)
- | _ -> error "split_lambda"
- in
- let rec split_product env avoid = function
- | (0, t) -> bdrec avoid env t
- | (n, DOP2(Cast,t,_)) -> split_product env avoid (n,t)
- | (n, DOP2(Prod,t,DLAM(na,b))) ->
- let ast = bdrec avoid env t in
- let id = next_name_away na avoid in
- let new_env = add_rel (Name id,()) env in
- split_product new_env (id::avoid) (n-1,b)
- | _ -> error "split_product"
- in
- let listdecl =
- list_map_i
- (fun i fi ->
- let (lparams,ast_of_def) =
- split_lambda [] def_env def_avoid
- (nv.(i)+1,vt.(i)) in
- let ast_of_typ =
- split_product env avoid (nv.(i)+1,cl.(i)) in
- ope("FDECL",
- [ nvar (string_of_id fi);
- ope ("BINDERS",List.rev lparams);
- ast_of_typ; ast_of_def ]))
- 0 lfi
- in
- ope("FIX", (nvar (string_of_id f))::listdecl)
-
- | IsCoFix (n,cl,lfn,vt) ->
- let lfi =
- List.map (fun na -> next_name_away na avoid) lfn in
- let def_env =
- List.fold_left
- (fun env id -> add_rel (Name id,()) env) env lfi in
- let def_avoid = lfi@avoid in
- let f = List.nth lfi n in
- let listdecl =
- list_map_i (fun i fi -> ope("CFDECL",
- [nvar (string_of_id fi);
- bdrec avoid env cl.(i);
- bdrec def_avoid def_env vt.(i)]))
- 0 lfi
- in
- ope("COFIX", (nvar (string_of_id f))::listdecl))
-
- and bdize_eqn avoid env constructid construct_params branch =
- let print_underscore = force_wildcard () in
- let cnvar = nvar (string_of_id constructid) in
- let rec buildrec nvarlist avoid env = function
- | _::l, DOP2(Lambda,_,DLAM(x,b)) ->
- let x'=
- if not print_underscore or (dependent (Rel 1) b) then x
- else Anonymous in
- let id = next_name_away x' avoid in
- let new_env = (add_rel (Name id,()) env) in
- let new_avoid = id::avoid in
- let new_nvarlist = (nvar (string_of_id id))::nvarlist in
- buildrec new_nvarlist new_avoid new_env (l,b)
-
- | l, DOP2(Cast,b,_) ->
- (* Oui, il y a parfois des cast *)
- buildrec nvarlist avoid env (l,b)
-
- | x::l, b ->
- (* eta-expansion : n'arrivera plus lorsque tous les
- termes seront construits à partir de la syntaxe Cases
- nommage de la nouvelle variable *)
- let id = next_name_away_with_default "x" x avoid in
- let new_nvarlist = (nvar (string_of_id id))::nvarlist in
- let new_env = (add_rel (Name id,()) env) in
- let new_avoid = id::avoid in
- let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
+(* Main translation function from constr -> ast *)
+
+let old_bdize_depcast opcast at_top env t =
+ let init_avoid = if at_top then ids_of_env env else [] in
+ let rec bdrec avoid env t =
+ match collapse_appl t with
+
+ (* Not well-formed constructions *)
+ | DLAM(na,c) ->
+ (match concrete_name avoid env na c with
+ (Some id,avoid') -> slam(Some (string_of_id id),
+ bdrec avoid' (add_rel (Name id,()) env) c)
+ | (None,avoid') -> slam(None,bdrec avoid' env (pop c)))
+ | DLAMV(na,cl) ->
+ if not(array_exists (dependent (Rel 1)) cl) then
+ slam(None,ope("V$",array_map_to_list
+ (fun c -> bdrec avoid env (pop c)) cl))
+ else
+ let id = next_name_away na avoid
+ in slam(Some (string_of_id id),
+ ope("V$", array_map_to_list
+ (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
+
+ (* Well-formed constructions *)
+ | regular_constr ->
+ (match kind_of_term regular_constr with
+ | IsRel n ->
+ (try match fst(lookup_rel n env) with
+ Name id -> nvar (string_of_id id)
+ | Anonymous -> raise Not_found
+ with Not_found -> ope("REL",[num n]))
+ (* TODO: Change this to subtract the current depth *)
+ | IsMeta n -> ope("META",[num n])
+ | IsVar id -> nvar (string_of_id id)
+ | IsXtra s -> ope("XTRA",[str s])
+ | IsSort s ->
+ (match s with
+ | Prop Null -> ope("PROP",[])
+ | Prop Pos -> ope("SET",[])
+ | Type u -> ope("TYPE",[path_section dummy_loc u.u_sp; num u.u_num]))
+ | IsCast (c1,c2) ->
+ if opcast=WithoutCast
+ then bdrec avoid env c1
+ else ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
+ | IsProd (Anonymous,ty,c) ->
+ (* Anonymous product are never factorized *)
+ ope("PROD",[bdrec [] env ty;slam(None,bdrec avoid env (pop c))])
+ | IsProd (Name _ as na,ty,c) ->
+ let (n,a) = factorize_binder 1 avoid env Prod na ty c in
+ (* PROD et PRODLIST doivent être distingués à cause du cas
+ non dépendant, pour isoler l'implication; peut-être un constructeur
+ ARROW serait-il plus justifié ? *)
+ let oper = if n=1 then "PROD" else "PRODLIST" in
+ ope(oper,[bdrec [] env ty;a])
+ | IsLambda (na,ty,c) ->
+ let (_,a) = factorize_binder 1 avoid env Lambda na ty c in
+ (* LAMBDA et LAMBDALIST se comportent pareil *)
+ ope("LAMBDALIST",[bdrec [] env ty;a])
+ | IsAppL (f,args) ->
+ bdize_app f (List.map (bdrec avoid env) (f::args))
+
+ | IsConst (sp,cl) ->
+ ope("CONST",((path_section dummy_loc sp)::
+ (array_map_to_list (bdrec avoid env) cl)))
+ | IsAbst (sp,cl) ->
+ ope("ABST",((path_section dummy_loc sp)::
+ (array_map_to_list (bdrec avoid env) cl)))
+ | IsMutInd (sp,tyi,cl) ->
+ ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
+ (array_map_to_list (bdrec avoid env) cl)))
+ | IsMutConstruct (sp,tyi,n,cl) ->
+ ope("MUTCONSTRUCT",((path_section dummy_loc sp)::(num tyi)::(num n)::
+ (array_map_to_list (bdrec avoid env) cl)))
+ | IsMutCase (annot,p,c,bl) ->
+ let synth_type = synthetize_type () in
+ let tomatch = bdrec avoid env c in
+ begin match annot with
+ None -> (* Pas d'annotation --> affichage avec vieux Case *)
+ let pred = bdrec avoid env p in
+ let bl' = array_map_to_list (bdrec avoid env) bl in
+ ope("MUTCASE",pred::tomatch::bl')
+ | Some indsp ->
+ let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
+ let lc = lc_of_lmis lmis in
+ let lcparams = Array.map get_params lc in
+ let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in
+ let pred = if synth_type & computable p k & lcparams <> [||]
+ then (str "SYNTH")
+ else bdrec avoid env p in
+ if PrintingIf.active indsp
+ then ope("FORCEIF", [ pred; tomatch;
+ bdrec avoid env bl.(0);
+ bdrec avoid env bl.(1) ])
+ else
+ let idconstructs = mip.mind_consnames in
+ let asttomatch = ope("TOMATCH", [tomatch]) in
+ let eqnv =
+ array_map3 (bdize_eqn avoid env) idconstructs
+ lcparams bl in
+ let eqnl = Array.to_list eqnv in
+ let tag =
+ if PrintingLet.active indsp then "FORCELET" else "MULTCASE"
+ in ope(tag,pred::asttomatch::eqnl)
+ end
+
+ | IsFix (nv,n,cl,lfn,vt) ->
+ let lfi = List.map (fun na -> next_name_away na avoid) lfn in
+ let def_env = List.fold_left
+ (fun env id -> add_rel (Name id,()) env) env lfi in
+ let def_avoid = lfi@avoid in
+ let f = List.nth lfi n in
+ let rec split_lambda binds env avoid = function
+ (0, t) -> (binds,bdrec avoid env t)
+ | (n, DOP2(Cast,t,_)) -> split_lambda binds env avoid (n,t)
+ | (n, DOP2(Lambda,t,DLAM(na,b))) ->
+ let ast = bdrec avoid env t in
+ let id = next_name_away na avoid in
+ let ast_of_bind = ope("BINDER",[ast;nvar (string_of_id id)]) in
+ let new_env = add_rel (Name id,()) env in
+ split_lambda (ast_of_bind::binds) new_env (id::avoid) (n-1,b)
+ | _ -> error "split_lambda" in
+ let rec split_product env avoid = function
+ (0, t) -> bdrec avoid env t
+ | (n, DOP2(Cast,t,_)) -> split_product env avoid (n,t)
+ | (n, DOP2(Prod,t,DLAM(na,b))) ->
+ let ast = bdrec avoid env t in
+ let id = next_name_away na avoid in
+ let new_env = add_rel (Name id,()) env in
+ split_product new_env (id::avoid) (n-1,b)
+ | _ -> error "split_product" in
+ let listdecl =
+ list_map_i
+ (fun i fi ->
+ let (lparams,ast_of_def) =
+ split_lambda [] def_env def_avoid (nv.(i)+1,vt.(i)) in
+ let ast_of_typ = split_product env avoid (nv.(i)+1,cl.(i)) in
+ ope("FDECL",
+ [nvar (string_of_id fi); ope ("BINDERS",List.rev lparams);
+ ast_of_typ; ast_of_def ]))
+ 0 lfi
+ in ope("FIX", (nvar (string_of_id f))::listdecl)
+
+ | IsCoFix (n,cl,lfn,vt) ->
+ let lfi = List.map (fun na -> next_name_away na avoid) lfn in
+ let def_env =
+ List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in
+ let def_avoid = lfi@avoid in
+ let f = List.nth lfi n in
+ let listdecl =
+ list_map_i (fun i fi -> ope("CFDECL",
+ [nvar (string_of_id fi);
+ bdrec avoid env cl.(i);
+ bdrec def_avoid def_env vt.(i)]))
+ 0 lfi
+ in ope("COFIX", (nvar (string_of_id f))::listdecl))
+
+ and bdize_eqn avoid env constructid construct_params branch =
+ let print_underscore = force_wildcard () in
+ let cnvar = nvar (string_of_id constructid) in
+ let rec buildrec nvarlist avoid env = function
+
+ _::l, DOP2(Lambda,_,DLAM(x,b))
+ -> let x'=
+ if not print_underscore or (dependent (Rel 1) b) then x
+ else Anonymous in
+ let id = next_name_away x' avoid in
+ let new_env = (add_rel (Name id,()) env) in
+ let new_avoid = id::avoid in
+ let new_nvarlist = (nvar (string_of_id id))::nvarlist in
+ buildrec new_nvarlist new_avoid new_env (l,b)
+
+ | l , DOP2(Cast,b,_) (* Oui, il y a parfois des cast *)
+ -> buildrec nvarlist avoid env (l,b)
+
+ | x::l, b (* eta-expansion : n'arrivera plus lorsque tous les
+ termes seront construits à partir de la syntaxe Cases *)
+ -> (* nommage de la nouvelle variable *)
+ let id = next_name_away_with_default "x" x avoid in
+ let new_nvarlist = (nvar (string_of_id id))::nvarlist in
+ let new_env = (add_rel (Name id,()) env) in
+ let new_avoid = id::avoid in
+ let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
buildrec new_nvarlist new_avoid new_env (l,new_b)
- | [], b ->
- let pattern =
- if nvarlist = [] then cnvar
- else ope ("APPLIST", cnvar::(List.rev nvarlist)) in
- let action = bdrec avoid env b in
- ope("XTRA", [str "EQN"; action; pattern])
- in
- buildrec [] avoid env (construct_params,branch)
-
- and factorize_binder n avoid env oper na ty c =
- let (env2, avoid2,na2) =
- match Strategy.concrete_name avoid env na c with
- | (Some id,l') ->
- add_rel (Name id,()) env, l', Some (string_of_id id)
- | (None,l') ->
- add_rel (Anonymous,()) env, l', None
- in
- let (p,body) = match c with
- | DOP2(oper',ty',DLAM(na',c'))
- when (oper = oper')
- & eq_constr (lift 1 ty) ty'
- & not (na' = Anonymous & oper = Prod)
- -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
- | _ -> (n,bdrec avoid2 env2 c)
- in
- (p,slam(na2, body))
+ | [] , b
+ -> let pattern =
+ if nvarlist = [] then cnvar
+ else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in
+ let action = bdrec avoid env b in
+ ope("EQN", [action; pattern])
+
+ in buildrec [] avoid env (construct_params,branch)
+
+ and factorize_binder n avoid env oper na ty c =
+ let (env2, avoid2,na2) =
+ match concrete_name avoid env na c with
+ (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id)
+ | (None,l') -> add_rel (Anonymous,()) env, l', None
in
+ let (p,body) = match c with
+ DOP2(oper',ty',DLAM(na',c'))
+ when (oper = oper')
+ & eq_constr (lift 1 ty) ty'
+ & not (na' = Anonymous & oper = Prod)
+ -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
+ | _ -> (n,bdrec avoid2 env2 c)
+ in (p,slam(na2, body))
+
+ in
bdrec init_avoid env t
- let bdize = bdize_depcast WithCast
- let bdize_no_casts = bdize_depcast WithoutCast
-
- let lookup_name_as_renamed env t s =
- let rec lookup avoid env n = function
- | DOP2(Prod,_,DLAM(name,c')) ->
- (match Strategy.concrete_name avoid env name c' with
- | (Some id,avoid') ->
- if id=s then (Some n)
- else lookup avoid' (add_rel (Name id,()) env) (n+1) c'
- | (None,avoid') -> lookup avoid' env (n+1) (pop c'))
- | DOP2(Cast,c,_) -> lookup avoid env n c
- | _ -> None
- in
- lookup (Strategy.ids_of_env env) env 1 t
-
- let lookup_index_as_renamed t n =
- let rec lookup n d = function
- | DOP2(Prod,_,DLAM(name,c')) ->
- (match Strategy.concrete_name [] (gLOB nil_sign) name c' with
- | (Some _,_) -> lookup n (d+1) c'
- | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
- | DOP2(Cast,c,_) -> lookup n d c
- | _ -> None
- in
- lookup n 1 t
-
-end (* of functor MakeTermAst *)
-
-(* This old version are currently no longer used.
-
-Until V6.2.4, similar names were allowed in hypothesis and quatified
-variables of a goal. This behaviour can still be recovered by using
-the functions available in the WeakTermAst module.
-
-module WeakTermAst = MakeTermAst(WeakRenamingStrategy)
-
-let bdize = WeakTermAst.bdize
-let bdize_no_casts = WeakTermAst.bdize_no_casts
-let lookup_name_as_renamed = WeakTermAst.lookup_name_as_renamed
-let lookup_index_as_renamed = WeakTermAst.lookup_index_as_renamed
+let lookup_name_as_renamed env t s =
+ let rec lookup avoid env n = function
+ DOP2(Prod,_,DLAM(name,c')) ->
+ (match concrete_name avoid env name c' with
+ (Some id,avoid') ->
+ if id=s then (Some n)
+ else lookup avoid' (add_rel (Name id,()) env) (n+1) c'
+ | (None,avoid') -> lookup avoid' env (n+1) (pop c'))
+ | DOP2(Cast,c,_) -> lookup avoid env n c
+ | _ -> None
+ in lookup (ids_of_env env) env 1 t
+
+let lookup_index_as_renamed t n =
+ let rec lookup n d = function
+ DOP2(Prod,_,DLAM(name,c')) ->
+ (match concrete_name [] (gLOB nil_sign) name c' with
+ (Some _,_) -> lookup n (d+1) c'
+ | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+ | DOP2(Cast,c,_) -> lookup n d c
+ | _ -> None
+ in lookup n 1 t
+
+(*
+Until V6.2.4, similar names were allowed in hypothesis and quantified
+variables of a goal.
*)
-module StrongTermAst = MakeTermAst(StrongRenamingStrategy)
+(* $Id$ *)
-let bdize = StrongTermAst.bdize
-let bdize_no_casts = StrongTermAst.bdize_no_casts
-let lookup_name_as_renamed = StrongTermAst.lookup_name_as_renamed
-let lookup_index_as_renamed = StrongTermAst.lookup_index_as_renamed
+exception StillDLAM;;
+
+let rec detype t =
+ match collapse_appl t with
+ (* Not well-formed constructions *)
+ | DLAM _ | DLAMV _ -> raise StillDLAM
+ (* Well-formed constructions *)
+ | regular_constr ->
+ (match kind_of_term regular_constr with
+ | IsRel n -> RRel (dummy_loc,n)
+ | IsMeta n -> RRef (dummy_loc,RMeta n)
+ | IsVar id -> RRef (dummy_loc,RVar id)
+ | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
+ (* ope("XTRA",((str s):: pl@(List.map detype cl)))*)
+ | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
+ | IsSort (Type _) -> RSort (dummy_loc,RType)
+ | IsCast (c1,c2) -> RCast(dummy_loc,detype c1,detype c2)
+ | IsProd (na,ty,c) -> RBinder (dummy_loc,BProd,na,detype ty,detype c)
+ | IsLambda (na,ty,c) -> RBinder (dummy_loc,BLambda,na,detype ty,detype c)
+ | IsAppL (f,args) -> RApp (dummy_loc,detype f,List.map detype args)
+ | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
+ | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr"
+ | IsMutInd (sp,tyi,cl) -> RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
+ | IsMutConstruct (sp,tyi,n,cl) ->
+ RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
+ | IsMutCase (annot,p,c,bl) ->
+ let synth_type = synthetize_type () in
+ let tomatch = detype c in
+ begin match annot with
+ None -> (* Pas d'annotation --> affichage avec vieux Case *)
+ warning "Printing in old Case syntax";
+ ROldCase (dummy_loc,false,Some (detype p),
+ tomatch,Array.map detype bl)
+ | Some indsp ->
+ let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
+ let lc = lc_of_lmis lmis in
+ let lcparams = Array.map get_params lc in
+ let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in
+ let pred = if synth_type & computable p k & lcparams <> [||]
+ then None
+ else Some (detype p) in
+ let constructs =
+ Array.init
+ (Array.length mip.mind_consnames)
+ (fun i -> ((indsp,i),[] (* on triche *))) in
+ let eqnv = array_map3 bdize_eqn constructs lcparams bl in
+ let eqnl = Array.to_list eqnv in
+ let tag =
+ if PrintingLet.active indsp then PrintLet else
+ if PrintingIf.active indsp then PrintIf else PrintCases
+ in RCases (dummy_loc,tag,pred,[tomatch],eqnl)
+ end
+
+ | IsFix (nv,n,cl,lfn,vt) ->
+ let l = Array.of_list (List.map
+ (function Name id -> id | Anonymous -> anomaly"detype") lfn) in
+ RRec(dummy_loc,RFix (nv,n),l,Array.map detype cl,Array.map detype vt)
+ | IsCoFix (n,cl,lfn,vt) ->
+ let l = Array.of_list (List.map
+ (function Name id -> id | Anonymous -> anomaly"detype") lfn) in
+ RRec(dummy_loc,RCofix n,l,Array.map detype cl,Array.map detype vt))
+
+ and bdize_eqn constr_id construct_params branch =
+ let avoid = global_vars_and_consts branch in
+ let make_pat x avoid b =
+ if not (force_wildcard ()) or (dependent (Rel 1) b) then
+ let id = next_name_away x avoid in
+ (PatVar (dummy_loc,Name id)),id::avoid,id
+ else PatVar (dummy_loc,Anonymous),avoid,id_of_string "_" in
+ let rec buildrec idl patlist avoid = function
+
+ _::l, DOP2(Lambda,_,DLAM(x,b))
+ -> let pat,new_avoid,id = make_pat x avoid b in
+ buildrec (id::idl) (pat::patlist) new_avoid (l,b)
+
+ | l , DOP2(Cast,b,_) (* Oui, il y a parfois des cast *)
+ -> buildrec idl patlist avoid (l,b)
+
+ | x::l, b (* eta-expansion : n'arrivera plus lorsque tous les
+ termes seront construits à partir de la syntaxe Cases *)
+ -> (* nommage de la nouvelle variable *)
+ let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
+ let pat,new_avoid,id = make_pat x avoid new_b in
+ buildrec (id::idl) (pat::patlist) new_avoid (l,new_b)
+
+ | [] , rhs
+ -> (idl, [PatCstr(dummy_loc, constr_id, List.rev patlist)], detype rhs)
+ in buildrec [] [] avoid (construct_params,branch)
+;;
+
+let implicit_of_ref = function
+ | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
+ | RInd (indid,_) -> inductive_implicits_list indid
+ | RConst (sp,_) -> constant_implicits_list sp
+ | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+ | _ -> []
+
+let ast_of_app impl f args =
+ if impl = []
+ then ope("APPLIST", f::args)
+ else if !print_implicits
+ then ope("APPLISTEXPL", (f::args))
+ else
+ let largs = List.length args in
+ let impl = List.rev (filter_until largs impl) in
+ let impl1,impl2=div_implicits largs impl in
+ let al1 = Array.of_list args in
+ List.iter
+ (fun i -> al1.(i) <-
+ ope("EXPL", [str "EX"; num i; al1.(i)]))
+ impl2;
+ List.iter
+ (fun i -> al1.(i) <-
+ ope("EXPL",[num i; al1.(i)]))
+ impl1;
+ (* On laisse les implicites, à charge du PP de ne pas les imprimer *)
+ ope("APPLISTEXPL",f::(Array.to_list al1))
+
+let rec ast_of_raw avoid env = function
+ | RRef (_,ref) -> ast_of_ref ref
+ | RRel (_,n) ->
+ (try match fst (lookup_rel n env) with
+ Name id -> ast_of_ident id
+ | Anonymous ->
+ anomaly "ast_of_raw: index to an anonymous variable"
+ with Not_found ->
+ ope("REL",[num (n - List.length (get_rels env))]))
+ | RApp (_,f,args) ->
+ let astf = ast_of_raw avoid env f in
+ let astargs = List.map (ast_of_raw avoid env ) args in
+ (match f with
+ RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
+ | _ -> ast_of_app [] astf astargs)
+ | RBinder (_,BProd,Anonymous,t,c) ->
+ (* Anonymous product are never factorized *)
+ ope("PROD",[ast_of_raw avoid env t;
+ slam(None,ast_of_raw avoid (add_rel (Anonymous,()) env) c)])
+ | RBinder (_,bk,na,t,c) ->
+ let (n,a) = factorize_binder 1 avoid env bk na t c in
+ let tag = match bk with
+ (* LAMBDA et LAMBDALIST se comportent pareil *)
+ BLambda -> "LAMBDALIST"
+ (* PROD et PRODLIST doivent être distingués à cause du cas *)
+ (* non dépendant, pour isoler l'implication; peut-être un *)
+ (* constructeur ARROW serait-il plus justifié ? *)
+ | BProd -> if n=1 then "PROD" else "PROLIST" in
+ ope(tag,[ast_of_raw [] env t;a])
+
+ | RCases (_,printinfo,typopt,tml,eqns) ->
+ let pred = ast_of_rawopt avoid env typopt in
+ let tag = match printinfo with
+ PrintIf -> "FORCEIF"
+ | PrintLet -> "FORCELET"
+ | PrintCases -> "MULTCASE" in
+ let asttomatch = ope("TOMATCH", List.map (ast_of_raw avoid env) tml) in
+ let asteqns = List.map (ast_of_eqn avoid env) eqns
+ in ope(tag,pred::asttomatch::asteqns)
+
+ | ROldCase (_,isrec,typopt,tm,bv) ->
+ warning "Old Case syntax";
+ ope("MUTCASE",(ast_of_rawopt avoid env typopt)
+ ::(ast_of_raw avoid env tm)
+ ::(Array.to_list (Array.map (ast_of_raw avoid env) bv)))
+ | RRec (_,fk,idv,tyv,bv) ->
+ let lfi = Array.map (fun id -> next_ident_away id avoid) idv in
+ let alfi = Array.map ast_of_ident lfi in
+ let def_avoid = (Array.to_list lfi)@avoid in
+ let def_env =
+ List.fold_left (fun env id -> add_rel (Name id,()) env) env
+ (Array.to_list lfi) in
+ (match fk with
+ | RFix (nv,n) ->
+ let rec split_lambda binds avoid env = function
+ (0, t) -> (binds,ast_of_raw avoid env t)
+ | (n, RBinder(_,BLambda,na,t,b)) ->
+ let ast = ast_of_raw avoid env t in
+ let id = next_name_away na avoid in
+ let bind = ope("BINDER",[ast;ast_of_ident id]) in
+ split_lambda (bind::binds) (id::avoid)
+ (add_rel (na,()) env) (n-1,b)
+ | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
+ let rec split_product avoid env = function
+ (0, t) -> ast_of_raw avoid env t
+ | (n, RBinder(_,BProd,na,t,b)) ->
+ let id = next_name_away na avoid in
+ split_product (id::avoid) (add_rel (na,()) env) (n-1,b)
+ | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
+ let listdecl =
+ Array.mapi
+ (fun i fi ->
+ let (lparams,astdef) =
+ split_lambda [] avoid def_env (nv.(i)+1,bv.(i)) in
+ let asttyp = split_product avoid env (nv.(i)+1,tyv.(i)) in
+ ope("FDECL",
+ [fi; ope ("BINDERS",List.rev lparams); asttyp; astdef]))
+ alfi
+ in ope("FIX", alfi.(n)::(Array.to_list listdecl))
+ | RCofix n ->
+ let listdecl =
+ Array.mapi (fun i fi -> ope("CFDECL",
+ [fi;
+ ast_of_raw avoid env tyv.(i);
+ ast_of_raw def_avoid def_env bv.(i)]))
+ alfi
+ in ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
+
+ | RSort (_,s) ->
+ (match s with
+ | RProp Null -> ope("PROP",[])
+ | RProp Pos -> ope("SET",[])
+ | RType -> ope("TYPE",[]))
+ | RHole _ -> ope("ISEVAR",[])
+ | RCast (_,c,t) ->
+ ope("CAST",[ast_of_raw avoid env c;ast_of_raw avoid env t])
+
+and ast_of_eqn avoid env (idl,pl,c) =
+ let new_env =
+ List.fold_left (fun env id -> add_rel (Name id,()) env) env idl in
+ let rhs = ast_of_raw avoid new_env c in
+ ope("EQN", rhs::(List.map ast_of_pattern pl))
+
+and ast_of_rawopt avoid env = function
+ | None -> (str "SYNTH")
+ | Some p -> ast_of_raw avoid env p
+
+and factorize_binder n avoid env oper na ty c =
+ let (env2, avoid2,na2) =
+ match weak_concrete_name avoid env na c with
+ (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id)
+ | (None,l') -> add_rel (Anonymous,()) env, l', None
+ in
+ let (p,body) = match c with
+ RBinder(_,oper',na',ty',c')
+ when (oper = oper')
+ & (ast_of_raw avoid env ty)
+ = (ast_of_raw avoid (add_rel (na,()) env) ty')
+ & not (na' = Anonymous & oper = BProd)
+ -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
+ | _ -> (n,ast_of_raw avoid2 env2 c)
+ in (p,slam(na2, body))
+
+(* A brancher sur le vrai concrete_name *)
+and weak_concrete_name avoid env na c =
+ match na with
+ Anonymous -> (None,avoid)
+ | Name id -> (Some id,avoid)
+;;
+
+let bdize_no_casts at_top env t =
+ try
+ let avoid = if at_top then ids_of_env env else [] in
+ ast_of_raw avoid env (detype t)
+ with StillDLAM -> old_bdize_depcast WithoutCast at_top env t
+
+(* En attendant que strong aille dans term.ml *)
+let rec strong whdfun t =
+ match whdfun t with
+ DOP0 _ as t -> t
+ (* Cas ad hoc *)
+ | DOP1(oper,c) -> DOP1(oper,strong whdfun c)
+ | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2)
+ | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl)
+ | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl)
+ | DLAM(na,c) -> DLAM(na,strong whdfun c)
+ | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c)
+ | VAR _ as t -> t
+ | Rel _ as t -> t
+
+let bdize at_top env t = bdize_no_casts at_top env (strong strip_outer_cast t)
+
+let ast_of_rawconstr = ast_of_raw []
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 06cab8244..fd704d48b 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -5,12 +5,15 @@
open Names
open Term
open Sign
+open Rawterm
(*i*)
-(* Translation of terms into syntax trees. Used for pretty-printing. *)
-
val print_implicits : bool ref
+(* Translation of pattern, rawterm and term into syntax trees for printing *)
+
+val ast_of_pattern : pattern -> Coqast.t
+val ast_of_rawconstr : unit assumptions -> rawconstr -> Coqast.t
val bdize : bool -> unit assumptions -> constr -> Coqast.t
val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
@@ -18,3 +21,7 @@ val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
val lookup_name_as_renamed :
unit assumptions -> constr -> identifier -> int option
val lookup_index_as_renamed : constr -> int -> int option
+
+(*i This is temporary *)
+val ids_of_ctxt : constr array -> identifier list
+(*i*)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 533d1f3c1..dc398cc36 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -227,77 +227,10 @@ let coe_value i =
let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
v,b
-(* pretty-print functions *)
-
-open Printer
-
-let string_of_strength = function
- | NeverDischarge -> "(global)"
- | DischargeAt sp -> "(disch@"^(string_of_path sp)
-
-let print_coercion_value v = prterm v.cOE_VALUE.uj_val
-
-let print_index_coercion c =
- let _,v = coercion_info_from_index c in
- print_coercion_value v
-
-let print_class i =
- let cl,x = class_info_from_index i in
- [< 'sTR x.cL_STR >]
-
-let print_path ((i,j),p) =
- [< 'sTR"[";
- prlist_with_sep (fun () -> [< 'sTR"; " >])
- (fun c -> print_index_coercion c) p;
- 'sTR"] : "; print_class i; 'sTR" >-> ";
- print_class j >]
-
-let print_graph () =
- [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >]
-
-let print_classes () =
- [< prlist_with_sep pr_spc
- (fun (_,(cl,x)) ->
- [< 'sTR x.cL_STR (*; 'sTR(string_of_strength x.cL_STRE) *) >])
- (!cLASSES) >]
-
-let print_coercions () =
- [< prlist_with_sep pr_spc
- (fun (_,(_,v)) -> [< print_coercion_value v >]) (!cOERCIONS) >]
-
-let cl_of_id id =
- match string_of_id id with
- | "FUNCLASS" -> CL_FUN
- | "SORTCLASS" -> CL_SORT
- | _ -> let v = Declare.global_reference CCI id in
- let cl,_ = constructor_at_head v in
- cl
-
-let index_cl_of_id id =
- try
- let cl = cl_of_id id in
- let i,_=class_info cl in
- i
- with _ ->
- errorlabstrm "index_cl_of_id"
- [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
-
-let print_path_between ids idt =
- let i = (index_cl_of_id ids) in
- let j = (index_cl_of_id idt) in
- let p =
- try
- lookup_path_between (i,j)
- with _ ->
- errorlabstrm "index_cl_of_id"
- [< 'sTR"No path between ";'sTR(string_of_id ids);
- 'sTR" and ";'sTR(string_of_id ids) >]
- in
- print_path ((i,j),p)
-
+(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)
-let message_ambig l =
+let message_ambig l =
[< 'sTR"Ambiguous paths : ";
prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8c2f84887..709b26b85 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -43,7 +43,9 @@ type inheritance_path = int list
val cte_of_constr : constr -> cte_typ
val class_info : cl_typ -> (int * cl_info_typ)
+val class_info_from_index : int -> cl_typ * cl_info_typ
val coercion_info : coe_typ -> (int * coe_info_typ)
+val coercion_info_from_index : int -> coe_typ * coe_info_typ
val constructor_at_head : constr -> cl_typ * int
val class_of : env -> 'c evar_map -> constr -> constr * int
val class_args_of : constr -> constr list
@@ -55,10 +57,6 @@ val lookup_path_between : (int * int) -> inheritance_path
val lookup_path_to_fun_from : int -> inheritance_path
val lookup_path_to_sort_from : int -> inheritance_path
val coe_value : int -> (unsafe_judgment * bool)
-val print_graph : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_classes : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_coercions : unit -> (int * string) Pp.ppcmd_token Stream.t
-val print_path_between : identifier -> identifier -> (int * string) ppcmd_token Stream.t
val arity_sort : constr -> int
val fully_applied : identifier -> int -> int -> unit
val stre_of_cl : cl_typ -> strength
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 500e6bfe7..96e97a040 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -328,7 +328,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
check_cofix env !isevars cofix;
make_judge cofix lara.(i))
-| RSort (loc,RProp c) -> make_judge_of_prop_contents c
+| RSort (loc,RProp c) -> judge_of_prop_contents c
| RSort (loc,RType) ->
{ uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort }
@@ -424,7 +424,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
uj_kind = snd (splay_prod env !isevars evalPt)}
| RCases (loc,prinfo,po,tml,eqns) ->
- Multcase.compile_multcase
+ Cases.compile_multcase
((fun vtyc env -> pretype vtyc env isevars),isevars)
vtcon env (po,tml,eqns)
@@ -473,6 +473,11 @@ let j_apply f env sigma j =
variables du sigma original. il faudrait que la fonction de typage
retourne aussi le nouveau sigma...
*)
+let ise_resolve_casted sigma env typ c =
+ let isevars = ref sigma in
+ let j = unsafe_fmachine (mk_tycon typ) false isevars [] env c in
+ (j_apply (fun _ -> process_evars true) env !isevars j).uj_val
+
let ise_resolve fail_evar sigma metamap env c =
let isevars = ref sigma in
let j = unsafe_fmachine mt_tycon false isevars metamap env c in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 995779783..c22653dab 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -49,6 +49,9 @@ val ise_resolve_type : bool -> unit evar_map -> (int * constr) list ->
* if we must coerce to a type *)
val ise_resolve1 : bool -> unit evar_map -> env -> rawconstr -> constr
+val ise_resolve_casted : unit evar_map -> env ->
+ constr -> rawconstr -> constr
+
(* progmach.ml tries to type ill-typed terms: does not perform the conversion
* test in application.
*)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 03d0d6e47..29fdf560c 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -11,12 +11,9 @@ open Type_errors
type loc = int * int
-type inductive_key = section_path * int
-type constructor_key = inductive_key * int
-
type pattern = (* locs here refers to the ident's location, not whole pat *)
| PatVar of loc * name
- | PatCstr of loc * (constructor_key * identifier list) * pattern list
+ | PatCstr of loc * (constructor_path * identifier list) * pattern list
| PatAs of loc * identifier * pattern
type binder_kind = BProd | BLambda
@@ -25,8 +22,8 @@ type rawsort = RProp of Term.contents | RType
type reference =
| RConst of section_path * identifier list
- | RInd of inductive_key * identifier list
- | RConstruct of constructor_key * identifier list
+ | RInd of inductive_path * identifier list
+ | RConstruct of constructor_path * identifier list
| RAbst of section_path
| RVar of identifier
| REVar of int * identifier list
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 44af99e19..af922be37 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -73,10 +73,10 @@ let rec execute mf env sigma cstr =
make_judge cofix larv.(i)
| IsSort (Prop c) ->
- make_judge_of_prop_contents c
+ judge_of_prop_contents c
| IsSort (Type u) ->
- let (j,_) = make_judge_of_type u in j
+ let (j,_) = judge_of_type u in j
| IsAppL (f,args) ->
let j = execute mf env sigma f in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 28ff39345..b2f65c84d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1051,7 +1051,7 @@ let _ =
let rec aux t = function
| 0 -> t
| n -> aux (ope("APPLIST",
- [t;ope("XTRA", [str "ISEVAR"])])) (n-1)
+ [t;ope("ISEVAR",[])])) (n-1)
in
syntax_definition id (aux com n);
if not(is_silent()) then
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 03:53:46 +0000