feat: handle typechecking and term building for datatypes

src/base-term/Base_types.ml

@@ -26,6 +26,9 @@ and fun_ = {
 
 and fun_view =
   | Fun_undef of fun_ty (* simple undefined constant *)
+  | Fun_select of select
+  | Fun_cstor of cstor
+  | Fun_is_a of cstor
   | Fun_def of {
       pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
       abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
@@ -75,12 +78,21 @@ and ty_def =
 
 and data = {
   data_id: ID.t;
-  data_cstors: (ty * select list) ID.Map.t;
+  data_cstors: cstor ID.Map.t lazy_t;
+  data_as_ty: ty lazy_t;
+}
+
+and cstor = {
+  cstor_id: ID.t;
+  cstor_is_a: ID.t;
+  cstor_args: select list lazy_t;
+  cstor_ty_as_data: data;
+  cstor_ty: ty lazy_t;
 }
 
 and select = {
-  select_name: ID.t lazy_t;
+  select_id: ID.t;
-  select_cstor: ID.t;
+  select_cstor: cstor;
   select_ty: ty lazy_t;
   select_i: int;
 }
@@ -96,6 +108,10 @@ and value =
       id: ID.t;
       ty: ty;
     } (** a named constant, distinct from any other constant *)
+  | V_cstor of {
+      c: cstor;
+      args: value list;
+    }
   | V_custom of {
       view: value_custom_view;
       pp: value_custom_view Fmt.printer;
@@ -130,24 +146,35 @@ let id_of_fun a = a.fun_id
 
 let[@inline] eq_ty a b = a.ty_id = b.ty_id
 
-let eq_value a b = match a, b with
+let eq_cstor c1 c2 =
+  ID.equal c1.cstor_id c2.cstor_id
+
+let rec eq_value a b = match a, b with
   | V_bool a, V_bool b -> a=b
   | V_element e1, V_element e2 ->
     ID.equal e1.id e2.id && eq_ty e1.ty e2.ty
   | V_custom x1, V_custom x2 ->
     x1.eq x1.view x2.view
-  | V_bool _, _ | V_element _, _ | V_custom _, _
+  | V_cstor x1, V_cstor x2 ->
+    eq_cstor x1.c x2.c &&
+    CCList.equal eq_value x1.args x2.args
+  | (V_bool _ | V_element _ | V_custom _ | V_cstor _), _
     -> false
 
-let hash_value a = match a with
+let rec hash_value a = match a with
   | V_bool a -> Hash.bool a
   | V_element e -> ID.hash e.id
   | V_custom x -> x.hash x.view
+  | V_cstor x ->
+    Hash.combine3 42 (ID.hash x.c.cstor_id) (Hash.list hash_value x.args)
 
-let pp_value out = function
+let rec pp_value out = function
   | V_bool b -> Fmt.bool out b
   | V_element e -> ID.pp out e.id
   | V_custom c -> c.pp out c.view
+  | V_cstor {c;args=[]} -> ID.pp out c.cstor_id
+  | V_cstor {c;args} ->
+    Fmt.fprintf out "(@[%a@ %a@])" ID.pp c.cstor_id (Util.pp_list pp_value) args
 
 let pp_db out (i,_) = Format.fprintf out "%%%d" i
 
@@ -383,8 +410,23 @@ end = struct
 end
 
 module Fun : sig
-  type view = fun_view
+  type view = fun_view =
-  type t = fun_
+    | Fun_undef of fun_ty (* simple undefined constant *)
+    | Fun_select of select
+    | Fun_cstor of cstor
+    | Fun_is_a of cstor
+    | Fun_def of {
+        pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
+        abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+        do_cc: bool; (* participate in congruence closure? *)
+        relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
+        ty : ID.t -> term IArray.t -> ty; (* compute type *)
+        eval: value IArray.t -> value; (* evaluate term *)
+      }
+  type t = fun_ = {
+    fun_id: ID.t;
+    fun_view: fun_view;
+  }
 
   val id : t -> ID.t
   val view : t -> view
@@ -394,6 +436,9 @@ module Fun : sig
   val as_undefined : t -> (t * Ty.Fun.t) option
   val as_undefined_exn : t -> t * Ty.Fun.t
   val is_undefined : t -> bool
+  val select : select -> t
+  val cstor : cstor -> t
+  val is_a : cstor -> t
 
   val do_cc : t -> bool
   val mk_undef : ID.t -> Ty.Fun.t -> t
@@ -404,8 +449,23 @@ module Fun : sig
   module Map : CCMap.S with type key = t
   module Tbl : CCHashtbl.S with type key = t
 end = struct
-  type view = fun_view
+  type view = fun_view =
-  type t = fun_
+    | Fun_undef of fun_ty (* simple undefined constant *)
+    | Fun_select of select
+    | Fun_cstor of cstor
+    | Fun_is_a of cstor
+    | Fun_def of {
+        pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
+        abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+        do_cc: bool; (* participate in congruence closure? *)
+        relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
+        ty : ID.t -> term IArray.t -> ty; (* compute type *)
+        eval: value IArray.t -> value; (* evaluate term *)
+      }
+  type t = fun_ = {
+    fun_id: ID.t;
+    fun_view: fun_view;
+  }
 
   let[@inline] id t = t.fun_id
   let[@inline] view t = t.fun_view
@@ -413,7 +473,7 @@ end = struct
 
   let as_undefined (c:t) = match view c with
     | Fun_undef ty -> Some (c,ty)
-    | Fun_def _ -> None
+    | Fun_def _ | Fun_cstor _ | Fun_select _ | Fun_is_a _ -> None
 
   let[@inline] is_undefined c = match view c with Fun_undef _ -> true | _ -> false
 
@@ -424,9 +484,12 @@ end = struct
   let[@inline] mk_undef id ty = make id (Fun_undef ty)
   let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty)
   let[@inline] mk_undef' id args ret = mk_undef id {fun_ty_args=args; fun_ty_ret=ret}
+  let is_a c : t = make c.cstor_is_a (Fun_is_a c)
+  let cstor c : t = make c.cstor_id (Fun_cstor c)
+  let select sel : t = make sel.select_id (Fun_select sel)
 
   let[@inline] do_cc (c:t) : bool = match view c with
-    | Fun_undef _ -> true
+    | Fun_cstor _ | Fun_select _ | Fun_undef _ | Fun_is_a _ -> true
     | Fun_def {do_cc;_} -> do_cc
 
   let equal a b = ID.equal a.fun_id b.fun_id
@@ -580,7 +643,10 @@ end = struct
                ))
             ty_args;
           ty_ret
+        | Fun_is_a _ -> Ty.bool
         | Fun_def def -> def.ty f.fun_id args
+        | Fun_select s -> Lazy.force s.select_ty
+        | Fun_cstor c -> Lazy.force c.cstor_ty
       end
 
   let iter f view =
@@ -641,6 +707,10 @@ module Term : sig
   val not_ : state -> t -> t
   val ite : state -> t -> t -> t -> t
 
+  val select : state -> select -> t -> t
+  val app_cstor : state -> cstor -> t IArray.t -> t
+  val is_a : state -> cstor -> t -> t
+
   (** Obtain unsigned version of [t], + the sign as a boolean *)
   val abs : state -> t -> t * bool
 
@@ -743,6 +813,10 @@ end = struct
   let[@inline] not_ st a = make st (Term_cell.not_ a)
   let ite st a b c  : t = make st (Term_cell.ite a b c)
 
+  let select st sel t : t = app_fun st (Fun.select sel) (IArray.singleton t)
+  let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t)
+  let app_cstor st c args : t = app_fun st (Fun.cstor c) args
+
   (* might need to tranfer the negation from [t] to [sign] *)
   let abs tst t : t * bool = match view t with
     | Bool false -> true_ tst, false
@@ -822,6 +896,10 @@ module Value : sig
   type t = value =
     | V_bool of bool
     | V_element of {id: ID.t; ty: ty}
+    | V_cstor of {
+        c: cstor;
+        args: value list;
+      }
     | V_custom of {
         view: value_custom_view;
         pp: value_custom_view Fmt.printer;
@@ -838,6 +916,7 @@ module Value : sig
   val is_bool : t -> bool
   val is_true : t -> bool
   val is_false : t -> bool
+  val cstor_app : cstor -> t list -> t
 
   val fresh : Term.t -> t
 
@@ -848,6 +927,10 @@ end = struct
   type t = value =
     | V_bool of bool
     | V_element of {id: ID.t; ty: ty}
+    | V_cstor of {
+        c: cstor;
+        args: value list;
+      }
     | V_custom of {
         view: value_custom_view;
         pp: value_custom_view Fmt.printer;
@@ -864,6 +947,7 @@ end = struct
   let[@inline] is_bool = function V_bool _ -> true | _ -> false
   let[@inline] is_true = function V_bool true -> true | _ -> false
   let[@inline] is_false = function V_bool false -> true | _ -> false
+  let cstor_app c args : t = V_cstor {c;args}
 
   let equal = eq_value
   let hash = hash_value
@@ -876,14 +960,28 @@ end
 module Data = struct
   type t = data = {
     data_id: ID.t;
-    data_cstors: (ty * select list) ID.Map.t;
+    data_cstors: cstor ID.Map.t lazy_t;
+    data_as_ty: ty lazy_t;
   }
+
+  let pp out d = ID.pp out d.data_id
+end
+
+module Cstor = struct
+  type t = cstor = {
+    cstor_id: ID.t;
+    cstor_is_a: ID.t;
+    cstor_args: select list lazy_t;
+    cstor_ty_as_data: data;
+    cstor_ty: ty lazy_t;
+  }
+  let equal = eq_cstor
 end
 
 module Select = struct
   type t = select = {
-    select_name: ID.t lazy_t;
+    select_id: ID.t;
-    select_cstor: ID.t;
+    select_cstor: cstor;
     select_ty: ty lazy_t;
     select_i: int;
   }
@@ -918,6 +1016,7 @@ module Statement = struct
         ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret
     | Stmt_assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t
     | Stmt_exit -> Fmt.string out "(exit)"
-    | Stmt_data _ -> assert false (* TODO *)
+    | Stmt_data l ->
+      Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data.pp) l
     | Stmt_define _ -> assert false (* TODO *)
 end

src/base-term/Model.ml

@@ -154,12 +154,32 @@ let eval (m:t) (t:Term.t) : Value.t option =
       let b = aux b in
       if Value.equal a b then Value.true_ else Value.false_
     | App_fun (c, args) ->
-      match Fun.view c with
+      match Fun.view c, (args :_ IArray.t:> _ array) with
-      | Fun_def udef ->
+      | Fun_def udef, _ ->
         (* use builtin interpretation function *)
         let args = IArray.map aux args in
         udef.eval args
-      | Fun_undef _ ->
+      | Fun_cstor c, _ ->
+        Value.cstor_app c (IArray.to_list_map aux args)
+      | Fun_select s, [|u|] ->
+        begin match aux u with
+          | V_cstor {c;args} when Cstor.equal c s.select_cstor ->
+            List.nth args s.select_i
+          | v_u ->
+            Error.errorf "cannot eval selector %a@ on %a" Term.pp t Value.pp v_u
+        end
+      | Fun_is_a c1, [|u|] ->
+        begin match aux u with
+          | V_cstor {c=c2;args=_} ->
+            Value.bool (Cstor.equal c1 c2)
+          | v_u ->
+            Error.errorf "cannot eval is-a %a@ on %a" Term.pp t Value.pp v_u
+        end
+      | Fun_select _, _ ->
+        Error.errorf "bad selector term %a" Term.pp t
+      | Fun_is_a _, _ ->
+        Error.errorf "bad is-a term %a" Term.pp t
+      | Fun_undef _, _ ->
         try Term.Map.find t m.values
         with Not_found ->
           begin match Fun.Map.find c m.funs with

src/main/main.ml

@@ -108,7 +108,8 @@ let main () =
   let solver =
     let theories = [
       Process.th_bool ;
-    ] (* TODO: more theories *)
+      Process.th_cstor;
+    ]
     in
     Process.Solver.create ~store_proof:!check ~theories tst ()
   in

src/smtlib/Process.ml

@@ -76,10 +76,9 @@ module Check_cc = struct
                Stat.incr n_calls;
                check_conflict si c))
       ()
-
 end
 
-(* TODO
+(* TODO: use external proof checker instead: check-sat(φ + model)
 (* check SMT model *)
 let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : unit =
   Log.debug 1 "(smt.check-smt-model)";
@@ -213,8 +212,8 @@ let process_stmt
     (* TODO: more? *)
   in
   begin match stmt with
-    | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA") ->
+    | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT") ->
-      E.return () (* TODO: QF_DT *)
+      E.return ()
     | Statement.Stmt_set_logic s ->
       Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
       E.return ()
@@ -246,25 +245,20 @@ let process_stmt
       Solver.add_clause solver (IArray.singleton atom);
       E.return()
     | Statement.Stmt_data _ ->
-      Error.errorf "cannot deal with datatypes yet"
+      E.return()
     | Statement.Stmt_define _ ->
       Error.errorf "cannot deal with definitions yet"
   end
 
-(* TODO: this + datatypes
 module Th_cstor = Sidekick_th_cstor.Make(struct
-    module Solver = Solver
+    module S = Solver
-    module T = Solver.A.Term
+    open Base_types
+    open Sidekick_th_cstor
 
-    let[@inline] view_as_cstor t = match view t with
+    let view_as_cstor t = match Term.view t with
-      | App_cst (c, args) when Fun.do_cc
+      | Term.App_fun ({fun_view=Fun.Fun_cstor _;_} as f, args) -> T_cstor (f, args)
-      | If (a,b,c) -> T_ite (a,b,c)
-      | Bool b -> T_bool b
       | _ -> T_other t
-    end
-
   end)
-   *)
 
 module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
@@ -272,5 +266,5 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   include Form
 end)
 
-let th_bool : Solver.theory =
+let th_bool : Solver.theory = Th_bool.theory
-  Th_bool.theory
+let th_cstor : Solver.theory = Th_cstor.theory

src/smtlib/Process.mli

@@ -8,6 +8,7 @@ module Solver
                             and type T.Ty.t = Ty.t
 
 val th_bool : Solver.theory
+val th_cstor : Solver.theory
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Typecheck.ml

@@ -26,8 +26,6 @@ module Ctx = struct
   type kind =
     | K_ty of ty_kind
     | K_fun of Fun.t
-    | K_cstor of Fun.t * Ty.t
-    | K_select of Fun.t * Ty.t * BT.Select.t
 
   and ty_kind =
     | K_atomic of Ty.def
@@ -35,35 +33,24 @@ module Ctx = struct
 
   type t = {
     tst: T.state;
-    names: ID.t StrTbl.t;
+    names: (ID.t * kind) StrTbl.t;
-    kinds: kind ID.Tbl.t;
     lets: T.t StrTbl.t;
-    data: (ID.t * Ty.t) list ID.Tbl.t; (* data -> cstors *)
     mutable loc: Loc.t option; (* current loc *)
   }
 
   let create (tst:T.state) : t = {
     tst;
     names=StrTbl.create 64;
-    kinds=ID.Tbl.create 64;
     lets=StrTbl.create 16;
-    data=ID.Tbl.create 64;
     loc=None;
   }
 
   let loc t = t.loc
   let set_loc ?loc t = t.loc <- loc
 
-  let add_id_ self (s:string) (k:ID.t -> kind): ID.t =
+  let add_id_ self (s:string) (id:ID.t) (k:kind) : unit =
-    let id = ID.make s in
+    StrTbl.add self.names s (id,k);
-    StrTbl.add self.names s id;
+    ()
-    ID.Tbl.add self.kinds id (k id);
-    id
-
-  let add_id self (s:string) (k:kind): ID.t = add_id_ self s (fun _ ->k)
-
-  let add_data self (id:ID.t) cstors: unit =
-    ID.Tbl.add self.data id cstors
 
   (* locally bind [bs] and call [f], then remove bindings *)
   let with_lets (self:t) (bs:(string*T.t) list) (f:unit -> 'a): 'a =
@@ -72,32 +59,14 @@ module Ctx = struct
       ~h:(fun () ->
           List.iter (fun (v,_) -> StrTbl.remove self.lets v) bs)
 
-  let find_kind self (id:ID.t) : kind =
+  let find_ty_def self (s:string) : Ty.def =
-    try ID.Tbl.find self.kinds id
+    match StrTbl.get self.names s with
-    with Not_found -> Error.errorf "did not find kind of ID `%a`" ID.pp id
+    | Some (_, K_ty (K_atomic def)) -> def
-
+    | _ -> Error.errorf "expected %s to be an atomic type" s
-  let find_ty_def self (id:ID.t) : Ty.def =
-    match find_kind self id with
-    | K_ty (K_atomic def) -> def
-    | _ -> Error.errorf "expected %a to be an atomic type" ID.pp id
-
-  let as_data _self (ty:Ty.t) : BT.Data.t =
-    match Ty.view ty with
-    | Ty.Ty_atomic {def=Ty.Ty_data d;_} -> d
-    | _ -> Error.errorf "expected %a to be a constant type" Ty.pp ty
 
   let pp_kind out = function
     | K_ty _ -> Format.fprintf out "type"
-    | K_cstor (_,ty) ->
-      Format.fprintf out "(@[cstor : %a@])" Ty.pp ty
-    | K_select (_,ty,s) ->
-      Format.fprintf out "(@[select-%a-%d : %a@])"
-        ID.pp s.Select.select_cstor s.Select.select_i Ty.pp ty
     | K_fun f -> Fun.pp out f
-
-  let pp out t =
-    Format.fprintf out "ctx {@[%a@]}"
-      Fmt.(seq ~sep:(return "@ ") @@ pair ID.pp pp_kind) (ID.Tbl.to_seq t.kinds)
 end
 
 let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx)
@@ -112,7 +81,7 @@ let check_bool_ ctx t =
     ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t)
   )
 
-let find_id_ ctx (s:string): ID.t =
+let find_id_ ctx (s:string): ID.t * Ctx.kind =
   try StrTbl.find ctx.Ctx.names s
   with Not_found -> errorf_ctx ctx "name `%s` not in scope" s
 
@@ -131,7 +100,7 @@ let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with
     ill_typed ctx "cannot handle ints for now"
     (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *)
   | PA.Ty_app (f, l) ->
-    let def = Ctx.find_ty_def ctx @@ find_id_ ctx f in
+    let def = Ctx.find_ty_def ctx f in
     let l = List.map (conv_ty ctx) l in
     Ty.atomic def l
   | PA.Ty_arrow _ ->
@@ -158,25 +127,18 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
     begin match StrTbl.find ctx.Ctx.lets f with
       | u -> u
       | exception Not_found ->
-        let id = find_id_ ctx f in
+        begin match find_id_ ctx f with
-        begin match Ctx.find_kind ctx id with
+          | _, Ctx.K_fun f -> T.const tst f
-          | Ctx.K_fun f -> T.const tst f
+          | _, Ctx.K_ty _ ->
-          | Ctx.K_ty _ ->
+            errorf_ctx ctx "expected term, not type; got `%s`" f
-            errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id
-          | Ctx.K_cstor _ ->
-            errorf_ctx ctx "cannot handle constructors for now"
-            (* FIXME: A.const id ty *)
-          | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported"
         end
     end
   | PA.App (f, args) ->
-    let id = find_id_ ctx f in
     let args = List.map (conv_term ctx) args in
-    begin match Ctx.find_kind ctx id with
+    begin match find_id_ ctx f with
-      | Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args)
+      | _, Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args)
-      | _ ->
+      | _, Ctx.K_ty _ ->
-        (* TODO: constructor + selector *)
+        errorf_ctx ctx "expected function, got type `%s` instead" f
-        errorf_ctx ctx "expected constant application; got `%a`" ID.pp id
     end
   | PA.If (a,b,c) ->
     let a = conv_term ctx a in
@@ -214,6 +176,13 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
     let a = conv_term ctx a in
     let b = conv_term ctx b in
     Form.imply tst a b
+  | PA.Is_a (s, u) ->
+    let u = conv_term ctx u in
+    begin match find_id_ ctx s with
+      | _, Ctx.K_fun {Fun.fun_view=Fun_cstor c; _} ->
+        Term.is_a tst c u
+      | _ -> errorf_ctx ctx "expected `%s` to be a constructor" s
+    end
   | PA.Match (_lhs, _l) ->
     errorf_ctx ctx "TODO: support match in %a" PA.pp_term t
     (* FIXME: do that properly, using [with_lets] with selectors
@@ -370,19 +339,20 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
   | PA.Stmt_set_info (a,b) -> [Stmt.Stmt_set_info (a,b)]
   | PA.Stmt_exit -> [Stmt.Stmt_exit]
   | PA.Stmt_decl_sort (s,n) ->
-    let id = Ctx.add_id_ ctx s
+    let id = ID.make s in
-        (fun id -> Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id))) in
+    Ctx.add_id_ ctx s id
+      (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id)));
     [Stmt.Stmt_ty_decl (id, n)]
   | PA.Stmt_decl fr ->
     let f, args, ret = conv_fun_decl ctx fr in
-    let id = Ctx.add_id_ ctx f
+    let id = ID.make f in
-        (fun id -> Ctx.K_fun (Fun.mk_undef' id args ret)) in
+    Ctx.add_id_ ctx f id
+      (Ctx.K_fun (Fun.mk_undef' id args ret));
     [Stmt.Stmt_decl (id, args,ret)]
-  | PA.Stmt_data l when List.for_all (fun ((_,n),_) -> n=0) l ->
+  | PA.Stmt_data l ->
-    errorf_ctx ctx "cannot typecheck datatypes"
-    (* FIXME
     (* first, read and declare each datatype (it can occur in the other
       datatypes' constructors) *)
+    (* TODO:remove
     let pre_parse ((data_name,arity),cases) =
       if arity <> 0 then (
         errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name;
@@ -391,48 +361,77 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
       data_id, cases
     in
     let l = List.map pre_parse l in
+       *)
+    let module Cstor = Base_types.Cstor in
+    let cstors_of_data data (cstors:PA.cstor list) : Cstor.t ID.Map.t =
+      let parse_case {PA.cstor_name; cstor_args; cstor_ty_vars} =
+        if cstor_ty_vars <> [] then (
+          errorf_ctx ctx "cannot handle polymorphic constructor %s" cstor_name;
+        );
+        let cstor_id = ID.make cstor_name in
+        (* how to translate selectors *)
+        let mk_selectors (cstor:Cstor.t) =
+          List.mapi
+            (fun i (name,ty) ->
+               let select_id = ID.make name in
+               let sel = {
+                 Select.
+                 select_id;
+                 select_ty=lazy (conv_ty ctx ty);
+                 select_cstor=cstor;
+                 select_i=i;
+               } in
+               (* now declare the selector *)
+               Ctx.add_id_ ctx name select_id
+                 (Ctx.K_fun (Fun.select sel));
+               sel)
+            cstor_args
+        in
+        let rec cstor = {
+          Cstor.
+          cstor_id;
+          cstor_is_a = ID.makef "is-a.%s" cstor_name; (* every fun needs a name *)
+          cstor_args=lazy (mk_selectors cstor);
+          cstor_ty_as_data=data;
+          cstor_ty=data.data_as_ty;
+        } in
+        (* declare cstor *)
+        Ctx.add_id_ ctx cstor_name cstor_id (Ctx.K_fun (Fun.cstor cstor));
+        cstor_id, cstor
+      in
+      let cstors = List.map parse_case cstors in
+      ID.Map.of_list cstors
+    in
     (* now parse constructors *)
     let l =
      List.map
-       (fun (data_id, (cstors:PA.cstor list)) ->
+       (fun ((data_name,arity), (cstors:PA.cstor list)) ->
-         let data_ty = Ty.const data_id in
+         if arity <> 0 then (
-         let parse_case {PA.cstor_name=c; cstor_args; cstor_ty_vars} =
+           (* TODO: handle poly datatypes properly *)
-           if cstor_ty_vars <> [] then (
+           errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name;
-             errorf_ctx ctx "cannot handle polymorphic constructor %s" c;
+         );
+         let data_id = ID.make data_name in
+         let rec data = {
+           Data.
+           data_id;
+           data_cstors=lazy (cstors_of_data data cstors);
+           data_as_ty=lazy (
+             let def = Ty.Ty_data data in
+             Ty.atomic def []
            );
-           let selectors =
+         } in
-             List.map (fun (n,ty) -> Some n, conv_ty_fst ctx ty) cstor_args
+         Ctx.add_id_ ctx data_name data_id
-           in
+           (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data data)));
-           let ty_args = List.map snd selectors in
+         data)
-           (* declare cstor *)
-           let ty_c = Ty.arrow_l ty_args data_ty in
-           let id_c = Ctx.add_id ctx c (Ctx.K_cstor ty_c) in
-           (* now declare selectors *)
-           List.iteri
-             (fun i (name_opt,ty) -> match name_opt with
-                | None -> ()
-                | Some select_str ->
-                  (* declare this selector *)
-                  let rec select_name = lazy
-                    (Ctx.add_id ctx select_str
-                       (Ctx.K_select (ty,
-                          {A.select_name; select_cstor=id_c; select_i=i})))
-                  in
-                  ignore (Lazy.force select_name))
-             selectors;
-           (* return cstor *)
-           id_c, ty_c
-         in
-         let cstors = List.map parse_case cstors in
-         (* update info on [data] *)
-         Ctx.add_data ctx data_id cstors;
-         {Ty.data_id; data_cstors=ID.Map.of_list cstors})
       l
     in
-    [A.Data l]
+    (* now force definitions *)
-       *)
+    List.iter
-  | PA.Stmt_data _ ->
+      (fun {Data.data_cstors=lazy m;data_as_ty=lazy _;_} ->
-    errorf_ctx ctx "not implemented: parametric datatypes" PA.pp_stmt stmt
+         ID.Map.iter (fun _ {Cstor.cstor_args=lazy _;_} -> ()) m;
+         ())
+      l;
+    [Stmt.Stmt_data l]
   | PA.Stmt_funs_rec _defs ->
     errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt
       (* TODO
@@ -447,9 +446,9 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
       {PA.fr_decl={PA.fun_ty_vars=[]; fun_args=[]; fun_name; fun_ret}; fr_body} ->
     (* turn [def f : ret := body] into [decl f : ret; assert f=body] *)
     let ret = conv_ty ctx fun_ret in
-    let id = Ctx.add_id_ ctx fun_name
+    let id = ID.make fun_name in
-        (fun id -> Ctx.K_fun (Fun.mk_undef_const id ret)) in
+    let f = Fun.mk_undef_const id ret in
-    let f = match Ctx.find_kind ctx id with Ctx.K_fun f->f | _ -> assert false in
+    Ctx.add_id_ ctx fun_name id (Ctx.K_fun f);
     let rhs = conv_term ctx fr_body in
     [ Stmt.Stmt_decl (id,[],ret);
       Stmt.Stmt_assert (Form.eq tst (T.const tst f) rhs);

src/smtlib/Typecheck.mli

@@ -14,7 +14,6 @@ type 'a or_error = ('a, string) CCResult.t
 module Ctx : sig
   type t
   val create: T.state -> t
-  val pp : t CCFormat.printer
 end
 
 val conv_term : Ctx.t -> PA.term -> T.t

src/smtlib/dune

@@ -3,7 +3,7 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
-   sidekick.mini-cc msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-cstor msat.backend smtlib-utils)
  (flags :standard -warn-error -27-37 -open Sidekick_util))
 
 ; TODO: enable warn-error again

src/th-cstor/Sidekick_th_cstor.ml

@@ -1,7 +1,7 @@
 (** {1 Theory for constructors} *)
 
 type ('c,'t) cstor_view =
-  | T_cstor of 'c * 't list
+  | T_cstor of 'c * 't IArray.t
   | T_other of 't
 
 let name = "th-cstor"
@@ -28,7 +28,7 @@ module Make(A : ARG) : S with module A = A = struct
     t: T.t;
     n: N.t;
     cstor: Fun.t;
-    args: T.t list;
+    args: T.t IArray.t;
   }
   (* associate to each class a unique constructor term in the class (if any) *)
 
@@ -65,8 +65,8 @@ module Make(A : ARG) : S with module A = A = struct
         in
         if Fun.equal cr1.cstor cr2.cstor then (
           (* same function: injectivity *)
-          assert (List.length cr1.args = List.length cr2.args);
+          assert (IArray.length cr1.args = IArray.length cr2.args);
-          List.iter2
+          IArray.iter2
             (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl)
             cr1.args cr2.args
         ) else (

src/th-cstor/dune

@@ -1,7 +1,7 @@
 
 (library
   (name Sidekick_th_cstor)
-  (public_name sidekick.smt.th-cstor)
+  (public_name sidekick.th-cstor)
   (libraries containers sidekick.core sidekick.util)
   (flags :standard -open Sidekick_util))