finish up comand line for petrinets

Author: andrevidela

src/Main.idr

@@ -64,13 +64,14 @@ checkFSM fileContent = do
 checkPetri : String -> FSMCheck ()
 checkPetri fileContent = do
     content <- maybe (Left JSONError) Right (parse fileContent)
-    petri <- either (const $ Left InvalidFSM) Right (Typedefs.TermParse.deserialiseJSON TPetriExec
+    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)
+    petri <- maybe (Left InvalidFSM) Right (convertExec $ petri')
+    let True = isJust $ composeWithId (Spec petri) (Path petri) (State petri)
       | Left InvalidFSM
     pure ()
 

src/PetriFormat.idr

@@ -6,18 +6,23 @@ import Typedefs.Names
 import Data.Vect
 import PetriGraph
 
+public export
 TNat : TDefR 2
 TNat = RRef 0
 
+public export
 TEdges : TDefR 2
 TEdges = RRef 1
 
+public export
 TState : TDefR 3
 TState = RRef 2
 
+public export
 TPetriSpec : TDefR 2
 TPetriSpec = TProd [TNat, TEdges]
 
+public export
 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)
@@ -27,6 +32,7 @@ convertSpec (places, edges) =
     convertList p = traverse (\(a, b) => [| MkPair (traverse (\v => natToFin v p) a)
                                                    (traverse (\v => natToFin v p) b) |])
 
+public export
 TTree : TDefR 1
 TTree = TMu
   [ ("Tensor", TProd [TVar 0, TVar 0])
@@ -36,13 +42,25 @@ TTree = TMu
   , ("Mor", TVar 1)
   ]
 
+-- converts from TDef to Tree
 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
 
+
+-- converts from Tree to TDef
+export
+convertTree' : Tree Nat Nat -> Ty [Nat] TTree
+convertTree' (Tensor a b) = (Inn (Left (convertTree' a, convertTree' b)))
+convertTree' (Sequence a b) = (Inn (Right (Left (convertTree' a, convertTree' b))))
+convertTree' (Sym a b) = (Inn (Right (Right (Left (a, b)))))
+convertTree' (Id x) = (Inn (Right (Right (Right (Left x)))))
+convertTree' (Mor x) = (Inn (Right (Right (Right (Right x)))))
+
+public export
 convertState : (spec : PetriSpec k) -> List Nat -> Maybe (PetriState spec)
 convertState spec = traverse (\s => natToFin s (Places spec))
 
@@ -51,8 +69,9 @@ 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
+dropContext tdef = really_believe_me tdef
 
-export
+public 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)