Commit c6ac849f authored by Francois Bobot's avatar Francois Bobot

driver.ml is working and alt-ergo.ml is up to date

parent aeb454f9
...@@ -104,8 +104,7 @@ doc/version.tex src/version.ml: Version version.sh config.status ...@@ -104,8 +104,7 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why # why
##### #####
CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo \ CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo pretty.cmo context_utils.cmo
pretty.cmo transform.cmo context_utils.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO)) CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
...@@ -114,8 +113,8 @@ UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO)) ...@@ -114,8 +113,8 @@ UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo typing.cmo transform_utils.cmo PARSER_CMO := parser.cmo lexer.cmo typing.cmo transform_utils.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO)) PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo \ TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \
flatten.cmo inlining.cmo flatten.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO)) TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \ OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \
......
...@@ -30,6 +30,8 @@ end ...@@ -30,6 +30,8 @@ end
theory algebra.AC theory algebra.AC
tag cloned op "AC" tag cloned op "AC"
remove cloned Comm
remove cloned Assoc
end end
(* (*
......
...@@ -50,12 +50,14 @@ let () = ...@@ -50,12 +50,14 @@ let () =
let in_emacs = Sys.getenv "TERM" = "dumb" let in_emacs = Sys.getenv "TERM" = "dumb"
let transformation l = let transformation env l =
let t1 = Simplify_recursive_definition.t env in
let t2 = Inlining.all env in
List.map (fun (t,c) -> List.map (fun (t,c) ->
let c = if !simplify_recursive let c = if !simplify_recursive
then Transform.apply Simplify_recursive_definition.t c then Transform.apply t1 c
else c in else c in
let c = if !inlining then Transform.apply Inlining.all c let c = if !inlining then Transform.apply t2 c
else c in else c in
(t,c)) l (t,c)) l
...@@ -91,14 +93,14 @@ let type_file env file = ...@@ -91,14 +93,14 @@ let type_file env file =
end else end else
Typing.add_from_file env file Typing.add_from_file env file
let extract_goals ctxt = let extract_goals env ctxt =
Transform.apply (Transform.split_goals ()) ctxt Transform.apply (Transform.split_goals env) ctxt
let transform env l = let transform env l =
let l = List.map let l = List.map
(fun t -> t, Context.use_export Context.init_context t) (fun t -> t, Context.use_export Context.init_context t)
(Typing.local_theories l) in (Typing.local_theories l) in
let l = transformation l in let l = transformation env l in
if !print_stdout then if !print_stdout then
List.iter List.iter
(fun (t,ctxt) -> Pretty.print_named_context (fun (t,ctxt) -> Pretty.print_named_context
...@@ -109,7 +111,7 @@ let transform env l = ...@@ -109,7 +111,7 @@ let transform env l =
| Some file -> | Some file ->
let drv = load_driver file env in let drv = load_driver file env in
begin match l with begin match l with
| (_,ctxt) :: _ -> begin match extract_goals ctxt with | (_,ctxt) :: _ -> begin match extract_goals env ctxt with
| g :: _ -> | g :: _ ->
Driver.print_context drv std_formatter g Driver.print_context drv std_formatter g
| [] -> | [] ->
......
...@@ -127,10 +127,14 @@ open Transform_utils ...@@ -127,10 +127,14 @@ open Transform_utils
let print_logic_decl drv ctxt fmt = function let print_logic_decl drv ctxt fmt = function
| Lfunction (ls, None) -> | Lfunction (ls, None) ->
let sac = match Driver.query_ident drv ls.ls_name with
| Driver.Remove -> assert false (*TODO message *)
| Driver.Syntax _ -> assert false (*TODO substitution *)
| Driver.Tag s -> if Snm.mem "AC" s then "ac " else "" in
let tyl = ls.ls_args in let tyl = ls.ls_args in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>logic %a : %a -> %a@]@\n" fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
(*(if cloned_from_ls env ctxt ac_th "op" ls then "ac " else "") *) sac
print_ident ls.ls_name print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty (print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) -> | Lfunction (ls, Some defn) ->
...@@ -154,11 +158,9 @@ let print_decl drv ctxt fmt d = match d.d_node with ...@@ -154,11 +158,9 @@ let print_decl drv ctxt fmt d = match d.d_node with
print_list newline print_type_decl fmt dl print_list newline print_type_decl fmt dl
| Dlogic dl -> | Dlogic dl ->
print_list newline (print_logic_decl drv ctxt) fmt dl print_list newline (print_logic_decl drv ctxt) fmt dl
| Dind _ -> | Dind _ -> assert false (* TODO *)
assert false | Dprop (Paxiom, pr) when
(* | Dprop (Paxiom, pr) when *) Driver.query_ident drv pr.pr_name = Driver.Remove -> ()
(* (cloned_from_pr drv ctxt ac_th "Comm" pr *)
(* || cloned_from_pr env ctxt ac_th "Assoc" pr) -> () *)
| Dprop (Paxiom, pr) -> | Dprop (Paxiom, pr) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla print_ident pr.pr_name print_fmla pr.pr_fmla
......
...@@ -18,8 +18,11 @@ ...@@ -18,8 +18,11 @@
(**************************************************************************) (**************************************************************************)
open Format open Format
open Ty
open Term
open Theory open Theory
open Driver_ast open Driver_ast
open Ident
type error = string type error = string
...@@ -56,6 +59,24 @@ type theory_driver = { ...@@ -56,6 +59,24 @@ type theory_driver = {
thd_tsymbol : unit ; thd_tsymbol : unit ;
} }
type translation =
| Remove
| Syntax of string
| Tag of Snm.t
let translation_union t1 t2 =
match t1, t2 with
| Remove, _ | _, Remove -> Remove
| ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
| Tag s1, Tag s2 -> Tag (Snm.union s1 s2)
let print_translation fmt = function
| Remove -> fprintf fmt "remove"
| Syntax s -> fprintf fmt "syntax %s" s
| Tag s -> fprintf fmt "tag %a"
(Pp.print_iter1 Snm.iter Pp.comma Pp.string) s
type printer = driver -> formatter -> context -> unit type printer = driver -> formatter -> context -> unit
and driver = { and driver = {
...@@ -65,10 +86,21 @@ and driver = { ...@@ -65,10 +86,21 @@ and driver = {
drv_call_file : string option; drv_call_file : string option;
drv_regexps : (string * prover_answer) list; drv_regexps : (string * prover_answer) list;
drv_prelude : string option; drv_prelude : string option;
drv_rules : (string list, theory_rules) Hashtbl.t; drv_thprelude : string Hid.t;
drv_theory : (string list, theory_driver) Hashtbl.t; (* the first is the translation only for this ident, the second is also for representant *)
drv_theory : (translation * translation) Hid.t;
drv_with_ctxt : translation Hid.t;
drv_env : Typing.env;
} }
let print_driver fmt driver =
printf "drv_theory %a@\n"
(Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
(Pp.print_pair print_translation print_translation))
driver.drv_theory
(** registering printers *) (** registering printers *)
let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17 let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17
...@@ -83,9 +115,78 @@ let load_file file = ...@@ -83,9 +115,78 @@ let load_file file =
close_in c; close_in c;
f f
let rec qualid_to_slist = function
| [] -> assert false
| [a] -> a,[]
| a::l -> let id,l = qualid_to_slist l in (id,a::l)
let string_of_qualid thl idl =
let thl = String.concat "." thl in
let idl = String.concat "." idl in
thl^"."^idl
let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = Typing.find_theory env qfile id in
let add_htheory cloned id t =
try
let t2,t3 = Hid.find driver.drv_theory id in
let t23 =
if cloned then (translation_union t t2),t3
else t2,(translation_union t t3) in
Hid.replace driver.drv_theory id t23
with Not_found ->
let t23 = if cloned then (Tag Snm.empty),t else t,(Tag Snm.empty) in
Hid.add driver.drv_theory id t23 in
let rec find_lident ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_ls).ls_name
| a::l -> find_lident (Mnm.find a ns.ns_ns) l in
let rec find_tyident ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_ts).ts_name
| a::l -> find_tyident (Mnm.find a ns.ns_ns) l in
let rec find_prident ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_pr).pr_name
| a::l -> find_prident (Mnm.find a ns.ns_ns) l in
let add = function
| Rremove (c,(loc,q)) ->
begin
try
add_htheory c (find_prident th.th_export q) Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
(string_of_qualid qualid q)
end
| Rsyntax ((loc,q),s) ->
begin
try
add_htheory false (find_lident th.th_export q) (Syntax s)
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
| Rtag (c,(loc,q),s) ->
begin
try
add_htheory c (find_lident th.th_export q) (Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
| Rprelude (loc,s) -> if Hid.mem driver.drv_thprelude th.th_name
then errorm ~loc "duplicate prelude"
else Hid.add driver.drv_thprelude th.th_name s in
List.iter add trl
let load_driver file env = let load_driver file env =
let f = load_file file in let f = load_file file in
let printer = ref (None : printer option) in let prelude = ref None in
let printer = ref None in
let call_stdin = ref None in
let call_file = ref None in
let regexps = ref [] in
let set_or_raise loc r v error =
if !r <> None then errorm ~loc "duplicate %s" error
else r := Some v in
let add (loc, g) = match g with let add (loc, g) = match g with
| Printer _ when !printer <> None -> | Printer _ when !printer <> None ->
errorm ~loc "duplicate printer" errorm ~loc "duplicate printer"
...@@ -93,35 +194,51 @@ let load_driver file env = ...@@ -93,35 +194,51 @@ let load_driver file env =
printer := Some (Hashtbl.find printers s) printer := Some (Hashtbl.find printers s)
| Printer s -> | Printer s ->
errorm ~loc "unknown printer %s" s errorm ~loc "unknown printer %s" s
| _ -> | Prelude s -> set_or_raise loc prelude s "prelude"
() (* TODO *) | CallStdin s -> set_or_raise loc call_stdin s "callstdin"
| CallFile s -> set_or_raise loc call_file s "callfile"
| RegexpValid s -> regexps:=(s,Valid)::!regexps
| RegexpInvalid s -> regexps:=(s,Invalid)::!regexps
| RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps
| RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
in in
List.iter add f.f_global; List.iter add f.f_global;
{ drv_printer = !printer; let driver = { drv_printer = !printer;
drv_context = Context.init_context; drv_context = Context.init_context;
drv_call_stdin = None; drv_call_stdin = !call_stdin;
drv_call_file = None; drv_call_file = !call_file;
drv_regexps = []; drv_regexps = !regexps;
drv_prelude = None; drv_prelude = !prelude;
drv_rules = Hashtbl.create 17; drv_thprelude = Hid.create 16;
drv_theory = Hashtbl.create 17; drv_theory = Hid.create 16;
} drv_with_ctxt = Hid.create 16;
drv_env = env;
} in
List.iter (load_rules env driver) f.f_rules;
driver
(** querying drivers *) (** querying drivers *)
type translation = let query_ident drv id =
| Remove try
| Syntax of string Hid.find drv.drv_with_ctxt id
| Tag of string list with Not_found ->
let r = try
let query_ident dr id = Mid.find id drv.drv_context.ctxt_cloned
assert false (*TODO*) with Not_found -> Sid.empty in
let tr = try fst (Hid.find drv.drv_theory id)
with Not_found -> Tag Snm.empty in
let tr = Sid.fold
(fun id acc -> try translation_union acc
(snd (Hid.find drv.drv_theory id))
with Not_found -> acc) r tr in
Hid.add drv.drv_with_ctxt id tr;
tr
(** using drivers *) (** using drivers *)
let print_context drv = match drv.drv_printer with let print_context drv fmt ctxt = match drv.drv_printer with
| None -> errorm "no printer" | None -> errorm "no printer"
| Some f -> f drv | Some f -> f {drv with drv_context = ctxt} fmt ctxt
let call_prover drv ctx = assert false (*TODO*) let call_prover drv ctx = assert false (*TODO*)
let call_prover_on_file drv filename = assert false (*TODO*) let call_prover_on_file drv filename = assert false (*TODO*)
......
...@@ -32,7 +32,7 @@ val load_driver : string -> Typing.env -> driver ...@@ -32,7 +32,7 @@ val load_driver : string -> Typing.env -> driver
type translation = type translation =
| Remove | Remove
| Syntax of string | Syntax of string
| Tag of string list | Tag of Snm.t
val query_ident : driver -> ident -> translation val query_ident : driver -> ident -> translation
......
...@@ -27,11 +27,11 @@ type trule = ...@@ -27,11 +27,11 @@ type trule =
| Rremove of cloned * qualid | Rremove of cloned * qualid
| Rsyntax of qualid * string | Rsyntax of qualid * string
| Rtag of cloned * qualid * string | Rtag of cloned * qualid * string
| Rprelude of string | Rprelude of loc * string
type theory_rules = { type theory_rules = {
th_name : qualid; thr_name : qualid;
th_rules : trule list; thr_rules : trule list;
} }
type global = type global =
......
...@@ -66,7 +66,7 @@ list0_theory: ...@@ -66,7 +66,7 @@ list0_theory:
theory: theory:
| THEORY qualid list0_trule END | THEORY qualid list0_trule END
{ { th_name = $2; th_rules = $3 } } { { thr_name = $2; thr_rules = $3 } }
; ;
list0_trule: list0_trule:
...@@ -75,7 +75,7 @@ list0_trule: ...@@ -75,7 +75,7 @@ list0_trule:
; ;
trule: trule:
| PRELUDE STRING { Rprelude $2 } | PRELUDE STRING { Rprelude (loc (),$2) }
| REMOVE cloned qualid { Rremove ($2, $3) } | REMOVE cloned qualid { Rremove ($2, $3) }
| SYNTAX qualid STRING { Rsyntax ($2, $3) } | SYNTAX qualid STRING { Rsyntax ($2, $3) }
| TAG cloned qualid STRING { Rtag ($2, $3, $4) } | TAG cloned qualid STRING { Rtag ($2, $3, $4) }
......
...@@ -21,15 +21,6 @@ open Ty ...@@ -21,15 +21,6 @@ open Ty
open Term open Term
open Theory open Theory
let qualid_of_lstring s =
assert false (*TODO*)
(* 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 = let cloned_from_ts env ctxt l s ls1 =
assert false (*TODO*) assert false (*TODO*)
(* try *) (* try *)
......
...@@ -17,13 +17,11 @@ ...@@ -17,13 +17,11 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
val qualid_of_lstring : string list -> Ptree.qualid
val cloned_from_ts : Typing.env -> Theory.context -> val cloned_from_ts : Typing.env -> Theory.context ->
string list -> string -> Ty.tysymbol -> bool string list -> string list -> Ty.tysymbol -> bool
val cloned_from_ls : Typing.env -> Theory.context -> val cloned_from_ls : Typing.env -> Theory.context ->
string list -> string -> Term.lsymbol -> bool string list -> string list -> Term.lsymbol -> bool
val cloned_from_pr : Typing.env -> Theory.context -> val cloned_from_pr : Typing.env -> Theory.context ->
string list -> string -> Theory.prop -> bool string list -> string list -> Theory.prop -> bool
...@@ -31,4 +31,4 @@ let elt a = ...@@ -31,4 +31,4 @@ let elt a =
r r
let t = Transform.elt elt let t env = Transform.elt (fun _ -> elt) env
...@@ -19,4 +19,4 @@ ...@@ -19,4 +19,4 @@
(* a list of decl_or_use to a list of decl *) (* a list of decl_or_use to a list of decl *)
val t : Transform.ctxt_t val t : Typing.env -> Transform.ctxt_t
...@@ -118,8 +118,8 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) = ...@@ -118,8 +118,8 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
(create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla))) (create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla)))
| Duse _ | Dclone _ -> env,add_decl ctxt d | Duse _ | Dclone _ -> env,add_decl ctxt d
let t ~isnotinlinedt ~isnotinlinedf = let t ~isnotinlinedt ~isnotinlinedf env =
Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env Transform.fold_map (fun _ -> fold isnotinlinedt isnotinlinedf) empty_env env
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false) let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......
...@@ -23,17 +23,18 @@ ...@@ -23,17 +23,18 @@
val t : val t :
isnotinlinedt:(Term.term -> bool) -> isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) -> isnotinlinedf:(Term.fmla -> bool) ->
Typing.env ->
Transform.ctxt_t Transform.ctxt_t
(* Inline them all *) (* Inline them all *)
val all : Transform.ctxt_t val all : Typing.env -> Transform.ctxt_t
(* Inline only the trivial definition : (* Inline only the trivial definition :
logic c : t = a logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *) logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : Transform.ctxt_t val trivial : Typing.env -> Transform.ctxt_t
(* Function to use in other transformations if inlining is needed *) (* Function to use in other transformations if inlining is needed *)
......
...@@ -140,9 +140,4 @@ let elt d = ...@@ -140,9 +140,4 @@ let elt d =
| Dind _ -> [d] (* TODO *) | Dind _ -> [d] (* TODO *)
| Dprop _ | Dclone _ | Duse _ -> [d] | Dprop _ | Dclone _ | Duse _ -> [d]
let elt d = let t env = Transform.elt (fun _ -> elt) env
let r = elt d in
(* Format.printf "srd : %a -> %a@\n" Pretty.print_decl d Pretty.print_decl_list r;*)
r
let t = Transform.elt elt
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
(* Simplify the recursive type and logic definition *) (* Simplify the recursive type and logic definition *)
val t : Transform.ctxt_t val t : Typing.env -> Transform.ctxt_t
(* ungroup recursive definition *) (* ungroup recursive definition *)
......
...@@ -20,21 +20,29 @@ ...@@ -20,21 +20,29 @@
open Ident open Ident
open Theory open Theory
open Context open Context
open Typing
(* the memoisation is inside the function *) (* the memoisation is inside the function *)
type 'a t = { all : context -> 'a; type 'a t = { all : context -> 'a;
clear : unit -> unit; clear : unit -> unit;
env : env;
} }
type ctxt_t = context t type ctxt_t = context t
let conv_res f c = {all = (fun x -> c (f.all x)); let conv_res f c = {all = (fun x -> c (f.all x));
clear = f.clear} clear = f.clear;
env = f.env}
let compose f g = {all = (fun x -> g.all (f.all x));