Commit d435e1a4 authored by Andrei Paskevich's avatar Andrei Paskevich

hopefully a better way to accomodate Metitarski (SPASS+T, etc)

parent a39b8c95
......@@ -34,18 +34,13 @@ transformation "eliminate_let"
transformation "simplify_unknown_lsymbols"
transformation "discriminate"
transformation "encoding_metitarski"
(*
transformation "encoding_tptp"
transformation "encoding_sort"
transformation "encoding_smt"
*)
theory BuiltIn
(* support for integers disabled because may be inconsistent
meta "encoding : kept" type int
*)
meta "encoding : kept" type real
meta "encoding : base" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
......@@ -265,4 +260,4 @@ theory int.Int
remove prop ZeroLessOne
end
*)
\ No newline at end of file
*)
......@@ -77,16 +77,8 @@ let encoding_tptp env = Trans.seq [
forget_kept;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
let encoding_metitarski env = Trans.seq [
Libencoding.monomorphise_goal;
(* forget_kept; *)
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
let () = register_env_transform "encoding_smt" encoding_smt
~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts."
let () = register_env_transform "encoding_tptp" encoding_tptp
~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."
let () = register_env_transform "encoding_metitarski" encoding_metitarski
~desc:"Encode@ polymorphic@ types@ for@ prover@ metitarski."
......@@ -87,12 +87,16 @@ let deco kept = Trans.decl (deco_decl kept) deco_init
(** Monomorphisation *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
let ty_base = ty_app ts_base []
let ts_deco = create_tysymbol (id_fresh "deco") [] None
let ty_deco = ty_app ts_deco []
let ls_deco = create_fsymbol (id_fresh "sort") [ty_type;ty_base] ty_deco
(* monomorphise a logical symbol *)
let lsmap kept = Wls.memoize 63 (fun ls ->
let lsmap kept = Hls.memo 63 (fun ls ->
if ls_equal ls ls_poly_deco then ls_deco else
let prot_arg = is_protecting_id ls.ls_name in
let prot_val = is_protected_id ls.ls_name in
......@@ -104,16 +108,14 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
&& List.for_all2 ty_equal tyl ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) tyl tyr)
let d_ts_deco = create_ty_decl ts_deco
let mono_init =
let init = Task.add_decl None d_ts_base in
let init = Task.add_decl init d_ts_deco in
let init = Task.add_decl None (create_ty_decl ts_base) in
let init = Task.add_decl init (create_ty_decl ts_deco) in
init
let mono kept =
let kept = Sty.add ty_type kept in
Trans.decl (d_monomorph kept (lsmap kept)) mono_init
Trans.decl (d_monomorph ty_base kept (lsmap kept)) mono_init
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.compose (deco kept) (mono kept))
......
......@@ -22,10 +22,15 @@ let debug = Debug.register_info_flag "encoding"
let meta_kept = register_meta "encoding : kept" [MTty]
~desc:"Specify@ a@ type@ to@ keep@ during@ polymorphism@ encoding."
(* sort symbol of the "universal" type *)
(* meta to tag the custom base type *)
let meta_base = register_meta_excl "encoding : base" [MTty]
~desc:"Specify@ the@ base@ type@ for@ monomorphic@ \
polymorphism@ encoding@ (`int'@ or@ `real'@ only)."
(* sort symbol of the default base type *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
(* "universal" sort *)
(* default base type *)
let ty_base = ty_app ts_base []
(* ts_base declaration *)
......@@ -77,17 +82,14 @@ let lsdecl_of_ts ts = create_param_decl (ls_of_ts ts)
(* convert a constant to a functional symbol of type ty_base *)
let ls_of_const =
let ht = Hterm.create 63 in
fun t -> match t.t_node with
Hty.memo 3 (fun ty_base ->
Hterm.memo 63 (fun t -> match t.t_node with
| Tconst _ ->
let t = t_label Slab.empty t in
begin try Hterm.find ht t with Not_found ->
let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
let ls = create_fsymbol (id_fresh s) [] ty_base in
Hterm.add ht t ls;
ls
end
| _ -> assert false
let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
create_fsymbol (id_fresh s) [] ty_base
| _ -> assert false))
let ls_of_const ty_base t = ls_of_const ty_base (t_label Slab.empty t)
(* unprotected and unprotecting idents *)
......@@ -108,19 +110,20 @@ let is_protected_ls kept ls =
(* monomorphise modulo the set of kept types * and an lsymbol map *)
let vs_monomorph kept vs =
if is_protected_vs kept vs then vs else
create_vsymbol (id_clone vs.vs_name) ty_base
let vs_monomorph ty_base kept vs =
if ty_equal vs.vs_ty ty_base || is_protected_vs kept vs
then vs else create_vsymbol (id_clone vs.vs_name) ty_base
let rec t_monomorph kept lsmap consts vmap t =
let t_mono = t_monomorph kept lsmap consts in
t_label_copy t (match t.t_node with
let t_monomorph ty_base kept lsmap consts vmap t =
let rec t_mono vmap t = t_label_copy t (match t.t_node with
| Tvar v ->
Mvs.find v vmap
| Tconst _ when ty_equal (t_type t) ty_base ->
t
| Tconst _ when Sty.mem (t_type t) kept ->
t
| Tconst _ ->
let ls = ls_of_const t in
let ls = ls_of_const ty_base t in
consts := Sls.add ls !consts;
fs_app ls [] ty_base
| Tapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
......@@ -132,19 +135,19 @@ let rec t_monomorph kept lsmap consts vmap t =
t_if (t_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
| Tlet (t1,b) ->
let u,t2,close = t_open_bound_cb b in
let v = vs_monomorph kept u in
let v = vs_monomorph ty_base kept u in
let t2 = t_mono (Mvs.add u (t_var v) vmap) t2 in
t_let (t_mono vmap t1) (close v t2)
| Tcase _ ->
Printer.unsupportedTerm t "no match expressions at this point"
| Teps b ->
let u,f,close = t_open_bound_cb b in
let v = vs_monomorph kept u in
let v = vs_monomorph ty_base kept u in
let f = t_mono (Mvs.add u (t_var v) vmap) f in
t_eps (close v f)
| Tquant (q,b) ->
let ul,tl,f1,close = t_open_quant_cb b in
let vl = List.map (vs_monomorph kept) ul in
let vl = List.map (vs_monomorph ty_base kept) ul in
let add acc u v = Mvs.add u (t_var v) acc in
let vmap = List.fold_left2 add vmap ul vl in
let tl = tr_map (t_mono vmap) tl in
......@@ -153,13 +156,12 @@ let rec t_monomorph kept lsmap consts vmap t =
t_binary op (t_mono vmap f1) (t_mono vmap f2)
| Tnot f1 ->
t_not (t_mono vmap f1)
| Ttrue | Tfalse ->
t)
| Ttrue | Tfalse -> t) in
t_mono vmap t
let d_monomorph kept lsmap d =
let d_monomorph ty_base kept lsmap d =
let consts = ref Sls.empty in
let kept = Sty.add ty_base kept in
let t_mono = t_monomorph kept lsmap consts in
let t_mono = t_monomorph ty_base kept lsmap consts in
let dl = match d.d_node with
| Dtype { ts_def = Some _ } -> []
| Dtype ts when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> []
......@@ -174,7 +176,7 @@ let d_monomorph kept lsmap d =
let conv (ls,ld) =
let ls = if ls_equal ls ps_equ then ls else lsmap ls in
let ul,e,close = open_ls_defn_cb ld in
let vl = List.map (vs_monomorph kept) ul in
let vl = List.map (vs_monomorph ty_base kept) ul in
let add acc u v = Mvs.add u (t_var v) acc in
let vmap = List.fold_left2 add Mvs.empty ul vl in
close ls vl (t_mono vmap e)
......@@ -190,7 +192,7 @@ let d_monomorph kept lsmap d =
let add ls acc = create_param_decl ls :: acc in
Sls.fold add !consts dl
let lsmap kept = Wls.memoize 63 (fun ls ->
let lsmap ty_base kept = Hls.memo 63 (fun ls ->
let prot_arg = is_protecting_id ls.ls_name in
let prot_val = is_protected_id ls.ls_name in
let neg ty = if prot_arg && Sty.mem ty kept then ty else ty_base in
......@@ -203,10 +205,20 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
(* replace all non-kept types with ty_base *)
let monomorphise_task =
Trans.on_meta_excl meta_base (fun base ->
let ty_base, d_ts_base = match base with
| Some [MAty ({ty_node = Tyapp (ts,[])} as ty)]
when ts_equal ts ts_int || ts_equal ts ts_real ->
ty, create_ty_decl ts
| Some [MAty _] -> Loc.errorm
"the \"enconding : base\" meta can only apply to `int' or `real'"
| Some _ -> assert false
| None -> ty_base, d_ts_base in
Trans.on_tagged_ty meta_kept (fun kept ->
let kept = Sty.add ty_type kept in
let decl = d_monomorph kept (lsmap kept) in
Trans.decl decl (Task.add_decl None d_ts_base))
let lsmap = lsmap ty_base kept in
let decl = d_monomorph ty_base kept lsmap in
Trans.decl decl (Task.add_decl None d_ts_base)))
(* replace type variables in a goal with fresh type constants *)
let monomorphise_goal = Trans.goal (fun pr f ->
......
......@@ -18,14 +18,8 @@ val debug : Debug.flag
(* meta to tag the protected types *)
val meta_kept : Theory.meta
(* sort symbol of the "universal" type *)
val ts_base : tysymbol
(* "universal" sort *)
val ty_base : ty
(* ts_base type declaration *)
val d_ts_base : decl
(* meta to tag the custom base type *)
val meta_base : Theory.meta
(* sort symbol of (polymorphic) types *)
val ts_type : tysymbol
......@@ -66,8 +60,8 @@ val is_protecting_id : Ident.ident -> bool
val is_protected_vs : Sty.t -> vsymbol -> bool
val is_protected_ls : Sty.t -> lsymbol -> bool
(* monomorphise wrt the set of kept types, and a symbol map *)
val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
(* monomorphise wrt the base type, the set of kept types, and a symbol map *)
val d_monomorph : ty -> Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
(* replace all non-kept types with ty_base *)
val monomorphise_task : Task.task Trans.trans
......
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