Commit c23ddb9d authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: toplevel "import <scope>" declaration

parent ce54f49f
......@@ -79,6 +79,8 @@ syn region whyNone matchgroup=whyKeyword start="\<\(use\|clone\)\>" matchgroup
syn keyword whyExport contained export
syn keyword whyImport contained import
syn region whyNone matchgroup=whyKeyword start="\<import\>" matchgroup=whyModSpec end="\<\(\u\(\w\|'\)*\.\)*\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
syn keyword whyKeyword as by constant
......
......@@ -177,7 +177,7 @@
%left OP3
%left OP4
%nonassoc prec_prefix_op
%nonassoc INTEGER REAL
%nonassoc INTEGER REAL (* stronger than MINUS *)
%nonassoc LEFTSQ
%nonassoc OPPREF
......@@ -210,6 +210,8 @@ scope_head:
module_decl:
| scope_head module_decl* END
{ Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
| IMPORT uqualid
{ Typing.import_scope (floc $startpos $endpos) $2 }
| d = pure_decl | d = prog_decl | d = meta_decl
{ Typing.add_decl (floc $startpos $endpos) d }
| use_clone { () }
......
......@@ -1249,6 +1249,14 @@ let close_scope loc ~import =
let muc = Loc.try1 ~loc (close_scope ~import) (Opt.get slice.muc) in
slice.muc <- Some muc
let import_scope loc q =
assert (not (Stack.is_empty state));
let slice = Stack.top state in
let muc = top_muc_on_demand loc slice in
if Debug.test_noflag debug_parse_only then
let muc = Loc.try2 ~loc import_scope muc (string_list_of_qualid q) in
slice.muc <- Some muc
let add_decl loc d =
assert (not (Stack.is_empty state));
let slice = Stack.top state in
......
......@@ -25,4 +25,6 @@ val open_scope : Loc.position -> Ptree.ident -> unit
val close_scope : Loc.position -> import:bool -> unit
val import_scope : Loc.position -> Ptree.qualid -> unit
val add_decl : Loc.position -> Ptree.decl -> unit
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment