Commit 398cfa92 authored by Francois Bobot's avatar Francois Bobot

correction de pretty print de ac dans alt-ergo

parent 08f037e6
......@@ -3,10 +3,14 @@ open Theory
let cloned_from ctxt i1 i2 =
(* Format.printf "@[<hov 2>cloned (%a = %a)?: %a@]@\n"
print_ident i2 print_ident i1
print_ctxt ctxt;*)
let rec aux i =
i == i2 || (let i3 = Mid.find i1 ctxt.ctxt_cloned in
aux i3)
i == i1 ||
try
let i3 = Mid.find i ctxt.ctxt_cloned in
List.exists aux i3
with Not_found -> false
in
try
aux i1
with Not_found -> false
aux i2
......@@ -145,7 +145,7 @@ and namespace = {
and context = {
ctxt_decls : (decl * context) option;
ctxt_known : decl Mid.t;
ctxt_cloned : ident Mid.t;
ctxt_cloned : ident list Mid.t;
ctxt_tag : int;
}
......@@ -347,14 +347,18 @@ module Context = struct
let push_decl ctxt kn d =
let cloned = match d.d_node with
| Dclone l -> List.fold_left (fun m (i1,i2) -> Mid.add i1 i2 m)
| Dclone l -> List.fold_left
(fun m (i1,i2) ->
let l = try Mid.find i1 m with Not_found -> [] in
Mid.add i1 (i2::l) m)
ctxt.ctxt_cloned l
| _ -> ctxt.ctxt_cloned in
Hctxt.hashcons { ctxt with
ctxt_decls = Some (d, ctxt);
ctxt_known = kn;
ctxt_cloned = cloned;
}
Hctxt.hashcons
{ ctxt with
ctxt_decls = Some (d, ctxt);
ctxt_known = kn;
ctxt_cloned = cloned;
}
(* Manage known symbols *)
......@@ -869,5 +873,12 @@ let rec print_namespace fmt ns =
fprintf fmt "@]"
let print_uc fmt uc = print_namespace fmt (Theory.get_namespace uc)
let print_ctxt fmt ctxt =
fprintf fmt "@[<hov 2>ctxt : cloned : %a@]"
(Pp.print_iter2 Mid.iter Pp.semi (Pp.constant_string "->")
print_ident (Pp.print_list Pp.simple_comma print_ident))
ctxt.ctxt_cloned
let print_th fmt th = fprintf fmt "<theory (TODO>"
......@@ -97,7 +97,7 @@ and namespace = private {
and context = private {
ctxt_decls : (decl * context) option;
ctxt_known : decl Mid.t;
ctxt_cloned : ident Mid.t;
ctxt_cloned : ident list Mid.t;
ctxt_tag : int;
}
......@@ -194,5 +194,7 @@ end
(** Debugging *)
val print_ident : Format.formatter -> ident -> unit
val print_uc : Format.formatter -> theory_uc -> unit
val print_ctxt : Format.formatter -> context -> unit
val print_th : Format.formatter -> theory -> unit
......@@ -109,20 +109,27 @@ let ac_th = (Ptree.Qdot
(Ptree.Qident {Ptree.id = "algebra";id_loc = Loc.dummy_position},
{Ptree.id = "AC";id_loc = Loc.dummy_position}))
let is_ac env ctxt ls1 =
let is_ls env ctxt s ls1 =
try
let th = Typing.find_theory env ac_th in
let ls2 = Mnm.find "op" th.th_export.ns_ls in
if Context_utils.cloned_from ctxt ls1.ls_name ls2.ls_name
then "ac " else ""
with Loc.Located _ -> ""
let ls2 = Mnm.find s th.th_export.ns_ls in
Context_utils.cloned_from ctxt ls1.ls_name ls2.ls_name
with Loc.Located _ -> assert false
let is_pr env ctxt s pr1 =
try
let th = Typing.find_theory env ac_th in
let pr2 = Mnm.find s th.th_export.ns_pr in
Context_utils.cloned_from ctxt pr1.pr_name pr2.pr_name
with Loc.Located _ -> assert false
let print_logic_decl env ctxt fmt = function
| Lfunction (ls, None) ->
let tyl = ls.ls_args in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
(is_ac env ctxt ls)
(if is_ls env ctxt "op" ls then "ac " else "")
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) ->
......@@ -142,6 +149,9 @@ let print_decl env ctxt fmt d = match d.d_node with
print_list newline (print_logic_decl env ctxt) fmt dl
| Dind _ ->
assert false
| Dprop (Paxiom, pr) when
(is_pr env ctxt "Comm" pr
|| is_pr env ctxt "Assoc" pr) -> ()
| Dprop (Paxiom, pr) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla
......
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