{-# LANGUAGE OverloadedStrings, LambdaCase, DeriveGeneric #-}
{-# LANGUAGE RecordWildCards, DuplicateRecordFields #-}

import Language.EFLINT.Spec hiding (Value(..))
import Language.EFLINT.State
import Language.EFLINT.Util
import Language.EFLINT.Options
import Language.EFLINT.StaticEval
import Language.EFLINT.Parse
import Language.EFLINT.Print (ppProgram)
import Language.EFLINT.Explorer hiding (Instruction(Revert), Response)
import Language.EFLINT.Interpreter
import Language.EFLINT.JSON(decode_json_file)
import qualified Language.EFLINT.Explorer as Explorer

import qualified Language.Explorer.Pure as EI

import Control.Monad
import Control.Applicative

import Data.Function (on)
import Data.Text (unpack)
import Text.Read (readMaybe)
import Data.List (isSuffixOf, sortBy, (\\))
import qualified Data.Set as S
import qualified Data.Map as M

import System.IO (hGetLine, hPutStrLn, hClose, IOMode(ReadWriteMode))
import System.IO.Error
import System.Environment (getArgs)
import System.Directory
import System.FilePath
import Network.Socket
import qualified Data.ByteString.Lazy.Char8 (pack,unpack)

import GHC.Generics
import Data.Aeson hiding (String, Value(..),Options(..))
import qualified Data.Aeson as JSON

-- determines which variant of execution graph to use
init_explorer = init_tree_explorer

main :: IO ()
main = do
  args <- getArgs
  cdir <- getCurrentDirectory
  case args of
    (f:p:opts) | ".eflint" `isSuffixOf` f, Just port_nr <- readMaybe p ->  do
                  fcont <- readFile f
                  opts' <- run_options (["-i",takeDirectory f,"-i",cdir] ++ opts)
                  case parse_component syn_directives_phrases fcont of
                    Left err1 -> case parse_flint fcont of
                      Left err2 -> do  putStrLn "could not parse flint phrases:\n" >> putStrLn err1
                                       putStrLn "could not parse flint spec:\n" >> putStrLn err2
                      Right (s, r, i, _) -> init_server opts' port_nr s r i
                    Right ps -> init_with_phrases opts' port_nr ps
    (p:opts)   | Just port_nr <- readMaybe p -> do
      opts <- run_options (["-i",cdir] ++ opts)
      init_with_phrases opts port_nr []
    _ -> putStrLn "please provide: <NAME>.eflint <PORT> <OPTIONS>"

init_with_phrases :: Options -> PortNumber -> [Either Directive Phrase] -> IO ()
init_with_phrases opts port_nr ps = do
  let explorer = init_explorer Nothing 
  run_directives_phrases opts ps (start_server opts port_nr) explorer
  return ()

type Cont a = Explorer -> IO a

run_directives_phrases :: Options -> [Either Directive Phrase] -> Cont a -> Cont a
run_directives_phrases opts [] cont exp = cont exp
run_directives_phrases opts (edp:ps) cont exp = let (_,_,(_,ctx)) = get_last_edge exp (EI.currRef exp) in
  case edp of
   Left d  -> run_directive opts d (run_directives_phrases opts ps cont) exp
   Right p -> run_phrase opts p (run_directives_phrases opts ps cont) exp

run_phrase :: Options -> Phrase -> Cont a -> Cont a
run_phrase opts phrase cont exp = case run_ exp (Execute (convert_programs [phrase]) emptyInput) of
  ResultTrans exp _ _ _  -> cont exp
  Path _                 -> putStrLn "Unexpected execution path encountered" >> cont exp 
  Nodes _                -> putStrLn "Unexpected collection of nodes encountered" >> cont exp 
  InvalidRevert          -> putStrLn "invalid revert error" >> cont exp
  ExportExploration _    -> putStrLn "Unexpected export problem of execution graph" >> cont exp
  LoadExploration _      -> putStrLn "Unexpected load problem of execution graph" >> cont exp

run_directive :: Options -> Directive -> Cont a -> Cont a
run_directive opts (Require fp) cont exp
  | has_been_included fp opts = cont exp
  | otherwise                 = run_directive opts (Include fp) cont exp
run_directive opts (Include fp) cont exp = do
  let dirs = find include_paths opts
  find_included_file dirs fp >>= \case
    []       -> putStrLn ("could not find " ++ fp ++ " in " ++ show dirs) >> cont exp
    (file:_) -> do
      add_include_path (takeDirectory file) opts
      add_include file opts
      case ".json" `isSuffixOf` file of
        True -> do
          mspec <- decode_json_file file
          case mspec of
            Left err -> putStrLn err >> cont exp
            Right spec -> putStrLn "including .json files is no longer supported" >> cont exp --repl_directive_phrases opts [Right (PFrames spec)] explorer
        False -> catchIOError (Right <$> readFile file) handler >>= \case
          Left err  -> putStrLn err >> cont exp
          Right str -> case parse_component syn_directives_phrases str of
            Left err -> putStrLn err >> cont exp
            Right eps -> run_directives_phrases opts eps cont exp
 where handler :: IOError -> IO (Either String a)
       handler exc | isDoesNotExistError exc = return (Left ("unknown file: " ++ fp))
                   | isPermissionError exc = return (Left ("cannot read: " ++ fp))
                   | isAlreadyInUseError exc = return (Left ("in use: " ++ fp))
                   | otherwise               = return (Left (show exc))



init_server :: Options -> PortNumber -> Spec -> Refiner -> Initialiser -> IO ()
init_server opts port_nr spec' ref' init' = do
  case compile_all spec' ref' init' [] of
    Left errs -> putStrLn "cannot compile specification" >> putStrLn (unlines errs)
    Right (spec', ref, init, _) -> do
      let spec = refine_specification spec' ref
      let state = make_initial_state spec init
      let explorer = init_explorer (Just (spec, state))
      start_server opts port_nr explorer

start_server :: Options -> PortNumber -> Cont ()
start_server opts port_nr explorer = do
      sock <- socket AF_INET Stream 0
      setSocketOption sock ReuseAddr 1
      Network.Socket.bind sock (SockAddrInet port_nr (tupleToHostAddress (127,0,0,1)))
      listen sock 2
      server opts sock  explorer

server :: Options -> Socket -> Cont ()
server opts = continue
  where continue :: Socket -> Cont ()
        continue sock exp = do
          putStrLn "--- AWAITING STATEMENT ---"
          conn <- accept sock
          handle <- socketToHandle (fst conn) ReadWriteMode
          string <- hGetLine handle
          let (_, _, (sid, ctx)) = get_last_edge exp (EI.currRef exp)
          putStrLn string
          let compile_and inpm program = report $ run_ exp (Execute [program] inpm)
              report res = case res of
                ResultTrans exp outs (old,oid) (new,sid) -> report_success sock outs oid old sid new exp
                Path path                        -> do
                  hPutStrLn handle (json_encode (GivePath path))
                  hClose handle
                  continue sock exp
--                Explorer.ExecError err    -> report_error (ExecError err) exp
                Nodes nodes -> do
                  hPutStrLn handle (json_encode (GiveNodes nodes))
                  hClose handle
                  continue sock exp
                ExportExploration exportGraph -> do
                  putStrLn "--- Exporting ---"
                  hPutStrLn handle (json_encode (GiveExportGraph exportGraph))
                  hClose handle
                  continue sock exp
                LoadExploration exp -> do
                  putStrLn "--- Loading execution graph ---"
                  hPutStrLn handle (json_encode (GiveLoadGraph))
                  hClose handle 
                  continue sock exp
                InvalidRevert             -> report_error InvalidState exp
--                CompilationError err      -> report_error (InvalidInput err) exp
              report_success sock outputs old_id c0 state_id ctx exp = do
                let facts_from = state_holds (cfg_state c0)
                let facts_to = state_holds (cfg_state ctx)
                let created_facts    = facts_to \\ facts_from
                let terminated_facts = facts_from \\ facts_to

                let viols = S.fromList (violations outputs)
                let outs = S.fromList (ex_triggers outputs)
                let errs = S.fromList (errors outputs)
                let qress = query_ress outputs

                let transitions = S.fromList (rest_transitions ctx)
                let new_duties = S.fromList (rest_duties ctx) S.\\ S.fromList (rest_duties c0)
                let new_enabled = S.fromList (rest_enabled ctx) S.\\ S.fromList (rest_enabled c0)
                let new_disabled = S.fromList (rest_disabled ctx) S.\\ S.fromList (rest_disabled c0)
                let all_duties = S.fromList $ rest_duties ctx

                let response = case missing_inputs outputs of
                      [] -> CommandSuccess old_id state_id
                                            facts_from facts_to created_facts terminated_facts
                                            viols outs errs qress
                                            new_duties all_duties
                                            new_enabled new_disabled transitions
                      ms -> InputRequired ms 
                hPutStrLn handle (json_encode response)
                hClose handle
                continue sock exp
              report_error err exp = do
                hPutStrLn handle (json_encode err)
                hClose handle
                continue sock exp
          let withCommand cmd = case cmd of 
                CreateEvent term inpm -> compile_and inpm $ Program (Create [] term) 
                TerminateEvent term inpm -> compile_and inpm $ Program (Terminate [] term) 
                QueryCommand term inpm  -> compile_and inpm $ Program (PQuery term)
                Revert new_state    -> report $ run_ exp (Explorer.Revert new_state)
                Status mid          -> report $ run_ exp (Display (maybe (EI.currRef exp) id mid))
                History mid         -> report $ run_ exp (DisplayFull (maybe (EI.currRef exp) id mid))
                Heads               -> report $ run_ exp ExplorationHeads
                CreateExport        -> report $ run_ exp CreateExportExploration
                LoadExport graph    -> report $ run_ exp (LoadExportExploration graph)
                GetFacts inpm       -> do hPutStrLn handle (json_encode (GiveFacts (state_input_holds (cfg_state ctx) inpm)))
                                          hClose handle
                                          continue sock exp
                Kill                -> hPutStrLn handle (json_encode ByeBye) >> hClose handle 
                ActionCommand d a r os force inpm -> compile_and inpm $ Program (PTrigger [] term)
                  where term = App d (Left (a : r : os))
                CmdTrigger t b inpm -> compile_and inpm (Program (PTrigger [] t)) 
                Phrase str inpm -> case parse_component syn_phrases str of
                  Left err  -> do hPutStrLn handle (json_encode (InvalidInput err))
                                  hClose handle >> continue sock exp
                  Right ps  -> report $ run_ exp (Execute (convert_programs ps) inpm)
                Phrases str inpm -> case parse_component syn_phrases str of
                  Left err  -> do hPutStrLn handle (json_encode (InvalidInput err))
                                  hClose handle >> continue sock exp
                  Right ps  -> report $ run_ exp (ExecuteOnce (collapse_programs (convert_programs ps)) inpm) 
          case eitherDecode (Data.ByteString.Lazy.Char8.pack string) of 
            Left err -> do when (find debug opts) (putStrLn err)
                           case (find accept_phrases opts) of
                            False -> do hPutStrLn handle (json_encode (InvalidCommand err))
                                        hClose handle
                                        continue sock exp
                            True  -> withCommand (Phrase string emptyInput)
            Right cmd-> withCommand cmd

json_encode r = Data.ByteString.Lazy.Char8.unpack (encode r)



data Command    = ActionCommand DomId Term Term [Term] Bool InputMap
                | CmdTrigger Term Bool InputMap
                | CreateEvent Term InputMap
                | TerminateEvent Term InputMap
                | QueryCommand Term InputMap
                | Revert Int
                | Status (Maybe Int)
                | Kill
                | GetFacts InputMap
                | History (Maybe Int)
                | Heads
                | CreateExport
                | LoadExport ExecutionGraph
                | Phrase String InputMap
                | Phrases String InputMap

instance FromJSON Command where
  parseJSON = withObject "Command" $ \v -> do
                cmd <- v .: "command"
                case cmd::String of
                  "create"      -> CreateEvent . value_to_term <$> v .: "value" <*> maybe_input v
                  "terminate"   -> TerminateEvent . value_to_term <$> v .: "value" <*> maybe_input v
                  "test-present"-> QueryCommand . value_to_term <$> v .: "value" <*> maybe_input v

                  "test-absent" -> QueryCommand . Not . value_to_term  <$> v .: "value" <*> maybe_input v

                  "enabled"     -> QueryCommand . Enabled . value_to_term <$> v .: "value" <*> maybe_input v
                  "revert"      -> Revert <$> v .: "value"
                  "action"      -> full_action <|> trigger_action
                    where full_action =
                            actionCommand <$>
                                    v .: "act-type" <*> v .: "actor" <*> v .: "recipient"
                               <*>  v .: "objects"  <*> maybe_force v <*> maybe_input v
                          trigger_action = CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v <*> maybe_input v
                          actionCommand d a r os = ActionCommand d (to_term a) (to_term r) (map to_term os)
                  "status"      -> Status <$> v .: "state"
                                <|> return (Status Nothing)
                  "history"     ->  History <$> v .: "state"
                                <|> return (History Nothing)
                  "trace-heads" -> return Heads
                  "create-export" -> return CreateExport
                  "load-export" -> LoadExport <$> v .: "graph"
                  "kill"        -> return Kill
                  "phrase"      -> Phrase <$> v .: "text" <*> maybe_input v
                  "phrases"     -> Phrases <$> v .: "text" <*> maybe_input v
                  "event"       -> CmdTrigger . value_to_term <$> v .: "value" <*> maybe_force v  <*> maybe_input v
                  "facts"       -> GetFacts <$> maybe_input v  
                  _             -> mzero

maybe_force v = v .: "force" <|> return False
maybe_input v = value_based_input <$> v .: "input" <|> return emptyInput

value_based_input :: [AssTuple] -> InputMap
value_based_input = M.fromList . map toTup
  where toTup at = (value_to_tagged $ (value :: AssTuple -> Value) at, assignment at)

encode_store :: Store -> [AssTuple]
encode_store = concatMap toTup . M.assocs
  where toTup (te, HoldsTrue)   = return $ AssTuple (tagged_to_value te) True
        toTup (te, HoldsFalse)  = return $ AssTuple (tagged_to_value te) False
        toTup (te, Unknown)     = [] 

data AssTuple = AssTuple { value :: Value
                         , assignment  :: Bool } deriving (Generic)
instance FromJSON AssTuple where
instance ToJSON AssTuple

data Value      = Atom DomId (Either String Int)
                | Composite DomId [Value]

data StringOrValue = ST String | VT Value

instance FromJSON StringOrValue where
  parseJSON v = case v of
    JSON.String str -> return (ST (unpack str))
    JSON.Object obj -> VT <$> parseJSON v
    _               -> fail ("looking for a string or a value, not a " ++ show v)

to_term :: StringOrValue -> Term
to_term (ST s) = StringLit s
to_term (VT v) = value_to_term v

tag_of :: Value -> DomId
tag_of (Atom d _) = d
tag_of (Composite d _) = d

value_to_term :: Value -> Term
value_to_term v = case v of
  Atom d (Left s)  -> App d (Left [StringLit s])
  Atom d (Right i) -> App d (Left [IntLit i])
  Composite d vs   -> App d (Right $ map value_to_modifier vs)

value_to_modifier :: Value -> Modifier
value_to_modifier v = Rename (no_decoration (tag_of v)) (value_to_term v)

value_to_tagged :: Value -> Tagged
value_to_tagged (Atom d (Left str)) = (String str, d)
value_to_tagged (Atom d (Right i))  = (Int i, d)
value_to_tagged (Composite d vs)    = (Product (map value_to_tagged vs), d)

tagged_to_value :: Tagged -> Value
tagged_to_value (String s, d) = Atom d (Left s)
tagged_to_value (Int i, d) = Atom d (Right i)
tagged_to_value (Product args, d) = Composite d (map tagged_to_value args)

instance FromJSON Value where
  parseJSON = withObject "Value" $ \v ->
                    (\c i -> Atom c (Right i)) <$> v .: "fact-type" <*> v .: "value"
                <|> (\c s -> Atom c (Left s))  <$> v .: "fact-type" <*> v .: "value"
                <|> Composite <$> v .: "fact-type" <*> v .: "value"
                <|> Composite <$> v .: "fact-type" <*> v .: "arguments"

instance ToJSON Value where
  toJSON v = case v of 
    Atom d (Left str) -> object [ "fact-type" .= d, "value" .= toJSON str ]
    Atom d (Right i)  -> object [ "fact-type" .= d, "value" .= toJSON i ]
    Composite d [v]   -> object [ "fact-type" .= d, "value" .= toJSON v ]
    Composite d vs    -> object [ "fact-type" .= d, "arguments" .= toJSON vs ]

data Response   = InvalidCommand String
                | InvalidInput String -- parse error
                | CommandSuccess Int -- Source node ID
                                 Int -- Target node ID
                                 [Tagged] -- source node facts
                                 [Tagged] -- target node facts
                                 [Tagged] -- created facts
                                 [Tagged] -- deleted facts
                                 (S.Set Violation)
                                 (S.Set TransInfo)
                                 (S.Set Error) -- errors: compilation + transition
                                 [QueryRes]         -- query results
                                 (S.Set Tagged) -- new duties
                                 (S.Set Tagged) -- all duties in the current state
                                 (S.Set Tagged) -- newly enabled transitions
                                 (S.Set Tagged) -- newly disabled transitions
                                 (S.Set Transition) -- all transitions
                | InvalidState
                | InputRequired [Tagged]
                | GiveFacts [Tagged]
                | GivePath Path
                | GiveNodes [Node]
                | GiveExportGraph ExecutionGraph
                | GiveLoadGraph
                | ByeBye

instance ToJSON Response where
  toJSON (InputRequired tes) = object [ "response" .= JSON.String "input required", "values" .= toJSON (map tagged_to_value tes)]
  toJSON (InvalidCommand err) = object [ "response" .= JSON.String "invalid command", "message" .= toJSON err ]
  toJSON (CommandSuccess sid_from i
                         facts_from facts_to created_facts terminated_facts
                         vs outs errs qress
                         new_duties all_duties
                         new_enabled new_disabled all_transitions) =
    object [ "response"   .= JSON.String "success"
           , "old-state" .= toJSON sid_from
           , "new-state"  .= toJSON i
           , "source_contents"  .= toJSON (map TaggedJSON facts_from)
           , "target_contents"  .= toJSON (map TaggedJSON facts_to)
           , "created_facts"    .= toJSON (map TaggedJSON created_facts)
           , "terminated_facts" .= toJSON (map TaggedJSON terminated_facts)

           , "violations" .= toJSON vs
           , "output-events" .= toJSON outs
           , "errors"     .= toJSON errs
           , "query-results" .= toJSON qress

           , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties)
           , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled)
           , "new-disabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_disabled)
           , "all-duties" .= toJSON (map TaggedJSON $ S.toList all_duties)
           , "all-disabled-transitions" .= toJSON (map TaggedJSON dis_transitions)
           , "all-enabled-transitions" .= toJSON (map TaggedJSON en_transitions)
           ]
   where en_transitions = map fst $ filter snd $ map get_transition (S.toList all_transitions)
         dis_transitions = map fst $ filter (not . snd) $ map get_transition (S.toList all_transitions)
  toJSON InvalidState       = object [ "response" .= JSON.String "invalid state" ]
  toJSON (InvalidInput err) = object [ "response" .= JSON.String "invalid input"
                                     , "error"    .= toJSON err ]
  toJSON ByeBye             = object [ "response"  .= JSON.String "bye world.." ]
  toJSON (GiveFacts tes)    = object [ "values" .= toJSON (map TaggedJSON tes) ]
  toJSON (GiveNodes nodes)  = object [ "nodes"  .= toJSON (map toJSONNode nodes) ]
    where toJSONNode (sid, cfg) =
            object [ "state_id"             .= toJSON sid
                   , "state_contents"       .= toJSON (map TaggedJSON (state_contents))
                   , "duties"               .= toJSON (map TaggedJSON $ S.toList all_duties)
                   , "disabled-transitions" .= toJSON (map TaggedJSON dis_transitions)
                   , "enabled-transitions"  .= toJSON (map TaggedJSON en_transitions)
                   ]
             where state_contents = state_holds (cfg_state cfg)
                   all_duties = S.fromList $ rest_duties cfg
                   all_transitions = S.fromList (map get_transition (rest_transitions cfg))
                   en_transitions = map fst $ filter snd $ S.toList all_transitions
                   dis_transitions = map fst $ filter (not . snd) $ S.toList all_transitions

  toJSON (GivePath edges)   = object [ "edges"  .= toJSON (map toJSONEdge edges') ]
    where edges' = sortBy (on compare (\((sid,_),_,_) -> sid)) edges
          toJSONEdge ((sid_from,ctx_from), (phr, output), (sid_to, ctx_to)) =
            object [ "phrase"           .= toJSON (ppProgram (snd phr))
                   , "input"            .= toJSON (fst phr)
                   , "source_id"        .= toJSON sid_from
                   , "target_id"        .= toJSON sid_to

                   , "source_contents"  .= toJSON (map TaggedJSON facts_from)
                   , "target_contents"  .= toJSON (map TaggedJSON facts_to)
                   , "created_facts"    .= toJSON (map TaggedJSON created)
                   , "terminated_facts" .= toJSON (map TaggedJSON terminated)

                   , "violations"       .= toJSON rep_viols
                   , "output-events"    .= toJSON outs
                   , "errors"           .= toJSON errs
                   , "query-results"    .= toJSON qress

                   , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties)
                   , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled)
                   , "new-disabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_disabled)
                   , "all-duties" .= toJSON (map TaggedJSON $ S.toList all_duties)
                   , "all-disabled-transitions" .= toJSON (map TaggedJSON dis_transitions)
                   , "all-enabled-transitions" .= toJSON (map TaggedJSON en_transitions)
                   ]
           where facts_from = state_holds (cfg_state ctx_from)
                 facts_to   = state_holds (cfg_state ctx_to)
                 created    = facts_to \\ facts_from
                 terminated = facts_from \\ facts_to

                 rep_viols  = violations output
                 outs = S.fromList (ex_triggers output)
                 errs = S.fromList (errors output)
                 qress = query_ress output

                 all_transitions = S.fromList (rest_transitions ctx_to)
                 en_transitions = map fst $ filter snd $ map get_transition (S.toList all_transitions)
                 dis_transitions = map fst $ filter (not . snd) $ map get_transition (S.toList all_transitions)
                 new_duties = S.fromList (rest_duties ctx_to) S.\\ S.fromList (rest_duties ctx_from)
                 new_enabled = S.fromList (rest_enabled ctx_to) S.\\ S.fromList (rest_enabled ctx_from)
                 new_disabled = S.fromList (rest_disabled ctx_to) S.\\ S.fromList (rest_disabled ctx_from)
                 all_duties = S.fromList $ rest_duties ctx_to

  toJSON (GiveExportGraph graph)  = toJSON graph
  toJSON GiveLoadGraph = object [ "response" .= JSON.String "success" ]

instance ToJSON Violation where
  toJSON (TriggerViolation info) =
    object [ "violation" .= JSON.String "trigger"
           , "info"     .= toJSON info 
           ]
  toJSON (DutyViolation te) =
    object [ "violation" .= toJSON ("duty"::String)
           , "value"     .= toJSON (TaggedJSON te) ]
  toJSON (InvariantViolation d) =
    object [ "violation" .= toJSON ("invariant"::String)
           , "invariant" .= toJSON d ]

instance FromJSON Violation where
  parseJSON = withObject "trigger or duty or invariant violation" $ \o -> do
    violationtype <- o .: "violation"
    case violationtype of
      "trigger"   -> TriggerViolation   <$> o .: "info"
      "duty"      -> DutyViolation      <$> o .: "value"
      "invariant" -> InvariantViolation <$> o .: "invariant"
      _           -> fail ("unknown type: " ++ violationtype)

instance ToJSON QueryRes where
  toJSON qres = case qres of
    QuerySuccess -> JSON.String "success"
    QueryFailure -> JSON.String "failure"

instance FromJSON QueryRes where
  parseJSON o = case o of
      "success" -> return QuerySuccess
      "failure" -> return QueryFailure
      res       -> fail ("unknown query-result " ++ show res)

instance ToJSON Error where
  toJSON err = case err of
    NotTriggerable d -> object ["error-type" .= JSON.String "not triggerable"
                               ,"value" .= d ]
    CompilationError err  -> object ["error-type" .= JSON.String "compilation error"
                                    ,"error" .= toJSON err]
    RuntimeError (MissingInput te) -> 
      object ["error-type" .= JSON.String "missing input"
             ,"error" .= JSON.toJSON (TaggedJSON te) ]
    RuntimeError (InternalError (EnumerateInfiniteDomain d dom)) ->
      object ["error-type" .= JSON.String "enumerating infinite domain"
             ,"error" .= toJSON (d, dom) ]
    RuntimeError (InternalError (MissingSubstitution var)) ->
      object ["error-type" .= JSON.String "missing substitution"
             ,"error" .= toJSON var ]
    RuntimeError (InternalError (PrimitiveApplication d)) ->
      object ["error-type" .= JSON.String "primitive application"
             ,"error" .= d ]
    RuntimeError (InternalError (UndeclaredType d)) ->
      object ["error-type" .= JSON.String "undeclared type"
             ,"error" .= d ]

instance FromJSON Error where
  parseJSON = withObject "NotTriggerable or CompilationError" $ \o -> do
    errortype <- o .: "error-type"
    case errortype of
      "not triggerable"              -> NotTriggerable <$> o .: "value"
      "compilation error"            -> CompilationError   <$> o .: "error"
      _                              -> fail ("unknown type: " ++ errortype)


instance ToJSON Output where
  toJSON (ExecutedTransition info) = object [ "output-type" .= JSON.String "executed-transition", "info" .= toJSON info]
  toJSON (Violation v)    = object [ "output-type" .= JSON.String "violation", "output" .= v]
  toJSON (QueryRes r)     = object [ "output-type" .= JSON.String "query-res", "output" .= r]
  toJSON (ErrorVal e)     = object [ "output-type" .= JSON.String "error-val", "output" .= e]

instance FromJSON Output where
  parseJSON = withObject "outputevent or violation or queryres or errorval" $ \o -> do
    outputtype <- o .: "output-type"
    case outputtype of
      "executed-transition" -> ExecutedTransition <$> o .: "info" 
      "violation"    -> Violation <$> o .: "output" 
      "query-res"    -> QueryRes <$> o .: "output" 
      "error-val"    -> ErrorVal <$> o .: "output" 
      _        -> fail ("unknown output: " ++ outputtype)

instance ToJSON Config where
  toJSON conf = object [
    "spec"             .= cfg_spec conf,
    "state"            .= cfg_state conf,
    "rest_transitions" .= rest_transitions conf,
    "rest_duties"      .= rest_duties conf
    ]

instance FromJSON Config where
  parseJSON = withObject "config" $ \o -> do
    cfg_spec         <- o .: "spec"
    cfg_state        <- o .: "state"
    rest_transitions <- o .: "rest_transitions"
    rest_duties      <- o .: "rest_duties"
    return Config{..}

instance ToJSON Elem where
  toJSON (String el)  = object ["elem-type" .= JSON.String "string",  "elem" .= el]
  toJSON (Int el)     = object ["elem-type" .= JSON.String "int",     "elem" .= el]
  toJSON (Product el) = object ["elem-type" .= JSON.String "product", "elem" .= el]

instance FromJSON Elem where
  parseJSON = withObject "string or int or product" $ \o -> do
    elemtype <- o .: "elem-type"
    case elemtype of
      "string"  -> String <$> o .: "elem"
      "int"     -> Int <$> o .: "elem"
      "product" -> Product <$> o .: "elem"
      _         -> fail ("unknown type: " ++ elemtype)

instance ToJSON Spec where
  toJSON spec = object [
    "decls"      .= decls spec,
    "aliases"    .= aliases spec
    ]

instance FromJSON Spec where
  parseJSON = withObject "spec" $ \o -> do
    decls      <- o .: "decls"
    aliases    <- o .: "aliases"
    return Spec{..}

-- TODO remove show and use ToJSON functions
instance ToJSON State where
  toJSON state = object [
    "contents" .=  show (contents state),
    "time"     .=  (time state)
    ]

-- TODO remove read and use FromJSON functions
instance FromJSON State where
  parseJSON = withObject "state" $ \o -> do
    contents_show <- o .: "contents"
    let contents = read contents_show
    time     <- o .: "time"
    return State{contents=contents, time=time}

instance ToJSON Info where
  toJSON info = object [
    "value" .= toJSON ((value :: Info -> Bool) info ),
    "from-sat" .= toJSON (from_sat info)
    ]

instance FromJSON Info where
  parseJSON = withObject "info" $ \o -> do
    value <- o .: "value"
    from_sat <- o .: "from-sat"
    return Info{..}

instance ToJSON TypeSpec where
  toJSON typespec = object [
    "kind"              .= kind typespec,
    "domain"            .= domain typespec,
    "domain_constraint" .= domain_constraint typespec,
    "derivation"        .= derivation typespec,
    "closed"            .= closed typespec,
    "conditions"        .= conditions typespec
    ]

instance FromJSON TypeSpec where
  parseJSON = withObject "typespec" $ \o -> do
    kind              <- o .: "kind"
    domain            <- o .: "domain"
    domain_constraint <- o .: "domain_constraint"
    derivation        <- o .: "derivation"
    closed            <- o .: "closed"
    conditions        <- o .: "conditions"
    return TypeSpec{..}

instance ToJSON Kind where
  toJSON (Fact kind)  = object ["kind-type" .= JSON.String "Fact",
                                "fact" .= kind]
  toJSON (Act kind)   = object ["kind-type" .= JSON.String "Act",
                                "act" .= kind]
  toJSON (Duty kind)  = object ["kind-type" .= JSON.String "Duty",
                                "duty" .= kind]
  toJSON (Event kind) = object ["kind-type" .= JSON.String "Event",
                                  "event" .= kind]

instance FromJSON Kind where
  parseJSON = withObject "fact or act or duty or event" $ \o -> do
    kindtype <- o .: "kind-type"
    case kindtype of
      "Fact"  -> Fact <$> o .: "fact"
      "Act"   -> Act <$> o .: "act"
      "Duty"  -> Duty <$> o .: "duty"
      "Event" -> Event <$> o .: "event"
      _       -> fail ("unknown type: " ++ kindtype)

instance ToJSON FactSpec where
  toJSON factspec = object [
    "invariant" .= invariant factspec,
    "actor"     .= actor factspec
    ]

instance FromJSON FactSpec where
  parseJSON = withObject "factsspec" $ \o -> do
    invariant <- o .: "invariant"
    actor  <- o .: "actor"
    return FactSpec{..}

instance ToJSON ActSpec where
  toJSON actspec = object [
    "effects"    .= effects actspec,
    "syncs"      .= syncs actspec
    ]

instance FromJSON ActSpec where
  parseJSON = withObject "actspec" $ \o -> do
    effects  <- o .: "effects"
    syncs  <- o .: "syncs"
    return ActSpec{..}

instance ToJSON Term where
  toJSON (Not t)          = object ["term-type" .= JSON.String "Not",
                                    "t" .= t]
  toJSON (And t1 t2)      = object ["term-type" .= JSON.String "And",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Or t1 t2)       = object ["term-type" .= JSON.String "Or",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (BoolLit b)      = object ["term-type" .= JSON.String "BoolLit",
                                    "b" .= b]

  toJSON (Leq t1 t2)      = object ["term-type" .= JSON.String "Leq",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Geq t1 t2)      = object ["term-type" .= JSON.String "Geq",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Ge t1 t2)       = object ["term-type" .= JSON.String "Ge",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Le t1 t2)       = object ["term-type" .= JSON.String "Le",
                                    "t1" .= t1, "t2" .= t2]

  toJSON (Sub t1 t2)      = object ["term-type" .= JSON.String "Sub",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Add t1 t2)      = object ["term-type" .= JSON.String "Add",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Mult t1 t2)     = object ["term-type" .= JSON.String "Mult",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Mod t1 t2)      = object ["term-type" .= JSON.String "Mod",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Div t1 t2)      = object ["term-type" .= JSON.String "Div",
                                    "t1" .= t1, "t2" .= t2]

  toJSON (IntLit i)       = object ["term-type" .= JSON.String "IntLit",
                                    "int" .= i]
  toJSON (StringLit s)    = object ["term-type" .= JSON.String "StringLit",
                                    "string" .= s]

  toJSON (Eq t1 t2)       = object ["term-type" .= JSON.String "Eq",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Neq t1 t2)      = object ["term-type" .= JSON.String "Neq",
                                    "t1" .= t1, "t2" .= t2]

  toJSON (Exists vars t)  = object ["term-type" .= JSON.String "Exists",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (Forall vars t)  = object ["term-type" .= JSON.String "Forall",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (Count vars t)   = object ["term-type" .= JSON.String "Count",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (Sum vars t)     = object ["term-type" .= JSON.String "Sum",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (Max vars t)     = object ["term-type" .= JSON.String "Max",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (Min vars t)     = object ["term-type" .= JSON.String "Min",
                                    "vars" .= vars,
                                    "t" .= t]
  toJSON (When t1 t2)     = object ["term-type" .= JSON.String "When",
                                    "t1" .= t1, "t2" .= t2]
  toJSON (Present t)      = object ["term-type" .= JSON.String "Present",
                                    "t" .= t]
  toJSON (Violated t)     = object ["term-type" .= JSON.String "Violated",
                                    "t" .= t]
  toJSON (Enabled t)      = object ["term-type" .= JSON.String "Enabled",
                                    "t" .= t]
  toJSON (Project t var)  = object ["term-type" .= JSON.String "Project",
                                    "t" .= t, "var" .= var]

  toJSON (Tag t domid)    = object ["term-type" .= JSON.String "Tag",
                                    "t" .= t, "domID" .= domid]
  toJSON (Untag t)        = object ["term-type" .= JSON.String "Untag",
                                    "t" .= t]
  toJSON (Ref var)        = object ["term-type" .= JSON.String "Ref",
                                    "var" .= var]
  toJSON (App domid args) = object ["term-type" .= JSON.String "App",
                                    "domID" .= domid, "args"  .= args]
  toJSON (CurrentTime)    = object ["term-type" .= JSON.String "CurrentTime"]

instance FromJSON Term where
  parseJSON = withObject "terms" $ \o -> do
    termtype <- o .: "term-type"
    case termtype of
      "Not"           -> Not <$> o .: "t"
      "And"           -> And <$> o .: "t1" <*> o .: "t2"
      "Or"            -> Or <$> o .: "t1" <*> o .: "t2"
      "BoolLit"       -> BoolLit <$> o .: "b"

      "Leq"           -> Leq <$> o .: "t1" <*> o .: "t2"
      "Geq"           -> Geq <$> o .: "t1" <*> o .: "t2"
      "Ge"            -> Ge <$> o .: "t1" <*> o .: "t2"
      "Le"            -> Le <$> o .: "t1" <*> o .: "t2"

      "Sub"           -> Sub <$> o .: "t1" <*> o .: "t2"
      "Add"           -> Add <$> o .: "t1" <*> o .: "t2"
      "Mult"          -> Mult <$> o .: "t1" <*> o .: "t2"
      "Mod"           -> Mod <$> o .: "t1" <*> o .: "t2"
      "Div"           -> Div <$> o .: "t1" <*> o .: "t2"

      "IntLit"        -> IntLit <$> o .: "int"
      "StringLit"     -> StringLit <$> o .: "string"

      "Eq"            -> Eq <$> o .: "t1" <*> o .: "t2"
      "Neq"           -> Neq <$> o .: "t1" <*> o .: "t2"

      "Exists"        -> Exists <$> o .: "vars" <*> o .: "t"
      "Forall"        -> Forall <$> o .: "vars" <*> o .: "t"
      "Count"         -> Count <$> o .: "vars" <*> o .: "t"
      "Sum"           -> Sum <$> o .: "vars" <*> o .: "t"
      "Max"           -> Max <$> o .: "vars" <*> o .: "t"
      "Min"           -> Min <$> o .: "vars" <*> o .: "t"

      "When"          -> When <$> o .: "t1" <*> o .: "t2"
      "Present"       -> Present <$> o .: "t"
      "Violated"      -> Violated <$> o .: "t"
      "Enabled"       -> Enabled <$> o .: "t"
      "Project"       -> Project <$> o .: "t" <*> o .: "var"

      "Tag"           -> Tag <$> o .: "t" <*> o .: "domID"
      "Untag"         -> Untag <$> o .: "t"
      "Ref"           -> Ref <$> o .: "var"
      "App"           -> App <$> o .: "domID" <*> o .: "args"
      "CurrentTime"   -> return CurrentTime{}

      _       -> fail ("unknown type: " ++ termtype)

instance ToJSON Modifier where
  toJSON (Rename var term) = object [
    "var"  .= var,
    "term" .= term
    ]

instance FromJSON Modifier where
  parseJSON = withObject "modifier" $ \o -> do
    var <- o.: "var"
    term <- o.: "term"
    return (Rename var term)


instance ToJSON Effect where
  toJSON (CAll vars t)  = object ["effect-type" .= JSON.String "CAll",
                                     "vars" .= vars,
                                     "term" .= t]
  toJSON (TAll vars t)  = object ["effect-type" .= JSON.String "TAll",
                                     "vars" .= vars,
                                     "term" .= t]
  toJSON (OAll vars t)  = object ["effect-type" .= JSON.String "OAll",
                                     "vars" .= vars,
                                     "term" .= t]

instance FromJSON Effect where
  parseJSON = withObject "CAll or Tall" $ \o -> do
    effecttype <- o .: "effect-type"
    case effecttype of
      "TAll"  -> TAll <$> o .: "vars" <*> o .: "term"
      "CAll"  -> CAll <$> o .: "vars" <*> o .: "term"
      _       -> fail ("unknown type: " ++ effecttype)

instance ToJSON Sync where
  toJSON (Sync vars term) = object [
    "vars"  .= vars,
    "term" .= term
    ]

instance FromJSON Sync where
  parseJSON = withObject "sync" $ \o -> do
    vars <- o.: "vars"
    term <- o.: "term"
    return (Sync vars term)

instance ToJSON Var where
  toJSON (Var domid string) = object [
    "domID"  .= domid,
    "string" .= string
    ]

instance FromJSON Var where
  parseJSON = withObject "var" $ \o -> do
    domid <- o.: "domID"
    string <- o.: "string"
    return (Var domid string)

instance ToJSON DutySpec where
  toJSON dutyspec = object [
    "enforcing_acts" .= enforcing_acts dutyspec,
    "violated_when"  .= violated_when dutyspec
    ]

instance FromJSON DutySpec where
  parseJSON = withObject "dutyspec" $ \o -> do
    enforcing_acts <- o.: "enforcing_acts"
    violated_when <- o.: "violated_when"
    return DutySpec{..}

instance ToJSON EventSpec where
  toJSON eventspec = object [
    "event_effects" .= event_effects eventspec
    ]

instance FromJSON EventSpec where
  parseJSON = withObject "eventspec" $ \o -> do
    event_effects <- o.: "event_effects"
    return EventSpec{..}

instance ToJSON Domain where
  toJSON (AnyString)       = object ["domain-type" .= JSON.String "AnyString"]
  toJSON (AnyInt)          = object ["domain-type" .= JSON.String "AnyInt"]
  toJSON (Strings strings) = object ["domain-type" .= JSON.String "Strings", "strings" .= strings]
  toJSON (Ints ints)       = object ["domain-type" .= JSON.String "Ints", "ints" .= ints]
  toJSON (Products vars)   = object ["domain-type" .= JSON.String "Products", "vars" .= vars]
  toJSON (Time)            = object ["domain-type" .= JSON.String "Time"]

instance FromJSON Domain where
  parseJSON = withObject "anystring or anyint or strings or ints or products or time or external" $ \o -> do
    domaintype <- o .: "domain-type"
    case domaintype of
      "AnyString" -> return AnyString{}
      "AnyInt"    -> return AnyInt{}
      "Strings"   -> Strings <$> o .: "strings"
      "Ints"      -> Ints <$> o .: "ints"
      "Products"  -> Products <$> o .: "vars"
      "Time"      -> return Time{}
      _           -> fail ("unknown type: " ++ domaintype)

instance ToJSON Derivation where
  toJSON (Dv vars term)   = object ["derivation-type" .= JSON.String "Dv",
                                    "vars" .= vars, "term" .= term]
  toJSON (HoldsWhen term) = object ["derivation-type" .= JSON.String "HoldsWhen",
                                    "term" .= term]

instance FromJSON Derivation where
  parseJSON = withObject "dv or holdswhen or externalvalue" $ \o -> do
    derivationtype <- o .: "derivation-type"
    case derivationtype of
      "Dv"            -> Dv <$> o .: "vars" <*> o .: "term"
      "HoldsWhen"     -> HoldsWhen <$> o .: "term"
      _       -> fail ("unknown type: " ++ derivationtype)

instance ToJSON TransInfo where
  toJSON info = object [  
      "trans-tagged"      .= toJSON (tagged_to_value (trans_tagged info))
    , "trans-assignments" .= toJSON (encode_store (trans_assignments info))
    , "trans-forced"      .= toJSON (trans_forced info)
    , "trans-actor"       .= toJSON (trans_actor info)
    , "trans-is-action"   .= toJSON (trans_is_action info)
    , "trans-syncs"       .= toJSON (trans_syncs info)
    ]

instance ToJSON Assignment where
  toJSON HoldsTrue = JSON.String "true"
  toJSON HoldsFalse = JSON.String "false"
  toJSON Unknown = JSON.String "unknown"

instance FromJSON Assignment where
  parseJSON o = case o of 
    "true" -> return HoldsTrue 
    "false" -> return HoldsFalse 
    "unknown" -> return Unknown
    s -> fail ("unknown assignment " ++ show s)

instance FromJSON TransInfo where
  parseJSON = withObject "TransInfo" $ \o -> do
    TransInfo <$> o .: "trans-tagged" 
              <*> o .: "trans-assignments"
              <*> o .: "trans-forced"
              <*> o .: "trans-actor"
              <*> o .: "trans-syncs"  

-- TODO remove show and use ToJSON functions
instance ToJSON Transition where
  toJSON transition = object [
    "tagged"  .= show (tagged transition),
    "present" .= exist transition
    ]

-- TODO remove read and use FromJSON functions
instance FromJSON Transition where
  parseJSON = withObject "transition" $ \o -> do
    tagged_show <- o .: "tagged"
    let tagged = read tagged_show
    exist  <- o .: "present"
    return Transition{tagged=tagged, exist=exist}

-- Converting to/from graph
instance ToJSON ExecutionGraph where
  toJSON graph = object [
    "current" .= current graph,
    "nodes"   .=  nodes graph,
    "edges"   .=  edges graph
    ]

instance FromJSON ExecutionGraph where
  parseJSON = withObject "execution graph" $ \o -> do
    current <- o .: "current"
    nodes   <- o .: "nodes"
    edges   <- o .: "edges"
    return ExecutionGraph{..}

instance ToJSON N where
  toJSON node = object [
    "ref"    .= ref node,
    "config" .= config node
    ]

instance FromJSON N where
  parseJSON = withObject "node" $ \o -> do
    ref    <- o .: "ref"
    config <- o .: "config"
    return N{..}

instance ToJSON Edge where
  toJSON edge = object [
    "source" .= source edge,
    "target" .= target edge,
    "po"     .= po edge
    ]

instance FromJSON Edge where
  parseJSON = withObject "edge" $ \o -> do
    source <- o .: "source"
    target <- o .: "target"
    po     <- o .: "po"
    return Edge{..}

-- TODO remove show and use ToJSON functions
instance ToJSON PO where
  toJSON po = object [
    "program" .= ppProgram (snd $ label po),
    "input"   .= show (fst $ label po),
    "output"  .= show (output po)
    ]

-- TODO remove read and use FromJSON functions
instance FromJSON PO where
  parseJSON = withObject "label output" $ \o -> do
    program_show <- o .: "label"
    output_show  <- o .: "output"
    input_show   <- o .: "input"
    let output =  read output_show
    let input = read input_show
    case parse_component syn_phrases program_show of
      Left err  -> error(err)
      Right ps  -> return PO{label=(input, collapse_programs (convert_programs ps)),..}