From d165681f308d9deaf61ce3e5662972cb22849afc Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@tertium.org>
Date: Wed, 2 Mar 2011 20:21:09 +0100
Subject: [PATCH] index algebraic constructors with integers
---
src/transform/eliminate_algebraic.ml | 26 ++++++++++++++++++++++++++
1 file changed, 26 insertions(+)
diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml
index 5ee3f867b1..0e59c3e0a1 100644
--- a/src/transform/eliminate_algebraic.ml
+++ b/src/transform/eliminate_algebraic.ml
@@ -188,6 +188,31 @@ let add_selector (state,task) ts ty = function
| [_] -> state, task
| csl -> add_selector (state,task) ts ty csl
+let add_indexer (state,task) ts ty csl =
+ (* declare the indexer function *)
+ let mt_id = id_derive ("index_" ^ ts.ts_name.id_string) ts.ts_name in
+ let mt_ls = create_fsymbol mt_id [ty] ty_int in
+ let task = add_decl task (create_logic_decl [mt_ls, None]) in
+ (* define the indexer function *)
+ let index = ref (-1) in
+ let mt_add tsk cs =
+ incr index;
+ let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
+ let pr = create_prsymbol (id_derive id cs.ls_name) in
+ let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
+ let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
+ let ix = t_const (ConstInt (string_of_int !index)) in
+ let ax = f_equ (t_app mt_ls [hd] ty_int) ix in
+ let ax = f_forall_close (List.rev vl) [[Term hd]] ax in
+ add_decl tsk (create_prop_decl Paxiom pr ax)
+ in
+ let task = List.fold_left mt_add task csl in
+ state, task
+
+let add_indexer (state,task) ts ty = function
+ | [_] -> state, task
+ | csl -> add_indexer (state,task) ts ty csl
+
let add_projections (state,task) _ts _ty csl =
(* declare and define the projection functions *)
let pj_add (m,tsk) cs =
@@ -235,6 +260,7 @@ let add_type (state,task) ts csl =
(* add selector, projections, and inversion axiom *)
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let state,task = add_selector (state,task) ts ty csl in
+ let state,task = add_indexer (state,task) ts ty csl in
let state,task = add_projections (state,task) ts ty csl in
let state,task = add_inversion (state,task) ts ty csl in
(* add the tag for enumeration if the type is one *)
--
GitLab