simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor a bit

Browse source
This commit is contained in:
Simon Cruanes 2022-07-28 14:54:23 -04:00
parent e70daf4531
commit c6407bfec1
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 49 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
src/core-logic/term.ml
View file

@ -441,46 +441,6 @@ module Make_ = struct
else else
aux e 0 aux e 0
let subst_ ~make ~recursive e0 (subst : subst) : t =
(* cache for types and some terms *)
let cache_ = T_int_tbl.create 16 in
let rec loop k e =
try T_int_tbl.find cache_ (e, k)
with Not_found ->
let r = loop_uncached_ k e in
T_int_tbl.add cache_ (e, k) r;
r
and loop_uncached_ k (e : t) : t =
match view e with
| _ when not (has_fvars e) -> e (* nothing to subst in *)
| E_var v ->
(* first, subst in type *)
let v = { v with v_ty = loop k v.v_ty } in
(match Var_.Map.find v subst.m with
| u ->
let u = db_shift_ ~make u k in
if recursive then
loop 0 u
else
u
| exception Not_found -> make (E_var v))
| E_const _ -> e
| _ ->
map_shallow_ e ~make ~f:(fun inb u ->
loop
(if inb then
k + 1
else
k)
u)
in
if Var_.Map.is_empty subst.m then
e0
else
loop 0 e0
let compute_ty_ ~make (view : view) : term = let compute_ty_ ~make (view : view) : term =
match view with match view with
| E_var v -> Var.ty v | E_var v -> Var.ty v
@ -562,6 +522,55 @@ module Make_ = struct
let app store f a = make_ store (E_app (f, a)) let app store f a = make_ store (E_app (f, a))
let app_l store f l = List.fold_left (app store) f l let app_l store f l = List.fold_left (app store) f l
(* general substitution, compatible with DB indices. We use this
also to abstract on a free variable, because it subsumes it and
it's better to minimize the number of DB indices manipulations *)
let subst_ ~make ~recursive e0 (subst : subst) : t =
(* cache for types and some terms *)
let cache_ = T_int_tbl.create 16 in
let rec loop k e =
if is_type_ e then
e
else if not (has_fvars e) then
(* no free variables, cannot change *)
e
else (
try T_int_tbl.find cache_ (e, k)
with Not_found ->
let r = loop_uncached_ k e in
T_int_tbl.add cache_ (e, k) r;
r
)
and loop_uncached_ k (e : t) : t =
match view e with
| E_var v ->
(* first, subst in type *)
let v = { v with v_ty = loop k v.v_ty } in
(match Var_.Map.find v subst.m with
| u ->
let u = db_shift_ ~make u k in
if recursive then
loop 0 u
else
u
| exception Not_found -> make (E_var v))
| E_const _ -> e
| _ ->
map_shallow_ e ~make ~f:(fun inb u ->
loop
(if inb then
k + 1
else
k)
u)
in
if Var_.Map.is_empty subst.m then
e0
else
loop 0 e0
let abs_on_ (store : store) (v : var) (e : term) : term = let abs_on_ (store : store) (v : var) (e : term) : term =
Store.check_e_uid store v.v_ty; Store.check_e_uid store v.v_ty;
Store.check_e_uid store e; Store.check_e_uid store e;