Skip to content

Commit

Permalink
count morphisms
Browse files Browse the repository at this point in the history
  • Loading branch information
riaqn committed Mar 19, 2024
1 parent 284b012 commit 1e25e06
Showing 1 changed file with 14 additions and 5 deletions.
19 changes: 14 additions & 5 deletions ocaml/typing/mode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -848,13 +848,14 @@ module Lattices_mono = struct
| Comonadic_with_locality -> Locality.max, unique_to_linear uniqueness
| Comonadic_with_regionality -> Regionality.max, unique_to_linear uniqueness

let rec apply : type a b d. b obj -> (a, b, d) morph -> a -> b =
fun dst f a ->
let rec apply' : type a b d. int ref -> b obj -> (a, b, d) morph -> a -> b =
fun cnt dst f a ->
cnt := !cnt + 1;
match f with
| Compose (f, g) ->
let mid = src dst f in
let g' = apply mid g in
let f' = apply dst f in
let g' = apply' cnt mid g in
let f' = apply' cnt dst f in
f' (g' a)
| Id -> a
| Proj (_, ax) -> proj ax a
Expand All @@ -875,7 +876,15 @@ module Lattices_mono = struct
| Map_comonadic f ->
let dst0 = proj_obj Areality dst in
let a0, a1 = a in
apply dst0 f a0, a1
apply' cnt dst0 f a0, a1

let apply : type a b d. b obj -> (a, b, d) morph -> a -> b =
fun dst f a ->
let cnt = ref 0 in
let b = apply' cnt dst f a in
if !cnt > 8
then Misc.fatal_errorf "Morphism chain too long: %a" (print_morph dst) f
else b

(** Compose m0 after m1. Returns [Some f] if the composition can be
represented by [f] instead of [Compose m0 m1]. [None] otherwise. *)
Expand Down

0 comments on commit 1e25e06

Please sign in to comment.