Commit 039db14d authored by Francois Bobot's avatar Francois Bobot

ajout de transform_utils pour la gestion des cloned_from_*. Correction de extract_goals

parent 398cfa92
......@@ -108,7 +108,7 @@ CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo typing.cmo
PARSER_CMO := parser.cmo lexer.cmo typing.cmo transform_utils.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
......
......@@ -241,6 +241,7 @@ let create_ty_decl tdl = Hdecl.hashcons (mk_decl (Dtype tdl))
let create_logic_decl ldl = Hdecl.hashcons (mk_decl (Dlogic ldl))
let create_ind_decl indl = Hdecl.hashcons (mk_decl (Dind indl))
let create_prop_decl k p = Hdecl.hashcons (mk_decl (Dprop (k, p)))
let create_prop_and_decl k preid f = Hdecl.hashcons (mk_decl (Dprop (k, create_prop preid f)))
let create_use_decl th = Hdecl.hashcons (mk_decl (Duse th))
let create_clone_decl sl = Hdecl.hashcons (mk_decl (Dclone sl))
......
......@@ -120,6 +120,7 @@ val create_ty_decl : ty_decl list -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
val create_prop_decl : prop_kind -> prop -> decl
val create_prop_and_decl : prop_kind -> preid -> fmla -> decl
(* exceptions *)
......
......@@ -170,6 +170,11 @@ let split_goals =
let f _ (ctxt,l) decl =
match decl.d_node with
| Dprop (Pgoal,_) -> (ctxt,(add_decl ctxt decl)::l)
| Dprop (Plemma,f) ->
let d1 = create_prop_and_decl Paxiom (id_dup f.pr_name) f.pr_fmla in
let d2 = create_prop_and_decl Pgoal (id_dup f.pr_name) f.pr_fmla in
(add_decl ctxt d1,
(add_decl ctxt d2)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (empty_context,[]) in
conv_res g snd
......@@ -178,6 +183,10 @@ let extract_goals =
let f _ (ctxt,l) decl =
match decl.d_node with
| Dprop (Pgoal,f) -> (ctxt,(f.pr_name,f.pr_fmla,ctxt)::l)
| Dprop (Plemma,f) ->
let d = create_prop_and_decl Paxiom (id_dup f.pr_name) f.pr_fmla in
(add_decl ctxt d,
(f.pr_name,f.pr_fmla,ctxt)::l)
| _ -> (add_decl ctxt decl,l) in
let g = fold_up f (empty_context,[]) in
conv_res g snd
......
......@@ -105,31 +105,15 @@ let print_type_decl fmt = function
| _, Talgebraic _ ->
assert false
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_ls env ctxt s ls1 =
try
let th = Typing.find_theory env ac_th in
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 ac_th = ["algebra";"AC"]
open Transform_utils
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"
(if is_ls env ctxt "op" ls then "ac " else "")
(if cloned_from_ls env ctxt ac_th "op" ls then "ac " else "")
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) ->
......@@ -150,8 +134,8 @@ let print_decl env ctxt fmt d = match d.d_node with
| Dind _ ->
assert false
| Dprop (Paxiom, pr) when
(is_pr env ctxt "Comm" pr
|| is_pr env ctxt "Assoc" pr) -> ()
(cloned_from_pr env ctxt ac_th "Comm" pr
|| cloned_from_pr env ctxt ac_th "Assoc" pr) -> ()
| Dprop (Paxiom, pr) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla
......
open Ty
open Term
open Theory
let qualid_of_lstring = function
| [] -> invalid_arg "Transfrom_utils.qualid_of_lstring : empty list"
| a :: l ->
let id = Ptree.Qident {Ptree.id = a;id_loc = Loc.dummy_position} in
List.fold_left (fun acc x ->
Ptree.Qdot (acc,{Ptree.id = x;id_loc = Loc.dummy_position})) id l
let cloned_from_ts env ctxt l s ls1 =
try
let th = Typing.find_theory env (qualid_of_lstring l) in
let ls2 = Mnm.find s th.th_export.ns_ts in
Context_utils.cloned_from ctxt ls1.ts_name ls2.ts_name
with Loc.Located _ -> assert false
let cloned_from_ls env ctxt l s ls1 =
try
let th = Typing.find_theory env (qualid_of_lstring l) in
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 cloned_from_pr env ctxt l s pr1 =
try
let th = Typing.find_theory env (qualid_of_lstring l) 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
val qualid_of_lstring : string list -> Ptree.qualid
val cloned_from_ts : Typing.env -> Theory.context ->
string list -> string -> Ty.tysymbol -> bool
val cloned_from_ls : Typing.env -> Theory.context ->
string list -> string -> Term.lsymbol -> bool
val cloned_from_pr : Typing.env -> Theory.context ->
string list -> string -> Theory.prop -> bool
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