diff options
Diffstat (limited to 'parsing/g_primnew.ml4')
-rw-r--r-- | parsing/g_primnew.ml4 | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4 new file mode 100644 index 00000000..c1875634 --- /dev/null +++ b/parsing/g_primnew.ml4 @@ -0,0 +1,84 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: g_primnew.ml4,v 1.4.2.2 2004/07/16 19:30:39 herbelin Exp $ i*) + +open Coqast +open Pcoq +open Names +open Libnames +open Topconstr + +let _ = + if not !Options.v7 then + Pcoq.reset_all_grammars() +let _ = + if not !Options.v7 then + let f = Gram.Unsafe.clear_entry in + f Prim.bigint; + f Prim.qualid; + f Prim.ast; + f Prim.reference + +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"] +let _ = + if not !Options.v7 then + 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] + +if not !Options.v7 then +GEXTEND Gram + GLOBAL: bigint qualid reference ne_string; + field: + [ [ s = FIELD -> local_id_of_string s ] ] + ; + fields: + [ [ id = field; (l,id') = fields -> (local_append l id,id') + | id = field -> ([],id) + ] ] + ; + basequalid: + [ [ id = base_ident; (l,id')=fields -> + local_make_qualid (local_append l id) id' + | id = base_ident -> local_make_short_qualid id + ] ] + ; + reference: + [ [ id = base_ident; (l,id') = fields -> + Qualid (loc, local_make_qualid (local_append l id) id') + | id = base_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 + ] ] + ; + bigint: (* Negative numbers are dealt with specially *) + [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ] + ; +END |