Add support for generic inductive types.

NOTES.md

@@ -0,0 +1,14 @@
+## Agda
+
+- Agda implementation: [Ulf Norell's PhD thesis](https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf)
+- [MiniAgda](https://github.com/andreasabel/miniagda)
+- implementation of dependent typechecking with NBE: [elaboration zoo](https://github.com/AndrasKovacs/elaboration-zoo) ([OCaml version](https://github.com/smimram/ocaml-elaboration-zoo))
+
+## Coq
+
+- [inductive types](https://rocq-prover.org/doc/v8.19/refman/language/core/inductive.html)
+- [formal description of Coq's termination checker](https://proofassistants.stackexchange.com/questions/1428/formal-description-of-coq-s-termination-checker): in [metaCoq](https://github.com/lgaeher/metacoq/blob/guarded/guarded/guardchecker.v), by [Bruno Barras](https://web.archive.org/web/20230130012659/https://coq.inria.fr/files/adt-2fev10-barras.pdf)
+
+## Lean
+
+- [Lean system description](https://lean-lang.org/papers/system.pdf)

README.md

@@ -4,8 +4,3 @@ DeCaml
 DeCaml is a dependently typed language with OCaml-like syntax, which roughly means Agda dressed as OCaml:
 
 ![agda-caml](https://github.com/user-attachments/assets/9bb6056b-57bb-425a-85fe-55244439f116)
-
-References
-----------
-
-- [elaboration zoo](https://github.com/AndrasKovacs/elaboration-zoo) ([OCaml version](https://github.com/smimram/ocaml-elaboration-zoo))

decaml.opam

@@ -8,12 +8,13 @@ license: "GPL-3.0-or-later"
 homepage: "https://github.com/smimram/decaml"
 bug-reports: "https://github.com/smimram/decaml/issues"
 depends: [
-  "dune" {>= "2.0"}
+  "dune" {>= "3.13"}
   "ocaml"
   "menhir"
+  "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {pinned}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"

dune-project

@@ -1,9 +1,10 @@
-(lang dune 2.0)
+(lang dune 3.13)
 (name decaml)
 (source (github smimram/decaml))
 (license GPL-3.0-or-later)
 (authors "Samuel Mimram <smimram@gmail.com>")
 (maintainers "Samuel Mimram <smimram@gmail.com>")
+(using menhir 3.0)
 
 (generate_opam_files true)
 
@@ -16,4 +17,3 @@
   menhir
  )
 )
-(using menhir 2.0)

src/Makefile

@@ -5,4 +5,5 @@ all:
 	$(MAKE) -C ..
 
 explain:
-	ocamlc -c common.ml extlib.ml preterm.ml term.ml value.ml lang.ml module.ml && menhir --infer --explain parser.mly && rm *.cmi *.cmo parser.ml parser.mli && less parser.conflicts && rm parser.conflicts
+	@dune build
+	less ../_build/default/src/parser.conflicts

src/dune

@@ -3,7 +3,7 @@
 (menhir (modules parser))
 
 (executable
- (name decaml)
+ (public_name decaml)
  (preprocess (pps ppx_deriving.show))
 )
 

src/extlib.ml

@@ -1,5 +1,7 @@
 let failwith fmt = Printf.ksprintf failwith fmt
 
+let fst3 (x,_y,_z) = x
+
 (* Very naive implementation, for backward compatibility... *)
 module Dynarray = struct
   type 'a t = 'a list ref

src/lang.ml

@@ -25,6 +25,7 @@ module Context = struct
       level : int; (** level for creating fresh variables for abstractions *)
       types : (string * V.ty) list; (** the typing environment *)
       bds : [`Bound | `Defined] list; (** whether variables of the environment are defined or bound (this is used for metavariables which only depend on bound variables) *)
+      inductive : V.inductive list; (** declared inductive types *)
     }
 
   (** Empty context. *)
@@ -34,6 +35,7 @@ module Context = struct
       level = 0;
       types = [];
       bds = [];
+      inductive = [];
     }
 
   (** Variables defined in the context. *)
@@ -47,6 +49,7 @@ module Context = struct
       level = ctx.level + 1;
       types = (x,a)::ctx.types;
       bds = `Bound::ctx.bds;
+      inductive = ctx.inductive;
     }
 
   (** Insert a new binding. *)
@@ -59,13 +62,25 @@ module Context = struct
       level = ctx.level + 1;
       types = (x,a)::ctx.types;
       bds = `Defined::ctx.bds;
+      inductive = ctx.inductive;
     }
 
   (* close : (Γ : Con) → Val (Γ, x : A) B → Closure Γ A B *)
   let close ctx (t:value) : V.closure = ctx.environment, V.quote (ctx.level + 1) t
+
+  (** Declare an inductive type. *)
+  let inductive ctx (ind : V.inductive) =
+    V.register_ind ind;
+    let ctx = define ctx ind.name (Ind (ind.name, ind.id, fun () -> ind)) ind.ty in
+    let ctx = List.fold_left (fun ctx (c,a) -> define ctx c (Ind_cons (ind,c,[])) a) ctx ind.constructors in
+    { ctx with inductive = ind :: ctx.inductive }
+
+  (** Find the inductive type associated to a constructor. *)
+  let find_constructor ctx c =
+    List.find_opt (fun ind -> List.mem_assoc c ind.V.constructors) ctx.inductive
 end
 
-let fresh_meta (ctx:Context.t) =
+let fresh_meta (ctx:Context.t) : term =
   let m = Value.fresh_meta () in
   InsertedMeta (m.id, ctx.bds)
 
@@ -190,8 +205,22 @@ let rec infer (ctx:Context.t) (t:preterm) : term * ty =
     let t = check ctx t a in
     t, a
   | Type -> Type, Type
-  | Unit -> Unit, Type
-  | U -> U, Unit
+
+  | Match (_t, l) ->
+    let ind =
+      if l = [] then failwith "empty elimination not supported yet";
+      let c = fst @@ List.hd l in
+      match Context.find_constructor ctx c with
+      | Some ind -> ind
+      | None -> failwith "unknown constructor %s" c
+    in
+    let l = List.map (fun c -> List.assoc c l) (List.map fst ind.constructors) in
+    let l = List.map (fun t -> `Explicit, t) l in
+    infer ctx (P.apps ~pos (P.mk ~pos (Ind_case (ind.name, ind.id))) l)
+  | Ind_case (n,id) ->
+    let ind = V.get_ind id in
+    Ind_case (n,id), ind.case
+
   | Nat -> Nat, Type
   | Z -> Z, Nat
   | S -> S, V.arr Nat Nat

src/lexer.mll

@@ -14,6 +14,12 @@ rule token = parse
   | "rec" { REC }
   | "in" { IN }
   | "fun" { FUN }
+  | "match" { MATCH }
+  | "with" { WITH }
+  | "inductive" { INDUCTIVE }
+  | "begin" { BEGIN }
+  | "end" { END }
+  | "|" { BAR }
   | ":" { COLON }
   | "=" { EQ }
   | "->" { TO }

src/module.ml

@@ -9,37 +9,66 @@ open P
 (** Toplevel declarations. *)
 type decl =
   | Def of (bool * var * P.ty option * P.t) (** a declaration, which might be recursive *)
+  | Ind of P.inductive
 
 (** A module. *)
 type t = decl list
 
 (** Add standard prelude. *)
 let prelude (d:t) : t =
-  let def x t d = (Def (false, x, None, mk t))::d in
-  def "unit" Unit @@
+let def x t d = (Def (false, x, None, mk t))::d in
+  (* let ind name parameters ty constructors d = (Ind {P.name; parameters; ty; constructors})::d in *)
+  (* ind "unit" [] (mk Type) ["U", mk (Var "unit")] @@ *)
+  (* ind "bool" [] (mk Type) ["true", mk (Var "bool"); "false", mk (Var "bool")] @@ *)
   def "nat" Nat @@
   def "Z" Z @@
   def "S" S @@
   d
 
-let eval_decl ctx = function
+let eval_decl ctx d =
+  let open Lang in
+  match d with
   | Def (r,x,a,t) ->
     let t = if r then mk (Fix (mk (Abs ((x,`Explicit,a),t)))) else t in
     (* Printf.printf "%s = %s\n%!" x (Preterm.to_string t); *)
     let t, a =
       match a with
       | Some a ->
-        let a = Lang.check ctx a Type in
-        let a = Lang.eval ctx a in
-        Lang.check ctx t a, a
+        let a = check ctx a Type in
+        let a = eval ctx a in
+        check ctx t a, a
       | None ->
-        Lang.infer ctx t
+        infer ctx t
     in
-    Printf.printf "%s : %s\n%!" x (Lang.to_string ctx a);
-    Printf.printf "%s = %s\n%!" x (T.to_string (Lang.Context.variables ctx) t);
-    Printf.printf "%s = %s\n%!" x (T.to_string (Lang.Context.variables ctx) (Lang.normalize ctx t));
+    Printf.printf "%s : %s\n%!" x (to_string ctx a);
+    Printf.printf "%s = %s\n%!" x (T.to_string (Context.variables ctx) t);
+    Printf.printf "%s = %s\n%!" x (T.to_string (Context.variables ctx) (normalize ctx t));
     print_newline ();
-    (* Lang.Context.bind ctx x a *)
-    Lang.Context.define ctx x (V.eval ctx.environment t) a
+    (* Context.bind ctx x a *)
+    Context.define ctx x (V.eval ctx.environment t) a
+  | Ind ind ->
+    Printf.printf "inductive %s : %s\n\n%!" ind.Preterm.name (String.concat " | " @@ List.map fst ind.constructors);
+    (* TODO: add arguments parameters to the type *)
+    let ty = eval ctx @@ check ctx ind.ty Type in
+    let rec inductive () : V.inductive =
+      let id = V.fresh_ind () in
+      let me = V.Ind (ind.Preterm.name, id, inductive) in
+      let ctx = Context.define ctx ind.name me ty in
+      { Value.
+        id = id;
+        name = ind.name;
+        ty = ty;
+        constructors =
+          List.map
+            (fun (c,a) ->
+               (* Printf.printf "check %s\n%!" (P.to_string a); *)
+               let a = check ctx a Type in
+               (* Printf.printf "checked\n%!"; *)
+               c, eval ctx a
+            ) ind.constructors;
+        case = Type (** TODO... *)
+      }
+    in
+    Context.inductive ctx (inductive ())
 
 let eval ctx (m : t) = List.fold_left eval_decl ctx m

src/parser.mly

@@ -3,7 +3,8 @@ open Preterm
 open Module
 %}
 
-%token LET REC IN EQ COLON HOLE FUN TO
+%token LET REC IN EQ COLON HOLE FUN TO INDUCTIVE BEGIN END
+%token MATCH WITH BAR
 %token LPAR RPAR LACC RACC
 %token TYPE
 %token<string> IDENT
@@ -23,6 +24,10 @@ decls:
 
 decl:
   | def { Def $1 }
+  | INDUCTIVE name=IDENT ty=opttype EQ constructors=list(constructor) { Ind { name; parameters=[]; ty = Option.value ~default:(mk ~pos:$loc(ty) Type) ty; constructors } }
+
+constructor:
+  | BAR c=IDENT COLON ty=mexpr { (c,ty) }
 
 def:
   | LET r=recursive f=IDENT args=args a=opttype EQ e=expr { (r, f, Option.map (pis ~pos:$loc args) a, abss ~pos:$loc args e) }
@@ -37,7 +42,7 @@ args:
 
 arg:
   | LPAR x=IDENT a=opttype RPAR { [x, `Explicit, a] }
-  | LACC xx=idents a=opttype RACC { List.map (fun x -> x, `Implicit, a) xx }
+  | LACC xx=list(IDENT) a=opttype RACC { List.map (fun x -> x, `Implicit, a) xx }
   | x=IDENT { [x, `Explicit, None] }
   | HOLE { ["_", `Explicit, None] }
 
@@ -51,14 +56,18 @@ piargs:
 
 piarg:
   | LPAR x=IDENT COLON a=expr RPAR { [(x, `Explicit, Some a)] }
-  | LACC xx=idents a=opttype RACC { List.map (fun x -> x, `Implicit, a) xx }
+  | LACC xx=list(IDENT) a=opttype RACC { List.map (fun x -> x, `Implicit, a) xx }
 
 expr:
-  | a=aexpr TO b=expr { arr ~pos:$loc a b }
-  | a=piargs TO b=expr { pis ~pos:$loc a b }
-  | FUN x=args TO t=expr { abss ~pos:$loc x t }
+  | MATCH t=expr WITH cases=list(case) { mk ~pos:$loc (Match (t, cases)) }
+  | mexpr { $1 }
+
+mexpr:
+  | a=aexpr TO b=mexpr { arr ~pos:$loc a b }
+  | a=piargs TO b=mexpr { pis ~pos:$loc a b }
+  | FUN x=args TO t=mexpr { abss ~pos:$loc x t }
 /* | LPAR IDENT COLON expr RPAR { mk ~pos:$loc (Cast (mk ~pos:$loc($2) (Var $2), $4)) } */
-  | def IN u=expr { let (r, f, a, t) = $1 in assert (r = false); mk ~pos:$loc (Let (f, a, t, u)) }
+  | def IN u=mexpr { let (r, f, a, t) = $1 in assert (r = false); mk ~pos:$loc (Let (f, a, t, u)) }
   | aexpr { $1 }
 
 // Application
@@ -73,9 +82,9 @@ sexpr:
   | TYPE { mk ~pos:$loc Type }
   | HOLE { mk ~pos:$loc Hole }
   | INT { nat ~pos:$loc $1 }
-  | LPAR RPAR {mk ~pos:$loc U }
+  | LPAR RPAR {mk ~pos:$loc (Var "uu") }
   | LPAR expr RPAR { $2 }
+  | BEGIN expr END { $2 }
 
-idents:
-  | IDENT idents { $1::$2 }
-  | IDENT { [$1] }
+case:
+  | BAR c=IDENT xx=list(IDENT) TO t=sexpr { (c, abss ~pos:$loc(t) (List.map (fun x -> x, `Explicit, None) xx) t) }

src/preterm.ml

@@ -24,12 +24,22 @@ and desc =
   | Fix of t
   | Hole
   | Cast of t * ty (** ensure that a term has given type *)
+  | Match of t * (string * t) list
+  | Ind_case of string * int
 
-  | Unit | U
   | Nat | Z | S
 
 and ty = t
 
+(** An inductive type. *)
+and inductive =
+  {
+    name : string; (** name *)
+    parameters : (string * icit * ty) list;
+    ty : ty;
+    constructors : (string * ty) list; (** constructors with given name and types *)
+  }
+
 let mk ?pos desc =
   let pos = Option.value ~default:Pos.dummy pos in
   { pos; desc }
@@ -47,6 +57,10 @@ let abss ?pos a e =
   in
   aux a
 
+let rec apps ?pos t = function
+  | u::l -> apps ?pos (mk ?pos (App (t,u))) l
+  | [] -> t
+
 (** Multiple pi types. *)
 let pis ?pos args a =
   let pos = Option.value ~default:a.pos pos in
@@ -93,8 +107,11 @@ let rec to_string ?(pa=false) e =
   | Fix t -> "fix " ^ to_string ~pa:true t
   | Cast (t,a) -> Printf.sprintf "(%s : %s)" (to_string t) (to_string a)
   | Type -> "type"
-  | Unit -> "unit"
-  | U -> "()"
+  | Match (t, l) ->
+    let l = List.map (fun (c,t) -> c ^ " -> " ^ to_string t) l in
+    let l = String.concat "\n" l in
+    Printf.sprintf "match %s with\n%s\n" (to_string t) l
+  | Ind_case (ind,_) -> ind ^ "_case"
   | Nat -> "nat"
   | Z -> "Z"
   | S -> "S"