Depth setting.

examples/Makefile

@@ -1,2 +1,2 @@
 test:
-	@dune runtest
+	@dune runtest -f

src/pasting.ml

@@ -40,6 +40,17 @@ let check_ccc a =
     | Obj -> failure c.pos "cannot prove identities between objects"
     | _ -> assert false
   in
+  let () =
+    let rec depth a =
+      match a.desc with
+      | Var _ -> 0
+      | Hom (a, _) -> 1 + depth a
+      | _ -> assert false
+    in
+    match !Setting.depth with
+    | Some d -> if depth a > d then failure a.pos "pasting has depth %d but we are limited to %d" (depth a) d
+    | None -> ()
+  in
   prove [] [] a
 
 (** Whether a type in a context is a pasting scheme. *)
@@ -151,6 +162,10 @@ let check ~pos l a =
     in
     List.iter check_ccc aa
 
+  | `Plain ->
+    let l = List.map snd l in
+    assert (List.mem a l)
+
 (*
   | `Monoid ->
     let rec get_prod a =

src/setting.ml

@@ -4,21 +4,33 @@ open Extlib
 open Common
 
 (** Mode for checking pasting schemes. *)
-type mode = [ `Monoid | `Category | `Monoidal | `Symmetric_monoidal | `Symmetric_monoidal_closed | `Cartesian_closed ]
+type mode = [
+  | `Plain
+  | `Monoid
+  | `Category
+  | `Monoidal
+  | `Symmetric_monoidal
+  | `Symmetric_monoidal_closed
+  | `Cartesian_closed
+]
 
 let mode = ref (`Cartesian_closed : mode)
 
+(** Maximal depth for pasting schemes. *)
+let depth = ref None
+
 let parse s =
   let k, v = String.split_on_first_char ':' s in
   let k = String.trim k in
   let v = String.trim v in
   try
-    mode :=
-      match k with
-      | "mode" ->
+    match k with
+    | "mode" ->
+      message "setting mode to %s" v;
+      mode :=
         (
-          message "setting mode to %s" v;
           match v with
+          | "plain" -> `Plain
           | "monoid" -> `Monoid
           | "category" -> `Category
           | "cartesian closed" | "ccc" -> `Cartesian_closed
@@ -27,6 +39,10 @@ let parse s =
           | "monoidal" -> `Monoidal
           | m -> warning "Unknown mode: %s" m; raise Exit
         )
-      | k -> warning "Unknown setting: %s" k; raise Exit
+    | "depth" ->
+      let n = int_of_string v in
+      message "setting depth to %d" n;
+      depth := Some n
+    | k -> warning "Unknown setting: %s" k; raise Exit
   with
   | Exit -> ()