wip: make Base really usable, add th-data/th-bool

src/base/Data_ty.ml

@@ -64,7 +64,13 @@ module Cstor = struct
 
   let id c = c.cstor_id
   let hash c = ID.hash c.cstor_id
-  let ty_args c = Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty
+  let ty_args c = Lazy.force c.cstor_args |> List.map Select.ty
+
+  let select_idx c i =
+    let (lazy sels) = c.cstor_args in
+    if i >= List.length sels then invalid_arg "cstor.select_idx: out of bound";
+    List.nth sels i
+
   let equal a b = ID.equal a.cstor_id b.cstor_id
   let pp out c = ID.pp out c.cstor_id
 end
@@ -111,3 +117,23 @@ let select tst s : Term.t =
 
 let is_a tst c : Term.t =
   Term.const tst @@ Const.make (Is_a c) ops ~ty:(Term.bool tst)
+
+let as_data t =
+  match Term.view t with
+  | E_const { Const.c_view = Data d; _ } -> Some d
+  | _ -> None
+
+let as_cstor t =
+  match Term.view t with
+  | E_const { Const.c_view = Cstor c; _ } -> Some c
+  | _ -> None
+
+let as_select t =
+  match Term.view t with
+  | E_const { Const.c_view = Select s; _ } -> Some s
+  | _ -> None
+
+let as_is_a t =
+  match Term.view t with
+  | E_const { Const.c_view = Is_a c; _ } -> Some c
+  | _ -> None

src/base/Data_ty.mli

@@ -40,6 +40,9 @@ end
 module Cstor : sig
   type t = cstor
 
+  val ty_args : t -> ty list
+  val select_idx : t -> int -> select
+
   include Sidekick_sigs.EQ_HASH_PRINT with type t := t
 end
 
@@ -49,3 +52,8 @@ val select : Term.store -> select -> Term.t
 val is_a : Term.store -> cstor -> Term.t
 
 (* TODO: select_ : store -> cstor -> int -> term *)
+
+val as_data : ty -> data option
+val as_select : term -> select option
+val as_cstor : term -> cstor option
+val as_is_a : term -> cstor option

src/base/Sidekick_base.ml

@@ -17,7 +17,7 @@
 *)
 
 module Types_ = Types_
-module Term = Sidekick_core.Term
+module Term = Term
 module Const = Sidekick_core.Const
 module Ty = Ty
 module ID = ID
@@ -27,7 +27,19 @@ module Data_ty = Data_ty
 module Cstor = Data_ty.Cstor
 module Select = Data_ty.Select
 module Statement = Statement
+module Solver = Solver
 module Uconst = Uconst
+module Th_data = Th_data
+module Th_bool = Th_bool
+(* FIXME
+   module Th_lra = Th_lra
+*)
+
+let th_bool : Solver.theory = Th_bool.theory
+let th_data : Solver.theory = Th_data.theory
+(* FIXME
+   let th_lra : Solver.theory = Th_lra.theory
+*)
 
 (* TODO
 

src/base/Solver.ml

@@ -0,0 +1,10 @@
+include Sidekick_smt_solver.Solver
+
+let default_arg =
+  (module struct
+    let view_as_cc = Term.view_as_cc
+    let is_valid_literal _ = true
+  end : Sidekick_smt_solver.Sigs.ARG)
+
+let create_default ?stat ?size ~proof ~theories tst : t =
+  create default_arg ?stat ?size ~proof ~theories tst ()

src/base/Term.ml

@@ -0,0 +1,3 @@
+include Sidekick_core.Term
+
+let view_as_cc = Sidekick_core.Default_cc_view.view_as_cc

src/base/th_bool.ml

@@ -0,0 +1,8 @@
+(** Reducing boolean formulas to clauses *)
+
+let theory : Solver.theory =
+  Sidekick_th_bool_static.theory
+    (module struct
+      let view_as_bool = Form.view
+      let mk_bool = Form.mk_of_view
+    end : Sidekick_th_bool_static.ARG)

src/base/th_data.ml

@@ -0,0 +1,77 @@
+(** Theory of datatypes *)
+
+open Sidekick_core
+
+let arg =
+  (module struct
+    module S = Solver
+    open! Sidekick_th_data
+    open Data_ty
+    module Cstor = Cstor
+
+    (* TODO: we probably want to make sure cstors are not polymorphic?!
+       maybe work on a type/cstor that's applied to pre-selected variables,
+       like [Map A B] with [A],[B] used for the whole type *)
+    let unfold_pi t =
+      let rec unfold acc t =
+        match Term.view t with
+        | Term.E_pi (_, ty, bod) -> unfold (ty :: acc) bod
+        | _ -> List.rev acc, t
+      in
+      unfold [] t
+
+    let as_datatype ty : _ data_ty_view =
+      let args, ret = unfold_pi ty in
+      if args <> [] then
+        Ty_arrow (args, ret)
+      else (
+        match Data_ty.as_data ty, Term.view ty with
+        | Some d, _ ->
+          let cstors = Lazy.force d.data_cstors in
+          let cstors = ID.Map.fold (fun _ c l -> c :: l) cstors [] in
+          Ty_data { cstors }
+        | None, E_app (a, b) -> Ty_other { sub = [ a; b ] }
+        | None, E_pi (_, a, b) -> Ty_other { sub = [ a; b ] }
+        | None, (E_const _ | E_var _ | E_type _ | E_bound_var _ | E_lam _) ->
+          Ty_other { sub = [] }
+      )
+
+    let view_as_data t : _ data_view =
+      let h, args = Term.unfold_app t in
+      match
+        Data_ty.as_cstor h, Data_ty.as_select h, Data_ty.as_is_a h, args
+      with
+      | Some c, _, _, _ ->
+        (* TODO: check arity? store it in [c] ? *)
+        T_cstor (c, args)
+      | None, Some sel, _, [ arg ] ->
+        T_select (sel.select_cstor, sel.select_i, arg)
+      | None, None, Some c, [ arg ] -> T_is_a (c, arg)
+      | _ -> T_other t
+
+    let mk_eq = Term.eq
+    let mk_cstor tst c args : Term.t = Term.app_l tst (Data_ty.cstor tst c) args
+
+    let mk_sel tst c i u =
+      Term.app_l tst (Data_ty.select tst @@ Data_ty.Cstor.select_idx c i) [ u ]
+
+    let mk_is_a tst c u : Term.t =
+      if c.cstor_arity = 0 then
+        Term.eq tst u (Data_ty.cstor tst c)
+      else
+        Term.app_l tst (Data_ty.is_a tst c) [ u ]
+
+    (* NOTE: maybe finiteness should be part of the core typeclass for
+       type consts? or we have a registry for infinite types? *)
+
+    let rec ty_is_finite ty =
+      match Term.view ty with
+      | E_const { Const.c_view = Uconst.Uconst _; _ } -> true
+      | E_const { Const.c_view = Data_ty.Data d; _ } -> true (* TODO: ?? *)
+      | E_pi (_, a, b) -> ty_is_finite a && ty_is_finite b
+      | _ -> true
+
+    let ty_set_is_finite _ _ = () (* TODO: remove, use a weak table instead *)
+  end : Sidekick_th_data.ARG)
+
+let theory = Sidekick_th_data.make arg

src/base/th_lra.ml

@@ -0,0 +1,48 @@
+(* TODO
+
+
+   (** Theory of Linear Rational Arithmetic *)
+   module Th_lra = Sidekick_arith_lra.Make (struct
+     module S = Solver
+     module T = Term
+     module Z = Sidekick_zarith.Int
+     module Q = Sidekick_zarith.Rational
+
+     type term = S.T.Term.t
+     type ty = S.T.Ty.t
+
+     module LRA = Sidekick_arith_lra
+
+     let mk_eq = Form.eq
+
+     let mk_lra store l =
+       match l with
+       | LRA.LRA_other x -> x
+       | LRA.LRA_pred (p, x, y) -> T.lra store (Pred (p, x, y))
+       | LRA.LRA_op (op, x, y) -> T.lra store (Op (op, x, y))
+       | LRA.LRA_const c -> T.lra store (Const c)
+       | LRA.LRA_mult (c, x) -> T.lra store (Mult (c, x))
+
+     let mk_bool = T.bool
+
+     let rec view_as_lra t =
+       match T.view t with
+       | T.LRA l ->
+         let module LRA = Sidekick_arith_lra in
+         (match l with
+         | Const c -> LRA.LRA_const c
+         | Pred (p, a, b) -> LRA.LRA_pred (p, a, b)
+         | Op (op, a, b) -> LRA.LRA_op (op, a, b)
+         | Mult (c, x) -> LRA.LRA_mult (c, x)
+         | To_real x -> view_as_lra x
+         | Var x -> LRA.LRA_other x)
+       | T.Eq (a, b) when Ty.equal (T.ty a) (Ty.real ()) -> LRA.LRA_pred (Eq, a, b)
+       | _ -> LRA.LRA_other t
+
+     let ty_lra _st = Ty.real ()
+     let has_ty_real t = Ty.equal (T.ty t) (Ty.real ())
+     let lemma_lra = Proof.lemma_lra
+
+     module Gensym = Gensym
+   end)
+*)