search

statebox / idris-stbx-core

Category theoretic semantics of glued open Petri nets in Idris
https://statebox.org/
1 stars 1 forks source link

Typedefify the FSM version of core #53

Open clayrat opened 4 years ago

clayrat commented 4 years ago

What: We want to build and document a very simple version of typed core that accepts TDefs as inputs, describing a FSM spec and a path, and returns a TDef as output, describing the codomain of the path. Why: We have three cores atm. A ReasonML one, an Idris one and a PureScript one. This project will allow to replace the current firing function in the other cores with its idris formally verified version. How: We have to:

Hook up TDefs and Typed core
Translate the FSM input, that now is given in a txt file, into a Tdef.
    The Tdef format should be:
        Input: (FSM spec, state, path)
In the core, use the FSM spec to build a graph and the free category on it.
Evaluate: id_state;path
Return: codomain of id_state;path
    Output format should be a tdef containing the codomain of path or a typechecking error.
clayrat commented 4 years ago

Working in https://github.com/statebox/idris-stbx-core/tree/fsm-oracle branch