From b8cbe0cf066cd2f3b09da05ca75f3d13af597404 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 23 Feb 2023 22:07:34 -0500 Subject: [PATCH] feat(core-logic): add level expressions, modify type checker --- src/core-logic/level.ml | 138 ++++++++++++++++++++++++++ src/core-logic/level.mli | 41 ++++++++ src/core-logic/sidekick_core_logic.ml | 1 + src/core-logic/term.ml | 107 ++++++++++++-------- src/core-logic/term.mli | 10 +- src/core-logic/types_.ml | 13 ++- 6 files changed, 266 insertions(+), 44 deletions(-) create mode 100644 src/core-logic/level.ml create mode 100644 src/core-logic/level.mli diff --git a/src/core-logic/level.ml b/src/core-logic/level.ml new file mode 100644 index 00000000..9c7ae424 --- /dev/null +++ b/src/core-logic/level.ml @@ -0,0 +1,138 @@ +open Types_ + +type view = level_view = + | L_zero + | L_succ of level + | L_var of string (** variable *) + | L_max of level * level (** max *) + | L_imax of level * level (** impredicative max. *) + +and t = level = { l_view: level_view; mutable l_id: int } + +let[@inline] view (self : t) : view = self.l_view +let[@inline] equal (a : t) (b : t) : bool = a == b +let[@inline] hash (a : t) : int = Hash.int a.l_id +let[@inline] compare a b : int = compare a.l_id b.l_id + +(* hashconsing *) +module H_cons = Hashcons.Make (struct + type nonrec t = t + + let equal (a : t) (b : t) : bool = + a == b + || + match view a, view b with + | L_zero, L_zero -> true + | L_succ a, L_succ b -> equal a b + | L_var a, L_var b -> String.equal a b + | L_imax (a1, a2), L_imax (b1, b2) | L_max (a1, a2), L_max (b1, b2) -> + equal a1 b1 && equal a2 b2 + | (L_zero | L_succ _ | L_var _ | L_max _ | L_imax _), _ -> false + + let hash a : int = + match view a with + | L_zero -> Hash.int 1 + | L_succ a -> Hash.combine2 2 (hash a) + | L_var v -> Hash.combine2 3 (Hash.string v) + | L_max (a, b) -> Hash.combine3 10 (hash a) (hash b) + | L_imax (a, b) -> Hash.combine3 20 (hash a) (hash b) + + let set_id self i = + assert (self.l_id = -1); + self.l_id <- i +end) + +let as_offset (self : t) : t * int = + let rec loop n l = + match view l with + | L_succ a -> loop (n + 1) a + | _ -> l, n + in + loop 0 self + +let rec pp out (self : t) : unit = + let lvl, offset = as_offset self in + let pp_offset out () = if offset > 0 then Fmt.fprintf out " + %d" offset in + match view lvl with + | L_zero -> Fmt.int out offset + | L_succ _ -> assert false + | L_var v -> Fmt.fprintf out "%s%a" v pp_offset () + | L_max (a, b) -> Fmt.fprintf out "max(%a, %a)%a" pp a pp b pp_offset () + | L_imax (a, b) -> Fmt.fprintf out "imax(%a, %a)%a" pp a pp b pp_offset () + +let to_string = Fmt.to_string pp + +type store = { h_cons: H_cons.t } + +module Store = struct + type t = store + + let create () : store = { h_cons = H_cons.create ~size:64 () } +end + +let make_ (self : store) (l_view : view) : t = + let lvl = { l_view; l_id = -1 } in + H_cons.hashcons self.h_cons lvl + +let zero self : t = make_ self L_zero +let succ self t : t = make_ self (L_succ t) +let one self = succ self @@ zero self +let var self n : t = make_ self (L_var n) + +let rec max self a b : t = + if equal a b then + a + else ( + match view a, view b with + | L_succ a', L_succ b' -> succ self (max self a' b') + | L_zero, _ -> b + | _, L_zero -> a + | _ -> + let a, b = + if compare a b > 0 then + b, a + else + a, b + in + make_ self (L_max (a, b)) + ) + +let rec imax self a b : t = + if equal a b then + a + else ( + match view a, view b with + | _, L_zero -> zero self (* imax(_, 0) = 0 *) + | L_succ a', L_succ b' -> succ self (imax self a' b') + | L_zero, _ -> b + | _ -> make_ self (L_imax (a, b)) + ) + +let of_int self i : t = + assert (i >= 0); + let rec loop i = + if i = 0 then + zero self + else + succ self @@ loop (i - 1) + in + loop i + +let[@inline] is_zero l = + match view l with + | L_zero -> true + | _ -> false + +let is_one l = + match view l with + | L_succ a -> is_zero a + | _ -> false + +let as_int self : _ option = + let lvl, offset = as_offset self in + if is_zero lvl then + Some offset + else + None + +let is_int self : bool = Option.is_some (as_int self) diff --git a/src/core-logic/level.mli b/src/core-logic/level.mli new file mode 100644 index 00000000..07deae2c --- /dev/null +++ b/src/core-logic/level.mli @@ -0,0 +1,41 @@ +open Types_ + +type view = level_view = + | L_zero + | L_succ of level + | L_var of string (** variable *) + | L_max of level * level (** max *) + | L_imax of level * level (** impredicative max. *) + +type t = level + +include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t + +val to_string : t -> string + +val as_offset : t -> t * int +(** [as_offset lvl] returns a pair [lvl' + n]. *) + +(** Hashconsing store *) +module Store : sig + type t + + val create : unit -> t +end + +type store = Store.t + +val zero : store -> t +val one : store -> t +val var : store -> string -> t +val succ : store -> t -> t +val of_int : store -> int -> t +val max : store -> t -> t -> t +val imax : store -> t -> t -> t + +(** {2 helpers} *) + +val is_zero : t -> bool +val is_one : t -> bool +val is_int : t -> bool +val as_int : t -> int option diff --git a/src/core-logic/sidekick_core_logic.ml b/src/core-logic/sidekick_core_logic.ml index c06f698a..977f2f20 100644 --- a/src/core-logic/sidekick_core_logic.ml +++ b/src/core-logic/sidekick_core_logic.ml @@ -5,6 +5,7 @@ module Const = Const module Subst = Subst module T_builtins = T_builtins module Store = Term.Store +module Level = Level (* TODO: move to separate library? *) module Str_const = Str_const diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml index 4614d4d2..92e32df2 100644 --- a/src/core-logic/term.ml +++ b/src/core-logic/term.ml @@ -5,7 +5,7 @@ type bvar = Bvar.t type nonrec term = term type view = term_view = - | E_type of int + | E_type of level | E_var of var | E_bound_var of bvar | E_const of const @@ -70,13 +70,23 @@ let[@inline] is_pi e = | E_pi _ -> true | _ -> false +let as_type e : level option = + match e.view with + | E_type l -> Some l + | _ -> None + +let as_type_exn e : level = + match e.view with + | E_type l -> l + | _ -> Error.errorf "Term.as_type_exn: `%a` is not a type" !pp_debug_ e + (* debug printer *) let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit = let rec loop k ~depth names out e = let pp' = loop k ~depth:(depth + 1) names in (match e.view with - | E_type 0 -> Fmt.string out "Type" - | E_type i -> Fmt.fprintf out "Type(%d)" i + | E_type lvl when Level.is_one lvl -> Fmt.string out "Type" + | E_type lvl -> Fmt.fprintf out "Type.{%a}" Level.pp lvl | E_var v -> Fmt.string out v.v_name (* | E_var v -> Fmt.fprintf out "(@[%s : %a@])" v.v_name pp v.v_ty *) | E_bound_var v -> @@ -103,15 +113,16 @@ let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit = Fmt.fprintf out "(@[\\%s:@[%a@].@ %a@])" n pp' _ty (loop (k + 1) ~depth:(depth + 1) (n :: names)) bod - | E_pi (_, ty, bod) when is_closed bod -> + | E_pi (_, ty_arg, bod) + when is_closed bod && Level.is_int (as_type_exn @@ ty ty_arg) -> (* actually just an arrow *) Fmt.fprintf out "(@[%a@ -> %a@])" (loop k ~depth:(depth + 1) names) - ty + ty_arg (loop (k + 1) ~depth:(depth + 1) ("" :: names)) bod - | E_pi ("", _ty, bod) -> - Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' _ty + | E_pi ("", ty_arg, bod) -> + Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' ty_arg (loop (k + 1) ~depth:(depth + 1) ("" :: names)) bod | E_pi (n, _ty, bod) -> @@ -164,7 +175,7 @@ module Hcons = Hashcons.Make (struct let hash e : int = match e.view with - | E_type i -> H.combine2 10 (H.int i) + | E_type i -> H.combine2 10 (Level.hash i) | E_const c -> H.combine2 20 (Const.hash c) | E_var v -> H.combine2 30 (Var.hash v) | E_bound_var v -> H.combine2 40 (Bvar.hash v) @@ -180,18 +191,22 @@ module Hcons = Hashcons.Make (struct end) module Store = struct - type t = { (* unique ID for this store *) - s_uid: int; s_exprs: Hcons.t } + type t = { + s_uid: int; (** unique ID for this store *) + s_exprs: Hcons.t; + s_lvl_store: Level.store; + } (* TODO: use atomic? CCAtomic? *) let n = ref 0 - let size self = Hcons.size self.s_exprs + let[@inline] size self = Hcons.size self.s_exprs + let[@inline] lvl_store self = self.s_lvl_store - let create ?(size = 256) () : t = + let create ?(level_store = Level.Store.create ()) ?(size = 256) () : t = (* store id, modulo 2^5 *) let s_uid = !n land store_id_mask in incr n; - { s_uid; s_exprs = Hcons.create ~size () } + { s_uid; s_exprs = Hcons.create ~size (); s_lvl_store = level_store } (* check that [e] belongs in this store *) let[@inline] check_e_uid (self : t) (e : term) = @@ -353,14 +368,15 @@ module Make_ = struct has_fvars f || has_fvars acc0 || List.exists has_fvars args | E_lam (_, ty, bod) | E_pi (_, ty, bod) -> has_fvars ty || has_fvars bod - let universe_ (e : term) : int = + let universe_ (e : term) : level = match e.view with | E_type i -> i | _ -> assert false - let[@inline] universe_of_ty_ (e : term) : int = + (** Universe of the type of [e] *) + let universe_of_ty_ (self : store) (e : term) : level = match e.view with - | E_type i -> i + 1 + | E_type lvl -> Level.succ self.s_lvl_store lvl | _ -> universe_ (ty e) module T_int_tbl = CCHashtbl.Make (struct @@ -438,34 +454,39 @@ module Make_ = struct else aux e 0 - let compute_ty_ store ~make (view : view) : term = + (* TODO: have beta-reduction here; level checking; and pluggable reduction + rules (in the store) so we can reduce quotients and recursors *) + + (** compute the type of [view]. *) + let compute_ty_ (self : store) ~make (view : view) : term = match view with | E_var v -> Var.ty v | E_bound_var v -> Bvar.ty v - | E_type i -> make (E_type (i + 1)) + | E_type lvl -> make (E_type (Level.succ self.s_lvl_store lvl)) | E_const c -> let ty = Const.ty c in - Store.check_e_uid store ty; + Store.check_e_uid self ty; if not (is_closed ty) then Error.errorf "const %a@ cannot have a non-closed type like %a" Const.pp c pp_debug ty; ty | E_lam (name, ty_v, bod) -> - Store.check_e_uid store ty_v; - Store.check_e_uid store bod; + Store.check_e_uid self ty_v; + Store.check_e_uid self bod; (* type of [\x:tau. bod] is [pi x:tau. typeof(bod)] *) let ty_bod = ty bod in make (E_pi (name, ty_v, ty_bod)) | E_app (f, a) -> (* type of [f a], where [a:tau] and [f: Pi x:tau. ty_bod_f], is [ty_bod_f[x := a]] *) - Store.check_e_uid store f; - Store.check_e_uid store a; + Store.check_e_uid self f; + Store.check_e_uid self a; let ty_f = ty f in let ty_a = ty a in (match ty_f.view with | E_pi (_, ty_arg_f, ty_bod_f) -> (* check that the expected type matches *) + (* FIXME: replace [equal] with definitional equality *) if not (equal ty_arg_f ty_a) then Error.errorf "@[<2>cannot @[apply `%a`@]@ @[to `%a`@],@ expected argument type: \ @@ -480,9 +501,9 @@ module Make_ = struct pp_debug f pp_debug a pp_debug ty_f) | E_app_fold { args = []; _ } -> assert false | E_app_fold { f; args = a0 :: other_args as args; acc0 } -> - Store.check_e_uid store f; - Store.check_e_uid store acc0; - List.iter (Store.check_e_uid store) args; + Store.check_e_uid self f; + Store.check_e_uid self acc0; + List.iter (Store.check_e_uid self) args; let ty_result = ty acc0 in let ty_a0 = ty a0 in (* check that all arguments have the same type *) @@ -503,32 +524,34 @@ module Make_ = struct pp_debug app1 pp_debug (ty app1) pp_debug ty_result; ty_result | E_pi (_, ty, bod) -> - (* TODO: check the actual triplets for COC *) (*Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;*) - Store.check_e_uid store ty; - Store.check_e_uid store bod; - let u = max (universe_of_ty_ ty) (universe_of_ty_ bod) in + Store.check_e_uid self ty; + Store.check_e_uid self bod; + let u = + Level.imax self.s_lvl_store (universe_of_ty_ self ty) + (universe_of_ty_ self bod) + in make (E_type u) let ty_assert_false_ () = assert false (* hashconsing + computing metadata + computing type (for new terms) *) - let rec make_ (store : store) view : term = + let rec make_ (self : store) view : term = let e = { view; ty = T_ty_delayed ty_assert_false_; id = -1; flags = 0 } in - let e2 = Hcons.hashcons store.s_exprs e in + let e2 = Hcons.hashcons self.s_exprs e in if e == e2 then ( (* new term, compute metadata *) - assert (store.s_uid land store_id_mask == store.s_uid); + assert (self.s_uid land store_id_mask == self.s_uid); (* first, compute type *) (match e.view with - | E_type i -> + | E_type lvl -> (* cannot force type now, as it's an infinite tower of types. Instead we will produce the type on demand. *) - let get_ty () = make_ store (E_type (i + 1)) in + let get_ty () = make_ self (E_type (Level.succ self.s_lvl_store lvl)) in e.ty <- T_ty_delayed get_ty | _ -> - let ty = compute_ty_ store ~make:(make_ store) view in + let ty = compute_ty_ self ~make:(make_ self) view in e.ty <- T_ty ty); let has_fvars = compute_has_fvars_ e in e2.flags <- @@ -537,13 +560,17 @@ module Make_ = struct 1 lsl store_id_bits else 0) - lor store.s_uid; - Store.check_e_uid store e2 + lor self.s_uid; + Store.check_e_uid self e2 ); e2 - let type_of_univ store i : term = make_ store (E_type i) - let type_ store : term = type_of_univ store 0 + let type_of_univ store lvl : term = make_ store (E_type lvl) + + let type_of_univ_int store i : term = + type_of_univ store (Level.of_int store.s_lvl_store i) + + let type_ store : term = type_of_univ store (Level.one store.s_lvl_store) let var store v : term = make_ store (E_var v) let var_str store name ~ty : term = var store (Var.make name ty) let bvar store v : term = make_ store (E_bound_var v) diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli index 82505f0d..6309788f 100644 --- a/src/core-logic/term.mli +++ b/src/core-logic/term.mli @@ -27,7 +27,7 @@ type store A view is the shape of the root node of a term. *) type view = term_view = - | E_type of int + | E_type of level | E_var of var | E_bound_var of bvar | E_const of const @@ -57,6 +57,8 @@ val unfold_app : t -> t * t list val is_app : t -> bool val is_const : t -> bool val is_pi : t -> bool +val as_type : t -> Level.t option +val as_type_exn : t -> Level.t val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit (** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included. @@ -114,12 +116,14 @@ val ty : t -> t module Store : sig type t = store - val create : ?size:int -> unit -> t + val create : ?level_store:Level.store -> ?size:int -> unit -> t val size : t -> int + val lvl_store : t -> Level.store end val type_ : store -> t -val type_of_univ : store -> int -> t +val type_of_univ : store -> level -> t +val type_of_univ_int : store -> int -> t val var : store -> var -> t val var_str : store -> string -> ty:t -> t val bvar : store -> bvar -> t diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml index 75a80db2..34b6d872 100644 --- a/src/core-logic/types_.ml +++ b/src/core-logic/types_.ml @@ -2,8 +2,19 @@ module H = CCHash type const_view = .. +(** View of a level expression. *) +type level_view = + | L_zero + | L_succ of level + | L_var of string (** variable *) + | L_max of level * level (** max *) + | L_imax of level * level (** impredicative max. *) + +and level = { l_view: level_view; mutable l_id: int } +(** A level expression *) + type term_view = - | E_type of int + | E_type of level | E_var of var | E_bound_var of bvar | E_const of const