eflint 3.0.0.2 → 3.1.0.0

raw patch · 14 files changed

+380/−201 lines, 14 filesdep ~basedep ~exploring-interpretersdep ~gllPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, exploring-interpreters, gll

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−3
• eflint.cabal +10/−10
• src/Language/EFLINT/Eval.hs +15/−5
• src/Language/EFLINT/Explorer.hs +3/−3
• src/Language/EFLINT/Interpreter.hs +23/−6
• src/Language/EFLINT/JSON.hs +8/−2
• src/Language/EFLINT/Options.hs +3/−19
• src/Language/EFLINT/Parse.hs +83/−41
• src/Language/EFLINT/Print.hs +9/−2
• src/Language/EFLINT/Spec.hs +78/−20
• src/Language/EFLINT/State.hs +27/−21
• src/Language/EFLINT/StaticEval.hs +63/−39
• src/REPL.hs +26/−20
• src/Server.hs +27/−10

@@ -1,5 +1,7 @@-# Revision history for flint-simulation+# Revision history for package `eflint`  -## 0.1.0.0 -- YYYY-mm-dd+## 3.1.0.0 (2023/05/22)   -* First version. Released on an unsuspecting world.+* Started using changelog.++Last significant update: inclusion of 'instance queries' of the form `?- <EXPR>.` 

@@ -1,7 +1,7 @@ cabal-version:       >=1.10  name:                eflint -version:             3.0.0.2+version:             3.1.0.0 synopsis:            Simulation interpreter for FLINT policy descriptions description: @@ -42,11 +42,11 @@                  Language.EFLINT.Interpreter                  Language.EFLINT.Util                  Language.EFLINT.Options-  build-depends:       base >=4.9 && < 4.15+  build-depends:       base >=4.9 && < 5                        , containers >=0.5 && <0.7                       , hxt >= 9.3.1.16                       , time >= 1.8.0.2-                      , gll >= 0.4.0.13+                      , gll >= 0.4.1.0                       , regex-applicative >= 0.3.3                       , aeson >= 1.4.6.0                       , bytestring >= 0.10.8.2@@ -54,7 +54,7 @@                       , text >= 1.2.4.0                       , filepath >= 1.4.2                       , directory >= 1.3.6-                      , exploring-interpreters >= 1.3.0.0+                      , exploring-interpreters >= 1.4.0.0                       , fgl >= 5.7                        , mtl >= 2.2    hs-source-dirs:      src@@ -76,11 +76,11 @@                  Language.EFLINT.Interpreter                  Language.EFLINT.Util                  Language.EFLINT.Options-  build-depends:       base >=4.9 && < 4.15+  build-depends:       base >=4.9 && < 5                        , containers >=0.5 && <0.7                       , hxt >= 9.3.1.16                       , time >= 1.8.0.2-                      , gll >= 0.4.0.13+                      , gll >= 0.4.1.0                       , regex-applicative >= 0.3.3                       , aeson >= 1.4.6.0                       , bytestring >= 0.10.8.2@@ -90,7 +90,7 @@                       , mtl >= 2.2                       , haskeline >= 0.8.1                       , transformers >= 0.5.6-                      , exploring-interpreters >= 1.3.0.0+                      , exploring-interpreters >= 1.4.0.0                       , text   hs-source-dirs:      src   default-language:    Haskell2010@@ -111,18 +111,18 @@                  Language.EFLINT.JSON                  Language.EFLINT.Util                  Language.EFLINT.Options-  build-depends:       base >=4.9 && < 4.15+  build-depends:       base >=4.9 && < 5                        , containers >=0.5 && <0.7                       , hxt >= 9.3.1.16                       , time >= 1.8.0.2-                      , gll >= 0.4.0.13+                      , gll >= 0.4.1.0                       , 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 +                      , exploring-interpreters >= 1.4.0.0                        , fgl >= 5.7                        , mtl >= 2.2    hs-source-dirs:      src

@@ -12,6 +12,7 @@ import Data.List ((\\)) import Data.Maybe (fromJust) import qualified Data.Map as M+import qualified Data.Set as S  data M_Subs a = M_Subs { runSubs :: Spec -> State -> InputMap -> Subs -> Either RuntimeError [a] } @@ -248,20 +249,26 @@           (ass `store_union` ass', is_f || is_f')  instantiate_trans :: Tagged -> M_Subs TransInfo-instantiate_trans te@(v,d) = do +instantiate_trans = instantiate_trans' S.empty++instantiate_trans' :: S.Set Tagged -> Tagged -> M_Subs TransInfo+instantiate_trans' done' te@(v,d) +  | te `S.member` done' = empty+  | otherwise           = 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 Nothing is_enabled (event_effects espec) []-  where do_transition te@(v,d) mActor is_enabled effects ss = do +      Event espec -> do_transition te Nothing is_enabled (event_effects espec) (event_syncs espec)+  where done = te `S.insert` done'+        do_transition te@(v,d) mActor 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 +            sync_infos <- concat <$> mapM (eval_sync' done) ss              let (ss_ass,any_f) = syncTransInfos sync_infos             ass' <- store_unions <$> mapM eval_effect effects             let ass = ass' `store_union` ss_ass@@ -270,7 +277,10 @@                           _                -> Nothing  eval_sync :: Sync -> M_Subs [TransInfo]-eval_sync (Sync xs t) = foreach xs (whenTagged (eval t) instantiate_trans)+eval_sync = eval_sync' S.empty++eval_sync' :: S.Set Tagged -> Sync -> M_Subs [TransInfo]+eval_sync' done (Sync xs t) = foreach xs (whenTagged (eval t) (instantiate_trans' done))  eval_effect :: Effect -> M_Subs Store eval_effect (CAll xs t) = M.fromList . map (,HoldsTrue) <$> foreach xs (whenTagged (eval t) return)

@@ -8,7 +8,7 @@ import Language.EFLINT.Print()  import qualified Language.Explorer.Pure as EI-import Language.Explorer.Monadic (jump)+import Language.Explorer.Monadic (revert, jump)  import Data.Tree (drawTree, Tree(..)) @@ -18,7 +18,7 @@  data Instruction = Execute [Program] InputMap                  | ExecuteOnce Program InputMap-                 | Revert Ref +                 | Revert Ref Bool {- whether the revert is destructive or not -}                   | 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@@ -100,7 +100,7 @@         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 +  Revert r d -> case (if d then revert else 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)

@@ -2,7 +2,7 @@  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+                   ,errors, violations, ex_triggers, query_ress, inst_query_ress, missing_inputs                    ,convert_programs, collapse_programs) where  import Language.EFLINT.Eval@@ -34,7 +34,8 @@ data Output = ErrorVal Error             | ExecutedTransition TransInfo              | Violation Violation-            | QueryRes QueryRes -- whether query succeed or not+            | QueryRes QueryRes -- whether query succeed or not +            | InstQueryRes [Tagged]             deriving (Eq, Show, Read)  convert_programs :: [Phrase] -> [Program]@@ -99,6 +100,11 @@   where op (QueryRes b) = [b]         op _ = [] +inst_query_ress :: [Output] -> [[Tagged]]+inst_query_ress = concatMap op+  where op (InstQueryRes vs) = [vs]+        op _                 = []+ missing_inputs :: [Output] -> [Tagged] missing_inputs = S.toList . S.fromList . concatMap op   where op (ErrorVal (RuntimeError (MissingInput te))) = [te]@@ -122,6 +128,8 @@                  let queryRes | all (== (ResBool True)) vs = QuerySuccess                               | otherwise                  = QueryFailure                  tell [QueryRes queryRes] >> no_effect+  CInstQuery vs t -> error_or_process (foreach vs (whenTagged (eval (When t (Present t))) return)) spec state inpm $ \vs -> +                      do tell [InstQueryRes (concat vs)] >> 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)@@ -152,7 +160,7 @@                   , ctx_transitions = concat tss                   , ctx_duties = duties                    }-          where state' = rebase_and_sat spec (make_assignments ass state)+          where state' = rebase_and_sat spec (make_assignments spec' ass state)                 spec'  = process_directives dirs spec          no_effect :: OutputWriter (Maybe Context)@@ -170,11 +178,20 @@         consider_transinfos [Left d] = tell [ErrorVal (NotTriggerable d)] >> no_effect         consider_transinfos [Right infos] = do           forM_ infos $ \info -> do  tell [ExecutedTransition info]-                                     when (trans_is_action info && trans_forced info) -                                       (tell [Violation (TriggerViolation info)])+                                     tell_violations info           return_context (store_unions (map trans_assignments infos)) []          consider_transinfos _ = error "ASSERT: consider_transinfos" +tell_violations :: TransInfo -> OutputWriter ()+tell_violations info +  | trans_is_action info = +      -- report whether this action is violated (potentially caused by any successor)+      -- if not violated, then so will not any successor+      when (trans_forced info) (tell [Violation (TriggerViolation info)])+  | otherwise = +      -- report whether successors are violated, given that they could be actions+      mapM_ tell_violations (trans_syncs info) + find_inv_violations :: [DomId] -> M_Subs [Violation] find_inv_violations ds = do    spec <- get_spec @@ -232,5 +249,5 @@     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)+      [sto] -> rebase_and_sat spec (make_assignments spec sto emptyState)       _     -> error "non-deterministic state initialisation"          

@@ -30,6 +30,7 @@     kind = Spec.Act aspec   , domain = Products args    , domain_constraint = BoolLit True+  , restriction = Nothing   , derivation = [HoldsWhen condition_term]   , closed = True    , conditions = []  @@ -42,7 +43,8 @@         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 = [] }+                        , syncs = []+                        , physical = False }           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) @@ -59,6 +61,7 @@   , domain = Products $ [no_decoration (duty_holder d)                         ,no_decoration (claimant d)] ++ objects   , domain_constraint = BoolLit True+  , restriction = Nothing   , derivation = case (derivation :: Duty -> Maybe Binder) d of        Nothing -> []        Just b  -> [dv (duty d) (vars b) (binder_expression b)]@@ -66,7 +69,9 @@   , conditions = []   }   where dspec = DutySpec {enforcing_acts = maybe [] (:[]) (enforcing d)-                         ,violated_when = []}+                         ,violated_when = []+                         ,terminating_acts = []+                         ,creating_acts = []}         objects | all isSpace (duty_components d) = []                 | otherwise                       = [no_decoration (duty_components d)] @@ -79,6 +84,7 @@                               _                                   -> Products []                 Just dom -> tDomain dom   , domain_constraint = BoolLit True+  , restriction = Nothing   , derivation = case function f of       ImplicitDV expr  -> case expr of            RefExpr (BaseVar "[]")    -> [] --Just (Dv [] (When (App (fact f) (Right [])) (BoolLit True)))

@@ -110,28 +110,12 @@                 "n"     -> False                  _       -> False -verbosity :: Options -> Int -> IO () -> IO ()-verbosity opts loc m = do +verbosity :: Options -> Level -> IO () -> IO ()+verbosity opts loc_level m = do    limit <- limitM <$> readIORef opts-  when (level <= limit) m+  when (loc_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)

@@ -19,8 +19,8 @@   , 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" +                , "Extend", "Event", "Act", "Fact", "Physical", "Bool", "Var", "Function", "Invariant", "Predicate", "Duty", "Actor", "Holder", "Claimant", "Recipient", "Related to", "Conditioned by", "Creates", "Terminates", "Obfuscates", "Terminated by", "Created by", "With" , "Identified by", "Derived from", "Derived externally", "Enforced by", "Syncs with"+                , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-"                  , "#", "##", "###", "####"                 , "#include", "#require"                 ]@@ -146,52 +146,74 @@ parse_flint = parse_component flint  declarations :: BNF Token [Decl]-declarations = "declarations" <:=> multiple1 frame +declarations = "declarations" <:=> concat <$$> multiple1 frame   placeholder :: BNF Token Decl placeholder = "placeholder-decl" <:=> PlaceholderDecl <$$ keyword "Placeholder" <**> id_lit <** keyword "For" <**> id_lit -frame :: BNF Token Decl+frame :: BNF Token [Decl] frame = "frame" <:=> fact                  <||> duty -                <||> act +                <||> act+                <||> physical                  <||> event -                <||> syn_ext-                <||> placeholder +                <||> (:[]) <$$> syn_ext+                <||> (:[]) <$$> placeholder    where fact = syn_fact_decl (make_fact False False)-          <||> syn_actor_decl (make_fact False True)+          <||> syn_bool_fact_decl make_bool_fact +          <||> syn_actor_decl (\d -> make_fact False True d Nothing)           <||> 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 make_fact :: Bool -> Bool -> Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> [Decl]+                make_fact inv is_actor is_closed restr ty dom dom_filter clauses = +                 [TypeDecl ty tspec, TypeExt ty clauses]                  where tspec = TypeSpec  { kind = Fact (FactSpec inv is_actor)                                          , domain = dom                                          , domain_constraint = dom_filter+                                         , restriction = restr                                          , derivation = []                                          , closed = is_closed                                          , conditions = [] }-                make_pred inv ty t = make_fact inv False True ty (Products []) (BoolLit True) [DerivationCl [HoldsWhen t]]+                make_pred inv ty t = make_fact inv False True Nothing ty (Products []) (BoolLit True) [DerivationCl [HoldsWhen t]]                 make_inv ty t = make_pred True ty t+                make_bool_fact is_closed ty clauses = +                  make_fact False False is_closed Nothing ty (Products []) (BoolLit True) clauses           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+                  [TypeDecl ty tspec, TypeExt ty clauses]                  where tspec = TypeSpec {-                        kind = Act (ActSpec {effects = [], syncs = []} ),+                        kind = Act (ActSpec {effects = [], syncs = [], physical = False } ),                         domain = Products (actor:(maybe [] (:[]) mrec ++ attrs)),                          domain_constraint = dom_filter,+                        restriction = Nothing,                          derivation = [],                         closed = is_closed,                          conditions = [] }                        actor = maybe (no_decoration "actor") id mact +        physical = syn_physical_decl make_physical+          where make_physical ty mact attrs dom_filter clauses = +                  [TypeDecl ty tspec, TypeExt ty (holds_true:clauses)]+                 where tspec = TypeSpec {+                        kind = Act (ActSpec { effects = [], syncs = [], physical = True }),+                        domain = Products (actor:attrs),+                        domain_constraint = dom_filter,+                        restriction = Nothing,+                        derivation = [],+                        closed = True,+                        conditions = [] }+                       actor = maybe (no_decoration "actor") id mact+                       holds_true = DerivationCl [HoldsWhen (BoolLit True)]+         event = syn_event_decl make_event            where make_event is_closed ty attrs dom_filter clauses =-                 TypeDecl ty $ apply_type_ext ty clauses tspec+                 [TypeDecl ty tspec, TypeExt ty clauses]                  where tspec = TypeSpec {-                          kind = Event (EventSpec { event_effects = [] })+                          kind = Event (EventSpec { event_effects = [], event_syncs = [] })                         , domain = Products attrs                         , domain_constraint = dom_filter+                        , restriction = Nothing                         , derivation = []                         , closed = is_closed                         , conditions = []@@ -199,22 +221,34 @@           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 +                  [TypeDecl ty tspec, TypeExt ty clauses]                  where tspec = TypeSpec {                         domain = Products (hold:claim:attrs),                         domain_constraint = dom_filter,-                        kind = Duty (DutySpec { violated_when = [], enforcing_acts = []}), +                        restriction = Nothing,+                        kind = Duty (DutySpec { violated_when = [], enforcing_acts = []+                                              , terminating_acts = [], creating_acts = [] }),                          derivation = [],                          closed = is_closed,                          conditions = []} -syn_fact_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a+syn_fact_decl :: (Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a syn_fact_decl cons = "fact-type-decl" <:=> cons <$$>-  syn_is_closed <** keyword "Fact" <**> id_lit <**>+  syn_is_closed <**> fact_restriction_by_keyword <**> id_lit <**>   optionalWithDef (keyword "Identified by" **> type_expr) AnyString <**>   syn_domain_constraint <**>    syn_fact_clauses +fact_restriction_by_keyword :: BNF Token (Maybe Restriction)+fact_restriction_by_keyword = "restricted-fact" <:=> +                Nothing                   <$$ keyword "Fact"+          <||>  Just VarRestriction       <$$ keyword "Var"+          <||>  Just FunctionRestriction  <$$ keyword "Function"++syn_bool_fact_decl :: (Bool -> DomId -> [ModClause] -> a) -> BNF Token a+syn_bool_fact_decl cons = "bool-fact-type-decl" <:=> cons <$$>+  syn_is_closed <** keyword "Bool" <**> id_lit <**> syn_fact_clauses + syn_ext :: BNF Token Decl syn_ext = "type-ext" <:=>    keyword "Extend" **> (    syn_fact_ext @@ -264,9 +298,18 @@   objects <**> syn_domain_constraint <**>    syn_event_clauses  +syn_physical_decl :: (DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a+syn_physical_decl cons = "physical-type-decl" <:=> cons <$$+  keyword "Physical" <**> id_lit <** optional (keyword "With") <**>+  optional (keyword "Actor" **> 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_physical_ext = "physical-type-ext" <:=> TypeExt <$$ keyword "Physical" <**> id_lit <**> syn_physical_clauses + syn_event_ext :: BNF Token Decl syn_event_ext = "event-type-ext" <:=> TypeExt <$$ keyword "Event" <**> id_lit <**> syn_event_clauses  @@ -283,6 +326,14 @@ syn_fact_clauses = multiple syn_fact_clause  where syn_fact_clause = "fact-clause" <:=> ConditionedByCl <$$> precondition'                                        <||> DerivationCl <$$> derivation_from++syn_physical_clauses :: BNF Token [ModClause]+syn_physical_clauses = multiple syn_physical_clause+  where syn_physical_clause = "physical-clause" <:=> ConditionedByCl <$$> precondition'+                                                <||> PostCondCl <$$> creating_post'+                                                <||> PostCondCl <$$> terminating_post'+                                                <||> PostCondCl <$$> obfuscating_post'+                                                <||> SyncCl <$$> synchronisations    syn_event_clauses :: BNF Token [ModClause] syn_event_clauses = multiple syn_event_clause@@ -299,6 +350,8 @@                                         <||> DerivationCl <$$> derivation_from                                         <||> ViolationCl <$$> violation_condition                                          <||> EnforcingActsCl <$$> enforcing_acts_clauses +                                        <||> TerminatedByCl <$$> terminated_by_clauses +                                        <||> CreatedByCl <$$> created_by_clauses   objects :: BNF Token [Var] objects = "related-to" <:=> optionalWithDef (keyword "Related to" **> multipleSepBy1 var (keychar ',')) []@@ -307,6 +360,14 @@ enforcing_acts_clauses = "enforcing-act-clauses"   <:=> keyword "Enforced by" **> multipleSepBy1 id_lit (keychar ',') +terminated_by_clauses :: BNF Token [DomId]+terminated_by_clauses = "terminated-by-clauses"+  <:=> keyword "Terminated by" **> multipleSepBy1 id_lit (keychar ',')++created_by_clauses :: BNF Token [DomId]+created_by_clauses = "created-by-clauses"+  <:=> keyword "Created by" **> multipleSepBy1 id_lit (keychar ',')+ violation_condition :: BNF Token [Term] violation_condition = "violation-conditions"   <:=> keyword "Violated when" **> multipleSepBy1 value_expr (keychar ',')@@ -392,17 +453,10 @@           <:=>  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 '.'@@ -416,19 +470,6 @@             <:=> 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 '.') @@ -453,6 +494,7 @@   <||> keychar '-'  **> opt_foreach Terminate   <||> keychar '~'  **> opt_foreach Obfuscate    <||> PQuery <$$ keychar '?'  <**> value_expr -  <||> PQuery . Not <$$ keyword "!?"  <**> value_expr  +  <||> PQuery . Not <$$ keyword "!?"  <**> value_expr +  <||> keyword "?-" **> opt_foreach PInstQuery    <||> PDeclBlock <$$> declarations  

@@ -16,6 +16,9 @@ ppPhrase :: Phrase -> String ppPhrase p = case p of   PQuery t          -> "?" ++ ppTerm t+  PInstQuery vs t +    | null vs       -> "?-" ++ ppTerm t+    | otherwise     -> "?-" ++ foreach vs (ppTerm t)   PDo t             -> ppTagged t   PTrigger vs t     -> foreach vs $ ppTerm t   Create vs t       -> "+" ++ foreach vs (ppTerm t)@@ -37,6 +40,9 @@   CTerminate vs t -> "-" ++ foreach vs (ppTerm t)   CObfuscate vs t -> "~" ++ foreach vs (ppTerm t)   CQuery t        -> "?" ++ ppTerm t+  CInstQuery vs t +    |null vs      -> "?-" ++ ppTerm t+    |otherwise    -> "?-" ++ foreach vs (ppTerm t)   CPDir dir       -> case dir of    DirInv ty      -> "Invariant " ++ ty    @@ -81,11 +87,12 @@                         ]  -- TODO print syncs(?)+-- TODO recipient? ppAct' domainID domain domain_constr clauses = -  "Act " ++ domainID ++ " Actor " ++ ppVar actor ++ " Recipient " ++ ppVar recipient ++ show_objects+  "Act " ++ domainID ++ " Actor " ++ ppVar actor ++ show_objects     ++ ppConstraint (domain_constr)     ++ ppClauses clauses-  where Products (actor:recipient:objects) = domain+  where Products (actor:objects) = domain         show_objects | null objects = ""                      | otherwise    = " Related to " ++ intercalate ", " (map (\(Var x dec) -> x++dec) objects) 

@@ -7,6 +7,8 @@ import qualified Data.Map as M import qualified Data.Set as S +import Control.Monad (join)+ import Data.Aeson hiding (String) import qualified Data.Aeson as JSON @@ -53,10 +55,14 @@ data Kind       = Fact FactSpec | Act ActSpec | Duty DutySpec | Event EventSpec                 deriving (Ord, Eq, Show, Read) +data Restriction = VarRestriction | FunctionRestriction+                 deriving (Ord, Eq, Show, Read, Enum)+ data TypeSpec   = TypeSpec {                       kind  :: Kind                     , domain :: Domain                     , domain_constraint :: Term+                    , restriction :: Maybe Restriction                     , derivation :: [Derivation]                     , closed :: Bool {- whether closed world assumption is made for this type -}                     , conditions  :: [Term]@@ -73,14 +79,17 @@                 deriving (Ord, Eq, Show, Read)  data DutySpec   = DutySpec {-                      enforcing_acts :: [DomId] --TODO consider moving to outer ast-                    , violated_when  :: [Term] +                      enforcing_acts    :: [DomId] -- for record-keeping only, semantics in static-eval+                    , terminating_acts  :: [DomId] -- for record-keeping only, semantics in static-eval+                    , creating_acts     :: [DomId] -- for record-keeping only, semantics in static-eval+                    , violated_when     :: [Term]                      }                 deriving (Ord, Eq, Show, Read)  data ActSpec    = ActSpec {                       effects     :: [Effect]-                    , syncs       :: [Sync] +                    , syncs       :: [Sync]+                    , physical    :: Bool                      }                 deriving (Ord, Eq, Show, Read) @@ -93,7 +102,8 @@                 deriving (Ord, Eq, Show, Read)  data EventSpec  = EventSpec { -                      event_effects :: [Effect] +                      event_effects :: [Effect]+                    , event_syncs   :: [Sync]                      }                 deriving (Ord, Eq, Show, Read) @@ -124,6 +134,7 @@ emptySpec = Spec { decls = built_in_decls, aliases = M.empty}   where built_in_decls = M.fromList [                             ("int", int_decl)+                          , ("string", string_decl)                           , (actor_ref_address, string_decl) -- used for actor identifiers                           , ("actor", actor_decl)                           ]@@ -137,6 +148,16 @@   where op d tspec res | null (derivation tspec) = res                         | otherwise               = S.insert d res +is_var :: Spec -> DomId -> Bool+is_var spec d = case join $ fmap restriction (M.lookup d (decls spec)) of+  Just VarRestriction -> True+  _                   -> False++is_function :: Spec -> DomId -> Bool+is_function spec d = case join $ fmap restriction (M.lookup d (decls spec)) of+  Just FunctionRestriction -> True+  _                        -> False+ -- 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)@@ -164,6 +185,7 @@             | Terminate [Var] Term             | Obfuscate [Var] Term             | PQuery Term+            | PInstQuery [Var] Term             | PDeclBlock [Decl]             | PSkip             deriving (Eq, Show, Read)@@ -173,11 +195,16 @@           | PlaceholderDecl DomId DomId            deriving (Eq, Show, Read) -introducesName :: Decl -> Bool-introducesName (TypeDecl _ _) = True-introducesName (TypeExt _ _) = False-introducesName (PlaceholderDecl _ _) = True+data CDecl = CTypeDecl DomId TypeSpec+           | CTypeExt DomId [CModClause]+           | CPlaceholderDecl DomId DomId +           deriving (Eq, Show, Read) +isInitialTypeDecl :: Decl -> Bool+isInitialTypeDecl (TypeDecl _ _) = True+isInitialTypeDecl (TypeExt _ _) = False+isInitialTypeDecl (PlaceholderDecl _ _) = False + extend_spec :: [Decl] -> Spec -> Spec extend_spec = flip (foldr op)          where op (TypeDecl ty tyspec) spec = spec { decls = M.insert ty tyspec (decls spec) }@@ -190,31 +217,57 @@                | SyncCl [Sync]                | ViolationCl [Term]                | EnforcingActsCl [DomId]+               | TerminatedByCl [DomId]+               | CreatedByCl [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+data CModClause = CConditionedByCl [Term]+                | CDerivationCl [Derivation]+                | CPostCondCl [Effect]+                | CSyncCl [Sync]+                | CViolationCl [Term]+                | CEnforcingActsCl [DomId]+                | CTerminatedByCl [DomId]+                | CCreatedByCl [DomId]+                deriving (Eq, Show, Read)++enforcing_act_condition :: DomId  {- act id -}-> Term+enforcing_act_condition a = Enabled (App a (Right []))++terminated_by_condition :: DomId {- duty id -} -> DomId {- act id -} -> Term+terminated_by_condition d a = App d (Right [])++terminated_by_precondition :: DomId {- duty id -} -> DomId {- act id -} -> Term+terminated_by_precondition d a = Present (App d (Right []))++created_by_condition :: DomId {- duty id -} -> DomId {- act id -} -> Term+created_by_condition d a = App d (Right [])++apply_type_ext :: DomId -> [CModClause] -> 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) }+        CConditionedByCl conds -> tspec { conditions = conds ++ conditions tspec }+        CDerivationCl dvs -> tspec { derivation = dvs ++ derivation tspec }+        CPostCondCl 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) }+        CSyncCl ss -> tspec { kind = add_syncs (kind tspec) }          where add_syncs (Act aspec) = Act $ aspec { syncs = ss ++ syncs aspec} +               add_syncs (Event espec) = Event $ espec { event_syncs = ss ++ event_syncs espec}                 add_syncs s = s-        ViolationCl vs -> tspec { kind = add_viol_conds (kind tspec) }+        CViolationCl 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) }+        CEnforcingActsCl 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+        CTerminatedByCl as -> tspec { kind = add_terms_acts (kind tspec) }+          where add_terms_acts (Duty dspec) = Duty $ dspec { terminating_acts = as ++ terminating_acts dspec }+                add_terms_acts s = s+        CCreatedByCl as -> tspec { kind = add_create_acts (kind tspec) }+          where add_create_acts (Duty dspec) = Duty $ dspec { creating_acts = as ++ creating_acts dspec }+                add_create_acts s = s  data CPhrase = CDo Tagged            -- execute computed instance              | CTrigger [Var] Term   -- execute instance to be computed@@ -222,6 +275,7 @@              | CTerminate [Var] Term              | CObfuscate [Var] Term              | CQuery Term+             | CInstQuery [Var] Term              | CPOnlyDecls              | CPDir CDirective              | CSeq CPhrase CPhrase@@ -466,6 +520,7 @@ actor_decl = TypeSpec { kind = Fact (FactSpec False True)                       , domain = AnyString                        , domain_constraint = BoolLit True+                      , restriction = Nothing                       , derivation = []                        , conditions = []                       , closed = True@@ -475,6 +530,7 @@ int_decl = TypeSpec {  kind = Fact (FactSpec False False)                      ,  domain = AnyInt                     ,  domain_constraint = BoolLit True+                    ,  restriction = Nothing                     ,  derivation = []                     ,  closed = True                       ,  conditions = [] } @@ -486,6 +542,7 @@ string_decl = TypeSpec  {  kind = Fact (FactSpec False False)                         ,  domain = AnyString                         ,  domain_constraint = BoolLit True+                        ,  restriction = Nothing                         ,  derivation = []                          ,  closed = True                          ,  conditions = [] }@@ -495,6 +552,7 @@   TypeSpec  { kind = Fact (FactSpec False False)             , domain = Strings ss             , domain_constraint = BoolLit True+            , restriction = Nothing             , derivation = []              , closed = True              , conditions = [] }

@@ -50,37 +50,43 @@ 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+make_assignments :: Spec -> Store -> State -> State+make_assignments spec = flip (M.foldrWithKey op)+  where op te@(_,d) HoldsTrue | is_var spec d       = var_assignment te+                              | is_function spec d  = function_assignment te+                              | otherwise           = 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+        create :: Tagged -> State -> State+        create te s = s { contents = M.insert te Info{ value = True, from_sat = False } (contents s) } -derive_all :: [Tagged] -> State -> State-derive_all = flip (foldr derive)+        terminate :: Tagged -> State -> State+        terminate te s = s { contents = M.insert te Info{ value = False, from_sat = False } (contents s) } -create :: Tagged -> State -> State-create te s = s { contents = M.insert te Info{ value = True, from_sat = False } (contents s) }+        obfuscate :: Tagged -> State -> State+        obfuscate te s = s { contents = M.delete te (contents s) } -create_all :: [Tagged] -> State -> State-create_all = flip (foldr create)+        var_assignment :: Tagged -> State -> State+        var_assignment te@(_,d) s = create te $ s { contents = M.mapWithKey op (contents s) }+          where op te@(_,d') i | d == d'   = i { value = False, from_sat = False }+                               | otherwise = i -terminate :: Tagged -> State -> State-terminate te s = s { contents = M.insert te Info{ value = False, from_sat = False } (contents s) }+        function_assignment :: Tagged -> State -> State+        function_assignment te@(Product [f,t], d) s = +          create te $ s { contents = M.mapWithKey op (contents s) }+          where op (Product [f',t'], d') i | d == d' && f == f' = i { value = False, from_sat = False }+                op _ i = i+        function_assignment _ s = 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) }+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 -obfuscate_all :: [Tagged] -> State -> State-obfuscate_all = flip (foldr obfuscate)+derive_all :: [Tagged] -> State -> State+derive_all = flip (foldr derive)  -- | assumes the instance of a closed type holds :: Tagged -> State -> Bool

@@ -9,7 +9,7 @@ import Control.Applicative  import Data.Maybe (isNothing)-import Data.List ((\\))+import Data.List ((\\), partition) import qualified Data.Map as M import qualified Data.Set as S @@ -47,12 +47,15 @@ get_spec :: M_Stc Spec get_spec = M_Stc $ \spec -> Right (spec, spec) -execute_decl :: Decl -> M_Stc ()+insert_typespec :: DomId -> TypeSpec -> M_Stc ()+insert_typespec ty tspec = M_Stc $ \spec -> Right (spec { decls = M.insert ty tspec (decls spec) }, ())++execute_decl :: CDecl -> 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) }+          CPlaceholderDecl f t -> spec { aliases = M.insert f t (aliases spec) }+          CTypeExt ty clauses ->  spec { decls = M.adjust (apply_type_ext ty clauses) ty (decls spec) }+          CTypeDecl ty tspec -> spec { decls = M.insert ty tspec (decls spec) }   in Right (spec', ())  with_spec :: Spec -> M_Stc a -> M_Stc a@@ -117,9 +120,18 @@   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))+  PInstQuery vs t   -> do+    fs <- free_vars t+    let unbounds = S.toList (fs `S.difference` S.fromList vs)+    CInstQuery (vs ++ unbounds) . fst <$> compile_term t   PDeclBlock ds     -> do-    forM_ (filter introducesName ds) execute_decl -    forM_ ds ((execute_decl =<<) . compile_decl)+    -- introduce new types first+    let (type_decls, others) = partition isInitialTypeDecl ds+    forM_ type_decls (\(TypeDecl d tspec) -> insert_typespec d tspec)+    -- then process other type declarations+    forM_ others $ \decl -> do+      decls <- compile_decl decl+      forM_ decls execute_decl     return CPOnlyDecls    where to_stmt (PTrigger vs t) = Trans vs Trigger (Left t)         to_stmt (Create vs t)     = Trans vs AddEvent (Left t)@@ -134,28 +146,40 @@         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 :: Decl -> M_Stc [CDecl]+compile_decl d@(PlaceholderDecl x y) = check_known_type [no_decoration y] +                                       >> return [CPlaceholderDecl x y] compile_decl d@(TypeExt ty clauses) = compile_ext ty clauses -compile_decl d@(TypeDecl ty tspec) = compile_type_spec ty tspec +compile_decl d@(TypeDecl ty tspec) = (:[]) <$> compile_type_spec ty tspec  -compile_ext :: DomId -> [ModClause] -> M_Stc Decl+compile_ext :: DomId -> [ModClause] -> M_Stc [CDecl] 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 +   Just tspec -> concat <$> 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+        ConditionedByCl conds -> to_ext ty . CConditionedByCl <$> mapM (convert_precon ty tspec) conds+        DerivationCl dvs -> to_ext ty . CDerivationCl <$> mapM (compile_derivation xs ty) dvs +        PostCondCl effs -> to_ext ty . CPostCondCl <$> mapM (compile_effect xs) effs +        SyncCl ss -> to_ext ty . CSyncCl <$> mapM (compile_sync xs) ss+        ViolationCl vts -> to_ext ty . CViolationCl <$> mapM (compile_violation_condition ty) vts+        EnforcingActsCl as -> do viols <- mapM compile_enf as +                                 return $ CTypeExt ty [CEnforcingActsCl as] : viols+          where compile_enf a = CTypeExt ty . (:[]) . CViolationCl . (:[]) . fst <$> compile_term (enforcing_act_condition a)+        TerminatedByCl as -> do posts <- mapM compile_termby as+                                holds <- mapM compile_holdsby as+                                return $ [CTypeExt ty [CTerminatedByCl as]] ++ posts ++ holds+          where compile_termby a = CTypeExt a . (:[]) . CPostCondCl . (:[]) <$> compile_effect' TAll xs [] (terminated_by_condition ty a)+                compile_holdsby a = CTypeExt a . (:[]) . CDerivationCl . (:[]) <$> compile_derivation xs a (HoldsWhen (terminated_by_precondition ty a))+        CreatedByCl as -> do posts <- mapM compile_createdby as+                             return $ [CTypeExt ty [CCreatedByCl as]] ++ posts+          where compile_createdby a = CTypeExt a . (:[]) . CPostCondCl . (:[]) <$> compile_effect' CAll xs [] (created_by_condition ty a)         where xs = case domain tspec of Products xs -> xs                                         _           -> [no_decoration ty]+              to_ext ty clause = [CTypeExt ty [clause]]  -compile_type_spec :: DomId -> TypeSpec -> M_Stc Decl +compile_type_spec :: DomId -> TypeSpec -> M_Stc CDecl  compile_type_spec ty tspec = do   with_decl ty tspec $ do -- ensure the declaration is active during its compilation      dom <- get_dom ty@@ -171,7 +195,8 @@     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,..}))+    return (CTypeDecl ty (TypeSpec {domain = domain tspec, closed = closed tspec+                                   ,restriction = restriction tspec, ..}))  check_domain :: DomId -> Domain -> M_Stc () check_domain dty (Products xs) = check_known_type xs @@ -207,18 +232,14 @@   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")+    -- convert syncs+    syncs' <- mapM (compile_sync xs) (event_syncs espec)+    return (Event (espec { event_effects = effects', event_syncs = syncs' } ))+  Duty dspec -> do  vconds <- mapM (compile_violation_condition ty) (violated_when dspec)+                    return $ (Duty (dspec { violated_when = vconds }))   Fact _     -> return k + compile_violation_condition :: DomId -> Term -> M_Stc Term compile_violation_condition dty term = do   domain <- get_dom dty@@ -244,8 +265,8 @@  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 _                   = []+      where op (CTypeDecl ty tspec) = [(ty,tspec)]+            op _                    = []  return (spec {decls = decls_union (decls spec) (M.fromList tspecs) })            compile_derivation :: [Var] -> DomId -> Derivation -> M_Stc Derivation@@ -302,13 +323,16 @@  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')+  TAll xs t -> compile_effect' TAll bound xs t+  CAll xs t -> compile_effect' CAll bound xs t+  OAll xs t -> compile_effect' OAll bound xs t++compile_effect' :: ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect +compile_effect' cons bound 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

@@ -81,8 +81,8 @@         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+        verbosity opts Default $ display_commands+        verbosity opts Default $ display_info opts [] c0 ctx         runInputT defaultSettings (repl opts explorer)     Left errs   -> putStrLn "compilation errors:" >> putStrLn (unlines errs)  @@ -102,14 +102,9 @@    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+      (":choose", mint) -> repl_trigger ctx mint+      (":jump", mint)   -> revert_or_jump False mint sid+      (":revert", mint) -> revert_or_jump True mint sid       (":display", _)   -> lift (display ctx) >> continue exp       (":d", _)         -> lift (display ctx) >> continue exp        (":spec", mty)    -> lift (display_spec ctx mty) >> continue exp@@ -139,6 +134,13 @@           Left err  -> outputStrLn err >> continue exp           Right ps  -> repl_phrases opts emptyInput ps exp >>= continue +        revert_or_jump destr mint sid = case readMaybe (dropWhile isSpace mint) of+          Just sid' -> case run_ exp (Revert sid' destr) of+                InvalidRevert -> outputStrLn ("state id " ++ show sid' ++ " unknown") >> continue exp+                ResultTrans exp outs (old,_) (new,sid) -> +                  lift (display_info opts outs old new) >> continue exp+          _ -> lift display_commands >> continue exp+ 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 = @@ -190,7 +192,7 @@                   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+    []  -> lift (verbosity opts TestMode (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@@ -224,17 +226,21 @@  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)+  verbosity opts TestMode $ display_errors (errors outs) +  verbosity opts TestMode $ display_query_results (query_ress outs)+  verbosity opts TestMode $ display_inst_query_results (inst_query_ress outs)+  verbosity opts Default $ display_transitions (ex_triggers outs)+  verbosity opts Default $ display_violations (violations outs)+  verbosity opts Default $ display_new_types (M.keysSet $ decls $ cfg_spec c0) (M.keysSet $ decls $ cfg_spec cfg)+  verbosity opts Default $ display_fact_changes (cfg_state c0) (cfg_state cfg)+  verbosity opts Default $ 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")+          where op QuerySuccess = verbosity opts Default (putStrLn "query successful")+                op QueryFailure = verbosity opts TestMode (putStrLn "query failed")++        display_inst_query_results vss = forM_ vss $ \vs -> do mapM_ (putStrLn . ppTagged) vs+                                                               putStrLn ""           display_errors [] = return ()         display_errors errs = mapM_ op errs

@@ -175,6 +175,7 @@                 let outs = S.fromList (ex_triggers outputs)                 let errs = S.fromList (errors outputs)                 let qress = query_ress outputs+                let iqress = inst_query_ress outputs                  let transitions = S.fromList (rest_transitions ctx)                 let new_duties = S.fromList (rest_duties ctx) S.\\ S.fromList (rest_duties c0)@@ -185,7 +186,7 @@                 let response = case missing_inputs outputs of                       [] -> CommandSuccess old_id state_id                                             facts_from facts_to created_facts terminated_facts-                                            viols outs errs qress+                                            viols outs errs qress iqress                                             new_duties all_duties                                             new_enabled new_disabled transitions                       ms -> InputRequired ms @@ -200,7 +201,7 @@                 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)+                Revert new_state destr  -> report $ run_ exp (Explorer.Revert new_state destr)                 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@@ -239,7 +240,7 @@                 | CreateEvent Term InputMap                 | TerminateEvent Term InputMap                 | QueryCommand Term InputMap-                | Revert Int+                | Revert Int Bool {- whether the revert is destructive or not -}                 | Status (Maybe Int)                 | Kill                 | GetFacts InputMap@@ -261,7 +262,7 @@                   "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"+                  "revert"      -> Revert <$> v .: "value" <*> (v .: "destructive" <|> return False)                   "action"      -> full_action <|> trigger_action                     where full_action =                             actionCommand <$>@@ -364,7 +365,8 @@                                  (S.Set Violation)                                  (S.Set TransInfo)                                  (S.Set Error) -- errors: compilation + transition-                                 [QueryRes]         -- query results+                                 [QueryRes]     -- query results+                                 [[Tagged]]     -- instance query results                                  (S.Set Tagged) -- new duties                                  (S.Set Tagged) -- all duties in the current state                                  (S.Set Tagged) -- newly enabled transitions@@ -384,7 +386,7 @@   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+                         vs outs errs qress iqress                          new_duties all_duties                          new_enabled new_disabled all_transitions) =     object [ "response"   .= JSON.String "success"@@ -399,6 +401,7 @@            , "output-events" .= toJSON outs            , "errors"     .= toJSON errs            , "query-results" .= toJSON qress+           , "inst-query-results" .= toJSON (map TaggedJSON (concat iqress))             , "new-duties" .= toJSON (map TaggedJSON $ S.toList new_duties)            , "new-enabled-transitions" .= toJSON (map TaggedJSON $ S.toList new_enabled)@@ -541,6 +544,7 @@   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 (InstQueryRes vs)= object [ "output-type" .= JSON.String "inst-query-res", "output" .= toJSON (map TaggedJSON vs)]   toJSON (ErrorVal e)     = object [ "output-type" .= JSON.String "error-val", "output" .= e]  instance FromJSON Output where@@ -637,9 +641,14 @@     kind              <- o .: "kind"     domain            <- o .: "domain"     domain_constraint <- o .: "domain_constraint"+    restriction_text  <- (Just <$> o .: "restriction" <|> return Nothing)     derivation        <- o .: "derivation"     closed            <- o .: "closed"     conditions        <- o .: "conditions"+    let restriction = case restriction_text::Maybe String of  +          Just "var"      -> Just VarRestriction+          Just "function" -> Just FunctionRestriction+          _               -> Nothing     return TypeSpec{..}  instance ToJSON Kind where@@ -677,13 +686,15 @@ instance ToJSON ActSpec where   toJSON actspec = object [     "effects"    .= effects actspec,-    "syncs"      .= syncs actspec+    "syncs"      .= syncs actspec,+    "physical"   .= physical actspec     ]  instance FromJSON ActSpec where   parseJSON = withObject "actspec" $ \o -> do     effects  <- o .: "effects"     syncs  <- o .: "syncs"+    physical <- o .: "physical"     return ActSpec{..}  instance ToJSON Term where@@ -870,24 +881,30 @@  instance ToJSON DutySpec where   toJSON dutyspec = object [-    "enforcing_acts" .= enforcing_acts dutyspec,-    "violated_when"  .= violated_when dutyspec+    "enforcing_acts"    .= enforcing_acts dutyspec,+    "violated_when"     .= violated_when dutyspec,+    "terminating_acts"  .= terminating_acts dutyspec,+    "creating_acts"     .= creating_acts dutyspec     ]  instance FromJSON DutySpec where   parseJSON = withObject "dutyspec" $ \o -> do     enforcing_acts <- o.: "enforcing_acts"+    terminating_acts <- o.: "terminating_acts"+    creating_acts <- o.: "creating_acts"     violated_when <- o.: "violated_when"     return DutySpec{..}  instance ToJSON EventSpec where   toJSON eventspec = object [-    "event_effects" .= event_effects eventspec+      "event_effects" .= event_effects eventspec+    , "event_syncs"   .= event_syncs eventspec     ]  instance FromJSON EventSpec where   parseJSON = withObject "eventspec" $ \o -> do     event_effects <- o.: "event_effects"+    event_syncs   <- o.: "event_syncs"     return EventSpec{..}  instance ToJSON Domain where