feat(core-logic): add a few builtins (=, bool, ite, not, true, false)

src/core-logic/dune

@@ -1,6 +1,6 @@
 (library
  (name sidekick_core_logic)
  (public_name sidekick.core-logic)
- (synopsis "Core AST for logic terms and types")
+ (synopsis "Core AST for logic terms in the calculus of constructions")
  (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
  (libraries containers iter sidekick.sigs sidekick.util))

src/core-logic/sidekick_core_logic.ml

@@ -3,6 +3,7 @@ module Var = Var
 module Bvar = Bvar
 module Const = Const
 module Subst = Subst
+module T_builtins = T_builtins
 
 (* *)
 

src/core-logic/t_builtins.ml

@@ -0,0 +1,84 @@
+open Types_
+open Term
+
+type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false
+
+let ops : const_ops =
+  (module struct
+    let equal a b =
+      match a, b with
+      | C_bool, C_bool
+      | C_eq, C_eq
+      | C_ite, C_ite
+      | C_not, C_not
+      | C_true, C_true
+      | C_false, C_false ->
+        true
+      | _ -> false
+
+    let hash = function
+      | C_bool -> CCHash.int 167
+      | C_eq -> CCHash.int 168
+      | C_ite -> CCHash.int 169
+      | C_not -> CCHash.int 170
+      | C_true -> CCHash.int 171
+      | C_false -> CCHash.int 172
+      | _ -> assert false
+
+    let pp out = function
+      | C_bool -> Fmt.string out "Bool"
+      | C_eq -> Fmt.string out "="
+      | C_ite -> Fmt.string out "ite"
+      | C_not -> Fmt.string out "not"
+      | C_true -> Fmt.string out "true"
+      | C_false -> Fmt.string out "false"
+      | _ -> assert false
+  end)
+
+let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store)
+let true_ store = const store @@ Const.make C_true ops ~ty:(bool store)
+let false_ store = const store @@ Const.make C_false ops ~ty:(bool store)
+
+let c_eq store =
+  let type_ = type_ store in
+  let v = bvar_i store 0 ~ty:type_ in
+  let ty =
+    DB.pi_db ~var_name:"A" store ~var_ty:type_
+    @@ arrow_l store [ v; v ] (bool store)
+  in
+  const store @@ Const.make C_eq ops ~ty
+
+let c_ite store =
+  let type_ = type_ store in
+  let v = bvar_i store 0 ~ty:type_ in
+  let ty =
+    DB.pi_db ~var_name:"A" store ~var_ty:type_
+    @@ arrow_l store [ bool store; v; v ] v
+  in
+  const store @@ Const.make C_eq ops ~ty
+
+let c_not store =
+  let b = bool store in
+  let ty = arrow store b b in
+  const store @@ Const.make C_not ops ~ty
+
+let eq store a b = app_l store (c_eq store) [ ty a; a; b ]
+let ite store a b c = app_l store (c_ite store) [ ty b; a; b; c ]
+let not store a = app store (c_not store) a
+
+let is_bool t =
+  match view t with
+  | E_const { c_view = C_bool; _ } -> true
+  | _ -> false
+
+let is_eq t =
+  match view t with
+  | E_const { c_view = C_eq; _ } -> true
+  | _ -> false
+
+let rec abs t =
+  match view t with
+  | E_app ({ view = E_const { c_view = C_not; _ }; _ }, u) ->
+    let sign, v = abs u in
+    Stdlib.not sign, v
+  | _ -> true, t

src/core-logic/t_builtins.mli

@@ -0,0 +1,32 @@
+(** Core builtins *)
+
+open Types_
+open Term
+
+type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false
+
+val bool : store -> t
+val c_not : store -> t
+val c_eq : store -> t
+val c_ite : store -> t
+val true_ : store -> t
+val false_ : store -> t
+
+val eq : store -> t -> t -> t
+(** [eq a b] is [a = b] *)
+
+val not : store -> t -> t
+
+val ite : store -> t -> t -> t -> t
+(** [ite a b c] is [if a then b else c] *)
+
+val is_eq : t -> bool
+val is_bool : t -> bool
+
+val abs : t -> bool * t
+(** [abs t] returns an "absolute value" for the term, along with the
+      sign of [t].
+
+      The idea is that we want to turn [not a] into [(false, a)],
+      or [(a != b)] into [(false, a=b)]. For terms without a negation this
+      should return [(true, t)]. *)

src/core-logic/term.ml

@@ -1,5 +1,9 @@
 open Types_
 
+type nonrec var = var
+type nonrec bvar = bvar
+type nonrec term = term
+
 type view = term_view =
   | E_type of int
   | E_var of var
@@ -219,63 +223,6 @@ let map_shallow_ ~make ~f (e : term) : term =
     else
       make (E_pi (n, tyv', bod'))
 
-(* TODO
-   (* map immediate subterms *)
-   let map_shallow ctx ~f (e : t) : t =
-     match view e with
-     | E_kind | E_type | E_const (_, []) | E_box _ -> e
-     | _ ->
-       let ty' =
-         lazy
-           (match e.e_ty with
-           | (lazy None) -> None
-           | (lazy (Some ty)) -> Some (f false ty))
-       in
-       (match view e with
-       | E_var v ->
-         let v_ty = f false v.v_ty in
-         if v_ty == v.v_ty then
-           e
-         else
-           make_ ctx (E_var { v with v_ty }) ty'
-       | E_const (c, args) ->
-         let args' = List.map (f false) args in
-         if List.for_all2 equal args args' then
-           e
-         else
-           make_ ctx (E_const (c, args')) ty'
-       | E_bound_var v ->
-         let ty' = f false v.bv_ty in
-         if v.bv_ty == ty' then
-           e
-         else
-           make_ ctx
-             (E_bound_var { v with bv_ty = ty' })
-             (Lazy.from_val (Some ty'))
-       | E_app (hd, a) ->
-         let hd' = f false hd in
-         let a' = f false a in
-         if a == a' && hd == hd' then
-           e
-         else
-           make_ ctx (E_app (f false hd, f false a)) ty'
-       | E_lam (n, tyv, bod) ->
-         let tyv' = f false tyv in
-         let bod' = f true bod in
-         if tyv == tyv' && bod == bod' then
-           e
-         else
-           make_ ctx (E_lam (n, tyv', bod')) ty'
-       | E_arrow (a, b) ->
-         let a' = f false a in
-         let b' = f false b in
-         if a == a' && b == b' then
-           e
-         else
-           make_ ctx (E_arrow (a', b')) ty'
-       | E_kind | E_type | E_box _ -> assert false)
-*)
-
 exception IsSub
 
 let[@inline] is_type_ e =
@@ -525,6 +472,7 @@ module Make_ = struct
   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)
+  let bvar_i store i ~ty : term = make_ store (E_bound_var (Bvar.make i ty))
   let const store c : term = make_ store (E_const c)
   let app store f a = make_ store (E_app (f, a))
   let app_l store f l = List.fold_left (app store) f l
@@ -650,8 +598,12 @@ end
 
 include Make_
 
+let map_shallow store ~f e : t = map_shallow_ ~make:(make_ store) ~f e
+
 (* re-export some internal things *)
 module Internal_ = struct
+  let is_type_ = is_type_
+
   let subst_ store ~recursive t subst =
     subst_ ~make:(make_ store) ~recursive t subst
 end

src/core-logic/term.mli

@@ -9,6 +9,10 @@
 
 open Types_
 
+type nonrec var = var
+type nonrec bvar = bvar
+type nonrec term = term
+
 type t = term
 (** A term, in the calculus of constructions *)
 
@@ -44,13 +48,35 @@ include WITH_SET_MAP_TBL with type t := t
 
 val view : t -> view
 val unfold_app : t -> t * t list
+
 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.
+        It must {b not} traverse [t] as a tree, but rather as a
+        perfectly shared DAG.
+
+        For example, in:
+        {[
+          let x = 2 in
+          let y = f x x in
+          let z = g y x in
+          z = z
+        ]}
+
+        the DAG has the following nodes:
+
+        {[ n1: 2
+           n2: f n1 n1
+           n3: g n2 n1
+           n4: = n3 n3
+         ]}
+    *)
 
 val iter_shallow : f:(bool -> t -> unit) -> t -> unit
 (** [iter_shallow f e] iterates on immediate subterms of [e],
   calling [f trdb e'] for each subterm [e'], with [trdb = true] iff
   [e'] is directly under a binder. *)
 
+val map_shallow : store -> f:(bool -> t -> t) -> t -> t
 val exists_shallow : f:(bool -> t -> bool) -> t -> bool
 val for_all_shallow : f:(bool -> t -> bool) -> t -> bool
 val contains : t -> sub:t -> bool
@@ -81,6 +107,7 @@ val type_of_univ : store -> int -> t
 val var : store -> var -> t
 val var_str : store -> string -> ty:t -> t
 val bvar : store -> bvar -> t
+val bvar_i : store -> int -> ty:t -> t
 val const : store -> const -> t
 val app : store -> t -> t -> t
 val app_l : store -> t -> t list -> t
@@ -126,6 +153,7 @@ end
 (**/**)
 
 module Internal_ : sig
+  val is_type_ : t -> bool
   val subst_ : store -> recursive:bool -> t -> subst -> t
 end
 

unittest/core-logic/t1.expected

@@ -1,6 +1,7 @@
 type0 : Type
 typeof(type0) : Type(1)
 type tower: [Type;Type(1);Type(2);Type(3);Type(4)]
+Bool: [true, false]
 a: a, b: b, typeof(a): Bool
 b2b: (Bool -> Bool)
 p(a): p a
@@ -14,7 +15,7 @@ lxy_px: (\x:Bool. (\y:Bool. p x[1]))
 lxy_px a b: ((\x:Bool. (\y:Bool. p x[1]))) a b
   type: Bool
 (=): =
-  type: (Pi Alpha:Type. (Pi _:Alpha[0]. (Alpha[1] -> Bool)))
+  type: (Pi A:Type. (Pi _:A[0]. (A[1] -> Bool)))
 p2: p2
   type: (tau -> (tau -> Bool))
 t2: = ((tau -> (tau -> Bool))) ((\x:tau. (\y:tau. p2 x[1] y[0]))) (= tau)

unittest/core-logic/t1.ml

@@ -11,7 +11,13 @@ let l =
 
 let () = Fmt.printf "type tower: %a@." (Fmt.Dump.list Term.pp_debug) l
 let () = assert (Term.(equal (type_ store) (type_ store)))
-let bool = Term.const store @@ Str_const.make "Bool" ~ty:(Term.type_ store)
+let bool = T_builtins.bool store
+
+let () =
+  Fmt.printf "%a: [%a, %a]@." Term.pp_debug (T_builtins.bool store)
+    Term.pp_debug (T_builtins.true_ store) Term.pp_debug
+    (T_builtins.false_ store)
+
 let a = Term.const store @@ Str_const.make "a" ~ty:bool
 let a' = Term.const store @@ Str_const.make "a" ~ty:bool
 let b = Term.const store @@ Str_const.make "b" ~ty:bool
@@ -62,20 +68,12 @@ let () =
 (* *)
 
 let tau = Term.const store @@ Str_const.make "tau" ~ty:type_
-
-let f_eq =
-  let vAlpha = Var.make "Alpha" type_ in
-  let tAlpha = Term.var store vAlpha in
-  Term.const store
-  @@ Str_const.make "="
-       ~ty:Term.(pi store vAlpha @@ arrow_l store [ tAlpha; tAlpha ] bool)
+let f_eq = T_builtins.c_eq store
 
 let () =
   Fmt.printf "@[<v2>(=): %a@ type: %a@]@." Term.pp_debug f_eq Term.pp_debug
     (Term.ty f_eq)
 
-let app_eq store x y = Term.app_l store f_eq [ Term.ty x; x; y ]
-
 let p2 =
   Term.const store
   @@ Str_const.make "p2" ~ty:Term.(arrow_l store [ tau; tau ] bool)
@@ -92,7 +90,7 @@ let t2 =
   Term.(
     let t1 = lam store vx @@ lam store vy @@ app_l store p2 [ tX; tY ]
     and t2 = app store f_eq tau in
-    app_eq store t1 t2)
+    T_builtins.eq store t1 t2)
 
 let () =
   Fmt.printf "@[<v2>t2: %a@ type: %a@]@." Term.pp_debug t2 Term.pp_debug