diff options
author | 2017-04-08 23:19:35 +0200 | |
---|---|---|
committer | 2017-04-25 00:32:37 +0200 | |
commit | 054d2736c1c1b55cb7708ff0444af521cd0fe2ba (patch) | |
tree | 5228705fd054a59afec759eec780d2b4e9b53435 /parsing/g_constr.ml4 | |
parent | d062642d6e3671bab8a0e6d70e346325558d2db3 (diff) |
[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.
Diffstat (limited to 'parsing/g_constr.ml4')
-rw-r--r-- | parsing/g_constr.ml4 | 150 |
1 files changed, 75 insertions, 75 deletions
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))] |