programs env: work in progress (does not even compile)

parent 9cd84f51
......@@ -282,7 +282,7 @@ PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
pgm_types pgm_module pgm_wp pgm_typing pgm_main # pgm_env
pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
......@@ -74,9 +74,11 @@ let find_theory env sl s =
else try Mnm.find s (find_library env sl)
with Not_found -> raise (TheoryNotFound (sl, s))
let find_channel env = env.env_ret_chan
let env_tag env = env.env_tag
(* module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end) *)
module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
(** Parsers *)
......
......@@ -25,7 +25,7 @@ type env
val env_tag : env -> Hashweak.tag
(* module Wenv : Hashweak.S with type key = env *)
module Wenv : Hashweak.S with type key = env
type retrieve_channel = string list -> in_channel
......@@ -39,6 +39,8 @@ val find_theory : env -> string list -> string -> theory
(** [find_theory e p n] finds the theory named [p.n] in environment [e]
@raise TheoryNotFound if theory not present in env [e] *)
val find_channel : env -> string list -> in_channel
(** Parsers *)
type read_channel = env -> string -> in_channel -> theory Mnm.t
......
open Why
open Util
open Ident
open Theory
open Term
open Ty
module E = Pgm_effect
open Pgm_module
(* environments *)
type env = {
uc : theory_uc;
(***
globals : type_v Mls.t;
locals : type_v Mvs.t;
***)
globals : (lsymbol * type_v) Mstr.t;
exceptions : lsymbol Mstr.t;
ts_arrow: tysymbol;
ts_bool : tysymbol;
ts_label: tysymbol;
ts_ref: tysymbol;
ts_exn: tysymbol;
ts_unit : tysymbol;
ls_at : lsymbol;
ls_bang : lsymbol;
ls_old : lsymbol;
ls_True : lsymbol;
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
ls_lt : lsymbol;
ls_gt : lsymbol;
ls_le : lsymbol;
ls_ge : lsymbol;
ls_add : lsymbol;
type t = {
env : Env.env;
retrieve : retrieve_module;
memo : (string list, Pgm_module.t Mnm.t) Hashtbl.t;
}
and retrieve_module = t -> in_channel -> Pgm_module.t Mnm.t
(* prelude *)
let find_ts uc = ns_find_ts (get_namespace uc)
let find_ls uc = ns_find_ls (get_namespace uc)
(* predefined lsymbols are memoized wrt the lsymbol for type "ref" *)
let memo_ls f =
let h = Hts.create 17 in
fun uc ->
let ts_ref = find_ts uc ["ref"] in
try Hts.find h ts_ref
with Not_found -> let s = f uc ts_ref in Hts.add h ts_ref s; s
(* logic ref ('a) : 'a ref *)
let ls_ref = memo_ls
(fun _uc ts_ref ->
let a = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "ref") [a] (Some (ty_app ts_ref [a])))
(* logic (:=)('a ref, 'a) : unit *)
let ls_assign = memo_ls
(fun uc ts_ref ->
let ty_unit = ty_app (find_ts uc ["unit"]) [] in
let a = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "infix :=") [ty_app ts_ref [a]; a] (Some ty_unit))
let ls_Exit = memo_ls
(fun uc _ ->
let ty_exn = ty_app (find_ts uc ["exn"]) [] in
create_lsymbol (id_fresh "%Exit") [] (Some ty_exn))
let add_type_v_ref uc m =
let ts_ref = find_ts uc ["ref"] in
let a = ty_var (create_tvsymbol (id_fresh "a")) in
let x = create_vsymbol (id_fresh "x") a in
let ty = ty_app ts_ref [a] in
let result = v_result ty in
let q = f_equ (t_app (find_ls uc ["prefix !"]) [t_var result] a) (t_var x) in
let c = { c_result_type = Tpure ty;
c_effect = Pgm_effect.empty;
c_pre = f_true;
c_post = (result, q), []; } in
let v = Tarrow ([x, Tpure a], c) in
Mstr.add "ref" (ls_ref uc, v) m
let get_env penv = penv.env
let add_type_v_assign uc m =
let ts_ref = find_ts uc ["ref"] in
let a = ty_var (create_tvsymbol (id_fresh "a")) in
let a_ref = ty_app ts_ref [a] in
let x = create_vsymbol (id_fresh "x") a_ref in
let y = create_vsymbol (id_fresh "y") a in
let ty = ty_app (find_ts uc ["unit"]) [] in
let result = v_result ty in
let q = f_equ (t_app (find_ls uc ["prefix !"]) [t_var x] a) (t_var y) in
let c = { c_result_type = Tpure ty;
c_effect = E.add_write (E.Rlocal x) E.empty;
c_pre = f_true;
c_post = (result, q), []; } in
let v = Tarrow ([x, Tpure a_ref; y, Tpure a], c) in
Mstr.add "infix :=" (ls_assign uc, v) m
let empty_env uc = {
uc = uc;
globals = add_type_v_ref uc (add_type_v_assign uc Mstr.empty);
exceptions = Mstr.add "%Exit" (ls_Exit uc) Mstr.empty;
(* types *)
ts_arrow = find_ts uc ["arrow"];
ts_bool = find_ts uc ["bool"];
ts_label = find_ts uc ["label"];
ts_ref = find_ts uc ["ref"];
ts_exn = find_ts uc ["exn"];
ts_unit = find_ts uc ["tuple0"];
(* functions *)
ls_at = find_ls uc ["at"];
ls_bang = find_ls uc ["prefix !"];
ls_old = find_ls uc ["old"];
ls_True = find_ls uc ["True"];
ls_False = find_ls uc ["False"];
ls_andb = find_ls uc ["andb"];
ls_orb = find_ls uc ["orb"];
ls_notb = find_ls uc ["notb"];
ls_unit = find_ls uc ["Tuple0"];
ls_lt = find_ls uc ["infix <"];
ls_gt = find_ls uc ["infix >"];
ls_le = find_ls uc ["infix <="];
ls_ge = find_ls uc ["infix >="];
ls_add = find_ls uc ["infix +"];
let create env retrieve = {
env = env;
retrieve = retrieve;
memo = Hashtbl.create 17;
}
(* addition *)
let add_global id tyv env =
let tyl, ty = uncurry_type tyv in
let s = create_lsymbol id tyl (Some ty) in
s, { env with globals = Mstr.add s.ls_name.id_string (s, tyv) env.globals }
let add_decl d env =
{ env with uc = Typing.with_tuples add_decl env.uc d }
let add_exception id ty env =
let tyl = match ty with None -> [] | Some ty -> [ty] in
let s = create_lsymbol id tyl (Some (ty_app env.ts_exn [])) in
s, { env with exceptions = Mstr.add s.ls_name.id_string s env.exceptions }
let t_True env =
t_app env.ls_True [] (ty_app env.ts_bool [])
let type_v_unit env =
Tpure (ty_app env.ts_unit [])
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
exception ModuleNotFound of string list * string
let rec add_suffix = function
| [] -> assert false
| [f] -> [f ^ ".mlw"]
| p :: f -> p :: add_suffix f
let find_library penv sl =
try Hashtbl.find penv.memo sl
with Not_found ->
Hashtbl.add penv.memo sl Mnm.empty;
let c = Env.find_channel penv.env (add_suffix sl) in
let m = penv.retrieve penv c in
close_in c;
Hashtbl.replace penv.memo sl m;
m
let find_module penv sl s =
try Mnm.find s (find_library penv sl)
with Not_found -> raise (ModuleNotFound (sl, s))
open Why
open Pgm_module
type t
val tag : t -> Hashweak.tag
val get_env : t -> Env.env
val create : Env.env -> t
type retrieve_module = t -> in_channel -> Pgm_module.t Mnm.t
val create : Env.env -> retrieve_module -> t
exception ModuleNotFound of string list * string
......
......@@ -27,14 +27,26 @@ open Ptree
open Pgm_ptree
open Pgm_module
let add_module ?(type_only=false) env lmod m =
let add_module ?(type_only=false) env penv lmod m =
let wp = not type_only in
let id = m.mod_name in
let uc = create_module (Ident.id_user id.id id.id_loc) in
let uc = List.fold_left (Pgm_typing.decl ~wp env lmod) uc m.mod_decl in
let uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in
let m = close_module uc in
Mstr.add id.id m lmod
let retrieve penv c =
let pgm_env_of_env =
let h = Env.Wenv.create 17 in
fun env ->
try
Env.Wenv.find h env
with Not_found ->
let penv = Pgm_env.create env retrieve in
Env.Wenv.set h env penv;
penv
let read_channel env file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
......@@ -43,7 +55,8 @@ let read_channel env file c =
Theory.Mnm.empty
else begin
let type_only = Debug.test_flag Typing.debug_type_only in
let mm = List.fold_left (add_module ~type_only env) Mstr.empty ml in
let penv = pgm_env_of_env env in
let mm = List.fold_left (add_module ~type_only env penv) Mstr.empty ml in
Mstr.fold
(fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm)
mm Theory.Mnm.empty
......
......@@ -1304,18 +1304,18 @@ let cannot_be_generalized gl = function
| Tpure _ | Tarrow _ ->
false
let find_module lmod q id = match q with
let find_module penv lmod q id = match q with
| [] ->
(* local module *)
Mstr.find id lmod
(* TODO? with Not_found -> find_theory env [] id end *)
| _ :: _ ->
(* theory in file f *)
assert false (*TODO*)
Pgm_env.find_module penv q id
(* env = to retrieve theories from the loadpath
penv = to retrieve modules from the loadpath
lmod = local modules *)
let rec decl ~wp env lmod uc = function
let rec decl ~wp env penv lmod uc = function
| Pgm_ptree.Dlogic dl ->
Pgm_module.parse_logic_decls env dl uc
| Pgm_ptree.Dlet (id, e) ->
......@@ -1363,7 +1363,7 @@ let rec decl ~wp env lmod uc = function
let q, id = Typing.split_qualid qid in
let m =
try
find_module lmod q id
find_module penv lmod q id
with Not_found ->
errorm ~loc "unbound module %a" print_qualid qid
in
......@@ -1390,7 +1390,7 @@ let rec decl ~wp env lmod uc = function
| Pgm_ptree.Dnamespace (id, import, dl) ->
let loc = id.id_loc in
let uc = open_namespace uc in
let uc = List.fold_left (decl ~wp env lmod) uc dl in
let uc = List.fold_left (decl ~wp env penv 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
......
......@@ -23,7 +23,7 @@ open Util
val debug : Debug.flag
val decl :
wp:bool -> Env.env -> Pgm_module.t Mstr.t ->
wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Mstr.t ->
Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
val print_post : Format.formatter -> Pgm_ttree.post -> 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