summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml437
-rw-r--r--parsing/g_constr.ml416
-rw-r--r--parsing/g_ltac.ml44
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--parsing/g_xml.ml418
-rw-r--r--parsing/lexer.ml415
-rw-r--r--parsing/pcoq.ml48
-rw-r--r--parsing/ppconstr.ml8
-rw-r--r--parsing/ppvernac.ml6
-rw-r--r--parsing/q_util.ml428
10 files changed, 66 insertions, 84 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index ec3c2c9c..638a8d65 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: argextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: argextend.ml4 8976 2006-06-23 10:03:54Z herbelin $ *)
open Genarg
open Q_util
@@ -176,41 +176,6 @@ let declare_vernac_argument loc s cl =
open Vernacexpr
open Pcoq
-
-let rec interp_entry_name loc s =
- let l = String.length s in
- if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
- List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
- else if l > 5 & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
- List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
- else if l > 4 & String.sub s (l-4) 4 = "_opt" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
- 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 ->
- match Pcoq.entry_type (Pcoq.get_univ "constr") s with
- | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
- | None ->
- match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
- | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
- | None -> None, <:expr< $lid:s$ >> in
- let t =
- match t with
- | Some t -> t
- | None ->
-(* Pp.warning_with Pp_control.err_ft
- ("Unknown primitive grammar entry: "^s);*)
- ExtraArgType s
- in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
-
open Pcaml
EXTEND
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9ee312ff..a1c0c9ae 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 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: g_constr.ml4 9043 2006-07-12 10:06:40Z herbelin $ *)
open Pcoq
open Constr
@@ -244,6 +244,7 @@ GEXTEND Gram
fixannot:
[ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
| "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
+ | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel)
| -> (None, CStructRec)
] ]
;
@@ -273,24 +274,25 @@ GEXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
;
eqn:
- [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
+ [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|";
+ "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
;
pattern:
[ "200" RIGHTA [ ]
- | "100" LEFTA
+ | "100" RIGHTA
[ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ]
| "99" RIGHTA [ ]
| "10" LEFTA
- [ p = pattern; lp = LIST1 (pattern LEVEL "0") ->
+ [ p = pattern; lp = LIST1 NEXT ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
| _ -> Util.user_err_loc
(cases_pattern_loc p, "compound_pattern",
Pp.str "Constructor expected"))
| p = pattern; "as"; id = ident ->
- CPatAlias (loc, p, id)
- | c = pattern; "%"; key=IDENT ->
- CPatDelimiters (loc,key,c) ]
+ CPatAlias (loc, p, id) ]
+ | "1" LEFTA
+ [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
| "0"
[ r = Prim.reference -> CPatAtom (loc,Some r)
| "_" -> CPatAtom (loc,None)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index eaa51810..c01c23b6 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 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *)
open Pp
open Util
@@ -134,7 +134,7 @@ GEXTEND Gram
| "()" -> TacVoid ] ]
;
match_key:
- [ [ "match" -> false ] ]
+ [ [ "match" -> false | "lazymatch" -> true ] ]
;
input_fun:
[ [ "_" -> None
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7405ae54..a72ced97 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 8929 2006-06-08 22:35:58Z herbelin $ *)
+(* $Id: g_vernac.ml4 9017 2006-07-05 17:27:34Z herbelin $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Pp
@@ -237,6 +237,7 @@ GEXTEND Gram
rec_annotation:
[ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
| "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel)
+ | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel)
| -> (None, CStructRec)
] ]
;
@@ -651,8 +652,11 @@ GEXTEND Gram
VernacBacktrack (n,m,p)
(* Tactic Debugger *)
- | IDENT "Debug"; IDENT "On" -> VernacDebug true
- | IDENT "Debug"; IDENT "Off" -> VernacDebug false
+ | IDENT "Debug"; IDENT "On" ->
+ VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue true)
+
+ | IDENT "Debug"; IDENT "Off" ->
+ VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue false)
] ];
END
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 5ad0193b..a89fffa0 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 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: g_xml.ml4 9016 2006-07-05 17:19:39Z herbelin $ *)
open Pp
open Util
@@ -228,6 +228,10 @@ and interp_xml_recursionOrder x =
(match l with
[c] -> RWfRec (interp_xml_type c)
| _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+ | "Measure" ->
+ (match l with
+ [c] -> RMeasureRec (interp_xml_type c)
+ | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
| _ ->
user_err_loc (locs,"",str "invalid recursion order")
@@ -252,22 +256,12 @@ and interp_xml_CoFixFunction x =
(* Interpreting tactic argument *)
-let rec (interp_xml_tactic_expr : xml -> glob_tactic_expr) = function
- | XmlTag (loc,"TACARG",[],[x]) ->
- TacArg (interp_xml_tactic_arg x)
- | _ -> error "Ill-formed xml tree"
-
-and interp_xml_tactic_arg = function
+let rec interp_xml_tactic_arg = function
| XmlTag (loc,"TERM",[],[x]) ->
ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
| 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,"TACTIC",[],[x]) ->
- Tacexp (interp_xml_tactic_expr x)
- | _ -> error "Ill-formed xml tree"
-*)
| XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
let parse_tactic_arg ch =
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c02dc59b..80eaf7f0 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 8924 2006-06-08 17:49:01Z notin $ i*)
+(*i $Id: lexer.ml4 9015 2006-07-05 17:19:22Z herbelin $ i*)
open Pp
open Token
@@ -146,12 +146,14 @@ let lookup_utf8_tail c cs =
(* 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 *)
+ (* utf-8 Cyrillic supplement 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 *)
+ (* utf-8 Arabic letters U0621-064A *)
| x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n
+ (* utf-8 Arabic supplement letters U0750-076D *)
+ | x when 0x0750 <= x & x <= 0x076D -> Utf8Letter n
| _ -> error_unsupported_unicode_character n cs
end
| 0x1000 ->
@@ -589,9 +591,10 @@ let is_ident_not_keyword s =
| _ -> false
let is_number s =
- match s.[0] with
- | '0'..'9' -> true
- | _ -> false
+ let rec aux i =
+ String.length s = i or
+ match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
+ in aux 0
let strip s =
let len =
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 127a911f..56e434fb 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 8926 2006-06-08 20:23:17Z herbelin $ i*)
+(*i $Id: pcoq.ml4 9043 2006-07-12 10:06:40Z herbelin $ i*)
open Pp
open Util
@@ -484,7 +484,11 @@ let default_levels =
0,Gramext.RightA]
let default_pattern_levels =
- [10,Gramext.LeftA;
+ [200,Gramext.RightA;
+ 100,Gramext.RightA;
+ 99,Gramext.RightA;
+ 10,Gramext.LeftA;
+ 1,Gramext.LeftA;
0,Gramext.RightA]
let level_stack =
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index d55a6c1e..a1ca386e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: ppconstr.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
(*i*)
open Util
@@ -186,12 +186,12 @@ let rec pr_patt sep inh p =
let pr_patt = pr_patt mt
-
let pr_eqn pr (loc,pl,rhs) =
spc() ++ hov 4
(pr_with_comments loc
(str "| " ++
- hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
+ hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
+ ++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
let begin_of_binder = function
@@ -384,6 +384,8 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
else mt()
| CWfRec c ->
spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+ | CMeasureRec c ->
+ spc () ++ str "{measure " ++ 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
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index aea44604..7e3c853d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
+(* $Id: ppvernac.ml 9020 2006-07-05 17:35:23Z herbelin $ *)
open Pp
open Names
@@ -414,7 +414,6 @@ let rec pr_vernac = function
| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l
in pr_showable s
| VernacCheckGuard -> str"Guarded"
- | VernacDebug b -> pr_topcmd b
(* Resetting *)
| VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
@@ -572,6 +571,9 @@ let rec pr_vernac = function
| CWfRec c ->
spc() ++ str "{wf " ++ pr_name name ++ spc() ++
pr_lconstr_expr c ++ str"}"
+ | CMeasureRec c ->
+ spc() ++ str "{measure " ++ 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_
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 07b23972..61a552f3 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_util.ml4 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: q_util.ml4 8982 2006-06-23 13:17:49Z herbelin $ *)
(* This file defines standard combinators to build ml expressions *)
@@ -84,21 +84,27 @@ let rec interp_entry_name loc s =
OptArgType t, <:expr< Gramext.Sopt $g$ >>
else
let s = if s = "hyp" then "var" else s in
- let t, se =
+ let t, se, lev =
+ match tactic_genarg_level s with
+ | Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
+ | None ->
match Pcoq.entry_type (Pcoq.get_univ "prim") s with
- | Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+ | Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
| None ->
match Pcoq.entry_type (Pcoq.get_univ "constr") s with
- | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+ | Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None
| None ->
match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
- | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
- | None -> None, <:expr< $lid:s$ >> in
+ | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None
+ | None -> None, <:expr< $lid:s$ >>, None in
let t =
match t with
| Some t -> t
- | None ->
-(* Pp.warning_with Pp_control.err_ft
- ("Unknown primitive grammar entry: "^s);*)
- ExtraArgType s
- in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+ | None -> ExtraArgType s in
+ let entry = match lev with
+ | Some n ->
+ let s = string_of_int n in
+ <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >>
+ | None ->
+ <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+ in t, entry
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 03:38:06 +0000