programs: avoid clashes between theories and modules

parent 362c5cb9
module M
use import module ref.Ref
let foo (x : ref int) (y: ref int) =
x := 1;
y := 2
val r : ref int
let rec test () =
foo r r
end
(* a theory is not a module *)
theory T
end
module M
use import module T
end
(* a module is not a theory *)
module M
end
module M1
use import M
end
......@@ -937,9 +937,9 @@ list1_theory_or_module_:
theory_or_module_:
| THEORY uident labels list0_full_decl END
{ { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
{ Ptheory { pth_name = add_lab $2 $3; pth_decl = $4; } }
| MODULE uident labels list0_program_decl END
{ { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
{ Pmodule { mod_name = add_lab $2 $3; mod_decl = $4; } }
;
list0_full_decl:
......
......@@ -245,11 +245,19 @@ type program_decl =
| Duse of qualid * imp_exp * (*as:*) ident option
| Dnamespace of loc * ident option * (* import: *) bool * program_decl list
type theory = {
pth_name : ident;
pth_decl : program_decl list;
}
type module_ = {
mod_name : ident;
mod_labels : label list;
mod_decl : program_decl list;
}
type program_file = module_ list
type theory_module =
| Ptheory of theory
| Pmodule of module_
type program_file = theory_module list
......@@ -24,6 +24,7 @@ open Why3
open Util
open Ident
open Theory
open Typing
open Ptree
open Pgm_module
......@@ -33,6 +34,22 @@ let () = Exn_printer.register (fun fmt e -> match e with
| ClashModule m -> fprintf fmt "clash with previous module %s" m
| _ -> raise e)
let add_theory env lenv m =
let id = m.pth_name in
let loc = id.id_loc in
let th = Theory.create_theory (Denv.create_user_id id) in
let rec add_decl th = function
| Dlogic d ->
Typing.add_decl env lenv th d
| Dnamespace (loc, name, import, dl) ->
let th = Theory.open_namespace th in
let th = List.fold_left add_decl th dl in
Typing.close_namespace loc import name th
| Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ -> assert false
in
let th = List.fold_left add_decl th m.pth_decl in
close_theory loc lenv th
let add_module ?(type_only=false) env penv (ltm, lmod) m =
let id = m.mod_name in
let loc = id.id_loc in
......@@ -44,9 +61,13 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m =
let uc =
List.fold_left (Pgm_typing.decl ~wp env penv ltm lmod) uc m.mod_decl
in
let m = close_module uc in
Mstr.add id.id m.m_pure ltm,
Mstr.add id.id m lmod
let md = close_module uc in
Mstr.add ("WP " ^ id.id) md.m_pure ltm, (* avoids a theory/module clash *)
Mstr.add id.id md lmod
let add_theory_module ?(type_only=false) env penv (ltm, lmod) = function
| Ptheory t -> add_theory env ltm t, lmod
| Pmodule m -> add_module ~type_only env penv (ltm, lmod) m
let retrieve penv file c =
let lb = Lexing.from_channel c in
......@@ -57,7 +78,7 @@ let retrieve penv file c =
else
let type_only = Debug.test_flag Typing.debug_type_only in
let env = Pgm_env.get_env penv in
List.fold_left (add_module ~type_only env penv)
List.fold_left (add_theory_module ~type_only env penv)
(Mstr.empty, Mstr.empty) ml
let pgm_env_of_env =
......
......@@ -295,8 +295,8 @@ let rec dtype ~user env = function
let mt = get_mtsymbol ts in
let np = List.length p in
if np <> a - mt.mt_regions then
errorm ~loc "@[the type %a expects %d argument(s),@
but is applied to %d argument(s)@]"
errorm ~loc
"@[type %a expects %d argument(s),@ but is applied to %d argument(s)@]"
print_qualid x (a - mt.mt_regions) np;
let tyl = List.map (dtype ~user env) p in
let tyl = create_regions ~user mt.mt_regions @ tyl in
......
theory M1
type t 'a = {| a : 'a |}
end
module M2
use import M1
let f (x: t int) = x.a
end
(*
module MutualRec
......@@ -15,28 +23,6 @@ module MutualRec
end
*)
(*
module PoorArrays
use import int.Int
use import module ref.Ref
use import map.Map as M
type array_contents 'a = {| length: int; elts : map int 'a |}
type array 'a = ref (array_contents 'a)
val get (a: array 'a) (i: int) :
{ 0 <= i < length !a } 'a { result = M.get !a.elts i }
val set (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length !a }
unit writes a
{ !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v }
end
*)
(*
module M
use import int.Int
......@@ -60,8 +46,6 @@ module M
(* let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end *)
end
*)
(*
Local Variables:
......
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