format boxes src/printer/tptp.ml

parent 01a4499f
......@@ -134,11 +134,11 @@ let print_decl drv fmt d = match d.d_node with
"tptp : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "fof(%s, axiom,@ %a).\n"
fprintf fmt "@[<hov 2>fof(%s, axiom,@ %a).@]@\n"
(id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
(print_fmla drv) f; true
| Dprop (Pgoal, pr, f) -> (* TODO : what is pr ? *)
fprintf fmt "fof(%s, conjecture,@ %a ).\n"
fprintf fmt "@[<hov 2>fof(%s, conjecture,@ %a ).@]@\n"
(id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
(print_fmla drv) f; true
(* fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; *)
......
......@@ -7,6 +7,7 @@ open Ty
module E = Pgm_effect
type effect = E.t
type reference = Pgm_effect.reference
type pre = Term.fmla
......@@ -142,25 +143,53 @@ let type_c_of_type_v env = function
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
let rec subst_type_c s c =
{ c_result_type = subst_type_v s c.c_result_type;
let rec subst_type_c ts s c =
{ c_result_type = subst_type_v ts s c.c_result_type;
c_effect = c.c_effect;
c_pre = f_subst s c.c_pre;
c_post = post_map (f_subst s) c.c_post; }
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
and subst_type_v s = function
| Tpure _ as v -> v
| Tarrow (bl, c) -> Tarrow (bl, subst_type_c s c)
and subst_type_v ts s = function
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (binder ts) s bl in
Tarrow (bl, subst_type_c ts s c)
and binder ts s (vs, v) =
let v = subst_type_v ts s v in
let s, vs = subst_var ts s vs in
s, (vs, v)
and 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 subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
let apply_type_v env v vs = match v with
| Tarrow ((x, _) :: bl, c) ->
| Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify env.uc tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c (subst1 x vs) c
subst_type_c ts (subst1 x vs) c
| Tarrow ([], _) | Tpure _ ->
assert false
let apply_type_v_ref env v r =
assert false (*TODO*)
(* pretty-printers *)
open Pp
......@@ -188,4 +217,8 @@ and print_type_c fmt c =
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
......@@ -8,6 +8,7 @@ open Decl
(* types *)
type effect = Pgm_effect.t
type reference = Pgm_effect.reference
type pre = Term.fmla
......@@ -46,7 +47,8 @@ val ls_assign : theory_uc -> lsymbol (* := : 'a ref -> 'a -> unit *)
val purify : theory_uc -> type_v -> ty
val apply_type_v : env -> type_v -> vsymbol -> type_c
val apply_type_v : env -> type_v -> vsymbol -> type_c
val apply_type_v_ref : env -> type_v -> reference -> type_c
val empty_env : theory_uc -> env
......
......@@ -79,8 +79,11 @@ and expr_desc env _loc ty = function
let e1 = expr env e1 in
let c = apply_type_v env e1.expr_type_v vs in
Eany c, c.c_result_type, c.c_effect
| Pgm_ttree.Eapply_ref _ ->
assert false (*TODO*)
(* TODO: do not forget about e1 *)
| Pgm_ttree.Eapply_ref (e1, r) ->
let e1 = expr env e1 in
let c = apply_type_v_ref env e1.expr_type_v r in
Eany c, c.c_result_type, c.c_effect
| Pgm_ttree.Efun (bl, t) ->
let env = add_binders env bl in
let t, c = triple env t in
......@@ -176,6 +179,10 @@ let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts env.ts_ref -> ty
| _ -> assert false
let is_ref_ty env ty = match ty.ty_node with
| Tyapp (ts, [_]) -> ts_equal ts env.ts_ref
| _ -> false
(* replace !r by v everywhere in formula f *)
let rec unref env r v f =
f_map (unref_term env r v) (unref env r v) f
......@@ -203,9 +210,17 @@ let quantify env ef f =
let abstract_wp env ef (q',ql') (q,ql) =
assert (List.length ql' = List.length ql);
let quantify_r f' f res =
let quantify_res f' f res =
let f = wp_implies f' f in
let f = match res with Some v -> wp_forall [v] [] f | None -> f in
let f = match res with
| Some v when is_ref_ty env v.vs_ty ->
let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in
wp_forall [v'] [] (unref env (E.Rlocal v) v' f)
| Some v ->
wp_forall [v] [] f
| None ->
f
in
quantify env ef f
in
let quantify_h (e',(x',f')) (e,(x,f)) =
......@@ -215,12 +230,12 @@ let abstract_wp env ef (q',ql') (q,ql) =
| None, None -> None, f'
| _ -> assert false
in
quantify_r f' f res
quantify_res f' f res
in
let f =
let res, f = q and res', f' = q' in
let f' = f_subst (subst1 res' res) f' in
quantify_r f' f (Some res)
quantify_res f' f (Some res)
in
wp_ands (f :: List.map2 quantify_h ql' ql)
......
......@@ -15,17 +15,9 @@ parameter r : int ref
parameter write : v:int -> {} unit writes r { !r = v }
let ff () =
{ true }
write 42
{ !r = 42 }
(* TODO
let ff () =
{ true }
let x = ref 0 in !x
{ result = 0 }
*)
{ !r >= 0 }
!r + 2
{ result = 42 }
(*
......
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