diff options
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 144 |
1 files changed, 50 insertions, 94 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index ce6d4e2f..d5ca5e0c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -6,133 +6,89 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: g_prim.ml4,v 1.22.2.2 2004/07/16 19:30:39 herbelin Exp $ i*) +(*i $Id: g_prim.ml4 7922 2006-01-23 19:11:11Z herbelin $ i*) -open Coqast open Pcoq open Names open Libnames open Topconstr -open Prim -let _ = reset_all_grammars() +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] +let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw +open Prim open Nametab -let local_id_of_string = id_of_string -let local_make_dirpath = make_dirpath -let local_make_qualid l id' = make_qualid (local_make_dirpath l) id' -let local_make_short_qualid id = make_short_qualid id -let local_make_posint = int_of_string -let local_make_negint n = - int_of_string n -let local_make_path l a = encode_kn (local_make_dirpath l) a -let local_make_binding loc a b = - match a with - | Nvar (_,id) -> Slam(loc,Some id,b) - | Nmeta (_,s) -> Smetalam(loc,s,b) - | _ -> failwith "Slam expects a var or a metavar" -let local_append l id = l@[id] -GEXTEND Gram - GLOBAL: ident natural integer bigint string preident ast - astlist qualid reference dirpath identref name base_ident var hyp; +let local_make_qualid l id = make_qualid (make_dirpath l) id - (* Compatibility: Prim.var is a synonym of Prim.ident *) - var: - [ [ id = ident -> id ] ] - ; - hyp: - [ [ id = ident -> id ] ] - ; - metaident: - [ [ s = METAIDENT -> Nmeta (loc,s) ] ] - ; +GEXTEND Gram + GLOBAL: + bigint natural integer identref name ident var preident + fullyqualid qualid reference dirpath + ne_string string; preident: [ [ s = IDENT -> s ] ] ; - base_ident: - [ [ s = IDENT -> local_id_of_string s ] ] - ; - name: - [ [ IDENT "_" -> (loc, Anonymous) - | id = base_ident -> (loc, Name id) ] ] - ; - identref: - [ [ id = base_ident -> (loc,id) ] ] - ; ident: - [ [ id = base_ident -> id ] ] + [ [ s = IDENT -> id_of_string s ] ] ; - natural: - [ [ i = INT -> local_make_posint i ] ] + var: (* as identref, but interpret as a term identifier in ltac *) + [ [ id = ident -> (loc,id) ] ] ; - bigint: - [ [ i = INT -> Bignat.POS (Bignat.of_string i) - | "-"; i = INT -> Bignat.NEG (Bignat.of_string i) ] ] - ; - integer: - [ [ i = INT -> local_make_posint i - | "-"; i = INT -> local_make_negint i ] ] + identref: + [ [ id = ident -> (loc,id) ] ] ; field: - [ [ s = FIELD -> local_id_of_string s ] ] - ; - dirpath: - [ [ id = base_ident; l = LIST0 field -> - local_make_dirpath (local_append l id) ] ] + [ [ s = FIELD -> id_of_string s ] ] ; fields: - [ [ id = field; (l,id') = fields -> (local_append l id,id') + [ [ id = field; (l,id') = fields -> (l@[id],id') | id = field -> ([],id) ] ] ; + fullyqualid: + [ [ id = ident; (l,id')=fields -> loc,id::List.rev (id'::l) + | id = ident -> loc,[id] + ] ] + ; basequalid: - [ [ id = base_ident; (l,id')=fields -> local_make_qualid (local_append l id) id' - | id = base_ident -> local_make_short_qualid id + [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' + | id = ident -> make_short_qualid id ] ] ; - qualid: - [ [ qid = basequalid -> loc, qid ] ] + name: + [ [ IDENT "_" -> (loc, Anonymous) + | id = ident -> (loc, Name id) ] ] ; reference: - [ [ id = base_ident; (l,id') = fields -> - Qualid (loc, local_make_qualid (local_append l id) id') - | id = base_ident -> Ident (loc,id) + [ [ id = ident; (l,id') = fields -> + Qualid (loc, local_make_qualid (l@[id]) id') + | id = ident -> Ident (loc,id) ] ] ; + qualid: + [ [ qid = basequalid -> loc, qid ] ] + ; + ne_string: + [ [ s = STRING -> + if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s + ] ] + ; + dirpath: + [ [ id = ident; l = LIST0 field -> + make_dirpath (l@[id]) ] ] + ; string: [ [ s = STRING -> s ] ] ; - astpath: - [ [ id = base_ident; (l,a) = fields -> - Path(loc, local_make_path (local_append l id) a) - | id = base_ident -> Nvar(loc, id) - ] ] + integer: + [ [ i = INT -> int_of_string i + | "-"; i = INT -> - int_of_string i ] ] ; - (* ast *) - ast: - [ [ id = metaident -> id - | p = astpath -> p - | s = INT -> Num(loc, local_make_posint s) - | s = STRING -> Str(loc, s) - | "{"; s = METAIDENT; "}" -> Id(loc,s) - | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l) - | "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id]) - | "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id]) - | "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id]) - | "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id]) - | "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l) - | "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id]) - | "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id]) - | "["; "<>"; "]"; b = ast -> Slam(loc,None,b) - | "["; a = ast; "]"; b = ast -> local_make_binding loc a b - -(* - | "["; ido = astidoption; "]"; b = ast -> Slam(loc,ido,b) - | "["; id = METAIDENT; "]"; b = ast -> Smetalam(loc,id,b) -*) - | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ] - ; - astlist: - [ [ l = LIST0 ast -> l ] ] + natural: + [ [ i = INT -> int_of_string i ] ] + ; + bigint: (* Negative numbers are dealt with specially *) + [ [ i = INT -> (Bigint.of_string i) ] ] ; END |