Commit 6fae2d4a authored by Mário Pereira's avatar Mário Pereira

Multiple "use": multiple module names allowed after "use". For instance:

  use int.Int, set.Fset, ref.Ref
  (as updated in the pigeonhole.mlw file)

Any module name can be followed by a "as M" clause, but only a single "import"
is allowed. For instance:

  use import int.Int as I, map.Map as M

imports both Int and Map. To import Int but not Map, one would have to write

  use import int.Int as I
  use map.Map as M
parent 8681df7d
...@@ -5,9 +5,7 @@ ...@@ -5,9 +5,7 @@
module Pigeonhole module Pigeonhole
use int.Int use int.Int, set.Fset, ref.Ref
use set.Fset
use ref.Ref
let rec below (n: int) : set int let rec below (n: int) : set int
requires { 0 <= n } requires { 0 <= n }
......
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -267,14 +267,16 @@ use_clone: ...@@ -267,14 +267,16 @@ use_clone:
{ Typing.add_decl (floc $startpos $endpos) (Duse $3) } { Typing.add_decl (floc $startpos $endpos) (Duse $3) }
| CLONE EXPORT tqualid clone_subst | CLONE EXPORT tqualid clone_subst
{ Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) } { Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
| USE boption(IMPORT) tqualid option(preceded(AS, uident)) | USE boption(IMPORT) m_as_list = comma_list1(use_as)
{ let loc = floc $startpos $endpos in { let loc = floc $startpos $endpos in
if $2 && $4 = None then Warning.emit ~loc let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
if $2 && not exists_as then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted"; "the keyword `import' is redundant here and can be omitted";
let import = $2 || $4 = None in let add_import (m, q) = let import = $2 || q = None in
Typing.open_scope loc (use_as $3 $4); Typing.open_scope loc (use_as m q);
Typing.add_decl loc (Duse $3); Typing.add_decl loc (Duse m);
Typing.close_scope loc ~import } Typing.close_scope loc ~import in
List.iter add_import m_as_list }
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
{ let loc = floc $startpos $endpos in { let loc = floc $startpos $endpos in
if $2 && $4 = None then Warning.emit ~loc if $2 && $4 = None then Warning.emit ~loc
...@@ -284,6 +286,9 @@ use_clone: ...@@ -284,6 +286,9 @@ use_clone:
Typing.add_decl loc (Dclone ($3, $5)); Typing.add_decl loc (Dclone ($3, $5));
Typing.close_scope loc ~import } Typing.close_scope loc ~import }
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }
clone_subst: clone_subst:
| (* epsilon *) { [] } | (* epsilon *) { [] }
| WITH comma_list1(single_clone_subst) { $2 } | WITH comma_list1(single_clone_subst) { $2 }
......
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