eflint 3.1.0.0 → 3.1.0.1

raw patch · 7 files changed

+29/−17 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−2
• eflint.cabal +1/−1
• src/Language/EFLINT/Interpreter.hs +5/−2
• src/Language/EFLINT/Parse.hs +3/−2
• src/Language/EFLINT/Print.hs +10/−6
• src/Language/EFLINT/Spec.hs +2/−2
• src/Language/EFLINT/StaticEval.hs +2/−2

@@ -1,7 +1,11 @@ # Revision history for package `eflint`  -## 3.1.0.0 (2023/05/22)  +## 3.1.0.0 (2023/04/22)    * Started using changelog. -Last significant update: inclusion of 'instance queries' of the form `?- <EXPR>.` +Last significant update: inclusion of 'instance queries' of the form `?- <EXPR>.`++## 3.1.0.1 (2023/04/24)++Added an additional form of instance query of the form `?-- <EXPR>.` as syntactic sugar for `?- <EXPR> When Holds(<EXPR>).`

@@ -1,7 +1,7 @@ cabal-version:       >=1.10  name:                eflint -version:             3.1.0.0+version:             3.1.0.1 synopsis:            Simulation interpreter for FLINT policy descriptions description: 

@@ -128,8 +128,11 @@                  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+  CInstQuery b vs t -> +    let t' | b         = When t (Present t)+           | otherwise = t+    in error_or_process (foreach vs (whenTagged (eval t') return)) spec state inpm $ \vs -> +                      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)

@@ -20,7 +20,7 @@                 , "Atom", "String", "Int", "Time", "Current Time"                 , "Exists", "Forall", "Foreach", "Force"                 , "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", "?-" +                , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-", "?--"                  , "#", "##", "###", "####"                 , "#include", "#require"                 ]@@ -495,6 +495,7 @@   <||> keychar '~'  **> opt_foreach Obfuscate    <||> PQuery <$$ keychar '?'  <**> value_expr    <||> PQuery . Not <$$ keyword "!?"  <**> value_expr -  <||> keyword "?-" **> opt_foreach PInstQuery +  <||> keyword "?-" **> opt_foreach (PInstQuery False)+  <||> keyword "?--" **> opt_foreach (PInstQuery True)   <||> PDeclBlock <$$> declarations  

@@ -16,9 +16,11 @@ ppPhrase :: Phrase -> String ppPhrase p = case p of   PQuery t          -> "?" ++ ppTerm t-  PInstQuery vs t -    | null vs       -> "?-" ++ ppTerm t-    | otherwise     -> "?-" ++ foreach vs (ppTerm t)+  PInstQuery b vs t +    | null vs       -> keyw ++ ppTerm t+    | otherwise     -> keyw ++ foreach vs (ppTerm t)+   where keyw | b         = "?--"+              | otherwise = "?-"   PDo t             -> ppTagged t   PTrigger vs t     -> foreach vs $ ppTerm t   Create vs t       -> "+" ++ foreach vs (ppTerm t)@@ -40,9 +42,11 @@   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)+  CInstQuery b vs t +    |null vs      -> keyw ++ ppTerm t+    |otherwise    -> keyw ++ foreach vs (ppTerm t)+   where keyw | b         = "?--"+              | otherwise = "?-"   CPDir dir       -> case dir of    DirInv ty      -> "Invariant " ++ ty    

@@ -185,7 +185,7 @@             | Terminate [Var] Term             | Obfuscate [Var] Term             | PQuery Term-            | PInstQuery [Var] Term+            | PInstQuery Bool {- whether requested instances must hold true -} [Var] Term             | PDeclBlock [Decl]             | PSkip             deriving (Eq, Show, Read)@@ -275,7 +275,7 @@              | CTerminate [Var] Term              | CObfuscate [Var] Term              | CQuery Term-             | CInstQuery [Var] Term+             | CInstQuery Bool {- whether generated instances must be present -} [Var] Term              | CPOnlyDecls              | CPDir CDirective              | CSeq CPhrase CPhrase

@@ -120,10 +120,10 @@   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+  PInstQuery b vs t   -> do     fs <- free_vars t     let unbounds = S.toList (fs `S.difference` S.fromList vs)-    CInstQuery (vs ++ unbounds) . fst <$> compile_term t+    CInstQuery b (vs ++ unbounds) . fst <$> compile_term t   PDeclBlock ds     -> do     -- introduce new types first     let (type_decls, others) = partition isInitialTypeDecl ds