Commit ea09b4e3 authored by Francois Bobot's avatar Francois Bobot
Browse files

eliminate algebraic add a tag for types defined by enumeration

parent b2a852d9
......@@ -25,6 +25,10 @@ open Decl
open Theory
open Task
let meta_enum = "enumeration"
let () = Theory.register_meta meta_enum [Theory.MTtysymbol]
(** Compile match patterns *)
let rec rewriteT kn t = match t.t_node with
......@@ -216,6 +220,12 @@ let add_type (state, task) ts csl =
let trgl = t_app mt_ls (ax_hd :: mt_tl) mt_ty in
let ax_f = f_forall (ax_vs :: mt_vl) [[Term trgl]] ax_f in
let task = add_decl task (create_prop_decl Paxiom ax_pr ax_f) in
(* Add the tag for enumeration if the type is one*)
let is_constant ls = ls.ls_args = [] in
let is_enumeration = List.for_all is_constant csl in
let task =
if is_enumeration then add_meta task meta_enum [MAts ts] else task
in
(* return the updated state and task *)
{ mt_map = mtmap; pj_map = pjmap }, task
......
......@@ -23,3 +23,4 @@ val eliminate_compiled_algebraic : Task.task Trans.trans
val eliminate_algebraic : Task.task Trans.trans
val meta_enum : string
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