Add error reporting, rewrite GoodHypergraph file

GoodHypergraphCategory was taking a _very_ long time to compile
what's more, it triggered a bug in the compiler relating to how
indices are tracked in lambda declarations. This problem is supposed
to be resolved with #4851
(idris-lang/Idris-dev#4851)

This bypasses the bug and improves compile times as well as add
error reporting on the TDef returned by the API in order to more
easily debug the source of failures when checking as petrinet
description.

Author: andrevidela

src/Cartographer/GoodHypergraphCategory.idr

@@ -33,28 +33,107 @@ getHypergraph _ {g} = g
 
 postulate subsetEq : Subset.getWitness g = Subset.getWitness h -> g = h
 
+---------------------------------
+-- GoodHypergraphCat functions --
+---------------------------------
+
+infixr 4 ~+~>
+
+||| GoodHypergraph signature
+(~+~>) : {s : Type} -> {ai, ao : s -> List o} -> (a , b : List o) -> Type
+(~+~>) a b {s} {ai} {ao} = Subset (Hypergraph s ai ao a b) GoodHypergraph
+
+goodHypergraphCatCompose : {s : Type} -> {ai, ao : s -> List o} -> (a,b,c : List o)
+    -> ((~+~>) {s} {ai} {ao} a b)
+    -> ((~+~>) {s} {ai} {ao} b c)
+    -> ((~+~>) {s} {ai} {ao} a c)
+goodHypergraphCatCompose _ _ _ f g = Element (compose (getWitness f) (getWitness g)) (HComp (getProof f) (getProof g))
+
+goodHypergraphCatComposeProof :  (a21 : List o) ->
+       (b22 : List o) ->
+       (c23 : List o) ->
+       (d : List o) ->
+       (f25 : Subset (Hypergraph sigma arityIn arityOut a21 b22)
+                     GoodHypergraph) ->
+       (g26 : Subset (Hypergraph sigma arityIn arityOut b22 c23)
+                     GoodHypergraph) ->
+       (h : Subset (Hypergraph sigma arityIn arityOut c23 d)
+                   GoodHypergraph) ->
+       Element (compose (getWitness f25)
+                        (compose (getWitness g26) (getWitness h)))
+               (HComp (getProof f25) (HComp (getProof g26) (getProof h))) =
+       Element (compose (compose (getWitness f25) (getWitness g26))
+                        (getWitness h))
+               (HComp (HComp (getProof f25) (getProof g26)) (getProof h))
+goodHypergraphCatComposeProof a b c d (Element f ff) (Element g gg) (Element h hh) =
+  subsetEq (hgAssoc a b c d f g h)
+
 goodHypergraphCat : (sigma : Type) -> (arityIn, arityOut : sigma -> List o) -> Category
 goodHypergraphCat {o} sigma arityIn arityOut = MkCategory
   (List o)
-  (\k, l => Subset (Hypergraph sigma arityIn arityOut k l) GoodHypergraph)
+  ((~+~>) {s=sigma} {ai=arityIn} {ao=arityOut})
   (\n => Element (identity n) (Permutation (permId n)))
-  (\_,_,_,f,g => Element (compose (getWitness f) (getWitness g)) (HComp (getProof f) (getProof g)))
+  goodHypergraphCatCompose
   (\a, b, (Element g gg) => subsetEq (hgLeftId a b g))
   (\a, b, (Element g gg) => subsetEq (hgRightId a b g))
-  (\a, b, c, d, (Element f ff), (Element g gg), (Element h hh) => subsetEq (hgAssoc a b c d f g h))
-
+  goodHypergraphCatComposeProof
 goodSingleton : {s : Type} -> {ai, ao : s -> List o} -> (edge : s) -> mor (goodHypergraphCat s ai ao) (ai edge) (ao edge)
 goodSingleton x = Element (Hypergraph.singleton x) (Singleton x)
 
 goodPermutation : {s : Type} -> {ai, ao : s -> List o} -> Perm k m -> mor (goodHypergraphCat s ai ao) k m
 goodPermutation p = Element (permutation p) (Permutation p)
 
-goodHyperGraphTensor : (s : Type) -> (ai, ao : s -> List o) -> CFunctor (productCategory (goodHypergraphCat s ai ao) (goodHypergraphCat s ai ao)) (goodHypergraphCat s ai ao)
+
+------------------------------------
+-- GoodHyperGraphTensor functions --
+------------------------------------
+
+tensorMor : (List o, List o) -> List o
+tensorMor a = Basics.fst a ++ Basics.snd a
+
+goodHypergraphTensorMor : {s : Type} -> {ai, ao : s -> List o} -> (a : (List o, List o))
+     -> (b : (List o, List o))
+     -> (ProductMorphism (goodHypergraphCat s ai ao)
+                         (goodHypergraphCat s ai ao) a b)
+     -> mor (goodHypergraphCat s ai ao) (tensorMor a) (tensorMor b)
+goodHypergraphTensorMor a b f =
+  Element (add (Subset.getWitness $ pi1 f) (Subset.getWitness $ pi2 f) {k=fst a} {l=fst b} {m=snd a} {n=snd b})
+          (VComp (getProof $ pi1 f) (getProof $ pi2 f))
+
+goodHypergraphTensorCompose : (a, b, c : (List o, List o)) ->
+        (f : ProductMorphism (goodHypergraphCat s ai ao) (goodHypergraphCat s ai ao) a b) ->
+        (g : ProductMorphism (goodHypergraphCat s ai ao) (goodHypergraphCat s ai ao) b c) ->
+        goodHypergraphTensorMor a c
+            (productCompose a b c f g) =
+            goodHypergraphCatCompose
+                (tensorMor a)
+                (tensorMor b)
+                (tensorMor c)
+                (goodHypergraphTensorMor a b f)
+                (goodHypergraphTensorMor b c g)
+goodHypergraphTensorCompose a b c f g =
+  subsetEq (hgPreserveCompose a b c (MkProductMorphism (getWitness $ pi1 f) (getWitness $ pi2 f))
+                                    (MkProductMorphism (getWitness $ pi1 g) (getWitness $ pi2 g)))
+goodHyperGraphTensor : (s : Type) -> (ai, ao : s -> List o) ->
+                       CFunctor (productCategory (goodHypergraphCat s ai ao) (goodHypergraphCat s ai ao))
+                                (goodHypergraphCat s ai ao)
 goodHyperGraphTensor s ai ao = MkCFunctor
-  (\a => fst a ++ snd a)
-  (\a, b, f => Element (add (getWitness $ pi1 f) (getWitness $ pi2 f) {k=fst a} {l=fst b} {m=snd a} {n=snd b}) (VComp (getProof $ pi1 f) (getProof $ pi2 f)))
+  tensorMor
+  goodHypergraphTensorMor
   (\a => subsetEq (hgPreserveId (fst a) (snd a)))
-  (\a, b, c, f, g => subsetEq (hgPreserveCompose a b c (MkProductMorphism (getWitness $ pi1 f) (getWitness $ pi2 f)) (MkProductMorphism (getWitness $ pi1 g) (getWitness $ pi2 g))))
+  goodHypergraphTensorCompose
+
+postulate
+composeGoodHypergraphProof : (a, b, c : List o) ->
+                      (d, e, f : List o) ->
+                      (g : Subset (Hypergraph s ai ao a b) GoodHypergraph) ->
+                      (h : Subset (Hypergraph s ai ao c d) GoodHypergraph) ->
+                      (k : Subset (Hypergraph s ai ao e f) GoodHypergraph) ->
+                      Element (add (getWitness g) (add (getWitness h) (getWitness k)))
+                              (VComp (getProof g) (VComp (getProof h) (getProof k))) =
+                      Element (add (add (getWitness g) (getWitness h)) (getWitness k))
+                              (VComp (VComp (getProof g) (getProof h)) (getProof k))
+composeGoodHypergraphProof fi fo gi go hi ho (Element f ff) (Element g gg) (Element h hh) = ?what -- subsetEq (hgTensorAssociative fi fo gi go hi ho f g h))
 
 goodHypergraphSMC : (sigma : Type) -> (arityIn, arityOut : sigma -> List o) -> StrictMonoidalCategory
 goodHypergraphSMC s ai ao = MkStrictMonoidalCategory
@@ -64,4 +143,4 @@ goodHypergraphSMC s ai ao = MkStrictMonoidalCategory
   (\as => Refl)
   (\as => appendNilRightNeutral as)
   appendAssociative
-  ?proofgoodhypergraph -- (\fi, fo, gi, go, hi, ho, (Element f ff), (Element g gg), (Element h hh) => subsetEq (hgTensorAssociative fi fo gi go hi ho f g h))
+  composeGoodHypergraphProof

src/Cartographer/HypergraphStrictMonoidalCategory.idr

@@ -31,20 +31,21 @@ hgPreserveId {s} {ai} {ao} as bs with (identity {s} {ai} {ao} as)
         `trans` permCompLeftId (permId (as ++ bs)))
       `trans` permCompLeftId (permId (as ++ bs))
 
+postulate
 hgPreserveCompose : {s : Type} -> {ai, ao : s -> List o} -> (a, b, c : (List o, List o))
                  -> (f : ProductMorphism (hypergraphCat s ai ao) (hypergraphCat s ai ao) a b)
                  -> (g : ProductMorphism (hypergraphCat s ai ao) (hypergraphCat s ai ao) b c)
                  -> add (compose (pi1 f) (pi1 g)) (compose (pi2 f) (pi2 g))
                   = compose (add (pi1 f) (pi2 f)) (add (pi1 g) (pi2 g))
-hgPreserveCompose a b c
-  (MkProductMorphism (MkHypergraph pf1 sf1) (MkHypergraph pf2 sf2))
-  (MkProductMorphism (MkHypergraph pg1 sg1) (MkHypergraph pg2 sg2))
-  = hypergraphEq p ?w
-  where
-    p : Perm ((pf1 ++ pg1) ++ (pf2 ++ pg2)) ((pf1 ++ pf2) ++ (pg1 ++ pg2))
-    p = rewriteLeft (sym $ appendAssociative pf1 pg1 (pf2 ++ pg2)) $
-        rewriteRight (sym $ appendAssociative pf1 pf2 (pg1 ++ pg2)) $
-        pf1 `permAddIdL` swapAddIdR pg1 pf2 pg2
+--hgPreserveCompose a b c
+--  (MkProductMorphism (MkHypergraph pf1 sf1) (MkHypergraph pf2 sf2))
+--  (MkProductMorphism (MkHypergraph pg1 sg1) (MkHypergraph pg2 sg2))
+--   = hypergraphEq p ?w
+--   where
+--     p : Perm ((pf1 ++ pg1) ++ (pf2 ++ pg2)) ((pf1 ++ pf2) ++ (pg1 ++ pg2))
+--     p = rewriteLeft (sym $ appendAssociative pf1 pg1 (pf2 ++ pg2)) $
+--         rewriteRight (sym $ appendAssociative pf1 pf2 (pg1 ++ pg2)) $
+--         pf1 `permAddIdL` swapAddIdR pg1 pf2 pg2
 
 hgTensor : (s : Type) -> (ai, ao : s -> List o) -> CFunctor (productCategory (hypergraphCat s ai ao) (hypergraphCat s ai ao)) (hypergraphCat s ai ao)
 hgTensor s ai ao = MkCFunctor

src/GraphCat.idr

@@ -62,7 +62,7 @@ constructNEPath g ((x, y) :: (y',z) :: pt) with (decEq y y')
 validateExec : IdrisType FSMExec -> FSMCheck (cat : Category ** a : obj cat ** b : obj cat ** mor cat a b)
 validateExec (spec, state, path) =
   do -- convert into a graph with `n` being the number of states
-     (m** MkGraph {n} edges) <- maybe (Left InvalidFSM) Right $ mkTGraph $ spec
+     (m** MkGraph {n} edges) <- maybe (Left $ InvalidFSM "Cannot convert to graph") Right $ mkTGraph $ spec
      -- get the inital state as a fin
      st <- maybe (Left InvalidState) Right $ natToFin state m
      -- Convert the edge list into fins

src/JSONFormat.idr

@@ -74,6 +74,6 @@ expectListListEdges : JSON -> Either String (List (List Nat, List Nat))
 expectListListEdges js = expectList js >>= traverse (expectPair expectListNat expectListNat)
 
 public export
-TResult : TDefR 0
+TResult : TDefR 1
 TResult = TSum [T1, TFSMErr]
 

src/Main.idr

@@ -48,35 +48,39 @@ import Language.JSON
 %access public export
 %default total
 
-checkFSM : String -> FSMCheck ()
-checkFSM fileContent = do
-    content <- maybe (Left JSONError) Right (parse fileContent)
-    fsm <- either (const $ Left InvalidFSM) Right (Typedefs.TermParse.deserialiseJSON FSMExec
-      [ (Nat ** expectNat)
-      , (List (Nat, Nat) ** expectListEdges)
-      , (List Nat ** expectListNat)
-      ]
-      content)
-    (cat ** a ** b ** m) <- validateExec fsm
-    let v = lastStep cat a b m
-    pure ()
+mapError : (a -> b) -> Either a c -> Either b c
+mapError f (Left a) = Left (f a)
+mapError _ (Right v) = Right v
+
+-- checkFSM : String -> FSMCheck ()
+-- checkFSM fileContent = do
+--     content <- maybe (Left JSONError) Right (parse fileContent)
+--     fsm <- mapErro (const $ InvalidFSM "could not convert from TDef") (Typedefs.TermParse.deserialiseJSON FSMExec
+--       [ (Nat ** expectNat)
+--       , (List (Nat, Nat) ** expectListEdges)
+--       , (List Nat ** expectListNat)
+--       ]
+--       content)
+--     (cat ** a ** b ** m) <- validateExec fsm
+--     let v = lastStep cat a b m
+--     pure ()
 
 checkPetri : String -> FSMCheck ()
 checkPetri fileContent = do
     content <- maybe (Left JSONError) Right (parse fileContent)
-    petri' <- either (const $ Left InvalidFSM) Right (Typedefs.TermParse.deserialiseJSON TPetriExec
+    petri' <- mapError (const $ InvalidFSM "could not convert from TDef") (Typedefs.TermParse.deserialiseJSON TPetriExec
       [ (Nat ** expectNat)
       , (List (List Nat, List Nat) ** expectListListEdges)
       , (List Nat ** expectListNat)
       ]
       content)
-    petri <- maybe (Left InvalidFSM) Right (convertExec $ petri')
+    petri <- mapError (InvalidFSM) (convertExec $ petri')
     let True = isJust $ composeWithId (Spec petri) (Path petri) (State petri)
-      | Left InvalidFSM
+      | Left InvalidPath
     pure ()
 
 
-toTDef : FSMCheck () -> Ty [] TResult
+toTDef : FSMCheck () -> Ty [String] TResult
 toTDef (Left err) = Right (toTDefErr err)
 toTDef (Right r) = Left r
 
@@ -87,8 +91,8 @@ main = do
       | _ => putStrLn "Usage: fsm-oracle FILE"
     content <-  (readFile filename)
     let asFSMCheck = either (const (Left FSError)) Right content
-    let checkedFSM = asFSMCheck >>= checkFSM
-    printLn (TermWrite.serialiseJSON [] [] TResult (toTDef checkedFSM))
+    let checkedFSM = asFSMCheck >>= checkPetri
+    printLn (TermWrite.serialiseJSON [String] [JString] TResult (toTDef checkedFSM))
 
 <<<<<<< HEAD
 =======

src/Permutations/PermutationsCategory.idr

@@ -23,27 +23,28 @@ permCompRightId {bs} (Ins ab' sw) with (shuffle sw (permId bs)) proof shprf
   | Ins bc' sw' = case insInjective $ trans shprf (shuffleId sw) of
     (Refl, Refl, Refl) => rewrite permCompRightId ab' in Refl
 
+postulate
 shuffleComp : (abb : SwapDown as bs) -> (bc : Perm bs cs) -> (cd : Perm cs ds)
            -> Ins bc' ayc = shuffle abb bc
            -> Ins {ys=ds1} cd' ad1d = shuffle ayc cd
            -> Ins {ys=ds2} bd' ad2d = shuffle abb (permComp bc cd)
            -> (ds1 = ds2, ad1d = ad2d, bd' = permComp bc' cd')
-shuffleComp  HereS       (Ins _ swx)   cd Refl eq2 eq3 with (shuffle swx cd)
-  | Ins bc' sw' with (eq2, eq3)
-    | (Refl, Refl) = (Refl, Refl, Refl)
-shuffleComp {ds} (ThereS aab) (Ins {ys=zs} bz bzc) cd eq1  eq2 eq3 with (shuffle aab bz) proof bcPrf
-  | Ins {ys=xs} ax axz with (shuffle bzc cd)
-    | Ins {ys=us} zu bud with (shuffle aab (permComp bz zu)) proof bdPrf
-      | Ins {ys=ts} at atu with (shuffle axz zu) proof cdPrf
-        | Ins {ys=qs} xq aqu with (shuffleComp aab bz zu bcPrf cdPrf bdPrf)
-          | (r1, r2, r3) with (swComb axz bzc)
-            | SW2 {ys=ws} bxw awc with (eq1)
-              | Refl with (shuffle awc cd)
-                | Ins {ys=vs} wv avd with (eq2)
-                  | Refl with (swComb atu bud)
-                    | SW2 {ys=ss} bts asd with (eq3)
-                      | Refl with (shuffle bxw wv)
-                        | Ins {ys=rs} xr brv = ?pleaseLeaveMeAlone
+--shuffleComp  HereS       (Ins _ swx)   cd Refl eq2 eq3 with (shuffle swx cd)
+--  | Ins bc' sw' with (eq2, eq3)
+--    | (Refl, Refl) = (Refl, Refl, Refl)
+--shuffleComp {ds} (ThereS aab) (Ins {ys=zs} bz bzc) cd eq1  eq2 eq3 with (shuffle aab bz) proof bcPrf
+--  | Ins {ys=xs} ax axz with (shuffle bzc cd)
+--    | Ins {ys=us} zu bud with (shuffle aab (permComp bz zu)) proof bdPrf
+--      | Ins {ys=ts} at atu with (shuffle axz zu) proof cdPrf
+--        | Ins {ys=qs} xq aqu with (shuffleComp aab bz zu bcPrf cdPrf bdPrf)
+--          | (r1, r2, r3) with (swComb axz bzc)
+--            | SW2 {ys=ws} bxw awc with (eq1)
+--              | Refl with (shuffle awc cd)
+--                | Ins {ys=vs} wv avd with (eq2)
+--                  | Refl with (swComb atu bud)
+--                    | SW2 {ys=ss} bts asd with (eq3)
+--                      | Refl with (shuffle bxw wv)
+--                        | Ins {ys=rs} xr brv = ?pleaseLeaveMeAlone
 -- vs = ss
 -- avd = asd
 -- rs = ts