wip: ciclib: start checking types and inductive specs

src/ciclib/inductive.ml

@@ -0,0 +1,35 @@
+module T = Term
+
+type cstor = Types_.cstor = { c_name: string; c_ty: T.t }
+
+type spec = Types_.spec = {
+  name: string;
+  univ_params: Level.var list;
+  n_params: int;
+  ty: T.t;
+  cstors: cstor list;
+}
+(** Inductive spec *)
+
+let pp_cstor out (c : cstor) : unit =
+  Fmt.fprintf out "(@[%s : %a@])" c.c_name T.pp_debug c.c_ty
+
+let pp_spec out (self : spec) : unit =
+  Fmt.fprintf out "@[<2>@[%s %a@]:@ %a [%d params] :=@ %a@]" self.name
+    Fmt.Dump.(list string)
+    self.univ_params T.pp_debug self.ty self.n_params
+    Fmt.(hvbox @@ Dump.(list pp_cstor))
+    self.cstors
+
+let cstor_is_valid (spec : spec) (self : cstor) : bool =
+  let rec loop (ty : T.t) : bool =
+    let hd, _args = T.unfold_app ty in
+    match T.view hd with
+    | T.E_const (c, _) when c.c_name = spec.name ->
+      (* TODO: check that [ty] is correct *)
+      true
+    | _ -> assert false (* TODO: handle recursive cases *)
+  in
+  loop self.c_ty
+
+let is_valid self = List.for_all (cstor_is_valid self) self.cstors

src/ciclib/inductive.mli

@@ -0,0 +1,18 @@
+module T = Term
+
+type cstor = Types_.cstor = { c_name: string; c_ty: T.t }
+
+type spec = Types_.spec = {
+  name: string;
+  univ_params: Level.var list;
+  n_params: int;
+  ty: T.t;
+  cstors: cstor list;
+}
+(** Inductive spec *)
+
+val pp_cstor : cstor Fmt.printer
+val pp_spec : spec Fmt.printer
+
+val is_valid : spec -> bool
+(** Check for validity of the spec *)

src/ciclib/level.ml

@@ -1,9 +1,11 @@
 open Types_
 
+type var = string
+
 type t = level =
   | L_zero
   | L_succ of level
-  | L_var of string  (** variable *)
+  | L_var of var  (** variable *)
   | L_max of level * level  (** max *)
   | L_imax of level * level  (** impredicative max. *)
 
@@ -94,16 +96,20 @@ let[@inline] is_zero l =
   | L_zero -> true
   | _ -> false
 
+type subst = t Util.Str_map.t
+
 (** [subst_v store lvl v u] replaces [v] with [u] in [lvl] *)
-let subst_v (lvl : t) (v : string) (u : t) =
+let subst (subst : subst) (lvl : t) : t =
   let rec loop lvl : t =
     if is_ground lvl then
       lvl
     else (
       match lvl with
-      | L_var v' when v = v' -> u
+      | L_var v ->
-      | L_var _ -> lvl
+        (match Util.Str_map.find v subst with
-      | L_zero -> assert false
+        | l -> l
+        | exception Not_found -> lvl)
+      | L_zero -> lvl
       | L_succ a -> succ (loop a)
       | L_max (a, b) -> max (loop a) (loop b)
       | L_imax (a, b) -> imax (loop a) (loop b)
@@ -111,6 +117,9 @@ let subst_v (lvl : t) (v : string) (u : t) =
   in
   loop lvl
 
+let subst_v (lvl : t) (v : string) (u : t) =
+  subst (Util.Str_map.singleton v u) lvl
+
 let is_one l =
   match l with
   | L_succ a -> is_zero a

src/ciclib/level.mli

@@ -1,9 +1,11 @@
 open Types_
 
+type var = string
+
 type t = level =
   | L_zero
   | L_succ of level
-  | L_var of string  (** variable *)
+  | L_var of var  (** variable *)
   | L_max of level * level  (** max *)
   | L_imax of level * level  (** impredicative max. *)
 
@@ -16,7 +18,7 @@ val as_offset : t -> t * int
 
 val zero : t
 val one : t
-val var : string -> t
+val var : var -> t
 val succ : t -> t
 val of_int : int -> t
 val max : t -> t -> t
@@ -29,6 +31,12 @@ val is_one : t -> bool
 val is_int : t -> bool
 val as_int : t -> int option
 
+(** {2 Substitutions} *)
+
+type subst = t Util.Str_map.t
+
+val subst : subst -> t -> t
+
 (** {2 Judgements}
 
     These are little proofs of some symbolic properties of levels, even

src/ciclib/sidekick_cic_lib.ml

@@ -3,3 +3,4 @@ module Bvar = Bvar
 module Const = Const
 module Level = Level
 module Reduce = Reduce
+module Inductive = Inductive

src/ciclib/term.ml

@@ -48,14 +48,16 @@ let as_type e : level option =
   | E_type l -> Some l
   | _ -> None
 
-let string_of_binder = function
-  | BI -> "BI"
-  | BS -> "BS"
-  | BC -> "BC"
-  | BD -> "BD"
-
 (* debug printer *)
 let expr_pp_with_ ~max_depth out (e : term) : unit =
+  let pp_binder b name pp_ty ty out =
+    match b with
+    | BD -> Fmt.fprintf out "(@[%s : %a@])" name pp_ty ty
+    | BI -> Fmt.fprintf out "{@[%s : %a@]}" name pp_ty ty
+    | BS -> Fmt.fprintf out "{{@[%s : %a@]}}" name pp_ty ty
+    | BC -> Fmt.fprintf out "[@[%s : %a@]]" name pp_ty ty
+  in
+
   let rec loop k ~depth names out e =
     let pp' = loop k ~depth:(depth + 1) names in
     match e.view with
@@ -73,15 +75,15 @@ let expr_pp_with_ ~max_depth out (e : term) : unit =
     | E_app _ ->
       let f, args = unfold_app e in
       Fmt.fprintf out "(%a@ %a)" pp' f (Util.pp_list pp') args
-    | E_lam (binder, name, _ty, bod) ->
+    | E_lam (binder, name, ty, bod) ->
-      Fmt.fprintf out "(@[\\[%s]%s:@[%a@].@ %a@])" (string_of_binder binder)
+      Fmt.fprintf out "(@[fun %t.@ %a@])"
-        name pp' _ty
+        (pp_binder binder name pp' ty)
-        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        (loop (k + 1) ~depth:(depth + 1) (name :: names))
         bod
     | E_pi (binder, name, ty_arg, bod) ->
-      Fmt.fprintf out "(@[Pi[%s] %s:@[%a@].@ %a@])" (string_of_binder binder)
+      Fmt.fprintf out "(@[@<1>∀ %t.@ %a@])"
-        name pp' ty_arg
+        (pp_binder binder name pp' ty_arg)
-        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        (loop (k + 1) ~depth:(depth + 1) (name :: names))
         bod
   in
   Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e
@@ -96,17 +98,14 @@ let as_type_exn e : level =
 let iter_shallow ~f (e : term) : unit =
   match e.view with
   | E_type _ -> ()
-  | _ ->
-    (match e.view with
   | E_const _ -> ()
-    | E_type _ -> assert false
   | E_bound_var _ -> ()
   | E_app (hd, a) ->
     f false hd;
     f false a
   | E_lam (_, _, tyv, bod) | E_pi (_, _, tyv, bod) ->
     f false tyv;
-      f true bod)
+    f true bod
 
 let[@inline] is_type e =
   match e.view with
@@ -249,6 +248,13 @@ let[@inline] app_l f l : term = List.fold_left app f l
 let[@inline] lam b str ~var_ty bod : term = make_ (E_lam (b, str, var_ty, bod))
 let[@inline] pi b str ~var_ty bod : term = make_ (E_pi (b, str, var_ty, bod))
 
+let rec subst_level (s : Level.subst) (e : t) : t =
+  match view e with
+  | E_type u -> type_of_univ (Level.subst s u)
+  | E_const (_, []) -> e
+  | E_const (c, args) -> const c (List.map (Level.subst s) args)
+  | _ -> map_shallow e ~f:(fun _ e' -> subst_level s e')
+
 module DB = struct
   let[@inline] subst_db0 e ~by : t = db_replace_ e [ by ]
   let[@inline] subst_db_l e env : t = db_replace_ e env

src/ciclib/term.mli

@@ -69,6 +69,9 @@ val app_l : t -> t list -> t
 val lam : binder -> string -> var_ty:t -> t -> t
 val pi : binder -> string -> var_ty:t -> t -> t
 
+val subst_level : Level.subst -> t -> t
+(** Substitute level variables in a term *)
+
 (** De bruijn indices *)
 module DB : sig
   val subst_db0 : t -> by:t -> t

src/ciclib/ty_infer.ml

@@ -0,0 +1,67 @@
+open Types_
+module T = Term
+module Str_map = Util.Str_map
+
+module Env = struct
+  type t = {
+    consts: T.t Str_map.t;
+    inductives: Inductive.spec Str_map.t;
+    cstors: Inductive.cstor Str_map.t;
+  }
+
+  let pp_str_map ppx out (m : _ Str_map.t) =
+    Fmt.iter Fmt.Dump.(pair string ppx) out (Str_map.to_iter m)
+
+  let pp out (self : t) =
+    let { consts; inductives; cstors } = self in
+    Fmt.fprintf out "{ @[consts=%a;@ inductives=%a;@ cstors=%a@] }"
+      (pp_str_map T.pp_debug) consts
+      (pp_str_map Inductive.pp_spec)
+      inductives
+      (pp_str_map Inductive.pp_cstor)
+      cstors
+
+  let empty : t =
+    {
+      consts = Str_map.empty;
+      inductives = Str_map.empty;
+      cstors = Str_map.empty;
+    }
+
+  let add_def (self : t) name rhs : t =
+    { self with consts = Str_map.add name rhs self.consts }
+
+  let add_inductive (self : t) (ind : Inductive.spec) : t =
+    {
+      self with
+      inductives = Str_map.add ind.name ind self.inductives;
+      cstors =
+        List.fold_left
+          (fun cstors c -> Str_map.add c.c_name c cstors)
+          self.cstors ind.cstors;
+    }
+end
+
+module Stack = struct
+  type t = T.t list
+
+  let empty = []
+  let push t l : t = t :: l
+  let pp = Fmt.Dump.(list T.pp_debug)
+end
+
+let ty_check (env : Env.t) (st : Stack.t) (self : T.t) : T.t =
+  let rec loop (st : Stack.t) (self : T.t) : T.t =
+    match T.view self with
+    | E_type l -> T.type_of_univ (Level.succ l)
+    | E_bound_var v ->
+      (match List.nth st v.bv_idx with
+      | exception _ ->
+        Error.errorf "bound variable %a is not bound in env %a" Bvar.pp v
+          Stack.pp st
+      | ty -> ty)
+    | E_const (c, args) -> assert false (* TODO: check definition? *)
+    | E_app (_, _) | E_lam (_, _, _, _) | E_pi (_, _, _, _) ->
+      assert false (* TODO: *)
+  in
+  loop st self

src/ciclib/ty_infer.mli

@@ -0,0 +1,27 @@
+module T = Term
+
+(** Env: definitions for constants and inductives *)
+module Env : sig
+  type t
+
+  val empty : t
+  val pp : t Fmt.printer
+
+  val add_def : t -> string -> T.t -> t
+  (** [add_def env name c] defines [name := c] in [env] *)
+
+  val add_inductive : t -> Inductive.spec -> t
+  (** Define an inductive *)
+end
+
+(** Stack: types for bound variables *)
+module Stack : sig
+  type t
+
+  val empty : t
+  val push : T.t -> t -> t
+  val pp : t Fmt.printer
+end
+
+val ty_check : Env.t -> Stack.t -> T.t -> T.t
+(** [ty_check env stack t] infers the type of [t] *)

src/ciclib/types_.ml

@@ -25,3 +25,14 @@ and term = {
   view: term_view;
   mutable flags: int;  (** contains: [highest DB var | 1:has free vars] *)
 }
+
+type cstor = { c_name: string; c_ty: term }
+
+type spec = {
+  name: string;
+  univ_params: string list;
+  n_params: int;
+  ty: term;
+  cstors: cstor list;
+}
+(** Inductive spec *)