Commit a4c8ef97 authored by Andrei Paskevich's avatar Andrei Paskevich

simplify the API of flag-dependent transformations (ex-private_register)

parent 84a20c62
......@@ -631,7 +631,7 @@ let find_prop_decl kn pr =
| Dprop (k,_,f) -> k,f
| _ -> assert false
exception NonExhaustiveExpr of (pattern list * expr)
exception NonExhaustiveExpr of pattern list * expr
let rec check_matchT kn () t = match t.t_node with
| Tcase (t1,bl) ->
......
......@@ -151,7 +151,7 @@ val merge_known : known_map -> known_map -> known_map
exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception NonExhaustiveExpr of (pattern list * expr)
exception NonExhaustiveExpr of pattern list * expr
exception NonFoundedTypeDecl of tysymbol
val find_constructors : known_map -> tysymbol -> lsymbol list
......
......@@ -245,7 +245,7 @@ end)
exception UnknownTrans of string
exception KnownTrans of string
exception TransFailure of (string * exn)
exception TransFailure of string * exn
let named s f (x : task) =
Debug.dprintf debug "Apply transformation %s@." s;
......@@ -280,40 +280,26 @@ let lookup_transform_l s =
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let list_transforms_l () = Hashtbl.fold (fun k _ acc -> k::acc) transforms_l []
(** private register *)
(** Flag-dependent transformations *)
type ('a,'b) private_register =
{ pr_meta : meta;
pr_default : string;
pr_table : (string,'a -> 'b trans) Hashtbl.t}
exception UnknownFlagTrans of meta * string * string list
exception IllegalFlagTrans of meta
type empty (* A type with no value *)
type ('a,'b) flag_trans = (string, 'a -> 'b trans) Hashtbl.t
exception UnknownTransPrivate of (empty,empty) private_register * string
let create_private_register meta_name d =
{ pr_meta = register_meta_excl meta_name [MTstring];
pr_table = Hashtbl.create 17;
pr_default = d}
let private_register_env pr name tr =
Hashtbl.add pr.pr_table name (fun e -> named name (tr e))
let private_register pr name tr =
Hashtbl.add pr.pr_table name (fun () -> named name tr)
let apply_private_register_env pr env =
on_meta_excl pr.pr_meta (fun alo ->
let on_flag m ft def arg =
on_meta_excl m (fun alo ->
let s = match alo with
| None -> pr.pr_default
| None -> def
| Some [MAstr s] -> s
| _ -> assert false in
try
(Hashtbl.find pr.pr_table s) env
with Not_found ->
raise (UnknownTransPrivate (Obj.magic pr,s)))
let apply_private_register opt = apply_private_register_env opt ()
| _ -> raise (IllegalFlagTrans m)
in
let t = try Hashtbl.find ft s with
| Not_found ->
let l = Hashtbl.fold (fun s _ l -> s :: l) ft [] in
raise (UnknownFlagTrans (m,s,l))
in
named s (t arg))
let () = Exn_printer.register (fun fmt exn -> match exn with
......@@ -321,12 +307,12 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Format.fprintf fmt "Transformation '%s' is already registered" s
| UnknownTrans s ->
Format.fprintf fmt "Unknown transformation '%s'" s
| UnknownTransPrivate (pr,arg) ->
Format.fprintf fmt "Wrong parameter %s@ for@ the@ meta@ %s, only@ the@ \
following@ parameters@ can@ be given@ (default: %s):@ %a"
arg pr.pr_meta.meta_name pr.pr_default
(Pp.print_iter2 Hashtbl.iter Pp.comma Pp.nothing Pp.string
Pp.nothing) pr.pr_table
| UnknownFlagTrans (m,s,l) ->
Format.fprintf fmt "Bad parameter %s for the meta %s@." s m.meta_name;
Format.fprintf fmt "Known parameters: %a"
(Pp.print_list Pp.space Pp.string) l
| IllegalFlagTrans m ->
Format.fprintf fmt "Meta %s must be exclusive string-valued" m.meta_name
| TransFailure (s,e) ->
Format.fprintf fmt "Failure in transformation %s@\n%a" s
Exn_printer.exn_printer e
......
......@@ -72,7 +72,7 @@ val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
val add_decls : decl list -> task trans
val add_tdecls : tdecl list -> task trans
(* dependent transformatons *)
(* Dependent Transformatons *)
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
val on_theory : theory -> (symbol_map list -> 'a trans) -> 'a trans
......@@ -85,14 +85,31 @@ val on_tagged_ts : meta -> (Sts.t -> 'a trans) -> 'a trans
val on_tagged_ls : meta -> (Sls.t -> 'a trans) -> 'a trans
val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
(** debug transformation *)
(* Flag-dependent Transformations *)
exception UnknownFlagTrans of meta * string * string list
exception IllegalFlagTrans of meta
type ('a,'b) flag_trans = (string, 'a -> 'b trans) Hashtbl.t
val on_flag : meta -> ('a,'b) flag_trans -> string -> 'a -> 'b trans
(** [on_flag m ft def arg] takes an exclusive meta [m] of type [[MTstring]],
a hash table [ft], a default flag value [def], and an argument [arg].
Returns a transformation that is associated in [ft] to the value of [m]
in a given task. If the meta [m] is not set in the task, returns the
transformation associated to [def]. Raises [UnknownFlagTrans] if [ft]
does not have a requested association. Raises [IllegalFlagTrans] if
the type of [m] is not [[MTstring]]. *)
(** Debug Transformations *)
val print_meta : Debug.flag -> meta -> task trans
(** [print_meta f m] is an identity transformation that
prints every meta [m] in the task if flag [d] is set *)
(** {2 Registration} *)
exception TransFailure of (string * exn)
exception TransFailure of string * exn
exception UnknownTrans of string
exception KnownTrans of string
......@@ -111,32 +128,3 @@ val list_transforms_l : unit -> string list
val named : string -> 'a trans -> 'a trans
(** give transformation a name without registering *)
(** {3 Private Registration} *)
(** Can be used for chosing a transformation from a meta *)
type ('a,'b) private_register = private
{ pr_meta : meta;
pr_default : string;
pr_table : (string,'a -> 'b trans) Hashtbl.t}
type empty
(* A type without value, an (empty,empty) private_register can't be used. *)
exception UnknownTransPrivate of (empty,empty) private_register * string
val create_private_register :
string -> string -> ('a, 'b) private_register
(** [create_provate_register meta_name default] *)
val private_register_env :
('a, 'b) private_register -> string -> ('a -> 'b trans) -> unit
val private_register :
(unit, 'b) private_register -> string -> 'b trans -> unit
val apply_private_register_env :
('a, 'b) private_register -> 'a -> 'b trans
val apply_private_register :
(unit, 'b) private_register -> 'b trans
......@@ -28,30 +28,28 @@ let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
let debug = Debug.register_flag "encoding"
let select_pr = Trans.create_private_register "enco_select" "kept"
let kept_pr = Trans.create_private_register "enco_kept" "bridge"
let poly_pr = Trans.create_private_register "enco_poly" "decorate"
let meta_enco_select = register_meta_excl "enco_select" [MTstring]
let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
let poly_smt_pr = poly_pr
let poly_tptp_pr = poly_pr
let def_enco_select_smt = "kept"
let def_enco_kept_smt = "bridge"
let def_enco_poly_smt = "decorate"
let print_kept = print_meta debug meta_kept
let enco_select env =
compose (apply_private_register_env select_pr env) print_kept
let def_enco_select_tptp = "kept"
let def_enco_kept_tptp = "bridge"
let def_enco_poly_tptp = "decorate"
let ft_enco_select = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_enco_kept = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_enco_poly = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
open Ty
open Term
let ty_all_quant =
let rec add_vs s ty = match ty.ty_node with
| Tyvar vs -> Stv.add vs s
| _ -> ty_fold add_vs s ty in
f_ty_fold add_vs Stv.empty
let monomorphise_goal =
Trans.goal (fun pr f ->
let stv = ty_all_quant f in
let stv = f_ty_freevars Stv.empty f in
let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
let ts = create_tysymbol (Ident.id_clone tv.tv_name) [] None in
Mtv.add tv (ty_app ts []) mty,ts::ltv) stv (Mtv.empty,[]) in
......@@ -62,20 +60,20 @@ let monomorphise_goal =
acc ltv in
acc)
let encoding_smt env =
Trans.seq [
monomorphise_goal;
enco_select env;
apply_private_register_env kept_pr env;
apply_private_register_env poly_smt_pr env]
let encoding_smt env = Trans.seq [
monomorphise_goal;
Trans.on_flag meta_enco_select ft_enco_select def_enco_select_smt env;
Trans.print_meta debug meta_kept;
Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
let encoding_tptp env =
Trans.seq [
monomorphise_goal;
enco_select env;
apply_private_register_env kept_pr env;
apply_private_register_env poly_tptp_pr env;
Encoding_enumeration.encoding_enumeration]
let encoding_tptp env = Trans.seq [
monomorphise_goal;
Trans.on_flag meta_enco_select ft_enco_select def_enco_select_tptp env;
Trans.print_meta debug meta_kept;
Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_tptp env;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env;
Encoding_enumeration.encoding_enumeration]
let () =
register_env_transform "encoding_smt" encoding_smt;
......
......@@ -28,13 +28,11 @@ val meta_kept : meta
val meta_kept_array : meta
val meta_base : meta
val select_pr : (env,task) Trans.private_register
val kept_pr : (env,task) Trans.private_register
val poly_pr : (env,task) Trans.private_register
val ft_enco_select : (env,task) Trans.flag_trans
val ft_enco_kept : (env,task) Trans.flag_trans
val ft_enco_poly : (env,task) Trans.flag_trans
val monomorphise_goal : Task.task Trans.trans
val encoding_smt : Env.env -> Task.task Trans.trans
val encoding_tptp : Env.env -> Task.task Trans.trans
val print_kept : Task.task Trans.trans
val encoding_smt : Env.env -> Task.task Trans.trans
......@@ -659,18 +659,20 @@ let create_env_array env thpoly task tenv kept kept_array =
(** add the clone *)
Sty.fold clone_arrays kept_array task_tenv
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
let encoding_smt_array env =
let th_array = Env.find_theory env ["array"] "Array" in
Trans.on_used_theory th_array (fun used ->
if not used then Encoding.encoding_smt env else
seq [Encoding.monomorphise_goal;
select_subterm_array th_array;
Encoding.print_kept;
Trans.print_meta Encoding.debug Encoding.meta_kept;
Encoding_instantiate.t (create_env_array env th_array);
meta_arrays_to_meta_kept;
Encoding.print_kept;
Trans.print_meta Encoding.debug Encoding.meta_kept;
Encoding_bridge.t env;
Trans.apply_private_register_env Encoding.poly_pr env])
Trans.on_flag meta_enco_poly Encoding.ft_enco_poly "decorate" env])
let () = Trans.register_env_transform "encoding_smt_array" encoding_smt_array
......
......@@ -281,5 +281,5 @@ let t env =
let init_task,tenv = load_prelude s env in
Trans.tdecl (decl tenv) init_task))
let () = Trans.private_register_env Encoding.kept_pr "bridge" t
let () = Hashtbl.replace Encoding.ft_enco_kept "bridge" t
......@@ -108,5 +108,5 @@ let t = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
let kept = Sty.add ty_type kept in
Trans.compose (deco kept) (mono kept))
let () = Trans.private_register_env Encoding.poly_pr "decorate" (const t)
let () = Hashtbl.replace Encoding.ft_enco_poly "decorate" (const t)
......@@ -183,6 +183,6 @@ let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
in
monomorph tyb)
let () = Trans.private_register_env Encoding.poly_pr "explicit"
let () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
(fun _ -> Trans.compose explicit monomorph)
......@@ -257,5 +257,5 @@ let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
in
monomorph tyb)
let () = Trans.private_register_env Encoding.poly_pr "guard"
let () = Hashtbl.replace Encoding.ft_enco_poly "guard"
(fun _ -> Trans.compose guard monomorph)
......@@ -527,15 +527,14 @@ let create_trans_complete kept complete =
let init_task,env = create_env task tenv kept in
Trans.fold_map fold_map env init_task
let encoding_instantiate _ =
let encoding_instantiate =
Trans.compose Libencoding.close_kept
(Trans.on_tagged_ty meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete kept complete)))
let () =
Trans.private_register_env Encoding.kept_pr
"instantiate" encoding_instantiate
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate"
(const encoding_instantiate)
let create_trans_complete create_env kept kept_array complete =
......@@ -601,7 +600,7 @@ let mono_in_mono = Trans.tdecl mono_in_mono None
let () =
List.iter (fun (name,t) ->
Trans.private_register_env Encoding.select_pr name (fun _ -> t))
Hashtbl.replace Encoding.ft_enco_select name (const t))
[ "kept", Trans.identity;
"goal", mono_in_goal;
"mono", mono_in_mono;
......
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