From 96fb8710c9d045e85bed88d7ad28e7b77c0a1051 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Wed, 16 Feb 2011 13:56:29 +0100
Subject: [PATCH] encoding enumerate : forbidden with explicit
---
src/transform/encoding.ml | 36 +++++---------------------
src/transform/encoding.mli | 1 -
src/transform/encoding_arrays.ml | 17 ++++++------
src/transform/encoding_enumeration.ml | 7 ++---
src/transform/encoding_enumeration.mli | 3 ---
src/transform/encoding_explicit.ml | 17 +++++++++---
6 files changed, 30 insertions(+), 51 deletions(-)
diff --git a/src/transform/encoding.ml b/src/transform/encoding.ml
index 2393941a4b..aa73cecdb5 100644
--- a/src/transform/encoding.ml
+++ b/src/transform/encoding.ml
@@ -64,30 +64,6 @@ 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 forbid_for_explicit =
- Encoding_enumeration.forbid_enumeration
- "explicit is unsound in presence of this finite type"
-
-let maybe_forbid_enumeration =
- Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
- let s = match alo with
- | None -> poly_smt_opt.default
- | Some [MAstr s] -> s
- | _ -> assert false in
- if s = "explicit"
- then forbid_for_explicit
- else Trans.identity)
-
-let forbid_enumeration =
- Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
- let s = match alo with
- | None -> poly_smt_opt.default
- | Some [MAstr s] -> s
- | _ -> assert false in
- if s = "explicit"
- then forbid_for_explicit
- else Encoding_enumeration.encoding_enumeration)
-
open Ty
open Term
@@ -113,15 +89,15 @@ let monomorphise_goal =
let encoding_smt env =
compose monomorphise_goal
- (compose maybe_forbid_enumeration
- (compose (enco_select env)
- (compose (enco_kept env) (enco_poly_smt env))))
+ (compose (enco_select env)
+ (compose (enco_kept env) (enco_poly_smt env)))
let encoding_tptp env =
compose monomorphise_goal
- (compose forbid_enumeration
- (compose (enco_select env)
- (compose (enco_kept env) (enco_poly_tptp env))))
+ (compose (enco_select env)
+ (compose (enco_kept env)
+ (compose (enco_poly_tptp env)
+ Encoding_enumeration.encoding_enumeration)))
let () =
register_env_transform "encoding_smt" encoding_smt;
diff --git a/src/transform/encoding.mli b/src/transform/encoding.mli
index 9e30ceca9b..dda00e804d 100644
--- a/src/transform/encoding.mli
+++ b/src/transform/encoding.mli
@@ -32,7 +32,6 @@ val register_enco_poly : string -> (env -> task trans) -> unit
val monomorphise_goal : Task.task Trans.trans
-val maybe_forbid_enumeration : Task.task Trans.trans
val enco_poly_smt : Env.env -> Task.task Trans.trans
val print_kept : Task.task Trans.trans
diff --git a/src/transform/encoding_arrays.ml b/src/transform/encoding_arrays.ml
index af62984049..0c9823999f 100644
--- a/src/transform/encoding_arrays.ml
+++ b/src/transform/encoding_arrays.ml
@@ -576,15 +576,14 @@ let encoding_smt_array env =
Trans.on_used_theory th_array (fun used ->
if not used then Encoding.encoding_smt env else
compose Encoding.monomorphise_goal
- (compose Encoding.maybe_forbid_enumeration
- (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)))))))))
+ (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))))))))
let () = Trans.register_env_transform "encoding_smt_array" encoding_smt_array
diff --git a/src/transform/encoding_enumeration.ml b/src/transform/encoding_enumeration.ml
index b5706f142c..690e5f283a 100644
--- a/src/transform/encoding_enumeration.ml
+++ b/src/transform/encoding_enumeration.ml
@@ -45,6 +45,8 @@ let proj tenv t ty = match ty.ty_node with
| Tyapp (ts,_) when Sts.mem ts tenv.enum ->
let fs = Hts.find tenv.projs ts in
t_app fs [t] t.t_ty
+ | _ when ty_s_any (fun ts -> Sts.mem ts tenv.enum) t.t_ty ->
+ Printer.unsupportedType ty "complexe finite type"
| _ -> t
let proj tenv t = match t.t_node with
@@ -93,10 +95,5 @@ let encoding_enumeration =
let tenv = { enum = enum ; projs = projs } in
Trans.decl (decl tenv) None)
-let forbid_enumeration s =
- Trans.on_tagged_ts meta_enum (fun enum ->
- if Sts.is_empty enum then Trans.identity
- else Printer.unsupportedTysymbol (Sts.choose enum) s)
-
let () = Trans.register_transform "encoding_enumeration" encoding_enumeration
diff --git a/src/transform/encoding_enumeration.mli b/src/transform/encoding_enumeration.mli
index 40281732ac..bd1ec2ad3c 100644
--- a/src/transform/encoding_enumeration.mli
+++ b/src/transform/encoding_enumeration.mli
@@ -18,6 +18,3 @@
(**************************************************************************)
val encoding_enumeration : Task.task Trans.trans
-val forbid_enumeration : string ->Task.task Trans.trans
-(* [forbid_enumeration s] if the task contains encoded enumeration
- unsupportedTysymbol is raised with the message [s] *)
diff --git a/src/transform/encoding_explicit.ml b/src/transform/encoding_explicit.ml
index 8381a89223..726d5c5bd3 100644
--- a/src/transform/encoding_explicit.ml
+++ b/src/transform/encoding_explicit.ml
@@ -38,9 +38,11 @@ module Debug = struct
(** utility to print a list of items *)
let rec print_list printer fmter = function
| [] -> Format.fprintf fmter ""
- | e::es -> if es = []
- then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
- else Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
+ | e::es ->
+ if es = [] then
+ Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
+ else
+ Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
let debug x = Format.eprintf "%s@." x
end
@@ -137,6 +139,15 @@ let decl d = match d.d_node with
let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
+let meta_enum = Eliminate_algebraic.meta_enum
+
+let explicit =
+ Trans.on_tagged_ts meta_enum (fun enum ->
+ if Sts.is_empty enum then explicit
+ else Printer.unsupportedTysymbol (Sts.choose enum)
+ "explicit is unsound in presence of type")
+
+
(** {2 monomorphise task } *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
--
GitLab