diff options
Diffstat (limited to 'parsing/g_module.ml4')
| -rw-r--r-- | parsing/g_module.ml4 | 66 |
1 files changed, 11 insertions, 55 deletions
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 index 56db0cb59..a3714c43b 100644 --- a/parsing/g_module.ml4 +++ b/parsing/g_module.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - (* $Id$ *) open Pp @@ -16,75 +14,33 @@ open Pcoq open Prim open Module open Util +open Topconstr (* Grammar rules for module expressions and types *) GEXTEND Gram - GLOBAL: ne_binders_list module_expr - module_type; + GLOBAL: module_expr module_type; - ident: - [ [ id = Prim.var -> id ] ] - ; - - ident_comma_list_tail: - [ [ ","; idl = LIST0 ident SEP "," -> idl - | -> [] ] ] - ; - - qualid: - [ [ id = Prim.var; l = fields -> <:ast< (QUALID $id ($LIST $l)) >> - | id = Prim.var -> <:ast< (QUALID $id) >> - ] ] - ; - fields: - [ [ id = FIELD; l = fields -> <:ast< ($VAR $id) >> :: l - | id = FIELD -> [ <:ast< ($VAR $id) >> ] - ] ] - ; - - vardecls: (* This is interpreted by Pcoq.abstract_binder *) - [ [ id = ident; idl = ident_comma_list_tail; - ":"; mty = module_type -> - <:ast< (BINDER $mty $id ($LIST $idl)) >> ] ] - ; - - ne_vardecls_list: - [ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl - | id = vardecls -> [id] ] ] - ; - - rawbinders: - [ [ "["; bl = ne_vardecls_list; "]" -> bl ] ] - ; - - ne_binders_list: - [ [ bl = rawbinders; bll = ne_binders_list -> bl @ bll - | bl = rawbinders -> bl ] ] - ; - module_expr: - [ [ qid = qualid -> <:ast< (MODEXPRQID $qid) >> - | me1 = module_expr; me2 = module_expr -> - <:ast< (MODEXPRAPP $me1 $me2) >> - | "("; me = module_expr; ")" -> - me + [ [ qid = qualid -> CMEident qid + | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2) + | "("; me = module_expr; ")" -> me (* ... *) ] ] ; with_declaration: - [ [ "Definition"; id = ident; ":="; c = Constr.constr -> - <:ast< (WITHDEFINITION $id $c) >> - | IDENT "Module"; id = ident; ":="; qid = qualid -> - <:ast< (WITHMODULE $id $qid) >> + [ [ "Definition"; id = base_ident; ":="; c = Constr.constr -> + CWith_Definition (id,c) + | IDENT "Module"; id = base_ident; ":="; qid = qualid -> + CWith_Module (id,qid) ] ] ; module_type: - [ [ qid = qualid -> <:ast< (MODTYPEQID $qid) >> + [ [ qid = qualid -> CMTEident qid (* ... *) | mty = module_type; "with"; decl = with_declaration -> - <:ast< (MODTYPEWITH $mty $decl)>> ] ] + CMTEwith (mty,decl) ] ] ; END |