Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 96fb8710 authored by François Bobot's avatar François Bobot
Browse files

encoding enumerate : forbidden with explicit

parent 54f72bbf
......@@ -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;
......
......@@ -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
......
......@@ -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
......
......@@ -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
......@@ -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] *)
......@@ -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
......
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