diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index aec812e830bd936a4073cb3b310cf596905973a7..a41d097e1529495d84d20876cb1668a9ea58cf20 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -119,15 +119,9 @@ module Builtin = struct
| _ -> `Not_found)
end
-(* Helper functions *)
-let is_array env n =
- let res =
- Ground.Ty.S.exists
- (function { app = { builtin = Expr.Array; _ }; _ } -> true | _ -> false)
- (Ground.tys env n)
- in
- Debug.dprintf3 debug "is_array %a: %b" Node.pp n res;
- res
+let mk_subst term_l ty_l =
+ Ground.Subst.
+ { term = Expr.Term.Var.M.of_list term_l; ty = Expr.Ty.Var.M.of_list ty_l }
let is_foreign env n =
let res =
@@ -334,23 +328,14 @@ module Theory = struct
let l = if !extended_comb then (const_pattern, const_run) :: l else l in
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
+ let new_array env s_index_ty s_value_ty f =
(* Extensionality rule ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
if not !restrict_ext then (
Datastructure.Push.iter db env ~f:(fun f2 ->
let subst =
- Ground.Subst.
- {
- term =
- Expr.Term.Var.M.of_list
- [ (va, Ground.node f2); (vb, Ground.node f) ];
- ty =
- Expr.Ty.Var.M.of_list
- [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ];
- }
+ mk_subst
+ [ (va, Ground.node f2); (vb, Ground.node f) ]
+ [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ]
in
Debug.dprintf2 debug "Found ext with %a" Ground.Subst.pp subst;
let n = distinct_term_node ~subst env ta tb in
@@ -360,13 +345,9 @@ module Theory = struct
(* ðð›¿: a |> a[ð] = 𛿠*)
if !extended_comb then (
let subst =
- Ground.Subst.
- {
- term = Expr.Term.Var.M.of_list [ (va, Ground.node f) ];
- ty =
- Expr.Ty.Var.M.of_list
- [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ];
- }
+ mk_subst
+ [ (va, Ground.node f) ]
+ [ (ind_ty_var, s_index_ty); (val_ty_var, s_value_ty) ]
in
let epsilon_app = apply_def_index ta in
let delta_app = apply_def_value ta in
@@ -380,24 +361,41 @@ end
let converter env (f : Ground.t) =
let s = Ground.sem f in
- (match s.ty with
- | { app = { builtin = Expr.Array; _ }; _ } ->
- (* apply rules that apply on all arrays *)
- Theory.new_array env f
- | _ -> ());
+ let f_is_array =
+ match s.ty with
+ | { app = { builtin = Expr.Array; _ }; args = [ s_ind_ty; s_val_ty ]; _ } ->
+ Theory.new_array env s_ind_ty s_val_ty f;
+ true
+ | _ -> false
+ in
match s with
- | { app = { builtin = Expr.Base; _ }; args; _ } ->
+ | { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
let fn = Ground.node f in
if IArray.is_empty args then (
- if !restrict_aup && is_array env fn then
+ if !restrict_aup && f_is_array then
(* update of the Linearity domain *)
Linearity_dom.upd_dom env fn Empty)
else if !restrict_ext then
(* update of the Foreign domain *)
- IArray.iter
- ~f:(fun n ->
- if is_array env n then Foreign_dom.set_dom env n IsForeign)
- args
+ let subst, param_tys =
+ match id_ty.ty_descr with
+ | Pi (tyvl, { ty_descr = Expr.Arrow (ptys, _); _ }) ->
+ ( List.fold_left2
+ (fun m k v -> Expr.Ty.Var.M.add k v m)
+ Expr.Ty.Var.M.empty tyvl tyargs,
+ ptys )
+ | Expr.Arrow (ptys, _) -> (Expr.Ty.Var.M.empty, ptys)
+ | _ -> (Expr.Ty.Var.M.empty, [])
+ in
+ if param_tys <> [] then
+ (* should be always true *)
+ IArray.iteri
+ ~f:(fun i n ->
+ match Ground.Ty.convert subst (List.nth param_tys i) with
+ | { app = { builtin = Expr.Array; _ }; _ } ->
+ Foreign_dom.set_dom env n IsForeign
+ | _ -> ())
+ args
| {
app = { builtin = Expr.Select; _ };
args;
@@ -408,20 +406,21 @@ let converter env (f : Ground.t) =
Egraph.register env a;
Egraph.register env i;
(* update of the Foreign domain *)
- if !restrict_ext && is_array env i then
- Foreign_dom.set_dom env i IsForeign;
+ if
+ !restrict_ext
+ &&
+ match s_ind_ty with
+ | { app = { builtin = Expr.Array; _ }; _ } -> true
+ | _ -> false
+ then Foreign_dom.set_dom env i IsForeign;
(* application of the `not default` rule ð≠: v = a[i], i ≠ð |> i ≠ð *)
(* should only be applied if the index sort is infinite,
otherwise the blast rule should be applied *)
if !extended_comb then (
let subst =
- Ground.Subst.
- {
- term = Expr.Term.Var.M.of_list [ (Theory.va, a); (Theory.vi, i) ];
- ty =
- Expr.Ty.Var.M.of_list
- [ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ];
- }
+ mk_subst
+ [ (Theory.va, a); (Theory.vi, i) ]
+ [ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ]
in
let eps_term = apply_def_index Theory.ta in
let eps_node = convert ~subst env eps_term in
@@ -447,15 +446,9 @@ let converter env (f : Ground.t) =
if !restrict_aup then Linearity_dom.upd_dom env (Ground.node f) (Linear a);
(* application of the `idx` rule *)
let subst =
- Ground.Subst.
- {
- term =
- Expr.Term.Var.M.of_list
- [ (Theory.va, a); (Theory.vk, k); (Theory.vv, v) ];
- ty =
- Expr.Ty.Var.M.of_list
- [ (ind_ty_var, s_ind_ty); (val_ty_var, s_val_ty) ];
- }
+ mk_subst
+ [ (Theory.va, a); (Theory.vk, k); (Theory.vv, v) ]
+ [ (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
let rn =
@@ -486,13 +479,7 @@ let converter env (f : Ground.t) =
Egraph.register env v;
(* application of the `Kð›¿` rule *)
if !default_values then (
- let subst =
- Ground.Subst.
- {
- term = Expr.Term.Var.M.of_list [ (Theory.vv, v) ];
- ty = Expr.Ty.Var.M.of_list [ (val_ty_var, s_val_ty) ];
- }
- in
+ let subst = mk_subst [ (Theory.vv, v) ] [ (val_ty_var, s_val_ty) ] in
let eq_node =
convert ~subst env
(Expr.Term.eq (apply_def_value (apply_const Theory.tv)) Theory.tv)