feat: Add fixpoints

examples/inductives.gcic

@@ -2,8 +2,8 @@ Inductive bool : Type :=
 | false : bool 
 | true : bool.
 
-Definition rec2 (c : Type@1) (fb tb : c) (b : bool) : c :=
-match@bool b as z return c with 
+Definition rec2 (c : bool -> Type@1) (fb : c false) (tb : c true) (b : bool) : c b :=
+match@bool b as z return c z with 
 | false => fb 
 | true => tb 
 end.
@@ -22,7 +22,7 @@ Inductive W (a : Type) (b : a -> Type) : Type@1 :=
 | sup (x : a) (f : b x -> W a b) : W a b.
 
 
-Definition natarity : bool -> Type := rec2 Type void unit.
+Definition natarity : bool -> Type := rec2 (fun (b : bool) => Type) void unit.
 
 Definition natW : Type@1 := W bool natarity.
 
@@ -41,3 +41,27 @@ match@sum s as z return c with
 | inl a b x => l x 
 | inr a b x => r x 
 end.
+
+Fixpoint recW (A : Type) (B : A -> Type) (E : W A B -> Type@1) 
+  (e : forall (x : A) (f : B x -> W A B) (rec : forall (b : B x), E (f b)), E (sup A B x f))
+  (w : W A B) {struct w} : E w :=
+match@W w as z return E z with
+| sup A B a f => e a f (fun (b : B a) => recW A B E e (f b))
+end.
+
+Definition recnatW (C : natW -> Type@1) 
+  (e : forall (x : bool) (f : natarity x -> W bool natarity) (rec : forall (b : natarity x), C (f b)), C (sup bool natarity x f))
+  (n : W bool natarity) : C n := recW bool natarity C e n.
+
+Definition double : natW -> natW :=
+recnatW (fun (x : natW) => natW) 
+  (rec2 (fun (b : bool ) =>
+    forall (f : natarity b -> natW)
+          (g : natarity b -> natW),
+          W bool natarity)
+        (fun (f : void -> natW)
+            (g : void -> natW) =>
+            zero)
+        (fun (f : unit -> natW)
+            (g : unit -> natW) =>
+            succ (succ (g tt)))).

examples/vector.gcic

@@ -0,0 +1,18 @@
+Inductive Nat : Type := 
+| O : Nat 
+| Succ (n : Nat) : Nat.
+
+Inductive unit : Type := | tt : unit. 
+
+Inductive prod (A B : Type) : Type := 
+| pair (a : A) (b : B) : prod A B.
+
+Fixpoint vec (A : Type) (n : Nat) {struct n} : Type := 
+    match@Nat n as z return Type with 
+    | O => unit 
+    | Succ m => prod A (vec A m) 
+    end.  
+
+Definition nil (A : Type) : vec A O := tt. 
+
+Definition cons (A : Type) (a : A) (n : Nat) (v : vec A n) : vec A (Succ n) := pair A (vec A n) a v.

lib/castCIC.ml

@@ -191,6 +191,44 @@ module Executor : Main.Executor = struct
       Const.add_cache name { name; ty = elab_ty; term = elab_term };
       Ok (Definition (name, ty))
 
+  let execute_fixpoint struct_id gdef : (cmd_result, execute_error) result =
+    let empty_ctx = Name.Map.empty in
+    match gdef with
+    | { name; ty; term } ->
+      let* rarg =
+        GCIC.prod_args ty
+        |> List.find_index_opt struct_id
+        |> Option.to_result
+             ~none:
+               (Format.asprintf
+                  "recursive argument not found: %s"
+                  (Name.to_string struct_id))
+      in
+      let* elab_ty, _ =
+        CastCICElab.elab_univ empty_ctx ty
+        |> Result.map_error Elaboration.Cast_CIC.string_of_error
+      in
+      let fix =
+        GCIC.Fixpoint { fix_id = name; fix_body = term; fix_type = ty; fix_rarg = rarg }
+      in
+      Const.add name { name; ty; term = fix };
+      Const.add_cache name { name; ty = elab_ty; term = Const name };
+      (* Temporary definition por typing *)
+      let* elab_term =
+        CastCICElab.check_elab empty_ctx term elab_ty
+        |> Result.map_error Elaboration.Cast_CIC.string_of_error
+      in
+      let elab_fix =
+        CastCIC.Fixpoint
+          { fix_id = name; fix_body = elab_term; fix_type = elab_ty; fix_rarg = rarg }
+      in
+      Const.add_cache name { name; ty = elab_ty; term = elab_fix };
+      let* _ =
+        CastCICTyping.check_type empty_ctx elab_term elab_ty
+        |> Result.map_error Typing.Cast_CIC.string_of_error
+      in
+      Ok (Definition (name, ty))
+
   let execute_inductive ind ctors : (cmd_result, execute_error) result =
     let empty_ctx = Name.Map.empty in
     let elab_univ_param (elab_params, ctx) (id, param) =
@@ -253,6 +291,7 @@ module Executor : Main.Executor = struct
     | Elab t -> execute_elab t
     | Set f -> execute_set_flag f
     | Define gdef -> execute_definition gdef
+    | Fix (struct_id, gdef) -> execute_fixpoint struct_id gdef
     | Load filename -> execute_load file_parser filename
     | Inductive (ind, ctors) -> execute_inductive ind ctors
 

lib/common/castCIC.ml

@@ -41,6 +41,7 @@ type term =
       ; f : Name.t
       ; branches : branch list
       }
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -54,13 +55,25 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
+(** Checks if a term is a lambda expression *)
+let is_lambda = function
+  | Lambda _ -> true
+  | _ -> false
+
 (** Pretty printer *)
 module Pretty = struct
   open Fmt
 
   (** Returns if a term requires a parenthesis for unambiguation *)
   let need_parens = function
-    | Lambda _ | Prod _ | Cast _ | Match _ -> true
+    | App _ | Lambda _ | Prod _ | Cast _ | Match _ | Fixpoint _ -> true
     | Inductive (_, _, args) -> args <> []
     | Constructor { params; args; _ } -> params <> [] || args <> []
     | _ -> false
@@ -79,7 +92,7 @@ module Pretty = struct
     | Var x -> pf ppf "%a" Name.pp x
     | Universe 0 -> pf ppf "▢"
     | Universe i -> pf ppf "▢%i" i
-    | App (t, t') -> pf ppf "@[%a@ %a@]" maybe_parens t maybe_parens t'
+    | App (t, t') -> pf ppf "@[%a@ %a@]" maybe_parens_app t maybe_parens t'
     | Lambda _ as t -> group_lambda_args [] t |> pp_lambda ppf
     | Prod { id; dom; body } as t ->
       if Name.is_default id
@@ -98,6 +111,7 @@ module Pretty = struct
       pf ppf "@[%a@ %a@]" Name.pp ctor (list ~sep:sp maybe_parens) (params @ args)
     | Match { discr; z; pred; _ } ->
       pf ppf "@[match %a as %a return@ %a with@]" pp discr Name.pp z pp pred
+    | Fixpoint { fix_body; _ } -> pf ppf "@[fix@ %a@]" maybe_parens fix_body
 
   (** Pretty-prints an argument of a lambda or prod *)
   and pp_arg ppf (x, ty) = pf ppf "@[(%a : %a)@]" Name.pp x pp ty
@@ -111,7 +125,15 @@ module Pretty = struct
     pf ppf "@[<hov 1>∀%a,@ %a@]" (list ~sep:sp pp_arg) args pp body
 
   (** Adds parenthesis around a term if needed *)
-  and maybe_parens ppf t = if need_parens t then parens pp ppf t else pp ppf t
+  and maybe_parens ppf t =
+    match t with
+    | _ -> if need_parens t then parens pp ppf t else pp ppf t
+
+  (** Adds parenthesis around a term if needed *)
+  and maybe_parens_app ppf t =
+    match t with
+    | App _ -> pp ppf t
+    | _ -> if need_parens t then parens pp ppf t else pp ppf t
 
   (** Returns the prettified version of a term *)
   let to_string = to_to_string pp
@@ -170,6 +192,9 @@ let rec subst ctx = function
       ; pred = subst (Context.add mi.z (Var mi.z) ctx) mi.pred
       ; branches = List.map (subst_branch ctx) mi.branches
       }
+  | Fixpoint fi ->
+    Fixpoint
+      { fi with fix_body = subst ctx fi.fix_body; fix_type = subst ctx fi.fix_type }
 
 and subst_branch ctx br =
   let ids_ctx = List.map (fun x -> x, Var x) br.ids |> List.to_seq in
@@ -230,8 +255,15 @@ let rec alpha_equal t1 t2 =
     && m1.z = m2.z
     && alpha_equal m1.pred m2.pred
     && List.equal alpha_equal_branch m1.branches m2.branches
+  | Fixpoint fi1, Fixpoint fi2 -> alpha_equal_fix fi1 fi2
   | _ -> false
 
+and alpha_equal_fix fi1 fi2 =
+  fi1.fix_id = fi2.fix_id
+  && alpha_equal fi1.fix_body fi2.fix_body
+  && alpha_equal fi1.fix_type fi2.fix_type
+  && fi1.fix_rarg = fi2.fix_rarg
+
 let rec subst_tele ?(acc = []) ts params =
   match ts, params with
   | [], [] -> List.rev acc

lib/common/castCIC.mli

@@ -36,6 +36,7 @@ type term =
       ; f : Name.t
       ; branches : branch list
       }
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -49,6 +50,16 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
+(** Checks if a term is a lambda expression *)
+val is_lambda : term -> bool
+
 (** Pretty printers *)
 val pp_term : Format.formatter -> term -> unit
 

lib/common/gCIC.ml

@@ -24,6 +24,7 @@ type term =
   | Ascription of term * term
   | UnknownT of int
   | Const of Name.t
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -37,6 +38,13 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
 (** Pretty printers *)
 
 (** Pretty printer *)
@@ -45,7 +53,7 @@ module Pretty = struct
 
   (** Returns if a term requires a parenthesis for disambiguation *)
   let need_parens = function
-    | Lambda _ | Prod _ | Ascription _ | Match _ -> true
+    | Lambda _ | Prod _ | Ascription _ | Match _ | Fixpoint _ -> true
     | Inductive (_, _, args) | Constructor (_, args) -> args <> []
     | _ -> false
 
@@ -89,6 +97,7 @@ module Pretty = struct
     | Ascription (t, ty) -> pf ppf "@[%a ::@ %a@]" pp t pp ty
     | UnknownT i -> pf ppf "?▢%i" i
     | Const x -> pf ppf "%a" Name.pp x
+    | Fixpoint { fix_body; _ } -> pf ppf "@[fix@ %a@]" maybe_parens fix_body
 
   (** Pretty-prints an argument of a lambda or prod *)
   and pp_arg ppf (x, ty) = pf ppf "@[(%a : %a)@]" Name.pp x pp ty
@@ -143,8 +152,15 @@ let rec eq t1 t2 =
   | Ascription (t1, ty1), Ascription (t2, ty2) -> eq t1 t2 && eq ty1 ty2
   | UnknownT i, UnknownT j -> i = j
   | Const c1, Const c2 -> c1 = c2
+  | Fixpoint fi1, Fixpoint fi2 -> eq_fix fi1 fi2
   | _ -> false
 
+and eq_fix fi1 fi2 =
+  fi1.fix_id = fi2.fix_id
+  && eq fi1.fix_body fi2.fix_body
+  && eq fi1.fix_type fi2.fix_type
+  && fi1.fix_rarg = fi2.fix_rarg
+
 and branch_eq b1 b2 =
   b1.ctor = b2.ctor && List.equal ( = ) b1.ids b2.ids && eq b1.term b2.term
 
@@ -153,3 +169,7 @@ let rec get_universe_lvl (t : term) =
   | Universe lvl -> lvl
   | Prod fi -> get_universe_lvl fi.body
   | _ -> failwith "type of inductive definition must be a universe"
+
+let rec prod_args : term -> Name.t list = function
+  | Prod fi -> fi.id :: prod_args fi.body
+  | _ -> []

lib/common/gCIC.mli

@@ -24,6 +24,7 @@ type term =
   | Ascription of term * term
   | UnknownT of int
   | Const of Name.t
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -37,6 +38,13 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
 (** Pretty printers *)
 val pp_term : Format.formatter -> term -> unit
 
@@ -52,3 +60,6 @@ val eq : term -> term -> bool
 (** Gets the level of a universe or a product.
     Raises an error if applied on something else. *)
 val get_universe_lvl : term -> int
+
+(** Returns the list of arguments of a product type. *)
+val prod_args : term -> Name.t list

lib/common/std.ml

@@ -38,4 +38,12 @@ module List = struct
       | _ -> List.rev acc, []
     in
     go [] n xs
+
+  let find_index_opt x xs =
+    let rec go acc xs =
+      match xs with
+      | [] -> None
+      | y :: ys -> if x = y then Some acc else go (acc + 1) ys
+    in
+    go 0 xs
 end

lib/elaboration/cast_CIC.ml

@@ -170,7 +170,7 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
         then (
           let new_ids = List.map (fun _ -> Var (new_identifier ())) b1.ids in
           let ids1 = List.combine b1.ids new_ids in
-          let ids2 = List.combine b1.ids new_ids in
+          let ids2 = List.combine b2.ids new_ids in
           let subst_body body ids =
             List.fold_left
               (fun body (old_id, new_id) -> subst1 old_id new_id body)
@@ -186,6 +186,7 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
       && m1.ind = m2.ind
       && are_consistent m1.pred m2.pred
       && List.equal are_consistent_branch m1.branches m2.branches
+    | Fixpoint fi1, Fixpoint fi2 -> fi1.fix_id = fi2.fix_id
     | _ -> false
 
   (** The elaboration procedure, as per the paper *)
@@ -266,6 +267,19 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
         | Not_found -> Error (`Err_free_identifier x)
       in
       Ok (CastCIC.Const x, ty)
+    | Fixpoint fi ->
+      let* elab_fix_type, _ = elab_univ ctx fi.fix_type in
+      let fix_ctx = Name.Map.add fi.fix_id elab_fix_type ctx in
+      let* elab_fix_body = check_elab fix_ctx fi.fix_body elab_fix_type in
+      let elab_fix =
+        CastCIC.Fixpoint
+          { fix_id = fi.fix_id
+          ; fix_body = elab_fix_body
+          ; fix_type = elab_fix_type
+          ; fix_rarg = fi.fix_rarg
+          }
+      in
+      Ok (elab_fix, elab_fix_type)
 
   (* CHECK rule from the original paper *)
   and check_elab ctx term (s_ty : CastCIC.term) =

lib/main.ml

@@ -139,6 +139,7 @@ module Make (E : Executor) : Run = struct
     | Elab t -> Elab (of_parsed_term t)
     | Set cfg -> Set cfg
     | Define d -> Define (of_parsed_const_decl d)
+    | Fix (rarg, d) -> Fix (rarg, of_parsed_const_decl d)
     | Load filename -> Load filename
     | Inductive (ind, ctors) ->
       let ind' = of_parsed_ind_decl ind in

lib/parsing/command.ml

@@ -8,5 +8,6 @@ type 'a t =
   | Elab of 'a
   | Set of Config.Flag.t
   | Define of 'a const_decl
+  | Fix of Common.Id.Name.t * 'a const_decl
   | Load of string
   | Inductive of 'a ind_decl * 'a ctor_decl list