Commit 84a20c62 authored by François Bobot's avatar François Bobot

Trans: Add private registration and use it in Encoding. Add Trans.seq.

parent ef43f13a
......@@ -46,6 +46,9 @@ let singleton f x = [f x]
let compose f g x = g (f x)
let compose_l f g x = list_apply g (f x)
let seq l x = List.fold_left (|>) x l
let seq_l l x = List.fold_left (fun x f -> list_apply f x) [x] l
module Wtask = Hashweak.Make (struct
type t = task_hd
let tag t = t.task_tag
......@@ -277,11 +280,53 @@ 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 *)
type ('a,'b) private_register =
{ pr_meta : meta;
pr_default : string;
pr_table : (string,'a -> 'b trans) Hashtbl.t}
type empty (* A type with no value *)
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 s = match alo with
| None -> pr.pr_default
| 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 ()
let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownTrans s ->
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
| TransFailure (s,e) ->
Format.fprintf fmt "Failure in transformation %s@\n%a" s
Exn_printer.exn_printer e
......
......@@ -37,9 +37,14 @@ val identity_l : task tlist
val singleton : 'a trans -> 'a tlist
val return : 'a -> 'a trans
(** Compose transformation *)
val compose : task trans -> 'a trans -> 'a trans
val compose_l : task tlist -> 'a tlist -> 'a tlist
val seq : task trans list -> task trans
val seq_l : task tlist list -> task tlist
(** Create Transformation *)
val fold : (task_hd -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
......@@ -106,3 +111,32 @@ 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,41 +28,16 @@ let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
let debug = Debug.register_flag "encoding"
type enco_opt =
{ meta : meta;
default : string;
table : (string,env -> task trans) Hashtbl.t}
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 enco_opt s d =
let table = Hashtbl.create 17 in
{ meta = register_meta_excl (Format.sprintf "enco_%s" s) [MTstring];
table = table;
default = d},
Hashtbl.add table
let select_opt,register_enco_select = enco_opt "select" "kept"
let kept_opt,register_enco_kept = enco_opt "kept" "bridge"
let poly_opt,register_enco_poly = enco_opt "poly" "decorate"
let poly_smt_opt = poly_opt
let poly_tptp_opt = poly_opt
let enco_gen opt env =
Trans.on_meta_excl opt.meta (fun alo ->
let s = match alo with
| None -> opt.default
| Some [MAstr s] -> s
| _ -> assert false in
try
Trans.named s ((Hashtbl.find opt.table s) env)
with Not_found -> failwith
(Format.sprintf "encoding : %s wrong argument %s" opt.meta.meta_name s))
let poly_smt_pr = poly_pr
let poly_tptp_pr = poly_pr
let print_kept = print_meta debug meta_kept
let enco_select env = compose (enco_gen select_opt env) print_kept
let enco_kept = enco_gen kept_opt
let enco_poly_smt = enco_gen poly_smt_opt
let enco_poly_tptp = enco_gen poly_tptp_opt
let enco_select env =
compose (apply_private_register_env select_pr env) print_kept
open Ty
......@@ -88,16 +63,19 @@ let monomorphise_goal =
acc)
let encoding_smt env =
compose monomorphise_goal
(compose (enco_select env)
(compose (enco_kept env) (enco_poly_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_tptp env =
compose monomorphise_goal
(compose (enco_select env)
(compose (enco_kept env)
(compose (enco_poly_tptp env)
Encoding_enumeration.encoding_enumeration)))
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 () =
register_env_transform "encoding_smt" encoding_smt;
......
......@@ -28,14 +28,13 @@ val meta_kept : meta
val meta_kept_array : meta
val meta_base : meta
val register_enco_select : string -> (env -> task trans) -> unit
val register_enco_kept : string -> (env -> task trans) -> unit
val register_enco_poly : string -> (env -> task trans) -> unit
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 monomorphise_goal : Task.task Trans.trans
val enco_poly_smt : Env.env -> Task.task Trans.trans
val print_kept : Task.task Trans.trans
val encoding_smt : Env.env -> Task.task Trans.trans
......@@ -663,15 +663,14 @@ 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
compose Encoding.monomorphise_goal
(compose (select_subterm_array th_array)
(compose Encoding.print_kept
(compose (Encoding_instantiate.t
(create_env_array env th_array))
(compose meta_arrays_to_meta_kept
(compose Encoding.print_kept
(compose (Encoding_bridge.t env)
(Encoding.enco_poly_smt env))))))))
seq [Encoding.monomorphise_goal;
select_subterm_array th_array;
Encoding.print_kept;
Encoding_instantiate.t (create_env_array env th_array);
meta_arrays_to_meta_kept;
Encoding.print_kept;
Encoding_bridge.t env;
Trans.apply_private_register_env Encoding.poly_pr 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 () = register_enco_kept "bridge" t
let () = Trans.private_register_env Encoding.kept_pr "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 () = Encoding.register_enco_poly "decorate" (const t)
let () = Trans.private_register_env Encoding.poly_pr "decorate" (const t)
......@@ -183,6 +183,6 @@ let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
in
monomorph tyb)
let () = Encoding.register_enco_poly "explicit"
let () = Trans.private_register_env Encoding.poly_pr "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 () = Encoding.register_enco_poly "guard"
let () = Trans.private_register_env Encoding.poly_pr "guard"
(fun _ -> Trans.compose guard monomorph)
......@@ -527,14 +527,15 @@ 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 () =
register_enco_kept "instantiate" (fun _ -> encoding_instantiate)
Trans.private_register_env Encoding.kept_pr
"instantiate" encoding_instantiate
let create_trans_complete create_env kept kept_array complete =
......@@ -599,7 +600,8 @@ let mono_in_mono d =
let mono_in_mono = Trans.tdecl mono_in_mono None
let () =
List.iter (fun (name,t) -> register_enco_select name (fun _ -> t))
List.iter (fun (name,t) ->
Trans.private_register_env Encoding.select_pr name (fun _ -> 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