eflint (empty) → 3.0.0.1
raw patch · 19 files changed
+4717/−0 lines, 19 filesdep +aesondep +basedep +bytestringsetup-changed
Dependencies added: aeson, base, bytestring, containers, directory, exploring-interpreters, fgl, filepath, gll, haskeline, hxt, mtl, network, regex-applicative, text, time, transformers
Files
- CHANGELOG.md +5/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- eflint.cabal +130/−0
- src/Language/EFLINT/Binders.hs +56/−0
- src/Language/EFLINT/Eval.hs +405/−0
- src/Language/EFLINT/Explorer.hs +132/−0
- src/Language/EFLINT/Interpreter.hs +237/−0
- src/Language/EFLINT/JSON.hs +303/−0
- src/Language/EFLINT/Options.hs +137/−0
- src/Language/EFLINT/Parse.hs +458/−0
- src/Language/EFLINT/Print.hs +245/−0
- src/Language/EFLINT/Saturation.hs +41/−0
- src/Language/EFLINT/Spec.hs +508/−0
- src/Language/EFLINT/State.hs +188/−0
- src/Language/EFLINT/StaticEval.hs +495/−0
- src/Language/EFLINT/Util.hs +16/−0
- src/REPL.hs +296/−0
- src/Server.hs +1033/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for flint-simulation++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2019-2022, L. Thomas van Binsbergen++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of L. Thomas van Binsbergen nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ eflint.cabal view
@@ -0,0 +1,130 @@+cabal-version: >=1.10++name: eflint +version: 3.0.0.1+synopsis: Simulation interpreter for FLINT policy descriptions+description:++ Software systems that share potentially sensitive data are subjected to laws, regulations, policies and/or contracts. The monitoring, control and enforcement processes applied to these systems are currently to a large extent manual, which we rather automate by embedding the processes as dedicated and adaptable software services in order to improve efficiency and effectiveness. This approach requires such regulatory services to be closely aligned with a formal description of the relevant norms.+ .+ eFLINT is a domain-specific language developed for formalizing norms from a variety of sources. The theoretical foundations of the language are found in transition systems and in Hohfeld’s framework of legal fundamental conceptions. The language can be used to formalize norms from a large variety of sources. The resulting specifications are executable and support several forms of reasoning such as automatic case assessment, manual exploration and simulation. Moreover, the specifications can be used to develop regulatory services for several types of monitoring, control and enforcement. The language is evaluated through a case study formalizing articles 6(1)(a) and 16 of the General Data Protection Regulation (GDPR).+ .+ Related papers:+ .+ *eFLINT: a Domain-Specific Language for Executable Norm Specifications. Proceedings of GPCE '20. L. Thomas van Binsbergen, Lu-Chi Liu, Robert van Doesburg, and Tom van Engers. <https://doi.org/10.1145/3425898.3426958>. + *Dynamic generation of access control policies from social policies. Proceedings of The 11th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH 2021). Procedia Computer Science 198C (2022) pp. 140-147. L. Thomas van Binsbergen, Milen G. Kebede, Joshua Baugh, Tom van Engers, Dannis G. van Vuurden. + .+ Preprints available at <https://ltvanbinsbergen.nl>++bug-reports: https://gitlab.com/eflint/haskell-implementation+homepage: http://cci-research.nl+license: BSD3+license-file: LICENSE+author: L. Thomas van Binsbergen+maintainer: ltvanbinsbergen@acm.org+copyright: Copyright (C) 2019-2022 L. Thomas van Binsbergen+category: Language+build-type: Simple+extra-source-files: CHANGELOG.md++executable eflint-server+ main-is: Server.hs+ other-modules: Language.EFLINT.State+ Language.EFLINT.Spec+ Language.EFLINT.Parse+ Language.EFLINT.Print+ Language.EFLINT.StaticEval+ Language.EFLINT.Eval+ Language.EFLINT.Saturation+ Language.EFLINT.Binders+ Language.EFLINT.JSON+ Language.EFLINT.Explorer+ Language.EFLINT.Interpreter+ Language.EFLINT.Util+ Language.EFLINT.Options+ build-depends: base >=4.9 && <= 4.14.1+ , containers >=0.5 && <0.7+ , hxt >= 9.3.1.16+ , time >= 1.8.0.2+ , gll >= 0.4.0.13+ , regex-applicative >= 0.3.3+ , aeson >= 1.4.6.0+ , bytestring >= 0.10.8.2+ , network >= 3.1+ , text >= 1.2.4.0+ , filepath >= 1.4.2+ , directory >= 1.3.6+ , exploring-interpreters >= 1.3.0.0+ , fgl >= 5.7 + , mtl >= 2.2 + hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports++executable eflint-repl+ main-is: REPL.hs+ other-modules: Language.EFLINT.State+ Language.EFLINT.Spec+ Language.EFLINT.Parse+ Language.EFLINT.Print+ Language.EFLINT.StaticEval+ Language.EFLINT.Eval+ Language.EFLINT.Saturation+ Language.EFLINT.Binders+ Language.EFLINT.JSON,+ Language.EFLINT.Explorer+ Language.EFLINT.Interpreter+ Language.EFLINT.Util+ Language.EFLINT.Options+ build-depends: base >=4.9 && <= 4.14.1+ , containers >=0.5 && <0.7+ , hxt >= 9.3.1.16+ , time >= 1.8.0.2+ , gll >= 0.4.0.13+ , regex-applicative >= 0.3.3+ , aeson >= 1.4.6.0+ , bytestring >= 0.10.8.2+ , network >= 3.1+ , filepath >= 1.4.2+ , directory >= 1.3.6+ , mtl >= 2.2+ , haskeline >= 0.8.1+ , transformers >= 0.5.6+ , exploring-interpreters >= 1.3.0.0+ , text+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports++library+ exposed-modules : Language.EFLINT.State+ , Language.EFLINT.Spec+ , Language.EFLINT.Parse+ , Language.EFLINT.Print+ , Language.EFLINT.Interpreter+ , Language.EFLINT.Explorer+ other-modules:+ Language.EFLINT.StaticEval+ Language.EFLINT.Eval+ Language.EFLINT.Saturation+ Language.EFLINT.Binders+ Language.EFLINT.JSON+ Language.EFLINT.Util+ Language.EFLINT.Options+ build-depends: base >=4.9 && <= 4.14.1+ , containers >=0.5 && <0.7+ , hxt >= 9.3.1.16+ , time >= 1.8.0.2+ , gll >= 0.4.0.13+ , regex-applicative >= 0.3.3+ , aeson >= 1.4.6.0+ , bytestring >= 0.10.8.2+ , network >= 3.1+ , filepath >= 1.4.2+ , directory >= 1.3.6+ , exploring-interpreters >= 1.3.0.0 + , fgl >= 5.7 + , mtl >= 2.2 + hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -fwarn-incomplete-patterns -fwarn-unused-imports
+ src/Language/EFLINT/Binders.hs view
@@ -0,0 +1,56 @@++module Language.EFLINT.Binders where++import Language.EFLINT.Spec++import qualified Data.Set as S++class HasVars a where+ free :: Spec -> a -> S.Set Var++instance HasVars a => HasVars [a] where+ free spec as = S.unions (map (free spec) as)++instance HasVars Term where+ free spec t = case t of+ BoolLit _ -> S.empty+ IntLit _ -> S.empty+ StringLit _ -> S.empty+ CurrentTime -> S.empty++ Ref v -> S.singleton v+ App d args -> case fmap domain (find_decl spec d) of+ Just (Products xs) -> (S.fromList xs `S.difference` S.fromList (map fst replacements))+ `S.union` free spec (map snd replacements)+ where replacements = make_substitutions_of xs args + _ -> free spec (either id (map (\(Rename p q) -> q)) args)++ Not t -> free spec t+ Present t -> free spec t+ Violated t -> free spec t+ Enabled t -> free spec t+ Project t x -> free spec t+ Tag t x -> free spec t+ Untag t -> free spec t++ And t1 t2 -> free spec t1 `S.union` free spec t2+ Or t1 t2 -> free spec t1 `S.union` free spec t2+ Leq t1 t2 -> free spec t1 `S.union` free spec t2+ Geq t1 t2 -> free spec t1 `S.union` free spec t2+ Ge t1 t2 -> free spec t1 `S.union` free spec t2+ Le t1 t2 -> free spec t1 `S.union` free spec t2+ Mult t1 t2 -> free spec t1 `S.union` free spec t2+ Mod t1 t2 -> free spec t1 `S.union` free spec t2+ Div t1 t2 -> free spec t1 `S.union` free spec t2+ Sub t1 t2 -> free spec t1 `S.union` free spec t2+ Add t1 t2 -> free spec t1 `S.union` free spec t2+ Eq t1 t2 -> free spec t1 `S.union` free spec t2+ Neq t1 t2 -> free spec t1 `S.union` free spec t2+ When t1 t2 -> free spec t1 `S.union` free spec t2++ Exists xs t -> free spec t `S.difference` S.fromList xs+ Forall xs t -> free spec t `S.difference` S.fromList xs+ Count xs t -> free spec t `S.difference` S.fromList xs+ Max xs t -> free spec t `S.difference` S.fromList xs+ Min xs t -> free spec t `S.difference` S.fromList xs+ Sum xs t -> free spec t `S.difference` S.fromList xs
+ src/Language/EFLINT/Eval.hs view
@@ -0,0 +1,405 @@+{-# LANGUAGE LambdaCase, TupleSections #-}++module Language.EFLINT.Eval where++import Language.EFLINT.Spec+import Language.EFLINT.State++import Control.Monad+import Control.Applicative++import Data.Bool (bool)+import Data.List ((\\))+import Data.Maybe (fromJust)+import qualified Data.Map as M++data M_Subs a = M_Subs { runSubs :: Spec -> State -> InputMap -> Subs -> Either RuntimeError [a] }++err :: RuntimeError -> M_Subs a +err re = M_Subs $ \spec state inpm subs -> Left re++nd :: [a] -> M_Subs a+nd vals = M_Subs $ \spec state inpm subs -> return vals++results :: M_Subs a -> M_Subs [a]+results n = M_Subs $ \spec state inpm subs -> (:[]) <$> runSubs n spec state inpm subs++ignoreMissingInput :: M_Subs a -> M_Subs a+ignoreMissingInput m = M_Subs $ \spec state inpm subs -> case runSubs m spec state inpm subs of+ Left (MissingInput _) -> Right []+ res -> res+ +bind :: Var -> Tagged -> M_Subs a -> M_Subs a+bind k v m = M_Subs $ \spec state inpm -> runSubs m spec state inpm . M.insert k v++scope_var :: Var -> M_Subs a -> M_Subs a+scope_var x m = do + te <- every_valid_subs x+ bind x te m++get_type_spec :: DomId -> M_Subs TypeSpec+get_type_spec d = M_Subs $ \spec state inpm subs -> + case find_decl spec d of+ Nothing -> Left (InternalError (UndeclaredType d))+ Just tspec -> Right [tspec]++get_dom :: DomId -> M_Subs (Domain, Term)+get_dom d = M_Subs $ \spec state inpm subs -> + case find_decl spec d of+ Nothing -> Left (InternalError (UndeclaredType d))+ Just tspec -> Right [(domain tspec, domain_constraint tspec)]++get_time :: M_Subs Int+get_time = M_Subs $ \spec state inpm subs -> return [time state]++get_subs :: M_Subs Subs+get_subs = M_Subs $ \spec state inpm subs -> return [subs]++modify_subs :: (Subs -> Subs) -> M_Subs a -> M_Subs a+modify_subs mod m = M_Subs $ \spec state inpm -> runSubs m spec state inpm . mod ++get_spec :: M_Subs Spec +get_spec = M_Subs $ \spec state inpm subs -> return [spec]++get_state :: M_Subs State+get_state = M_Subs $ \spec state inpm subs -> return [state]++get_input :: M_Subs InputMap+get_input = M_Subs $ \spec state inpm subs -> return [inpm]++get_input_assignment :: Tagged -> M_Subs Assignment+get_input_assignment te = M_Subs $ \spec state inpm subs -> + Right [maybe Unknown (bool HoldsFalse HoldsTrue) (M.lookup te inpm)]++get_assignment :: Tagged -> M_Subs Assignment+get_assignment te@(_,d) = M_Subs $ \spec state inpm subs -> + Right [maybe Unknown op (M.lookup te (contents state))]+ where op info | from_sat info = Unknown+ | value info = HoldsTrue+ | otherwise = HoldsFalse ++instance Functor M_Subs where+ fmap = liftM ++instance Applicative M_Subs where+ pure = return+ (<*>) = ap++instance Monad M_Subs where+ return a = M_Subs $ \spec state inpm subs -> return [a]+ (>>=) m f = M_Subs $ \spec state inpm subs -> do + as <- runSubs m spec state inpm subs+ let op res a = (++res) <$> runSubs (f a) spec state inpm subs+ foldM op [] as ++instance Alternative M_Subs where+ empty = M_Subs $ \spec state inpm subs -> return []+ m1 <|> m2 = M_Subs $ \spec state inpm subs -> do+ xs <- runSubs m1 spec state inpm subs + ys <- runSubs m2 spec state inpm subs+ return (xs ++ ys)++instance MonadPlus M_Subs where++instantiate_domain :: DomId -> Domain -> M_Subs Elem+instantiate_domain d dom = case dom of+ Time -> get_time >>= \time -> nd [ Int i | i <- [0..time]]+ AnyString -> err (InternalError $ EnumerateInfiniteDomain d dom)+ AnyInt -> err (InternalError $ EnumerateInfiniteDomain d dom)+ Strings ss -> nd [ String s | s <- ss ]+ Ints is -> nd [ Int i | i <- is ]+ Products xs -> Product <$> sequence (map every_valid_subs xs)++substitute_var :: Var -> M_Subs Tagged+substitute_var x = do+ spec <- get_spec+ subs <- get_subs+ case M.lookup x subs of+ Just te@(v,d') -> return (v, remove_decoration spec x)+ Nothing -> err (InternalError $ MissingSubstitution x)++every_valid_subs :: Var -> M_Subs Tagged+every_valid_subs x = do+ spec <- get_spec+ let d = remove_decoration spec x+ (dom, _) <- get_dom d + if enumerable spec dom then generate_instances d+ else every_available_subs spec d+ where generate_instances d = do + (dom, dom_filter) <- get_dom d + e <- instantiate_domain d dom+ let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args)+ _ -> M.singleton (no_decoration d) (e,d)+ modify_subs (`subsUnion` bindings) (checkTrue (eval dom_filter))+ return (e,d)+ every_available_subs spec d = do+ state <- get_state + inpm <- get_input+ nd [ te | te@(v,d') <- state_input_holds state inpm, d' == d ]++-- if fact/duty/event/action is of an inenumerable type, is derived with "Holds when" and is not in state,+-- then check if it is a valid instance and whether it satisfies derivation clause+-- if so, consider it to hold true+is_in_virtual_state :: Tagged -> M_Subs Bool+is_in_virtual_state te@(_,d) = do+ spec <- get_spec+ is_valid_instance te >>= \case+ False -> return False+ True -> do+ get_input_assignment te >>= \case+ HoldsTrue -> return True+ HoldsFalse -> return False+ Unknown -> do+ get_assignment te >>= \case+ HoldsTrue -> return True+ HoldsFalse -> return False+ Unknown -> do+ is_derivable te >>= \case+ True -> return True+ False -> case fromJust (closed_type spec d) of+ True -> return False+ False -> err (MissingInput te)++is_enabled :: Tagged -> M_Subs Bool +is_enabled v@(e,d) = do + spec <- get_spec+ is_in_virtual_state v >>= \case + False -> return False + True -> sat_conditions v >>= \case+ False -> return False+ True -> case fmap kind (find_decl spec d) of+ Just (Act aspec) -> do+ (dom, _) <- get_dom d+ let (Product args, Products xs) = (e, dom)+ modify_subs (`subsUnion` (M.fromList (zip xs args))) $ do+ sync_infos <- concat <$> mapM eval_sync (syncs aspec) + return (all (not . trans_forced) sync_infos)+ _ -> return True++is_valid_instance :: Tagged -> M_Subs Bool+is_valid_instance te@(e,d) = do + (dom, dom_filter) <- get_dom d + let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args)+ _ -> M.singleton (no_decoration d) te+ let check_constraint = modify_subs (`subsUnion` bindings) (whenBool (eval dom_filter) return)+ case (e, dom) of + (Int i, Ints is) | i `elem` is -> check_constraint+ (Int i, AnyInt) -> check_constraint+ (String s, Strings ss) | s `elem` ss -> check_constraint+ (String s, AnyString) -> check_constraint+ (Product args, Products params) | length args == length params ->+ and <$> mapM is_valid_instance args >>= \case+ False -> return False+ True -> check_constraint + _ -> return False++is_derivable :: Tagged -> M_Subs Bool+is_derivable te@(e,d) = derivation_closure_on te $ do+ spec <- get_spec+ (dom, _) <- get_dom d+ let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args)+ _ -> M.singleton (no_decoration d) te+ let consider_clause deriv = case deriv of + Dv xs dvt -> do tes <- modify_subs (`subsUnion` bindings) + (foreach (xs \\ M.keys bindings) (whenTagged (eval dvt) return))+ return (te `elem` tes) -- valid instance and in DV+ HoldsWhen t -> modify_subs (`subsUnion` bindings) (whenBool (eval t) return )+ case fmap derivation (find_decl spec d) of + Nothing -> return False+ Just dvs -> (or <$> mapM consider_clause dvs) >>= \case + True -> sat_conditions te+ False -> return False++derivation_closure_on :: Tagged -> M_Subs Bool -> M_Subs Bool+derivation_closure_on te m = M_Subs $ \spec state inpm subs -> case M.lookup te (contents state) of+ Just info -> return [value info]+ Nothing -> runSubs m spec (mod state) inpm subs+ where mod s = s { contents = M.insert te (Info { value = False, from_sat = True }) (contents s) }++sat_conditions :: Tagged -> M_Subs Bool+sat_conditions te@(v,d) = + is_valid_instance te >>= \case + False -> return False+ True -> do+ tspec <- get_type_spec d+ (dom, _) <- get_dom d+ let bindings = case (dom,v) of (Products xs, Product args) -> M.fromList (zip xs args)+ _ -> M.singleton (no_decoration d) te+ modify_subs (`subsUnion` bindings) (and <$> mapM (flip whenBool return . eval) (conditions tspec))++is_violated :: Tagged -> M_Subs Bool+is_violated te@(_,d) = (&&) <$> is_in_virtual_state te <*> violation_condition te+ where violation_condition te = do + spec <- get_spec + eval_violation_condition te (find_violation_cond spec d)++eval_violation_condition :: Tagged -> Maybe [Term] -> M_Subs Bool+eval_violation_condition te@(v,d) mconds = do+ (dom, _) <- get_dom d+ let Products xs = dom+ Product args = v+ modify_subs (`subsUnion` (M.fromList (zip xs args))) + (whenBool (eval (maybe (BoolLit False) (foldr Or (BoolLit False)) mconds)) return)+++syncTransInfos :: [TransInfo] -> (Store, Bool {- forced? -})+syncTransInfos = foldr op (emptyStore, False)+ where op (TransInfo te ass is_f is_a tes) (ass',is_f') = + (ass `store_union` ass', is_f || is_f')++instantiate_trans :: Tagged -> M_Subs TransInfo+instantiate_trans te@(v,d) = do + tspec <- get_type_spec d+ is_enabled <- is_enabled te + case kind tspec of + Fact _ -> empty+ Duty _ -> empty + Act aspec -> do_transition te actor is_enabled (effects aspec) (syncs aspec)+ Event espec -> do_transition te actor is_enabled (event_effects espec) []+ where do_transition te@(v,d) isAction is_enabled effects ss = do + (dom, _) <- get_dom d+ let Products xs = dom+ let Product args = v+ modify_subs (`subsUnion` (M.fromList (zip xs args))) $ do+ sync_infos <- concat <$> mapM eval_sync ss + let (ss_ass,any_f) = syncTransInfos sync_infos+ ass' <- store_unions <$> mapM eval_effect effects+ let ass = ass' `store_union` ss_ass+ return (TransInfo te ass (any_f || not is_enabled) isAction sync_infos)+ actor = case v of Product (a:objs) -> Just a+ _ -> Nothing++eval_sync :: Sync -> M_Subs [TransInfo]+eval_sync (Sync xs t) = foreach xs (whenTagged (eval t) instantiate_trans)++eval_effect :: Effect -> M_Subs Store+eval_effect (CAll xs t) = M.fromList . map (,HoldsTrue) <$> foreach xs (whenTagged (eval t) return)+eval_effect (TAll xs t) = M.fromList . map (,HoldsFalse) <$> foreach xs (whenTagged (eval t) return)+eval_effect (OAll xs t) = M.fromList . map (,Unknown) <$> foreach xs (whenTagged (eval t) return)++get_kind :: DomId -> M_Subs Kind+get_kind d = M_Subs $ \spec state inpm subs -> return $ maybe [] (:[]) (find_kind spec d) + where find_kind :: Spec -> DomId -> Maybe Kind + find_kind spec d = fmap kind (find_decl spec d)++whenBool :: M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a+whenBool m f = m >>= \case ResBool b -> f b+ _ -> empty++checkTrue :: M_Subs Value -> M_Subs () +checkTrue m = m >>= \case ResBool True -> return () + _ -> empty++checkFalse :: M_Subs Value -> M_Subs () +checkFalse m = m >>= \case ResBool False -> return () + _ -> empty+++whenInt :: M_Subs Value -> (Int -> M_Subs a) -> M_Subs a+whenInt m f = m >>= \case ResInt v -> f v+ _ -> empty++whenInts :: M_Subs Value -> ([Int] -> M_Subs a) -> M_Subs a+whenInts m f = results m >>= sequence . map (flip whenInt return . return) >>= f++whenTagged :: M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a+whenTagged m f = m >>= \case ResTagged v -> f v+ _ -> empty++whenTaggedHolds m f = m >>= \case ResTagged v -> is_in_virtual_state v >>= \case+ True -> f v+ False -> empty+ _ -> empty++whenString :: M_Subs Value -> (String -> M_Subs a) -> M_Subs a+whenString m f = m >>= \case ResString s -> f s+ _ -> empty++eval :: Term -> M_Subs Value+eval t0 = case t0 of+ CurrentTime -> ResInt <$> get_time+ StringLit s -> return (ResString s)+ BoolLit b -> return (ResBool b)+ IntLit i -> return (ResInt i)+ Ref x -> ResTagged <$> substitute_var x+ App d params-> do (dom,dom_filter) <- get_dom d+ case dom of + Products xs -> do + let replacements = make_substitutions_of xs params+ tes <- mapM (\(x,t) -> whenTagged (eval t) (return . (x,))) replacements+ args <- modify_subs (`subsUnion` M.fromList tes) (mapM substitute_var xs)+ modify_subs (`subsUnion` (M.fromList (zip xs args))) $ do+ checkTrue (eval dom_filter)+ return (ResTagged (Product args, d))+ _ -> err (InternalError $ PrimitiveApplication d)+ Tag t d -> eval t >>= flip tag d+ Untag t -> eval t >>= untag+ Not t -> whenBool (eval t) $ \b -> return (ResBool (not b))+ And t1 t2 -> whenBool (eval t1) $ \case + False -> return (ResBool False)+ True -> whenBool (eval t2) (return . ResBool) + Or t1 t2 -> whenBool (eval t1) $ \case + True -> return (ResBool True)+ False -> whenBool (eval t2) (return . ResBool)+-- And t1 t2 -> whenBool (eval t1) $ \b1 -> whenBool (eval t2) (\b2 -> return (ResBool (and [b1,b2])))+-- Or t1 t2 -> whenBool (eval t1) $ \b1 -> whenBool (eval t2) (\b2 -> return (ResBool (or [b1,b2])))+ Leq t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResBool (v1 <= v2)))+ Le t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResBool (v1 < v2)))+ Geq t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResBool (v1 >= v2)))+ Ge t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResBool (v1 > v2)))+ Mult t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResInt (v1 * v2)))+ Mod t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResInt (v1 `mod` v2)))+ Div t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResInt (v1 `div` v2)))+ Sub t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResInt (v1 - v2)))+ Add t1 t2 -> whenInt (eval t1) $ \v1 -> whenInt (eval t2) (\v2 -> return (ResInt (v1 + v2)))+ Eq t1 t2 -> ((ResBool .) . (==)) <$> eval t1 <*> eval t2+ Neq t1 t2 -> ((ResBool .) . (/=)) <$> eval t1 <*> eval t2++ Sum xs t1 -> ResInt . sum <$> foreach xs (whenInt (eval t1) return)+ Count xs t1 -> ResInt . length <$> foreach xs (eval t1)+ Max xs t1 -> ResInt . (\xs -> if null xs then 0 else maximum xs) <$> foreach xs (whenInt (eval t1) return)+ Min xs t1 -> ResInt . (\xs -> if null xs then 0 else minimum xs) <$> foreach xs (whenInt (eval t1) return)+ When t1 t2 -> -- order matters because of constraint that equal variables have equal instantiations+ -- however, with renaming some of these constraints can be lifted+ -- this modification propagates in the same order as the evaluation order+ eval t1 >>= \v1 -> whenBool (eval t2) (\case True -> return v1+ False -> empty)+ {- whenBool (eval t2) $ \case True -> eval t1 + False -> empty-}+ Present t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_in_virtual_state v)+ Violated t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_violated v)+ Enabled t1 -> whenTagged (eval t1) (\v -> ResBool <$> is_enabled v)+ Exists xs t -> ResBool . not . null <$> results (foldr scope_var (checkTrue (eval t)) xs) + Forall xs t -> ResBool . and <$> results (foldr scope_var (whenBool (eval t) return) xs)++ Project t x -> whenTagged (eval (t)) $ \te@(e,d) -> case e of + Product tes -> do (dom, _) <- get_dom d+ case dom of Products rs | length tes == length rs -> + case elemIndex x rs of+ Nothing -> empty+ Just j -> return (ResTagged (tes !! j))+ _ -> empty+ _ -> empty+ where elemIndex x rs = msum (zipWith op [0..] rs)+ where op j y | x == y = Just j+ | otherwise = Nothing+++foreach :: [Var] -> M_Subs a -> M_Subs [a]+foreach xs m = results (foldr scope_var m xs)++tag :: Value -> DomId -> M_Subs Value+tag (ResInt i) d = return $ ResTagged (Int i,d)+tag (ResString s) d = return $ ResTagged (String s, d)+tag (ResTagged (v,_)) d = return $ ResTagged (v,d)+tag (ResBool b) _ = empty++untag :: Value -> M_Subs Value+untag (ResTagged (Int i, d)) = return $ ResInt i+untag (ResTagged (String s, d)) = return $ ResString s+untag (ResTagged (Product _, _)) = empty+untag (ResBool _) = empty+untag (ResInt _) = empty+untag (ResString _) = empty++
+ src/Language/EFLINT/Explorer.hs view
@@ -0,0 +1,132 @@+{-# LANGUAGE TupleSections #-}++module Language.EFLINT.Explorer where++import Language.EFLINT.Spec (Spec, Phrase(PSkip), ppTagged)+import Language.EFLINT.State (State, emptyInput, InputMap, TransInfo(..), Assignment(..), trans_is_action)+import Language.EFLINT.Interpreter (Program(..), Config(..), interpreter, initialConfig, Output, getOutput)+import Language.EFLINT.Print()++import qualified Language.Explorer.Pure as EI+import Language.Explorer.Monadic (jump)++import Data.Tree (drawTree, Tree(..))++type Explorer = EI.Explorer Label Config [Output]++type Label = (InputMap, Program)++data Instruction = Execute [Program] InputMap+ | ExecuteOnce Program InputMap+ | Revert Ref + | Display Ref -- `last' edge leading to given ref+ | DisplayFull Ref -- full `history', see `Path' below, for given ref+ | ExplorationHeads -- nodes in the execution graph without outgoing edges+ | CreateExportExploration -- create export data to recreate execution graph+ | LoadExportExploration ExecutionGraph -- load execution graph+data Response = ResultTrans Explorer [Output] (Config, Ref) (Config, Ref)+ | Path Path+ | Nodes [Node]+ | InvalidRevert+ | ExportExploration ExecutionGraph+ | LoadExploration Explorer++type Ref = Int -- state identifier+type Path = [(Node, (Label, [Output]), Node)] +type Node = (Ref, Config)++data N = N {+ ref :: Ref+ , config :: Config+ } + deriving (Eq)++data Edge = Edge {+ source :: Ref+ , target :: Ref+ , po :: PO+ } + deriving (Eq)++data PO = PO {+ label :: Label + , output :: [Output]+ } + deriving (Eq)++data ExecutionGraph = ExecutionGraph {+ current :: Ref+ , nodes :: [N]+ , edges :: [Edge]+ }++showTree :: Explorer -> String+showTree = drawTree . fmap (("#"++) . show . fst) . EI.toTree++showTriggerTree :: TransInfo -> String+showTriggerTree = drawTree . fmap report . triggerTree+ where report info = ppTagged (trans_tagged info) ++ " " ++ whether_enabled +-- ++ "\n" ++ unlines (map (uncurry mod) (M.assocs (trans_assignments info)))+ where mod te ass = case ass of HoldsTrue -> "+" ++ ppTagged te+ HoldsFalse -> "-" ++ ppTagged te+ Unknown -> "~" ++ ppTagged te+ whether_enabled | not (trans_is_action info) = ""+ | trans_forced info = "(DISABLED)"+ | otherwise = "(ENABLED)"++triggerTree :: TransInfo -> Tree TransInfo +triggerTree t = Node t (map triggerTree (trans_syncs t))++get_last_edge :: Explorer -> Ref -> ((Ref, Config), (Label, [Output]), (Ref, Config))+get_last_edge exp cr = case reverse (EI.getPathFromTo exp 1 cr) of+ (edge:_) -> edge + _ -> maybe (error ("ASSERT: get_last_edge1")) (\cfg -> ((cr,cfg), ((emptyInput, Program PSkip),[]), (cr,cfg))) (EI.deref exp cr) + +init_tree_explorer, init_graph_explorer :: Maybe (Spec,State) -> Explorer+init_tree_explorer = EI.mkExplorer False (const . const $ False) defInterpreter . initialConfig+init_graph_explorer = EI.mkExplorer True (==) defInterpreter . initialConfig++defInterpreter p c = getOutput $ interpreter p c++run_ :: Explorer -> Instruction -> Response+run_ exp instr = case instr of + Execute ps inpm -> + let (exp',outs) = EI.executeAll (map (inpm,) ps) exp+ cfg' = EI.config exp'+ ref' = EI.currRef exp'+ in ResultTrans exp' outs (EI.config exp, EI.currRef exp) (cfg', ref')+ ExecuteOnce ps inpm -> + let (exp',outs) = EI.execute (inpm,ps) exp+ cfg' = EI.config exp'+ ref' = EI.currRef exp'+ in ResultTrans exp' outs (EI.config exp, EI.currRef exp) (cfg', ref')+ Revert r -> case jump r exp of + Nothing -> InvalidRevert+ Just exp' -> ResultTrans exp' [] (EI.config exp, EI.currRef exp) (EI.config exp', EI.currRef exp')+ Display id -> ResultTrans exp out (from, pr) (to, cr)+ where ((pr,from), (_,out), (cr, to)) = get_last_edge exp id+ DisplayFull id -> Path $ EI.getPathFromTo exp 1 id+ ExplorationHeads -> Nodes $ EI.leaves exp+ CreateExportExploration -> ExportExploration $ convertToGraph (EI.toExport exp)+ LoadExportExploration graph -> LoadExploration $ EI.fromExport exp (convertFromGraph graph)++convertToGraph :: (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))]) -> ExecutionGraph+convertToGraph (cid, nodes, edges) = ExecutionGraph{current=cid, nodes=(map convertToN nodes), edges=(map convertToEdges edges)}++convertFromGraph :: ExecutionGraph -> (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])+convertFromGraph graph = (current graph, map convertFromN (nodes graph), map convertFromEdges (edges graph))++convertToN :: (Ref, Config) -> N+convertToN (r, c) = N{ref=r, config=c}++convertFromN :: N -> (Ref, Config) +convertFromN n = (ref n, config n)++convertToEdges :: (Ref, Ref, (Label, [Output])) -> Edge+convertToEdges (sid, tid, (p, o)) = Edge{source=sid, target=tid, po=PO{label=p, output=o}}++convertFromEdges :: Edge -> (Ref, Ref, (Label, [Output]))+convertFromEdges edge = (source edge, target edge, convertFromPO (po edge))++convertFromPO :: PO -> (Label, [Output])+convertFromPO po = (label po, output po)
+ src/Language/EFLINT/Interpreter.hs view
@@ -0,0 +1,237 @@+{-# LANGUAGE RecordWildCards, LambdaCase #-}++module Language.EFLINT.Interpreter (Config(..), Program(..), interpreter, initialConfig, rest_disabled, rest_enabled, get_transition, context2config, make_initial_state+ ,OutputWriter, Output(..), getOutput+ ,errors, violations, ex_triggers, query_ress, missing_inputs+ ,convert_programs, collapse_programs) where++import Language.EFLINT.Eval+import Language.EFLINT.Spec+import Language.EFLINT.Saturation+import Language.EFLINT.StaticEval (compile_phrase, runStatic) +import Language.EFLINT.State++import Control.Monad (forM, when)+import Control.Monad.Writer (Writer, tell, runWriter)+import Control.Applicative (empty)++import qualified Data.Map as M+import qualified Data.Set as S++data Program = Program Phrase + | PSeq Program Program+ | ProgramSkip+ deriving (Eq, Show)++data Config = Config {+ cfg_spec :: Spec+ , cfg_state :: State + , rest_transitions :: [Transition] -- (label * enabled?) -- replaced+ , rest_duties :: [Tagged] -- replaced after ever step+ }+ deriving (Eq)++data Output = ErrorVal Error+ | ExecutedTransition TransInfo + | Violation Violation+ | QueryRes QueryRes -- whether query succeed or not+ deriving (Eq, Show, Read)++convert_programs :: [Phrase] -> [Program]+convert_programs phrases = map Program phrases++collapse_programs :: [Program] -> Program+collapse_programs [] = ProgramSkip+collapse_programs programs = (foldr1 PSeq programs)++interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config)+interpreter (inpm, Program p) cfg = case runStatic (compile_phrase p) (ctx_spec ctx) of+ Left err -> tell [ErrorVal (CompilationError (unlines err))] >> return Nothing + Right (spec', p') -> fmap context2config <$> sem_phrase p' inpm + (ctx{ctx_spec = spec', ctx_state = rebase_and_sat spec' (ctx_state ctx)}) + where ctx = config2context cfg+interpreter (inpm, PSeq p1 p2) cfg = (interpreter (inpm,p1) cfg) >>= interpreter (inpm,p2) . maybe cfg id+interpreter (inpm, ProgramSkip) cfg = return Nothing++initialConfig Nothing = context2config (emptyContext emptySpec)+initialConfig (Just (spec,state)) = context2config $+ (emptyContext spec) { ctx_state = state }++context2config :: Context -> Config+context2config ctx = Config {+ cfg_spec = ctx_spec ctx+ , cfg_state = ctx_state ctx+ , rest_transitions = ctx_transitions ctx+ , rest_duties = ctx_duties ctx+ }++config2context :: Config -> Context+config2context cfg = Context {+ ctx_spec = cfg_spec cfg+ , ctx_state = cfg_state cfg+ , ctx_transitions = []+ , ctx_duties = []+ }++rest_enabled = map fst . filter snd . map get_transition . rest_transitions+rest_disabled = map fst . filter (not . snd) . map get_transition . rest_transitions++get_transition :: Transition -> (Tagged, Bool)+get_transition transition = (tagged transition, exist transition)++ex_triggers :: [Output] -> [TransInfo]+ex_triggers = concatMap op+ where op (ExecutedTransition out) = [out]+ op _ = []++violations :: [Output] -> [Violation]+violations = concatMap op+ where op (Violation v) = [v]+ op _ = []++errors :: [Output] -> [Error]+errors = concatMap op+ where op (ErrorVal err) = [err]+ op _ = []++query_ress :: [Output] -> [QueryRes]+query_ress = concatMap op+ where op (QueryRes b) = [b]+ op _ = []++missing_inputs :: [Output] -> [Tagged]+missing_inputs = S.toList . S.fromList . concatMap op+ where op (ErrorVal (RuntimeError (MissingInput te))) = [te]+ op _ = []++type OutputWriter = Writer [Output]++getOutput :: OutputWriter a -> (a,[Output])+getOutput = runWriter++error_or_process :: M_Subs a -> Spec -> State -> InputMap -> ([a] -> OutputWriter (Maybe Context)) -> OutputWriter (Maybe Context)+error_or_process ma spec state inpm fa = case runSubs ma spec state inpm emptySubs of+ Left err -> tell [ErrorVal $ RuntimeError err] >> return Nothing+ Right as -> fa as++sem_phrase :: CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)+sem_phrase p inpm c0 = case p of+ CPSkip -> return Nothing+ CPOnlyDecls -> no_effect + CQuery t -> error_or_process (eval t) spec state inpm $ \vs -> do + let queryRes | all (== (ResBool True)) vs = QuerySuccess+ | otherwise = QueryFailure+ tell [QueryRes queryRes] >> no_effect+ CCreate vs t -> single_effect (CAll vs t)+ CTerminate vs t -> single_effect (TAll vs t)+ CObfuscate vs t -> single_effect (OAll vs t)+ CDo te -> error_or_process (trigger_or_fail te) spec state inpm (consider_transinfos . (:[]))+ CTrigger vs t -> let m_subs = do tes <- foreach vs (whenTagged (eval t) return)+ forM tes trigger_or_fail + in error_or_process m_subs spec state inpm consider_transinfos+ CPDir dir -> return_context emptyStore [dir] + CSeq p q -> sem_phrase p inpm c0 >>= (sem_phrase q inpm . maybe c0 id)+ where spec = ctx_spec c0+ state = ctx_state c0++ return_context :: Store -> [CDirective] -> OutputWriter (Maybe Context)+ return_context ass dirs = do + let duties = [ te | te@(v,d) <- (state_input_holds state' inpm)+ , Duty _ <- maybe [] (:[]) (fmap kind (find_decl spec' d)) ]+ error_or_process (find_duty_violations duties) spec' state' inpm $ \d_viols -> + error_or_process (find_inv_violations (S.toList $ invariants spec')) spec' state' inpm $ \i_viols -> do+ tell (map Violation (concat d_viols ++ concat i_viols)) + error_or_process find_transitions spec' state' inpm $ \tss -> + return $ Just $ c0+ { ctx_state = state'+ , ctx_spec = spec'+ , ctx_transitions = concat tss+ , ctx_duties = duties + }+ where state' = rebase_and_sat spec (make_assignments ass state)+ spec' = process_directives dirs spec++ no_effect :: OutputWriter (Maybe Context)+ no_effect = return_context emptyStore []++ single_effect :: Effect -> OutputWriter (Maybe Context)+ single_effect eff =+ error_or_process (eval_effect eff) spec state inpm $ \stores ->+ return_context (M.unions stores) {- always just one store-} []++ trigger_or_fail :: Tagged -> M_Subs (Either Tagged TransInfo)+ trigger_or_fail te@(_,d) | triggerable spec d = Right <$> instantiate_trans te+ | otherwise = return $ Left te++ consider_transinfos infos = case infos of+ [[Left te]] -> tell [ErrorVal (NotTriggerable te)] >> no_effect+ [[Right info]] -> report_on_trans info+ _ -> tell [ErrorVal NonDeterministicTransition] >> no_effect +++ report_on_trans :: TransInfo -> OutputWriter (Maybe Context)+ report_on_trans info = do+ tell [ExecutedTransition info]+ when (trans_is_action info && trans_forced info) + (tell [Violation (TriggerViolation info)])+ return_context (trans_assignments info) [] ++find_inv_violations :: [DomId] -> M_Subs [Violation]+find_inv_violations ds = do + spec <- get_spec + forM ds $ \d -> do+ let term = Exists [Var d ""] (Present (Ref (Var d "")))+ ignoreMissingInput (checkFalse (eval term))+ return (InvariantViolation d)++find_duty_violations :: [Tagged] -> M_Subs [Violation]+find_duty_violations tes = do + spec <- get_spec + forM tes $ \te@(_,d) -> do+ ignoreMissingInput (eval_violation_condition te (find_violation_cond spec d)) >>= \case + True -> return (DutyViolation te)+ False -> empty + +find_transitions :: M_Subs [Transition]+find_transitions = do+ spec <- get_spec + concat <$> mapM gen_trans (trigger_decls spec)+ where gen_trans (d,_) = results $ ignoreMissingInput $ do+ tagged <- every_possible_subs (no_decoration d)+ exist <- is_in_virtual_state tagged+ return Transition{..}++every_possible_subs :: Var -> M_Subs Tagged+every_possible_subs x = do+ spec <- get_spec+ let d = remove_decoration spec x+ (dom, _) <- get_dom d+ if enumerable spec dom then generate_instances d+ else every_available_subs d+ where generate_instances d = do+ (dom, dom_filter) <- get_dom d+ e <- instantiate_domain d dom+ let bindings = case (dom,e) of (Products xs, Product args) -> M.fromList (zip xs args)+ _ -> M.singleton (no_decoration d) (e,d) + modify_subs (`subsUnion` bindings) (checkTrue (eval dom_filter))+ return (e,d)+ every_available_subs d = do+ (dom, dom_filter) <- get_dom d+ case dom of+ Products xs -> do+ args <- sequence (map every_possible_subs xs)+ modify_subs (`subsUnion` (M.fromList (zip xs args))) (checkTrue (eval dom_filter))+ return (Product args, d)+ _ -> do+ state <- get_state+ input <- get_input+ nd $ [ te | te@(v,d') <- state_input_holds state input, d' == d ]++make_initial_state :: Spec -> Initialiser -> State+make_initial_state spec inits = do+ case runSubs (store_unions <$> mapM eval_effect inits) spec emptyState emptyInput emptySubs of+ Left err -> error (print_runtime_error err)+ Right res -> case res of + [] -> error "failed to initialise state"+ [sto] -> rebase_and_sat spec (make_assignments sto emptyState)+ _ -> error "non-deterministic state initialisation"
+ src/Language/EFLINT/JSON.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE DeriveGeneric, DuplicateRecordFields, TupleSections #-}++module Language.EFLINT.JSON where++import Language.EFLINT.Spec hiding (FactSpec(actor))+import qualified Language.EFLINT.Spec as Spec++import Data.Aeson hiding (object)+import Data.Maybe+import Data.Char (toLower, isUpper, isSpace)+import qualified Data.Map as M++import GHC.Generics++decode_json_file :: String -> IO (Either String Spec)+decode_json_file f = fmap tModel <$> eitherDecodeFileStrict f++tExpr :: Expression -> Term+tExpr e = case e of + RefExpr v -> Ref (tVariable v) + MultiExpr m -> case (expression :: Multi -> String) m of+ "AND" -> foldr And (BoolLit True) (map tExpr (fromJust (operands m)))+ "OR" -> foldr Or (BoolLit False) (map tExpr (fromJust (operands m)))+ "NOT" -> Not (tExpr (fromJust (operand m)))+ "LIST"-> tExpr (fromJust (items m))+ cons -> error ("JSON2SPEC: unknown expression type: " ++ cons)++tAct :: Act -> (DomId, TypeSpec)+tAct a = (act a,) $ TypeSpec {+ kind = Spec.Act aspec+ , domain = Products args + , domain_constraint = BoolLit True+ , derivation = [HoldsWhen condition_term]+ , closed = True + , conditions = [] + }+ where condition_term = foldr And (BoolLit True) $ + [ tExpr (preconditions a) + , Ref (no_decoration (actor a))+ , Ref (no_decoration (interested_party a))] +++ (map Ref objects)+ args = [no_decoration (actor a), no_decoration (interested_party a)] ++ objects+ aspec = ActSpec { effects = map mkT ((terminate :: Act -> [OptBinder]) a) + ++ map mkC ((create :: Act -> [OptBinder]) a)+ , syncs = [] }+ where mkT ob = case ob of ImplicitDV expr -> tAll [] expr+ ExplicitDV b -> tAll (vars b) (binder_expression b)+ where tAll vs expr = TAll (map tVariable vs) (tExpr expr) + mkC ob = case ob of ImplicitDV expr -> cAll [] expr+ ExplicitDV b -> cAll [] (binder_expression b)+ where cAll vs expr = CAll (map tVariable vs) (tExpr expr) + objects | all isSpace (object a) = []+ | otherwise = [no_decoration (object a)]+++tDuty :: Duty -> (DomId, TypeSpec)+tDuty d = (duty d,) $ TypeSpec {+ kind = Spec.Duty dspec+ , domain = Products $ [no_decoration (duty_holder d)+ ,no_decoration (claimant d)] ++ objects+ , domain_constraint = BoolLit True+ , derivation = case (derivation :: Duty -> Maybe Binder) d of + Nothing -> [] + Just b -> [dv (duty d) (vars b) (binder_expression b)]+ , closed = True+ , conditions = []+ }+ where dspec = DutySpec {enforcing_acts = maybe [] (:[]) (enforcing d)+ ,violated_when = []}+ objects | all isSpace (duty_components d) = []+ | otherwise = [no_decoration (duty_components d)]++tFact :: Fact -> (DomId, TypeSpec)+tFact f = (fact f,) $ TypeSpec {+ kind = Spec.Fact fspec + , domain = case (domain :: Fact -> Maybe Language.EFLINT.JSON.Domain) f of + Nothing -> case function f of + ImplicitDV (RefExpr (BaseVar "[]")) -> AnyString + _ -> Products []+ Just dom -> tDomain dom+ , domain_constraint = BoolLit True+ , derivation = case function f of+ ImplicitDV expr -> case expr of + RefExpr (BaseVar "[]") -> [] --Just (Dv [] (When (App (fact f) (Right [])) (BoolLit True)))+ RefExpr (BaseVar "<<>>") -> [] + expr -> [dv (fact f) [] expr]+ ExplicitDV d -> [dv (fact f) (vars d) (binder_expression d)]+ , closed = False+ , conditions = []+ }+ where fspec = FactSpec { invariant = False, Spec.actor = False }++dv :: String -> [Variable] -> Expression -> Spec.Derivation+dv cons vars expr = Dv (map tVariable vars) (When (App cons (Right [])) (tExpr expr))++tDomain :: Language.EFLINT.JSON.Domain -> Spec.Domain+tDomain d = case type_constructor d of + "ANY-STRING" -> AnyString+ "ANY-INT" -> AnyInt+ "STRING" -> Strings (fromJust (strings d))+ "INT" -> Ints (fromJust (ints d))+ "PRODUCT" -> Products (map tVariable (fromJust (arguments d)))+ cons -> error ("unknown type-constructor: " ++ cons)++tVariable :: Variable -> Spec.Var+tVariable (BaseVar var) = Var var ""+tVariable (DecVar (DecoratedVariable x d)) = Var x d ++tModel :: Model -> Spec+tModel m = Spec { decls = M.fromList $ + map tAct (acts m) ++ + map tDuty (duties m) ++ + map tFact (facts m)+ , aliases = M.empty}++unhyphen :: String -> String+unhyphen = map op+ where op '-' = '_'+ op c = c++hyphen :: String -> String+hyphen = map op+ where op '_' = '-'+ op c = c++process_string :: String -> String+process_string = id+{-+process_string ('<':'<':s) = reverse (drop 2 (reverse (concatMap replace s)))+process_string ('<':s) = reverse (drop 1 (reverse (concatMap replace s)))+process_string ('[':s) = reverse (drop 1 (reverse (concatMap replace s)))+process_string s = s+-}++replace :: Char -> String+replace ',' = ""+replace '-' = ""+replace c | isUpper c = [toLower c]+replace c = [c]++customOptions = defaultOptions { fieldLabelModifier = hyphen, sumEncoding = UntaggedValue}++type BaseVariable = String+data Variable = BaseVar BaseVariable+ | DecVar DecoratedVariable+ deriving (Show, Generic)+instance ToJSON Variable where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Variable where+ parseJSON = genericParseJSON customOptions ++data DecoratedVariable = DecoratedVariable {+ base :: BaseVariable+ , modifier :: String+ } deriving (Show, Generic)+instance ToJSON DecoratedVariable where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON DecoratedVariable where+ parseJSON = genericParseJSON customOptions ++data Model = Model {+ acts :: [Act]+ , facts :: [Fact]+ , duties :: [Duty]+ } deriving (Show, Generic) +instance ToJSON Model where+ toEncoding = genericToEncoding (defaultOptions { constructorTagModifier = unhyphen, sumEncoding = UntaggedValue} )+instance FromJSON Model where++data Act = Act {+ act :: String+ , actor :: String+ , action :: String+ , object :: String+ , interested_party :: String+ , preconditions :: Expression + , create :: [OptBinder]+ , terminate :: [OptBinder]+ , derivation :: Maybe Binder+ , sources :: Maybe [Source]+ , explanation :: Maybe String+ , version :: Maybe String+ , reference :: Maybe References+ , juriconnect :: Maybe String+ , sourcetext :: Maybe String+ } deriving (Show, Generic)+instance ToJSON Act where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Act where+ parseJSON = genericParseJSON customOptions ++data Fact = Fact {+ fact :: String+ , function :: OptBinder+ , domain :: Maybe Language.EFLINT.JSON.Domain+ , sources :: Maybe [Source]+ , explanation :: Maybe String+ , version :: Maybe String+ , reference :: Maybe References + , juriconnect :: Maybe String+ , sourcetext :: Maybe String+ } deriving (Show, Generic)+instance ToJSON Fact where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Fact where+ parseJSON = genericParseJSON customOptions ++data Domain = Domain {+ type_constructor :: String+ , arguments :: Maybe [Variable]+ , strings :: Maybe [String]+ , ints :: Maybe [Int]+ } deriving (Show, Generic)+instance ToJSON Language.EFLINT.JSON.Domain where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Language.EFLINT.JSON.Domain where+ parseJSON = genericParseJSON customOptions ++data Duty = Duty {+ duty :: String+ , duty_components :: String+ , duty_holder :: String+ , claimant :: String+ , create :: String+ , terminate :: String+ , enforcing :: Maybe String+ , derivation :: Maybe Binder+ , sources :: Maybe [Source]+ , explanation :: Maybe String+ , version :: Maybe String+ , reference :: Maybe References+ , juriconnect :: Maybe String+ , sourcetext :: Maybe String+ } deriving (Show, Generic)+instance ToJSON Duty where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Duty where+ parseJSON = genericParseJSON customOptions ++data OptBinder = ExplicitDV Binder+ | ImplicitDV Expression + deriving (Show, Generic)+instance ToJSON OptBinder where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON OptBinder where+ parseJSON = genericParseJSON customOptions ++data Binder = Binder {+ vars :: [Variable]+ , binder_expression :: Expression+ } deriving (Show, Generic)+instance ToJSON Binder where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Binder where+ parseJSON = genericParseJSON customOptions ++data Source = Source {+ validFrom :: String+ , validTo :: Maybe String+ , citation :: String+ , juriconnect :: String+ , text :: String+ } deriving (Show, Generic)+instance ToJSON Source where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Source where+ parseJSON = genericParseJSON customOptions++data Expression = RefExpr Variable + | MultiExpr Multi + deriving (Show, Generic)+instance ToJSON Expression where+ toJSON = genericToJSON customOptions+ toEncoding = genericToEncoding customOptions +instance FromJSON Expression where+ parseJSON = genericParseJSON customOptions++data Multi = Multi {+ expression :: String+ , operands :: Maybe [Expression]+ , operand :: Maybe Expression+ , items :: Maybe Expression+ } deriving (Show, Generic)+instance ToJSON Multi where+instance FromJSON Multi where++data References = RSingle String+ | RMulti [String]+ deriving (Show, Generic)+instance ToJSON References where+ toEncoding = genericToEncoding customOptions+ toJSON = genericToJSON customOptions +instance FromJSON References where+ parseJSON = genericParseJSON customOptions
+ src/Language/EFLINT/Options.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE LambdaCase #-}++module Language.EFLINT.Options where++import Language.EFLINT.Util++import Control.Monad (when)++import System.Directory+import System.IO.Unsafe+import Data.IORef++type Options = IORef OptionsStruct++data OptionsStruct = OptionsStruct {+ include_paths :: [FilePath]+ , included_files :: [FilePath]+ , filepath :: Maybe FilePath+ , input :: [Bool] + , ignore_scenario :: Bool+ , debug :: Bool+ , accept_phrases :: Bool+ , test_mode :: Bool+ }++find :: (OptionsStruct -> a) -> Options -> a+find proj = proj . unsafePerformIO . readIORef++defaultOptionsStruct = OptionsStruct {+ include_paths = []+ , included_files = []+ , filepath = Nothing+ , input = [] + , ignore_scenario = False+ , debug = False+ , test_mode = False + , accept_phrases = False+ }++is_in_test_mode :: Options -> IO Bool+is_in_test_mode opts = test_mode <$> readIORef opts++run_options :: [String] -> IO Options+run_options args = do+ ref <- newIORef defaultOptionsStruct + run_options' args ref + return ref+ where+ run_options' [] opts = return ()+ run_options' ("--ignore-scenario":args) opts = do+ modifyIORef opts (\os -> os { ignore_scenario = True } )+ run_options' args opts + run_options' ("--debug":args) opts = do+ modifyIORef opts (\os -> os { debug = True })+ run_options' args opts + run_options' ("--test-mode":args) opts = do -- errors and failed queries only+ modifyIORef opts (\os -> os { test_mode = True })+ run_options' args opts + run_options' ("--accept-phrases":args) opts = do+ modifyIORef opts (\os -> os { accept_phrases = True })+ run_options' args opts + run_options' ("-i":(sdir:args)) opts = add_include_path sdir opts >> run_options' args opts+ run_options' (_:args) opts = run_options' args opts++add_include_path :: String -> Options -> IO () +add_include_path fp opts = doesDirectoryExist fp >>= \case+ False -> return ()+ True -> modifyIORef opts (\os -> os {include_paths = include_paths os ++ [fp] })++add_include :: String -> Options -> IO ()+add_include fp opts = doesFileExist fp >>= \case+ False -> return () + True -> modifyIORef opts (\os -> os {included_files = included_files os ++ [fp] })++has_been_included :: FilePath -> Options -> Bool+has_been_included file opts = unsafePerformIO $ do + dirs <- include_paths <$> readIORef opts+ files <- included_files <$> readIORef opts+ find_included_file dirs file >>= \case+ [] -> return False+ (file:_) -> return (file `elem` files)++add_filepath :: FilePath -> Options -> IO ()+add_filepath fp opts = do modifyIORef opts (\os -> os { filepath = Just fp })++add_input :: [String] -> Options -> IO ()+add_input ss opts = modifyIORef opts (\os -> os { input = map readAssignmentMaybe ss })++consume_input :: Options -> IO (Maybe Bool)+consume_input opts = do + optss <- readIORef opts+ case input optss of + [] -> return Nothing+ bs -> do modifyIORef opts (\os -> os { input = tail bs }) + return (Just $ head bs)++readAssignmentMaybe :: String -> Bool+readAssignmentMaybe s = case s of+ "True" -> True + "true" -> True + "t" -> True + "T" -> True + "y" -> True + "Y" -> True + "False" -> False+ "false" -> False + "f" -> False + "F" -> False + "N" -> False + "n" -> False + _ -> False++verbosity :: Options -> Int -> IO () -> IO ()+verbosity opts loc m = do + limit <- limitM <$> readIORef opts+ when (level <= limit) m+ where limitM opts | debug opts = Verbose+ | test_mode opts = TestMode+ | otherwise = Default+ level = case loc of + 0 -> Default+ 1 -> Default+ 2 -> Default+ 3 -> TestMode + 4 -> TestMode + 5 -> TestMode + 6 -> Default + 7 -> Default + 8 -> Default + 9 -> Default + 10-> Default + 11-> Default + 12-> TestMode + _ -> Default + ++data Level = TestMode | Default | Verbose deriving (Ord, Enum, Eq)
+ src/Language/EFLINT/Parse.hs view
@@ -0,0 +1,458 @@+{-# LANGUAGE TupleSections #-}++module Language.EFLINT.Parse where++import Language.EFLINT.Spec++import GLL.Combinators hiding (many, some, IntLit, BoolLit, StringLit)+import Text.Regex.Applicative hiding ((<**>), optional)++import Data.Char (isLower)+import qualified Data.Map as M++flint_lexer :: String -> Either String [Token]+flint_lexer = lexerEither lexer_settings++lexer_settings :: LexerSettings+lexer_settings = emptyLanguage {+ identifiers = types+ , keywords = ["!?","||", "&&", "<=", ">=", "..", "True", "False", "Sum", "==", "!=", "When", "Where","Holds when", "Holds", "Present when", "Present", "Max", "Min", "Count", "Union", "Enabled", "Violated when", "Violated"+ , "Atom", "String", "Int", "Time", "Current Time"+ , "Exists", "Forall", "Foreach", "Force"+ , "Extend", "Event", "Act", "Fact", "Invariant", "Predicate", "Duty", "Actor", "Holder", "Claimant", "Recipient", "Related to", "Conditioned by", "Creates", "Terminates", "Obfuscates", "Terminated by", "With" , "Identified by", "Derived from", "Derived externally", "Enforced by", "Syncs with"+ , "Do", "Placeholder", "For", "Not", "Open", "Closed" + , "#", "##", "###", "####"+ , "#include", "#require"+ ]+ , keychars = ['[', ']', '(', ')', '!', ',', '\'', '+', '-', '*', '/', '.', '=', '>', '<', ':', '?', '{', '}', '%', '~']+ } + where types = (concat .) . (:) <$> + word <*> many ((++) <$> (concat <$> some ((:[]) <$> psym (== ' '))) <*> word) <|> + (\id -> "[" ++ id ++ "]") <$ sym '[' <*> many internal <* sym ']' <|>+ (\id -> "<" ++ id ++ ">") <$ sym '<' <*> act_or_duty <* sym '>'+ where word = (\c ss -> c:concat ss) <$> psym isLower <*> many ((:[]) <$> psym isLower <|> hyphen <|> ((:[]) <$> sym '_'))+ where hyphen = (\c1 c2 -> [c1,c2]) <$> sym '-' <*> psym isLower + act_or_duty = (\id -> "<" ++ id ++ ">") <$ sym '<' <*> many internal <* sym '>'+ <|> (:) <$> psym (not . flip elem "< =") <*> many internal + internal = psym (\c -> not (c `elem` "]>+="))++value_expr :: BNF Token Term+value_expr = "value-expr"+ <::= BoolLit True <$$ keyword "True"+ <||> BoolLit False <$$ keyword "False"+ <||> When <$$> value_expr <** keyword_when <**> value_expr+ + <||> Or <$$> value_expr <** keyword "||" <<<**> value_expr+ <||> And <$$> value_expr <** keyword "&&" <<<**> value_expr++ <||> Eq <$$> value_expr <** keyword "==" <**> value_expr+ <||> Neq <$$> value_expr <** keyword "!=" <**> value_expr++ <||> Leq <$$> value_expr <** keyword "<=" <<<**> value_expr+ <||> Geq <$$> value_expr <** keyword ">=" <<<**> value_expr+ <||> Le <$$> value_expr <** keychar '<' <<<**> value_expr+ <||> Ge <$$> value_expr <** keychar '>' <<<**> value_expr+ <||> Sub <$$> value_expr <** keychar '-' <**>>> value_expr + <||> Add <$$> value_expr <** keychar '+' <**>>> value_expr + <||> Mult <$$> value_expr <** keychar '*' <**>>> value_expr + <||> Mod <$$> value_expr <** keychar '%' <**>>> value_expr + <||> Div <$$> value_expr <** keychar '/' <**>>> value_expr + <||> Not <$$ keychar '!' <**> value_expr + <||> Not <$$ keyword "Not" <**> value_expr ++ <||> keyword "Sum" **> foreach Sum+ <||> keyword "Count" **> foreach Count + <||> keyword "Max" **> foreach Max+ <||> keyword "Min" **> foreach Min++ <||> IntLit <$$> int_lit+ <||> StringLit <$$> atom + <||> Ref <$$> var + <||> application App+ <||> Project <$$> value_expr <** keychar '.' <**> (var <||> parens var)+ <||> Tag <$$> value_expr <** keychar ':' <**> id_lit ++ <||> parens (Exists <$$ keyword "Exists" <**> multipleSepBy1 var (keychar ',') <** keychar ':' <**> value_expr)+ <||> parens (Forall <$$ keyword "Forall" <**> multipleSepBy1 var (keychar ',') <** keychar ':' <**> value_expr)+ <||> Present <$$ keyword "Present" <**> value_expr+ <||> Present <$$ keyword "Holds" <**> value_expr+ <||> Violated <$$ keyword "Violated" <**> value_expr+ <||> Enabled <$$ keyword "Enabled" <**> value_expr+ <||> parens value_expr+ <||> CurrentTime <$$ keyword "Current Time"++keyword_when :: BNF Token String+keyword_when = "when-or-where" <:=> keyword "Where" <||> keyword "When"++var :: BNF Token Var+var = "decorated-type-lit"+ <:=> Var <$$> id_lit <**> decoration++atom :: BNF Token String+atom = "atom" <:=> string_lit <||> alt_id_lit++decoration :: BNF Token String +decoration = "decoration"+ <:=> make_f <$$> optional int_lit <**> multiple (keychar '\'')+ where make_f mi str = maybe "" show mi ++ str++arguments :: BNF Token Arguments +arguments = "arguments"+ <:=> parens ( Right <$$> multipleSepBy modifier (keychar ',')+ <||> Left <$$> multipleSepBy1 value_expr (keychar ',') )++modifier :: BNF Token Modifier+modifier = "modifier"+ <:=> Rename <$$> var <** keychar '=' <**> value_expr ++type_expr :: BNF Token Domain+type_expr = "type-expr"+ <::= Products . (:[]) <$$> var + <||> Strings <$$> manySepBy2 atom (keychar '+' <||> keychar ',')+ <||> Ints <$$> manySepBy2 int_lit (keychar '+' <||> keychar ',')+ <||> Products <$$> manySepBy2 var (keychar '*')+ <||> parens (Products <$$> manySepBy2 var (keychar '*'))+ <||> Ints . (:[]) <$$> int_lit+ <||> ints_from_domain <$$> int_lit <** keyword ".." <**> int_lit+ <||> Strings . (:[]) <$$> atom + <||> strings_from_domain <$$> char_lit <** keyword ".." <**> char_lit+ <||> AnyString <$$ keyword "String"+ <||> AnyString <$$ keyword "Atom"+ <||> AnyInt <$$ keyword "Int"+ <||> Time <$$ keyword "Time"+ where ints_from_domain :: Int -> Int -> Domain + ints_from_domain min max = Ints $ [min..max]++ strings_from_domain :: Char -> Char -> Domain+ strings_from_domain min max = Strings $ map (:[]) [min..max]+++-- parsing frame specifications+parse_component :: BNF Token a -> String -> Either String a+parse_component p str = case flint_lexer str of+ Left err -> Left err+ Right ts -> case parseWithOptionsAndError [maximumErrors 1] p ts of+ Left err -> Left err+ Right as -> Right (head as)++flint :: BNF Token (Spec, Refiner, Initialiser, Scenario)+flint = "flint" <:=> cons <$$ + optional (keyword "#") <**> declarations <**> + optionalWithDef (keyword "##" **> refiner) M.empty <**>+ optionalWithDef (keyword "###" **> initialiser) [] <**> + optionalWithDef (keyword "####" **> scenario) []+ where cons ds r i s = (extend_spec ds emptySpec, r, i, s)++parse_flint = parse_component flint++declarations :: BNF Token [Decl]+declarations = "declarations" <:=> multiple1 frame ++placeholder :: BNF Token Decl+placeholder = "placeholder-decl" <:=> PlaceholderDecl <$$ keyword "Placeholder" <**> id_lit <** keyword "For" <**> id_lit++frame :: BNF Token Decl+frame = "frame" <:=> fact + <||> duty + <||> act + <||> event + <||> syn_ext+ <||> placeholder + where fact = syn_fact_decl (make_fact False False)+ <||> syn_actor_decl (make_fact False True)+ <||> syn_pred_decl (make_pred False) + <||> syn_inv_decl make_inv + where make_fact inv is_actor is_closed ty dom dom_filter clauses = + TypeDecl ty $ apply_type_ext ty clauses tspec+ where tspec = TypeSpec { kind = Fact (FactSpec inv is_actor)+ , domain = dom+ , domain_constraint = dom_filter+ , derivation = []+ , closed = is_closed+ , conditions = [] }+ make_pred inv ty t = make_fact inv False True ty (Products []) (BoolLit True) [DerivationCl [HoldsWhen t]]+ make_inv ty t = make_pred True ty t++ act = syn_act_decl make_act+ where make_act is_closed ty mact mrec attrs dom_filter clauses = + TypeDecl ty $ apply_type_ext ty clauses tspec+ where tspec = TypeSpec {+ kind = Act (ActSpec {effects = [], syncs = []} ),+ domain = Products (actor:(maybe [] (:[]) mrec ++ attrs)), + domain_constraint = dom_filter,+ derivation = [],+ closed = is_closed, + conditions = [] }+ actor = maybe (no_decoration "actor") id mact++ event = syn_event_decl make_event + where make_event is_closed ty attrs dom_filter clauses =+ TypeDecl ty $ apply_type_ext ty clauses tspec+ where tspec = TypeSpec {+ kind = Event (EventSpec { event_effects = [] })+ , domain = Products attrs+ , domain_constraint = dom_filter+ , derivation = []+ , closed = is_closed+ , conditions = []+ } + + duty = syn_duty_decl make_duty + where make_duty is_closed ty hold claim attrs dom_filter clauses = + TypeDecl ty $ apply_type_ext ty clauses tspec + where tspec = TypeSpec {+ domain = Products (hold:claim:attrs),+ domain_constraint = dom_filter,+ kind = Duty (DutySpec { violated_when = [], enforcing_acts = []}), + derivation = [], + closed = is_closed, + conditions = []}++syn_fact_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a+syn_fact_decl cons = "fact-type-decl" <:=> cons <$$>+ syn_is_closed <** keyword "Fact" <**> id_lit <**>+ optionalWithDef (keyword "Identified by" **> type_expr) AnyString <**>+ syn_domain_constraint <**> + syn_fact_clauses++syn_ext :: BNF Token Decl+syn_ext = "type-ext" <:=> + keyword "Extend" **> ( syn_fact_ext + <||> syn_act_ext + <||> syn_duty_ext + <||> syn_event_ext )++syn_is_closed :: BNF Token Bool+syn_is_closed = "is-type-closed-modifier" <:=> optionalWithDef alts True+ where alts = True <$$ keyword "Closed"+ <||> False <$$ keyword "Open"++syn_fact_ext :: BNF Token Decl+syn_fact_ext = "fact-type-ext" <:=> TypeExt <$$ keyword "Fact" <**> id_lit <**> syn_fact_clauses ++syn_actor_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a+syn_actor_decl cons = "actor-type-decl" <:=> cons' <$$>+ syn_is_closed <** keyword "Actor" <**> id_lit <**> + optionalWithDef (keyword "With" **> manySepBy1 var (keychar '*')) [] <**>+ syn_domain_constraint <**> + syn_fact_clauses + where cons' isc d vars t = cons isc d (Products (Var actor_ref_address "" : vars)) t ++syn_pred_decl :: (DomId -> Term -> a) -> BNF Token a+syn_pred_decl cons = "pred-type-decl" <:=> cons <$$ + keyword "Predicate" <**> id_lit <** keyword_when <**> value_expr++syn_inv_decl :: (DomId -> Term -> a) -> BNF Token a+syn_inv_decl cons = "inv-type-decl" <:=> cons <$$+ keyword "Invariant" <**> id_lit <** keyword_when <**> value_expr ++syn_domain_constraint = optionalWithDef (keyword_when **> value_expr) (BoolLit True)++syn_duty_decl :: (Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a+syn_duty_decl cons = "duty-type-decl" <:=> cons <$$>+ syn_is_closed <** keyword "Duty" <**> id_lit <** optional (keyword "With") <**+ keyword "Holder" <**> var <**+ keyword "Claimant" <**> var <**> + objects <**> syn_domain_constraint <**>+ syn_duty_clauses ++syn_act_decl :: (Bool -> DomId -> Maybe Var -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a+syn_act_decl cons = "act-type-decl" <:=> cons <$$>+ syn_is_closed <** keyword "Act" <**> id_lit <** optional (keyword "With") <**>+ optional (keyword "Actor" **> var) <**> + optional (keyword "Recipient" **> var) <**> + objects <**> syn_domain_constraint <**> + syn_event_clauses ++syn_act_ext :: BNF Token Decl+syn_act_ext = "act-type-ext" <:=> TypeExt <$$ keyword "Act" <**> id_lit <**> syn_event_clauses ++syn_event_ext :: BNF Token Decl+syn_event_ext = "event-type-ext" <:=> TypeExt <$$ keyword "Event" <**> id_lit <**> syn_event_clauses ++syn_duty_ext :: BNF Token Decl+syn_duty_ext = "duty-type-ext" <:=> TypeExt <$$ keyword "Duty" <**> id_lit <**> syn_duty_clauses ++syn_event_decl :: (Bool -> DomId -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a+syn_event_decl cons = "event-type-decl" <:=> cons <$$>+ syn_is_closed <** keyword "Event" <**> id_lit <** optional (keyword "With") <**> + objects <**> syn_domain_constraint <**> + syn_event_clauses++syn_fact_clauses :: BNF Token [ModClause]+syn_fact_clauses = multiple syn_fact_clause+ where syn_fact_clause = "fact-clause" <:=> ConditionedByCl <$$> precondition'+ <||> DerivationCl <$$> derivation_from+ +syn_event_clauses :: BNF Token [ModClause]+syn_event_clauses = multiple syn_event_clause+ where syn_event_clause = "event-clause" <:=> ConditionedByCl <$$> precondition'+ <||> DerivationCl <$$> derivation_from+ <||> PostCondCl <$$> creating_post'+ <||> PostCondCl <$$> terminating_post'+ <||> PostCondCl <$$> obfuscating_post'+ <||> SyncCl <$$> synchronisations++syn_duty_clauses :: BNF Token [ModClause]+syn_duty_clauses = multiple syn_duty_clause+ where syn_duty_clause = "duty-clause" <:=> ConditionedByCl <$$> precondition'+ <||> DerivationCl <$$> derivation_from+ <||> ViolationCl <$$> violation_condition + <||> EnforcingActsCl <$$> enforcing_acts_clauses ++objects :: BNF Token [Var]+objects = "related-to" <:=> optionalWithDef (keyword "Related to" **> multipleSepBy1 var (keychar ',')) []++enforcing_acts_clauses :: BNF Token [DomId]+enforcing_acts_clauses = "enforcing-act-clauses"+ <:=> keyword "Enforced by" **> multipleSepBy1 id_lit (keychar ',')++violation_condition :: BNF Token [Term]+violation_condition = "violation-conditions"+ <:=> keyword "Violated when" **> multipleSepBy1 value_expr (keychar ',')++precondition :: BNF Token [Term]+precondition = "preconditions" <:=> + optionalWithDef precondition' []+precondition' = keyword "Conditioned by" **> multipleSepBy value_expr (keychar ',') ++creating_post :: BNF Token [Effect]+creating_post = "creating-postcondition" <:=> + optionalWithDef creating_post' [] +creating_post' = keyword "Creates" **> (map (uncurry CAll) <$$> multipleSepBy1 effect (keychar ','))++terminating_post :: BNF Token [Effect]+terminating_post = "terminating-postcondition" <:=>+ optionalWithDef terminating_post' []+terminating_post' = keyword "Terminates" **> (map (uncurry TAll) <$$> multipleSepBy1 effect (keychar ','))++obfuscating_post :: BNF Token [Effect]+obfuscating_post = "obfuscating-postcondition" <:=>+ optionalWithDef obfuscating_post' []+obfuscating_post' = keyword "Obfuscates" **> (map (uncurry OAll) <$$> multipleSepBy1 effect (keychar ','))+++postconditions :: BNF Token [Effect]+postconditions = "postconditions" + <:=> (++) <$$> creating_post <**> terminating_post + <||> (++) <$$> terminating_post <**> creating_post++effect :: BNF Token ([Var], Term) +effect = "effect-foreach" + <:=> ([],) <$$> value_expr + <||> foreach (,)++synchronisations :: BNF Token [Sync]+synchronisations = "synchronisations"+ <:=> keyword "Syncs with" **> multipleSepBy1 (opt_foreach Sync) (keychar ',')++application :: (DomId -> Arguments -> a) -> BNF Token a+application cons = "application" <:=> cons <$$> id_lit <**> arguments++foreach :: ([Var] -> Term -> a) -> BNF Token a+foreach cons = "foreach"+ <:=> parens (cons <$$ keyword "Foreach" <**> multipleSepBy1 var (keychar ',') + <** keychar ':' <**> value_expr )++opt_foreach :: ([Var] -> Term -> a) -> BNF Token a+opt_foreach cons = "optional-foreach"+ <:=> cons [] <$$> value_expr + <||> foreach cons++derivation_from :: BNF Token [Derivation]+derivation_from = "derivation" + <:=> keyword "Derived from" **> multipleSepBy1 term_deriv (keychar ',')+ <||> map HoldsWhen <$$ keyword_present_when <**> multipleSepBy1 value_expr (keychar ',')+ where term_deriv = "term-derivation" <:=> Dv [] <$$> value_expr <||> foreach Dv ++keyword_present_when :: BNF Token String+keyword_present_when = "present-when"+ <:=> "Holds when" <$$ keyword "Present" <** keyword "When" + <||> "Holds when" <$$ keyword "Holds" <** keyword "When" + <||> "Holds when" <$$ keyword "Present when"+ <||> keyword "Holds when"++-- parsing refiner specifications+parse_refiner :: String -> Either String Refiner+parse_refiner = parse_component refiner++refiner :: BNF Token Refiner+refiner = "refinement" <:=> M.fromList <$$> multiple refine++refine :: BNF Token (DomId, Domain)+refine = "refine" <:=> (,) <$$ keyword "Fact" <**> id_lit <** keyword "Identified by" <**> type_expr++-- parsing initial state specifications+parse_initialiser :: String -> Either String Initialiser+parse_initialiser = parse_component initialiser ++initialiser :: BNF Token Initialiser+initialiser = "initial state" <:=> multiple (initial <** keychar '.') + where initial = "initial-statement" + <:=> foreach CAll+ <||> CAll [] <$$> value_expr++-- parsing scenario specifications+parse_scenario :: String -> Either String Scenario+parse_scenario = parse_component scenario+ +scenario :: BNF Token Scenario+scenario = "scenario" <:=> multiple statement+++parse_statement :: String -> Either String Statement+parse_statement = parse_component statement++statement :: BNF Token Statement+statement = "statement"+ <:=> ($) <$$> actioner <**> maybe_action <** keychar '.'+ <||> Query <$$ keychar '?' <**> value_expr <** keychar '.'+ <||> Query . Not <$$ keyword "!?" <**> value_expr <** keychar '.'+ where actioner = "actioner" + <:=> (\(xs, d, ms) -> Trans xs Trigger (Right (d,ms))) <$$ optional (keychar '!')+ <||> (\(xs, d, ms) -> Trans xs AddEvent (Right (d,ms))) <$$ keychar '+' + <||> (\(xs, d, ms) -> Trans xs RemEvent (Right (d,ms))) <$$ keychar '-'+ maybe_action = "action-statement" + <:=> application ([],,)+ <||> parens ((\xs (d,args) -> (xs,d,args)) <$$ keyword "Foreach" <**> (multipleSepBy1 var (keychar ',')) <** keychar ':' <**> application (,))+ +statement_phrase :: BNF Token Phrase +statement_phrase = "statement-phrase"+ <:=> ($) <$$> actioner <**> maybe_action <** keychar '.'+ <||> PQuery <$$ keychar '?' <**> value_expr <** keychar '.'+ <||> PQuery . Not <$$ keyword "!?" <**> value_expr <** keychar '.'+ where actioner = "actioner" + <:=> (\(xs, d, ms) -> PTrigger xs (App d ms)) <$$ optional (keychar '!')+ <||> (\(xs, d, ms) -> Create xs (App d ms)) <$$ keychar '+' + <||> (\(xs, d, ms) -> Terminate xs (App d ms)) <$$ keychar '-'+ maybe_action = "action-statement" + <:=> application ([],,)+ <||> parens ((\xs (d,args) -> (xs,d,args)) <$$ keyword "Foreach" <**> (multipleSepBy1 var (keychar ',')) <** keychar ':' <**> application (,))+ +phrase_scenario :: BNF Token [Phrase]+phrase_scenario = "phrase-scenario" <:=> multiple (syn_phrase <** keychar '.')++syn_directives_phrases :: BNF Token [Either Directive Phrase]+syn_directives_phrases = "opt.directives.phrases" <:=> optionalWithDef + (someSepBy1 (Left <$$> syn_directive <||> Right <$$> syn_phrase) (keychar '.') + <** optional (keychar '.')) [] ++syn_directive :: BNF Token Directive+syn_directive = "directive" <:=> + Include <$$ keyword "#include" <**> string_lit+ <||> Require <$$ keyword "#require" <**> string_lit++syn_phrases :: BNF Token [Phrase]+syn_phrases = "opt.phrase" <:=> optionalWithDef + (someSepBy1 syn_phrase (keychar '.') <** optional (keychar '.')) []+ +syn_phrase :: BNF Token Phrase+syn_phrase = "phrase"+ <:=> optional (keychar '!') **> opt_foreach PTrigger + <||> keychar '+' **> opt_foreach Create + <||> keychar '-' **> opt_foreach Terminate+ <||> keychar '~' **> opt_foreach Obfuscate + <||> PQuery <$$ keychar '?' <**> value_expr + <||> PQuery . Not <$$ keyword "!?" <**> value_expr + <||> PDeclBlock <$$> declarations +
+ src/Language/EFLINT/Print.hs view
@@ -0,0 +1,245 @@+module Language.EFLINT.Print where++import Prelude hiding (seq)++import Language.EFLINT.Spec+import Language.EFLINT.Interpreter (Program(..))++import Data.List (intercalate, intersperse)++ppProgram :: Program -> String+ppProgram p = case p of+ Program p -> ppPhrase p + PSeq p1 p2 -> ppProgram p1 ++ "\n" ++ ppProgram p2+ ProgramSkip -> ""++ppPhrase :: Phrase -> String+ppPhrase p = case p of+ PQuery t -> "?" ++ ppTerm t+ PDo t -> ppTagged t+ PTrigger vs t -> foreach vs $ ppTerm t+ Create vs t -> "+" ++ foreach vs (ppTerm t)+ Terminate vs t -> "-" ++ foreach vs (ppTerm t)+ Obfuscate vs t -> "~" ++ foreach vs (ppTerm t)+ PSkip -> ""+ PDeclBlock ds -> unlines (map ppDecl ds)++ppCPhrase :: CPhrase -> String+ppCPhrase p = case p of + CPSkip -> ""+ CPOnlyDecls -> ""+ CSeq CPSkip p2 -> ppCPhrase p2+ CSeq p1 CPSkip -> ppCPhrase p1+ CSeq p1 p2 -> seq [ppCPhrase p1,ppCPhrase p2]+ CDo te -> ppTagged te+ CTrigger vs t -> foreach vs $ ppTerm t+ CCreate vs t -> "+" ++ foreach vs (ppTerm t)+ CTerminate vs t -> "-" ++ foreach vs (ppTerm t)+ CObfuscate vs t -> "~" ++ foreach vs (ppTerm t)+ CQuery t -> "?" ++ ppTerm t+ CPDir dir -> case dir of+ DirInv ty -> "Invariant " ++ ty ++ppDecl :: Decl -> String+ppDecl td = case td of + PlaceholderDecl f t -> ppPlaceholder f t+ TypeExt ty clauses -> ppTypeExt ty clauses+ TypeDecl ty tspec -> ppDeclSpec ty tspec++ppTypeExt :: DomId -> [ModClause] -> String+ppTypeExt ty clauses = "Type extension of " ++ ty -- TODO, requires knowing kind of extended type++ppDeclSpec :: DomId -> TypeSpec -> String+ppDeclSpec d tspec = case kind tspec of+ Fact fspec -> ppFact d tspec fspec+ Duty dspec -> ppDuty d tspec dspec+ Event espec -> ppEvent d tspec espec+ Act aspec -> ppAct d tspec aspec++ppDirective :: Directive -> String+ppDirective (Include fp) = "#include" ++ show fp+ppDirective (Require fp) = "#require" ++ show fp++ppClauses :: [ModClause] -> String+ppClauses = unwords . intersperse " " . concatMap ppClause++ppClause :: ModClause -> [String]+ppClause clause = case clause of+ ConditionedByCl pres | not (null pres) -> [ppPreConditions pres]+ DerivationCl dvs | not (null dvs) -> [ppDerivRules dvs]+ SyncCl ss | not (null ss) -> [] -- TODO+ PostCondCl effs | not (null effs) -> [ppPostConditions effs]+ ViolationCl vcs | not (null vcs) -> [ppViolationConds vcs] + EnforcingActsCl ds | not (null ds) -> [ppEnforcingActs ds] + _ -> []++ppAct d tspec aspec = ppAct' d (domain tspec) (domain_constraint tspec) + [DerivationCl (derivation tspec) + ,ConditionedByCl (conditions tspec)+ ,PostCondCl (effects aspec)+ ,SyncCl (syncs aspec)+ ]++-- TODO print syncs(?)+ppAct' domainID domain domain_constr clauses = + "Act " ++ domainID ++ " Actor " ++ ppVar actor ++ " Recipient " ++ ppVar recipient ++ show_objects+ ++ ppConstraint (domain_constr)+ ++ ppClauses clauses+ where Products (actor:recipient:objects) = domain+ show_objects | null objects = ""+ | otherwise = " Related to " ++ intercalate ", " (map (\(Var x dec) -> x++dec) objects)++ppPostConditions :: [Effect] -> String+ppPostConditions effects = created_facts ++ terminated_facts ++ obfuscated_facts+ where (createds, terminateds, obfs) = foldr op ([],[],[]) effects+ where op e@(CAll _ _) (cs,ts,os) = (e:cs,ts,os) + op e@(TAll _ _) (cs,ts,os) = (cs,e:ts,os)+ op e@(OAll _ _) (cs,ts,os) = (cs,ts,e:os)+ created_facts | null createds = ""+ | otherwise = " Creates " ++ intercalate ", " (map ppEffect createds)+ terminated_facts | null terminateds = ""+ | otherwise = " Terminates " ++ intercalate ", " (map ppEffect terminateds)+ obfuscated_facts | null obfs = ""+ | otherwise = " Obfuscates " ++ intercalate ", " (map ppEffect obfs)++ppPreConditions :: [Term] -> String+ppPreConditions [] = ""+ppPreConditions ts = " Conditioned by " ++ intercalate ", " (map ppTerm ts)++ppEvent d tspec espec = ppEvent' d (domain tspec) (domain_constraint tspec)+ [DerivationCl (derivation tspec)+ ,ConditionedByCl (conditions tspec) + ,PostCondCl (event_effects espec)]++ppEvent' domainID domain domain_constr clauses =+ "Event " ++ domainID ++ show_objects+ ++ ppConstraint domain_constr+ ++ ppClauses clauses+ where Products objects = domain+ show_objects | null objects = ""+ | otherwise = " Related to " ++ intercalate ", " (map (\(Var x dec) -> x++dec) objects)++ppEffect (CAll vs t) = foreach vs (ppTerm t)+ppEffect (TAll vs t) = foreach vs (ppTerm t)+ppEffect (OAll vs t) = foreach vs (ppTerm t)++ppFact :: DomId -> TypeSpec -> FactSpec -> String+ppFact d tspec fspec = + "Fact " ++ d ++ " Identified by " ++ ppDom (domain tspec) (domain_constraint tspec) + ++ ppPreConditions (conditions tspec)+ ++ ppDerivRules (derivation tspec)++ppDerivRules deriv = case deriv of + [] -> "" + holds | all isHolds holds -> "\n Holds when " ++ intercalate ", " (map ppTerm ts)+ where isHolds (HoldsWhen _) = True+ isHolds _ = False+ ts = concatMap op holds+ where op (HoldsWhen t) = [t]+ op _ = []+ ts -> "\n Derived from " ++ intercalate ", " (map ppDeriv ts)++ppDuty d tspec dspec = ppDuty' d (domain tspec) (domain_constraint tspec)+ [DerivationCl (derivation tspec)+ ,ConditionedByCl (conditions tspec)+ ,ViolationCl (violated_when dspec)]++ppDuty' domainID domain domain_constr clauses = + "Duty " ++ domainID ++ " Holder " ++ ppVar holder ++ " Claimant " ++ ppVar claimant ++ show_objects+ ++ ppConstraint domain_constr+ ++ ppClauses clauses+ where Products (holder:claimant:objects) = domain+ show_objects | null objects = ""+ | otherwise = " Related to " ++ intercalate ", " (map (\(Var x dec) -> x++dec) objects)++ppViolationConds :: [Term] -> String+ppViolationConds ts | null ts = ""+ | otherwise = "\n Violated when " ++ intercalate ", " (map ppTerm ts)++ppEnforcingActs :: [DomId] -> String+ppEnforcingActs ds | null ds = ""+ | otherwise = "\n Enforced by " ++ intercalate ", " ds++ppDeriv :: Derivation -> String+ppDeriv (HoldsWhen a) = "<HOLDS WHEN>"+ppDeriv (Dv xs t) = foreach xs (ppTerm t) ++ppDom :: Domain -> Term -> String+ppDom dom c = types ++ ppConstraint c+ where types = case dom of+ Strings ss -> intercalate ", " ss+ Ints is -> intercalate ", " (map show is)+ AnyString -> "String"+ AnyInt -> "Int"+ -- Products rs -> intercalate " * " (map show rs)+ Products rs -> intercalate " * " (map ppVar rs)+ Time -> "<TIME>"++ppConstraint c = case c of BoolLit True -> ""+ (Exists [] (BoolLit True)) -> ""+ _ -> " Where " ++ ppTerm c++ppTerm :: Term -> String+ppTerm t = case t of+ Not t -> app "Not" [ppTerm t]+ And t1 t2 -> app_infix "&&" (ppTerm t1) (ppTerm t2)+ Or t1 t2 -> app_infix "||" (ppTerm t1) (ppTerm t2)+ BoolLit b -> show b+ Leq t1 t2 -> app_infix "<=" (ppTerm t1) (ppTerm t2)+ Geq t1 t2 -> app_infix ">=" (ppTerm t1) (ppTerm t2)+ Ge t1 t2 -> app_infix ">" (ppTerm t1) (ppTerm t2)+ Le t1 t2 -> app_infix "<" (ppTerm t1) (ppTerm t2)+ Sub t1 t2 -> app_infix "-" (ppTerm t1) (ppTerm t2)+ Add t1 t2 -> app_infix "+" (ppTerm t1) (ppTerm t2)+ Mult t1 t2 -> app_infix "*" (ppTerm t1) (ppTerm t2)+ Mod t1 t2 -> app_infix "%" (ppTerm t1) (ppTerm t2)+ Div t1 t2 -> app_infix "/" (ppTerm t1) (ppTerm t2)+ IntLit i -> show i+ StringLit s -> show s+ Eq t1 t2 -> app_infix "==" (ppTerm t1) (ppTerm t2)+ Neq t1 t2 -> app_infix "!=" (ppTerm t1) (ppTerm t2)+ Exists vs t -> exists vs (ppTerm t)+ Forall vs t -> forall vs (ppTerm t)+ Count vs t -> "Count" ++ foreach vs (ppTerm t)+ Sum vs t -> "Sum" ++ foreach vs (ppTerm t)+ Max vs t -> "Max" ++ foreach vs (ppTerm t)+ Min vs t -> "Min" ++ foreach vs (ppTerm t)+ When t1 t2 -> app_infix "When" (ppTerm t1) (ppTerm t2)+ Present t -> app "Holds" [ppTerm t]+ Violated t -> app "Violated" [ppTerm t] + Enabled t -> app "Enabled" [ppTerm t] + Project t v -> app "" [ppTerm t] ++ "." ++ ppVar v+ Tag t d -> app d [ppTerm t]+ Untag t -> app "Untag" [ppTerm t]+ Ref v -> ppVar v+ App d args -> case args of+ Left ts -> app d $ map ppTerm ts+ Right ms -> app d $ map ppMod ms+ CurrentTime -> "<TIME>"++ppVar :: Var -> String+ppVar (Var x dec) = x ++ dec++ppMod :: Modifier -> String+ppMod (Rename v t) = ppVar v ++ "=" ++ ppTerm t ++ppPlaceholder :: DomId -> DomId -> String+ppPlaceholder var for = "Placeholder " ++ var ++ " For " ++ for++seq :: [String] -> String+seq = intercalate ".\n" ++foreach = binder "Foreach"+exists = binder "Exists"+forall = binder "Forall"+count = binder "Count"++binder :: String -> [Var] -> String -> String+binder op [] str = str+binder op vs str = "(" ++ op ++ " " ++ intercalate "," (map ppVar vs) ++ ": " ++ str ++ ")"++app :: String -> [String] -> String+app cons args = cons ++ "(" ++ intercalate "," args ++ ")"++app_infix :: String -> String -> String -> String+app_infix op x y = x ++ " " ++ op ++ " " ++ y
+ src/Language/EFLINT/Saturation.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE LambdaCase #-}++module Language.EFLINT.Saturation (rebase_and_sat) where++import Language.EFLINT.Spec+import Language.EFLINT.State+import Language.EFLINT.Eval++import Control.Monad (forM)+import Control.Applicative (empty)++import qualified Data.Map as M+import qualified Data.Set as S++rebase_and_sat spec = saturate spec . rebase spec++rebase :: Spec -> State -> State+rebase spec s = s { contents = M.filterWithKey op (contents s) }+ where op (_,d) i = not (from_sat i)++saturate :: Spec -> State -> State+saturate spec state = case saturate' spec state of+ state' | state == state' -> state+ | otherwise -> saturate spec state'+ where + saturate' spec s = foldl op s (S.toList (derived spec))+ where op s d = case find_decl spec d of + Nothing -> s+ Just tdecl -> foldl clause s (derivation tdecl) + where clause s (HoldsWhen t) + | Products xs <- domain tdecl = derive xs (When (App d $ Right []) t) s+ | otherwise = derive [no_decoration d] (When (Ref $ no_decoration d) t) s+ clause s (Dv xs t) = derive xs t s+ where derive xs t s = let dyn = do tes <- foreach xs (whenTagged (eval t) return) + forM tes $ \te -> sat_conditions te >>= \case+ True -> return te+ False -> empty+ ress = case runSubs dyn spec s M.empty M.empty of+ Left err -> [] --error ("saturation error:\n" ++ show err)+ Right x -> x+ in derive_all (concat ress) s
+ src/Language/EFLINT/Spec.hs view
@@ -0,0 +1,508 @@+{-# LANGUAGE OverloadedStrings #-}++module Language.EFLINT.Spec where++import Data.Foldable (asum)+import Data.List (intercalate)+import qualified Data.Map as M+import qualified Data.Set as S++import Data.Aeson hiding (String)+import qualified Data.Aeson as JSON++type DomId = String -- type identifiers+type Tagged = (Elem, DomId)++data Var = Var DomId String {- decoration -}+ deriving (Ord, Eq, Show, Read)++data Elem = String String + | Int Int+ | Product [Tagged]+ deriving (Ord, Eq, Show, Read)++data Domain = AnyString+ | AnyInt+ | Strings [String]+ | Ints [Int]+ | Products [Var]+ | Time+ deriving (Ord, Eq, Show, Read)++enumerable :: Spec -> Domain -> Bool+enumerable spec d = case d of+ Strings _ -> True+ Ints _ -> True+ Products vars -> all (enumerable_var spec) vars+ AnyString -> False+ AnyInt -> False+ Time -> False+ where enumerable_var :: Spec -> Var -> Bool+ enumerable_var spec v = case fmap domain (find_decl spec (remove_decoration spec v)) of+ Nothing -> False+ Just dom -> enumerable spec dom++closed_type :: Spec -> DomId -> Maybe Bool+closed_type spec d = fmap closed (find_decl spec d)++type Arguments = Either [Term] [Modifier]++data Modifier = Rename Var Term -- with var instantiated instead as the value of expr+ deriving (Ord, Eq, Show, Read)++data Kind = Fact FactSpec | Act ActSpec | Duty DutySpec | Event EventSpec+ deriving (Ord, Eq, Show, Read)++data TypeSpec = TypeSpec {+ kind :: Kind+ , domain :: Domain+ , domain_constraint :: Term+ , derivation :: [Derivation]+ , closed :: Bool {- whether closed world assumption is made for this type -}+ , conditions :: [Term]+ } deriving (Eq, Show, Read)++data Derivation = Dv [Var] Term+ | HoldsWhen Term+ deriving (Ord, Eq, Show, Read)++data FactSpec = FactSpec {+ invariant :: Bool -- TODO move to outer AST+ , actor :: Bool+ }+ deriving (Ord, Eq, Show, Read)++data DutySpec = DutySpec {+ enforcing_acts :: [DomId] --TODO consider moving to outer ast+ , violated_when :: [Term] + }+ deriving (Ord, Eq, Show, Read)++data ActSpec = ActSpec {+ effects :: [Effect]+ , syncs :: [Sync] + }+ deriving (Ord, Eq, Show, Read)++data Effect = CAll [Var] Term+ | TAll [Var] Term+ | OAll [Var] Term+ deriving (Ord, Eq, Show, Read)++data Sync = Sync [Var] Term+ deriving (Ord, Eq, Show, Read)++data EventSpec = EventSpec { + event_effects :: [Effect] + }+ deriving (Ord, Eq, Show, Read)++data Spec = Spec {+ decls :: M.Map DomId TypeSpec+ , aliases :: M.Map DomId DomId+ }+ deriving (Eq, Show, Read)++-- | Union of specifications with overrides/replacements, not concretizations+spec_union :: Spec -> Spec -> Spec+spec_union old_spec new_spec = + Spec {decls = decls_union (decls old_spec) (decls new_spec)+ ,aliases = aliases_union (aliases old_spec) (aliases new_spec)+ }++-- | Right-based union over type declarations, only replacement, no concretization+decls_union :: M.Map DomId TypeSpec -> M.Map DomId TypeSpec -> M.Map DomId TypeSpec+decls_union old new = M.union new old++aliases_union :: M.Map DomId DomId -> M.Map DomId DomId -> M.Map DomId DomId+aliases_union old new = M.union new old++actor_ref_address :: String+actor_ref_address = "ref"++emptySpec :: Spec+emptySpec = Spec { decls = built_in_decls, aliases = M.empty}+ where built_in_decls = M.fromList [+ ("int", int_decl)+ , (actor_ref_address, string_decl) -- used for actor identifiers+ , ("actor", actor_decl)+ ]+basic :: Spec -> S.Set DomId +basic spec = M.foldrWithKey op S.empty (decls spec)+ where op d tspec res | null (derivation tspec) = S.insert d res+ | otherwise = res ++derived :: Spec -> S.Set DomId +derived spec = M.foldrWithKey op S.empty (decls spec)+ where op d tspec res | null (derivation tspec) = res + | otherwise = S.insert d res++-- type-environment pairs, restricting either:+-- * the components of the initial state (all instantiations of <TYPE> restricted by <ENV>)+-- (can be thought of as the Genesis transition, constructing the Garden of Eden)+-- * the possible actions performed in a state, only the actions <TYPE> are enabled +-- if they are consistent with <ENV>+type Initialiser= [Effect] ++emptyInitialiser :: Initialiser+emptyInitialiser = []++data Statement = Trans [Var] TransType (Either Term (DomId, Arguments)) -- foreach-application that should evaluate to exactly one act+ | Query Term++data TransType = Trigger | AddEvent | RemEvent | ObfEvent+ deriving (Ord, Eq, Enum)++type Scenario = [Statement]++data Directive = Include FilePath+ | Require FilePath++data Phrase = PDo Tagged+ | PTrigger [Var] Term+ | Create [Var] Term+ | Terminate [Var] Term+ | Obfuscate [Var] Term+ | PQuery Term+ | PDeclBlock [Decl]+ | PSkip+ deriving (Eq, Show, Read)++data Decl = TypeDecl DomId TypeSpec+ | TypeExt DomId [ModClause]+ | PlaceholderDecl DomId DomId + deriving (Eq, Show, Read)++introducesName :: Decl -> Bool+introducesName (TypeDecl _ _) = True+introducesName (TypeExt _ _) = False+introducesName (PlaceholderDecl _ _) = True++extend_spec :: [Decl] -> Spec -> Spec+extend_spec = flip (foldr op)+ where op (TypeDecl ty tyspec) spec = spec { decls = M.insert ty tyspec (decls spec) }+ op (PlaceholderDecl f t) spec = spec { aliases = M.insert f t (aliases spec) }+ op _ spec = spec++data ModClause = ConditionedByCl [Term]+ | DerivationCl [Derivation]+ | PostCondCl [Effect]+ | SyncCl [Sync]+ | ViolationCl [Term]+ | EnforcingActsCl [DomId]+ deriving (Eq, Show, Read)++apply_ext :: DomId -> [ModClause] -> Spec -> Spec+apply_ext ty clauses spec = case find_decl spec ty of+ Nothing -> spec+ Just tspec -> spec { decls = M.insert ty (apply_type_ext ty clauses tspec) (decls spec) }+ +apply_type_ext :: DomId -> [ModClause] -> TypeSpec -> TypeSpec+apply_type_ext ty clauses tspec = foldr apply_clause tspec clauses + where apply_clause clause tspec = case clause of + ConditionedByCl conds -> tspec { conditions = conds ++ conditions tspec }+ DerivationCl dvs -> tspec { derivation = dvs ++ derivation tspec }+ PostCondCl effs -> tspec { kind = add_effects (kind tspec) }+ where add_effects (Act aspec) = Act (aspec { effects = effs ++ effects aspec})+ add_effects (Event espec)= Event (espec { event_effects = effs ++ event_effects espec })+ add_effects s = s+ SyncCl ss -> tspec { kind = add_syncs (kind tspec) }+ where add_syncs (Act aspec) = Act $ aspec { syncs = ss ++ syncs aspec} + add_syncs s = s+ ViolationCl vs -> tspec { kind = add_viol_conds (kind tspec) }+ where add_viol_conds (Duty dspec) = Duty $ dspec { violated_when = vs ++ violated_when dspec }+ add_viol_conds s = s+ EnforcingActsCl ds -> tspec { kind = add_enf_acts (kind tspec) }+ where add_enf_acts (Duty dspec) = Duty $ dspec { enforcing_acts = ds ++ enforcing_acts dspec }+ add_enf_acts s = s++data CPhrase = CDo Tagged -- execute computed instance+ | CTrigger [Var] Term -- execute instance to be computed+ | CCreate [Var] Term+ | CTerminate [Var] Term+ | CObfuscate [Var] Term+ | CQuery Term+ | CPOnlyDecls+ | CPDir CDirective+ | CSeq CPhrase CPhrase+ | CPSkip++data CDirective = DirInv DomId++process_directives :: [CDirective] -> Spec -> Spec+process_directives = flip (foldr op)+ where op (DirInv ty) spec = spec { decls = M.adjust mod ty (decls spec) }+ where mod tspec = case kind tspec of + Fact fspec -> tspec { kind = Fact (fspec {invariant = True}) }+ _ -> tspec+++invariants :: Spec -> S.Set DomId+invariants spec = foldr op S.empty (M.assocs (decls spec))+ where op (ty,tspec) acc = case kind tspec of+ Fact fspec | invariant fspec -> S.insert ty acc+ _ -> acc++actors :: Spec -> S.Set DomId+actors spec = foldr op S.empty (M.assocs (decls spec))+ where op (ty,tspec) acc = case kind tspec of+ Fact fspec | actor fspec -> S.insert ty acc+ _ -> acc++type Subs = M.Map Var Tagged++data Term = Not Term+ | And Term Term+ | Or Term Term+ | BoolLit Bool++ | Leq Term Term+ | Geq Term Term+ | Ge Term Term+ | Le Term Term++ | Sub Term Term+ | Add Term Term+ | Mult Term Term+ | Mod Term Term+ | Div Term Term+ | IntLit Int++ | StringLit String++ | Eq Term Term+ | Neq Term Term++ | Exists [Var] Term+ | Forall [Var] Term+ | Count [Var] Term+ | Sum [Var] Term + | Max [Var] Term+ | Min [Var] Term+ | When Term Term + | Present Term+ | Violated Term+ | Enabled Term+ | Project Term Var++ | Tag Term DomId -- should perhaps not be exposed to the user, auxiliary+ | Untag Term -- auxiliary+ | Ref Var+ | App DomId Arguments + | CurrentTime+ deriving (Show, Ord, Eq, Read)++data Value = ResBool Bool+ | ResString String+ | ResInt Int+ | ResTagged Tagged+ deriving (Eq, Show)++data Type = TyStrings+ | TyInts+ | TyBool+ | TyTagged DomId+ deriving (Eq, Show)++instance Show TransType where+ show Trigger = ""+ show AddEvent = "+"+ show RemEvent = "-"+ show ObfEvent = "~"++-- instance Show Elem where+-- show v = case v of+-- String s -> show s+-- Int i -> show i+-- Product cs -> "(" ++ intercalate "," (map show_component cs) ++ ")"++-- instance Show Domain where+-- show r = case r of+-- Time -> "<TIME>"+-- AnyString -> "<STRING>" +-- Strings ss -> "<STRING:" ++ intercalate "," (map show ss) ++ ">"+-- AnyInt -> "<INT>"+-- Ints is -> "<INT:" ++ intercalate "," (map show is) ++ ">"+-- Products rs -> "(" ++ intercalate " * " (map show rs) ++ ")"++-- instance Show Modifier where+-- show (Rename dt1 dt2) = show dt1 ++ " = " ++ show dt2++-- instance Show Var where+-- show (Var ty dec) = ty ++ dec++no_decoration :: DomId -> Var+no_decoration ty = Var ty "" ++remove_decoration :: Spec -> Var -> DomId+remove_decoration spec (Var dom _) = chase_alias spec dom ++duty_decls :: Spec -> [(DomId, DutySpec)]+duty_decls spec = concatMap op $ M.assocs (decls spec)+ where op (d,tspec) = case kind tspec of + Duty ds -> [(d,ds)]+ _ -> []++trigger_decls :: Spec -> [(DomId, Either EventSpec ActSpec)]+trigger_decls spec = concatMap op $ M.assocs (decls spec)+ where op (d,tspec) = case kind tspec of + Event e -> [(d,Left e)]+ Act a -> [(d,Right a)]+ _ -> []++triggerable :: Spec -> DomId -> Bool+triggerable spec d = case fmap kind (find_decl spec d) of+ Nothing -> False+ Just (Act _) -> True+ Just (Event _) -> True + Just _ -> False++find_decl :: Spec -> DomId -> Maybe TypeSpec+find_decl spec d = M.lookup (chase_alias spec d) (decls spec)++find_violation_cond :: Spec -> DomId -> Maybe [Term]+find_violation_cond spec d = case M.lookup (chase_alias spec d) (decls spec) of+ Nothing -> Nothing + Just ts -> case kind ts of + Duty ds -> Just $ violated_when ds+ _ -> Nothing ++chase_alias :: Spec -> DomId -> DomId+chase_alias spec d = chase_alias' S.empty d+ where chase_alias' tried d + | d `S.member` tried = d+ | otherwise = maybe d (chase_alias' (S.insert d tried)) (M.lookup d (aliases spec))++show_arguments :: Arguments -> String+show_arguments (Right mods) = show_modifiers mods+show_arguments (Left xs) = "(" ++ intercalate "," (map show xs) ++ ")"++show_modifiers :: [Modifier] -> String+show_modifiers [] = "()"+show_modifiers cs = "(" ++ intercalate "," (map show cs) ++ ")"++show_projections :: [Var] -> String+show_projections [] = ""+show_projections ds = "[" ++ intercalate "," (map show ds) ++ "]"++show_component :: Tagged -> String+show_component = ppTagged ++ppTagged :: Tagged -> String+ppTagged (v,t) = case v of + String s -> t ++ "(" ++ show s ++ ")"+ Int i -> t ++ "(" ++ show i ++ ")"+ Product tes -> t ++ "(" ++ intercalate "," (map ppTagged tes) ++ ")"+++show_stmt :: Statement -> String+show_stmt (Query t) = "?" ++ show t +show_stmt (Trans xs atype etm) = case xs of + [] -> case etm of Left t -> show atype ++ show t+ Right (d,mods) -> show atype ++ d ++ show_arguments mods + _ -> "(" ++ "Foreach " ++ intercalate "," (map show xs) ++ " : " ++ show_stmt (Trans [] atype etm) ++ ")"++valOf :: Tagged -> Elem+valOf (c,t) = c++tagOf :: Tagged -> DomId+tagOf (c,t) = t++substitutions_of :: [Modifier] -> [(Var, Term)]+substitutions_of = map (\(Rename x y) -> (x,y)) ++make_substitutions_of :: [Var] -> Arguments -> [(Var, Term)] +make_substitutions_of _ (Right mods) = substitutions_of mods+make_substitutions_of xs (Left args) = zip xs args++project :: Tagged -> DomId -> Maybe Tagged+project (Product tvs,_) ty = asum (map try tvs)+ where try tv@(v,ty') | ty == ty' = Just tv+ try _ = Nothing+project _ _ = Nothing++-- environments++emptySubs :: Subs+emptySubs = M.empty++-- | right-biased+subsUnion :: Subs -> Subs -> Subs+subsUnion = flip M.union++subsUnions :: [Subs] -> Subs+subsUnions = foldr subsUnion M.empty++{-+subsUnify :: Subs -> Subs -> Bool +subsUnify e1 = M.foldrWithKey op True + where op k v res | Just v' <- M.lookup k e1, v /= v' = False+ | otherwise = res+-}++-- functions related to partial instantiation (refinement)++type Refiner = M.Map DomId Domain++emptyRefiner :: Refiner+emptyRefiner = M.empty++refine_specification :: Spec -> Refiner -> Spec+refine_specification spec rm = + spec { decls = M.foldrWithKey reinserter (decls spec) (decls spec) }+ where reinserter k tspec sm' = case M.lookup k rm of + Nothing -> sm'+ Just d -> case (d, domain tspec) of + (Strings ss, AnyString) -> sm''+ (Strings ss, Strings ss') + | all (`elem` ss') ss -> sm''+ (Ints is, AnyInt) -> sm''+ (Ints is, Ints is')+ | all (`elem` is') is -> sm''+ _ -> sm'+ where sm'' = M.insert k (tspec {domain = d}) sm'++actor_decl :: TypeSpec+actor_decl = TypeSpec { kind = Fact (FactSpec False True)+ , domain = AnyString + , domain_constraint = BoolLit True+ , derivation = [] + , conditions = []+ , closed = True+ }++int_decl :: TypeSpec+int_decl = TypeSpec { kind = Fact (FactSpec False False) + , domain = AnyInt+ , domain_constraint = BoolLit True+ , derivation = []+ , closed = True + , conditions = [] } ++ints_decl :: [Int] -> TypeSpec+ints_decl is = int_decl { domain = Ints is } ++string_decl :: TypeSpec+string_decl = TypeSpec { kind = Fact (FactSpec False False)+ , domain = AnyString+ , domain_constraint = BoolLit True+ , derivation = [] + , closed = True + , conditions = [] }++strings_decl :: [String] -> TypeSpec+strings_decl ss = + TypeSpec { kind = Fact (FactSpec False False)+ , domain = Strings ss+ , domain_constraint = BoolLit True+ , derivation = [] + , closed = True + , conditions = [] }++newtype TaggedJSON = TaggedJSON Tagged++instance ToJSON TaggedJSON where+ toJSON (TaggedJSON te@(v,d)) = case v of + String s -> object [ "tagged-type" .= JSON.String "string", "fact-type" .= toJSON d, "value" .= toJSON s, "textual" .= toJSON (ppTagged te) ]+ Int i -> object [ "tagged-type" .= JSON.String "int", "fact-type" .= toJSON d, "value" .= toJSON i, "textual" .= toJSON (ppTagged te) ]+ Product tes -> object [ "tagged-type" .= JSON.String "product", "fact-type" .= toJSON d, "arguments" .= toJSON (map TaggedJSON tes), "textual" .= toJSON (ppTagged te) ]
+ src/Language/EFLINT/State.hs view
@@ -0,0 +1,188 @@+module Language.EFLINT.State where++import Language.EFLINT.Spec++import Data.Maybe (isJust)+import qualified Data.Map as M++import Control.Applicative (empty)++data Info = Info {+ value :: Bool+ , from_sat :: Bool -- whether assignment came from saturation process+ }+ deriving (Eq, Read, Show)++data State = State {+ contents :: M.Map Tagged Info -- meta-info about components+ , time :: Int+ }+ deriving Eq++data Transition = Transition {+ tagged :: Tagged+ , exist :: Bool+ } + deriving (Ord, Eq, Show, Read)++type InputMap = M.Map Tagged Bool++type Store = M.Map Tagged Assignment ++data Assignment = HoldsTrue+ | HoldsFalse+ | Unknown+ deriving (Eq, Ord, Show, Read)++emptyInput :: InputMap+emptyInput = M.empty++emptyStore = M.empty++-- | based union over stores, precedence HoldsTrue > HoldsFalse > Unknown+store_union :: Store -> Store -> Store+store_union = M.unionWith op+ where op HoldsTrue _ = HoldsTrue+ op _ HoldsTrue = HoldsTrue+ op HoldsFalse _ = HoldsFalse+ op _ HoldsFalse = HoldsFalse+ op Unknown Unknown = Unknown+store_unions :: [Store] -> Store+store_unions = foldr store_union emptyStore++make_assignments :: Store -> State -> State+make_assignments = flip (M.foldrWithKey op)+ where op te HoldsTrue = create te+ op te HoldsFalse = terminate te+ op te Unknown = obfuscate te++derive :: Tagged -> State -> State+derive te s = s { contents = M.alter adj te (contents s) }+ where adj Nothing = Just $ Info{ value = True, from_sat = True }+ adj (Just info) = Just info++derive_all :: [Tagged] -> State -> State+derive_all = flip (foldr derive)++create :: Tagged -> State -> State+create te s = s { contents = M.insert te Info{ value = True, from_sat = False } (contents s) }++create_all :: [Tagged] -> State -> State+create_all = flip (foldr create)++terminate :: Tagged -> State -> State+terminate te s = s { contents = M.insert te Info{ value = False, from_sat = False } (contents s) }++terminate_all :: [Tagged] -> State -> State+terminate_all = flip (foldr terminate)++obfuscate :: Tagged -> State -> State+obfuscate te s = s { contents = M.delete te (contents s) }++obfuscate_all :: [Tagged] -> State -> State+obfuscate_all = flip (foldr obfuscate)++-- | assumes the instance of a closed type+holds :: Tagged -> State -> Bool+holds te s = maybe False ((==True) . value) (M.lookup te (contents s))++emptyState = State { contents = M.empty, time = 0 }++increment_time state = state { time = 1 + (time state) }++instance Show State where+ show state = unlines $ + [ show_component c ++ " = " ++ show (value m)+ | (c,m) <- M.assocs (contents state)+ ]++-- instance ToJSON State where+-- toJSON state = toJSON (map TaggedJSON (state_holds state)) ++state_holds :: State -> [Tagged]+state_holds state = [ te | (te, m) <- M.assocs (contents state), True == value m ]++state_input_holds :: State -> InputMap -> [Tagged]+state_input_holds state inpm = state_holds state ++ input_holds inpm++state_not_holds :: State -> [Tagged]+state_not_holds state = [ te | (te, m) <- M.assocs (contents state), False == value m ]++input_holds :: InputMap -> [Tagged]+input_holds inpm = [ te | (te, True) <- M.assocs inpm ]++data Context = Context {+ ctx_spec :: Spec --mutable + , ctx_state :: State --mutable + , ctx_transitions :: [Transition] -- (label * enabled?) -- replaceable+ , ctx_duties :: [Tagged] -- replaceable+ }++-- mutable means c0 ; c1 results in c1 adding to c0 with possible override+-- appendable means c0 ; c1 results in effects of c0 and c1 being concatenated+-- replaceable means c0 ; c1 results in effect of c1++emptyContext spec = + Context { + ctx_spec = spec+ , ctx_state = emptyState+ , ctx_transitions = empty+ , ctx_duties = empty }++data TransInfo = TransInfo {+ trans_tagged :: Tagged + , trans_assignments :: Store -- includes sync'ed effects+ , trans_forced :: Bool -- whether this or a sync'ed transition is not enabled was forced (i.e. was not enabled)+ , trans_actor :: Maybe Tagged+ , trans_syncs :: [TransInfo] -- the transitions this transitions sync'ed with + }+ deriving (Eq, Ord, Show, Read) ++trans_is_action :: TransInfo -> Bool+trans_is_action = isJust . trans_actor++data Violation = DutyViolation Tagged+ | TriggerViolation TransInfo + | InvariantViolation DomId+ deriving (Ord, Eq, Show, Read) ++data QueryRes = QuerySuccess+ | QueryFailure+ deriving (Ord, Eq, Show, Read)++data Error = -- trigger errors+ NotTriggerable Tagged+ | NonDeterministicTransition+ | CompilationError String+ | RuntimeError RuntimeError+ deriving (Eq, Ord, Show, Read) ++data RuntimeError+ = MissingInput Tagged + | InternalError InternalError+ deriving (Eq, Ord, Show, Read) ++data InternalError + = EnumerateInfiniteDomain DomId Domain + | MissingSubstitution Var+ | PrimitiveApplication DomId+ | UndeclaredType DomId + deriving (Eq, Ord, Show, Read)++print_error :: Error -> String+print_error (NotTriggerable te) = "not a triggerable instance: " ++ ppTagged te+print_error (NonDeterministicTransition) = "non-deterministic transition attempt"+print_error (CompilationError err) = err+print_error (RuntimeError err) = print_runtime_error err++print_runtime_error :: RuntimeError -> String+print_runtime_error (MissingInput te) = "missing input assignment for: " ++ ppTagged te+print_runtime_error (InternalError err) = "INTERNAL ERROR " ++ print_internal_error err++print_internal_error :: InternalError -> String+print_internal_error (EnumerateInfiniteDomain d AnyString) = "cannot enumerate all strings of type: " ++ d+print_internal_error (EnumerateInfiniteDomain d AnyInt) = "cannot enumerate all integers of type: " ++ d+print_internal_error (EnumerateInfiniteDomain d _) = "cannot enumerate all instances of type: " ++ d+print_internal_error (MissingSubstitution (Var base dec)) = "variable " ++ base ++ dec ++ " not bound"+print_internal_error (PrimitiveApplication d) = "application of primitive type: " ++ d+print_internal_error (UndeclaredType d) = "undeclared type: " ++ d
+ src/Language/EFLINT/StaticEval.hs view
@@ -0,0 +1,495 @@+{-# LANGUAGE RecordWildCards, LambdaCase, TupleSections #-}++module Language.EFLINT.StaticEval where++import Language.EFLINT.Spec+import Language.EFLINT.Binders++import Control.Monad+import Control.Applicative++import Data.Maybe (isNothing)+import Data.List ((\\))+import qualified Data.Map as M+import qualified Data.Set as S++data M_Stc a = M_Stc {runStatic :: Spec -> Either [String] (Spec, a)}++instance Monad M_Stc where+ return a = M_Stc $ \spec -> Right (spec, a)+ m >>= f = M_Stc $ \spec -> case runStatic m spec of + Right (spec',a) -> runStatic (f a) spec'+ Left err -> Left err++instance Applicative M_Stc where+ pure = return+ (<*>) = ap++instance Functor M_Stc where+ fmap = liftM++instance Alternative M_Stc where+ empty = M_Stc (const (Left []))+ p <|> q = M_Stc $ \spec -> case runStatic p spec of + Left ers1 -> case runStatic q spec of+ Left ers2 -> Left (ers1 ++ ers2)+ Right x -> Right x+ Right x -> Right x++err :: String -> M_Stc a+err str = M_Stc $ \spec -> Left [str]++get_dom :: DomId -> M_Stc Domain+get_dom d = M_Stc $ \spec -> case find_decl spec d of + Just tspec -> Right (spec, domain tspec)+ _ -> Left ["undeclared type: " ++ d]++get_spec :: M_Stc Spec+get_spec = M_Stc $ \spec -> Right (spec, spec)++execute_decl :: Decl -> M_Stc ()+execute_decl decl = M_Stc $ \spec -> + let spec' = case decl of + PlaceholderDecl f t -> spec { aliases = M.insert f t (aliases spec) }+ TypeExt ty clauses -> spec { decls = M.adjust (apply_type_ext ty clauses) ty (decls spec) }+ TypeDecl ty tspec -> spec { decls = M.insert ty tspec (decls spec) }+ in Right (spec', ())++with_spec :: Spec -> M_Stc a -> M_Stc a+with_spec spec' m = M_Stc $ \spec -> case runStatic m spec' of+ Left err -> Left err+ Right (_,a) -> Right (spec, a)++with_decl :: DomId -> TypeSpec -> M_Stc a -> M_Stc a+with_decl ty tspec m = M_Stc $ \spec -> case runStatic m (spec{decls=M.insert ty tspec (decls spec)}) of+ Left err -> Left err+ Right (_,a) -> Right (spec, a)++free_vars :: Term -> M_Stc (S.Set Var)+free_vars t = do spec <- get_spec+ let xs = free spec t+ check_known_type (S.toList xs)+ return xs++compile_all :: Spec -> Refiner -> Initialiser -> Scenario -> Either [String] (Spec, Refiner, Initialiser, Scenario) +compile_all f r i s = case runStatic compile f of+ Left errs -> Left errs + Right (_,(spec, init, scen)) -> Right (spec, r, init, scen)+ where compile = do+ f' <- compile_spec+ with_spec f' $ do+ i' <- compile_initialiser i+ s' <- compile_stmts s+ return (f',i',s')++compile_initialiser :: Initialiser -> M_Stc Initialiser+compile_initialiser = mapM (compile_effect [])++compile_stmts :: [Statement] -> M_Stc [Statement]+compile_stmts = mapM compile_stmt++compile_stmt :: Statement -> M_Stc Statement+compile_stmt (Query t0) = do+ spec <- get_spec+ fs <- free_vars t0+ let unbounds = S.toList fs+ let t1 | null unbounds = t0+ | Not inner <- t0 = Not (Exists unbounds inner)+ | otherwise = Exists unbounds t0+ case filter (isNothing . find_decl spec . remove_decoration spec) unbounds of+ [] -> Query <$> convert_term t1 TyBool+ (t:_) -> err ("undeclared type " ++ remove_decoration spec t ++ " in query")+compile_stmt (Trans xs aty (Right (d,mods))) = compile_trans_term xs aty (App d mods) (Just d)+compile_stmt (Trans xs aty (Left t)) = compile_trans_term xs aty t Nothing+compile_trans_term xs aty term md = do + fs <- free_vars term+ let unbounds = S.toList (fs `S.difference` S.fromList xs)+ Trans (xs ++ unbounds) aty . Left <$> converter term+ where converter term = case md of Just d -> convert_term term (TyTagged d)+ _ -> fst <$> compile_term term++compile_phrase :: Phrase -> M_Stc CPhrase+compile_phrase p = case p of+ PSkip -> return CPSkip+ PDo tv -> return (CDo tv)+ PTrigger vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p))+ Create vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p))+ Terminate vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p))+ Obfuscate vs t -> fmap (de_stmt p) (compile_stmt (to_stmt p))+ PQuery t -> fmap (de_stmt p) (compile_stmt (to_stmt p))+ PDeclBlock ds -> do+ forM_ (filter introducesName ds) execute_decl + forM_ ds ((execute_decl =<<) . compile_decl)+ return CPOnlyDecls + where to_stmt (PTrigger vs t) = Trans vs Trigger (Left t)+ to_stmt (Create vs t) = Trans vs AddEvent (Left t)+ to_stmt (Terminate vs t) = Trans vs RemEvent (Left t)+ to_stmt (Obfuscate vs t) = Trans vs ObfEvent (Left t)+ to_stmt (PQuery t) = Query t+ to_stmt _ = error "Explorer.assert 1"+ de_stmt (PTrigger vs t) (Trans vs' Trigger (Left t')) = CTrigger vs' t'+ de_stmt (Create vs t) (Trans vs' AddEvent (Left t')) = CCreate vs' t'+ de_stmt (Terminate vs t) (Trans vs' RemEvent (Left t')) = CTerminate vs' t'+ de_stmt (Obfuscate vs t) (Trans vs' ObfEvent (Left t')) = CObfuscate vs' t'+ de_stmt (PQuery t) (Query t') = CQuery t'+ de_stmt _ _ = error "Explorer.assert 2"++compile_decl :: Decl -> M_Stc Decl+compile_decl d@(PlaceholderDecl x y) = check_known_type [no_decoration y] >> return d +compile_decl d@(TypeExt ty clauses) = compile_ext ty clauses +compile_decl d@(TypeDecl ty tspec) = compile_type_spec ty tspec ++compile_ext :: DomId -> [ModClause] -> M_Stc Decl+compile_ext ty clauses = do+ spec <- get_spec + case M.lookup ty (decls spec) of+ Nothing -> err ("cannot find the type " ++ ty ++ " to extend or " ++ ty ++ " of the wrong kind")+ Just tspec -> TypeExt ty <$> mapM (compile_clause ty tspec) clauses + where compile_clause ty tspec clause = case clause of + ConditionedByCl conds -> ConditionedByCl <$> mapM (convert_precon ty tspec) conds+ DerivationCl dvs -> DerivationCl <$> mapM (compile_derivation xs ty) dvs + PostCondCl effs -> PostCondCl <$> mapM (compile_effect xs) effs + SyncCl ss -> SyncCl <$> mapM (compile_sync xs) ss+ ViolationCl vts -> ViolationCl <$> mapM (compile_violation_condition ty) vts+ EnforcingActsCl ds -> return $ EnforcingActsCl ds+ where xs = case domain tspec of Products xs -> xs+ _ -> [no_decoration ty]+ +compile_type_spec :: DomId -> TypeSpec -> M_Stc Decl +compile_type_spec ty tspec = do+ with_decl ty tspec $ do -- ensure the declaration is active during its compilation + dom <- get_dom ty+ check_domain ty dom+ let xs = case dom of + Products xs -> xs+ _ -> [no_decoration ty]+ derivation <- mapM (compile_derivation xs ty) (derivation tspec) + kind <- compile_kind ty tspec (kind tspec)+ conditions <- mapM (convert_precon ty tspec) (conditions tspec)+ dom_filter <- convert_term (domain_constraint tspec) TyBool+ ffs <- free_vars dom_filter+ let domain_constraint = case S.toList (ffs `S.difference` S.fromList xs) of+ [] -> dom_filter+ vars -> Exists vars dom_filter+ return (TypeDecl ty (TypeSpec {domain = domain tspec, closed = closed tspec,..}))++check_domain :: DomId -> Domain -> M_Stc ()+check_domain dty (Products xs) = check_known_type xs +check_domain _ _ = return ()++check_known_type :: [Var] -> M_Stc ()+check_known_type xs = do+ spec <- get_spec+ let op var@(Var base dec) = case find_decl spec (remove_decoration spec var) of+ Nothing -> err ("Undeclared type or placeholder `" ++ base ++ dec ++ "`")+ Just _ -> return ()+ mapM_ op xs++convert_precon :: DomId -> TypeSpec -> Term -> M_Stc Term+convert_precon ty tspec t = do + let xs = case domain tspec of Products xs -> xs+ _ -> [no_decoration ty]+ cond' <- convert_term t TyBool+ cond_fs <- free_vars cond'+ let unbounds = S.toList (cond_fs `S.difference` S.fromList xs)+ return $ if null unbounds then cond' else Exists unbounds cond'++compile_kind :: DomId -> TypeSpec -> Kind -> M_Stc Kind+compile_kind ty tspec k = case k of+ Act aspec -> do + let Products xs = domain tspec+ -- convert post-conditions+ effects' <- sequence (map (compile_effect xs) (effects aspec))+ -- convert syncs+ syncs' <- mapM (compile_sync xs) (syncs aspec)+ -- build new act+ return (Act (aspec { effects = effects', syncs = syncs' } ))+ Event espec -> do + let Products xs = domain tspec+ effects' <- sequence (map (compile_effect xs) (event_effects espec))+ return (Event (espec { event_effects = effects' } ))+ Duty dspec -> do -- TODO, should be dealt with by outer -> inner translation+ e_conds <- concat <$> mapM select_condition (enforcing_acts dspec)+ vconds <- mapM (compile_violation_condition ty) (e_conds ++ violated_when dspec)+ return $ (Duty (dspec { violated_when = vconds }))+ where select_condition a = do+ spec <- get_spec+ case M.lookup a (decls spec) of + Just tspec | Act _ <- kind tspec -> return [foldr And (BoolLit True) (conditions tspec)]+ _ -> err ("duty " ++ ty ++ " is declared with enforcing act " ++ a ++ " which is not a declared or not declared as an act")+ Fact _ -> return k++compile_violation_condition :: DomId -> Term -> M_Stc Term+compile_violation_condition dty term = do+ domain <- get_dom dty+ let Products xs = domain+ term' <- convert_term term TyBool+ fs <- free_vars term'+ let unbounds = S.toList (fs `S.difference` (S.fromList xs))+ term'' | null unbounds = term'+ | otherwise = Exists unbounds term'+ return term'' ++compile_sync :: [Var] -> Sync -> M_Stc Sync +compile_sync bound (Sync vars t) = do+ (t', tau) <- compile_term t+ case tau of+ TyTagged _ -> do frees <- free_vars t'+ let unbounds = S.toList (frees `S.difference` S.fromList (vars ++ bound))+ return $ Sync (vars ++ unbounds) t' + _ -> err ("sync clause is not an instance expression")++compile_spec :: M_Stc Spec+compile_spec = do+ spec <- get_spec+ ds <- sequence (map (uncurry compile_type_spec) (M.toList (decls spec)))+ let tspecs = concatMap op ds+ where op (TypeDecl ty tspec) = [(ty,tspec)]+ op _ = []+ return (spec {decls = decls_union (decls spec) (M.fromList tspecs) })+ +compile_derivation :: [Var] -> DomId -> Derivation -> M_Stc Derivation+compile_derivation bound d (HoldsWhen t) = do+ t' <- convert_term t TyBool + fs <- free_vars t'+ let unbounds = S.toList (fs `S.difference` (S.fromList bound))+ return (HoldsWhen (if null unbounds then t' else Exists unbounds t'))+compile_derivation bound d (Dv xs t) = compile_derived_from_clause xs t d++compile_derived_from_clause xs t d = do+ t' <- convert_term t (TyTagged d)+ fs <- free_vars t'+ let unbounds = S.toList (fs `S.difference` (S.fromList xs))+ return (Dv (xs ++ unbounds) t')++compile_primitive_application :: DomId -> Arguments -> M_Stc (Term, Type)+compile_primitive_application d params = get_dom d >>= \dom -> case (dom, params) of+ (_, Left as) | length as > 1 -> err error_string+-- (AnyString, Left []) -> primitive d (StringLit "()") (Just TyStrings)+-- (AnyString, Right []) -> primitive d (StringLit "()") (Just TyStrings)+ (AnyString, Left [a]) -> primitive d a (Just TyStrings)+ (Strings [s], Left []) -> primitive d (StringLit s) (Just TyStrings)+ (Strings [s], Right [])-> primitive d (StringLit s) (Just TyStrings)+ (Strings _, Left [a]) -> primitive d a (Just TyStrings)+ (AnyInt, Left [a]) -> primitive d a (Just TyInts)+ (Ints [i], Right []) -> primitive d (IntLit i) (Just TyInts)+ (Ints [i], Left []) -> primitive d (IntLit i) (Just TyInts)+ (Ints _, Left [a]) -> primitive d a (Just TyInts)+ (_, Right _) -> err error_string+ _ -> err error_string+ where error_string = "The constructor " ++ d ++ " is primitive, and should receive exactly one argument in functional style"+ primitive d t Nothing = do (t', _) <- compile_term t+ return (Tag t' d, TyTagged d)+ primitive d t (Just ty) = do t' <- convert_term t ty+ return (Tag t' d, TyTagged d)+ + +compile_arguments :: DomId -> Arguments -> M_Stc Arguments+compile_arguments _ (Right ms) = Right <$> compile_modifiers ms+compile_arguments d (Left ts) = do+ spec <- get_spec+ dom <- get_dom d+ case dom of Products xs + | length xs == length ts -> Right <$> compile_modifiers (map (uncurry Rename) (zip xs ts))+ | otherwise -> err ("elements of " ++ d ++ " have " ++ show (length xs) ++ " components, " ++ show (length ts) ++ " given")+ _ -> err ("non-composite " ++ d ++ " used in application")++compile_modifiers :: [Modifier] -> M_Stc [Modifier]+compile_modifiers mods = do+ spec <- get_spec+ let compile_mod (Rename x t) = Rename x <$> convert_term t (TyTagged (remove_decoration spec x)) + sequence (map compile_mod mods)++compile_effect :: [Var] -> Effect -> M_Stc Effect+compile_effect bound eff = case eff of + TAll xs t -> compile_effect' TAll xs t+ CAll xs t -> compile_effect' CAll xs t+ OAll xs t -> compile_effect' OAll xs t+ where compile_effect' cons xs t = do (t',tau) <- compile_term t+ fs <- free_vars t'+ let unbounds = S.toList (fs `S.difference` S.fromList (bound ++ xs))+ return (cons (xs ++ unbounds) t')++compile_term :: Term -> M_Stc (Term, Type)+compile_term t0 = do+ spec <- get_spec + case t0 of+ CurrentTime -> return (CurrentTime, TyInts)+ StringLit s -> return (t0, TyStrings)+ IntLit i -> return (t0, TyInts)+ BoolLit b -> return (t0, TyBool)+ Ref x -> check_known_type [x] >> return (t0, TyTagged (remove_decoration spec x))+ App d ms -> do check_known_type [no_decoration d]+ case fmap domain (find_decl spec d) of + Just (Products _) -> do + ms' <- compile_arguments d ms + return (App d ms', TyTagged d)+ _ -> compile_primitive_application d ms + Tag t d -> err "tagging is an auxiliary operation" + Untag t -> do (t', ty) <- compile_term t+ case ty of TyTagged d -> case find_decl spec d of+ Nothing -> err "untagging is an auxiliary operation"+ Just decl -> case domain decl of+ Strings _ -> return (Untag t', TyStrings)+ Ints _ -> return (Untag t', TyInts)+ AnyString -> return (Untag t', TyStrings)+ AnyInt -> return (Untag t', TyInts)+ _ -> err "untagging is an auxiliary operation"+ _ -> err "untagging is an auxiliary operation"++ Not t -> do t' <- convert_term t TyBool+ return (Not t', TyBool)+ And t1 t2 -> do t1' <- convert_term t1 TyBool+ t2' <- convert_term t2 TyBool+ return (And t1' t2', TyBool)+ Or t1 t2 -> do t1' <- convert_term t1 TyBool+ t2' <- convert_term t2 TyBool+ return (Or t1' t2', TyBool)++ Geq t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Geq t1' t2', TyBool)+ Leq t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Leq t1' t2', TyBool)+ Le t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Le t1' t2', TyBool)+ Ge t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Ge t1' t2', TyBool)++ Mult t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Mult t1' t2', TyInts)+ Mod t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Mod t1' t2', TyInts)+ Div t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Div t1' t2', TyInts)+ Sub t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Sub t1' t2', TyInts)+ Add t1 t2 -> do t1' <- convert_term t1 TyInts+ t2' <- convert_term t2 TyInts+ return (Add t1' t2', TyInts)+ Sum xs t -> do t' <- convert_term t TyInts + return (Sum xs t', TyInts)++ Eq t1 t2 -> (do (t1', tau1) <- compile_term t1+ t2' <- convert_term t2 tau1+ return (Eq t1' t2', TyBool)) <|>+ (do (t2', tau2) <- compile_term t2+ t1' <- convert_term t1 tau2+ return (Eq t1' t2', TyBool))+ Neq t1 t2 -> (do (t1', tau1) <- compile_term t1+ t2' <- convert_term t2 tau1+ return (Neq t1' t2', TyBool)) <|>+ (do (t2', tau2) <- compile_term t2+ t1' <- convert_term t1 tau2+ return (Neq t1' t2', TyBool))+ Count xs t -> do (t', tau) <- compile_term t+ return (Count xs t', TyInts)+ Max xs t -> do (t', tau) <- compile_term t+ return (Max xs t', TyInts)+ Min xs t -> do (t', tau) <- compile_term t+ return (Min xs t', TyInts)+ When t1 t2 -> do (t1', tau) <- compile_term t1+ t2' <- convert_term t2 TyBool+ return (When t1' t2', tau)+ Present t -> do (t', tau) <- compile_term t -- simplification, assuming no conversion to tagged-elems yet+ case tau of TyTagged d -> return (Present t', TyBool) + errt -> err ("Holds(t) requires t to evaluate to a an instance, not a literal")+ Violated t -> do (t', tau) <- compile_term t -- simplification, as above+ case tau of TyTagged d -> return (Violated t', TyBool)+ errt -> err ("Violated(t) requires t to evaluate to an instance, not a literal")+ Enabled t -> do (t', tau) <- compile_term t -- simplification, as above+ case tau of TyTagged d -> return (Enabled t', TyBool)+ errt -> err ("Enabled(t) requires t to evaluate to an instance, not a literal")+ Exists xs t -> do t' <- convert_term t TyBool+ return (Exists xs t', TyBool)+ Forall xs t -> do t' <- convert_term t TyBool+ return (Forall xs t', TyBool)+ Project t x -> do (t',tau) <- compile_term t+ case tau of + TyTagged d -> do + dom <- get_dom d+ case dom of + Products xs -> if elem x xs + then return (Project t' x, TyTagged (remove_decoration spec x))+ else err ("project(" ++ show t++ ","++show x++") expects t to evaluate to a value of a product-type containing a reference to " ++ show x ++ " instead got: " ++ show xs) + _ -> err ("project(" ++ show t++ ","++show x++") expects t to evaluate to a value of a product-type, instead got: " ++ show dom) + _ -> err ("project(" ++ show t++ ","++show x++") expects t to evaluate to a tagged-element, instead got: " ++ show tau) ++-- term => term : type+convert_term :: Term -> Type -> M_Stc Term+convert_term t ty = do+ (t', ty') <- compile_term t+ if ty' == ty then return t' -- rule id+ else case ty of+ TyStrings -> case ty' of TyTagged d -> flip match_domain AnyString <$> get_dom d >>= \case+ True -> return (Untag t')+ False -> conv_err ty' ty+ _ -> conv_err ty' ty+ TyInts -> case ty' of TyTagged d -> flip match_domain AnyInt <$> get_dom d >>= \case+ True -> return (Untag t')+ False -> conv_err ty' ty + _ -> conv_err ty' ty+ TyBool -> case ty' of TyInts -> return $ Geq t' (IntLit 1) -- rule INT -> BOOL+ TyTagged _ -> return $ Present t' + _ -> conv_err ty' ty+ TyTagged d -> get_dom d >>= match_type ty' >>= \case True -> return (Tag t' d)+ False -> conv_err ty' ty+ where conv_err source target = err ("cannot convert " ++ show source ++ " to " ++ show target)++match_type :: Type -> Domain -> M_Stc Bool+match_type (TyTagged d) dom = get_dom d >>= return . flip match_domain dom +match_type TyInts dom = case dom of+ AnyInt -> return True+ Ints _ -> return True+ Time -> return True+ Strings _ -> return False+ AnyString -> return False+ Products _ -> return False+match_type TyStrings dom = case dom of+ AnyString -> return True+ Strings _ -> return True+ AnyInt -> return False+ Ints _ -> return False+ Products _ -> return False+ Time -> return False+match_type _ _ = return False++-- | second domain is the conversion target+match_domain :: Domain -> Domain -> Bool+match_domain dom dom' = case (dom, dom') of+ (AnyString, AnyString) -> True + (Strings _, AnyString) -> True+ (AnyString, Strings _) -> False+ (Strings s1, Strings s2) -> null (s1 \\ s2) + (AnyString, _) -> False+ (Strings _, _) -> False++ (AnyInt, AnyInt) -> True+ (Ints _, AnyInt) -> True+ (AnyInt, Ints _) -> True+ (Ints i1, Ints i2) -> null (i1 \\ i2)+ (AnyInt, AnyString) -> False+ (AnyInt, Strings _) -> False+ (AnyInt, Products _) -> False+ (Ints _, AnyString) -> False+ (Ints _, Strings _) -> False+ (Ints _, Products _) -> False+ (AnyInt, Time) -> False+ (Ints _, Time) -> False+ + (Time, Time) -> True+ (Time, AnyInt) -> True+ (Time, Ints _) -> False+ (Time, AnyString) -> False+ (Time, Strings _) -> False+ (Time, Products _) -> False++ (Products r, Products r') -> r == r'+ (Products _, _) -> False
+ src/Language/EFLINT/Util.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE LambdaCase #-}++module Language.EFLINT.Util where++import Control.Monad (forM)+import System.FilePath+import System.Directory++find_included_file :: [FilePath] -> FilePath -> IO [FilePath]+find_included_file dirs path = do + concat <$> forM dirs (\dir -> do + let file = dir </> path + doesFileExist file >>= \case True -> return [file]+ False -> (doesFileExist (file ++ ".eflint") >>= \case True -> return [file ++ ".eflint"]+ False -> return []))+
+ src/REPL.hs view
@@ -0,0 +1,296 @@+{-# LANGUAGE LambdaCase #-}++module Main where++import Language.EFLINT.Spec+import Language.EFLINT.Explorer+import Language.EFLINT.Interpreter+import Language.EFLINT.Parse+import Language.EFLINT.Print (ppDeclSpec)+import Language.EFLINT.State+import Language.EFLINT.StaticEval+import Language.EFLINT.Options+import Language.EFLINT.Util+import Language.EFLINT.JSON(decode_json_file)++import qualified Language.Explorer.Pure as EI ++import Control.Monad (forM_, foldM, when, unless)+import Control.Monad.Trans.Class (lift)+import Data.Char (isSpace)+import Data.List (isPrefixOf, isSuffixOf, (\\))+import qualified Data.Map as M+import qualified Data.Set as S++import Text.Read (readMaybe)++import System.IO.Error+import System.Environment +import System.Directory+import System.FilePath+import System.Console.Haskeline hiding (display)++-- the kind of explorer to use+init_explorer = init_tree_explorer++main = getArgs >>= arg_select ++arg_select :: [String] -> IO ()+arg_select args = do+ cdir <- getCurrentDirectory + let (files, flags') = span (not . (\a -> isPrefixOf "--" a || isPrefixOf "-" a)) args+ opts <- run_options (["-i",cdir] ++ flags')+ case files of+ [] -> repl_without opts+ [f] | ".eflint" `isSuffixOf` f -> repl_with opts f+ [f] | ".json" `isSuffixOf` f -> repl_with opts f+ _ -> putStrLn "Please provide: <NAME>.eflint <OPTIONS>"++repl_without :: Options -> IO ()+repl_without opts = compile_and_init opts emptySpec M.empty [] []++repl_with :: Options -> FilePath -> IO ()+repl_with opts fsrc = do + add_filepath fsrc opts + input_exists <- doesFileExist (fsrc ++ ".input")+ when input_exists $+ readFile (fsrc ++ ".input") >>= flip add_input opts . lines+ add_include_path (takeDirectory fsrc) opts+ add_include fsrc opts+ case ".json" `isSuffixOf` fsrc of+ True -> decode_json_file fsrc >>= \case+ Left err -> putStrLn "could not parse JSON file:\n" >> putStrLn err+ Right spec -> compile_and_init opts spec M.empty [] []+ False -> do+ fl <- readFile fsrc+ case parse_component syn_directives_phrases fl of+ Left err1 -> case parse_flint fl of + Left err2 -> do putStrLn "could not parse flint phrases:\n" >> putStrLn err1+ putStrLn "could not parse flint spec:\n" >> putStrLn err2+ Right (f,r,i,s) -> case find ignore_scenario opts of+ True -> compile_and_init opts f r i []+ False -> compile_and_init opts f r i s+ Right ps -> init_with_phrases opts ps++compile_and_init :: Options -> Spec -> Refiner -> Initialiser -> Scenario -> IO ()+compile_and_init opts f r i s = case compile_all f r i s of+ Right (spec',r',i',s') -> do+ test <- is_in_test_mode opts+ unless test $ do + let spec = refine_specification spec' r'+ let state = make_initial_state spec i'+ let explorer = init_explorer (Just (spec,state))+ let ((_,c0),_,(sid, ctx)) = get_last_edge explorer (EI.currRef explorer)+ verbosity opts 1 $ display_commands+ verbosity opts 2 $ display_info opts [] c0 ctx+ runInputT defaultSettings (repl opts explorer)+ Left errs -> putStrLn "compilation errors:" >> putStrLn (unlines errs) ++init_with_phrases :: Options -> [Either Directive Phrase] -> IO ()+init_with_phrases opts ps = do + let explorer = init_explorer Nothing+ test <- is_in_test_mode opts+ runInputT defaultSettings $ do + exp <- repl_directive_phrases opts ps explorer+ unless test (repl opts exp)++repl :: Options -> Explorer -> InputT IO ()+repl opts exp = do+ let (_, _, (sid, ctx)) = get_last_edge exp (EI.currRef exp)+ maybeLine <- getInputLine ("#" ++ show sid ++ " > ")+ case maybeLine of+ Nothing -> return ()+ Just input -> do+ case span (not . isSpace) input of + (":choose", mint) -> repl_trigger ctx mint + (":revert", mint) | Just sid' <- readMaybe (dropWhile isSpace mint)+ -> case run_ exp (Revert sid') of+ InvalidRevert -> outputStrLn ("state id " ++ show sid' ++ " unknown") >> continue exp+ ResultTrans exp outs (old,_) (new,sid) -> do+ lift (display_info opts outs old new)+ continue exp+ | otherwise -> lift display_commands >> continue exp+ (":display", _) -> lift (display ctx) >> continue exp+ (":d", _) -> lift (display ctx) >> continue exp + (":spec", mty) -> lift (display_spec ctx mty) >> continue exp+ (":session", _) -> outputStrLn (showTree exp) >> continue exp + (":s", _) -> outputStrLn (showTree exp) >> continue exp + (":options", _) -> lift (display_all_triggers ctx) >> continue exp + (":o", _) -> lift (display_all_triggers ctx) >> continue exp+ (":help", _) -> lift display_commands >> continue exp+ (":h", _) -> lift display_commands >> continue exp+ (":quit", _) -> return ()+ (":q", _) -> return ()+ ((':':mint),_) -> repl_trigger ctx mint+ ("#include", fp') -> repl_directive opts (Include fp) exp >>= continue + where fp = case readMaybe fp' of Nothing -> dropWhile isSpace fp' + Just str -> str+ ("#require", fp') -> repl_directive opts (Require fp) exp >>= continue + where fp = case readMaybe fp' of Nothing -> dropWhile isSpace fp' + Just str -> str+ _ -> repl_recognize_phrase input+ where continue = repl opts+ repl_trigger ctx mint = case readMaybe (dropWhile isSpace mint) of+ Just trig | trig <= length (rest_transitions ctx), trig > 0+ -> repl_phrases opts emptyInput [PDo (fst $ map get_transition (rest_transitions ctx) !! (trig - 1))] exp >>= continue+ _ -> lift display_commands >> continue exp++ repl_recognize_phrase str = case parse_component syn_phrases str of+ Left err -> outputStrLn err >> continue exp+ Right ps -> repl_phrases opts emptyInput ps exp >>= continue++repl_directive_phrases :: Options -> [Either Directive Phrase] -> Explorer -> InputT IO Explorer+repl_directive_phrases opts [] explorer = return explorer+repl_directive_phrases opts (edp:ps) explorer = + case edp of + Left d -> repl_directive opts d explorer >>= repl_directive_phrases opts ps+ Right p -> repl_phrases opts emptyInput [p] explorer >>= repl_directive_phrases opts ps+ where (_,_,(_,ctx)) = get_last_edge explorer (EI.currRef explorer) + isQuery phrase = case phrase of PQuery _ -> True+ _ -> False ++repl_phrases :: Options -> InputMap -> [Phrase] -> Explorer -> InputT IO Explorer +repl_phrases opts inpm phrases explorer = + repl_report opts inpm phrases (run_ explorer (Execute (convert_programs phrases) inpm)) explorer++repl_directive :: Options -> Directive -> Explorer -> InputT IO Explorer +repl_directive opts (Include fp) explorer = repl_import opts fp explorer+repl_directive opts (Require fp) explorer + | has_been_included fp opts = return explorer+ | otherwise = repl_import opts fp explorer++repl_import :: Options -> FilePath -> Explorer -> InputT IO Explorer+repl_import opts fp explorer = do+ let dirs = find include_paths opts+ files <- lift $ find_included_file dirs fp+ case files of + [] -> lift $ putStrLn ("could not find " ++ fp ++ " in " ++ show dirs) >> return explorer+ (file:_) -> do+ lift $ add_include_path (takeDirectory file) opts+ lift $ add_include file opts+ case ".json" `isSuffixOf` file of + True -> do+ mspec <- lift (decode_json_file file)+ case mspec of+ Left err -> lift (putStrLn err) >> return explorer+ Right spec -> lift (putStrLn "including .json files is no longer supported") >> return explorer --repl_directive_phrases opts [Right (PFrames spec)] explorer+ False -> lift (catchIOError (Right <$> readFile file) handler) >>= \case + Left err -> lift (putStrLn err) >> return explorer+ Right str -> case parse_component syn_directives_phrases str of+ Left err -> lift (putStrLn err) >> return explorer+ Right eps -> repl_directive_phrases opts eps explorer+ 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))+++repl_report :: Options -> InputMap -> [Phrase] -> -- both used for re-execution in case of missing input + Response -> Explorer -> InputT IO Explorer+repl_report opts inpm phrases res exp = case res of+ ResultTrans exp outs (old,_) (ctx,sid) -> case missing_inputs outs of+ [] -> lift (verbosity opts 3 (display_info opts outs old ctx)) >> return exp+ ms -> do minpm <- foldM consider (Just inpm) ms+ case minpm of Just inpm' -> repl_phrases opts inpm' phrases exp + Nothing -> return exp+ where consider Nothing _ = return Nothing+ consider (Just inpm) te@(_,d) = do+ mass <- lift (consume_input opts)+ let tryWith b = Just $ M.insert te b inpm+ case mass of+ Just b -> return (tryWith b)+ Nothing -> do+ lift $ putStrLn ("\nmissing truth-value for: " ++ ppTagged te)+ lift $ putStrLn ("is this fact True or False?") + getInputLine "(True/False) > " >>= \case+ Just s -> return $ tryWith (readAssignmentMaybe s)+ Nothing -> return Nothing+ InvalidRevert -> error "REPL.assert 1"++display_commands = + putStrLn "Available commands:\n\+ \ :<INT> same as :choose <INT>\n\+ \ :choose <INT> choose action or event trigger <INT>\n\+ \ :force <INT> choose and force action or event trigger <INT>\n\+ \ :revert <INT> revert to the configuration with id <INT>\n\+ \ :display :d show all contents of the current configuration\n\+ \ :spec pretty-print all type definitions\n\+ \ :session :s show the history of the session\n\+ \ :options :o show all actions & events, including disabled actions\n\+ \ :help :h show these commands\n\+ \ :quit :q end the exploration\n\+ \ or just type a <PHRASE>"++display_info :: Options -> [Output] -> Config -> Config -> IO ()+display_info opts outs c0 cfg = do+ verbosity opts 4 $ display_errors (errors outs) + verbosity opts 5 $ display_query_results (query_ress outs)+ verbosity opts 6 $ display_transitions (ex_triggers outs)+ verbosity opts 7 $ display_violations (violations outs)+ verbosity opts 8 $ display_new_types (M.keysSet $ decls $ cfg_spec c0) (M.keysSet $ decls $ cfg_spec cfg)+ verbosity opts 9 $ display_fact_changes (cfg_state c0) (cfg_state cfg)+ verbosity opts 10$ display_new_invariants (invariants $ cfg_spec c0) (invariants $ cfg_spec cfg)+ where display_query_results [] = return ()+ display_query_results ress = mapM_ op ress+ where op QuerySuccess = verbosity opts 11 (putStrLn "query successful")+ op QueryFailure = verbosity opts 12 (putStrLn "query failed")++ display_errors [] = return ()+ display_errors errs = mapM_ op errs+ where op (CompilationError err) = putStr err+ op err = putStrLn (print_error err)+++display_violations [] = return () +display_violations vs = putStrLn "violations:" >> mapM_ op vs+ where op (DutyViolation te) = putStrLn (" violated duty!: " ++ ppTagged te)+ op (InvariantViolation d) = putStrLn (" violated invariant!: " ++ d)+ op (TriggerViolation tinfo) = putStrLn (" disabled " ++ trans_type ++ ": " ++ ppTagged (trans_tagged tinfo))+ where trans_type = if trans_is_action tinfo then "action" else "event"++display_transitions = mapM_ display_transition +display_transition trans = do + putStr ("executed transition: \n") + putStr (showTriggerTree trans)+ +display_fact_changes :: State -> State -> IO ()+display_fact_changes prev cur = do+ display_facts "~" (S.toList (M.keysSet (contents prev) `S.difference` M.keysSet (contents cur)))+ display_facts "-" (state_not_holds cur \\ state_not_holds prev)+ display_facts "+" (state_holds cur \\ state_holds prev)+ where display_facts pref fs = mapM_ op fs+ where op f = putStrLn (pref ++ ppTagged f)++display_new_types :: S.Set DomId -> S.Set DomId -> IO ()+display_new_types prev cur = do+ display_type_info "New type " (S.toList (cur `S.difference` prev)) + display_type_info "Removed type " (S.toList (prev `S.difference` cur))+ where display_type_info pref ts = mapM_ op ts+ where op t = putStrLn (pref ++ t)++display_new_invariants :: S.Set DomId -> S.Set DomId -> IO ()+display_new_invariants prev cur = do + display_invariants "New invariant " (cur S.\\ prev)+ display_invariants "Removed invariant " (prev S.\\ cur)+ where display_invariants pref is = mapM_ op (S.toList is)+ where op i = putStrLn (pref ++ i)++display_all_triggers :: Config -> IO ()+display_all_triggers cfg = display_triggers "" (map get_transition (rest_transitions cfg))++display_triggers str tes = display_triggers' tes + where display_triggers' [] = putStrLn ("no " ++ str ++ "actions or events")+ display_triggers' tes = putStrLn (str ++ "actions & events:") >> mapM_ op (zip [1..] tes)+ where op (i, (te,en)) = putStrLn (show i ++ ". " ++ ppTagged te ++ enabled)+ where enabled | en = " (ENABLED)"+ | otherwise = " (DISABLED)"++display :: Config -> IO ()+display cfg = putStrLn (show (cfg_state cfg))++display_spec :: Config -> String -> IO ()+display_spec ctx mty = case find_decl (cfg_spec ctx) ty of+ Nothing -> forM_ (M.assocs (decls (cfg_spec ctx))) (putStrLn . uncurry ppDeclSpec) + Just tspec -> putStrLn (ppDeclSpec ty tspec) + where ty = dropWhile isSpace mty
+ src/Server.hs view
@@ -0,0 +1,1033 @@+{-# 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+ NonDeterministicTransition -> object [ "error-type" .= JSON.String "non-deterministic transition"]+ NotTriggerable te -> object ["error-type" .= JSON.String "not triggerable"+ ,"value" .= TaggedJSON te ]+ 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 "NonDeterministicTransition or NotTriggerable or CompilationError" $ \o -> do+ errortype <- o .: "error-type"+ case errortype of+ "non-deterministic transition" -> return NonDeterministicTransition+ "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)),..}