Add support for latest Typedefs API

André Videla · André Videla · commit b89435c37338 · 2020-06-23T18:58:50.000+01:00
diff --git a/elba.lock b/elba.lock
@@ -7,7 +7,7 @@ id = 'statebox/idris-ct@git+https://github.com/statebox/idris-ct#fbc7f633e0d86bf
 version = '0.1.0'
 
 [[packages.dependencies]]
-id = 'typedefs/typedefs@git+https://github.com/typedefs/typedefs#a0ce68a1e467ec845917cb1e1411250cfb89b881'
+id = 'typedefs/typedefs@git+https://github.com/typedefs/typedefs#17eea0cb3ef7b4ae7ec3f0d2e89d2ea1b8635250'
 version = '0.1.0'
 
 [[packages]]
@@ -16,7 +16,7 @@ version = '0.1.0'
 dependencies = []
 
 [[packages]]
-id = 'typedefs/typedefs@git+https://github.com/typedefs/typedefs#a0ce68a1e467ec845917cb1e1411250cfb89b881'
+id = 'typedefs/typedefs@git+https://github.com/typedefs/typedefs#17eea0cb3ef7b4ae7ec3f0d2e89d2ea1b8635250'
 version = '0.1.0'
 
 [[packages.dependencies]]
diff --git a/elba.toml b/elba.toml
@@ -4,8 +4,8 @@ version = "0.1.0"
 authors = []
 
 [dependencies]
-"typedefs/typedefs" = { git = "https://github.com/typedefs/typedefs" , tag="a0ce68a1e467ec845917cb1e1411250cfb89b881"}
-"statebox/idris-ct" = { git = "https://github.com/statebox/idris-ct" , tag="master"}
+"typedefs/typedefs" = { git = "https://github.com/typedefs/typedefs" , tag="17eea0cb3ef7b4ae7ec3f0d2e89d2ea1b8635250"}
+"statebox/idris-ct" = { git = "https://github.com/statebox/idris-ct" , tag="416ad13ded92a88dc93761d0125d14061ed6140e"}
 
 [[targets.bin]]
 path = "src"
diff --git a/src/JSONFormat.idr b/src/JSONFormat.idr
@@ -31,45 +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
-
 export
-expectNat : JSONParser Nat
+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 : JSONParser (Nat, Nat)
-expectEdges (JObject [("input", a),("output", b)])= [| MkPair (expectNat a) (expectNat b) |]
-expectEdges _ = Left "Expected List of edges"
-
-expectList : JSONParser (List JSON)
-expectList (JArray ls) = pure ls
-expectList _ = Left "Expected List"
-
-export
-expectListNat : JSONParser (List Nat)
-expectListNat js = expectList js >>= traverse expectNat
-
-export
-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 1
+TResult : TDefR 0
 TResult = TSum [T1, TFSMErr]
 
diff --git a/src/Main.idr b/src/Main.idr
@@ -34,6 +34,8 @@ import Discrete.DiscreteCategory
 import Typedefs.Typedefs
 import Typedefs.TermParse
 import Typedefs.TermWrite
+import Typedefs.Idris
+import Typedefs.Library
 
 -- FSM-Oracle
 import TGraph
@@ -52,30 +54,28 @@ import Language.JSON
 
 checkFSM : JSON -> FSMCheck ()
 checkFSM content = do
-    fsm <- mapLeft InvalidFSM (Typedefs.TermParse.deserialiseJSON FSMExec
-      [ (Nat ** expectNat)
-      , (List (Nat, Nat) ** expectListEdges)
-      , (List Nat ** expectListNat)
-      ]
-      content)
+    fsm <- mapLeft InvalidFSM (Typedefs.TermParse.deserialise
+                              StandardParsers
+                              []
+                              FSMExec
+                              content)
     (cat ** a ** b ** m) <- validateExec fsm
     let v = lastStep cat a b m
     pure ()
 
 checkPetri : JSON -> FSMCheck ()
 checkPetri content = do
-    petri' <- mapLeft InvalidFSM (Typedefs.TermParse.deserialiseJSON TPetriExec
-      [ (Nat ** expectNat)
-      , (List (List Nat, List Nat) ** expectListListEdges)
-      , (List Nat ** expectListNat)
-      ]
-      content)
+    petri' <- mapLeft InvalidFSM (Typedefs.TermParse.deserialise
+                                 StandardParsers
+                                 [liftParse expectNat]
+                                 TPetriExec
+                                 content)
     petri <- mapLeft InvalidFSM (convertExec $ petri')
     let True = isJust $ composeWithId (Spec petri) (Path petri) (State petri)
       | Left InvalidPath
     pure ()
 
-toTDef : FSMCheck () -> Ty [String] TResult
+toTDef : FSMCheck () -> Ty' StandardIdris [] TResult
 toTDef (Left err) = Right (toTDefErr err)
 toTDef (Right r) = Left r
 
@@ -85,7 +85,7 @@ parseMode : String -> Maybe OracleMode
 parseMode "-f" = Just FSM
 parseMode "--fsm" = Just FSM
 parseMode "-p" = Just Petri
-parseMode "-petri" = Just Petri
+parseMode "--petri" = Just Petri
 parseMode _ = Nothing
 
 printHelp : IO ()
@@ -106,5 +106,5 @@ main = do
     let result = do fileContent <- mapLeft (const FSError) content
                     jsonContent <- maybeToEither JSONError (parse fileContent)
                     (pickChecker pmode) jsonContent
-    printLn (TermWrite.serialiseJSON [String] [JString] TResult (toTDef result))
+    printLn (TermWrite.serialise StandardContext [] TResult (toTDef result))
 
diff --git a/src/PetriFormat.idr b/src/PetriFormat.idr
@@ -2,30 +2,33 @@
 module PetriFormat
 
 import Typedefs.Typedefs
+import Typedefs.Library
+import Typedefs.Idris
 import Typedefs.Names
 import Data.Vect
 import PetriGraph
 
 public export
-TNat : TDefR 2
-TNat = RRef 0
+App : TDef' n b -> Vect n (TDef' m b) -> TDef' m b
+App td args = TApp (TName "" td) args
 
 public export
-TEdges : TDefR 2
-TEdges = RRef 1
+TEdges : TDefR 1
+TEdges = App TList [TProd [TList,  TList]]
 
 public export
-TState : TDefR 3
-TState = RRef 2
+TState : TDefR 1
+TState = TList
 
 public export
-TPetriSpec : TDefR 2
-TPetriSpec = TProd [TNat, TEdges]
+TPetriSpec : TDefR 1
+TPetriSpec = TProd [TNat1, TEdges]
 
 public export
-convertSpec : Ty [Nat, List (List Nat, List Nat)] TPetriSpec -> Maybe (n ** PetriSpec n)
+convertSpec : Ty' StandardIdris [Nat] TPetriSpec -> Maybe (n ** PetriSpec n)
 convertSpec (places, edges) =
-  MkDPair (length edges) . MkPetriSpec places <$> convertList places (fromList 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)))
@@ -43,14 +46,13 @@ TTree = TMu
   ]
 
 -- converts from TDef to Tree
-convertTree : Ty [Nat] TTree -> (Tree Nat Nat)
+convertTree : Ty' StandardIdris [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
@@ -60,31 +62,22 @@ 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)))))
 
-example : Tree Nat Nat
-example = Id Z
-
-export
-exampleTDef : Ty [Nat] TTree
-exampleTDef = convertTree' example
-
 public export
 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)
+TPetriExec : TDefR 1
+TPetriExec = TProd [ TPetriSpec -- spec
+                   , TState     -- initial state
+                                -- /!\ the type argument is shared between Tree and List
+                   , TTree      -- execution
                    ]
 
-dropContext : Ty [Nat, a, b] (weakenTDef TTree 3 (LTESucc LTEZero)) -> Ty [Nat] TTree
-dropContext tdef = really_believe_me tdef
-
 public export
-convertExec : Ty [Nat, List (List Nat, List Nat), List Nat] TPetriExec -> Either String PetriExec
+convertExec : Ty' StandardIdris [Nat] TPetriExec -> Either String PetriExec
 convertExec ((a, b), c, d) = do (k ** spec) <-  maybeToEither "indices are wrong" $ convertSpec (a , b)
-                                path <- maybeToEither "illegal tree" $ checkTree spec (convertTree $ dropContext d)
+                                path <- maybeToEither "illegal tree" $ checkTree spec (convertTree d)
                                 state <- maybeToEither  "Illegal states" $ convertState spec c
                                 pure $ MkPetriExec spec path state
 
diff --git a/src/TGraph.idr b/src/TGraph.idr
@@ -32,45 +32,41 @@ import Graph.Graph
 -- typedefs
 import Typedefs.Names
 import Typedefs.Typedefs
+import Typedefs.Idris
+import Typedefs.Library
 
 %access public export
 %default total
 
--- Base definitions
-
--- Defines naturals
-TNat : TDefR 3
-TNat = RRef 0
-
 -- Graph definitions
 
 ||| The type definition for vertices in the graph is jsut
 ||| A natural enumerating the vertexes. e.g. 5 means
 ||| That there are 5 vertexes, denoted 0,1,2,3,4
-FSMVertex : TDefR 3
+FSMVertex : TDefR 0
 FSMVertex = TNat
 
 ||| The type definition for edges in the graph is just a couple
 ||| of vertexes defining the edge source and target
-FSMEdges : TDefR 3
-FSMEdges = RRef 1
+FSMEdges : TDefR 0
+FSMEdges = TApp (TName "" TList) [TProd [TNat, TNat]]
 
 ||| A Finite State Machine is defined by its vertices and a list of edges
 ||| The definition might not be valid if edges endpoints are out of range
-FSMSpec : TDefR 3
+FSMSpec : TDefR 0
 FSMSpec = TProd [FSMVertex, FSMEdges]
 
 ||| A state is a vertex in the graph (might be out of range)
-FSMState : TDefR 3
+FSMState : TDefR 0
 FSMState = FSMVertex
 
 ||| A path is a list of edges (might not be valid)
-FSMPath : TDefR 3
-FSMPath =  RRef 2-- TList `ap` [FSMEdge]
+FSMPath : TDefR 0
+FSMPath =  TApp (TName "" TList) [TNat]
 
 ||| An execution is a FSM, a state representing an inital edge and a path from that edge.
 ||| The execution might not be valid.
-FSMExec : TDefR 3
+FSMExec : TDefR 0
 FSMExec = TProd [FSMSpec, FSMState, FSMPath]
 
 ||| Errors related to checking if a FSM description is valid
@@ -86,15 +82,15 @@ data FSMError =
   ||| Error when reading the file
   FSError
 
-TFSMErr : TDefR 1
-TFSMErr = TMu [("InvalidFSM", RRef 1),
-               ("InvalidState", T1),
-               ("InvalidPath", T1),
-               ("JSONError", T1),
-               ("FSError", T1)
+TFSMErr : TDefR 0
+TFSMErr = TMu [("InvalidFSM", TString1)
+              ,("InvalidState", T1)
+              ,("InvalidPath", T1)
+              ,("JSONError", T1)
+              ,("FSError", T1)
               ]
 
-toTDefErr : FSMError -> Ty [String] TFSMErr
+toTDefErr : FSMError -> Ty' StandardIdris [] TFSMErr
 toTDefErr (InvalidFSM s) = Inn (Left s)
 toTDefErr InvalidState   = Inn (Right (Left ()))
 toTDefErr InvalidPath    = Inn (Right (Right (Left ())))
@@ -108,8 +104,8 @@ Show FSMError where
   show JSONError    = "JSON parsing error"
   show FSError      = "Filesystem error"
 
-IdrisType : TDefR 3 -> Type
-IdrisType = Ty [Nat, List (Nat, Nat), List Nat]
+IdrisType : TDefR 0 -> Type
+IdrisType = Ty' StandardIdris []
 
 ||| Monad to check errors when compiling FSMs
 FSMCheck : Type -> Type
