only recursive defs left to implement

Author: thibautbenjamin

dune-project

@@ -8,7 +8,7 @@
 (maintainers "Thibaut Benjamin <thibaut.benjamin@gmail.com>"
              "Chiara Sarti  <cs2197@cam.ac.uk>")
 (license MIT)
-(using menhir 2.0)
+(using menhir 3.0)
 (cram enable)
 (using coq 0.9)
 

examples/test.catt

@@ -0,0 +1,26 @@
+let idU (x : *) : Inv(id x) = can (id x {})
+
+let compididU (x : *) : Inv(comp (id x) (id x)) =
+    can ( (comp (id x) (id x)) { (idU x) , (idU x) })
+
+let compinv (x : *) (y : *) (z : *)
+            (f : x -> y) (g : y -> z)
+            (e : Inv (f)) (e' : Inv (g)) =
+    can ( (comp f g) { e , e' })
+
+coh assoc (x(f)y(g)z(h)w) : comp (comp f g) h -> comp f (comp g h)
+coh assoc- (x(f)y(g)z(h)w) : comp f (comp g h) -> comp (comp f g) h
+
+coind 2of6
+      (x : *) (y : *) (z : *) (w : *)
+      (f : x -> y) (g : y -> z) (h : z -> w)
+      (e : Inv(comp f g)) (e' : Inv(comp g h)) =
+      { g ,
+        comp (left (e)) f,
+        comp h (right (e')) ,
+        comp (assoc (left (e)) f g) (ε (e)) ,
+        comp (assoc- g h (right (e'))) (η (e')) ,
+        can (comp (assoc (left (e)) f g) (ε (e))  { can (assoc (left (e)) f g {}) , Iε (e) } ) ,
+        can (
+        comp (assoc- g h (right (e'))) (η (e')) { can (assoc- g h (right (e')) {}) , Iη (e') } )
+}

lib/dune

@@ -1,5 +1,6 @@
 (menhir
- (modules parser))
+ (modules parser)
+ (explain "true"))
 
 (ocamllex lexer)
 

lib/elaborate.ml

@@ -41,25 +41,33 @@ module Constraints = struct
           (NotUnifiable (Unchecked.ty_to_string ty1, Unchecked.ty_to_string ty2))
 
   and unify_tm cst tm1 tm2 =
-    match (tm1, tm2) with
-    | Meta_tm _, Meta_tm _ when tm1 = tm2 -> ()
-    | Meta_tm _, _ | _, Meta_tm _ -> Queue.enqueue cst.tm (tm1, tm2)
-    | Var v1, Var v2 when v1 = v2 -> ()
-    | Coh (coh1, s1), Coh (coh2, s2) -> (
-        try
-          Coh.check_equal coh1 coh2;
-          unify_sub_ps cst s1 s2
-        with Invalid_argument _ ->
-          raise (NotUnifiable (Coh.to_string coh1, Coh.to_string coh2)))
-    | App (t1, s1), App (t2, s2) when t1 == t2 -> unify_sub cst s1 s2
-    | App (t, s), ((App _ | Coh _ | Var _) as tm2)
-    | ((Coh _ | Var _) as tm2), App (t, s) ->
-        unify_tm cst (Unchecked.tm_apply_sub (Tm.develop t) s) tm2
-    | Var _, Coh _ | Coh _, Var _ | Var _, Var _ ->
-        raise
-          (NotUnifiable (Unchecked.tm_to_string tm1, Unchecked.tm_to_string tm2))
-    | _, _ ->
-        Error.fatal "unification not implemented for invertibility structures"
+    (* Io.debug "unfiying tm %s and %s" *)
+    (*   (Unchecked.tm_to_string tm1) *)
+    (*   (Unchecked.tm_to_string tm2); *)
+    if tm1 = tm2 then ()
+    else
+      match (tm1, tm2) with
+      | Meta_tm _, _ | _, Meta_tm _ -> Queue.enqueue cst.tm (tm1, tm2)
+      | Var v1, Var v2 when v1 = v2 -> ()
+      | Coh (coh1, s1), Coh (coh2, s2) -> (
+          try
+            Coh.check_equal coh1 coh2;
+            unify_sub_ps cst s1 s2
+          with Invalid_argument _ ->
+            raise (NotUnifiable (Coh.to_string coh1, Coh.to_string coh2)))
+      | App (t1, s1), App (t2, s2) when t1 == t2 -> unify_sub cst s1 s2
+      | App (t, s), ((App _ | Coh _ | Var _) as tm2)
+      | ((Coh _ | Var _) as tm2), App (t, s) ->
+          unify_tm cst (Unchecked.tm_apply_sub (Tm.develop t) s) tm2
+      | Var _, Coh _ | Coh _, Var _ | Var _, Var _ ->
+          raise
+            (NotUnifiable
+               (Unchecked.tm_to_string tm1, Unchecked.tm_to_string tm2))
+      | _, _ ->
+          Error.fatal
+            (Printf.sprintf "trying to unify %s and %s"
+               (Unchecked.tm_to_string tm1)
+               (Unchecked.tm_to_string tm2))
 
   and unify_sub cst s1 s2 =
     match (s1, s2) with
@@ -111,6 +119,20 @@ module Constraints = struct
             List.map
               (fun (x, (t, e)) -> (x, (tm_replace_meta_tm (i, tm') t, e)))
               s )
+    | Can (tm, tms) ->
+        Can
+          ( tm_replace_meta_tm (i, tm') tm,
+            List.map (tm_replace_meta_tm (i, tm')) tms )
+    | IS (inv, u) -> IS (inv, tm_replace_meta_tm (i, tm') u)
+    | Coind (t0, t1, t2, t3, t4, t5, t6) ->
+        Coind
+          ( tm_replace_meta_tm (i, tm') t0,
+            tm_replace_meta_tm (i, tm') t1,
+            tm_replace_meta_tm (i, tm') t2,
+            tm_replace_meta_tm (i, tm') t3,
+            tm_replace_meta_tm (i, tm') t4,
+            tm_replace_meta_tm (i, tm') t5,
+            tm_replace_meta_tm (i, tm') t6 )
     | _ ->
         Error.fatal
           "resolution of meta_variables in invertibility\n\
@@ -194,8 +216,26 @@ module Constraints = struct
     aux c { uty = []; utm = [] }
 end
 
+let inverse_ty ty =
+  match ty with
+  | Obj | Inv _ -> assert false
+  | Arr (ty, u, v) -> Arr (ty, v, u)
+  | Meta_ty _ -> Meta.new_ty ()
+
+let lunit_ty tm linv =
+  let y = Construct.tgt 1 tm in
+  Construct.arr (Construct.comp linv tm) (Construct.id y)
+
+let runit_ty tm rinv =
+  let x = Construct.src 1 tm in
+  Construct.arr (Construct.comp tm rinv) (Construct.id x)
+
 module Constraints_typing = struct
   let rec tm ctx meta_ctx t cst =
+    (* Io.debug "constraint typing term %s in ctx %s, meta_ctx %s" *)
+    (*   (Unchecked.tm_to_string t) *)
+    (*   (Unchecked.ctx_to_string ctx) *)
+    (*   (Unchecked.meta_ctx_to_string meta_ctx); *)
     Io.info ~v:5
       (lazy
         (Printf.sprintf "constraint typing term %s in ctx %s, meta_ctx %s"
@@ -222,6 +262,41 @@ module Constraints_typing = struct
         let ty = Ty.forget (Tm.typ t) in
         let s = sub ctx meta_ctx s tgt cst in
         (App (t, s), Unchecked.ty_apply_sub ty s)
+    | Can (t, tms) ->
+        let t, _ = tm ctx meta_ctx t cst in
+        let tms = List.map (fun t -> fst (tm ctx meta_ctx t cst)) tms in
+        (* ignore the constraints on tms : no elaboration *)
+        (Can (t, tms), Inv t)
+    | IS (inv, e) ->
+        let e, te = tm ctx meta_ctx e cst in
+        let u = match te with Inv u -> u | _ -> assert false in
+        let u, tu = tm ctx meta_ctx u cst in
+        let tui = inverse_ty tu in
+        let ty =
+          match inv with
+          | LInv -> tui
+          | RInv -> tui
+          | Lunit -> lunit_ty (u, tu) (IS (LInv, e), tui)
+          | Runit -> runit_ty (u, tu) (IS (RInv, e), tui)
+          | Lwit -> Inv (IS (Lunit, e))
+          | Rwit -> Inv (IS (Runit, e))
+        in
+        (IS (inv, e), ty)
+    | Coind (t0, t1, t2, t3, t4, t5, t6) ->
+        let t0, ty0 = tm ctx meta_ctx t0 cst in
+        let t1, ty1 = tm ctx meta_ctx t1 cst in
+        let t2, ty2 = tm ctx meta_ctx t2 cst in
+        let t3, ty3 = tm ctx meta_ctx t3 cst in
+        let t4, ty4 = tm ctx meta_ctx t4 cst in
+        let t5, ty5 = tm ctx meta_ctx t5 cst in
+        let t6, ty6 = tm ctx meta_ctx t6 cst in
+        Constraints.unify_ty cst (inverse_ty ty0) ty1;
+        Constraints.unify_ty cst (inverse_ty ty0) ty2;
+        Constraints.unify_ty cst (lunit_ty (t0, ty0) (t1, ty1)) ty3;
+        Constraints.unify_ty cst (runit_ty (t0, ty0) (t2, ty2)) ty4;
+        Constraints.unify_ty cst (Inv t3) ty5;
+        Constraints.unify_ty cst (Inv t4) ty6;
+        (Coind (t0, t1, t2, t3, t4, t5, t6), Inv t0)
     | _ -> Error.fatal "invertibility structures in constraint typing"
 
   and sub src meta_ctx s tgt cst =

lib/environment.ml

@@ -41,9 +41,10 @@ let add_let v c ?ty t =
     let pp_data = (Var.to_string v, 0, []) in
     let kc = Kernel.Ctx.check c in
     let tm = Kernel.check_term kc ?ty ~name:pp_data t in
-    let ty = Kernel.(Ty.forget (Tm.typ tm)) in
+    let ty = Kernel.Tm.typ tm in
+    let dim_output = Kernel.Ty.dim ty in
+    let ty = Kernel.Ty.forget ty in
     let dim_input = Unchecked.dim_ctx c in
-    let dim_output = Unchecked.dim_ty ty in
     Io.info ~v:4
       (lazy
         (Printf.sprintf "term %s of type %s added to environment"

lib/kernel.ml

@@ -20,6 +20,7 @@ module rec Sub : sig
   val free_vars : t -> Var.t list
   val src : t -> Ctx.t
   val tgt : t -> Ctx.t
+  val args_of_dim : int -> t -> Tm.t list
 end = struct
   type t = {
     list : Tm.t list;
@@ -81,6 +82,16 @@ end = struct
         sub
 
   let forget s = s.unchecked
+
+  let args_of_dim n s =
+    let rec provide s tgt =
+      match (s, tgt) with
+      | [], [] -> []
+      | tm :: s, (_, ty) :: tgt when Ty.dim ty == n -> tm :: provide s tgt
+      | _ :: s, _ :: tgt -> provide s tgt
+      | _, _ -> assert false
+    in
+    provide s.list (Ctx.value s.tgt)
 end
 
 (** A context, associating a type to each context variable. *)
@@ -326,6 +337,7 @@ and Ty : sig
   val ctx : t -> Ctx.t
   val dim : t -> int
   val base_inv : t -> Tm.t
+  val inv : Tm.t -> Ty.t
 end = struct
   open Unchecked (Coh) (Tm)
   module Unchecked = Make (Coh) (Tm)
@@ -407,6 +419,14 @@ end = struct
   let forget t = t.unchecked
   let to_string ty = Unchecked.ty_to_string (forget ty)
 
+  let inv t =
+    match (Tm.typ t).e with
+    | Obj | Inv _ -> assert false
+    | Arr (_, _, _) ->
+        let e = Inv t in
+        let c = (Tm.typ t).c in
+        { c; e; unchecked = Inv (Tm.forget t) }
+
   (** Test for equality. *)
   let check_equal ty1 ty2 =
     Ctx.check_equal ty1.c ty2.c;
@@ -432,7 +452,7 @@ end = struct
     match t.e with
     | Obj -> 0
     | Arr (a, _, _) -> 1 + dim a
-    | Inv _ -> raise IsInv
+    | Inv u -> dim (Tm.typ u)
 end
 
 (** Operations on terms. *)
@@ -484,6 +504,7 @@ end = struct
     | Coh of Coh.t * Sub.t
     | App of Tm.t * Sub.t
     | IS of inv * Tm.t
+    | Can of Tm.t * Tm.t list
     | Coind of Tm.t * Tm.t * Tm.t * Tm.t * Tm.t * Tm.t * Tm.t
     | Rec of Tm.t * Tm.t * Tm.t * Tm.t * Tm.t * Tm.t * Tm.t
 
@@ -511,7 +532,7 @@ end = struct
     | Var x -> x :: fvty
     | Coh (_, sub) | App (_, sub) -> Sub.free_vars sub
     | IS (_, t) -> free_vars t
-    (* | Can (t, _) -> free_vars t *)
+    | Can (t, _) -> free_vars t
     | Coind (t, _, _, _, _, _, _) -> free_vars t
     | Rec (t, _, _, _, _, _, _) -> free_vars t
 
@@ -533,7 +554,16 @@ end = struct
     let ty = Constr.arr (Constr.comp t rinv) (Constr.id x) in
     Ty.check c ty
 
-  let rec check c ?ty ?name t =
+  let rec args_max_coh c tm =
+    let tm = Tm.develop tm in
+    let tm = check c tm in
+    match tm.e with
+    | Var _ | App _ | Coind _ | Rec _ | Can _ | IS _ -> assert false
+    | Coh (c, sub) ->
+        let n = Coh.dim c in
+        Sub.args_of_dim n sub
+
+  and check c ?ty ?name t =
     Io.info ~v:5
       (lazy
         (Printf.sprintf "building\n    kernel term %s in context %s"
@@ -573,17 +603,34 @@ end = struct
                     let linv = check c (IS (LInv, tm)) in
                     lunit_ty c base_inv linv
                 | Runit ->
-                    let rinv = check c (IS (LInv, tm)) in
+                    let rinv = check c (IS (RInv, tm)) in
                     runit_ty c base_inv rinv
                 | Lwit -> Ty.check c (Inv (IS (Lunit, tm)))
                 | Rwit -> Ty.check c (Inv (IS (Runit, tm)))
               in
               let tm = { ty; e; unchecked = t; developped = Some t; name } in
               Hashtbl.add tbl (c, t) tm;
               tm
-          | Can (_, _) ->
-              Error.fatal
-                "canonical invertibility structures not yet implemented"
+          | Can (tm, tms) ->
+              let tm = check c tm in
+              let args = args_max_coh c tm in
+              let rec check_next args invs =
+                match (args, invs) with
+                | t :: args, e :: invs ->
+                    let e = Tm.check c ~ty:(Ty.inv t) e in
+                    let invs = check_next args invs in
+                    e :: invs
+                | [], [] -> []
+                | _ ->
+                    Error.fatal
+                      "wrong number of arguments in canonical structure"
+              in
+              let tms = check_next args tms in
+              let e = Can (tm, tms) in
+              let ty = Ty.inv tm in
+              let tm = { ty; e; unchecked = t; developped = Some t; name } in
+              Hashtbl.add tbl (c, t) tm;
+              tm
           | Coind (t0, t1, t2, t3, t4, t5, t6) ->
               let t0_checked = check c t0 in
               let _, x, y = Ty.retrieve_arrow t0_checked.ty in
@@ -593,7 +640,7 @@ end = struct
                 check c ~ty:(lunit_ty c t0_checked t1_checked) t3
               in
               let t4_checked =
-                check c ~ty:(runit_ty c t0_checked t1_checked) t4
+                check c ~ty:(runit_ty c t0_checked t2_checked) t4
               in
               let t5_checked = check c ~ty:(Ty.check c (Inv t3)) t5 in
               let t6_checked = check c ~ty:(Ty.check c (Inv t4)) t6 in

lib/kernel.mli

@@ -53,6 +53,7 @@ and Ty : sig
   type t
 
   val forget : t -> Unchecked_types(Coh)(Tm).ty
+  val dim : t -> int
 end
 
 and Tm : sig

lib/lexer.mll

@@ -16,6 +16,7 @@ rule token = parse
   | "can" { CAN }
   | "coind" { COIND }
   | "rec" { REC }
+  | "," { COMMA }
   | "check" { CHECK }
   | "let" { LET }
   | "in" { IN }

lib/parser.mly

@@ -34,7 +34,7 @@
 
 %token COH OBJ MOR WILD IGNORE
 %token INVTY LEFT RIGHT LUNIT RUNIT LWITNESS RWITNESS CAN COIND REC
-%token LPAR RPAR LBRA RBRA LCUR RCUR COL BANG OP AT
+%token LPAR RPAR LBRA RBRA LCUR RCUR COL BANG OP AT COMMA
 %token <string> BUILTIN
 %token <int*int*int> CONECOMP
 %token <int*int*int> CYLCOMP
@@ -76,8 +76,8 @@ cmd:
   | SET IDENT EQUAL IDENT { Set ($2,$4) }
   | SET IDENT EQUAL INT { Set ($2,$4) }
   | DECLARE IDENT EQUAL builtin { Decl_builtin (Var.make_var $2,$4) }
-  | COIND IDENT args_or_ps EQUAL tmexpr tmexpr tmexpr tmexpr tmexpr tmexpr tmexpr { CoindDef (Var.make_var $2, $3, $5, $6, $7, $8, $9, $10, $11) }
-  | REC IDENT args_or_ps EQUAL tmexpr tmexpr tmexpr tmexpr tmexpr tmexpr tmexpr { RecDef (Var.make_var $2, $3, $5, $6, $7, $8, $9, $10, $11) }
+  | COIND IDENT args_or_ps EQUAL LCUR tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr RCUR { CoindDef (Var.make_var $2, $3, $6, $8, $10, $12, $14, $16, $18) }
+  | REC IDENT args_or_ps EQUAL LCUR tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr COMMA tmexpr RCUR { RecDef (Var.make_var $2, $3, $6, $8, $10, $12, $14, $16, $18) }
 
 args_of_same_ty :
   | IDENT COL tyexpr { [Var.make_var $1, $3], $3 }
@@ -132,14 +132,17 @@ simple_tmexpr:
   | INV LPAR tmexpr RPAR { Inverse $3 }
   | UNIT LPAR tmexpr RPAR { Unit $3 }
   | invertibility_destructor LPAR tmexpr RPAR { ISR($1, $3) }
-  | CAN LPAR tmexpr LBRA tmexpr_list RBRA RPAR { CanR($3, $5) }
+  | CAN LPAR tmexpr LCUR tmexpr_list RCUR RPAR { CanR($3, $5) }
   | IDENT { VarR (Var.make_var $1) }
   | builtin_tm { $1 }
 
-tmexpr_list:
-  | tmexpr tmexpr_list { $1::$2 }
-  | { [] }
+nonempty_tmexpr_list:
+  | tmexpr_list COMMA  tmexpr { $3::$1 }
+  | tmexpr { [ $1 ] }
 
+tmexpr_list :
+  | nonempty_tmexpr_list { $1 }
+  | { [] }
 
 functed_tmexpr:
   | LBRA maybe_functed_tmexpr RBRA { let t,n = $2 in t,n+1 }