summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /parsing
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml48
-rw-r--r--parsing/egrammar.ml8
-rw-r--r--parsing/g_ascii_syntax.ml2
-rw-r--r--parsing/g_constr.ml419
-rw-r--r--parsing/g_ltac.ml44
-rw-r--r--parsing/g_proofs.ml44
-rw-r--r--parsing/g_tactic.ml424
-rw-r--r--parsing/g_vernac.ml425
-rw-r--r--parsing/g_xml.ml491
-rw-r--r--parsing/lexer.ml4381
-rw-r--r--parsing/pcoq.ml453
-rw-r--r--parsing/pcoq.mli41
-rw-r--r--parsing/ppconstr.ml37
-rw-r--r--parsing/ppconstr.mli11
-rw-r--r--parsing/pptactic.ml350
-rw-r--r--parsing/ppvernac.ml40
-rw-r--r--parsing/prettyp.ml8
-rw-r--r--parsing/printer.ml9
-rw-r--r--parsing/printer.mli7
-rw-r--r--parsing/q_coqast.ml428
-rw-r--r--parsing/tacextend.ml48
21 files changed, 711 insertions, 447 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 650afe17..ec3c2c9c 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: argextend.ml4 7739 2005-12-26 17:08:16Z herbelin $ *)
+(* $Id: argextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
open Genarg
open Q_util
@@ -30,7 +30,6 @@ let rec make_rawwit loc = function
| ConstrArgType -> <:expr< Genarg.rawwit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
| QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
- | TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >>
| RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
| OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
| ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
@@ -56,7 +55,6 @@ let rec make_globwit loc = function
| SortArgType -> <:expr< Genarg.globwit_sort >>
| ConstrArgType -> <:expr< Genarg.globwit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
- | TacticArgType n -> <:expr< Genarg.globwit_tactic $mlexpr_of_int n$ >>
| RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
| OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
| ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
@@ -82,7 +80,6 @@ let rec make_wit loc = function
| SortArgType -> <:expr< Genarg.wit_sort >>
| ConstrArgType -> <:expr< Genarg.wit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
- | TacticArgType n -> <:expr< Genarg.wit_tactic $mlexpr_of_int n$ >>
| RedExprArgType -> <:expr< Genarg.wit_red_expr >>
| OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
| ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
@@ -193,6 +190,9 @@ let rec interp_entry_name loc s =
OptArgType t, <:expr< Gramext.Sopt $g$ >>
else
let t, se =
+ if tactic_genarg_level s <> None then
+ Some (ExtraArgType s), <:expr< Tactic. tactic >>
+ else
match Pcoq.entry_type (Pcoq.get_univ "prim") s with
| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
| None ->
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c723175c..9ec7c532 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml 7762 2005-12-30 10:55:33Z herbelin $ *)
+(* $Id: egrammar.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
open Pp
open Util
@@ -160,7 +160,7 @@ type grammar_tactic_production =
let make_prod_item = function
| TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
- | TacNonTerm (_,(nont,t), po) -> (nont, option_app (fun p -> (p,t)) po)
+ | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po)
(* Tactic grammar extensions *)
@@ -210,7 +210,7 @@ let rec interp_entry_name up_level u s =
else
try
let i = find_index "tactic" s in
- TacticArgType i,
+ ExtraArgType s,
if i=up_level then Gramext.Sself else
if i=up_level-1 then Gramext.Snext else
Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
@@ -232,7 +232,7 @@ let make_vprod_item n univ = function
| VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
| VNonTerm (loc, nt, po) ->
let (etyp, e) = interp_entry_name n univ nt in
- e, option_app (fun p -> (p,etyp)) po
+ e, option_map (fun p -> (p,etyp)) po
let get_tactic_entry n =
if n = 0 then
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index e6324e00..ac54fc63 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -72,7 +72,7 @@ let make_ascii_string n =
if n>=32 && n<=126 then String.make 1 (char_of_int n)
else Printf.sprintf "%03d" n
-let uninterp_ascii_string r = option_app make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r)
let _ =
Notation.declare_string_interpreter "char_scope"
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9f7f7304..9ee312ff 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_constr.ml4 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: g_constr.ml4 8875 2006-05-29 19:59:11Z msozeau $ *)
open Pcoq
open Constr
@@ -28,7 +28,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
let mk_cast = function
(c,(_,None)) -> c
- | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty)
+ | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty)
let mk_lam = function
([],c) -> c
@@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c =
let rec index_and_rec_order_of_annot loc bl ann =
match names_of_local_assums bl,ann with
- | [_], (None, r) -> 0, r
+ | [_], (None, r) -> Some 0, r
| lids, (Some x, ro) ->
let ids = List.map snd lids in
- (try list_index (snd x) ids - 1, ro
+ (try Some (list_index (snd x) ids - 1), ro
with Not_found ->
user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
- | _ -> user_err_loc(loc,"index_of_annot",
- Pp.str "cannot guess decreasing argument of fix")
+ | _, (None, r) -> None, r
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
@@ -76,7 +75,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
(snd id,(n,ro),bl,ty,body)
let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
- let _ = option_app (fun (aloc,_) ->
+ let _ = option_map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofixb",
Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
@@ -156,8 +155,8 @@ GEXTEND Gram
[ "200" RIGHTA
[ c = binder_constr -> c ]
| "100" RIGHTA
- [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2)
- | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ]
+ [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2)
+ | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ]
| "99" RIGHTA [ ]
| "90" RIGHTA
[ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -321,7 +320,7 @@ GEXTEND Gram
| "("; id=name; ":="; c=lconstr; ")" ->
LocalRawDef (id,c)
| "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t))
+ LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t))
] ]
;
binder:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 6ed22c7e..eaa51810 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_ltac.ml4 8129 2006-03-05 09:05:12Z herbelin $ *)
+(* $Id: g_ltac.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
open Pp
open Util
@@ -23,7 +23,7 @@ type let_clause_kind =
| LETCLAUSE of
(Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
-let fail_default_value = Genarg.ArgArg 0
+let fail_default_value = ArgArg 0
let out_letin_clause loc = function
| LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 886b33e2..94205fa8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_proofs.ml4 7936 2006-01-28 18:36:54Z herbelin $ *)
+(* $Id: g_proofs.ml4 8875 2006-05-29 19:59:11Z msozeau $ *)
open Pcoq
open Pp
@@ -117,6 +117,6 @@ GEXTEND Gram
;
constr_body:
[ [ ":="; c = lconstr -> c
- | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
+ | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ]
;
END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1974d8bc..cba2e7d0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_tactic.ml4 8651 2006-03-21 21:54:43Z jforest $ *)
+(* $Id: g_tactic.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
open Pp
open Pcoq
@@ -102,7 +102,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
(id,n,CProdN(loc,bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
- let _ = option_app (fun (aloc,_) ->
+ let _ = option_map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofix_tac",
Pp.str"Annotation forbidden in cofix expression")) ann in
@@ -121,8 +121,8 @@ GEXTEND Gram
simple_intropattern;
int_or_var:
- [ [ n = integer -> Genarg.ArgArg n
- | id = identref -> Genarg.ArgVar id ] ]
+ [ [ n = integer -> Rawterm.ArgArg n
+ | id = identref -> Rawterm.ArgVar id ] ]
;
(* An identifier or a quotation meta-variable *)
id_or_meta:
@@ -155,11 +155,11 @@ GEXTEND Gram
conversion:
[ [ c = constr -> (None, c)
| c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
- | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
+ | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr ->
(Some (nl,c1), c2) ] ]
;
occurrences:
- [ [ "at"; nl = LIST1 integer -> nl
+ [ [ "at"; nl = LIST1 int_or_var -> nl
| -> [] ] ]
;
pattern_occ:
@@ -240,7 +240,7 @@ GEXTEND Gram
] ]
;
hypident_occ:
- [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ]
+ [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ]
;
clause:
[ [ "in"; "*"; occs=occurrences ->
@@ -261,6 +261,11 @@ GEXTEND Gram
[ [ "in"; idl = LIST1 id_or_meta -> idl
| -> [] ] ]
;
+ orient:
+ [ [ "->" -> true
+ | "<-" -> false
+ | -> true ]]
+ ;
fixdecl:
[ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
@@ -285,7 +290,8 @@ GEXTEND Gram
[ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
;
by_tactic:
- [ [ IDENT "by"; tac = tactic -> TacComplete tac | -> TacId [] ] ]
+ [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
+ | -> TacId [] ] ]
;
simple_tactic:
[ [
@@ -411,6 +417,8 @@ GEXTEND Gram
| IDENT "transitivity"; c = constr -> TacTransitivity c
(* Equality and inversion *)
+ | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause ->
+ TacRewrite (b,c,cl)
| IDENT "dependent"; k =
[ IDENT "simple"; IDENT "inversion" -> SimpleInversion
| IDENT "inversion" -> FullInversion
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 18a424a8..7405ae54 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_vernac.ml4 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: g_vernac.ml4 8929 2006-06-08 22:35:58Z herbelin $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Pp
@@ -218,16 +218,15 @@ GEXTEND Gram
let ni =
match fst annot with
Some id ->
- (try list_index (Name id) names - 1
- with Not_found -> Util.user_err_loc
- (loc,"Fixpoint",
- Pp.str "No argument named " ++ Nameops.pr_id id))
+ (try Some (list_index (Name id) names - 1)
+ with Not_found -> Util.user_err_loc
+ (loc,"Fixpoint",
+ Pp.str "No argument named " ++ Nameops.pr_id id))
| None ->
- if List.length names > 1 then
- Util.user_err_loc
- (loc,"Fixpoint",
- Pp.str "the recursive argument needs to be specified");
- 0 in
+ (* If there is only one argument, it is the recursive one,
+ otherwise, we search the recursive index later *)
+ if List.length names = 1 then Some 0 else None
+ in
((id, (ni, snd annot), bl, type_, def),ntn) ] ]
;
corec_definition:
@@ -320,8 +319,8 @@ GEXTEND Gram
VernacDeclareModuleType (id, bl, mty_o)
| IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
- bl = LIST0 module_binder; mty_o = of_module_type ->
- VernacDeclareModule (export, id, bl, mty_o)
+ bl = LIST0 module_binder; ":"; mty = module_type ->
+ VernacDeclareModule (export, id, bl, (mty,true))
(* Section beginning *)
| IDENT "Section"; id = identref -> VernacBeginSection id
| IDENT "Chapter"; id = identref -> VernacBeginSection id
@@ -430,7 +429,7 @@ GEXTEND Gram
(* Implicit *)
| IDENT "Implicit"; IDENT "Arguments"; qid = global;
pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
- let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+ let pos = option_map (List.map (fun id -> ExplByName id)) pos in
VernacDeclareImplicits (qid,pos)
| IDENT "Implicit"; ["Type" | IDENT "Types"];
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index b4580750..5ad0193b 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_xml.ml4 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: g_xml.ml4 8875 2006-05-29 19:59:11Z msozeau $ *)
open Pp
open Util
@@ -19,6 +19,7 @@ open Tacexpr
open Libnames
open Nametab
+open Detyping
(* Generic xml parser without raw data *)
@@ -83,7 +84,7 @@ let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a)
let inductive_of_cdata a = match global_of_cdata a with
| IndRef (kn,_) -> kn
- | _ -> failwith "kn"
+ | _ -> anomaly "XML parser: not an inductive"
let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
@@ -95,7 +96,9 @@ let sort_of_cdata (loc,a) = match a with
let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
-let get_xml_inductive_kn al = inductive_of_cdata (get_xml_attr "uri" al)
+let get_xml_inductive_kn al =
+ inductive_of_cdata (* uriType apparent synonym of uri *)
+ (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
@@ -105,43 +108,66 @@ let get_xml_inductive al =
let get_xml_constructor al =
(get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-let get_xml_name al =
+let get_xml_binder al =
try Name (ident_of_cdata (List.assoc "binder" al))
with Not_found -> Anonymous
let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
+let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
+
let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
+let get_xml_no al = nmtoken (get_xml_attr "no" al)
+
+(* A leak in the xml dtd: arities of constructor need to know global env *)
+
+let compute_branches_lengths ind =
+ let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+ mip.Declarations.mind_consnrealdecls
+
+let compute_inductive_nargs ind =
+ Inductiveops.inductive_nargs (Global.env()) ind
+
(* Interpreting constr as a rawconstr *)
let rec interp_xml_constr = function
| XmlTag (loc,"REL",al,[]) ->
RVar (loc, get_xml_ident al)
- | XmlTag (loc,"VAR",al,[]) -> failwith ""
- | XmlTag (loc,"LAMBDA",al,[x1;x2]) ->
- let na,t = interp_xml_decl x1 in
- RLambda (loc, na, t, interp_xml_target x2)
- | XmlTag (loc,"PROD",al,[x1;x2]) ->
- let na,t = interp_xml_decl x1 in
- RProd (loc, na, t, interp_xml_target x2)
+ | XmlTag (loc,"VAR",al,[]) ->
+ error "XML parser: unable to interp free variables"
+ | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
+ let body,decls = list_sep_last xl in
+ let ctx = List.map interp_xml_decl decls in
+ List.fold_right (fun (na,t) b -> RLambda (loc, na, t, b))
+ ctx (interp_xml_target body)
+ | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
+ let body,decls = list_sep_last xl in
+ let ctx = List.map interp_xml_decl decls in
+ List.fold_right (fun (na,t) b -> RProd (loc, na, t, b))
+ ctx (interp_xml_target body)
| XmlTag (loc,"LETIN",al,[x1;x2]) ->
let na,t = interp_xml_def x1 in
RLetIn (loc, na, t, interp_xml_target x2)
| XmlTag (loc,"APPLY",_,x::xl) ->
RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
+ | XmlTag (loc,"instantiate",_,
+ (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
+ RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
| XmlTag (loc,"META",al,xl) ->
- failwith "META: TODO"
+ REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
| XmlTag (loc,"CONST",al,[]) ->
RRef (loc, ConstRef (get_xml_constant al))
- | XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *)
- failwith "XML MUTCASE TO DO";
-(*
- ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x),
- interp_xml_inductiveTerm y,
- Array.of_list (List.map interp_xml_pattern yl),
- ref None)
-*)
+ | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
+ let ind = get_xml_inductive al in
+ let p = interp_xml_patternsType x in
+ let tm = interp_xml_inductiveTerm y in
+ let brs = List.map interp_xml_pattern yl in
+ let brns = Array.to_list (compute_branches_lengths ind) in
+ let mat = simple_cases_matrix_of_branches ind brns brs in
+ let nparams,n = compute_inductive_nargs ind in
+ let nal,rtn = return_type_of_predicate ind nparams n p in
+ RCases (loc,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
RRef (loc, IndRef (get_xml_inductive al))
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
@@ -149,12 +175,13 @@ let rec interp_xml_constr = function
| XmlTag (loc,"FIX",al,xl) ->
let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
let ln,lc,lt = list_split3 lnct in
- RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+ let lctx = List.map (fun _ -> []) ln in
+ RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"COFIX",al,xl) ->
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"CAST",al,[x1;x2]) ->
- RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2)
+ RCast (loc, interp_xml_term x1, CastConv DEFAULTcast, interp_xml_type x2)
| XmlTag (loc,"SORT",al,[]) ->
RSort (loc, get_xml_sort al)
| XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
@@ -177,10 +204,13 @@ and interp_xml_body x = interp_xml_constr_alias "body" x
and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
+and interp_xml_arg x = interp_xml_constr_alias "arg" x
+and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
+ (* no support for empty substitution from official dtd *)
and interp_xml_decl_alias s x =
match interp_xml_tag s x with
- | (_,al,[x]) -> (get_xml_name al, interp_xml_constr x)
+ | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
@@ -201,23 +231,22 @@ and interp_xml_recursionOrder x =
| _ ->
user_err_loc (locs,"",str "invalid recursion order")
-
and interp_xml_FixFunction x =
match interp_xml_tag "FixFunction" x with
- | (loc,al,[x1;x2;x3]) ->
- ((nmtoken (get_xml_attr "recIndex" al),
+ | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
+ ((Some (nmtoken (get_xml_attr "recIndex" al)),
interp_xml_recursionOrder x1),
- (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
- | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
- ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
- (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
+ (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
+ | (loc,al,[x1;x2]) ->
+ ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
+ (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
and interp_xml_CoFixFunction x =
match interp_xml_tag "CoFixFunction" x with
| (loc,al,[x1;x2]) ->
- (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)
+ (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 6119b86e..c02dc59b 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lexer.ml4 7870 2006-01-15 20:29:09Z herbelin $ i*)
+(*i $Id: lexer.ml4 8924 2006-06-08 17:49:01Z notin $ i*)
open Pp
open Token
@@ -54,7 +54,7 @@ let ttree_find ttree str =
in
proc_rec ttree 0
-(* Lexer conventions on tokens *)
+(* Errors occuring while lexing (explained as "Lexer error: ...") *)
type error =
| Illegal_character
@@ -65,8 +65,163 @@ type error =
exception Error of error
+let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str)
+
let bad_token str = raise (Error (Bad_token str))
+(* Lexer conventions on tokens *)
+
+type utf8_token =
+ Utf8Letter of int | Utf8IdentPart of int | Utf8Symbol | AsciiChar
+
+let error_unsupported_unicode_character n cs =
+ let bp = Stream.count cs in
+ err (bp,bp+n) (Bad_token "Unsupported Unicode character")
+
+let error_utf8 cs =
+ let bp = Stream.count cs in
+ err (bp, bp+1) Illegal_character
+
+let njunk n = Util.repeat n Stream.junk
+
+let check_utf8_trailing_byte cs c =
+ if Char.code c land 0xC0 <> 0x80 then error_utf8 cs
+
+(* Recognize utf8 blocks (of length less than 4 bytes) *)
+(* but don't certify full utf8 compliance (e.g. no emptyness check) *)
+let lookup_utf8_tail c cs =
+ let c1 = Char.code c in
+ if c1 land 0x40 = 0 or c1 land 0x38 = 0x38 then error_utf8 cs
+ else
+ let n, unicode =
+ if c1 land 0x20 = 0 then
+ match Stream.npeek 2 cs with
+ | [_;c2] ->
+ check_utf8_trailing_byte cs c2;
+ 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F)
+ | _ -> error_utf8 cs
+ else if c1 land 0x10 = 0 then
+ match Stream.npeek 3 cs with
+ | [_;c2;c3] ->
+ check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
+ 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 +
+ (Char.code c3 land 0x3F)
+ | _ -> error_utf8 cs
+ else match Stream.npeek 4 cs with
+ | [_;c2;c3;c4] ->
+ check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
+ check_utf8_trailing_byte cs c4;
+ 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 +
+ (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
+ | _ -> error_utf8 cs
+ in
+ match unicode land 0x1F000 with
+ | 0x0 ->
+ begin match unicode with
+ (* utf-8 Latin-1 non breaking space U00A0 *)
+ | 0x00A0 -> Utf8Letter n
+ (* utf-8 Latin-1 symbols U00A1-00BF *)
+ | x when 0x00A0 <= x & x <= 0x00BF -> Utf8Symbol
+ (* utf-8 Latin-1 letters U00C0-00D6 *)
+ | x when 0x00C0 <= x & x <= 0x00D6 -> Utf8Letter n
+ (* utf-8 Latin-1 symbol U00D7 *)
+ | 0x00D7 -> Utf8Symbol
+ (* utf-8 Latin-1 letters U00D8-00F6 *)
+ | x when 0x00D8 <= x & x <= 0x00F6 -> Utf8Letter n
+ (* utf-8 Latin-1 symbol U00F7 *)
+ | 0x00F7 -> Utf8Symbol
+ (* utf-8 Latin-1 letters U00F8-00FF *)
+ | x when 0x00F8 <= x & x <= 0x00FF -> Utf8Letter n
+ (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
+ | x when 0x0100 <= x & x <= 0x0241 -> Utf8Letter n
+ (* utf-8 Phonetic letters U0250-02AF *)
+ | x when 0x0250 <= x & x <= 0x02AF -> Utf8Letter n
+ (* utf-8 what do to with diacritics U0300-U036F ? *)
+ (* utf-8 Greek letters U0380-03FF *)
+ | x when 0x0380 <= x & x <= 0x03FF -> Utf8Letter n
+ (* utf-8 Cyrillic letters U0400-0481 *)
+ | x when 0x0400 <= x & x <= 0x0481 -> Utf8Letter n
+ (* utf-8 Cyrillic symbol U0482 *)
+ | 0x0482 -> Utf8Symbol
+ (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
+ (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
+ | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter n
+ (* utf-8 Cyrillic supplements letters U0500-U050F *)
+ | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter n
+ (* utf-8 Hebrew letters U05D0-05EA *)
+ | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter n
+ (* utf-8 Hebrew letters U0621-064A *)
+ | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n
+ | _ -> error_unsupported_unicode_character n cs
+ end
+ | 0x1000 ->
+ begin match unicode with
+ (* utf-8 Georgian U10A0-10FF (has holes) *)
+ | x when 0x10A0 <= x & x <= 0x10FF -> Utf8Letter n
+ (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
+ | x when 0x1100 <= x & x <= 0x11FF -> Utf8Letter n
+ (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
+ | x when 0x1E00 <= x & x <= 0x1E9B -> Utf8Letter n
+ | x when 0x1EA0 <= x & x <= 0x1EF9 -> Utf8Letter n
+ | _ -> error_unsupported_unicode_character n cs
+ end
+ | 0x2000 ->
+ begin match unicode with
+ (* utf-8 general punctuation U2080-2089 *)
+ (* Hyphens *)
+ | x when 0x2010 <= x & x <= 0x2011 -> Utf8Letter n
+ (* Dashes and other symbols *)
+ | x when 0x2012 <= x & x <= 0x2027 -> Utf8Symbol
+ (* Per mille and per ten thousand signs *)
+ | x when 0x2030 <= x & x <= 0x2031 -> Utf8Symbol
+ (* Prime letters *)
+ | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> Utf8IdentPart n
+ (* Miscellaneous punctuation *)
+ | x when 0x2039 <= x & x <= 0x2056 -> Utf8Symbol
+ | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol
+ (* Invisible mathematical operators *)
+ | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol
+
+ (* utf-8 subscript U2080-2089 *)
+ | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart n
+ (* utf-8 letter-like U2100-214F *)
+ | x when 0x2100 <= x & x <= 0x214F -> Utf8Letter n
+ (* utf-8 number-forms U2153-2183 *)
+ | x when 0x2153 <= x & x <= 0x2183 -> Utf8Symbol
+ (* utf-8 arrows A U2190-21FF *)
+ (* utf-8 mathematical operators U2200-22FF *)
+ (* utf-8 miscellaneous technical U2300-23FF *)
+ | x when 0x2190 <= x & x <= 0x23FF -> Utf8Symbol
+ (* utf-8 box drawing U2500-257F has ceiling, etc. *)
+ (* utf-8 block elements U2580-259F *)
+ (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
+ (* utf-8 miscellaneous symbols U2600-26FF *)
+ | x when 0x2500 <= x & x <= 0x26FF -> Utf8Symbol
+ (* utf-8 arrows B U2900-297F *)
+ | x when 0x2900 <= x & x <= 0x297F -> Utf8Symbol
+ (* utf-8 mathematical operators U2A00-2AFF *)
+ | x when 0x2A00 <= x & x <= 0x2AFF -> Utf8Symbol
+ | _ -> error_unsupported_unicode_character n cs
+ end
+ | _ ->
+ begin match unicode with
+ (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
+ | x when 0x3040 <= x & x <= 0x30FF -> Utf8Letter n
+ (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
+ | x when 0x4E00 <= x & x <= 0x9FA5 -> Utf8Letter n
+ (* utf-8 Hangul syllables UAC00-D7AF *)
+ | x when 0xAC00 <= x & x <= 0xD7AF -> Utf8Letter n
+ (* utf-8 Gothic U10330-1034A *)
+ | x when 0x10330 <= x & x <= 0x1034A -> Utf8Letter n
+ | _ -> error_unsupported_unicode_character n cs
+ end
+
+let lookup_utf8 cs =
+ match Stream.peek cs with
+ | Some ('\x00'..'\x7F') -> Some AsciiChar
+ | Some ('\x80'..'\xFF' as c) -> Some (lookup_utf8_tail c cs)
+ | None -> None
+
let check_special_token str =
let rec loop_symb = parser
| [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str
@@ -76,35 +231,19 @@ let check_special_token str =
loop_symb (Stream.of_string str)
let check_ident str =
- let first_letter = function
- (''' | '0'..'9') -> false
- | _ -> true in
- let rec loop_id = parser
- | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_'); s >] ->
- loop_id s
- (* utf-8 Greek letters U0380-03FF *)
- | [< ' ('\xCE' | '\xCF'); ' ('\x80'..'\xBF'); s >] -> loop_id s
- | [< ''\xE2'; 'c2; 'c3; s >] ->
- (match c2, c3 with
- (* utf-8 letter-like U2100-214F *)
- | ( ('\x84', '\x80'..'\xBF')
- | ('\x85', '\x80'..'\x8F')
- (* utf-8 subscript U2080-2089 *)
- | ('\x82', '\x80'..'\x89')) ->
- loop_id s
- (* utf-8 symbols (see [parse_226_tail]) *)
- | (('\x86'..'\x8F' | '\x94'..'\x9B'
- | '\xA4'..'\xA5' | '\xA8'..'\xAB'),_) ->
- bad_token str
- | _ ->
- bad_token str)
- | [< _ = Stream.empty >] -> ()
- | [< >] -> bad_token str
+ let rec loop_id intail = parser
+ | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '_'); s >] ->
+ loop_id true s
+ | [< ' ('0'..'9' | ''') when intail; s >] ->
+ loop_id true s
+ | [< s >] ->
+ match lookup_utf8 s with
+ | Some (Utf8Letter n) -> njunk n s; loop_id true s
+ | Some (Utf8IdentPart n) when intail -> njunk n s; loop_id true s
+ | Some _ -> bad_token str
+ | None -> ()
in
- if String.length str > 0 && first_letter str.[0] then
- loop_id (Stream.of_string str)
- else
- bad_token str
+ loop_id false (Stream.of_string str)
let check_keyword str =
try check_special_token str
@@ -145,9 +284,6 @@ let init () =
let _ = init()
-(* Errors occuring while lexing (explained as "Lexer error: ...") *)
-let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str)
-
(* The string buffering machinery *)
let buff = ref (String.create 80)
@@ -158,36 +294,20 @@ let store len x =
!buff.[len] <- x;
succ len
-let mstore len s =
- let rec add_rec len i =
- if i == String.length s then len else add_rec (store len s.[i]) (succ i)
- in
- add_rec len 0
+let rec nstore n len cs =
+ if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len
let get_buff len = String.sub !buff 0 len
-
(* The classical lexer: idents, numbers, quoted strings, comments *)
let rec ident_tail len = parser
| [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
ident_tail (store len c) s
- (* utf-8 Greek letters U0380-03FF *)
- | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2) ; s >] ->
- ident_tail (store (store len c1) c2) s
| [< s >] ->
- match Stream.peek s with
- | Some '\xE2' ->
- (match List.tl (Stream.npeek 3 s) with
- (* utf-8 subscript U2080-2089 *)
- | ['\x82' as c2; ('\x80'..'\x89' as c3)]
- (* utf-8 letter-like U2100-214F part 1 *)
- | ['\x84' as c2; ('\x80'..'\xBF' as c3)]
- (* utf-8 letter-like U2100-214F part 2 *)
- | ['\x85' as c2; ('\x80'..'\x8F' as c3)] ->
- Stream.junk s; Stream.junk s; Stream.junk s;
- ident_tail (store (store (store len '\xE2') c2) c3) s
- | _ -> len)
+ match lookup_utf8 s with
+ | Some (Utf8IdentPart n | Utf8Letter n) ->
+ ident_tail (nstore n len s) s
| _ -> len
let rec number len = parser
@@ -292,89 +412,61 @@ let rec comment bp = parser bp2
(* Parse a special token, using the [token_tree] *)
-let progress_special c = function
- | None -> None
- | Some tt -> try Some (CharMap.find c tt.branch) with Not_found -> None
-
-let rec special tt cs = match tt with
- | None -> None
- | Some tt ->
- match
- match Stream.peek cs with
- | Some c ->
- (try Some (CharMap.find c tt.branch) with Not_found -> None)
- | None -> None
- with
- | Some _ as tt' -> Stream.junk cs; special tt' cs
- | None -> tt.node
-
+(* Peek as much utf-8 lexemes as possible *)
+(* then look if a special token is obtained *)
+let rec special tt cs =
+ match Stream.peek cs with
+ | Some c -> progress_from_byte 0 tt cs c
+ | None -> tt.node
+
+ (* nr is the number of char peeked; n the number of char in utf8 block *)
+and progress_utf8 nr n c tt cs =
+ try
+ let tt = CharMap.find c tt.branch in
+ let tt =
+ if n=1 then tt else
+ match Stream.npeek (n-nr) cs with
+ | l when List.length l = n-nr ->
+ let l = Util.list_skipn (1-nr) l in
+ List.iter (check_utf8_trailing_byte cs) l;
+ List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l
+ | _ ->
+ error_utf8 cs
+ in
+ for i=1 to n-nr do Stream.junk cs done;
+ special tt cs
+ with Not_found ->
+ tt.node
+
+and progress_from_byte nr tt cs = function
+ (* Utf8 leading byte *)
+ | '\x00'..'\x7F' as c -> progress_utf8 nr 1 c tt cs
+ | '\xC0'..'\xDF' as c -> progress_utf8 nr 2 c tt cs
+ | '\xE0'..'\xEF' as c -> progress_utf8 nr 3 c tt cs
+ | '\xF0'..'\xF7' as c -> progress_utf8 nr 4 c tt cs
+ | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
+ error_utf8 cs
+
+(* Must be a special token *)
let process_chars bp c cs =
- let t =
- try special (Some (CharMap.find c !token_tree.branch)) cs
- with Not_found -> !token_tree.node
- in
+ let t = progress_from_byte 1 !token_tree cs c in
let ep = Stream.count cs in
match t with
| Some t -> (("", t), (bp, ep))
| None -> err (bp, ep) Undefined_token
-type token_226_tail =
- | TokSymbol of string option
- | TokIdent of string
-
-(* 1110xxxx 10yyyyzz 10zztttt utf-8 codes for xxxx=0010 *)
-let parse_226_tail tk = parser
- | [< ''\x82' as c2; ' ('\x80'..'\x89' as c3);
- (* utf-8 subscript U2080-2089 *)
- len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] ->
- TokIdent (get_buff len)
- | [< ''\x84' as c2; ' ('\x80'..'\xBF' as c3);
- (* utf-8 letter-like U2100-214F part 1 *)
- len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] ->
- TokIdent (get_buff len)
- | [< ''\x85' as c2; ' ('\x80'..'\x8F' as c3);
- (* utf-8 letter-like U2100-214F part 2 *)
- len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] ->
- TokIdent (get_buff len)
- | [< ' ('\x86'..'\x8F' | '\x94'..'\x9B' | '\xA4'..'\xA5'
- | '\xA8'..'\xAB' as c2); 'c3;
- (* utf-8 arrows A U2190-21FF *)
- (* utf-8 mathematical operators U2200-22FF *)
- (* utf-8 miscellaneous technical U2300-23FF *)
- (* utf-8 box drawing U2500-257F has ceiling, etc. *)
- (* utf-8 block elements U2580-259F *)
- (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
- (* utf-8 miscellaneous symbols U2600-26FF *)
- (* utf-8 arrows B U2900-297F *)
- (* utf-8 mathematical operators U2A00-2AFF *)
- t = special (progress_special c3 (progress_special c2
- (progress_special '\xE2' tk))) >] ->
- TokSymbol t
- | [< '_; '_ >] ->
- (* Unsupported utf-8 code *)
- TokSymbol None
-
(* Parse what follows a dot *)
let parse_after_dot bp c = parser
- | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
- len = ident_tail (store 0 c) >] ->
- ("FIELD", get_buff len)
- (* utf-8 Greek letters U0380-03FF *)
- | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2);
- len = ident_tail (store (store 0 c1) c2) >] ->
+ | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ->
("FIELD", get_buff len)
- (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
- | [< ''\xE2'; t = parse_226_tail
- (progress_special '.' (Some !token_tree)) >] ep ->
- (match t with
- | TokSymbol (Some t) -> ("", t)
- | TokSymbol None -> err (bp, ep) Undefined_token
- | TokIdent t -> ("FIELD", t))
- | [< (t,_) = process_chars bp c >] -> t
-
+ | [< s >] ->
+ match lookup_utf8 s with
+ | Some (Utf8Letter n) ->
+ ("FIELD", get_buff (ident_tail (nstore n 0 s) s))
+ | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None ->
+ fst (process_chars bp c s)
(* Parse a token in a char stream *)
-
let rec next_token = parser bp
| [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
comm_loc bp; push_char c; next_token s
@@ -383,27 +475,13 @@ let rec next_token = parser bp
(("METAIDENT", get_buff len), (bp,ep))
| [< ''.' as c; t = parse_after_dot bp c >] ep ->
comment_stop bp;
+ if Options.do_translate() & t=("",".") then between_com := true;
(t, (bp,ep))
| [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
len = ident_tail (store 0 c) >] ep ->
let id = get_buff len in
comment_stop bp;
(try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
- (* utf-8 Greek letters U0380-03FF [CE80-CEBF and CF80-CFBF] *)
- | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2);
- len = ident_tail (store (store 0 c1) c2) >] ep ->
- let id = get_buff len in
- comment_stop bp;
- (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
- (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
- | [< ''\xE2'; t = parse_226_tail (Some !token_tree) >] ep ->
- comment_stop bp;
- (match t with
- | TokSymbol (Some t) -> ("", t), (bp, ep)
- | TokSymbol None -> err (bp, ep) Undefined_token
- | TokIdent id ->
- (try ("", find_keyword id) with Not_found -> ("IDENT", id)),
- (bp, ep))
| [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
comment_stop bp;
(("INT", get_buff len), (bp, ep))
@@ -419,8 +497,19 @@ let rec next_token = parser bp
next_token s
| [< t = process_chars bp c >] -> comment_stop bp; t >] ->
t
- | [< 'c; t = process_chars bp c >] -> comment_stop bp; t
- | [< _ = Stream.empty >] -> comment_stop bp; (("EOI", ""), (bp, bp + 1))
+ | [< s >] ->
+ match lookup_utf8 s with
+ | Some (Utf8Letter n) ->
+ let len = ident_tail (nstore n 0 s) s in
+ let id = get_buff len in
+ let ep = Stream.count s in
+ comment_stop bp;
+ (try ("",find_keyword id) with Not_found -> ("IDENT",id)), (bp, ep)
+ | Some (Utf8Symbol | AsciiChar | Utf8IdentPart _) ->
+ let t = process_chars bp (Stream.next s) s in
+ comment_stop bp; t
+ | None ->
+ comment_stop bp; (("EOI", ""), (bp, bp + 1))
(* Location table system for creating tables associating a token count
to its location in a char stream (the source) *)
@@ -461,10 +550,10 @@ let func cs =
Stream.from
(fun i ->
let (tok, loc) = next_token cs in
- loct_add loct i loc; Some tok)
+ loct_add loct i loc; Some tok)
in
- current_location_table := loct;
- (ts, loct_func loct)
+ current_location_table := loct;
+ (ts, loct_func loct)
type location_table = (int * int) option array array ref
let location_table () = !current_location_table
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d743fffa..127a911f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.ml4 7826 2006-01-09 22:00:34Z herbelin $ i*)
+(*i $Id: pcoq.ml4 8926 2006-06-08 20:23:17Z herbelin $ i*)
open Pp
open Util
@@ -286,6 +286,55 @@ let force_entry_type (u, utab) s etyp =
with Not_found ->
new_entry etyp (u, utab) s
+(* Tactics as arguments *)
+
+let tactic_main_level = 5
+
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+
+let wit_tactic = function
+ | 0 -> wit_tactic0
+ | 1 -> wit_tactic1
+ | 2 -> wit_tactic2
+ | 3 -> wit_tactic3
+ | 4 -> wit_tactic4
+ | 5 -> wit_tactic5
+ | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let globwit_tactic = function
+ | 0 -> globwit_tactic0
+ | 1 -> globwit_tactic1
+ | 2 -> globwit_tactic2
+ | 3 -> globwit_tactic3
+ | 4 -> globwit_tactic4
+ | 5 -> globwit_tactic5
+ | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let rawwit_tactic = function
+ | 0 -> rawwit_tactic0
+ | 1 -> rawwit_tactic1
+ | 2 -> rawwit_tactic2
+ | 3 -> rawwit_tactic3
+ | 4 -> rawwit_tactic4
+ | 5 -> rawwit_tactic5
+ | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let tactic_genarg_level s =
+ if String.length s = 7 && String.sub s 0 6 = "tactic" then
+ let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
+ else None
+ else None
+
+let is_tactic_genarg = function
+| ExtraArgType s -> tactic_genarg_level s <> None
+| _ -> false
+
+
(* [make_gen_entry] builds entries extensible by giving its name (a string) *)
(* For entries extensible only via the ML name, Gram.Entry.create is enough *)
@@ -382,7 +431,6 @@ module Tactic =
let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
- let tactic_main_level = 5
let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
(* Main entry for quotations *)
@@ -391,6 +439,7 @@ module Tactic =
end
+
module Vernac_ =
struct
let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fe6fd083..3998d71b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.mli 7826 2006-01-09 22:00:34Z herbelin $ i*)
+(*i $Id: pcoq.mli 8926 2006-06-08 20:23:17Z herbelin $ i*)
open Util
open Names
@@ -77,10 +77,46 @@ val force_entry_type :
val create_constr_entry :
string * gram_universe -> string -> constr_expr Gram.Entry.e
-val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
val get_generic_entry : string -> grammar_object Gram.Entry.e
val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
+(* Tactics as arguments *)
+
+val tactic_main_level : int
+
+val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val is_tactic_genarg : argument_type -> bool
+
+val tactic_genarg_level : string -> int option
+
(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e
@@ -148,7 +184,6 @@ module Tactic :
val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic_expr : raw_tactic_expr Gram.Entry.e
- val tactic_main_level : int
val tactic : raw_tactic_expr Gram.Entry.e
val tactic_eoi : raw_tactic_expr Gram.Entry.e
end
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a43463c6..d55a6c1e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: ppconstr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
(*i*)
open Util
@@ -117,7 +117,7 @@ let pr_optc pr = function
let pr_universe = Univ.pr_uni
-let pr_sort = function
+let pr_rawsort = function
| RProp Term.Null -> str "Prop"
| RProp Term.Pos -> str "Set"
| RType u -> str "Type" ++ pr_opt pr_universe u
@@ -153,8 +153,8 @@ let pr_lname = function
| lna -> pr_located pr_name lna
let pr_or_var pr = function
- | Genarg.ArgArg x -> pr x
- | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
+ | ArgArg x -> pr x
+ | ArgVar (loc,s) -> pr_lident (loc,s)
let pr_prim_token = function
| Numeral n -> Bigint.pr_bigint n
@@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
let ids = names_of_local_assums bl in
match ro with
CStructRec ->
- if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+ if List.length ids > 1 && n <> None then
+ spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
else mt()
| CWfRec c ->
- spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+ spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
@@ -563,7 +563,7 @@ let rec pr sep inherited a =
| CHole _ -> str "_", latom
| CEvar (_,n) -> str (Evd.string_of_existential n), latom
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
- | CSort (_,s) -> pr_sort s, latom
+ | CSort (_,s) -> pr_rawsort s, latom
| CCast (_,a,_,b) ->
hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
lcast
@@ -619,19 +619,16 @@ let rec strip_context n iscast t =
let pr_constr_expr c = pr lsimple c
let pr_lconstr_expr c = pr ltop c
let pr_pattern_expr c = pr lsimple c
+let pr_lpattern_expr c = pr ltop c
+
let pr_cases_pattern_expr = pr_patt ltop
let pr_binders = pr_undelimited_binders (pr ltop)
-let pr_pattern_occ prc = function
- ([],c) -> prc c
- | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
- hov 0 (prlist_with_sep spc int nl))
-
-let pr_unfold_occ pr_ref = function
- ([],qid) -> pr_ref qid
- | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
- hov 0 (prlist_with_sep spc int nl))
+let pr_with_occurrences pr = function
+ ([],c) -> pr c
+ | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
let pr_red_flag pr r =
(if r.rBeta then pr_arg str "beta" else mt ()) ++
@@ -651,7 +648,7 @@ let pr_metaid id = str"?" ++ pr_id id
let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
| Red false -> str "red"
| Hnf -> str "hnf"
- | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o
+ | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o
| Cbv f ->
if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
str "compute"
@@ -661,11 +658,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
| Unfold l ->
hov 1 (str "unfold" ++ spc() ++
- prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l)
+ prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l)
| Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
| Pattern l ->
hov 1 (str "pattern" ++
- pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
+ pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
| Red true -> error "Shouldn't be accessible from user"
| ExtraRedExpr s -> str s
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 7441f130..8f965d9b 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppconstr.mli 7907 2006-01-21 11:03:29Z herbelin $ i*)
+(*i $Id: ppconstr.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
open Pp
open Environ
@@ -53,17 +53,20 @@ val pr_id : identifier -> std_ppcmds
val pr_name : name -> std_ppcmds
val pr_qualid : qualid -> std_ppcmds
+val pr_with_occurrences :
+ ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
val pr_red_expr :
- ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
+ ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
('a,'b) red_expr_gen -> std_ppcmds
val pr_may_eval :
- ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
('a,'b) may_eval -> std_ppcmds
-val pr_sort : rawsort -> std_ppcmds
+val pr_rawsort : rawsort -> std_ppcmds
val pr_binders : local_binder list -> std_ppcmds
val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
val pr_constr_expr : constr_expr -> std_ppcmds
val pr_lconstr_expr : constr_expr -> std_ppcmds
val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index e6c12f4f..2113ae89 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml 8651 2006-03-21 21:54:43Z jforest $ *)
+(* $Id: pptactic.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
open Pp
open Names
@@ -127,7 +127,7 @@ let rec pr_message_token prid = function
| MsgInt n -> int n
| MsgIdent id -> prid id
-let rec pr_raw_generic prc prlc prtac prref x =
+let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
match Genarg.genarg_tag x with
| BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
| IntArgType -> pr_arg int (out_gen rawwit_int x)
@@ -139,16 +139,14 @@ let rec pr_raw_generic prc prlc prtac prref x =
| IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
| VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
| RefArgType -> pr_arg prref (out_gen rawwit_ref x)
- | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
+ | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prlc prref)
- (out_gen rawwit_constr_may_eval x)
+ pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x)
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
| RedExprArgType ->
pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
- | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
@@ -182,18 +180,18 @@ let rec pr_glob_generic prc prlc prtac x =
| IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
| VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
| RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
- | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
+ | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
| ConstrMayEvalArgType ->
pr_arg (pr_may_eval prc prlc
- (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
+ (pr_or_var (pr_and_short_name pr_evaluable_reference)))
+ (out_gen globwit_constr_may_eval x)
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
| RedExprArgType ->
pr_arg (pr_red_expr
(prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
(out_gen globwit_red_expr x)
- | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
@@ -228,7 +226,7 @@ let rec pr_generic prc prlc prtac x =
| IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
| VarArgType -> pr_arg pr_id (out_gen wit_var x)
| RefArgType -> pr_arg pr_global (out_gen wit_ref x)
- | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
+ | SortArgType -> pr_arg pr_sort (out_gen wit_sort x)
| ConstrArgType -> pr_arg prc (out_gen wit_constr x)
| ConstrMayEvalArgType ->
pr_arg prc (out_gen wit_constr_may_eval x)
@@ -237,7 +235,6 @@ let rec pr_generic prc prlc prtac x =
| RedExprArgType ->
pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference))
(out_gen wit_red_expr x)
- | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
@@ -381,17 +378,14 @@ let pr_by_tactic prt = function
| TacId [] -> mt ()
| tac -> spc() ++ str "by " ++ prt tac
-let pr_occs pp = function
- [] -> pp
- | nl -> hov 1 (pp ++ spc() ++ str"at " ++
- hov 0 (prlist_with_sep spc int nl))
-
let pr_hyp_location pr_id = function
- | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
- | id, occs, InHypTypeOnly ->
- spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
- | id, occs, InHypValueOnly ->
- spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+ | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+ | occs, InHypTypeOnly ->
+ spc () ++
+ pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
+ | occs, InHypValueOnly ->
+ spc () ++
+ pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
@@ -401,11 +395,11 @@ let pr_simple_clause pr_id = function
let pr_clauses pr_id = function
{ onhyps=None; onconcl=true; concl_occs=nl } ->
- pr_in (pr_occs (str " *") nl)
+ pr_in (pr_with_occurrences (fun () -> str " *") (nl,()))
| { onhyps=None; onconcl=false } -> pr_in (str " * |-")
| { onhyps=Some l; onconcl=true; concl_occs=nl } ->
pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
- ++ pr_occs (str" |- *") nl)
+ ++ pr_with_occurrences (fun () -> str" |- *") (nl,()))
| { onhyps=Some l; onconcl=false } ->
pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
@@ -418,6 +412,8 @@ let pr_clause_pattern pr_id = function
++ spc () ++ pr_id id) l ++
pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
+let pr_orient b = if b then mt () else str " <-"
+
let pr_induction_arg prc = function
| ElimOnConstr c -> prc c
| ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
@@ -436,17 +432,27 @@ let pr_match_pattern pr_pat = function
| Subterm (Some id,a) ->
str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-let pr_match_hyps pr_pat = function
- | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+let pr_match_hyps pr_pat (Hyp (nal,mp)) =
+ pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
let pr_match_rule m pr pr_pat = function
| Pat ([],mp,t) when m ->
pr_match_pattern pr_pat mp ++
spc () ++ str "=>" ++ brk (1,4) ++ pr t
+(*
+ | Pat (rl,mp,t) ->
+ hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl ++
+ (if rl <> [] then spc () else mt ()) ++
+ hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+ str "=>" ++ brk (1,4) ++ pr t))
+*)
| Pat (rl,mp,t) ->
- prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
- spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
- str "=>" ++ brk (1,4) ++ pr t
+ hov 0 (
+ hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl) ++
+ (if rl <> [] then spc () else mt ()) ++
+ hov 0 (
+ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+ str "=>" ++ brk (1,4) ++ pr t))
| All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
let pr_funvar = function
@@ -532,38 +538,46 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
open Closure
+(** A printer for tactics that polymorphically works on the three
+ "raw", "glob" and "typed" levels; in practice, the environment is
+ used only at the glob and typed level: it is used to feed the
+ constr printers *)
+
let make_pr_tac
(pr_tac_level,pr_constr,pr_lconstr,pr_pat,
pr_cst,pr_ind,pr_ref,pr_ident,
- pr_extend,strip_prod_binders) =
-
-let pr_bindings env =
- pr_bindings (pr_lconstr env) (pr_constr env) in
-let pr_ex_bindings env =
- pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
-let pr_with_bindings env =
- pr_with_bindings (pr_lconstr env) (pr_constr env) in
-let pr_eliminator env cb =
- str "using" ++ pr_arg (pr_with_bindings env) cb in
-let pr_extend env =
- pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) in
-let pr_red_expr env =
- pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) in
-
-let pr_constrarg env c = spc () ++ pr_constr env c in
-let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
+ pr_extend,strip_prod_binders) env =
+
+(* The environment is not used by the tactic printer: it is passed to the
+ constr and cst printers; hence we can make some abbreviations *)
+let pr_constr = pr_constr env in
+let pr_lconstr = pr_lconstr env in
+let pr_cst = pr_cst env in
+let pr_ind = pr_ind env in
+let pr_tac_level = pr_tac_level env in
+
+(* Other short cuts *)
+let pr_bindings = pr_bindings pr_lconstr pr_constr in
+let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
+let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
+let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level in
+let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst) in
+
+let pr_constrarg c = spc () ++ pr_constr c in
+let pr_lconstrarg c = spc () ++ pr_lconstr c in
let pr_intarg n = spc () ++ int n in
-let pr_binder_fix env (nal,t) =
+(* Some printing combinators *)
+let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
+
+let pr_binder_fix (nal,t) =
(* match t with
| CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
| _ ->*)
- let s =
- prlist_with_sep spc (pr_lname) nal ++ str ":" ++
- pr_lconstr env t in
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr_lconstr t in
spc() ++ hov 1 (str"(" ++ s ++ str")") in
-let pr_fix_tac env (id,n,c) =
+let pr_fix_tac (id,n,c) =
let rec set_nth_name avoid n = function
(nal,ty)::bll ->
if n <= List.length nal then
@@ -589,17 +603,17 @@ let pr_fix_tac env (id,n,c) =
if List.length names = 1 then mt()
else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
hov 1 (str"(" ++ pr_id id ++
- prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++
- pr_lconstrarg env ty ++ str")") in
+ prlist pr_binder_fix bll ++ annot ++ str" :" ++
+ pr_lconstrarg ty ++ str")") in
(* spc() ++
hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
- env c)
+ c)
*)
-let pr_cofix_tac env (id,c) =
- hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
+let pr_cofix_tac (id,c) =
+ hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
(* Printing tactics as arguments *)
-let rec pr_atom0 env = function
+let rec pr_atom0 = function
| TacIntroPattern [] -> str "intros"
| TacIntroMove (None,None) -> str "intro"
| TacAssumption -> str "assumption"
@@ -607,77 +621,78 @@ let rec pr_atom0 env = function
| TacTrivial ([],Some []) -> str "trivial"
| TacAuto (None,[],Some []) -> str "auto"
| TacReflexivity -> str "reflexivity"
- | t -> str "(" ++ pr_atom1 env t ++ str ")"
+ | TacClear (true,[]) -> str "clear"
+ | t -> str "(" ++ pr_atom1 t ++ str ")"
(* Main tactic printer *)
-and pr_atom1 env = function
+and pr_atom1 = function
| TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
| TacSuperAuto _ | TacExtend (_,
("GTauto"|"GIntuition"|"TSimplif"|
"LinearIntuition"),_) ->
errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
| TacExtend (loc,s,l) ->
- pr_with_comments loc (pr_extend env 1 s l)
+ pr_with_comments loc (pr_extend 1 s l)
| TacAlias (loc,s,l,_) ->
- pr_with_comments loc (pr_extend env 1 s (List.map snd l))
+ pr_with_comments loc (pr_extend 1 s (List.map snd l))
(* Basic tactics *)
- | TacIntroPattern [] as t -> pr_atom0 env t
+ | TacIntroPattern [] as t -> pr_atom0 t
| TacIntroPattern (_::_ as p) ->
hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
| TacIntrosUntil h ->
hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
- | TacIntroMove (None,None) as t -> pr_atom0 env t
+ | TacIntroMove (None,None) as t -> pr_atom0 t
| TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
| TacIntroMove (ido1,Some id2) ->
hov 1
(str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
pr_lident id2)
- | TacAssumption as t -> pr_atom0 env t
- | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
- | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c)
- | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
+ | TacAssumption as t -> pr_atom0 t
+ | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
+ | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
+ | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb)
| TacElim (cb,cbo) ->
- hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++
- pr_opt (pr_eliminator env) cbo)
- | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c)
- | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb)
- | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
+ hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++
+ pr_opt pr_eliminator cbo)
+ | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
+ | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings cb)
+ | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
- str"with " ++ prlist_with_sep spc (pr_fix_tac env) l)
+ str"with " ++ prlist_with_sep spc pr_fix_tac l)
| TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
| TacMutualCofix (id,l) ->
hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
- str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
- | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
+ str"with " ++ prlist_with_sep spc pr_cofix_tac l)
+ | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
| TacAssert (Some tac,ipat,c) ->
hov 1 (str "assert" ++
- pr_assumption (pr_lconstr env) (pr_constr env) ipat c ++
- pr_by_tactic (pr_tac_level env ltop) tac)
+ pr_assumption pr_lconstr pr_constr ipat c ++
+ pr_by_tactic (pr_tac_level ltop) tac)
| TacAssert (None,ipat,c) ->
hov 1 (str "pose proof" ++
- pr_assertion (pr_lconstr env) (pr_constr env) ipat c)
+ pr_assertion pr_lconstr pr_constr ipat c)
| TacGeneralize l ->
hov 1 (str "generalize" ++ spc () ++
- prlist_with_sep spc (pr_constr env) l)
+ prlist_with_sep spc pr_constr l)
| TacGeneralizeDep c ->
hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
- pr_constrarg env c)
+ pr_constrarg c)
| TacLetTac (na,c,cl) when cl = nowhere ->
- hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c)
+ hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
| TacLetTac (na,c,cl) ->
- hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++
+ hov 1 (str "set" ++ pr_pose pr_lconstr pr_constr na c ++
pr_clauses pr_ident cl)
(* | TacInstantiate (n,c,ConclLocation ()) ->
hov 1 (str "instantiate" ++ spc() ++
hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg env c ++ str ")" ))
+ pr_lconstrarg c ++ str ")" ))
| TacInstantiate (n,c,HypLocation (id,hloc)) ->
hov 1 (str "instantiate" ++ spc() ++
hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg env c ++ str ")" )
+ pr_lconstrarg c ++ str ")" )
++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
*)
(* Derived basic tactics *)
@@ -685,47 +700,49 @@ and pr_atom1 env = function
hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
| TacNewInduction (h,e,ids) ->
hov 1 (str "induction" ++ spc () ++
- prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
- pr_opt (pr_eliminator env) e)
+ prlist_with_sep spc (pr_induction_arg pr_constr) h ++
+ pr_with_names ids ++
+ pr_opt pr_eliminator e)
| TacSimpleDestruct h ->
hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
| TacNewDestruct (h,e,ids) ->
hov 1 (str "destruct" ++ spc () ++
- prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
+ prlist_with_sep spc (pr_induction_arg pr_constr) h ++
pr_with_names ids ++
- pr_opt (pr_eliminator env) e)
+ pr_opt pr_eliminator e)
| TacDoubleInduction (h1,h2) ->
hov 1
(str "double induction" ++
pr_arg pr_quantified_hypothesis h1 ++
pr_arg pr_quantified_hypothesis h2)
| TacDecomposeAnd c ->
- hov 1 (str "decompose record" ++ pr_constrarg env c)
+ hov 1 (str "decompose record" ++ pr_constrarg c)
| TacDecomposeOr c ->
- hov 1 (str "decompose sum" ++ pr_constrarg env c)
+ hov 1 (str "decompose sum" ++ pr_constrarg c)
| TacDecompose (l,c) ->
hov 1 (str "decompose" ++ spc () ++
- hov 0 (str "[" ++ prlist_with_sep spc (pr_ind env) l
- ++ str "]" ++ pr_constrarg env c))
+ hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
+ ++ str "]" ++ pr_constrarg c))
| TacSpecialize (n,c) ->
hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
- pr_with_bindings env c)
+ pr_with_bindings c)
| TacLApply c ->
- hov 1 (str "lapply" ++ pr_constrarg env c)
+ hov 1 (str "lapply" ++ pr_constrarg c)
(* Automation tactics *)
- | TacTrivial ([],Some []) as x -> pr_atom0 env x
+ | TacTrivial ([],Some []) as x -> pr_atom0 x
| TacTrivial (lems,db) ->
hov 0 (str "trivial" ++
- pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
- | TacAuto (None,[],Some []) as x -> pr_atom0 env x
+ pr_auto_using pr_constr lems ++ pr_hintbases db)
+ | TacAuto (None,[],Some []) as x -> pr_atom0 x
| TacAuto (n,lems,db) ->
hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
- pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
+ pr_auto_using pr_constr lems ++ pr_hintbases db)
| TacDAuto (n,p) ->
hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
(* Context management *)
+ | TacClear (true,[]) as t -> pr_atom0 t
| TacClear (keep,l) ->
hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
prlist_with_sep spc pr_ident l)
@@ -743,77 +760,81 @@ and pr_atom1 env = function
str "into" ++ brk (1,1) ++ pr_ident id2)
(* Constructors *)
- | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l)
- | TacRight l -> hov 1 (str "right" ++ pr_bindings env l)
- | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l)
- | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l)
+ | TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
+ | TacRight l -> hov 1 (str "right" ++ pr_bindings l)
+ | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings l)
+ | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings l)
| TacAnyConstructor (Some t) ->
- hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t)
- | TacAnyConstructor None as t -> pr_atom0 env t
+ hov 1 (str "constructor" ++ pr_arg (pr_tac_level (latom,E)) t)
+ | TacAnyConstructor None as t -> pr_atom0 t
| TacConstructor (n,l) ->
- hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l)
+ hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
(* Conversion *)
| TacReduce (r,h) ->
- hov 1 (pr_red_expr env r ++
+ hov 1 (pr_red_expr r ++
pr_clauses pr_ident h)
| TacChange (occ,c,h) ->
hov 1 (str "change" ++ brk (1,1) ++
(match occ with
None -> mt()
- | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
+ | Some([],c1) -> hov 1 (pr_constr c1 ++ spc() ++ str "with ")
| Some(ocl,c1) ->
- hov 1 (pr_constr env c1 ++ spc() ++
- str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+ hov 1 (pr_constr c1 ++ spc() ++
+ str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++
+ spc() ++
str "with ") ++
- pr_constr env c ++ pr_clauses pr_ident h)
+ pr_constr c ++ pr_clauses pr_ident h)
(* Equivalence relations *)
- | TacReflexivity as x -> pr_atom0 env x
+ | TacReflexivity as x -> pr_atom0 x
| TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
- | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c
+ | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
(* Equality and inversion *)
+ | TacRewrite (b,c,cl) ->
+ hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings c ++
+ pr_clauses pr_ident cl)
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
- pr_with_names ids ++ pr_with_constr (pr_constr env) c)
+ pr_with_names ids ++ pr_with_constr pr_constr c)
| TacInversion (NonDepInversion (k,cl,ids),hyp) ->
hov 1 (pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
pr_with_names ids ++ pr_simple_clause pr_ident cl)
| TacInversion (InversionUsing (c,cl),hyp) ->
hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
- spc () ++ str "using" ++ spc () ++ pr_constr env c ++
+ spc () ++ str "using" ++ spc () ++ pr_constr c ++
pr_simple_clause pr_ident cl)
in
-let rec pr_tac env inherited tac =
+let rec pr_tac inherited tac =
let (strm,prec) = match tac with
| TacAbstract (t,None) ->
- str "abstract " ++ pr_tac env (labstract,L) t, labstract
+ str "abstract " ++ pr_tac (labstract,L) t, labstract
| TacAbstract (t,Some s) ->
hov 0
- (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++
+ (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++
str "using " ++ pr_id s),
labstract
| TacLetRecIn (l,t) ->
hv 0
- (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++
- fnl () ++ pr_tac env (llet,E) t),
+ (str "let rec " ++ pr_rec_clauses (pr_tac ltop) l ++ str " in" ++
+ fnl () ++ pr_tac (llet,E) t),
llet
| TacLetIn (llc,u) ->
v 0
- (hv 0 (pr_let_clauses (pr_tac env ltop) llc
+ (hv 0 (pr_let_clauses (pr_tac ltop) llc
++ str " in") ++
- fnl () ++ pr_tac env (llet,E) u),
+ fnl () ++ pr_tac (llet,E) u),
llet
| TacMatch (lz,t,lrul) ->
- hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with"
+ hov 0 (pr_lazy lz ++ str "match " ++ pr_tac ltop t ++ str " with"
++ prlist
(fun r -> fnl () ++ str "| " ++
- pr_match_rule true (pr_tac env ltop) pr_pat r)
+ pr_match_rule true (pr_tac ltop) pr_pat r)
lrul
++ fnl() ++ str "end"),
lmatch
@@ -822,79 +843,78 @@ let rec pr_tac env inherited tac =
str (if lr then "match reverse goal with" else "match goal with")
++ prlist
(fun r -> fnl () ++ str "| " ++
- pr_match_rule false (pr_tac env ltop) pr_pat r)
+ pr_match_rule false (pr_tac ltop) pr_pat r)
lrul
++ fnl() ++ str "end"),
lmatch
| TacFun (lvar,body) ->
-(* let env = List.fold_right (option_fold_right Idset.add) lvar env in*)
hov 2 (str "fun" ++
prlist pr_funvar lvar ++ str " =>" ++ spc () ++
- pr_tac env (lfun,E) body),
+ pr_tac (lfun,E) body),
lfun
| TacThens (t,tl) ->
- hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++
- pr_seq_body (pr_tac env ltop) tl),
+ hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
+ pr_seq_body (pr_tac ltop) tl),
lseq
| TacThen (t1,t2) ->
- hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++
- pr_tac env (lseq,L) t2),
+ hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+ pr_tac (lseq,L) t2),
lseq
| TacTry t ->
- hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t),
+ hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
| TacDo (n,t) ->
hov 1 (str "do " ++ pr_or_var int n ++ spc () ++
- pr_tac env (ltactical,E) t),
+ pr_tac (ltactical,E) t),
ltactical
| TacRepeat t ->
- hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t),
+ hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
| TacProgress t ->
- hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t),
+ hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
| TacInfo t ->
- hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t),
+ hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
| TacOrelse (t1,t2) ->
- hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
- pr_tac env (lorelse,E) t2),
+ hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+ pr_tac (lorelse,E) t2),
lorelse
| TacFail (n,l) ->
str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
prlist (pr_arg (pr_message_token pr_ident)) l, latom
| TacFirst tl ->
- str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+ str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacSolve tl ->
- str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+ str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
- str "complete" ++ spc () ++ pr_tac env (lcomplete,E) t, lcomplete
+ str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete
| TacId l ->
str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
| TacAtom (loc,TacAlias (_,s,l,_)) ->
pr_with_comments loc
- (pr_extend env (level_of inherited) s (List.map snd l)),
+ (pr_extend (level_of inherited) s (List.map snd l)),
latom
| TacAtom (loc,t) ->
- pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
- | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom
+ pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+ | TacArg(Tacexp e) -> pr_tac_level (latom,E) e, latom
| TacArg(ConstrMayEval (ConstrTerm c)) ->
- str "constr:" ++ pr_constr env c, latom
+ str "constr:" ++ pr_constr c, latom
| TacArg(ConstrMayEval c) ->
- pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+ pr_may_eval pr_constr pr_lconstr pr_cst c, leval
| TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
| TacArg(Integer n) -> int n, latom
| TacArg(TacCall(loc,f,l)) ->
pr_with_comments loc
(hov 1 (pr_ref f ++ spc () ++
- prlist_with_sep spc (pr_tacarg env) l)),
+ prlist_with_sep spc pr_tacarg l)),
lcall
- | TacArg a -> pr_tacarg env a, latom
+ | TacArg a -> pr_tacarg a, latom
in
if prec_less prec inherited then strm
else str"(" ++ strm ++ str")"
-and pr_tacarg env = function
+and pr_tacarg = function
| TacDynamic (loc,t) ->
pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
| MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
@@ -902,13 +922,13 @@ and pr_tacarg env = function
| TacVoid -> str "()"
| Reference r -> pr_ref r
| ConstrMayEval c ->
- pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
+ pr_may_eval pr_constr pr_lconstr pr_cst c
| TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
| TacExternal (_,com,req,la) ->
str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
- spc() ++ prlist_with_sep spc (pr_tacarg env) la
+ spc() ++ prlist_with_sep spc pr_tacarg la
| (TacCall _|Tacexp _|Integer _) as a ->
- str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
+ str "ltac:" ++ pr_tac (latom,E) (TacArg a)
in (pr_tac, pr_match_rule)
@@ -936,7 +956,7 @@ let rec raw_printers =
(pr_raw_tactic_level,
drop_env pr_constr_expr,
drop_env pr_lconstr_expr,
- pr_pattern_expr,
+ pr_lpattern_expr,
drop_env pr_reference,
drop_env pr_reference,
pr_reference,
@@ -945,10 +965,10 @@ let rec raw_printers =
strip_prod_binders_expr)
and pr_raw_tactic_level env n (t:raw_tactic_expr) =
- fst (make_pr_tac raw_printers) env n t
+ fst (make_pr_tac raw_printers env) n t
and pr_raw_match_rule env t =
- snd (make_pr_tac raw_printers) env t
+ snd (make_pr_tac raw_printers env) t
let pr_and_constr_expr pr (c,_) = pr c
@@ -956,7 +976,7 @@ let rec glob_printers =
(pr_glob_tactic_level,
(fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
(fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
- (fun c -> pr_constr_pattern_env (Global.env()) c),
+ (fun c -> pr_lconstr_pattern_env (Global.env()) c),
(fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
(fun env -> pr_or_var (pr_inductive env)),
pr_ltac_or_var (pr_located pr_ltac_constant),
@@ -965,17 +985,16 @@ let rec glob_printers =
strip_prod_binders_rawterm)
and pr_glob_tactic_level env n (t:glob_tactic_expr) =
- fst (make_pr_tac glob_printers) env n t
+ fst (make_pr_tac glob_printers env) n t
and pr_glob_match_rule env t =
- snd (make_pr_tac glob_printers) env t
+ snd (make_pr_tac glob_printers env) t
-let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) =
- make_pr_tac
+let typed_printers =
(pr_glob_tactic_level,
pr_constr_env,
pr_lconstr_env,
- pr_constr_pattern,
+ pr_lconstr_pattern,
pr_evaluable_reference_env,
pr_inductive,
pr_ltac_constant,
@@ -983,6 +1002,8 @@ let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> s
pr_extend,
strip_prod_binders_constr)
+let pr_tactic_level env = fst (make_pr_tac typed_printers env)
+
let pr_raw_tactic env = pr_raw_tactic_level env ltop
let pr_glob_tactic env = pr_glob_tactic_level env ltop
let pr_tactic env = pr_tactic_level env ltop
@@ -996,3 +1017,14 @@ let _ = Tactic_debug.set_match_pattern_printer
let _ = Tactic_debug.set_match_rule_printer
(fun rl ->
pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)
+
+open Pcoq
+
+let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
+
+let _ = for i=0 to 5 do
+ declare_extra_genarg_pprule
+ (rawwit_tactic i, pr_tac_polymorphic i)
+ (globwit_tactic i, pr_tac_polymorphic i)
+ (wit_tactic i, pr_tac_polymorphic i)
+done
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0b6e5771..aea44604 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: ppvernac.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
open Pp
open Names
@@ -277,7 +277,7 @@ let pr_onescheme (id,dep,ind,s) =
hov 0 (pr_lident id ++ str" :=") ++ spc() ++
hov 0 ((if dep then str"Induction for" else str"Minimality for")
++ spc() ++ pr_reference ind) ++ spc() ++
- hov 0 (str"Sort" ++ spc() ++ pr_sort s)
+ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
let begin_of_inductive = function
[] -> 0
@@ -555,18 +555,23 @@ let rec pr_vernac = function
else ([],def,type_) in
let bl = bl @ bl' in
let ids = List.flatten (List.map name_of_binder bl) in
- let name =
- try snd (List.nth ids n)
- with Failure _ ->
- warn (str "non-printable fixpoint \""++pr_id id++str"\"");
- Anonymous in
let annot =
- match (ro : Topconstr.recursion_order_expr) with
- CStructRec ->
- if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_name name ++ str"}"
- else mt()
- | CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+ match n with
+ | None -> mt ()
+ | Some n ->
+ let name =
+ try snd (List.nth ids n)
+ with Failure _ ->
+ warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+ Anonymous in
+ match (ro : Topconstr.recursion_order_expr) with
+ CStructRec ->
+ if List.length ids > 1 then
+ spc() ++ str "{struct " ++ pr_name name ++ str"}"
+ else mt()
+ | CWfRec c ->
+ spc() ++ str "{wf " ++ pr_name name ++ spc() ++
+ pr_lconstr_expr c ++ str"}"
in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -823,6 +828,13 @@ and pr_extend s cl =
try
let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+ let start,rl,cl =
+ match rl with
+ | Egrammar.TacTerm s :: rl -> str s, rl, cl
+ | Egrammar.TacNonTerm _ :: rl ->
+ (* Will put an unnecessary extra space in front *)
+ pr_gen (Global.env()) (List.hd cl), rl, List.tl cl
+ | [] -> anomaly "Empty entry" in
let (pp,_) =
List.fold_left
(fun (strm,args) pi ->
@@ -831,7 +843,7 @@ and pr_extend s cl =
(strm ++ pr_gen (Global.env()) (List.hd args),
List.tl args)
| Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
- (mt(),cl) rl in
+ (start,cl) rl in
hov 1 pp
with Not_found ->
hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index a22f5796..4534369f 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: prettyp.ml 7938 2006-01-28 22:03:33Z herbelin $ *)
+(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
open Pp
open Util
@@ -278,11 +278,11 @@ let print_constructors envpar names types =
hv 0 (str " " ++ pc)
let build_inductive sp tyi =
- let (mib,mip) = Global.lookup_inductive (sp,tyi) in
+ let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in
let params = mib.mind_params_ctxt in
let args = extended_rel_list 0 params in
let env = Global.env() in
- let arity = hnf_prod_applist env mip.mind_user_arity args in
+ let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in
let cstrtypes = arities_of_constructors env (sp,tyi) in
let cstrtypes =
Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -401,7 +401,7 @@ let print_context with_values =
| h::rest when n = None or out_some n > 0 ->
(match print_library_entry with_values h with
| None -> prec n rest
- | Some pp -> prec (option_app ((+) (-1)) n) rest ++ pp ++ fnl ())
+ | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
| _ -> mt ()
in
prec
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 82676b79..8cb5ac42 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 7855 2006-01-12 08:21:57Z herbelin $ *)
+(* $Id: printer.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
open Pp
open Util
@@ -77,11 +77,18 @@ let pr_rawconstr c =
let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
+let pr_lconstr_pattern_env env c =
+ pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c)
let pr_constr_pattern_env env c =
pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+
+let pr_lconstr_pattern t =
+ pr_lconstr_expr (extern_constr_pattern empty_names_context t)
let pr_constr_pattern t =
pr_constr_expr (extern_constr_pattern empty_names_context t)
+let pr_sort s = pr_rawsort (extern_sort s)
+
let _ = Termops.set_print_constr pr_lconstr_env
(**********************************************************************)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 66471d41..9d59bf75 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: printer.mli 7855 2006-01-12 08:21:57Z herbelin $ i*)
+(*i $Id: printer.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
(*i*)
open Pp
@@ -50,11 +50,16 @@ val pr_lrawconstr : rawconstr -> std_ppcmds
val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
val pr_rawconstr : rawconstr -> std_ppcmds
+val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds
+val pr_lconstr_pattern : constr_pattern -> std_ppcmds
+
val pr_constr_pattern_env : env -> constr_pattern -> std_ppcmds
val pr_constr_pattern : constr_pattern -> std_ppcmds
val pr_cases_pattern : cases_pattern -> std_ppcmds
+val pr_sort : sorts -> std_ppcmds
+
(* Printing global references using names as short as possible *)
val pr_global_env : Idset.t -> global_reference -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 35801f73..b5b07091 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_coqast.ml4 8651 2006-03-21 21:54:43Z jforest $ *)
+(* $Id: q_coqast.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
open Util
open Names
@@ -77,20 +77,22 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
let mlexpr_of_loc loc = <:expr< $dloc$ >>
let mlexpr_of_or_var f = function
- | Genarg.ArgArg x -> <:expr< Genarg.ArgArg $f x$ >>
- | Genarg.ArgVar id -> <:expr< Genarg.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+ | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
+ | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
-let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
+let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)
+
+let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
let mlexpr_of_hyp_location = function
- | id, occs, Tacexpr.InHyp ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHyp) >>
- | id, occs, Tacexpr.InHypTypeOnly ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypTypeOnly) >>
- | id, occs, Tacexpr.InHypValueOnly ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypValueOnly) >>
+ | occs, Tacexpr.InHyp ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >>
+ | occs, Tacexpr.InHypTypeOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >>
+ | occs, Tacexpr.InHypValueOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >>
let mlexpr_of_clause cl =
<:expr< {Tacexpr.onhyps=
@@ -140,7 +142,8 @@ let rec mlexpr_of_constr = function
| _ -> failwith "mlexpr_of_constr: TODO"
let mlexpr_of_occ_constr =
- mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr
+ mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
+ mlexpr_of_constr
let mlexpr_of_red_expr = function
| Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
@@ -151,7 +154,7 @@ let mlexpr_of_red_expr = function
| Rawterm.Lazy f ->
<:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
| Rawterm.Unfold l ->
- let f1 = mlexpr_of_list mlexpr_of_int in
+ let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in
let f2 = mlexpr_of_reference in
let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
<:expr< Rawterm.Unfold $f l$ >>
@@ -179,7 +182,6 @@ let rec mlexpr_of_argtype loc = function
| Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
| Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
| Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
- | Genarg.TacticArgType n -> <:expr< Genarg.TacticArgType $mlexpr_of_int n$ >>
| Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
| Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
| Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 48a124a7..3d41e388 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacextend.ml4 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: tacextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
open Genarg
open Q_util
@@ -36,8 +36,6 @@ let rec make_when loc = function
<:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
| _::l -> make_when loc l
-let is_tactic_arg = function TacticArgType _ -> true | _ -> false
-
let rec make_let e = function
| [] -> e
| TacNonTerm(loc,t,_,Some p)::l ->
@@ -47,7 +45,7 @@ let rec make_let e = function
let v =
(* Special case for tactics which must be stored in algebraic
form to avoid marshalling closures and to be reprinted *)
- if is_tactic_arg t then
+ if Pcoq.is_tactic_genarg t then
<:expr< ($v$, Tacinterp.eval_tactic $v$) >>
else v in
<:expr< let $lid:p$ = $v$ in $e$ >>
@@ -84,7 +82,7 @@ let rec make_args = function
let rec make_eval_tactic e = function
| [] -> e
- | TacNonTerm(loc,TacticArgType _,_,Some p)::l ->
+ | TacNonTerm(loc,tag,_,Some p)::l when Pcoq.is_tactic_genarg tag ->
let loc = join_loc loc (MLast.loc_of_expr e) in
let e = make_eval_tactic e l in
(* Special case for tactics which must be stored in algebraic
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 14:20:03 +0000