Commit ebfad25c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

namespaces in modules

parent 479ade45
......@@ -64,6 +64,7 @@
"let", LET;
"match", MATCH;
"module", MODULE;
"namespace", NAMESPACE;
"not", NOT;
"of", OF;
"parameter", PARAMETER;
......
......@@ -96,6 +96,7 @@ let create_module n =
let open_namespace uc = match uc.uc_import with
| ns :: _ -> { uc with
uc_th = Theory.open_namespace uc.uc_th;
uc_import = ns :: uc.uc_import;
uc_export = empty_ns :: uc.uc_export; }
| [] -> assert false
......@@ -109,7 +110,8 @@ let close_namespace uc import s =
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
let e1 = match s with Some s -> add_ns true s e0 e1 | _ -> e1 in
{ uc with uc_import = i1 :: sti; uc_export = e1 :: ste; }
let th = Theory.close_namespace uc.uc_th import s in
{ uc with uc_th = th; uc_import = i1 :: sti; uc_export = e1 :: ste; }
| [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
......
......@@ -118,7 +118,8 @@
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO ELSE END
%token EXCEPTION EXPORT FOR
%token FUN GHOST IF IMPORT IN INVARIANT LABEL LET MATCH MODULE NOT OF PARAMETER
%token FUN GHOST IF IMPORT IN INVARIANT LABEL LET MATCH MODULE
%token NAMESPACE NOT OF PARAMETER
%token RAISE RAISES READS REC
%token THEN TO TRY TYPE USE VARIANT WHILE WITH WRITES
......@@ -231,6 +232,8 @@ decl:
{ Dexn (add_lab $2 $3, Some $5) }
| USE MODULE use
{ $3 }
| NAMESPACE opt_import uident list0_decl END
{ Dnamespace ($3, $2, $4) }
;
use:
......@@ -246,6 +249,11 @@ imp_exp:
| /* epsilon */ { Nothing }
;
opt_import:
| /* epsilon */ { false }
| IMPORT { true }
;
list1_recfun_sep_and:
| recfun { [ $1 ] }
| recfun AND list1_recfun_sep_and { $1 :: $3 }
......
......@@ -108,7 +108,8 @@ type decl =
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
(* modules *)
| Duse of qualid * Ptree.imp_exp * (*as*) ident option
| Duse of qualid * Ptree.imp_exp * (*as:*) ident option
| Dnamespace of ident * (* import: *) bool * decl list
type module_ = {
mod_name : ident;
......
......@@ -1315,7 +1315,7 @@ let find_module lmod q id = match q with
(* env = to retrieve theories from the loadpath
lmod = local modules *)
let decl env lmod uc = function
let rec decl env lmod uc = function
| Pgm_ptree.Dlogic dl ->
Pgm_module.parse_logic_decls env dl uc
| Pgm_ptree.Dlet (id, e) ->
......@@ -1380,8 +1380,15 @@ let decl env lmod uc = function
close_namespace uc true n
| Export ->
use_export uc m
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s
with ClashSymbol s ->
errorm ~loc "clash with previous symbol %s" s
end
| Pgm_ptree.Dnamespace (id, import, dl) ->
let loc = id.id_loc in
let uc = open_namespace uc in
let uc = List.fold_left (decl env lmod) uc dl in
begin try close_namespace uc import (Some id.id)
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
(*
Local Variables:
......
......@@ -3,7 +3,9 @@
theory Test
use import list.List
namespace N
use import list.List
end
logic p (list 'a)
......
......@@ -15,16 +15,19 @@ end
module P
{ use import programs.Prelude
use import list.List }
{ use import programs.Prelude }
use module import A as B
{ logic n : int }
let f x = x + B.f 2
namespace N
{ use import list.List }
{ logic c : list int }
let h (x:int) = Cons x c
end
let g x = { x >= 0 } f (x+2) { result >= 0 }
let g x = { x >= 0 } N.c { true }
end
......
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