Commit b54aec3f authored by Andrei Paskevich's avatar Andrei Paskevich

specify the kind of instance in Pretty and Why3

parent 3cb0ff15
......@@ -319,13 +319,13 @@ let print_pkind fmt = function
let print_inst fmt (id1,id2) =
if Hid.mem thash id2 then
let n = id_unique tprinter id1 in
fprintf fmt "%s = %a" n print_ts (Hid.find thash id2)
fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
else if Hid.mem lhash id2 then
let n = id_unique lprinter id1 in
fprintf fmt "%s = %a" n print_ls (Hid.find lhash id2)
fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
else if Hid.mem phash id2 then
let n = id_unique pprinter id1 in
fprintf fmt "%s = %a" n print_pr (Hid.find phash id2)
fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
else assert false
let print_decl fmt d = match d.d_node with
......@@ -342,7 +342,7 @@ let print_decl fmt d = match d.d_node with
print_th th (print_list comma print_inst) inst
let print_decls fmt dl =
fprintf fmt "@[<hov>%a@]" (print_list newline2 print_decl) dl
fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl
let print_context fmt ctxt = print_decls fmt (Context.get_decls ctxt)
......
......@@ -320,13 +320,13 @@ let print_pkind fmt = function
let print_inst fmt (id1,id2) =
if Hid.mem thash id2 then
let n = id_unique tprinter id1 in
fprintf fmt "%s = %a" n print_ts (Hid.find thash id2)
fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
else if Hid.mem lhash id2 then
let n = id_unique lprinter id1 in
fprintf fmt "%s = %a" n print_ls (Hid.find lhash id2)
fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
else if Hid.mem phash id2 then
let n = id_unique pprinter id1 in
fprintf fmt "%s = %a" n print_pr (Hid.find phash id2)
fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
else assert false
let print_decl fmt d = match d.d_node with
......@@ -343,7 +343,7 @@ let print_decl fmt d = match d.d_node with
print_th th (print_list comma print_inst) inst
let print_decls fmt dl =
fprintf fmt "@[<hov>%a@]" (print_list newline2 print_decl) dl
fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl
let print_context drv fmt ctxt =
forget_all ();
......
......@@ -13,6 +13,7 @@ theory Test
logic id2(x: int) : int = id(x)
logic succ(x:int) : int = id(x+1)
logic even(x: int) = 2*(x/2) = x
clone ThA with type test = int, logic test = (-_)
goal G : forall x:int. 1 = succ(id2(zero))
goal G2 : forall x:int. 0 = 1
end
......
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