From 8d70c10e18263c2681f53780223089d21b93dfcf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 7 Mar 2023 23:38:31 -0500 Subject: [PATCH] wip: ciclib: start checking types and inductive specs --- src/ciclib/inductive.ml | 35 ++++++++++++++++++ src/ciclib/inductive.mli | 18 +++++++++ src/ciclib/level.ml | 19 +++++++--- src/ciclib/level.mli | 12 +++++- src/ciclib/sidekick_cic_lib.ml | 1 + src/ciclib/term.ml | 54 +++++++++++++++------------ src/ciclib/term.mli | 3 ++ src/ciclib/ty_infer.ml | 67 ++++++++++++++++++++++++++++++++++ src/ciclib/ty_infer.mli | 27 ++++++++++++++ src/ciclib/types_.ml | 11 ++++++ 10 files changed, 216 insertions(+), 31 deletions(-) create mode 100644 src/ciclib/inductive.ml create mode 100644 src/ciclib/inductive.mli create mode 100644 src/ciclib/ty_infer.ml create mode 100644 src/ciclib/ty_infer.mli diff --git a/src/ciclib/inductive.ml b/src/ciclib/inductive.ml new file mode 100644 index 00000000..83045844 --- /dev/null +++ b/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 diff --git a/src/ciclib/inductive.mli b/src/ciclib/inductive.mli new file mode 100644 index 00000000..6c1862f2 --- /dev/null +++ b/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 *) diff --git a/src/ciclib/level.ml b/src/ciclib/level.ml index e0e42a6d..6053186d 100644 --- a/src/ciclib/level.ml +++ b/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 _ -> lvl - | L_zero -> assert false + | L_var v -> + (match Util.Str_map.find v subst with + | 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 diff --git a/src/ciclib/level.mli b/src/ciclib/level.mli index 5b7721da..7cec98fc 100644 --- a/src/ciclib/level.mli +++ b/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 diff --git a/src/ciclib/sidekick_cic_lib.ml b/src/ciclib/sidekick_cic_lib.ml index 1ab9629c..056ee9e9 100644 --- a/src/ciclib/sidekick_cic_lib.ml +++ b/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 diff --git a/src/ciclib/term.ml b/src/ciclib/term.ml index c20dfc19..dd34d4be 100644 --- a/src/ciclib/term.ml +++ b/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) -> - Fmt.fprintf out "(@[\\[%s]%s:@[%a@].@ %a@])" (string_of_binder binder) - name pp' _ty - (loop (k + 1) ~depth:(depth + 1) ("" :: names)) + | E_lam (binder, name, ty, bod) -> + Fmt.fprintf out "(@[fun %t.@ %a@])" + (pp_binder binder name pp' ty) + (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) - name pp' ty_arg - (loop (k + 1) ~depth:(depth + 1) ("" :: names)) + Fmt.fprintf out "(@[@<1>∀ %t.@ %a@])" + (pp_binder binder name pp' ty_arg) + (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) + | E_const _ -> () + | 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 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 diff --git a/src/ciclib/term.mli b/src/ciclib/term.mli index f87338ed..e033db17 100644 --- a/src/ciclib/term.mli +++ b/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 diff --git a/src/ciclib/ty_infer.ml b/src/ciclib/ty_infer.ml new file mode 100644 index 00000000..772bb688 --- /dev/null +++ b/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 diff --git a/src/ciclib/ty_infer.mli b/src/ciclib/ty_infer.mli new file mode 100644 index 00000000..e317bd73 --- /dev/null +++ b/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] *) diff --git a/src/ciclib/types_.ml b/src/ciclib/types_.ml index c62e1670..6c81beff 100644 --- a/src/ciclib/types_.ml +++ b/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 *)