diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 368 |
1 files changed, 368 insertions, 0 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 new file mode 100644 index 00000000..7b0f7da2 --- /dev/null +++ b/parsing/g_constr.ml4 @@ -0,0 +1,368 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_constr.ml4,v 1.52.2.1 2004/07/16 19:30:38 herbelin Exp $ *) + +open Pcoq +open Constr +open Rawterm +open Term +open Names +open Libnames +open Prim +open Topconstr + +(* Initialize the lexer *) +let constr_kw = + [ "Cases"; "of"; "with"; "end"; "as"; "in"; "Prop"; "Set"; "Type"; + ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!"; + "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/"; + "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-"; + "~"; "'"; "<<"; ">>"; "<>" + ] +let _ = + if !Options.v7 then + List.iter (fun s -> Lexer.add_token ("",s)) constr_kw +(* "let" is not a keyword because #Core#let.cci would not parse. + Is it still accurate ? *) + + +let coerce_to_var = function + | CRef (Ident (_,id)) -> id + | ast -> Util.user_err_loc + (constr_loc ast,"Ast.coerce_to_var", + (Pp.str"This expression should be a simple identifier")) + +let coerce_to_name = function + | CRef (Ident (loc,id)) -> (loc, Name id) + | ast -> Util.user_err_loc + (constr_loc ast,"Ast.coerce_to_var", + (Pp.str"This expression should be a simple identifier")) + +let set_loc loc = function + | CRef(Ident(_,i)) -> CRef(Ident(loc,i)) + | CRef(Qualid(_,q)) -> CRef(Qualid(loc,q)) + | CFix(_,x,a) -> CFix(loc,x,a) + | CCoFix(_,x,a) -> CCoFix(loc,x,a) + | CArrow(_,a,b) -> CArrow(loc,a,b) + | CProdN(_,bl,a) -> CProdN(loc,bl,a) + | CLambdaN(_,bl,a) -> CLambdaN(loc,bl,a) + | CLetIn(_,x,a,b) -> CLetIn(loc,x,a,b) + | CAppExpl(_,f,a) -> CAppExpl(loc,f,a) + | CApp(_,f,a) -> CApp(loc,f,a) + | CCases(_,p,a,br) -> CCases(loc,p,a,br) + | COrderedCase(_,s,p,a,br) -> COrderedCase(loc,s,p,a,br) + | CLetTuple(_,ids,p,a,b) -> CLetTuple(loc,ids,p,a,b) + | CIf(_,e,p,a,b) -> CIf(loc,e,p,a,b) + | CHole _ -> CHole loc + | CPatVar(_,v) -> CPatVar(loc,v) + | CEvar(_,ev) -> CEvar(loc,ev) + | CSort(_,s) -> CSort(loc,s) + | CCast(_,a,b) -> CCast(loc,a,b) + | CNotation(_,n,l) -> CNotation(loc,n,l) + | CNumeral(_,i) -> CNumeral(loc,i) + | CDelimiters(_,s,e) -> CDelimiters(loc,s,e) + | CDynamic(_,d) -> CDynamic(loc,d) + +open Util + +let rec abstract_constr loc c = function + | [] -> c + | LocalRawDef ((loc',x),b)::bl -> + CLetIn (join_loc loc' loc, (loc', x), b, abstract_constr loc c bl) + | LocalRawAssum (nal,t)::bl -> + let loc' = join_loc (fst (List.hd nal)) loc in + CLambdaN(loc', [nal, t], abstract_constr loc c bl) + +(* Hack to parse "(n)" as nat without conflicts with the (useless) *) +(* admissible notation "(n)" *) +let test_int_rparen = + Gram.Entry.of_parser "test_int_rparen" + (fun strm -> + match Stream.npeek 1 strm with + | [("INT", _)] -> + begin match Stream.npeek 2 strm with + | [_; ("", ")")] -> () + | _ -> raise Stream.Failure + end + | _ -> raise Stream.Failure) + +(* Hack to parse "n" at level 0 without conflicting with "n!" at level 91 *) +(* admissible notation "(n)" *) +let test_int_bang = + Gram.Entry.of_parser "test_int_bang" + (fun strm -> + match Stream.npeek 1 strm with + | [("INT", n)] -> + begin match Stream.npeek 2 strm with + | [_; ("", "!")] -> () + | _ -> raise Stream.Failure + end + | _ -> raise Stream.Failure) + +(* Hack to parse "`id:...`" at level 0 without conflicting with + "`...`" from ZArith *) +let test_ident_colon = + Gram.Entry.of_parser "test_ident_colon" + (fun strm -> + match Stream.npeek 1 strm with + | [("IDENT", _)] -> + begin match Stream.npeek 2 strm with + | [_; ("", ":")] -> () + | _ -> raise Stream.Failure + end + | _ -> raise Stream.Failure) + + +if !Options.v7 then +GEXTEND Gram + GLOBAL: operconstr lconstr constr sort global constr_pattern Constr.ident annot + (*ne_name_comma_list*); + Constr.ident: + [ [ id = Prim.ident -> id + + (* This is used in quotations and Syntax *) + | id = METAIDENT -> id_of_string id ] ] + ; + global: + [ [ r = Prim.reference -> r + + (* This is used in quotations *) + | id = METAIDENT -> Ident (loc,id_of_string id) ] ] + ; + constr_pattern: + [ [ c = constr -> c ] ] + ; + ne_constr_list: + [ [ cl = LIST1 constr -> cl ] ] + ; + sort: + [ [ "Set" -> RProp Pos + | "Prop" -> RProp Null + | "Type" -> RType None ] ] + ; + constr: + [ [ c = operconstr LEVEL "8" -> c ] ] + ; + lconstr: + [ [ c = operconstr LEVEL "10" -> c ] ] + ; + operconstr: + [ "10" RIGHTA + [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") -> + CAppExpl (loc, (None,f), args) +(* + | "!"; f = global; "with"; b = binding_list -> + <:ast< (APPLISTWITH $f $b) >> +*) + | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ] + | "9" RIGHTA + [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ] + | "8" RIGHTA + [ c1 = operconstr; "->"; c2 = operconstr LEVEL "8"-> CArrow (loc, c1, c2) ] + | "1" RIGHTA + [ "<"; p = annot; ">"; IDENT "Match"; c = constr; "with"; + cl = LIST0 constr; "end" -> + COrderedCase (loc, MatchStyle, Some p, c, cl) + | "<"; p = annot; ">"; IDENT "Case"; c = constr; "of"; + cl = LIST0 constr; "end" -> + COrderedCase (loc, RegularStyle, Some p, c, cl) + | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" -> + COrderedCase (loc, RegularStyle, None, c, cl) + | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" -> + COrderedCase (loc, MatchStyle, None, c, cl) + | IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; + c = constr; "in"; c1 = constr -> + (* TODO: right loc *) + COrderedCase + (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)]) + | IDENT "let"; na = name; "="; c = opt_casted_constr; + "in"; c1 = constr -> + CLetIn (loc, na, c, c1) + | IDENT "if"; c1 = constr; + IDENT "then"; c2 = constr; + IDENT "else"; c3 = constr -> + COrderedCase (loc, IfStyle, None, c1, [c2; c3]) + | "<"; p = annot; ">"; + IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; + "in"; c1 = constr -> + (* TODO: right loc *) + COrderedCase (loc, LetStyle, Some p, c, + [CLambdaN (loc, [b, CHole loc], c1)]) + | "<"; p = annot; ">"; + IDENT "if"; c1 = constr; + IDENT "then"; c2 = constr; + IDENT "else"; c3 = constr -> + COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) + | ".."; c = operconstr LEVEL "0"; ".." -> + CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] + | "0" RIGHTA + [ "?" -> CHole loc + | "?"; n = Prim.natural -> CPatVar (loc, (false,Pattern.patvar_of_int n)) + | bll = binders; c = constr -> abstract_constr loc c bll + (* Hack to parse syntax "(n)" as a natural number *) + | "("; test_int_rparen; n = bigint; ")" -> + (* Delimiter "N" moved to "nat" in V7 *) + CDelimiters (loc,"nat",CNumeral (loc,n)) + | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_tail -> + let id = coerce_to_name lc1 in + CProdN (loc, ([id], c)::bl, body) +(* TODO: Syntaxe (_:t...)t et (_,x...)t *) + | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; + (bl,body) = product_tail -> + let id1 = coerce_to_name lc1 in + let id2 = coerce_to_name lc2 in + CProdN (loc, ([id1; id2], c)::bl, body) + | "("; lc1 = lconstr; ","; lc2 = lconstr; ","; + idl = ne_name_comma_list; ":"; c = constr; (bl,body) = product_tail -> + let id1 = coerce_to_name lc1 in + let id2 = coerce_to_name lc2 in + CProdN (loc, (id1::id2::idl, c)::bl, body) + | "("; lc1 = lconstr; ")" -> + if Options.do_translate() then set_loc loc lc1 else lc1 + | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> + (match lc1 with + | CPatVar (loc2,(false,n)) -> + CApp (loc,(None,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) + | _ -> + Util.error "Second-order pattern-matching expects a head metavariable") + | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" -> + CFix (loc, id, fbinders) + | IDENT "CoFix"; id = identref; "{"; fbinders = cofixbinders; "}" -> + CCoFix (loc, id, fbinders) + | IDENT "Prefix" ; "(" ; s = STRING ; cl = LIST0 constr ; ")" -> + CNotation(loc, s, cl) + | s = sort -> CSort (loc, s) + | v = global -> CRef v + | n = bigint -> CNumeral (loc,n) + | "!"; f = global -> CAppExpl (loc,(None,f),[]) + | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> + (* Delimiter "N" implicitly moved to "nat" in V7 *) + let key = if key = "N" then "nat" else key in + let key = if key = "P" then "positive" else key in + let key = if key = "T" then "type" else key in + CDelimiters (loc,key,c) ] ] + ; + constr91: + [ [ test_int_bang; n = INT; "!"; c = operconstr LEVEL "9" -> + (c, Some (loc,ExplByPos (int_of_string n))) + | c = operconstr LEVEL "9" -> (c, None) ] ] + ; + (* annot and product_annot_tail are hacks to forbid concrete syntax *) + (* ">" (e.g. for gt, Zgt, ...) in annotations *) + annot: + [ RIGHTA + [ bll = binders; c = annot -> abstract_constr loc c bll + | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_annot_tail -> + let id = coerce_to_name lc1 in + CProdN (loc, ([id], c)::bl, body) + | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; + (bl,body) = product_annot_tail -> + let id1 = coerce_to_name lc1 in + let id2 = coerce_to_name lc2 in + CProdN (loc, ([id1; id2], c)::bl, body) + | "("; lc1 = lconstr; ","; lc2 = lconstr; ","; + idl = ne_name_comma_list; ":"; c = constr; + (bl,body) = product_annot_tail -> + let id1 = coerce_to_name lc1 in + let id2 = coerce_to_name lc2 in + CProdN (loc, (id1::id2::idl, c)::bl, body) + | "("; lc1 = lconstr; ")" -> lc1 + | c1 = annot; "->"; c2 = annot -> CArrow (loc, c1, c2) ] + | RIGHTA + [ c1 = annot; "\\/"; c2 = annot -> CNotation (loc, "_ \\/ _", [c1;c2]) ] + | RIGHTA + [ c1 = annot; "/\\"; c2 = annot -> CNotation (loc, "_ /\\ _", [c1;c2]) ] + | RIGHTA + [ "~"; c = SELF -> CNotation (loc, "~ _", [c]) ] + | RIGHTA + [ c1 = SELF; "=="; c2 = NEXT -> CNotation (loc, "_ == _", [c1;c2]) ] + | RIGHTA + [ c1 = SELF; "="; c2 = NEXT -> CNotation (loc, "_ = _", [c1;c2]) ] + | [ c = operconstr LEVEL "4L" -> c ] ] + ; + product_annot_tail: + [ [ ";"; idl = ne_name_comma_list; ":"; c = constr; + (bl,c2) = product_annot_tail -> ((idl, c)::bl, c2) + | ";"; idl = ne_name_comma_list; (bl,c2) = product_annot_tail -> + ((idl, CHole (fst (List.hd idl)))::bl, c2) + | ")"; c = annot -> ([], c) ] ] + ; + ne_name_comma_list: + [ [ nal = LIST1 name SEP "," -> nal ] ] + ; + name_comma_list_tail: + [ [ ","; idl = ne_name_comma_list -> idl + | -> [] ] ] + ; + opt_casted_constr: + [ [ c = constr; ":"; t = constr -> CCast (loc, c, t) + | c = constr -> c ] ] + ; + vardecls: + [ [ na = name; nal = name_comma_list_tail; c = type_option -> + LocalRawAssum (na::nal,c) + | na = name; "="; c = opt_casted_constr -> + LocalRawDef (na, c) + | na = name; ":="; c = opt_casted_constr -> + LocalRawDef (na, c) + + (* This is used in quotations *) + | id = METAIDENT; c = type_option -> LocalRawAssum ([loc, Name (id_of_string id)], c) + ] ] + ; + ne_vardecls_list: + [ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl + | id = vardecls -> [id] ] ] + ; + binders: + [ [ "["; bl = ne_vardecls_list; "]" -> bl ] ] + ; + simple_params: + [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c) + | idl = LIST1 name SEP "," -> (idl, CHole loc) + ] ] + ; + simple_binders: + [ [ "["; bll = LIST1 simple_params SEP ";"; "]" -> bll ] ] + ; + ne_simple_binders_list: + [ [ bll = LIST1 simple_binders -> List.flatten bll ] ] + ; + type_option: + [ [ ":"; c = constr -> c + | -> CHole loc ] ] + ; + fixbinder: + [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr; + ":="; def = constr -> + (id, recarg-1, [], type_, def) + | id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr; + ":="; def = constr -> + let ni = List.length (List.flatten (List.map fst bl)) -1 in + let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in + (id, ni, bl, type_, def) ] ] + ; + fixbinders: + [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ] + ; + cofixbinder: + [ [ id = base_ident; ":"; type_ = constr; ":="; def = constr -> + (id, [],type_, def) ] ] + ; + cofixbinders: + [ [ fbs = LIST1 cofixbinder SEP "with" -> fbs ] ] + ; + product_tail: + [ [ ";"; idl = ne_name_comma_list; ":"; c = constr; + (bl,c2) = product_tail -> ((idl, c)::bl, c2) + | ";"; idl = ne_name_comma_list; (bl,c2) = product_tail -> + ((idl, CHole (fst (List.hd idl)))::bl, c2) + | ")"; c = constr -> ([], c) ] ] + ; +END;; |