summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egrammar.ml34
-rw-r--r--parsing/g_ascii_syntax.ml4
-rw-r--r--parsing/g_constr.ml432
-rw-r--r--parsing/g_intsyntax.ml6
-rw-r--r--parsing/g_ltac.ml46
-rw-r--r--parsing/g_minicoq.ml4177
-rw-r--r--parsing/g_prim.ml420
-rw-r--r--parsing/g_tactic.ml4151
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--parsing/g_xml.ml444
-rw-r--r--parsing/g_zsyntax.ml6
-rw-r--r--parsing/lexer.ml462
-rw-r--r--parsing/pcoq.ml428
-rw-r--r--parsing/pcoq.mli6
-rw-r--r--parsing/ppconstr.ml14
-rw-r--r--parsing/ppconstr.mli3
-rw-r--r--parsing/pptactic.ml249
-rw-r--r--parsing/pptactic.mli4
-rw-r--r--parsing/ppvernac.ml13
-rw-r--r--parsing/prettyp.ml20
-rw-r--r--parsing/printer.ml34
-rw-r--r--parsing/printer.mli5
-rw-r--r--parsing/q_coqast.ml455
-rw-r--r--parsing/q_util.ml47
-rw-r--r--parsing/q_util.mli6
-rw-r--r--parsing/search.ml4
-rw-r--r--parsing/tacextend.ml44
-rw-r--r--parsing/tactic_printer.ml84
-rw-r--r--parsing/tactic_printer.mli6
-rw-r--r--parsing/vernacextend.ml44
30 files changed, 497 insertions, 601 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 9416bff2..825d1af0 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml 10987 2008-05-26 12:28:36Z herbelin $ *)
+(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -114,27 +114,33 @@ let make_constr_prod_item univ assoc from forpat = function
let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
grammar_extend entry pos reinit [(name, p4assoc, [])]
-let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) =
+let pure_sublevels level symbs =
+ map_succeed (function
+ | Gramext.Snterml (_,n) when Some (int_of_string n) <> level ->
+ int_of_string n
+ | _ ->
+ failwith "") symbs
+
+let extend_constr (entry,level) (n,assoc) mkact forpat pt =
let univ = get_univ "constr" in
let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
let (symbs,ntl) = List.split pil in
- let needed_levels = register_empty_levels forpat symbs in
+ let pure_sublevels = pure_sublevels level symbs in
+ let needed_levels = register_empty_levels forpat pure_sublevels in
+ let pos,p4assoc,name,reinit = find_position forpat assoc level in
List.iter (prepare_empty_levels entry) needed_levels;
grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
let extend_constr_notation (n,assoc,ntn,rule) =
(* Add the notation in constr *)
let mkact loc env = CNotation (loc,ntn,List.map snd env) in
- let (e,level) = get_constr_entry false (ETConstr (n,())) in
- let pos,p4assoc,name,reinit = find_position false assoc level in
- extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit)
- (make_constr_action mkact) (false,rule);
+ let e = get_constr_entry false (ETConstr (n,())) in
+ extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
(* Add the notation in cases_pattern *)
let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
- let (e,level) = get_constr_entry true (ETConstr (n,())) in
- let pos,p4assoc,name,reinit = find_position true assoc level in
- extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit)
- (make_cases_pattern_action mkact) (true,rule)
+ let e = get_constr_entry true (ETConstr (n,())) in
+ extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
+ true rule
(**********************************************************************)
(** Making generic actions in type generic_argument *)
@@ -228,7 +234,7 @@ let rec interp_entry_name up_level s =
try get_entry (get_univ "prim") s
with _ ->
try get_entry (get_univ "constr") s
- with _ -> error ("Unknown entry "^s)
+ with _ -> error ("Unknown entry "^s^".")
in
let o = object_of_typed_entry e in
let t = type_of_typed_entry e in
@@ -248,7 +254,7 @@ let get_tactic_entry n =
else if 1<=n && n<5 then
weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
else
- error ("Invalid Tactic Notation level: "^(string_of_int n))
+ error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
(* Declaration of the tactic grammar rule *)
@@ -261,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) =
let rules =
if lev = 0 then begin
if not (head_is_ident prods) then
- error "Notation for simple tactic must start with an identifier";
+ error "Notation for simple tactic must start with an identifier.";
let mkact s tac loc l =
(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
make_rule univ (mkact key tac) mkprod prods
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index b262b978..944e2338 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i $Id: g_ascii_syntax.ml 10744 2008-04-03 14:09:56Z herbelin $ i*)
+(*i $Id: g_ascii_syntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Pp
open Util
@@ -53,7 +53,7 @@ let interp_ascii_string dloc s =
then int_of_string s
else
user_err_loc (dloc,"interp_ascii_string",
- str "Expects a single character or a three-digits ascii code") in
+ str "Expects a single character or a three-digits ascii code.") in
interp_ascii dloc p
let uninterp_ascii r =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ba61eb61..b93fdadd 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_constr.ml4 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: g_constr.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pcoq
open Constr
@@ -47,7 +47,7 @@ let rec index_and_rec_order_of_annot loc bl ann =
| lids, (Some (loc, n), ro) ->
if List.exists (fun (_, x) -> x = Name n) lids then
Some (loc, n), ro
- else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable")
+ else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.")
| _, (None, r) -> None, r
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -61,7 +61,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
let _ = Option.map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofixb",
- Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
+ Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
let ty = match tyc with
Some ty -> ty
| None -> CHole (loc, None) in
@@ -326,7 +326,7 @@ GEXTEND Gram
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
| _ -> Util.user_err_loc
(cases_pattern_expr_loc p, "compound_pattern",
- Pp.str "Constructor expected"))
+ Pp.str "Constructor expected."))
| p = pattern; "as"; id = ident ->
CPatAlias (loc, p, id) ]
| "1" LEFTA
@@ -398,7 +398,12 @@ GEXTEND Gram
[LocalRawAssum ([id],Default Implicit,c)]
| "{"; id=name; idl=LIST1 name; "}" ->
List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
- | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc
+ | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
+ | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+ | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
] ]
;
binder:
@@ -407,19 +412,14 @@ GEXTEND Gram
| "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
] ]
;
- typeclass_constraint_binder:
- [ [ tc = typeclass_constraint ->
- let (n,bk,t) = tc in
- LocalRawAssum ([n], TypeClass bk, t)
- ] ]
- ;
-
typeclass_constraint:
[ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
- | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
- (loc, Name iid), expl, c
- | c = operconstr LEVEL "200" ->
- (loc, Anonymous), Implicit, c
+ | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+ id, expl, c
+ | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+ (loc, Name iid), expl, c
+ | c = operconstr LEVEL "200" ->
+ (loc, Anonymous), Implicit, c
] ]
;
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index 6ab8f99c..a589ccf1 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: g_intsyntax.ml 11087 2008-06-10 13:29:52Z letouzey $ i*)
+(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
(* digit-based syntax for int31, bigN bigZ and bigQ *)
@@ -122,7 +122,7 @@ let int31_of_pos_bigint dloc n =
RApp (dloc, ref_construct, List.rev (args 31 n))
let error_negative dloc =
- Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers")
+ Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
let interp_int31 dloc n =
if is_pos_or_zero n then
@@ -212,7 +212,7 @@ let bigN_of_pos_bigint dloc n =
result hght (word_of_pos_bigint dloc hght n)
let bigN_error_negative dloc =
- Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers")
+ Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
let interp_bigN dloc n =
if is_pos_or_zero n then
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 78a9fbc7..dbd81e7f 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_ltac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -72,10 +72,10 @@ GEXTEND Gram
| ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
| "1" RIGHTA
[ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
- TacMatchContext (b,false,mrl)
+ TacMatchGoal (b,false,mrl)
| b = match_key; IDENT "reverse"; IDENT "goal"; "with";
mrl = match_context_list; "end" ->
- TacMatchContext (b,true,mrl)
+ TacMatchGoal (b,true,mrl)
| b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
TacMatch (b,c,mrl)
| IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
deleted file mode 100644
index a9275cf9..00000000
--- a/parsing/g_minicoq.ml4
+++ /dev/null
@@ -1,177 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id: g_minicoq.ml4 10007 2007-07-16 09:18:44Z corbinea $ *)
-
-open Pp
-open Util
-open Names
-open Univ
-open Term
-open Environ
-
-let lexer =
- {Token.func = Lexer.func; Token.using = Lexer.add_token;
- Token.removing = (fun _ -> ()); Token.tparse = Lexer.tparse;
- Token.text = Lexer.token_text}
-;;
-
-type command =
- | Definition of identifier * constr option * constr
- | Parameter of identifier * constr
- | Variable of identifier * constr
- | Inductive of
- (identifier * constr) list *
- (identifier * constr * (identifier * constr) list) list
- | Check of constr
-
-let gram = Grammar.create lexer
-
-let term = Grammar.Entry.create gram "term"
-let name = Grammar.Entry.create gram "name"
-let nametype = Grammar.Entry.create gram "nametype"
-let inductive = Grammar.Entry.create gram "inductive"
-let constructor = Grammar.Entry.create gram "constructor"
-let command = Grammar.Entry.create gram "command"
-
-let path_of_string s = make_path [] (id_of_string s)
-
-EXTEND
- name:
- [ [ id = IDENT -> Name (id_of_string id)
- | "_" -> Anonymous
- ] ];
- nametype:
- [ [ id = IDENT; ":"; t = term -> (id_of_string id, t)
- ] ];
- term:
- [ [ id = IDENT ->
- mkVar (id_of_string id)
- | IDENT "Rel"; n = INT ->
- mkRel (int_of_string n)
- | "Set" ->
- mkSet
- | "Prop" ->
- mkProp
- | "Type" ->
- mkType (new_univ())
- | "Const"; id = IDENT ->
- mkConst (path_of_string id, [||])
- | "Ind"; id = IDENT; n = INT ->
- let n = int_of_string n in
- mkMutInd ((path_of_string id, n), [||])
- | "Construct"; id = IDENT; n = INT; i = INT ->
- let n = int_of_string n and i = int_of_string i in
- mkMutConstruct (((path_of_string id, n), i), [||])
- | "["; na = name; ":"; t = term; "]"; c = term ->
- mkLambda (na,t,c)
- | "("; na = name; ":"; t = term; ")"; c = term ->
- mkProd (na,t,c)
- | c1 = term; "->"; c2 = term ->
- mkArrow c1 c2
- | "("; id = IDENT; cl = LIST1 term; ")" ->
- let c = mkVar (id_of_string id) in
- mkApp (c, Array.of_list cl)
- | "("; cl = LIST1 term; ")" ->
- begin match cl with
- | [c] -> c
- | c::cl -> mkApp (c, Array.of_list cl)
- end
- | "("; c = term; "::"; t = term; ")" ->
- mkCast (c, t)
- | "<"; p = term; ">";
- IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT;
- "of"; bl = LIST0 term; "end" ->
- let ind = (path_of_string id,int_of_string i) in
- let nc = List.length bl in
- let dummy_pats = Array.create nc RegularPat in
- let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in
- mkMutCase (dummy_ci, p, c, Array.of_list bl)
- ] ];
- command:
- [ [ "Definition"; id = IDENT; ":="; c = term; "." ->
- Definition (id_of_string id, None, c)
- | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." ->
- Definition (id_of_string id, Some t, c)
- | "Parameter"; id = IDENT; ":"; t = term; "." ->
- Parameter (id_of_string id, t)
- | "Variable"; id = IDENT; ":"; t = term; "." ->
- Variable (id_of_string id, t)
- | "Inductive"; "["; params = LIST0 nametype SEP ";"; "]";
- inds = LIST1 inductive SEP "with" ->
- Inductive (params, inds)
- | IDENT "Check"; c = term; "." ->
- Check c
- | EOI -> raise End_of_file
- ] ];
- inductive:
- [ [ id = IDENT; ":"; ar = term; ":="; constrs = LIST0 constructor SEP "|" ->
- (id_of_string id,ar,constrs)
- ] ];
- constructor:
- [ [ id = IDENT; ":"; c = term -> (id_of_string id,c) ] ];
-END
-
-(* Pretty-print. *)
-
-let print_univers = ref false
-let print_casts = ref false
-
-let print_type u =
- if !print_univers then (str "Type" ++ pr_uni u)
- else (str "Type")
-
-let print_name = function
- | Anonymous -> (str "_")
- | Name id -> pr_id id
-
-let print_rel bv n = print_name (List.nth bv (pred n))
-
-let rename bv = function
- | Anonymous -> Anonymous
- | Name id as na ->
- let idl =
- List.fold_left
- (fun l n -> match n with Name x -> x::l | _ -> l) [] bv
- in
- if List.mem na bv then Name (next_ident_away id idl) else na
-
-let rec pp bv t =
- match kind_of_term t with
- | Sort (Prop Pos) -> (str "Set")
- | Sort (Prop Null) -> (str "Prop")
- | Sort (Type u) -> print_type u
- | Lambda (na, t, c) ->
- (str"[" ++ print_name na ++ str":" ++ pp bv t ++ str"]" ++ pp (na::bv) c)
- | Prod (Anonymous, t, c) ->
- (pp bv t ++ str"->" ++ pp (Anonymous::bv) c)
- | Prod (na, t, c) ->
- (str"(" ++ print_name na ++ str":" ++ pp bv t ++ str")" ++ pp (na::bv) c)
- | Cast (c, t) ->
- if !print_casts then
- (str"(" ++ pp bv c ++ str"::" ++ pp bv t ++ str")")
- else
- pp bv c
- | App(h, v) ->
- (str"(" ++ pp bv h ++ spc () ++
- prvect_with_sep (fun () -> (spc ())) (pp bv) v ++ str")")
- | Const (sp, _) ->
- (str"Const " ++ pr_id (basename sp))
- | Ind ((sp,i), _) ->
- (str"Ind " ++ pr_id (basename sp) ++ str" " ++ int i)
- | Construct (((sp,i),j), _) ->
- (str"Construct " ++ pr_id (basename sp) ++ str" " ++ int i ++
- str" " ++ int j)
- | Var id -> pr_id id
- | Rel n -> print_rel bv n
- | _ -> (str"<???>")
-
-let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])
-
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index c3792d65..1e738384 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(*i $Id: g_prim.ml4 10155 2007-09-28 22:36:35Z glondu $ i*)
+(*i $Id: g_prim.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Pcoq
open Names
@@ -23,6 +23,16 @@ open Nametab
let local_make_qualid l id = make_qualid (make_dirpath l) id
+let my_int_of_string loc s =
+ try
+ let n = int_of_string s in
+ (* To avoid Array.make errors (that e.g. Undo uses), we set a *)
+ (* more restricted limit than int_of_string does *)
+ if n > 1024 * 2048 then raise Exit;
+ n
+ with Failure _ | Exit ->
+ Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+
GEXTEND Gram
GLOBAL:
bigint natural integer identref name ident var preident
@@ -79,7 +89,7 @@ GEXTEND Gram
;
ne_string:
[ [ s = STRING ->
- if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
+ if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
] ]
;
dirpath:
@@ -90,11 +100,11 @@ GEXTEND Gram
[ [ s = STRING -> s ] ]
;
integer:
- [ [ i = INT -> int_of_string i
- | "-"; i = INT -> - int_of_string i ] ]
+ [ [ i = INT -> my_int_of_string loc i
+ | "-"; i = INT -> - my_int_of_string loc i ] ]
;
natural:
- [ [ i = INT -> int_of_string i ] ]
+ [ [ i = INT -> my_int_of_string loc i ] ]
;
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> (Bigint.of_string i) ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c0a4ba5b..49f00d40 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_tactic.ml4 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: g_tactic.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Pcoq
@@ -26,7 +26,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
-let lpar_id_coloneq =
+let test_lpar_id_coloneq =
Gram.Entry.of_parser "lpar_id_coloneq"
(fun strm ->
match Stream.npeek 1 strm with
@@ -34,9 +34,7 @@ let lpar_id_coloneq =
(match Stream.npeek 2 strm with
| [_; ("IDENT",s)] ->
(match Stream.npeek 3 strm with
- | [_; _; ("", ":=")] ->
- Stream.junk strm; Stream.junk strm; Stream.junk strm;
- Names.id_of_string s
+ | [_; _; ("", ":=")] -> ()
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
@@ -56,7 +54,7 @@ let test_lpar_idnum_coloneq =
| _ -> raise Stream.Failure)
(* idem for (x:t) *)
-let lpar_id_colon =
+let test_lpar_id_colon =
Gram.Entry.of_parser "lpar_id_colon"
(fun strm ->
match Stream.npeek 1 strm with
@@ -64,9 +62,7 @@ let lpar_id_colon =
(match Stream.npeek 2 strm with
| [_; ("IDENT",id)] ->
(match Stream.npeek 3 strm with
- | [_; _; ("", ":")] ->
- Stream.junk strm; Stream.junk strm; Stream.junk strm;
- Names.id_of_string id
+ | [_; _; ("", ":")] -> ()
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
@@ -131,15 +127,15 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
| _, Some x ->
let ids = List.map snd (List.flatten (List.map pi1 bl)) in
(try list_index (snd x) ids
- with Not_found -> error "no such fix variable")
- | _ -> error "cannot guess decreasing argument of fix" in
+ with Not_found -> error "No such fix variable.")
+ | _ -> error "Cannot guess decreasing argument of fix." in
(id,n,CProdN(loc,bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
let _ = Option.map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofix_tac",
- Pp.str"Annotation forbidden in cofix expression")) ann in
+ Pp.str"Annotation forbidden in cofix expression.")) ann in
(id,CProdN(loc,bl,ty))
(* Functions overloaded by quotifier *)
@@ -162,6 +158,8 @@ let mkCLambdaN_simple bl c =
let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in
mkCLambdaN_simple_loc loc bl c
+let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
+
let map_int_or_var f = function
| Rawterm.ArgArg x -> Rawterm.ArgArg (f x)
| Rawterm.ArgVar _ as y -> y
@@ -237,27 +235,32 @@ GEXTEND Gram
intropatterns:
[ [ l = LIST0 simple_intropattern -> l ]]
;
- simple_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
- | "()" -> IntroOrAndPattern [[]]
- | "("; si = simple_intropattern; ")" -> IntroOrAndPattern [[si]]
+ disjunctive_intropattern:
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc
+ | "()" -> loc,IntroOrAndPattern [[]]
+ | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]]
| "("; si = simple_intropattern; ",";
tc = LIST1 simple_intropattern SEP "," ; ")" ->
- IntroOrAndPattern [si::tc]
+ loc,IntroOrAndPattern [si::tc]
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
| ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
- | t::q -> IntroOrAndPattern [[t;pairify q]]
- in pairify (si::tc)
- | "_" -> IntroWildcard
- | prefix = pattern_ident -> IntroFresh prefix
- | "?" -> IntroAnonymous
- | id = ident -> IntroIdentifier id
- | "->" -> IntroRewrite true
- | "<-" -> IntroRewrite false
- ] ]
+ | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
+ in loc,pairify (si::tc) ] ]
+ ;
+ naming_intropattern:
+ [ [ prefix = pattern_ident -> loc, IntroFresh prefix
+ | "?" -> loc, IntroAnonymous
+ | id = ident -> loc, IntroIdentifier id ] ]
+ ;
+ simple_intropattern:
+ [ [ pat = disjunctive_intropattern -> pat
+ | pat = naming_intropattern -> pat
+ | "_" -> loc, IntroWildcard
+ | "->" -> loc, IntroRewrite true
+ | "<-" -> loc, IntroRewrite false ] ]
;
simple_binding:
[ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
@@ -402,7 +405,18 @@ GEXTEND Gram
[ [ "using"; el = constr_with_bindings -> el ] ]
;
with_names:
- [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
+ [ [ "as"; ipat = simple_intropattern -> ipat
+ | -> dummy_loc,IntroAnonymous ] ]
+ ;
+ with_inversion_names:
+ [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
+ | -> None ] ]
+ ;
+ with_induction_names:
+ [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern
+ -> (eq,Some ipat)
+ | "as"; eq = naming_intropattern -> (Some eq,None)
+ | -> (None,None) ] ]
;
as_name:
[ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
@@ -439,30 +453,40 @@ GEXTEND Gram
oriented_rewriter :
[ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
;
+ induction_clause:
+ [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
+ el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ]
+ ;
+ move_location:
+ [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
+ | IDENT "before"; id = id_or_meta -> MoveBefore id
+ | "at"; IDENT "bottom" -> MoveToEnd true
+ | "at"; IDENT "top" -> MoveToEnd false ] ]
+ ;
simple_tactic:
[ [
(* Basic tactics *)
IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
TacIntrosUntil id
| IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
- | IDENT "intro"; id = ident; IDENT "after"; id2 = identref ->
- TacIntroMove (Some id, Some id2)
- | IDENT "intro"; IDENT "after"; id2 = identref ->
- TacIntroMove (None, Some id2)
- | IDENT "intro"; id = ident -> TacIntroMove (Some id, None)
- | IDENT "intro" -> TacIntroMove (None, None)
+ | IDENT "intro"; id = ident; hto = move_location ->
+ TacIntroMove (Some id, hto)
+ | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
+ | IDENT "intro"; id = ident -> TacIntroMove (Some id, no_move)
+ | IDENT "intro" -> TacIntroMove (None, no_move)
| IDENT "assumption" -> TacAssumption
| IDENT "exact"; c = constr -> TacExact c
| IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
| IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
- | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl)
- | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl)
- | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings ->
- TacApply (false,false,cl)
- | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings ->
- TacApply (false, true,cl)
+ | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," ->
+ TacApply (true,false,cl)
+ | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," ->
+ TacApply (true,true,cl)
+ | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","
+ -> TacApply (false,false,cl)
+ | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> TacApply (false,true,cl)
| IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
TacElim (false,cl,el)
| IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
@@ -492,10 +516,12 @@ GEXTEND Gram
TacLetTac (na,c,p,false)
(* Begin compatibility *)
- | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" ->
- TacAssert (None,IntroIdentifier id,c)
- | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic ->
- TacAssert (Some tac,IntroIdentifier id,c)
+ | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ c = lconstr; ")" ->
+ TacAssert (None,(loc,IntroIdentifier id),c)
+ | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
+ TacAssert (Some tac,(loc,IntroIdentifier id),c)
(* End compatibility *)
| IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
@@ -521,23 +547,19 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
- TacSimpleInduction h
- | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names;
- el = OPT eliminator; cl = opt_clause ->
- TacNewInduction (false,lc,el,ids,cl)
- | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names;
- el = OPT eliminator; cl = opt_clause ->
- TacNewInduction (true,lc,el,ids,cl)
+ TacSimpleInductionDestruct (true,h)
+ | IDENT "induction"; ic = induction_clause ->
+ TacInductionDestruct (true,false,[ic])
+ | IDENT "einduction"; ic = induction_clause ->
+ TacInductionDestruct(true,true,[ic])
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
| IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
- TacSimpleDestruct h
- | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names;
- el = OPT eliminator; cl = opt_clause ->
- TacNewDestruct (false,lc,el,ids,cl)
- | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names;
- el = OPT eliminator; cl = opt_clause ->
- TacNewDestruct (true,lc,el,ids,cl)
+ TacSimpleInductionDestruct (false,h)
+ | IDENT "destruct"; ic = induction_clause ->
+ TacInductionDestruct(false,false,[ic])
+ | IDENT "edestruct"; ic = induction_clause ->
+ TacInductionDestruct(false,true,[ic])
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
| IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
| IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
@@ -565,8 +587,8 @@ GEXTEND Gram
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
| IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
| IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
- | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta ->
- TacMove (true,id1,id2)
+ | IDENT "move"; dep = [IDENT "dependent" -> true | -> false];
+ hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto)
| IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
| IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
@@ -601,16 +623,19 @@ GEXTEND Gram
| IDENT "inversion" -> FullInversion
| IDENT "inversion_clear" -> FullInversionClear ];
hyp = quantified_hypothesis;
- ids = with_names; co = OPT ["with"; c = constr -> c] ->
+ ids = with_inversion_names; co = OPT ["with"; c = constr -> c] ->
TacInversion (DepInversion (k,co,ids),hyp)
| IDENT "simple"; IDENT "inversion";
- hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ hyp = quantified_hypothesis; ids = with_inversion_names;
+ cl = simple_clause ->
TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
| IDENT "inversion";
- hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ hyp = quantified_hypothesis; ids = with_inversion_names;
+ cl = simple_clause ->
TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
| IDENT "inversion_clear";
- hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ hyp = quantified_hypothesis; ids = with_inversion_names;
+ cl = simple_clause ->
TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
| IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = simple_clause ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 00469ad5..87c11164 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_vernac.ml4 11083 2008-06-09 22:08:14Z herbelin $ *)
+(* $Id: g_vernac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
@@ -113,7 +113,7 @@ let test_plurial_form = function
let no_coercion loc (c,x) =
if c then Util.user_err_loc
- (loc,"no_coercion",Pp.str"no coercion allowed here");
+ (loc,"no_coercion",str"No coercion allowed here.");
x
(* Gallina declarations *)
@@ -271,7 +271,7 @@ GEXTEND Gram
Some (loc, id)
else Util.user_err_loc
(loc,"Fixpoint",
- Pp.str "No argument named " ++ Nameops.pr_id id))
+ str "No argument named " ++ Nameops.pr_id id ++ str"."))
| None ->
(* If there is only one argument, it is the recursive one,
otherwise, we search the recursive index later *)
@@ -311,7 +311,7 @@ GEXTEND Gram
LocalRawAssum(l,ty) -> (l,ty)
| LocalRawDef _ ->
Util.user_err_loc
- (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ]
+ (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ]
;
*)
(* ... with coercions *)
@@ -491,7 +491,7 @@ GEXTEND Gram
props = typeclass_field_types ->
VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
- | IDENT "Context"; c = typeclass_context ->
+ | IDENT "Context"; c = binders_let ->
VernacContext c
| global = [ IDENT "Global" -> true | -> false ];
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 5b2d8668..72d5d275 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_xml.ml4 10727 2008-03-28 20:22:43Z msozeau $ *)
+(* $Id: g_xml.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -31,7 +31,7 @@ type xml = XmlTag of loc * string * attribute list * xml list
let check_tags loc otag ctag =
if otag <> ctag then
user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
- str "does not match open xml tag " ++ str otag)
+ str "does not match open xml tag " ++ str otag ++ str ".")
let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e)
@@ -55,11 +55,19 @@ GEXTEND Gram
;
END
+(* Errors *)
+
+let error_expect_one_argument loc =
+ user_err_loc (loc,"",str "wrong number of arguments (expect one).")
+
+let error_expect_no_argument loc =
+ user_err_loc (loc,"",str "wrong number of arguments (expect none).")
+
(* Interpreting attributes *)
let nmtoken (loc,a) =
try int_of_string a
- with Failure _ -> user_err_loc (loc,"",str "nmtoken expected")
+ with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
let interp_xml_attr_qualid = function
| "uri", s -> qualid_of_string s
@@ -94,7 +102,7 @@ let sort_of_cdata (loc,a) = match a with
| "Prop" -> RProp Null
| "Set" -> RProp Pos
| "Type" -> RType None
- | _ -> user_err_loc (loc,"",str "sort expected")
+ | _ -> user_err_loc (loc,"",str "sort expected.")
let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
@@ -188,18 +196,18 @@ let rec interp_xml_constr = function
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)
+ | XmlTag (loc,s,_,_) ->
+ user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
and interp_xml_tag s = function
| XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl)
| XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
- str "Expect tag " ++ str s ++ str " but find " ++ str s)
+ str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
and interp_xml_constr_alias s x =
match interp_xml_tag s x with
| (_,_,[x]) -> interp_xml_constr x
- | (loc,_,_) ->
- user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+ | (loc,_,_) -> error_expect_one_argument loc
and interp_xml_term x = interp_xml_constr_alias "term" x
and interp_xml_type x = interp_xml_constr_alias "type" x
@@ -215,8 +223,7 @@ and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
and interp_xml_decl_alias s x =
match interp_xml_tag s x with
| (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
- | (loc,_,_) ->
- user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+ | (loc,_,_) -> error_expect_one_argument loc
and interp_xml_def x = interp_xml_decl_alias "def" x
and interp_xml_decl x = interp_xml_decl_alias "decl" x
@@ -227,17 +234,17 @@ and interp_xml_recursionOrder x =
match s with
"Structural" ->
(match l with [] -> RStructRec
- | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)"))
+ | _ -> error_expect_no_argument loc)
| "WellFounded" ->
(match l with
[c] -> RWfRec (interp_xml_type c)
- | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+ | _ -> error_expect_one_argument loc)
| "Measure" ->
(match l with
[c] -> RMeasureRec (interp_xml_type c)
- | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+ | _ -> error_expect_one_argument loc)
| _ ->
- user_err_loc (locs,"",str "invalid recursion order")
+ user_err_loc (locs,"",str "Invalid recursion order.")
and interp_xml_FixFunction x =
match interp_xml_tag "FixFunction" x with
@@ -248,15 +255,15 @@ and interp_xml_FixFunction x =
| (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)")
+ | (loc,_,_) ->
+ error_expect_one_argument loc
and interp_xml_CoFixFunction x =
match interp_xml_tag "CoFixFunction" x with
| (loc,al,[x1;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)")
+ error_expect_one_argument loc
(* Interpreting tactic argument *)
@@ -266,7 +273,8 @@ let rec interp_xml_tactic_arg = function
| XmlTag (loc,"CALL",al,xl) ->
let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
- | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
+ | XmlTag (loc,s,_,_) ->
+ user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
let parse_tactic_arg ch =
interp_xml_tactic_arg
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index aab266c0..8b9c0d22 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_zsyntax.ml 10806 2008-04-16 23:51:06Z letouzey $ *)
+(* $Id: g_zsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pcoq
open Pp
@@ -57,7 +57,7 @@ let pos_of_bignat dloc x =
let error_non_positive dloc =
user_err_loc (dloc, "interp_positive",
- str "Only strictly positive numbers in type \"positive\"")
+ str "Only strictly positive numbers in type \"positive\".")
let interp_positive dloc n =
if is_strictly_pos n then pos_of_bignat dloc n
@@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n =
RRef (dloc, glob_N0)
let error_negative dloc =
- user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"")
+ user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
let n_of_int dloc n =
if is_pos_or_zero n then n_of_binnat dloc true n
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c1e4cfc6..1b0c24da 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 11059 2008-06-06 09:29:20Z herbelin $ i*)
+(*i $Id: lexer.ml4 11238 2008-07-19 09:34:03Z herbelin $ i*)
(*i camlp4use: "pr_o.cmo" i*)
@@ -324,43 +324,49 @@ let rec comment bp = parser bp2
(* Parse a special token, using the [token_tree] *)
(* 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 =
+(* and retain the longest valid special token obtained *)
+let rec progress_further last nj tt cs =
+ try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
+ with Failure _ -> last
+
+and update_longest_valid_token last nj tt cs =
+ match tt.node with
+ | Some _ as last' ->
+ for i=1 to nj do Stream.junk cs done;
+ progress_further last' 0 tt cs
+ | None ->
+ progress_further last nj tt cs
+
+(* nr is the number of char peeked since last valid token *)
+(* n the number of char in utf8 block *)
+and progress_utf8 last nj 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
+ if n=1 then
+ update_longest_valid_token last (nj+n) tt cs
+ else
+ match Util.list_skipn (nj+1) (Stream.npeek (nj+n) cs) with
+ | l when List.length l = n-1 ->
+ List.iter (check_utf8_trailing_byte cs) l;
+ let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
+ update_longest_valid_token last (nj+n) tt cs
+ | _ ->
+ error_utf8 cs
with Not_found ->
- tt.node
+ last
-and progress_from_byte nr tt cs = function
+and progress_from_byte last nj 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
+ | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
+ | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
+ | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
+ | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
| _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
error_utf8 cs
(* Must be a special token *)
let process_chars bp c cs =
- let t = progress_from_byte 1 !token_tree cs c in
+ let t = progress_from_byte None (-1) !token_tree cs c in
let ep = Stream.count cs in
match t with
| Some t -> (("", t), (bp, ep))
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 70a41ddc..2e55b656 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
-(*i $Id: pcoq.ml4 10987 2008-05-26 12:28:36Z herbelin $ i*)
+(*i $Id: pcoq.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Pp
open Util
@@ -247,7 +247,7 @@ let get_entry (u, utab) s =
Hashtbl.find utab s
with Not_found ->
errorlabstrm "Pcoq.get_entry"
- (str "unknown grammar entry " ++ str u ++ str ":" ++ str s)
+ (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".")
let new_entry etyp (u, utab) s =
let ename = u ^ ":" ^ s in
@@ -307,12 +307,12 @@ let get_generic_entry s =
try
object_of_typed_entry (Hashtbl.find utab s)
with Not_found ->
- error ("unknown grammar entry "^u^":"^s)
+ error ("Unknown grammar entry "^u^":"^s^".")
let get_generic_entry_type (u,utab) s =
try type_of_typed_entry (Hashtbl.find utab s)
with Not_found ->
- error ("unknown grammar entry "^u^":"^s)
+ error ("Unknown grammar entry "^u^":"^s^".")
let force_entry_type (u, utab) s etyp =
try
@@ -578,7 +578,7 @@ let error_level_assoc p current expected =
errorlabstrm ""
(str "Level " ++ int p ++ str " is already declared " ++
pr_assoc current ++ str " associative while it is now expected to be " ++
- pr_assoc expected ++ str " associative")
+ pr_assoc expected ++ str " associative.")
let find_position_gen forpat ensure assoc lev =
let ccurrent,pcurrent as current = List.hd !level_stack in
@@ -628,13 +628,13 @@ let rec list_mem_assoc_triple x = function
| [] -> false
| (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
-let register_empty_levels forpat symbs =
- map_succeed (function
- | Gramext.Snterml (_,n) when
- let levels = (if forpat then snd else fst) (List.hd !level_stack) in
- not (list_mem_assoc_triple (int_of_string n) levels) ->
- find_position_gen forpat true None (Some (int_of_string n))
- | _ -> failwith "") symbs
+let register_empty_levels forpat levels =
+ map_succeed (fun n ->
+ let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+ if not (list_mem_assoc_triple n levels) then
+ find_position_gen forpat true None (Some n)
+ else
+ failwith "") levels
let find_position forpat assoc level =
find_position_gen forpat false assoc level
@@ -695,7 +695,7 @@ let compute_entry allow_create adjust forpat = function
| ETPattern -> weaken_entry Constr.pattern, None, false
| ETOther ("constr","annot") ->
weaken_entry Constr.annot, None, false
- | ETConstrList _ -> error "List of entries cannot be registered"
+ | ETConstrList _ -> error "List of entries cannot be registered."
| ETOther (u,n) ->
let u = get_univ u in
let e =
@@ -762,6 +762,6 @@ let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
user_err_loc (loc, "coerce_reference_to_id",
- str "This expression should be a simple identifier")
+ str "This expression should be a simple identifier.")
let coerce_global_to_id = coerce_reference_to_id
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 44a3686e..525727ce 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 10987 2008-05-26 12:28:36Z herbelin $ i*)
+(*i $Id: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Util
open Names
@@ -188,7 +188,7 @@ module Tactic :
val int_or_var : int or_var Gram.Entry.e
val red_expr : raw_red_expr Gram.Entry.e
val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
- val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
+ val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic_expr : raw_tactic_expr Gram.Entry.e
val binder_tactic : raw_tactic_expr Gram.Entry.e
@@ -229,7 +229,7 @@ val find_position :
val synchronize_level_positions : unit -> unit
-val register_empty_levels : bool -> Compat.token Gramext.g_symbol list ->
+val register_empty_levels : bool -> int list ->
(Gramext.position option * Gramext.g_assoc option *
string option * Gramext.g_assoc option) list
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 985396f5..5f6ffe87 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: ppconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
(*i*)
open Util
@@ -96,12 +96,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
let pr_delimiters key strm =
strm ++ str ("%"^key)
-let pr_located pr (loc,x) =
- if Flags.do_translate() && loc<>dummy_loc then
- let (b,e) = unloc loc in
- comment b ++ pr x ++ comment e
- else pr x
-
let pr_com_at n =
if Flags.do_translate() && n <> 0 then comment n
else mt()
@@ -219,13 +213,13 @@ let surround_binder k p =
match k with
Default Explicit -> hov 1 (str"(" ++ p ++ str")")
| Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
- | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+ | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
let surround_implicit k p =
match k with
Default Explicit -> p
| Default Implicit -> (str"{" ++ p ++ str"}")
- | TypeClass b -> (str"[" ++ p ++ str"]")
+ | TypeClass _ -> (str"[" ++ p ++ str"]")
let pr_binder many pr (nal,k,t) =
match t with
@@ -719,7 +713,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
hov 1 (str "pattern" ++
pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
- | Red true -> error "Shouldn't be accessible from user"
+ | Red true -> error "Shouldn't be accessible from user."
| ExtraRedExpr s -> str s
| CbvVm -> str "vm_compute"
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index a0eb4ad9..8047e968 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 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: ppconstr.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Pp
open Environ
@@ -35,7 +35,6 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
val pr_tight_coma : unit -> std_ppcmds
-val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
val pr_metaid : identifier -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f955d83b..6a7ae9bc 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: pptactic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Names
@@ -58,7 +58,7 @@ let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
let s = match unquote wit with
| ExtraArgType s -> s
| _ -> error
- "Can declare a pretty-printing rule only for extra argument types"
+ "Can declare a pretty-printing rule only for extra argument types."
in
let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
@@ -142,41 +142,40 @@ let out_bindings = function
let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel 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)
- | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x)
- | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
- | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
- | IntroPatternArgType -> pr_arg pr_intro_pattern
- (out_gen rawwit_intro_pattern 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_rawsort (out_gen rawwit_sort x)
- | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
+ | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
+ | IntArgType -> int (out_gen rawwit_int x)
+ | IntOrVarArgType -> pr_or_var pr_int (out_gen rawwit_int_or_var x)
+ | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
+ | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
+ | IdentArgType -> pr_id (out_gen rawwit_ident x)
+ | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
+ | RefArgType -> prref (out_gen rawwit_ref x)
+ | SortArgType -> pr_rawsort (out_gen rawwit_sort x)
+ | ConstrArgType -> prc (out_gen rawwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prlc (pr_or_by_notation prref))
+ pr_may_eval prc prlc (pr_or_by_notation prref)
(out_gen rawwit_constr_may_eval x)
- | QuantHypArgType ->
- pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
+ | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr (prc,prlc,pr_or_by_notation prref))
+ pr_red_expr (prc,prlc,pr_or_by_notation prref)
(out_gen rawwit_red_expr x)
- | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
+ | OpenConstrArgType b -> 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)
+ pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x)
| BindingsArgType ->
- pr_arg (pr_bindings_no_with prc prlc) (out_gen rawwit_bindings x)
+ pr_bindings_no_with prc prlc (out_gen rawwit_bindings x)
| List0ArgType _ ->
- hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
+ hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+ (fold_list0 (fun a l -> a::l) x []))
| List1ArgType _ ->
- hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
+ hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+ (fold_list1 (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prref) (mt()) x)
| PairArgType _ ->
hov 0
(fold_pair
- (fun a b -> pr_raw_generic prc prlc prtac prref a ++ spc () ++
- pr_raw_generic prc prlc prtac prref b)
+ (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prref) [a;b])
x)
| ExtraArgType s ->
try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
@@ -185,107 +184,105 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
let rec pr_glob_generic prc prlc prtac x =
match Genarg.genarg_tag x with
- | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false")
- | IntArgType -> pr_arg int (out_gen globwit_int x)
- | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x)
- | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\""
- | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
- | IntroPatternArgType ->
- pr_arg pr_intro_pattern (out_gen globwit_intro_pattern 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_rawsort (out_gen globwit_sort x)
- | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
+ | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
+ | IntArgType -> int (out_gen globwit_int x)
+ | IntOrVarArgType -> pr_or_var pr_int (out_gen globwit_int_or_var x)
+ | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
+ | PreIdentArgType -> str (out_gen globwit_pre_ident x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
+ | IdentArgType -> pr_id (out_gen globwit_ident x)
+ | VarArgType -> pr_located pr_id (out_gen globwit_var x)
+ | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
+ | SortArgType -> pr_rawsort (out_gen globwit_sort x)
+ | ConstrArgType -> prc (out_gen globwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prlc
- (pr_or_var (pr_and_short_name pr_evaluable_reference)))
+ pr_may_eval prc prlc
+ (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)
+ 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)))
+ pr_red_expr
+ (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference))
(out_gen globwit_red_expr x)
- | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
+ | OpenConstrArgType b -> 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)
+ pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x)
| BindingsArgType ->
- pr_arg (pr_bindings_no_with prc prlc) (out_gen globwit_bindings x)
+ pr_bindings_no_with prc prlc (out_gen globwit_bindings x)
| List0ArgType _ ->
- hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
+ hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+ (fold_list0 (fun a l -> a::l) x []))
| List1ArgType _ ->
- hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
+ hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+ (fold_list1 (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac) (mt()) x)
| PairArgType _ ->
hov 0
(fold_pair
- (fun a b -> pr_glob_generic prc prlc prtac a ++ spc () ++
- pr_glob_generic prc prlc prtac b)
+ (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac) [a;b])
x)
| ExtraArgType s ->
try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str " [no printer for " ++ str s ++ str "] "
+ with Not_found -> str "[no printer for " ++ str s ++ str "] "
open Closure
let rec pr_generic prc prlc prtac x =
match Genarg.genarg_tag x with
- | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false")
- | IntArgType -> pr_arg int (out_gen wit_int x)
- | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x)
- | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\""
- | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
- | IntroPatternArgType ->
- pr_arg pr_intro_pattern (out_gen wit_intro_pattern 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 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)
- | QuantHypArgType ->
- pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
+ | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
+ | IntArgType -> int (out_gen wit_int x)
+ | IntOrVarArgType -> pr_or_var pr_int (out_gen wit_int_or_var x)
+ | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
+ | PreIdentArgType -> str (out_gen wit_pre_ident x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
+ | IdentArgType -> pr_id (out_gen wit_ident x)
+ | VarArgType -> pr_id (out_gen wit_var x)
+ | RefArgType -> pr_global (out_gen wit_ref x)
+ | SortArgType -> pr_sort (out_gen wit_sort x)
+ | ConstrArgType -> prc (out_gen wit_constr x)
+ | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x)
+ | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference))
- (out_gen wit_red_expr x)
- | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
+ pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x)
+ | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
let (c,b) = out_gen wit_constr_with_bindings x in
- pr_arg (pr_with_bindings prc prlc) (c,out_bindings b)
+ pr_with_bindings prc prlc (c,out_bindings b)
| BindingsArgType ->
- pr_arg (pr_bindings_no_with prc prlc)
- (out_bindings (out_gen wit_bindings x))
- | List0ArgType _ ->
- hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
+ pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x))
+ | List0ArgType _ ->
+ hov 0 (pr_sequence (pr_generic prc prlc prtac)
+ (fold_list0 (fun a l -> a::l) x []))
| List1ArgType _ ->
- hov 0 (fold_list1 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
+ hov 0 (pr_sequence (pr_generic prc prlc prtac)
+ (fold_list1 (fun a l -> a::l) x []))
| OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac) (mt()) x)
| PairArgType _ ->
hov 0
- (fold_pair
- (fun a b -> pr_generic prc prlc prtac a ++ spc () ++
- pr_generic prc prlc prtac b)
+ (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac) [a;b])
x)
| ExtraArgType s ->
try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> str " [no printer for " ++ str s ++ str "]"
+ with Not_found -> str "[no printer for " ++ str s ++ str "]"
-let rec pr_tacarg_using_rule pr_gen = function
- | Some s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
- | None :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al)
- | [], [] -> mt ()
+let rec tacarg_using_rule_token pr_gen = function
+ | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
+ | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al)
+ | [], [] -> []
| _ -> failwith "Inconsistent arguments of extended tactic"
-let pr_extend_gen prgen lev s l =
+let pr_tacarg_using_rule pr_gen l=
+ pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l)
+
+let pr_extend_gen pr_gen lev s l =
try
let tags = List.map genarg_tag l in
let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
- let p = pr_tacarg_using_rule prgen (pl,l) in
+ let p = pr_tacarg_using_rule pr_gen (pl,l) in
if lev' > lev then surround p else p
with Not_found ->
- str s ++ prlist prgen l ++ str " (* Generic printer *)"
+ str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
let pr_raw_extend prc prlc prtac =
pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
@@ -366,9 +363,22 @@ let pr_with_constr prc = function
| None -> mt ()
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+let pr_with_induction_names = function
+ | None, None -> mt ()
+ | eqpat, ipat ->
+ spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++
+ pr_opt pr_intro_pattern ipat)
+
+let pr_as_intro_pattern ipat =
+ spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+let pr_with_inversion_names = function
+ | None -> mt ()
+ | Some ipat -> pr_as_intro_pattern ipat
+
let pr_with_names = function
- | IntroAnonymous -> mt ()
- | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+ | _,IntroAnonymous -> mt ()
+ | ipat -> pr_as_intro_pattern ipat
let pr_as_name = function
| Anonymous -> mt ()
@@ -454,7 +464,7 @@ let pr_induction_kind = function
| FullInversion -> str "inversion"
| FullInversionClear -> str "inversion_clear"
-let pr_lazy lz = if lz then str "lazy " else mt ()
+let pr_lazy lz = if lz then str "lazy" else mt ()
let pr_match_pattern pr_pat = function
| Term a -> pr_pat a
@@ -489,8 +499,9 @@ let pr_funvar = function
| None -> spc () ++ str "_"
| Some id -> spc () ++ pr_id id
-let pr_let_clause k pr (id,t) =
- hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t))
+let pr_let_clause k pr (id,(bl,t)) =
+ hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
+ str " :=" ++ brk (1,1) ++ pr (TacArg t))
let pr_let_clauses recflag pr = function
| hd::tl ->
@@ -599,6 +610,10 @@ let pr_intarg n = spc () ++ int n in
(* Some printing combinators *)
let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
+let extract_binders = function
+ | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+ | body -> ([],body) in
+
let pr_binder_fix (nal,t) =
(* match t with
| CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
@@ -644,7 +659,7 @@ let pr_cofix_tac (id,c) =
(* Printing tactics as arguments *)
let rec pr_atom0 = function
| TacIntroPattern [] -> str "intros"
- | TacIntroMove (None,None) -> str "intro"
+ | TacIntroMove (None,hto) when hto = no_move -> str "intro"
| TacAssumption -> str "assumption"
| TacAnyConstructor (false,None) -> str "constructor"
| TacAnyConstructor (true,None) -> str "econstructor"
@@ -672,12 +687,10 @@ and pr_atom1 = function
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 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)
+ | TacIntroMove (None,hto) as t when hto = no_move -> pr_atom0 t
+ | TacIntroMove (Some id,hto) when hto = no_move -> str "intro " ++ pr_id id
+ | TacIntroMove (ido,hto) ->
+ hov 1 (str"intro" ++ pr_opt pr_id ido ++ pr_move_location pr_ident hto)
| 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)
@@ -685,7 +698,7 @@ and pr_atom1 = function
| TacApply (a,ev,cb) ->
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
- pr_with_bindings cb)
+ prlist_with_sep pr_coma pr_with_bindings cb)
| TacElim (ev,cb,cbo) ->
hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
pr_opt pr_eliminator cbo)
@@ -737,22 +750,17 @@ and pr_atom1 = function
++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
*)
(* Derived basic tactics *)
- | TacSimpleInduction h ->
- hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewInduction (ev,h,e,ids,cl) ->
- hov 1 (str (with_evars ev "induction") ++ spc () ++
- prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
- pr_with_names ids ++
- pr_opt pr_eliminator e ++
- pr_opt_no_spc (pr_clauses pr_ident) cl)
- | TacSimpleDestruct h ->
- hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewDestruct (ev,h,e,ids,cl) ->
- hov 1 (str (with_evars ev "destruct") ++ spc () ++
- prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
- pr_with_names ids ++
- pr_opt pr_eliminator e ++
- pr_opt_no_spc (pr_clauses pr_ident) cl)
+ | TacSimpleInductionDestruct (isrec,h) ->
+ hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
+ ++ pr_arg pr_quantified_hypothesis h)
+ | TacInductionDestruct (isrec,ev,l) ->
+ hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
+ spc () ++
+ prlist_with_sep pr_coma (fun (h,e,ids,cl) ->
+ prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
+ pr_with_induction_names ids ++
+ pr_opt pr_eliminator e ++
+ pr_opt_no_spc (pr_clauses pr_ident) cl) l)
| TacDoubleInduction (h1,h2) ->
hov 1
(str "double induction" ++
@@ -796,8 +804,8 @@ and pr_atom1 = function
(* Rem: only b = true is available for users *)
assert b;
hov 1
- (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
- str "after" ++ brk (1,1) ++ pr_ident id2)
+ (str "move" ++ brk (1,1) ++ pr_ident id1 ++
+ pr_move_location pr_ident id2)
| TacRename l ->
hov 1
(str "rename" ++ brk (1,1) ++
@@ -852,11 +860,11 @@ and pr_atom1 = function
| 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 c)
+ pr_with_inversion_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)
+ pr_with_inversion_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 c ++
@@ -874,6 +882,7 @@ let rec pr_tac inherited tac =
str "using " ++ pr_id s),
labstract
| TacLetIn (recflag,llc,u) ->
+ let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
v 0
(hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
fnl () ++ pr_tac (llet,E) u),
@@ -886,7 +895,7 @@ let rec pr_tac inherited tac =
lrul
++ fnl() ++ str "end"),
lmatch
- | TacMatchContext (lz,lr,lrul) ->
+ | TacMatchGoal (lz,lr,lrul) ->
hov 0 (pr_lazy lz ++
str (if lr then "match reverse goal with" else "match goal with")
++ prlist
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index e5162dae..e24f666f 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pptactic.mli 9842 2007-05-20 17:44:23Z herbelin $ i*)
+(*i $Id: pptactic.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Pp
open Genarg
@@ -78,6 +78,8 @@ val pr_extend :
(tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
string -> typed_generic_argument list -> std_ppcmds
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ac2adde2..67cd6f72 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 11059 2008-06-06 09:29:20Z herbelin $ *)
+(* $Id: ppvernac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Names
@@ -403,9 +403,6 @@ 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_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
-let pr_lname_lident_constr (oi,bk,a) =
- (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ())
- ++ pr_lconstr a in
let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l
++ sep ++ pr_constrarg c in
@@ -717,8 +714,7 @@ let rec pr_vernac = function
| VernacContext l ->
hov 1 (
str"Context" ++ spc () ++ str"[" ++ spc () ++
- prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++
- spc () ++ str "]")
+ pr_and_type_binders_arg l ++ spc () ++ str "]")
| VernacDeclareInstance id ->
@@ -808,10 +804,7 @@ let rec pr_vernac = function
(Global.env())
body in
hov 1
- (((*if !Flags.p1 then
- (if rc then str "Recursive " else mt()) ++
- str "Tactic Definition " else*)
- (* Rec by default *) str "Ltac ") ++
+ ((str "Ltac ") ++
prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
| VernacHints (local,dbnames,h) ->
pr_hints local dbnames h pr_constr pr_pattern_expr
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 401ef7fe..3aa51c53 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
* on May-June 2006 for implementation of abstraction of pretty-printing of objects.
*)
-(* $Id: prettyp.ml 10971 2008-05-22 17:12:11Z barras $ *)
+(* $Id: prettyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -219,7 +219,7 @@ let pr_located_qualid = function
| ModuleType (qid,_) ->
str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid)
| Undefined qid ->
- pr_qualid qid ++ str " is not a defined object"
+ pr_qualid qid ++ spc () ++ str "not a defined object."
let print_located_qualid ref =
let (loc,qid) = qualid_of_reference ref in
@@ -303,7 +303,7 @@ let build_inductive sp tyi =
| Polymorphic ar ->
it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
let arity = hnf_prod_applist env fullarity args in
- let cstrtypes = arities_of_constructors env (sp,tyi) in
+ let cstrtypes = type_of_constructors env (sp,tyi) in
let cstrtypes =
Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
let cstrnames = mip.mind_consnames in
@@ -599,12 +599,12 @@ let read_sec_context r =
let dir =
try Nametab.locate_section qid
with Not_found ->
- user_err_loc (loc,"read_sec_context", str "Unknown section") in
+ user_err_loc (loc,"read_sec_context", str "Unknown section.") in
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| (_,Lib.ClosedSection _)::rest ->
- error "Cannot print the contents of a closed section"
+ error "Cannot print the contents of a closed section."
(* LEM: Actually, we could if we wanted to. *)
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
@@ -648,7 +648,7 @@ let print_name ref =
print_leaf_entry true (oname,lobj)
with Not_found ->
errorlabstrm
- "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object")
+ "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
let print_opaque_name qid =
let env = Global.env () in
@@ -658,7 +658,7 @@ let print_opaque_name qid =
if cb.const_body <> None then
print_constant_with_infos cst
else
- error "not a defined constant"
+ error "Not a defined constant."
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr ->
@@ -736,7 +736,8 @@ let index_of_class cl =
try
fst (class_info cl)
with _ ->
- errorlabstrm "index_of_class" (pr_class cl ++ str" is not a defined class")
+ errorlabstrm "index_of_class"
+ (pr_class cl ++ spc() ++ str "not a defined class.")
let print_path_between cls clt =
let i = index_of_class cls in
@@ -746,7 +747,8 @@ let print_path_between cls clt =
lookup_path_between (i,j)
with _ ->
errorlabstrm "index_cl_of_id"
- (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt)
+ (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
+ ++ str ".")
in
print_path ((i,j),p)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 6a19cb0a..b126cc9c 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 11001 2008-05-27 16:56:07Z aspiwack $ *)
+(* $Id: printer.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -28,6 +28,7 @@ open Refiner
open Pfedit
open Ppconstr
open Constrextern
+open Tacexpr
let emacs_str s alts =
match !Flags.print_emacs, !Flags.print_emacs_safechar with
@@ -318,7 +319,7 @@ let rec pr_evars_int i = function
let default_pr_subgoal n =
let rec prrec p = function
- | [] -> error "No such goal"
+ | [] -> error "No such goal."
| g::rest ->
if p = 1 then
let pg = default_pr_goal g in
@@ -421,14 +422,14 @@ let pr_prim_rule = function
| Intro id ->
str"intro " ++ pr_id id
- | Intro_replacing id ->
- (str"intro replacing " ++ pr_id id)
-
- | Cut (b,id,t) ->
- if b then
- (str"assert " ++ pr_constr t)
- else
- (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+ | Cut (b,replace,id,t) ->
+ if b then
+ (* TODO: express "replace" *)
+ (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
+ else
+ let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
+ (str"cut " ++ pr_constr t ++
+ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
| FixRule (f,n,[]) ->
(str"fix " ++ pr_id f ++ str"/" ++ int n)
@@ -472,7 +473,7 @@ let pr_prim_rule = function
| Move (withdep,id1,id2) ->
(str (if withdep then "dependent " else "") ++
- str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2)
+ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2)
| Rename (id1,id2) ->
(str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
@@ -527,3 +528,14 @@ let pr_assumptionset env s =
in
(Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
+
+open Typeclasses
+
+let pr_instance i =
+ pr_global (ConstRef (instance_impl i))
+
+let pr_instance_gmap insts =
+ prlist_with_sep fnl (fun (gr, insts) ->
+ prlist_with_sep fnl pr_instance (cmap_to_list insts))
+ (Gmap.to_list insts)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 935fca12..40bb9122 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 11001 2008-05-27 16:56:07Z aspiwack $ i*)
+(*i $Id: printer.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
(*i*)
open Pp
@@ -22,6 +22,7 @@ open Termops
open Evd
open Proof_type
open Rawterm
+open Tacexpr
(*i*)
(* These are the entry points for printing terms, context, tac, ... *)
@@ -137,3 +138,5 @@ val set_printer_pr : printer_pr -> unit
val default_printer_pr : printer_pr
+val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
+ Pp.std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 24562459..a4cfe27a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
-(* $Id: q_coqast.ml4 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: q_coqast.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Names
@@ -62,6 +62,10 @@ let mlexpr_of_reference = function
| Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
| Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
+
+let mlexpr_of_loc loc = <:expr< $dloc$ >>
+
let mlexpr_of_by_notation f = function
| Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
| Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >>
@@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function
| Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >>
| Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >>
-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
| Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
| Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
@@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function
let mlexpr_of_binder_kind = function
| Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
- | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >>
+ | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
let rec mlexpr_of_constr = function
| Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
@@ -242,6 +242,11 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
let mlexpr_of_constr_with_binding =
mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
+let mlexpr_of_move_location f = function
+ | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >>
+ | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >>
+ | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >>
+
let mlexpr_of_induction_arg = function
| Tacexpr.ElimOnConstr c ->
<:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >>
@@ -279,13 +284,13 @@ let mlexpr_of_message_token = function
let rec mlexpr_of_atomic_tactic = function
(* Basic tactics *)
| Tacexpr.TacIntroPattern pl ->
- let pl = mlexpr_of_list mlexpr_of_intro_pattern pl in
+ let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
<:expr< Tacexpr.TacIntroPattern $pl$ >>
| Tacexpr.TacIntrosUntil h ->
<:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacIntroMove (idopt,idopt') ->
let idopt = mlexpr_of_ident_option idopt in
- let idopt'=mlexpr_of_option (mlexpr_of_located mlexpr_of_ident) idopt' in
+ let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
<:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
| Tacexpr.TacAssumption ->
<:expr< Tacexpr.TacAssumption >>
@@ -296,7 +301,7 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacVmCastNoCheck c ->
<:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
| Tacexpr.TacApply (b,false,cb) ->
- <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >>
+ <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >>
| Tacexpr.TacElim (false,cb,cbo) ->
let cb = mlexpr_of_constr_with_binding cb in
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
@@ -332,7 +337,7 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacCut c ->
<:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
| Tacexpr.TacAssert (t,ipat,c) ->
- let ipat = mlexpr_of_intro_pattern ipat in
+ let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in
<:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
$mlexpr_of_constr c$ >>
| Tacexpr.TacGeneralize cl ->
@@ -348,18 +353,18 @@ let rec mlexpr_of_atomic_tactic = function
$mlexpr_of_bool b$ >>
(* Derived basic tactics *)
- | Tacexpr.TacSimpleInduction h ->
- <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
- | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) ->
- let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_intro_pattern ids in
- <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
- | Tacexpr.TacSimpleDestruct h ->
- <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
- | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) ->
- let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_intro_pattern ids in
- <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
+ | Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
+ <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$
+ $mlexpr_of_quantified_hypothesis h$ >>
+ | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
+ <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
+ $mlexpr_of_list (mlexpr_of_quadruple
+ (mlexpr_of_list mlexpr_of_induction_arg)
+ (mlexpr_of_option mlexpr_of_constr_with_binding)
+ (mlexpr_of_pair
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))
+ (mlexpr_of_option mlexpr_of_clause)) l$ >>
(* Context management *)
| Tacexpr.TacClear (b,l) ->
@@ -371,7 +376,7 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacMove (dep,id1,id2) ->
<:expr< Tacexpr.TacMove $mlexpr_of_bool dep$
$mlexpr_of_hyp id1$
- $mlexpr_of_hyp id2$ >>
+ $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
(* Constructors *)
| Tacexpr.TacLeft (ev,l) ->
@@ -462,8 +467,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
$mlexpr_of_bool lz$
$mlexpr_of_tactic t$
$mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
- | Tacexpr.TacMatchContext (lz,lr,l) ->
- <:expr< Tacexpr.TacMatchContext
+ | Tacexpr.TacMatchGoal (lz,lr,l) ->
+ <:expr< Tacexpr.TacMatchGoal
$mlexpr_of_bool lz$
$mlexpr_of_bool lr$
$mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index da78e287..da4329bb 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "q_MLast.cmo" i*)
-(* $Id: q_util.ml4 10091 2007-08-24 10:57:37Z herbelin $ *)
+(* $Id: q_util.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
(* This file defines standard combinators to build ml expressions *)
@@ -53,6 +53,11 @@ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
<:expr< ($e1$, $e2$, $e3$) >>
+let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)=
+ let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in
+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in
+ <:expr< ($e1$, $e2$, $e3$, $e4$) >>
+
(* We don't give location for tactic quotation! *)
let loc = dummy_loc
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 901f9198..b950e68f 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: q_util.mli 9265 2006-10-24 08:35:38Z herbelin $ i*)
+(*i $Id: q_util.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
val patt_of_expr : MLast.expr -> MLast.patt
@@ -20,6 +20,10 @@ val mlexpr_of_triple :
('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr)
-> 'a * 'b * 'c -> MLast.expr
+val mlexpr_of_quadruple :
+ ('a -> MLast.expr) -> ('b -> MLast.expr) ->
+ ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> MLast.expr
+
val mlexpr_of_bool : bool -> MLast.expr
val mlexpr_of_int : int -> MLast.expr
diff --git a/parsing/search.ml b/parsing/search.ml
index c375826c..c6ff4c04 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: search.ml 10840 2008-04-23 21:29:34Z herbelin $ *)
+(* $Id: search.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -150,7 +150,7 @@ let rec id_from_pattern = function
| PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
*)
| PApp (p,_) -> id_from_pattern p
- | _ -> error "the pattern is not simple enough"
+ | _ -> error "The pattern is not simple enough."
let raw_pattern_search extra_filter display_function pat =
let name = id_from_pattern pat in
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 3d71af84..695677a3 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: tacextend.ml4 10091 2007-08-24 10:57:37Z herbelin $ *)
+(* $Id: tacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Genarg
@@ -206,7 +206,7 @@ EXTEND
let t, g = Q_util.interp_entry_name loc e sep in
TacNonTerm (loc, t, g, Some s)
| s = STRING ->
- if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
+ if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal.");
TacTerm s
] ]
;
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index c5b77774..e0836984 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactic_printer.ml 11146 2008-06-19 08:26:38Z corbinea $ *)
+(* $Id: tactic_printer.ml 11313 2008-08-07 11:15:03Z barras $ *)
open Pp
open Util
@@ -90,7 +90,8 @@ let pr_change gl =
str"change " ++
pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
-let rec print_decl_script tac_printer nochange sigma pf =
+let print_decl_script tac_printer ?(nochange=true) sigma pf =
+ let rec print_prf pf =
match pf.ref with
| None ->
(if nochange then
@@ -99,46 +100,38 @@ let rec print_decl_script tac_printer nochange sigma pf =
pr_change pf.goal)
++ fnl ()
| Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
- | Some (Prim Change_evars,[subpf]) ->
- print_decl_script tac_printer nochange sigma subpf
+ | Some (Prim Change_evars,[subpf]) -> print_prf subpf
| Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
begin
match instr.instr,subprfs with
Pescape,[{ref=Some(_,subsubprfs)}] ->
hov 7
(pr_rule_dot_fnl rule ++
- prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
- if opened then mt () else str "return."
+ prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
+ if opened then mt () else str "return."
| Pclaim _,[body;cont] ->
- hov 2
- (pr_rule_dot_fnl rule ++
- print_decl_script tac_printer nochange sigma body) ++
- fnl () ++
- if opened then mt () else str "end claim." ++ fnl () ++
- print_decl_script tac_printer nochange sigma cont
+ hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
+ (if opened then mt () else str "end claim." ++ fnl ()) ++
+ print_prf cont
| Pfocus _,[body;cont] ->
- hov 2
- (pr_rule_dot_fnl rule ++
- print_decl_script tac_printer nochange sigma body) ++
- fnl () ++
- if opened then mt () else str "end focus." ++ fnl () ++
- print_decl_script tac_printer nochange sigma cont
+ hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++
+ fnl () ++
+ (if opened then mt () else str "end focus." ++ fnl ()) ++
+ print_prf cont
| (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
- hov 2
- (pr_rule_dot_fnl rule ++
- print_decl_script tac_printer nochange sigma body) ++
- fnl () ++
- print_decl_script tac_printer nochange sigma cont
+ hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
+ print_prf cont
| _,[next] ->
- pr_rule_dot_fnl rule ++
- print_decl_script tac_printer nochange sigma next
+ pr_rule_dot_fnl rule ++ print_prf next
| _,[] ->
pr_rule_dot rule
| _,_ -> anomaly "unknown branching instruction"
end
- | _ -> anomaly "Not Applicable"
+ | _ -> anomaly "Not Applicable" in
+ print_prf pf
-let rec print_script nochange sigma pf =
+let print_script ?(nochange=true) sigma pf =
+ let rec print_prf pf =
match pf.ref with
| None ->
(if nochange then
@@ -153,26 +146,25 @@ let rec print_script nochange sigma pf =
end ++
begin
hov 0 (str "proof." ++ fnl () ++
- print_decl_script (print_script nochange sigma)
- nochange sigma (List.hd script))
+ print_decl_script print_prf
+ ~nochange sigma (List.hd script))
end ++ fnl () ++
begin
if opened then mt () else (str "end proof." ++ fnl ())
end
| Some(Daimon,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
- prlist_with_sep pr_fnl
- (print_script nochange sigma) spfl )
+ prlist_with_sep pr_fnl print_prf spfl )
| Some(rule,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
pr_rule_dot_fnl rule ++
- prlist_with_sep pr_fnl
- (print_script nochange sigma) spfl )
+ prlist_with_sep pr_fnl print_prf spfl ) in
+ print_prf pf
(* printed by Show Script command *)
-let print_treescript nochange sigma pf =
- let rec aux pf =
+let print_treescript ?(nochange=true) sigma pf =
+ let rec print_prf pf =
match pf.ref with
| None ->
if nochange then
@@ -184,23 +176,21 @@ let print_treescript nochange sigma pf =
begin
if nochange then mt () else pr_change pf.goal ++ fnl ()
end ++
- hov 0
+ hov 0
begin str "proof." ++ fnl () ++
- print_decl_script aux
- nochange sigma (List.hd script)
+ print_decl_script print_prf ~nochange sigma (List.hd script)
end ++ fnl () ++
- begin
- if opened then mt () else (str "end proof." ++ fnl ())
- end
+ begin
+ if opened then mt () else (str "end proof." ++ fnl ())
+ end
| Some(Daimon,spfl) ->
- ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
- prlist_with_sep pr_fnl
- (print_script nochange sigma) spfl )
+ (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+ prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
| Some(r,spfl) ->
let indent = if List.length spfl >= 2 then 1 else 0 in
- (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
- hv indent (pr_rule_dot_fnl r ++ prlist_with_sep mt aux spfl)
- in hov 0 (aux pf)
+ (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+ hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
+ in hov 0 (print_prf pf)
let rec print_info_script sigma osign pf =
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 676dbdf2..affc5ec2 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tactic_printer.mli 10580 2008-02-22 13:39:13Z lmamane $ i*)
+(*i $Id: tactic_printer.mli 11313 2008-08-07 11:15:03Z barras $ i*)
(*i*)
open Pp
@@ -23,6 +23,6 @@ val pr_rule : rule -> std_ppcmds
val pr_tactic : tactic_expr -> std_ppcmds
val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds
val print_script :
- bool -> evar_map -> proof_tree -> std_ppcmds
+ ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
val print_treescript :
- bool -> evar_map -> proof_tree -> std_ppcmds
+ ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index d12ca098..08feb17a 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: vernacextend.ml4 10091 2007-08-24 10:57:37Z herbelin $ *)
+(* $Id: vernacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Genarg
@@ -110,7 +110,7 @@ EXTEND
rule:
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
->
- if s = "" then Util.user_err_loc (loc,"",Pp.str "Command name is empty");
+ if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty.");
(s,l,<:expr< fun () -> $e$ >>)
] ]
;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-08 09:23:08 +0000