added new files for modules

parent 70e507e0
open Why
open Util
open Ident
open Theory
open Term
open Pgm_types
open Pgm_ttree
module Mnm = Mstr
type namespace = {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exceptions*)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
let empty_ns = {
ns_pr = Mnm.empty;
ns_ex = Mnm.empty;
ns_ns = Mnm.empty;
}
exception ClashSymbol of string
let ns_replace eq chk x vo vn =
if not chk then vn else
if eq vo vn then vo else
raise (ClashSymbol x)
let ns_union eq chk =
Mnm.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
let pr_equal p1 p2 = ls_equal p1.p_ls p2.p_ls
let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_pr = ns_union pr_equal chk ns1.ns_pr ns2.ns_pr;
ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_ns = Mnm.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mnm.change x (function
| None -> Some ns
| Some os -> Some (merge_ns chk ns os)) m
let ns_add eq chk x v m = Mnm.change x (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) m
let pr_add = ns_add pr_equal
let ex_add = ns_add ls_equal
let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
let rec ns_find get_map ns = function
| [] -> assert false
| [a] -> Mnm.find a (get_map ns)
| a::l -> ns_find get_map (Mnm.find a ns.ns_ns) l
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(* modules under construction *)
type uc = {
uc_name : Ident.ident;
uc_th : theory_uc; (* the logic theory used to type annotations *)
uc_decls : decl list; (* the program declarations *)
uc_import : namespace list;
uc_export : namespace list;
}
let create_module n =
let uc = Theory.create_theory n in
(* let th = Env.find_theory env ["programs"] "Prelude" in *)
(* let uc = Theory.use_export uc th in *)
{ uc_name = id_register n;
uc_th = uc;
uc_decls = [];
uc_import = [empty_ns];
uc_export = [empty_ns];
}
let open_namespace uc = match uc.uc_import with
| ns :: _ -> { uc with
uc_import = ns :: uc.uc_import;
uc_export = empty_ns :: uc.uc_export; }
| [] -> assert false
exception NoOpenedNamespace
let close_namespace uc import s =
match uc.uc_import, uc.uc_export with
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
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; }
| [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
type t = {
m_name : Ident.ident;
m_th : theory;
m_decls : decl list;
m_export : namespace;
}
exception CloseModule
let close_module uc = match uc.uc_export with
| [e] ->
{ m_name = uc.uc_name;
m_decls = List.rev uc.uc_decls;
m_export = e;
m_th = close_theory uc.uc_th; }
| _ ->
raise CloseModule
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
open Why
open Ident
open Term
open Pgm_types
module Mnm : Map.S with type key = string
type namespace = private {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exception symbols *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
val ns_find_pr : namespace -> string list -> psymbol
val ns_find_ex : namespace -> string list -> esymbol
val ns_find_ns : namespace -> string list -> namespace
(** a module under construction *)
type uc
(** a module *)
type t
val create_module : preid -> uc
val close_module : uc -> t
val open_namespace : uc -> uc
val close_namespace : uc -> bool -> string option -> uc
(* exceptions *)
exception CloseModule
open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl
module E = Pgm_effect
(* types *)
type effect = Pgm_effect.t
type reference = Pgm_effect.reference
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
(* purify: turns program types into logic types *)
let ts_arrow =
let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
Ty.create_tysymbol (Ident.id_fresh "arrow") v None
let make_arrow_type tyl ty =
let arrow ty1 ty2 = Ty.ty_app ts_arrow [ty1; ty2] in
List.fold_right arrow tyl ty
let rec uncurry_type = function
| Tpure ty ->
[], ty
| Tarrow (bl, c) ->
let tyl1 = List.map (fun (v,_) -> v.vs_ty) bl in
let tyl2, ty = uncurry_type c.c_result_type in
tyl1 @ tyl2, ty (* TODO: improve? *)
let purify v =
let tyl, ty = uncurry_type v in
make_arrow_type tyl ty
(* symbols *)
type psymbol = {
p_ls : lsymbol;
p_tv : type_v;
}
(* TODO: ensure ls = purify v *)
let create_psymbol ls v = { p_ls = ls; p_tv = v }
type esymbol = lsymbol
(* misc. functions *)
let v_result ty = create_vsymbol (id_fresh "result") ty
let exn_v_result ls = match ls.ls_args with
| [] -> None
| [ty] -> Some (v_result ty)
| _ -> assert false
let post_map f ((v, q), ql) =
(v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
let type_c_of_type_v = function
| Tarrow ([], c) ->
c
| v ->
let ty = purify v in
{ c_result_type = v;
c_effect = Pgm_effect.empty;
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let rec subst_var ts s vs =
let ty' = ty_inst ts vs.vs_ty in
if ty_equal ty' vs.vs_ty then
s, vs
else
let vs' = create_vsymbol (id_clone vs.vs_name) ty' in
Mvs.add vs (t_var vs') s, vs'
and subst_post ts s ((v, q), ql) =
let vq = let s, v = subst_var ts s v in v, f_ty_subst ts s q in
let handler (e, (v, q)) = match v with
| None -> e, (v, f_ty_subst ts s q)
| Some v -> let s, v = subst_var ts s v in e, (Some v, f_ty_subst ts s q)
in
vq, List.map handler ql
let rec subst_type_c ef ts s c =
{ c_result_type = subst_type_v ef ts s c.c_result_type;
c_effect = E.subst ef c.c_effect;
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
and subst_type_v ef ts s = function
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (binder ef ts) s bl in
Tarrow (bl, subst_type_c ef ts s c)
and binder ef ts s (vs, v) =
let v = subst_type_v ef ts s v in
let s, vs = subst_var ts s vs in
s, (vs, v)
let tpure ty = Tpure ty
let tarrow bl c = match bl with
| [] ->
invalid_arg "tarrow"
| _ ->
let rename (e, s) (vs, v) =
let vs' = create_vsymbol (id_clone vs.vs_name) vs.vs_ty in
let v' = subst_type_v e Mtv.empty s v in
let e' = Mvs.add vs (E.Rlocal vs') e in
let s' = Mvs.add vs (t_var vs') s in
(e', s'), (vs', v')
in
let (e, s), bl' = Util.map_fold_left rename (Mvs.empty, Mvs.empty) bl in
Tarrow (bl', subst_type_c e Mtv.empty s c)
let subst1 vs1 t2 = Mvs.add vs1 t2 Mvs.empty
let apply_type_v v vs = match v with
| Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify tyx) vs.vs_ty in
let c = type_c_of_type_v (Tarrow (bl, c)) in
subst_type_c Mvs.empty ts (subst1 x (t_var vs)) c
| Tarrow ([], _) | Tpure _ ->
assert false
let apply_type_v_ref v r = match r, v with
| E.Rlocal vs as r, Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify tyx) vs.vs_ty in
let c = type_c_of_type_v (Tarrow (bl, c)) in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_var vs)) c
| E.Rglobal ls as r, Tarrow ((x, tyx) :: bl, c) ->
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
let ts = ty_match Mtv.empty (purify tyx) ty in
let c = type_c_of_type_v (Tarrow (bl, c)) in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_app ls [] ty)) c
| _ ->
assert false
let occur_formula r f = match r with
| E.Rlocal vs -> f_occurs_single vs f
| E.Rglobal ls -> f_s_any (fun _ -> false) (ls_equal ls) f
let rec occur_type_v r = function
| Tpure _ ->
false
| Tarrow (bl, c) ->
occur_arrow r bl c
and occur_arrow r bl c = match bl with
| [] ->
occur_type_c r c
| (vs, v) :: bl ->
occur_type_v r v ||
not (E.ref_equal r (E.Rlocal vs)) && occur_arrow r bl c
and occur_type_c r c =
occur_type_v r c.c_result_type ||
occur_formula r c.c_pre ||
E.occur r c.c_effect ||
occur_post r c.c_post
and occur_post r ((_, q), ql) =
occur_formula r q ||
List.exists (fun (_, (_, qe)) -> occur_formula r qe) ql
let rec eq_type_v v1 v2 = match v1, v2 with
| Tpure ty1, Tpure ty2 ->
ty_equal ty1 ty2
| Tarrow _, Tarrow _ ->
false (* TODO? *)
| _ ->
assert false
(* pretty-printers *)
open Pp
open Format
open Pretty
let print_post fmt ((_,q), el) =
let print_exn_post fmt (l,(_,q)) =
fprintf fmt "| %a -> {%a}" print_ls l print_fmla q
in
fprintf fmt "{%a} %a" print_fmla q (print_list space print_exn_post) el
let rec print_type_v fmt = function
| Tpure ty ->
print_ty fmt ty
| Tarrow (bl, c) ->
fprintf fmt "@[<hov 2>%a ->@ %a@]"
(print_list arrow print_binder) bl print_type_c c
and print_type_c fmt c =
fprintf fmt "@[{%a}@ %a%a@ %a@]" print_fmla c.c_pre
print_type_v c.c_result_type Pgm_effect.print c.c_effect
print_post c.c_post
and print_binder fmt (x, v) =
fprintf fmt "(%a:%a)" print_vs x print_type_v v
(* let apply_type_v env v vs = *)
(* eprintf "apply_type_v: v=%a vs=%a@." print_type_v v print_vs vs; *)
(* apply_type_v env v vs *)
open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl
(* types *)
type effect = Pgm_effect.t
type reference = Pgm_effect.reference
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v = private
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
val tpure : Ty.ty -> type_v
val tarrow : binder list -> type_c -> type_v
(* symbols *)
type psymbol = private {
p_ls : lsymbol;
p_tv : type_v;
}
val create_psymbol : lsymbol -> type_v -> psymbol
type esymbol = lsymbol
(* program types -> logic types *)
val ts_arrow : tysymbol
val purify :type_v -> ty
(* operations on program types *)
val apply_type_v : type_v -> vsymbol -> type_c
val apply_type_v_ref : type_v -> reference -> type_c
val occur_type_v : reference -> type_v -> bool
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val post_map : (fmla -> fmla) -> post -> post
val subst1 : vsymbol -> term -> term Mvs.t
val eq_type_v : type_v -> type_v -> bool
(* pretty-printers *)
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_post : Format.formatter -> 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