From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- parsing/g_constr.ml4 | 22 ++++++++++++++-------- parsing/g_proofs.ml4 | 4 ++-- parsing/g_vernac.ml4 | 10 +++++----- parsing/g_xml.ml4 | 4 ++-- parsing/ppconstr.ml | 15 +++++++++------ parsing/q_constr.ml4 | 2 +- 6 files changed, 33 insertions(+), 24 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9163f3c1..1cde66e2 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 9562 2007-01-31 09:00:36Z msozeau $ *) +(* $Id: g_constr.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) open Pcoq open Constr @@ -21,14 +21,14 @@ open Util let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; + "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return"; "Prop"; "Set"; "Type"; ".("; "_"; ".." ] let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) let mk_lam = function ([],c) -> c @@ -156,13 +156,15 @@ GEXTEND Gram [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - CCast(loc,c1, CastConv VMcast,c2) + CCast(loc,c1, CastConv (VMcast,c2)) | c1 = operconstr; "<:"; c2 = SELF -> - CCast(loc,c1, CastConv VMcast,c2) + CCast(loc,c1, CastConv (VMcast,c2)) | c1 = operconstr; ":";c2 = binder_constr -> - CCast(loc,c1, CastConv DEFAULTcast,c2) + CCast(loc,c1, CastConv (DEFAULTcast,c2)) | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv DEFAULTcast,c2) ] + CCast(loc,c1, CastConv (DEFAULTcast,c2)) + | c1 = operconstr; ":>" -> + CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -210,6 +212,10 @@ GEXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CLetTuple (loc,List.map snd lb,po,c1,c2) + | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern; + "in"; c2 = operconstr LEVEL "200" -> + CCases (loc, None, [(c1, (None, None))], + [loc, [[p]], c2]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -328,7 +334,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t)) + LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t))) ] ] ; binder: diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 2f515a81..0a48748f 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_proofs.ml4 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: g_proofs.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) open Pcoq open Pp @@ -118,6 +118,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ] ; END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9a98df80..6a9388b2 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 9562 2007-01-31 09:00:36Z msozeau $ *) +(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -202,7 +202,7 @@ GEXTEND Gram def_body: [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -264,8 +264,8 @@ GEXTEND Gram ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) - | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) + | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; @@ -304,7 +304,7 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) | id = name; ":="; b = lconstr -> match b with - CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t)) + CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; assum_list: diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index c13532cc..2f31c0b6 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 9200 2006-10-03 14:11:08Z herbelin $ *) +(* $Id: g_xml.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -183,7 +183,7 @@ let rec interp_xml_constr = function let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - RCast (loc, interp_xml_term x1, CastConv DEFAULTcast, interp_xml_type x2) + RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> RSort (loc, get_xml_sort al) | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 349d5df8..275e179e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 9304 2006-10-28 09:58:16Z herbelin $ *) +(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *) (*i*) open Util @@ -215,7 +215,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c,_,t) -> c, t + | CCast(_,c, CastConv (_,t)) -> c, t | _ -> c, CHole dummy_loc in hov 1 (surround (pr_lname na ++ pr_opt_type pr_c topt ++ @@ -566,10 +566,13 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_rawsort s, latom - | CCast (_,a,k,b) -> - let s = match k with CastConv VMcast -> "<:" | _ -> ":" in + | CCast (_,a,CastConv (k,b)) -> + let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), lcast + | CCast (_,a,CastCoerce) -> + hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), + lcast | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env @@ -590,7 +593,7 @@ let pr = pr mt let rec strip_context n iscast t = if n = 0 then - [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t + [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t else match t with | CLambdaN (loc,(nal,t)::bll,c) -> let n' = List.length nal in @@ -613,7 +616,7 @@ let rec strip_context n iscast t = | CArrow (loc,t,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawAssum ([loc,Anonymous],t) :: bl', c - | CCast (_,c,_,_) -> strip_context n false c + | CCast (_,c,_) -> strip_context n false c | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 768bc45c..21c851df 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -73,7 +73,7 @@ EXTEND | "0" [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >> + | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >> | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] -- cgit v1.2.3