add type definitions for petrinets

Author: andrevidela

src/JSONFormat.idr

@@ -31,6 +31,14 @@ import TGraph
 
 import Typedefs.Typedefs
 
+public export
+ParseError : Type -> Type
+ParseError = Either String
+
+public export
+JSONParser : Type -> Type
+JSONParser t = JSON -> ParseError t
+
 listPairToJSON : List (Nat, Nat) -> JSON
 listPairToJSON xs = JArray $ map
   (\(a, b) => JObject [("input", JNumber $ cast a), ("output", JNumber $ cast b)]) xs
@@ -41,7 +49,7 @@ expectNat (JNumber n) = if n < 0 then Left "Expected Nat"
                                  else pure $ Prelude.toNat {a=Int} $ cast n
 expectNat _ = Left "Expected Nat"
 
-expectEdges : JSON -> Either String (Nat, Nat)
+expectEdges : JSONParser (Nat, Nat)
 expectEdges (JObject [("input", a),("output", b)])= [| MkPair (expectNat a) (expectNat b) |]
 expectEdges _ = Left "expected list of edges"
 
@@ -54,9 +62,17 @@ expectListNat : JSON -> Either String (List Nat)
 expectListNat js = expectList js >>= traverse expectNat
 
 export
-expectListEdges : JSON -> Either String (List (Nat, Nat))
+expectListEdges : JSONParser (List (Nat, Nat))
 expectListEdges js = expectList js >>= traverse expectEdges
 
+expectPair : (JSONParser a) -> (JSONParser b) -> JSONParser (a, b)
+expectPair pa pb (JObject [("_0", a), ("_1", b)]) = [| MkPair (pa a) (pb b) |]
+expectPair pa pb _ = Left "Expected Pair"
+
+export
+expectListListEdges : JSON -> Either String (List (List Nat, List Nat))
+expectListListEdges js = expectList js >>= traverse (expectPair expectListNat expectListNat)
+
 public export
 TResult : TDefR 0
 TResult = TSum [T1, TFSMErr]

src/Main.idr

@@ -36,6 +36,8 @@ import Typedefs.TermParse
 import Typedefs.TermWrite
 
 import TGraph
+import PetriGraph
+import PetriFormat
 import GraphCat
 
 -- base
@@ -59,6 +61,19 @@ checkFSM fileContent = do
     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
+      [ (Nat ** expectNat)
+      , (List (List Nat, List Nat) ** expectListListEdges)
+      , (List Nat ** expectListNat)
+      ]
+      content)
+    let True = isJust $ composeWithId (Spec petri) (Path petri) (State Petri)
+      | Left InvalidFSM
+    pure ()
+
 
 toTDef : FSMCheck () -> Ty [] TResult
 toTDef (Left err) = Right (toTDefErr err)
@@ -74,4 +89,14 @@ main = do
     let checkedFSM = asFSMCheck >>= checkFSM
     printLn (TermWrite.serialiseJSON [] [] TResult (toTDef checkedFSM))
 
+-- partial
+-- main : IO ()
+-- main = do
+--     [_,filename] <- getArgs
+--       | _ => 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))
+--
 

src/PetriFormat.idr

@@ -12,6 +12,8 @@ TNat = RRef 0
 TEdges : TDefR 2
 TEdges = RRef 1
 
+TState : TDefR 3
+TState = RRef 2
 
 TPetriSpec : TDefR 2
 TPetriSpec = TProd [TNat, TEdges]
@@ -41,3 +43,19 @@ 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
 
+convertState : (spec : PetriSpec k) -> List Nat -> Maybe (PetriState spec)
+convertState spec = traverse (\s => natToFin s (Places spec))
+
+public export
+TPetriExec : TDefR 3
+TPetriExec = TProd [TProd [RRef 0 , RRef 1], RRef 2, weakenTDef TTree 3 (LTESucc LTEZero)]
+
+dropContext : Ty [Nat, a, b] (weakenTDef TTree 3 (LTESucc LTEZero)) -> Ty [Nat] TTree
+
+export
+convertExec : Ty [Nat, List (List Nat, List Nat), List Nat] TPetriExec -> Maybe PetriExec
+convertExec ((a, b), c, d) = do (k ** spec) <- convertSpec (a , b)
+                                path <- checkTree spec (convertTree $ dropContext d)
+                                state <- convertState spec c
+                                pure $ MkPetriExec spec path state
+

src/PetriGraph.idr

@@ -13,40 +13,6 @@ import MonoidalCategory.StrictMonoidalCategory
 
 
 %default total
-{-
-StringDiag := {
-  tensor := {
-    tensor := {
-      f
-      g
-    }
-    sequence := {
-      h
-      identity A
-      }
-    }
-  }
-}
-
-data Tree o m = Tensor Tree Tree | Sequence Tree Tree | Id o | Mor m
--}
--- PetriSpec
--- Vertex: Nat, Edges : List ((List Nat), (List Nat))
-{-
-PetriVertex : TDefR 0
-PetriVertex = TProd [TList Nat, TList (TList Nat, TList Nat)]
-
-PetriState : TDefR 0
-PetriState = TList `ap` TNat
-
-PetriPath : TDefR 2
-PetriPath = TMu [ ("Tensor", TProd [TVar 0, TVar 0])
-                , ("Sequence", TProd [TVar 0, TVar 0])
-                , ("Id", TVar 1)
-                , ("Mor", TVar 2)
-                ]
-
--}
 
 public export
 record PetriSpec (k : Nat) where
@@ -61,25 +27,39 @@ data Tree o m = Tensor (Tree o m) (Tree o m)
               | Id o
               | Mor m
 
+public export
+PetriState : PetriSpec k -> Type
+PetriState spec = List (Fin (Places spec))
+
+public export
+PetriPath : Nat -> Nat -> Type
+PetriPath places k = Tree (Fin places) (Fin k)
+
+public export
+record PetriExec where
+  constructor MkPetriExec
+  Spec : PetriSpec k
+  Path : PetriPath (Places Spec) k
+  State : PetriState Spec
+
+
+public export
 Domain : (morphisms : Vect k (List a, List a)) -> Tree a (Fin k) -> List a
 Domain m (Tensor l r) = (Domain m l) ++ (Domain m r)
 Domain m (Sequence l r) = Domain m l
 Domain m (Id o) = pure o
 Domain m (Sym l r) = [l, r]
 Domain m (Mor i) = fst $ index i m
 
-
+public export
 Codomain : (morphisms : Vect k (List a, List a)) -> Tree a (Fin k) -> List a
 Codomain m (Tensor l r) = Codomain m l ++ Codomain m r
 Codomain m (Sequence l r) = Codomain m r
 Codomain m (Id o) = pure o
 Codomain m (Sym l r) = [r, l]
 Codomain m (Mor i) = snd $ index i m
 
-
-PetriPath : Nat -> Nat -> Type
-PetriPath places k = Tree (Fin places) (Fin k)
-
+export
 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) |]
@@ -88,6 +68,7 @@ checkTree spec (Id x) = Id <$> natToFin x (Places spec)
 checkTree spec (Mor x) {k} = Mor <$> natToFin x k
 
 
+public export
 goodPetriSMC : (spec : PetriSpec k) -> StrictMonoidalCategory
 goodPetriSMC spec = goodHypergraphSMC (Fin k)
                                       (\m => fst $ index m (Edges spec))
@@ -123,9 +104,7 @@ 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))
-
+export
 composeWithId : (spec : PetriSpec k) -> (path : PetriPath (Places spec) k)
              -> (state : PetriState spec)
              -> Maybe (mor (cat (goodPetriSMC spec))