From 4875b8231b1a8995457976feb3ae3728928995ff Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Thu, 17 Nov 2022 10:13:27 +0100
Subject: [PATCH] Use of polymorphic arrays instead of int arrays
---
colibri2/theories/array/array.ml | 83 +++++++++++++++++++++++---------
1 file changed, 59 insertions(+), 24 deletions(-)
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index f16b4f608..aec812e83 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -43,6 +43,8 @@ let default_values =
"def-values"
let db = Datastructure.Push.create Ground.pp "Array.db"
+(* Use one db per array type? *)
+
let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
let stats = Debug.register_stats_int "Array.rule"
let array_num = Debug.register_stats_int "Array.num"
@@ -52,32 +54,40 @@ let convert ~subst =
Colibri2_theories_quantifiers.Subst.convert ~subst_old:Ground.Subst.empty
~subst_new:subst
-let int_ty = Expr.Ty.int
-let array_ty = Expr.Ty.array int_ty int_ty
+let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
+let val_ty_var = Expr.Ty.Var.mk "val_ty"
+let ind_ty = Expr.Ty.of_var ind_ty_var
+let val_ty = Expr.Ty.of_var val_ty_var
+let array_ty = Expr.Ty.array ind_ty val_ty
+let bind_tys tyvl ty = Expr.Ty.pi tyvl ty
(* Builtins *)
module Builtin = struct
- type _ Expr.t += Array_diff | Array_const
+ type _ Expr.t +=
+ | Array_diff
+ | Array_const
+ | Array_default_index
+ | Array_default_value
let array_diff : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"array_diff" ~builtin:Array_diff
(Dolmen_std.Path.global "array_diff")
- (Expr.Ty.arrow [ array_ty; array_ty ] int_ty)
+ (Expr.Ty.arrow [ array_ty; array_ty ] ind_ty)
let array_const : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"array_const" ~builtin:Array_const
(Dolmen_std.Path.global "array_const")
- (Expr.Ty.arrow [ int_ty ] array_ty)
+ (Expr.Ty.arrow [ val_ty ] array_ty)
let array_default_index : Dolmen_std.Expr.term_cst =
- Expr.Id.mk ~name:"array_default_index" ~builtin:Array_diff
+ Expr.Id.mk ~name:"array_default_index" ~builtin:Array_default_index
(Dolmen_std.Path.global "array_default_index")
- (Expr.Ty.arrow [ array_ty ] int_ty)
+ (Expr.Ty.arrow [ array_ty ] ind_ty)
let array_default_value : Dolmen_std.Expr.term_cst =
- Expr.Id.mk ~name:"array_default_value" ~builtin:Array_const
+ Expr.Id.mk ~name:"array_default_value" ~builtin:Array_default_value
(Dolmen_std.Path.global "array_default_value")
- (Expr.Ty.arrow [ array_ty ] int_ty)
+ (Expr.Ty.arrow [ array_ty ] val_ty)
let () =
let app1 env s f =
@@ -148,18 +158,17 @@ module Theory = struct
open Colibri2_theories_quantifiers
let term_of_var = Expr.Term.of_var
- let mk_int_var name = Expr.Term.Var.mk name int_ty
+ let mk_index_var name = Expr.Term.Var.mk name ind_ty
+ let mk_value_var name = Expr.Term.Var.mk name val_ty
let mk_array_var name = Expr.Term.Var.mk name array_ty
- let vi = mk_int_var "i"
- let vj = mk_int_var "j"
- let vk = mk_int_var "k"
- let vv = mk_int_var "v"
- let vw = mk_int_var "w"
+ let vi = mk_index_var "i"
+ let vj = mk_index_var "j"
+ let vk = mk_index_var "k"
+ let vv = mk_value_var "v"
let ti = term_of_var vi
let tj = term_of_var vj
let tk = term_of_var vk
let tv = term_of_var vv
- let tw = term_of_var vw
let va = mk_array_var "a"
let vb = mk_array_var "b"
let ta = term_of_var va
@@ -326,6 +335,9 @@ module Theory = struct
List.iter (fun (p, r) -> InvertedPath.add_callback env p r) l
let new_array env f =
+ let s = Ground.sem f in
+ let s_index_ty = List.hd s.ty.args in
+ let s_value_ty = List.hd (List.tl s.ty.args) in
(* Extensionality rule ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
if not !restrict_ext then (
Datastructure.Push.iter db env ~f:(fun f2 ->
@@ -335,7 +347,9 @@ module Theory = struct
term =
Expr.Term.Var.M.of_list
[ (va, Ground.node f2); (vb, Ground.node f) ];
- ty = Expr.Ty.Var.M.empty;
+ ty =
+ Expr.Ty.Var.M.of_list
+ [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ];
}
in
Debug.dprintf2 debug "Found ext with %a" Ground.Subst.pp subst;
@@ -349,7 +363,9 @@ module Theory = struct
Ground.Subst.
{
term = Expr.Term.Var.M.of_list [ (va, Ground.node f) ];
- ty = Expr.Ty.Var.M.empty;
+ ty =
+ Expr.Ty.Var.M.of_list
+ [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ];
}
in
let epsilon_app = apply_def_index ta in
@@ -382,7 +398,12 @@ let converter env (f : Ground.t) =
~f:(fun n ->
if is_array env n then Foreign_dom.set_dom env n IsForeign)
args
- | { app = { builtin = Expr.Select; _ }; args; _ } ->
+ | {
+ app = { builtin = Expr.Select; _ };
+ args;
+ tyargs = [ s_ind_ty; s_val_ty ];
+ _;
+ } ->
let a, i = IArray.extract2_exn args in
Egraph.register env a;
Egraph.register env i;
@@ -397,7 +418,9 @@ let converter env (f : Ground.t) =
Ground.Subst.
{
term = Expr.Term.Var.M.of_list [ (Theory.va, a); (Theory.vi, i) ];
- ty = Expr.Ty.Var.M.empty;
+ ty =
+ Expr.Ty.Var.M.of_list
+ [ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ];
}
in
let eps_term = apply_def_index Theory.ta in
@@ -410,7 +433,12 @@ let converter env (f : Ground.t) =
in
Egraph.register env i_eps_neq_node;
Boolean.set_true env i_eps_neq_node))
- | { app = { builtin = Expr.Store; _ }; args; _ } ->
+ | {
+ app = { builtin = Expr.Store; _ };
+ args;
+ tyargs = [ s_ind_ty; s_val_ty ];
+ _;
+ } ->
let a, k, v = IArray.extract3_exn args in
Egraph.register env a;
Egraph.register env k;
@@ -424,7 +452,9 @@ let converter env (f : Ground.t) =
term =
Expr.Term.Var.M.of_list
[ (Theory.va, a); (Theory.vk, k); (Theory.vv, v) ];
- ty = Expr.Ty.Var.M.empty;
+ ty =
+ Expr.Ty.Var.M.of_list
+ [ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ];
}
in
let store_term = Expr.Term.store Theory.ta Theory.tk Theory.tv in
@@ -446,7 +476,12 @@ let converter env (f : Ground.t) =
let a, b = IArray.extract2_exn args in
Egraph.register env a;
Egraph.register env b
- | { app = { builtin = Builtin.Array_const; _ }; args; _ } ->
+ | {
+ app = { builtin = Builtin.Array_const; _ };
+ args;
+ tyargs = [ s_val_ty ];
+ _;
+ } ->
let v = IArray.extract1_exn args in
Egraph.register env v;
(* application of the `Kð›¿` rule *)
@@ -455,7 +490,7 @@ let converter env (f : Ground.t) =
Ground.Subst.
{
term = Expr.Term.Var.M.of_list [ (Theory.vv, v) ];
- ty = Expr.Ty.Var.M.empty;
+ ty = Expr.Ty.Var.M.of_list [ (val_ty_var, s_val_ty) ];
}
in
let eq_node =
--
GitLab