Commit dfb52c23 authored by Francois Bobot's avatar Francois Bobot

ajout de cloned dans context et essaie d'utilisation dans alt-ergo.ml

parent 92067658
......@@ -101,7 +101,8 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why
#####
CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo transform.cmo
CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo transform.cmo \
context_utils.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
......
open Ident
open Theory
let cloned_from ctxt i1 i2 =
let rec aux i =
i == i2 || (let i3 = Mid.find i1 ctxt.ctxt_cloned in
aux i3)
in
try
aux i1
with Not_found -> false
open Ident
open Theory
val cloned_from : context -> ident -> ident -> bool
......@@ -145,6 +145,7 @@ and namespace = {
and context = {
ctxt_decls : (decl * context) option;
ctxt_known : decl Mid.t;
ctxt_cloned : ident Mid.t;
ctxt_tag : int;
}
......@@ -340,13 +341,19 @@ module Context = struct
let empty_context = Hctxt.hashcons {
ctxt_decls = None;
ctxt_known = builtin_known;
ctxt_cloned = Mid.empty;
ctxt_tag = -1;
}
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)
ctxt.ctxt_cloned l
| _ -> ctxt.ctxt_cloned in
Hctxt.hashcons { ctxt with
ctxt_decls = Some (d, ctxt);
ctxt_known = kn
ctxt_known = kn;
ctxt_cloned = cloned;
}
(* Manage known symbols *)
......
......@@ -97,6 +97,7 @@ and namespace = private {
and context = private {
ctxt_decls : (decl * context) option;
ctxt_known : decl Mid.t;
ctxt_cloned : ident Mid.t;
ctxt_tag : int;
}
......
......@@ -85,14 +85,14 @@ let type_file env file =
let extract_goals ctxt =
Transform.apply Transform.extract_goals ctxt
let transform l =
let transform env l =
let l = List.map (fun t -> t,t.th_ctxt) (Typing.list_theory l) in
let l = Transform.apply transformation l in
if !print_stdout then
List.iter (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
else if !alt_ergo then match l with
| (_,ctxt) :: _ -> begin match extract_goals ctxt with
| g :: _ -> Alt_ergo.print_goal std_formatter g
| g :: _ -> Alt_ergo.print_goal env std_formatter g
| [] -> ()
end
| [] -> ()
......@@ -103,7 +103,7 @@ let () =
try
let env = Typing.create !loadpath in
let l = List.fold_left type_file env !files in
transform l
transform env l
with e when not !debug ->
eprintf "%a@." report e;
exit 1
......
......@@ -105,11 +105,25 @@ let print_type_decl fmt = function
| _, Talgebraic _ ->
assert false
let print_logic_decl fmt = function
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 =
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 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 %a : %a -> %a@]@\n" print_ident ls.ls_name
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
(is_ac env ctxt ls)
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) ->
let id = ls.ls_name in
......@@ -121,11 +135,11 @@ let print_logic_decl fmt = function
| Lpredicate _ ->
assert false (*TODO*)
let print_decl fmt d = match d.d_node with
let print_decl env ctxt fmt d = match d.d_node with
| Dtype dl ->
print_list newline print_type_decl fmt dl
| Dlogic dl ->
print_list newline print_logic_decl fmt dl
print_list newline (print_logic_decl env ctxt) fmt dl
| Dind _ ->
assert false
| Dprop (Paxiom, pr) ->
......@@ -139,11 +153,11 @@ let print_decl fmt d = match d.d_node with
| Duse _ | Dclone _ ->
()
let print_context fmt ctxt =
let print_context env fmt ctxt =
let decls = Context.get_decls ctxt in
print_list newline2 print_decl fmt decls
print_list newline2 (print_decl env ctxt) fmt decls
let print_goal fmt (id, f, ctxt) =
print_context fmt ctxt;
let print_goal env fmt (id, f, ctxt) =
print_context env fmt ctxt;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]" print_ident id print_fmla f
......@@ -8,6 +8,6 @@ val print_term : formatter -> term -> unit
val print_fmla : formatter -> fmla -> unit
val print_context : formatter -> context -> unit
val print_context : Typing.env -> formatter -> context -> unit
val print_goal : formatter -> ident * fmla * context -> unit
val print_goal : Typing.env -> formatter -> ident * fmla * context -> 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