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

feat(Term): offer is_type and is_a_type

Browse source
This commit is contained in:
Simon Cruanes 2022-08-10 22:41:26 -04:00
parent d14617ca77
commit 67d5f244c1
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 26 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -30,14 +30,17 @@ let[@inline] has_fvars e = (e.flags lsr store_id_bits) land 1 == 1
let[@inline] store_uid e : int = e.flags land store_id_mask let[@inline] store_uid e : int = e.flags land store_id_mask
let[@inline] is_closed e : bool = db_depth e == 0 let[@inline] is_closed e : bool = db_depth e == 0
let[@inline] ty e : term = (* slow path *)
match e.ty with let[@inline never] ty_force_delayed_ e f =
| T_ty t -> t
| T_ty_delayed f ->
let ty = f () in let ty = f () in
e.ty <- T_ty ty; e.ty <- T_ty ty;
ty ty
let[@inline] ty e : term =
match e.ty with
| T_ty t -> t
| T_ty_delayed f -> ty_force_delayed_ e f
(* open an application *) (* open an application *)
let unfold_app (e : term) : term * term list = let unfold_app (e : term) : term * term list =
let[@unroll 1] rec aux acc e = let[@unroll 1] rec aux acc e =
@ -225,16 +228,18 @@ let map_shallow_ ~make ~f (e : term) : term =
exception IsSub exception IsSub
let[@inline] is_type_ e = let[@inline] is_type e =
match e.view with match e.view with
| E_type _ -> true | E_type _ -> true
| _ -> false | _ -> false
let[@inline] is_a_type (t : t) = is_type (ty t)
let iter_dag ?(seen = Tbl.create 8) ~iter_ty ~f e : unit = let iter_dag ?(seen = Tbl.create 8) ~iter_ty ~f e : unit =
let rec loop e = let rec loop e =
if not (Tbl.mem seen e) then ( if not (Tbl.mem seen e) then (
Tbl.add seen e (); Tbl.add seen e ();
if iter_ty && not (is_type_ e) then loop (ty e); if iter_ty && not (is_type e) then loop (ty e);
f e; f e;
iter_shallow e ~f:(fun _ u -> loop u) iter_shallow e ~f:(fun _ u -> loop u)
) )
@ -276,7 +281,7 @@ let free_vars ?(init = Var.Set.empty) e : Var.Set.t =
module Make_ = struct module Make_ = struct
let compute_db_depth_ e : int = let compute_db_depth_ e : int =
if is_type_ e then if is_type e then
0 0
else ( else (
let d1 = db_depth @@ ty e in let d1 = db_depth @@ ty e in
@ -292,7 +297,7 @@ module Make_ = struct
) )
let compute_has_fvars_ e : bool = let compute_has_fvars_ e : bool =
if is_type_ e then if is_type e then
false false
else else
has_fvars (ty e) has_fvars (ty e)
@ -325,7 +330,7 @@ module Make_ = struct
let rec loop e k : term = let rec loop e k : term =
if is_closed e then if is_closed e then
e e
else if is_type_ e then else if is_type e then
e e
else ( else (
match view e with match view e with
@ -356,7 +361,7 @@ module Make_ = struct
(* recurse in subterm [e], under [k] intermediate binders (so any (* recurse in subterm [e], under [k] intermediate binders (so any
bound variable under k is bound by them) *) bound variable under k is bound by them) *)
let rec aux e k : term = let rec aux e k : term =
if is_type_ e then if is_type e then
e e
else if db_depth e < k then else if db_depth e < k then
e e
@ -425,8 +430,9 @@ module Make_ = struct
db_0_replace_ ~make ty_bod_f ~by:a db_0_replace_ ~make ty_bod_f ~by:a
| _ -> | _ ->
Error.errorf Error.errorf
"@[<2>cannot apply %a,@ must have Pi type, but actual type is %a@]" "@[<2>cannot apply %a@ (to %a),@ must have Pi type, but actual type \
pp_debug f pp_debug ty_f) is %a@]"
pp_debug f pp_debug a pp_debug ty_f)
| E_pi (_, ty, bod) -> | E_pi (_, ty, bod) ->
(* TODO: check the actual triplets for COC *) (* TODO: check the actual triplets for COC *)
(*Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;*) (*Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;*)
@ -440,6 +446,7 @@ module Make_ = struct
(* hashconsing + computing metadata + computing type (for new terms) *) (* hashconsing + computing metadata + computing type (for new terms) *)
let rec make_ (store : store) view : term = let rec make_ (store : store) view : term =
let e = { view; ty = T_ty_delayed ty_assert_false_; id = -1; flags = 0 } in let e = { view; ty = T_ty_delayed ty_assert_false_; id = -1; flags = 0 } in
Log.debugf 50 (fun k -> k "term.make `%a`" pp_debug_with_ids e);
let e2 = Hcons.hashcons store.s_exprs e in let e2 = Hcons.hashcons store.s_exprs e in
if e == e2 then ( if e == e2 then (
(* new term, compute metadata *) (* new term, compute metadata *)
@ -485,7 +492,7 @@ module Make_ = struct
let cache_ = T_int_tbl.create 16 in let cache_ = T_int_tbl.create 16 in
let rec loop k e = let rec loop k e =
if is_type_ e then if is_type e then
e e
else if not (has_fvars e) then else if not (has_fvars e) then
(* no free variables, cannot change *) (* no free variables, cannot change *)
@ -602,8 +609,6 @@ let map_shallow store ~f e : t = map_shallow_ ~make:(make_ store) ~f e
(* re-export some internal things *) (* re-export some internal things *)
module Internal_ = struct module Internal_ = struct
let is_type_ = is_type_
let subst_ store ~recursive t subst = let subst_ store ~recursive t subst =
subst_ ~make:(make_ store) ~recursive t subst subst_ ~make:(make_ store) ~recursive t subst
end end

7
src/core-logic/term.mli
View file

@ -83,6 +83,12 @@ val contains : t -> sub:t -> bool
val free_vars_iter : t -> var Iter.t val free_vars_iter : t -> var Iter.t
val free_vars : ?init:Var.Set.t -> t -> Var.Set.t val free_vars : ?init:Var.Set.t -> t -> Var.Set.t
val is_type : t -> bool
(** [is_type t] is true iff [view t] is [Type _] *)
val is_a_type : t -> bool
(** [is_a_type t] is true if [is_ty (ty t)] *)
val is_closed : t -> bool val is_closed : t -> bool
(** Is the term closed (all bound variables are paired with a binder)? (** Is the term closed (all bound variables are paired with a binder)?
time: O(1) *) time: O(1) *)
@ -153,7 +159,6 @@ end
(**/**) (**/**)
module Internal_ : sig module Internal_ : sig
val is_type_ : t -> bool
val subst_ : store -> recursive:bool -> t -> subst -> t val subst_ : store -> recursive:bool -> t -> subst -> t
end end