From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 23:19:35 +0200 Subject: [location] [ast] Switch Constrexpr AST to an extensible node type. Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. --- parsing/egramcoq.ml | 16 +++--- parsing/g_constr.ml4 | 150 +++++++++++++++++++++++++-------------------------- parsing/g_proofs.ml4 | 2 +- parsing/g_vernac.ml4 | 12 ++--- 4 files changed, 90 insertions(+), 90 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 49bf267db..712d10a96 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -313,11 +313,11 @@ let interp_entry forpat e = match e with | ETBinderList (true, _) -> assert false | ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) -let constr_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with +let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (Loc.tag ?loc id), None) -let cases_pattern_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with +let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id))) @@ -342,13 +342,13 @@ match e with | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (Loc.tag @@ CPrim (Numeral v)) - | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v)) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral v)) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral v)) end | TTReference -> begin match forpat with - | ForConstr -> push_constr subst (Loc.tag @@ CRef (v, None)) - | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v)) + | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) + | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v)) end | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } @@ -431,12 +431,12 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> let env = (env.constrs, env.constrlists, List.map fst env.binders) in - Loc.tag ~loc @@ CNotation (notation , env) + CAst.make ~loc @@ CNotation (notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in - Loc.tag ~loc @@ CPatNotation (notation, env, []) + CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = let n = ng.notgram_level in diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 45585d9ce..a44aa5400 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -34,11 +34,11 @@ let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) - in Loc.tag ?loc @@ CCast(c, CastConv ty) + in CAst.make ?loc @@ CCast(c, CastConv ty) let binder_of_name expl (loc,na) = CLocalAssum ([loc, na], Default expl, - Loc.tag ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) + CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = List.map (binder_of_name Explicit) l @@ -46,7 +46,7 @@ let binders_of_names l = let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty - | None -> Loc.tag @@ CHole (None, IntroAnonymous, None) in + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = @@ -56,16 +56,16 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty - | None -> Loc.tag @@ CHole (None, IntroAnonymous, None) in + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = if kw then let fb = List.map mk_fixb dcls in - Loc.tag ~loc @@ CFix(id,fb) + CAst.make ~loc @@ CFix(id,fb) else let fb = List.map mk_cofixb dcls in - Loc.tag ~loc @@ CCoFix(id,fb) + CAst.make ~loc @@ CCoFix(id,fb) let mk_single_fix (loc,kw,dcl) = let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) @@ -120,7 +120,7 @@ let name_colon = | _ -> err ()) | _ -> err ()) -let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None +let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr universe_level sort global @@ -159,62 +159,62 @@ GEXTEND Gram ; constr: [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global; i = instance -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ] + | "@"; f=global; i = instance -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ] ; operconstr: [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) | c1 = operconstr; "<<:"; c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) | c1 = operconstr; "<<:"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) | c1 = operconstr; ":";c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) | c1 = operconstr; ":>" -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] + CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> Loc.tag ~loc:(!@loc) @@ CApp((None,f),args) - | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),args) + [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) + | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> - let args = List.map (fun x -> Loc.tag @@ CRef (Ident x,None), None) args in - Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ?loc:locid @@ CPatVar id),args) ] + let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in + CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - Loc.tag ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - Loc.tag ~loc:(!@loc) @@ CApp((Some (List.length args+1), Loc.tag @@ CRef (f,None)),args@[c,None]) + CAst.make ~loc:(!@loc) @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) | c=operconstr; ".("; "@"; f=global; args=LIST0 (operconstr LEVEL "9"); ")" -> - Loc.tag ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) - | c=operconstr; "%"; key=IDENT -> Loc.tag ~loc:(!@loc) @@ CDelimiters (key,c) ] + CAst.make ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) + | c=operconstr; "%"; key=IDENT -> CAst.make ~loc:(!@loc) @@ CDelimiters (key,c) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c | "("; c = operconstr LEVEL "200"; ")" -> - (match snd c with + (match c.CAst.v with CPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) + CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c | "`{"; c = operconstr LEVEL "200"; "}" -> - Loc.tag ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) + CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> - Loc.tag ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) + CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) ] ] ; record_declaration: - [ [ fs = record_fields -> Loc.tag ~loc:(!@loc) @@ CRecord fs ] ] + [ [ fs = record_fields -> CAst.make ~loc:(!@loc) @@ CRecord fs ] ] ; record_fields: @@ -236,40 +236,40 @@ GEXTEND Gram | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> let ty,c1 = match ty, c1 with - | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) + | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) | _, _ -> ty, c1 in - Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, + CAst.make ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in - let (li,id) = match snd fixp with + let (li,id) = match fixp.CAst.v with CFix(id,_) -> id | CCoFix(id,_) -> id | _ -> assert false in - Loc.tag ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) + CAst.make ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ CLetTuple (lb,po,c1,c2) + CAst.make ~loc:!@loc @@ CLetTuple (lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> - Loc.tag ~loc:(!@loc) @@ CIf (c, po, b1, b2) + CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2) | c=fix_constr -> c ] ] ; appl_arg: @@ -278,14 +278,14 @@ GEXTEND Gram | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: - [ [ g=global; i=instance -> Loc.tag ~loc:!@loc @@ CRef (g,i) - | s=sort -> Loc.tag ~loc:!@loc @@ CSort s - | n=INT -> Loc.tag ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n)) - | s=string -> Loc.tag ~loc:!@loc @@ CPrim (String s) - | "_" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None) - | "?"; "["; id=ident; "]" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) - | "?"; "["; id=pattern_ident; "]" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroFresh id, None) - | id=pattern_ident; inst = evar_instance -> Loc.tag ~loc:!@loc @@ CEvar(id,inst) ] ] + [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i) + | s=sort -> CAst.make ~loc:!@loc @@ CSort s + | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n)) + | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s) + | "_" -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) + | "?"; "["; id=ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) + | "?"; "["; id=pattern_ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroFresh id, None) + | id=pattern_ident; inst = evar_instance -> CAst.make ~loc:!@loc @@ CEvar(id,inst) ] ] ; inst: [ [ id = ident; ":="; c = lconstr -> (id,c) ] ] @@ -326,7 +326,7 @@ GEXTEND Gram ; match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> Loc.tag ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ] + br=branches; "end" -> CAst.make ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ] ; case_item: [ [ c=operconstr LEVEL "100"; @@ -368,46 +368,46 @@ GEXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> Loc.tag ~loc:!@loc @@ CPatOr (p::pl) ] + [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> - Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ] + CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> - (match p with - | _, CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp) - | loc, CPatCstr (r, None, l2) -> + (let open CAst in match p with + | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) + | { v = CPatCstr (r, None, l2); loc } -> CErrors.user_err ?loc ~hdr:"compound_pattern" (Pp.str "Nested applications not supported.") - | _, CPatCstr (r, l1, l2) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) - | _, CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp) + | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) + | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp) | _ -> CErrors.user_err ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" (Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST0 NEXT -> - Loc.tag ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] + CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> Loc.tag ~loc:!@loc @@ CPatDelimiters (key,c) ] + [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ] | "0" - [ r = Prim.reference -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r) - | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat - | "_" -> Loc.tag ~loc:!@loc @@ CPatAtom None + [ r = Prim.reference -> CAst.make ~loc:!@loc @@ CPatAtom (Some r) + | "{|"; pat = record_patterns; "|}" -> CAst.make ~loc:!@loc @@ CPatRecord pat + | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None | "("; p = pattern LEVEL "200"; ")" -> - (match p with - | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) + (match p.CAst.v with + | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> + CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p) | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> let p = match p with - | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) + | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z -> + CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p in - Loc.tag ~loc:!@loc @@ CPatCast (p, ty) - | n = INT -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n)) - | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ] + CAst.make ~loc:!@loc @@ CPatCast (p, ty) + | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n)) + | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ] ; impl_ident_tail: [ [ "}" -> binder_of_name Implicit @@ -415,7 +415,7 @@ GEXTEND Gram (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> (fun na -> CLocalAssum (na::nal,Default Implicit, - Loc.tag ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> (fun na -> CLocalAssum ([na],Default Implicit,c)) ] ] @@ -449,7 +449,7 @@ GEXTEND Gram binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2], - Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' ] ] @@ -458,7 +458,7 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [CLocalAssum ([id],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + [ [ id = name -> [CLocalAssum ([id],Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder -> bl ] ] ; closed_binder: @@ -467,27 +467,27 @@ GEXTEND Gram | "("; id=name; ":"; c=lconstr; ")" -> [CLocalAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> - (match c with - | (_, CCast(c, CastConv t)) -> [CLocalDef (id,c,Some t)] + (match c.CAst.v with + | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)] | _ -> [CLocalDef (id,c,None)]) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> [CLocalDef (id,c,Some t)] | "{"; id=name; "}" -> - [CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + [CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [CLocalAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> [CLocalAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl) + List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc | "'"; p = pattern LEVEL "0" -> let (p, ty) = - match p with - | _, CPatCast (p, ty) -> (p, Some ty) + match p.CAst.v with + | CPatCast (p, ty) -> (p, Some ty) | _ -> (p, None) in [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 488995201..ee0f06fe0 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -120,7 +120,7 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> Loc.tag ~loc:!@loc @@ CCast(c,CastConv t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] ; mode: [ [ l = LIST1 [ "+" -> ModeInput diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c8101875d..27f879154 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -233,14 +233,14 @@ GEXTEND Gram DefineBody ([], red, c, None) else (match c with - | _, CCast(c, CastConv t) -> DefineBody (bl, red, c, Some t) + | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = if List.exists (function CLocalPattern _ -> true | _ -> false) bl then (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = Loc.tag ~loc:!@loc @@ CCast (c, CastConv t) in + let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in (([],mkCLambdaN ~loc:!@loc bl c), None) else ((bl, c), Some t) in @@ -305,7 +305,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -354,14 +354,14 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> fun id -> (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t))) | l = binders; ":="; b = lconstr -> fun id -> - match snd b with + match b.CAst.v with | CCast(b', (CastConv t|CastVM t|CastNative t)) -> (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t))) | _ -> (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id, Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -380,7 +380,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] -> t l ]] ; -- cgit v1.2.3