Skip to content

GitLab

Commit f7ae2401 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

rework translations in Driver, adapt the printers

parent 3595c4f7
Hide whitespace changes
Inline Side-by-side
src/driver/driver.ml
View file @ f7ae2401
......@@ -106,34 +106,28 @@ let syntax_arguments s print fmt l =
(** drivers *)
type translation =
| Remove
| Syntax of string
| Tag of Sstr.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 (Sstr.union s1 s2)
let print_translation fmt = function
| Remove -> Format.fprintf fmt "remove"
| Syntax s -> Format.fprintf fmt "syntax %s" s
| Tag s -> Format.fprintf fmt "tag %a"
(Pp.print_iter1 Sstr.iter Pp.comma Pp.string) s
type driver_query = {
query_syntax : ident -> string option;
query_remove : ident -> bool;
query_tags : ident -> Sstr.t;
}
type printer = (ident -> translation) -> Format.formatter -> task -> unit
type printer = driver_query -> Format.formatter -> task -> unit
type driver = {
drv_env : Env.env;
drv_printer : printer option;
drv_prelude : string list;
drv_filename : string option;
drv_transform : task trans_reg;
drv_thprelude : string list Mid.t;
drv_translations : (translation * translation) Mid.t;
drv_regexps : (Str.regexp * Call_provers.prover_answer) list;
drv_exitcodes : (int * Call_provers.prover_answer) list;
drv_env : Env.env;
drv_printer : printer option;
drv_prelude : string list;
drv_filename : string option;
drv_transform : task trans_reg;
drv_thprelude : string list Mid.t;
drv_tags : Sstr.t Mid.t;
drv_tags_cl : Sstr.t Mid.t;
drv_syntax : string Mid.t;
drv_remove : Sid.t;
drv_remove_cl : Sid.t;
drv_regexps : (Str.regexp * Call_provers.prover_answer) list;
drv_exitcodes : (int * Call_provers.prover_answer) list;
}
(** register printers and transformations *)
......@@ -169,56 +163,6 @@ let load_file file =
let string_of_qualid thl idl =
String.concat "." thl ^ "." ^ String.concat "." idl
let add_htheory tmap cloned id t =
try
let t2,t3 = Mid.find id tmap in
let t23 = if cloned
then translation_union t t2, t3
else t2, translation_union t t3
in
Mid.add id t23 tmap
with Not_found ->
let t23 = if cloned
then Tag Sstr.empty, t
else t, Tag Sstr.empty
in
Mid.add id t23 tmap
let load_rules env (pmap,tmap) { thr_name = (loc,qualid); thr_rules = trl } =
let qfile,id = let l = List.rev qualid in List.rev (List.tl l),List.hd l in
let th = try Env.find_theory env qfile id with Env.TheoryNotFound (l,s) ->
errorm ~loc "theory %s.%s not found" (String.concat "." l) s
in
let find_pr (loc,q) = try ns_find_pr th.th_export q with Not_found ->
errorm ~loc "Unknown proposition %s" (string_of_qualid qualid q)
in
let find_ls (loc,q) = try ns_find_ls th.th_export q with Not_found ->
errorm ~loc "Unknown logic symbol %s" (string_of_qualid qualid q)
in
let find_ts (loc,q) = try ns_find_ts th.th_export q with Not_found ->
errorm ~loc "Unknown type symbol %s" (string_of_qualid qualid q)
in
let add (pmap,tmap) (loc,rule) = match rule with
| Rremove (c,q) ->
pmap, add_htheory tmap c (find_pr q).pr_name Remove
| Rsyntaxls (q,s) -> let ls = find_ls q in
check_syntax loc s (List.length ls.ls_args);
pmap, add_htheory tmap false ls.ls_name (Syntax s)
| Rsyntaxty (q,s) -> let ts = find_ts q in
check_syntax loc s (List.length ts.ts_args);
pmap, add_htheory tmap false ts.ts_name (Syntax s)
| Rtagls (c,q,s) ->
pmap, add_htheory tmap c (find_ls q).ls_name (Tag (Sstr.singleton s))
| Rtagty (c,q,s) ->
pmap, add_htheory tmap c (find_ts q).ts_name (Tag (Sstr.singleton s))
| Rtagpr (c,q,s) ->
pmap, add_htheory tmap c (find_pr q).pr_name (Tag (Sstr.singleton s))
| Rprelude s ->
let l = try Mid.find th.th_name pmap with Not_found -> [] in
Mid.add th.th_name (s::l) pmap, tmap
in
List.fold_left add (pmap,tmap) trl
let load_driver env file =
let prelude = ref [] in
let regexps = ref [] in
......@@ -226,12 +170,13 @@ let load_driver env file =
let filename = ref None in
let printer = ref None in
let transform = ref identity in
let set_or_raise loc r v error = match !r with
| Some _ -> errorm ~loc "duplicate %s" error
| None -> r := Some v
in
let add_to_list r v = (r := v :: !r) in
let add (loc, g) = match g with
let add_global (loc, g) = match g with
| Prelude s -> add_to_list prelude s
| RegexpValid s -> add_to_list regexps (Str.regexp s, Valid)
| RegexpInvalid s -> add_to_list regexps (Str.regexp s, Invalid)
......@@ -253,43 +198,106 @@ let load_driver env file =
| Plugin files -> load_plugin (Filename.dirname file) files
in
let f = load_file file in
List.iter add f.f_global;
let (pmap,tmap) =
List.fold_left (load_rules env) (Mid.empty,Mid.empty) f.f_rules
List.iter add_global f.f_global;
let thprelude = ref Mid.empty in
let tags = ref Mid.empty in
let tags_cl = ref Mid.empty in
let syntax = ref Mid.empty in
let remove = ref Sid.empty in
let remove_cl = ref Sid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try ns_find_pr th.th_export q with Not_found ->
errorm ~loc "unknown proposition %s" (string_of_qualid !qualid q)
in
let find_ls th (loc,q) = try ns_find_ls th.th_export q with Not_found ->
errorm ~loc "unknown logic symbol %s" (string_of_qualid !qualid q)
in
let find_ts th (loc,q) = try ns_find_ts th.th_export q with Not_found ->
errorm ~loc "unknown type symbol %s" (string_of_qualid !qualid q)
in
let add_syntax loc k (_,q) id n s =
check_syntax loc s n;
if Mid.mem id !syntax then
errorm ~loc "duplicate syntax rule for %s symbol %s"
k (string_of_qualid !qualid q);
syntax := Mid.add id s !syntax
in
let add_tag c id s =
let mr = if c then tags_cl else tags in
let im = try Mid.find id !mr with Not_found -> Sstr.empty in
mr := Mid.add id (Sstr.add s im) !mr
in
let add_local th (loc,rule) = match rule with
| Rprelude s ->
let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxls (q,s) ->
let ls = find_ls th q in
add_syntax loc "logic" q ls.ls_name (List.length ls.ls_args) s
| Rsyntaxts (q,s) ->
let ts = find_ts th q in
add_syntax loc "type" q ts.ts_name (List.length ts.ts_args) s
| Rremovepr (c,q) ->
let sr = if c then remove_cl else remove in
sr := Sid.add (find_pr th q).pr_name !sr
| Rtagts (c,q,s) -> add_tag c (find_ts th q).ts_name s
| Rtagls (c,q,s) -> add_tag c (find_ls th q).ls_name s
| Rtagpr (c,q,s) -> add_tag c (find_pr th q).pr_name s
in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th = try Env.find_theory env f id with Env.TheoryNotFound (l,s) ->
errorm ~loc "theory %s.%s not found" (String.concat "." l) s
in
qualid := q;
List.iter (add_local th) trl
in
List.iter add_theory f.f_rules;
{
drv_env = env;
drv_printer = !printer;
drv_prelude = !prelude;
drv_filename = !filename;
drv_transform = !transform;
drv_thprelude = pmap;
drv_translations = tmap;
drv_regexps = !regexps;
drv_exitcodes = !exitcodes;
drv_env = env;
drv_printer = !printer;
drv_prelude = !prelude;
drv_filename = !filename;
drv_transform = !transform;
drv_thprelude = !thprelude;
drv_tags = !tags;
drv_tags_cl = !tags_cl;
drv_syntax = !syntax;
drv_remove = !remove;
drv_remove_cl = !remove_cl;
drv_regexps = !regexps;
drv_exitcodes = !exitcodes;
}
(** querying drivers *)
let query_ident drv clone =
let h = Hid.create 7 in
fun id ->
try
Hid.find h id
with Not_found ->
let r = try
Mid.find id clone
with Not_found -> Sid.empty in
let tr = try fst (Mid.find id drv.drv_translations)
with Not_found -> Tag Sstr.empty in
let tr = Sid.fold
(fun id acc -> try translation_union acc
(snd (Mid.find id drv.drv_translations))
with Not_found -> acc) r tr in
Hid.add h id tr;
tr
(** using drivers *)
(** query drivers *)
let get_tags map id = try Mid.find id map with Not_found -> Sstr.empty
let add_tags drv id acc = Sstr.union (get_tags drv.drv_tags_cl id) acc
let add_remove drv id acc = acc || Sid.mem id drv.drv_remove_cl
let query_driver drv clone =
let htags = Hid.create 7 in
let query_tags id = try Hid.find htags id with Not_found ->
let r = try Mid.find id clone with Not_found -> Sid.empty in
let s = Sid.fold (add_tags drv) r (get_tags drv.drv_tags id) in
Hid.replace htags id s; s
in
let hremove = Hid.create 7 in
let query_remove id = try Hid.find hremove id with Not_found ->
let r = try Mid.find id clone with Not_found -> Sid.empty in
let s = Sid.fold (add_remove drv) r (Sid.mem id drv.drv_remove) in
Hid.replace hremove id s; s
in
let query_syntax id =
try Some (Mid.find id drv.drv_syntax) with Not_found -> None
in
{ query_syntax = query_syntax;
query_remove = query_remove;
query_tags = query_tags }
(** apply drivers *)
let print_prelude drv used fmt =
let pr_pr s () = Format.fprintf fmt "%s@\n" s in
......@@ -313,7 +321,7 @@ let print_task drv fmt task =
let task = apply_env drv.drv_transform drv.drv_env task in
let printer = match drv.drv_printer with
| None -> errorm "no printer specified in the driver file"
| Some p -> p (query_ident drv (task_clone task))
| Some p -> p (query_driver drv (task_clone task))
in
print_prelude drv (task_used task) fmt;
Format.fprintf fmt "@[%a@]@?" printer task
......
src/driver/driver.mli
View file @ f7ae2401
......@@ -20,6 +20,7 @@
(** Drivers for calling external provers *)
open Format
open Util
open Ident
open Task
open Trans
......@@ -37,11 +38,6 @@ val load_driver : env -> string -> driver
(** {2 query a driver} *)
type translation =
| Remove
| Syntax of string
| Tag of Util.Sstr.t
val syntax_arguments : string -> (formatter -> 'a -> unit) ->
formatter -> 'a list -> unit
(** (syntax_argument templ print_arg fmt l) prints in the formatter fmt
......@@ -49,7 +45,13 @@ val syntax_arguments : string -> (formatter -> 'a -> unit) ->
(** {2 register printers and transformations} *)
type printer = (ident -> translation) -> formatter -> task -> unit
type driver_query = {
query_syntax : ident -> string option;
query_remove : ident -> bool;
query_tags : ident -> Sstr.t;
}
type printer = driver_query -> formatter -> task -> unit
val register_printer : string -> printer -> unit
......
src/driver/driver_ast.ml
View file @ f7ae2401
......@@ -23,18 +23,18 @@ type qualid = loc * string list
type cloned = bool
type trule =
| Rremove of cloned * qualid
| Rsyntaxty of qualid * string
type th_rule =
| Rprelude of string
| Rsyntaxts of qualid * string
| Rsyntaxls of qualid * string
| Rtagty of cloned * qualid * string
| Rremovepr of cloned * qualid
| Rtagts of cloned * qualid * string
| Rtagls of cloned * qualid * string
| Rtagpr of cloned * qualid * string
| Rprelude of string
type theory_rules = {
thr_name : qualid;
thr_rules : (loc * trule) list;
thr_rules : (loc * th_rule) list;
}
type global =
......
src/driver/driver_parser.mly
View file @ f7ae2401
......@@ -85,10 +85,10 @@ list0_trule:
trule:
| PRELUDE STRING { Rprelude ($2) }
| REMOVE cloned PROP qualid { Rremove ($2, $4) }
| SYNTAX TYPE qualid STRING { Rsyntaxty ($3, $4) }
| SYNTAX TYPE qualid STRING { Rsyntaxts ($3, $4) }
| SYNTAX LOGIC qualid STRING { Rsyntaxls ($3, $4) }
| TAG cloned TYPE qualid STRING { Rtagty ($2, $4, $5) }
| REMOVE cloned PROP qualid { Rremovepr ($2, $4) }
| TAG cloned TYPE qualid STRING { Rtagts ($2, $4, $5) }
| TAG cloned LOGIC qualid STRING { Rtagls ($2, $4, $5) }
| TAG cloned PROP qualid STRING { Rtagpr ($2, $4, $5) }
;
......
src/printer/alt_ergo.ml
View file @ f7ae2401
......@@ -49,25 +49,16 @@ let forget_var v = forget_id ident_printer v.vs_name
let rec print_type drv fmt ty = match ty.ty_node with
| Tyvar id ->
print_tvsymbols fmt id
| Tyapp (ts, tl) ->
match drv ts.ts_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_type drv) fmt tl
| Driver.Tag _ ->
begin
match ty.ty_node with
| Tyvar _ -> assert false
| Tyapp (ts,[]) ->
print_ident fmt ts.ts_name
| Tyapp (ts, [ty]) ->
fprintf fmt "%a %a" (print_type drv)
ty print_ident ts.ts_name
| Tyapp (ts, tyl) ->
fprintf fmt "(%a) %a"
(print_list comma (print_type drv))
tyl print_ident ts.ts_name
end
| Tyapp (ts, tl) -> begin match drv.Driver.query_syntax ts.ts_name with
| Some s -> Driver.syntax_arguments s (print_type drv) fmt tl
| None -> fprintf fmt "%a%a" (print_tyapp drv) tl print_ident ts.ts_name
end
and print_tyapp drv fmt = function
| [] -> ()
| [ty] -> fprintf fmt "%a " (print_type drv) ty
| tl -> fprintf fmt "(%a) " (print_list comma (print_type drv)) tl
let rec print_term drv fmt t = match t.t_node with
| Tbvar _ ->
assert false
......@@ -75,19 +66,10 @@ let rec print_term drv fmt t = match t.t_node with
Pretty.print_const fmt c
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp (ls, tl) ->
begin
match drv ls.ls_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_term drv) fmt tl
| Driver.Tag _ ->
match tl with
| [] -> print_ident fmt ls.ls_name
| tl ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma (print_term drv)) tl
end
| Tapp (ls, tl) -> begin match drv.Driver.query_syntax ls.ls_name with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp drv) tl
end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
......@@ -100,19 +82,18 @@ let rec print_term drv fmt t = match t.t_node with
| Teps _ ->
assert false
and print_tapp drv fmt = function
| [] -> ()
| tl -> fprintf fmt "(%a)" (print_list comma (print_term drv)) tl
let rec print_fmla drv fmt f = match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
| Fapp (ls, tl) ->
begin
match drv ls.ls_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_term drv) fmt tl
| Driver.Tag _ ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma (print_term drv)) tl
end
| Fapp (ls, tl) -> begin match drv.Driver.query_syntax ls.ls_name with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "%a(%a)" print_ident ls.ls_name
(print_list comma (print_term drv)) tl
end
| Fquant (q, fq) ->
let q = match q with Fforall -> "forall" | Fexists -> "exists" in
let vl, tl, f = f_open_quant fq in
......@@ -156,63 +137,58 @@ and print_triggers drv fmt tl =
let print_logic_binder drv fmt v =
fprintf fmt "%a: %a" print_ident v.vs_name (print_type drv) v.vs_ty
let print_type_decl fmt ts = match ts.ts_args with
| [] -> fprintf fmt "type %a" print_ident ts.ts_name
| tl -> fprintf fmt "type (%a) %a"
(print_list comma print_tvsymbols) tl print_ident ts.ts_name
let print_type_decl drv fmt = function
| ts, Tabstract ->
begin
match drv ts.ts_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag _ ->
match ts.ts_args with
| [] -> fprintf fmt "type %a" print_ident ts.ts_name; true
| _ -> fprintf fmt "type (%a) %a"
(print_list comma print_tvsymbols) ts.ts_args
print_ident ts.ts_name; true
end
| _, Talgebraic _ ->
assert false
| ts, Tabstract when drv.Driver.query_syntax ts.ts_name <> None -> false
| ts, Tabstract -> print_type_decl fmt ts; true
| _, Talgebraic _ -> assert false
let ac_th = ["algebra";"AC"]
let print_logic_decl drv _task fmt (ls,ld) =
match drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag s ->
begin match ld with
| None ->
let sac = if Util.Sstr.mem "AC" s then "ac " else "" in
fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
sac print_ident ls.ls_name
(print_list comma (print_type drv)) ls.ls_args
(if ls.ls_args = [] then "" else " -> ")
(print_option_or_default "prop" (print_type drv)) ls.ls_value
| Some ld ->
let vl,e = open_ls_defn ld in
begin match e with
| Term t ->
(* TODO AC? *)
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_type drv) (Util.of_option ls.ls_value)
(print_term drv) t
| Fmla f ->
fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_fmla drv) f
end;
List.iter forget_var vl
let print_logic_decl drv fmt (ls,ld) =
let tags = drv.Driver.query_tags ls.ls_name in
match ld with
| None ->
let sac = if Util.Sstr.mem "AC" tags then "ac " else "" in
fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
sac print_ident ls.ls_name
(print_list comma (print_type drv)) ls.ls_args
(if ls.ls_args = [] then "" else " -> ")
(print_option_or_default "prop" (print_type drv)) ls.ls_value
| Some ld ->
let vl,e = open_ls_defn ld in
begin match e with
| Term t ->
(* TODO AC? *)
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_type drv) (Util.of_option ls.ls_value)
(print_term drv) t
| Fmla f ->
fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_fmla drv) f
end;
true
let print_decl drv task fmt d = match d.d_node with
List.iter forget_var vl
let print_logic_decl drv fmt d =
match drv.Driver.query_syntax (fst d).ls_name with
| Some _ -> false
| None -> print_logic_decl drv fmt d; true
let print_decl drv fmt d = match d.d_node with
| Dtype dl ->
print_list_opt newline (print_type_decl drv) fmt dl
| Dlogic dl ->
print_list_opt newline (print_logic_decl drv task) fmt dl
print_list_opt newline (print_logic_decl drv) fmt dl
| Dind _ -> assert false (* TODO *)
| Dprop (Paxiom, pr, _) when
drv pr.pr_name = Driver.Remove -> false
| Dprop (Paxiom, pr, _) when drv.Driver.query_remove pr.pr_name -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla drv) f; true
......@@ -224,7 +200,7 @@ let print_decl drv task fmt d = match d.d_node with
let print_task drv fmt task =
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv task) fmt decls)
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
let () = Driver.register_printer "alt-ergo"
(fun drv fmt task ->
......
src/printer/coq.ml
View file @ f7ae2401
......@@ -76,14 +76,12 @@ let print_pr fmt pr =
let rec print_ty drv fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) ->
begin match drv ts.ts_name with
| Syntax s -> syntax_arguments s (print_ty drv) fmt tl
| _ ->
begin match tl with
| Tyapp (ts, tl) -> begin match drv.Driver.query_syntax ts.ts_name with
| Some s -> syntax_arguments s (print_ty drv) fmt tl
| None -> begin match tl with
| [] -> print_ts fmt ts
| l -> fprintf fmt "(%a@ %a)" print_ts ts
(print_list space (print_ty drv)) l
(print_list space (print_ty drv)) l
end
end
......@@ -115,9 +113,8 @@ let rec print_pat drv fmt p = match p.pat_node with
| Pwild -> fprintf fmt "_"
| Pvar v -> print_vs fmt v
| Pas (p,v) -> fprintf fmt "%a as %a" (print_pat drv) p print_vs v
| Papp (cs,pl) ->
begin match drv cs.ls_name with
| Syntax s -> syntax_arguments s (print_pat drv) fmt pl
| Papp (cs,pl) -> begin match drv.query_syntax cs.ls_name with
| Some s -> syntax_arguments s (print_pat drv) fmt pl
| _ -> fprintf fmt "%a%a"
print_ls cs (print_paren_r (print_pat drv)) pl
end
......@@ -162,7 +159,7 @@ and print_tnode opl opr drv fmt t = match t.t_node with
| Tvar v ->
print_vs fmt v
| Tconst (ConstInt n) -> fprintf fmt "%s%%Z" n
| Tconst (ConstReal c) ->
| Tconst (ConstReal c) ->
Print_real.print_with_integers
"(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c
| Tif (f,t1,t2) ->
......@@ -183,8 +180,8 @@ and print_tnode opl opr drv fmt t = match t.t_node with
(print_vsty drv) v (print_opl_fmla drv) f;
forget_var v
| Tapp (fs, tl) ->
begin match drv fs.ls_name with
| Syntax s