programs: a few pretty-printers for debugging purposes

parent 81908686
......@@ -197,8 +197,8 @@ clean::
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_parser.output src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing \
pgm_itree pgm_effect pgm_wp pgm_main
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect pgm_typing \
pgm_itree pgm_wp pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
......@@ -21,7 +21,10 @@ open Why
open Util
open Ident
open Term
open Pgm_ttree
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
module Reference = struct
......@@ -61,4 +64,28 @@ let add_read r t = { t with reads = R.add r t.reads }
let add_write r t = { t with writes = R.add r t.writes }
let add_raise e t = { t with raises = E.add e t.raises }
let union t1 t2 =
{ reads = R.union t1.reads t2.reads;
writes = R.union t1.writes t2.writes;
raises = E.union t1.raises t2.raises; }
open Format
open Pp
open Pretty
let print_reference fmt = function
| Rlocal vs -> print_vs fmt vs
| Rglobal ls -> print_ls fmt ls
let print_rset fmt s = print_list comma print_reference fmt (R.elements s)
let print_eset fmt s = print_list comma print_ls fmt (E.elements s)
let print fmt e =
if not (R.is_empty e.reads) then
fprintf fmt "@ reads %a" print_rset e.reads;
if not (R.is_empty e.writes) then
fprintf fmt "@ writes %a" print_rset e.writes;
if not (E.is_empty e.raises) then
fprintf fmt "@ raises %a" print_eset e.raises
......@@ -19,7 +19,10 @@
open Why
open Term
open Pgm_ttree
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
module R : Set.S with type elt = reference
......@@ -35,4 +38,7 @@ val add_read : reference -> t -> t
val add_write : reference -> t -> t
val add_raise : lsymbol -> t -> t
val union : t -> t -> t
val print_reference : Format.formatter -> reference -> unit
val print : Format.formatter -> t -> unit
......@@ -45,7 +45,7 @@ type loop_annotation = Pgm_ttree.loop_annotation
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
expr_type_v: type_v;
expr_effect: Pgm_effect.t;
expr_loc : loc;
}
......
......@@ -82,8 +82,7 @@
let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
let type_c p ty ef q =
{ pc_result_name = id_result ();
pc_result_type = ty;
{ pc_result_type = ty;
pc_effect = ef;
pc_pre = p;
pc_post = q; }
......
......@@ -57,8 +57,7 @@ type type_v =
| Tarrow of binder list * type_c
and type_c =
{ pc_result_name : ident;
pc_result_type : type_v;
{ pc_result_type : type_v;
pc_effect : effect;
pc_pre : pre;
pc_post : post; }
......
......@@ -50,8 +50,7 @@ type dtype_v =
| DTarrow of dbinder list * dtype_c
and dtype_c =
{ dc_result_name : string;
dc_result_type : dtype_v;
{ dc_result_type : dtype_v;
dc_effect : deffect;
dc_pre : dpre;
dc_post : dpost; }
......@@ -104,27 +103,23 @@ and dtriple = dpre * dexpr * dpost
type variant = Term.term * Term.lsymbol
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
type reference = Pgm_effect.reference
type effect = {
e_reads : reference list;
e_writes : reference list;
e_raises : Term.lsymbol list;
}
type effect = Pgm_effect.t
type pre = Term.fmla
type post = Term.fmla * (Term.lsymbol * Term.fmla) list
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_name : Term.vsymbol;
c_result_type : type_v;
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
......
......@@ -26,6 +26,7 @@ open Term
open Theory
open Denv
open Ptree
open Pgm_effect
open Pgm_ttree
type error =
......@@ -201,8 +202,7 @@ let rec dtype_v env = function
and dtype_c env c =
let ty = dtype_v env c.Pgm_ptree.pc_result_type in
{ dc_result_name = c.Pgm_ptree.pc_result_name.id;
dc_result_type = ty;
{ dc_result_type = ty;
dc_effect = deffect env c.Pgm_ptree.pc_effect;
dc_pre = env.denv, lexpr c.Pgm_ptree.pc_pre;
dc_post = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
......@@ -433,40 +433,44 @@ let currying uc tyl ty =
let make_arrow_type ty1 ty2 = Ty.ty_app (ts_arrow uc) [ty1; ty2] in
List.fold_right make_arrow_type tyl ty
let purify uc = function
let rec purify uc = function
| Tpure ty ->
ty
| Tarrow (bl, c) ->
currying uc (List.map (fun (v,_) -> v.vs_ty) bl) c.c_result_name.vs_ty
currying uc (List.map (fun (v,_) -> v.vs_ty) bl)
(purify uc c.c_result_type)
let reference _uc env = function
| DRlocal x -> Rlocal (Mstr.find x env)
| DRglobal ls -> Rglobal ls
let effect uc env e =
{ e_reads = List.map (reference uc env) e.de_reads;
e_writes = List.map (reference uc env) e.de_writes;
e_raises = e.de_raises; }
let reads ef r = add_read (reference uc env r) ef in
let writes ef r = add_write (reference uc env r) ef in
let raises ef l = add_raise l ef in
let ef = List.fold_left reads Pgm_effect.empty e.de_reads in
let ef = List.fold_left writes ef e.de_writes in
List.fold_left raises ef e.de_raises
let pre env (denv, l) = Typing.type_fmla denv env l
let post env ty (q, ql) =
let exn (ls, (denv, l)) =
let env = match ls.ls_args with
let v, env = match ls.ls_args with
| [] ->
env
None, env
| [ty] ->
let v_result = create_vsymbol (id_fresh id_result) ty in
Mstr.add id_result v_result env
Some v_result, Mstr.add id_result v_result env
| _ ->
assert false
in
(ls, Typing.type_fmla denv env l)
(ls, (v, Typing.type_fmla denv env l))
in
let denv, l = q in
let v_result = create_vsymbol (id_fresh id_result) ty in
let env = Mstr.add id_result v_result env in
Typing.type_fmla denv env l, List.map exn ql
(v_result, Typing.type_fmla denv env l), List.map exn ql
let variant denv env (t, ps) =
let loc = t.pp_loc in
......@@ -490,9 +494,7 @@ let rec type_v uc env = function
and type_c uc env c =
let tyv = type_v uc env c.dc_result_type in
let ty = purify uc tyv in
let v = create_vsymbol (id_fresh c.dc_result_name) ty in
{ c_result_name = v;
c_result_type = tyv;
{ c_result_type = tyv;
c_effect = effect uc env c.dc_effect;
c_pre = pre env c.dc_pre;
c_post = post env ty c.dc_post;
......@@ -721,11 +723,30 @@ and triple uc env ((denvp, p), e, q) =
(* pretty-printing (for debugging) *)
open Pp
open Pretty
let print_reference fmt = function
| Rlocal vs -> print_vs fmt vs
| Rglobal ls -> print_ls fmt ls
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 "@[%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 rec print_expr fmt e = match e.expr_desc with
| Elogic t ->
......@@ -797,7 +818,9 @@ let file env uc dl =
List.fold_left (Typing.add_decl env Mnm.empty) uc dl, acc
| Pgm_ptree.Dlet (id, e) ->
let e = type_expr uc e in
(* printf "@[%s:@\n %a@]@." id.id print_expr e; exit 42; *)
(*DEBUG*)
printf "@[--typing %s-----@\n %a@]@."
id.id print_expr e;
let tyl, ty = uncurrying uc e.expr_type in
let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
add_global ls;
......
......@@ -29,3 +29,5 @@ val errorm : ?loc:Loc.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val report : Format.formatter -> error -> unit
val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
val print_type_v : Format.formatter -> Pgm_ttree.type_v -> unit
......@@ -17,36 +17,61 @@
(* *)
(**************************************************************************)
open Format
open Why
open Ident
open Term
open Decl
open Theory
open Pgm_ttree
open Pgm_itree
open Pgm_typing
module E = Pgm_effect
let errorm = Pgm_typing.errorm
(* translation to intermediate trees and effect inference *)
let logic_effect _t =
Pgm_effect.empty (* TODO *)
let rec expr e =
let ty = e.Pgm_ttree.expr_type in
let loc = e.Pgm_ttree.expr_loc in
let d, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
{ expr_desc = d; expr_type = ty; expr_effect = ef; expr_loc = loc }
let d, v, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
{ expr_desc = d; expr_type_v = v; expr_effect = ef; expr_loc = loc }
and expr_desc _loc _ty = function
| Pgm_ttree.Elogic _t ->
and expr_desc _loc ty = function
| Pgm_ttree.Elogic t ->
Elogic t, Tpure ty, logic_effect t
| Pgm_ttree.Elocal _ ->
assert false (*TODO*)
| Pgm_ttree.Eapply _ as _e ->
| Pgm_ttree.Eglobal _ ->
assert false (*TODO*)
| Pgm_ttree.Efun (_bl, (_p, e, _q)) ->
let _e = expr e in
| Pgm_ttree.Eapply _ ->
assert false (*TODO*)
| Pgm_ttree.Eapply_ref _ ->
assert false (*TODO*)
| Pgm_ttree.Efun (bl, t) ->
let t, c = triple t in
Efun (bl, t), Tarrow (bl, c), Pgm_effect.empty
| Pgm_ttree.Elet (v, e1, e2) ->
let e1 = expr e1 in
let e2 = expr e2 in
let ef = Pgm_effect.union e1.expr_effect e2.expr_effect in
Elet (v, e1, e2), e2.expr_type_v, ef
| _ ->
assert false (*TODO*)
and triple (p, e, q) =
let e = expr e in
let c =
{ c_result_type = e.expr_type_v;
c_effect = e.expr_effect;
c_pre = p;
c_post = q }
in
(p, e, q), c
and recfun _ =
assert false (*TODO*)
......@@ -64,6 +89,9 @@ let add_wp_decl uc l f =
let decl uc = function
| Pgm_ttree.Dlet (l, e) ->
let e = expr e in
(* DEBUG *)
printf "@[--effect %a-----@\n %a@]@\n---------@."
Pretty.print_ls l print_type_v e.expr_type_v;
let f = wp l e in
add_wp_decl uc l f
| Pgm_ttree.Dletrec dl ->
......
......@@ -12,9 +12,8 @@ parameter imp_sub :
let ff () =
{ }
let x = ref (2+3) in
let y = ref (3+4) in
imp_sub x y
let x = 1 in
f x 2
{ true }
......
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