From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- parsing/argextend.ml4 | 37 +------------------------------------ parsing/g_constr.ml4 | 16 +++++++++------- parsing/g_ltac.ml4 | 4 ++-- parsing/g_vernac.ml4 | 10 +++++++--- parsing/g_xml.ml4 | 18 ++++++------------ parsing/lexer.ml4 | 15 +++++++++------ parsing/pcoq.ml4 | 8 ++++++-- parsing/ppconstr.ml | 8 +++++--- parsing/ppvernac.ml | 6 ++++-- parsing/q_util.ml4 | 28 +++++++++++++++++----------- 10 files changed, 66 insertions(+), 84 deletions(-) (limited to 'parsing') 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 -- cgit v1.2.3