Merge pull request thibautbenjamin#76 from thibautbenjamin/feature/me…

…ta-operations-errors

Feature/meta operations errors

lib/error.ml

@@ -53,8 +53,7 @@ let unknown_id s =
 
 let functorialisation t s =
   Io.error
-    "Could not compute the functorialisation of %s for the following reason:\n\
-     %s%!"
+    "Could not compute the transformation of %s for the following reason:\n%s%!"
     t s;
   raise InvalidEntry
 

lib/functorialisation.ml

@@ -3,6 +3,8 @@ open Kernel
 open Unchecked_types.Unchecked_types (Coh)
 
 exception FunctorialiseMeta
+exception NotClosed
+exception Unsupported
 
 let coh_depth1 = ref (fun _ -> Error.fatal "Uninitialised forward reference")
 
@@ -17,6 +19,28 @@ module Memo = struct
       res
 end
 
+let check_upwards_closed ctx l =
+  let closed =
+    List.for_all
+      (fun x ->
+        List.for_all
+          (fun (y, (ty, _)) ->
+            (not (Unchecked.ty_contains_var ty x)) || List.mem y l)
+          ctx)
+      l
+  in
+  if not closed then raise NotClosed
+
+let check_codim1 c n l =
+  let is_comdim1 =
+    List.for_all
+      (fun x ->
+        let ty, _ = List.assoc x c in
+        Unchecked.dim_ty ty >= n - 1)
+      l
+  in
+  if not is_comdim1 then raise Unsupported
+
 let rec next_round l =
   match l with
   | [] -> ([], [])
@@ -184,8 +208,9 @@ and coh_depth0 coh l =
   check_coh psf ty (name, susp, func_data)
 
 and coh coh l =
-  let ps, _, _ = Coh.forget coh in
+  let ps, ty, _ = Coh.forget coh in
   let c = Unchecked.ps_to_ctx ps in
+  check_upwards_closed c l;
   let depth0 = List.for_all (fun (x, (_, e)) -> e || not (List.mem x l)) c in
   let cohf =
     if depth0 then
@@ -194,7 +219,9 @@ and coh coh l =
       let pscf = ctx (Unchecked.ps_to_ctx ps) l in
       let cohf = coh_depth0 coh l in
       (Coh (cohf, sf), pscf)
-    else !coh_depth1 coh l
+    else (
+      check_codim1 c (Unchecked.dim_ty ty) l;
+      !coh_depth1 coh l)
   in
   cohf
 
@@ -246,27 +273,32 @@ and tm c t s =
     tm c t next
   else (t, c)
 
+(* Public API *)
+let report_errors f str =
+  try f () with
+  | FunctorialiseMeta ->
+      Error.functorialisation (Lazy.force str)
+        "cannot functorialise meta-variables"
+  | NotClosed ->
+      Error.functorialisation (Lazy.force str)
+        "list of functorialised arguments is not closed"
+  | Unsupported ->
+      Error.functorialisation (Lazy.force str)
+        "higher-dimensional transformations in depth >= 0 are not yet supported"
+
 (* Functorialisation of a coherence: exposed function *)
 let coh c l =
-  try coh c l
-  with FunctorialiseMeta ->
-    Error.functorialisation
-      ("coherence: " ^ Coh.to_string c)
-      (Printf.sprintf "cannot functorialise meta-variables")
+  report_errors (fun _ -> coh c l) (lazy ("coherence: " ^ Coh.to_string c))
 
 let coh_depth0 c l =
-  try coh_depth0 c l
-  with FunctorialiseMeta ->
-    Error.functorialisation
-      ("coherence: " ^ Coh.to_string c)
-      (Printf.sprintf "cannot functorialise meta-variables")
+  report_errors
+    (fun _ -> coh_depth0 c l)
+    (lazy ("coherence: " ^ Coh.to_string c))
 
 let coh_successively c l =
-  try coh_successively c l
-  with FunctorialiseMeta ->
-    Error.functorialisation
-      ("coherence: " ^ Coh.to_string c)
-      (Printf.sprintf "cannot functorialise meta-variables")
+  report_errors
+    (fun _ -> coh_successively c l)
+    (lazy ("coherence: " ^ Coh.to_string c))
 
 let rec sub s l =
   match s with
@@ -295,11 +327,7 @@ let coh_all c =
 
 (* Functorialisation a term: exposed function *)
 let tm c t s =
-  try tm c t s
-  with FunctorialiseMeta ->
-    Error.functorialisation
-      ("term: " ^ Unchecked.tm_to_string t)
-      (Printf.sprintf "cannot functorialise meta-variables")
+  report_errors (fun _ -> tm c t s) (lazy ("term: " ^ Unchecked.tm_to_string t))
 
 let ps p l =
   let c = ctx (Unchecked.ps_to_ctx p) l in

test.t/fails/invalidinverse.catt

@@ -0,0 +1,3 @@
+let fail1 (x(f)y(g)z) = I (comp f g)
+
+let fail1 (x(f(a)g)y(h)z) = I (comp [a] [id g])

test.t/fails/invalidnaturality.catt

@@ -1,2 +1,3 @@
 let fail1 (x : *) (f : x -> x) = @comp x [f] f x f
-coh whisk (x(f(a(m)b)g)y(h)z) : comp [a] h -> comp [b] h
+let whisk (x(f(a)g)y(h)z) = comp [a] h
+let fail2 (x(f(a(m)b)g)y(h)z) = @whisk [_] [_] [_] [_] [m] _ [h]

test.t/run.t

@@ -356,17 +356,28 @@
 
   $ catt --keep-going fails/invalidnaturality.catt
   [=^.^=] let fail1 = (@_builtin_comp  x [f] f x f)
-  [=X.X=] The constraints generated for the term: (!1builtin_comp3 (intch_src f f) (builtin_comp2_red [(!1builtin_comp2_red (builtin_assc f f f))]) (intch_tgt x f f)) could not be solved for the following reason:
-  could not unify (builtin_comp2 f f) and f
-  [=^.^=] coh whisk = (_builtin_comp  [a] h) -> (_builtin_comp  [b] h)
-  [=I.I=] successfully defined whisk.
+  [=X.X=] Could not compute the transformation of coherence: builtin_comp2 for the following reason:
+  list of functorialised arguments is not closed
+  [=^.^=] let whisk = (_builtin_comp  [a] h)
+  [=I.I=] successfully defined term (builtin_comp2 [a] h) of type (builtin_comp2 f h) -> (builtin_comp2 g h).
+  [=^.^=] let fail2 = (@whisk  [_] [_] [_] [_] [m] _ [h])
+  [=X.X=] Could not compute the transformation of term: (builtin_comp2 [a] h) for the following reason:
+  higher-dimensional transformations in depth >= 0 are not yet supported
 
   $ catt --keep-going fails/uninferrable.catt
   [=^.^=] let fail1 = (_builtin_comp  (_builtin_id  _) (_builtin_id  _))
   [=X.X=] Incomplete constraints: some of the meta-variable could not be resolved in the following term: (builtin_comp2 (builtin_id _tm1) (builtin_id _tm1))
   [=^.^=] coh fail2 = (_builtin_comp  (_builtin_id  _) _) -> f
   [=X.X=] Incomplete constraints: some of the meta-variable could not be resolved in the following coherence: fail2
 
+  $ catt --keep-going fails/invalidinverse.catt
+  [=^.^=] let fail1 = I((_builtin_comp  f g))
+  [=X.X=] Could not compute the inverse of term: (builtin_comp2 f g) for the following reason:
+  term f is not invertible
+  [=^.^=] let fail1 = I((_builtin_comp  [a] [(_builtin_id  g)]))
+  [=X.X=] Could not compute the inverse of term: (builtin_comp2 [a] [(!1builtin_id g)]) for the following reason:
+  term a is not invertible
+
   $ catt coverage/eckmann-hilton-unoptimized.catt
   [=^.^=] coh comp3 = x1 -> x4
   [=I.I=] successfully defined comp3.