add typedefs for spec and state

Author: andrevidela

src/JSONFormat.idr

@@ -36,25 +36,25 @@ listPairToJSON xs = JArray $ map
   (\(a, b) => JObject [("input", JNumber $ cast a), ("output", JNumber $ cast b)]) xs
 
 export
-expectNat : JSON -> Maybe Nat
-expectNat (JNumber n) = if n < 0 then Nothing
-                                 else Just $ Prelude.toNat {a=Int} $ cast n
-expectNat _ = Nothing
+expectNat : JSON -> Either String Nat
+expectNat (JNumber n) = if n < 0 then Left "Expected Nat"
+                                 else pure $ Prelude.toNat {a=Int} $ cast n
+expectNat _ = Left "Expected Nat"
 
-expectEdges : JSON -> Maybe (Nat, Nat)
+expectEdges : JSON -> Either String (Nat, Nat)
 expectEdges (JObject [("input", a),("output", b)])= [| MkPair (expectNat a) (expectNat b) |]
-expectEdges _ = Nothing
+expectEdges _ = Left "expected list of edges"
 
-expectList : JSON -> Maybe (List JSON)
-expectList (JArray ls) = Just ls
-expectList _ = Nothing
+expectList : JSON -> Either String (List JSON)
+expectList (JArray ls) = pure ls
+expectList _ = Left "expected List"
 
 export
-expectListNat : JSON -> Maybe (List Nat)
+expectListNat : JSON -> Either String (List Nat)
 expectListNat js = expectList js >>= traverse expectNat
 
 export
-expectListEdges : JSON -> Maybe (List (Nat, Nat))
+expectListEdges : JSON -> Either String (List (Nat, Nat))
 expectListEdges js = expectList js >>= traverse expectEdges
 
 public export

src/Main.idr

@@ -49,7 +49,7 @@ import Language.JSON
 checkFSM : String -> FSMCheck ()
 checkFSM fileContent = do
     content <- maybe (Left JSONError) Right (parse fileContent)
-    fsm <- maybe (Left InvalidFSM) Right (Typedefs.TermParse.deserializeJSON FSMExec
+    fsm <- either (const $ Left InvalidFSM) Right (Typedefs.TermParse.deserialiseJSON FSMExec
       [ (Nat ** expectNat)
       , (List (Nat, Nat) ** expectListEdges)
       , (List Nat ** expectListNat)
@@ -72,6 +72,6 @@ main = do
     content <-  (readFile filename)
     let asFSMCheck = either (const (Left FSError)) Right content
     let checkedFSM = asFSMCheck >>= checkFSM
-    printLn (TermWrite.serializeJSON [] [] TResult (toTDef checkedFSM))
+    printLn (TermWrite.serialiseJSON [] [] TResult (toTDef checkedFSM))
 
 

src/PetriFormat.idr

@@ -0,0 +1,43 @@
+
+module PetriFormat
+
+import Typedefs.Typedefs
+import Typedefs.Names
+import Data.Vect
+import PetriGraph
+
+TNat : TDefR 2
+TNat = RRef 0
+
+TEdges : TDefR 2
+TEdges = RRef 1
+
+
+TPetriSpec : TDefR 2
+TPetriSpec = TProd [TNat, TEdges]
+
+convertSpec : Ty [Nat, List (List Nat, List Nat)] TPetriSpec -> Maybe (n ** PetriSpec n)
+convertSpec (places, edges) =
+  MkDPair (length edges) . MkPetriSpec places <$> convertList places (fromList edges)
+  where
+    convertList : (p : Nat) ->  (Vect n (List Nat, List Nat))
+               -> Maybe (Vect n (List (Fin p), List (Fin p)))
+    convertList p = traverse (\(a, b) => [| MkPair (traverse (\v => natToFin v p) a)
+                                                   (traverse (\v => natToFin v p) b) |])
+
+TTree : TDefR 1
+TTree = TMu
+  [ ("Tensor", TProd [TVar 0, TVar 0])
+  , ("Sequence", TProd [TVar 0, TVar 0])
+  , ("Sym", TProd [TVar 1, TVar 1])
+  , ("Id", TVar 1)
+  , ("Mor", TVar 1)
+  ]
+
+convertTree : Ty [Nat] TTree -> (Tree Nat Nat)
+convertTree (Inn (Left (a, b))) = Tensor (convertTree a) (convertTree b)
+convertTree (Inn (Right (Left (a, b)))) = Sequence (convertTree a) (convertTree b)
+convertTree (Inn (Right (Right (Left (a, b))))) = Sym a b
+convertTree (Inn (Right (Right (Right (Left i))))) = Id i
+convertTree (Inn (Right (Right (Right (Right m))))) = Mor m
+

src/PetriGraph.idr

@@ -48,14 +48,13 @@ PetriPath = TMu [ ("Tensor", TProd [TVar 0, TVar 0])
 
 -}
 
+public export
 record PetriSpec (k : Nat) where
   constructor MkPetriSpec
   Places : Nat
   Edges : Vect k (List (Fin Places), List (Fin Places))
 
-PetriState : Type
-PetriState = List Nat
-
+public export
 data Tree o m = Tensor (Tree o m) (Tree o m)
               | Sequence (Tree o m) (Tree o m)
               | Sym o o
@@ -81,6 +80,14 @@ Codomain m (Mor i) = snd $ index i m
 PetriPath : Nat -> Nat -> Type
 PetriPath places k = Tree (Fin places) (Fin k)
 
+checkTree : (spec : PetriSpec k) -> Tree Nat Nat -> Maybe (PetriPath (Places spec) k)
+checkTree spec (Tensor x y) = [| Tensor (checkTree spec x) (checkTree spec y) |]
+checkTree spec (Sequence x y) = [| Sequence (checkTree spec x) (checkTree spec y) |]
+checkTree spec (Sym x y) = [| Sym (natToFin x (Places spec)) (natToFin y (Places spec)) |]
+checkTree spec (Id x) = Id <$> natToFin x (Places spec)
+checkTree spec (Mor x) {k} = Mor <$> natToFin x k
+
+
 goodPetriSMC : (spec : PetriSpec k) -> StrictMonoidalCategory
 goodPetriSMC spec = goodHypergraphSMC (Fin k)
                                       (\m => fst $ index m (Edges spec))
@@ -115,3 +122,15 @@ goodMapping s (Sequence x y) {k} = do
 goodMapping s (Id x) = Just $ identity (cat (goodPetriSMC s)) [x]
 goodMapping s (Sym a b) = Just $ goodPermutation (swap [a] [b])
 goodMapping s (Mor x) = Just $ goodSingleton x
+
+PetriState : PetriSpec k -> Type
+PetriState spec = List (Fin (Places spec))
+
+composeWithId : (spec : PetriSpec k) -> (path : PetriPath (Places spec) k)
+             -> (state : PetriState spec)
+             -> Maybe (mor (cat (goodPetriSMC spec))
+                           (state)
+                           (Codomain (Edges spec) path))
+composeWithId spec path state with (decEq state (Domain (Edges spec) path))
+  composeWithId spec path state | Yes prf = rewrite prf in goodMapping spec path
+  composeWithId spec path state | No _ = Nothing