updates I/O spec generator to latest syntax changes in Gobra

Author: ArquintL

specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/FactEncoding.hs

@@ -214,6 +214,7 @@ mFunc :: Document d => d
 mFunc = 
     text "ghost" $$
     text "ensures res == (linearFacts(l) subset s && persistentFacts(l) subset s)" $$
+    text "decreases" $$
     text "pure func M(l mset[Fact], s mset[Fact]) (res bool) {" $$
     nest 4 (
         text "// non-persistent facts" $$
@@ -231,6 +232,7 @@ uFunc :: Document d => d
 uFunc = 
     text "ghost" $$
     text "ensures result == s setminus linearFacts(l) union r" $$
+    text "decreases" $$
     text "pure func U(l mset[Fact], r mset[Fact], s mset[Fact]) (result mset[Fact])"
 
 {- ---- -}
@@ -240,6 +242,7 @@ filterIsPersFunc =
     text "ghost" $$
     text "// returns a multiset containing just the persistent facts of l all with multiplicity 1" $$
     text "ensures forall f Fact :: { f # result } (f # result) == (persistent(f) && (f # l) > 0 ? 1 : 0)" $$
+    text "decreases" $$
     text "pure func persistentFacts(l mset[Fact]) (result mset[Fact])"
 
 {- ---- -}
@@ -249,6 +252,7 @@ filterIsLinFunc =
     text "ghost" $$
     text "// returns a multiset containing just the non-persistent facts of l while retaining their multiplicity" $$
     text "ensures forall f Fact :: { f # result } (f # result) == (persistent(f) ? 0 : (f # l))" $$
+    text "decreases" $$
     text "pure func linearFacts(l mset[Fact]) (result mset[Fact])"
 
 

specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/PermissionEncoding.hs

@@ -160,6 +160,7 @@ getPermDef p@(TID.IOSFpred (TID.Perm _ _name) _) =
         functionDefPerm perm@(TID.IOSFpred (TID.Perm _ _) _) n termsWithType retTermWithType =
             text "ghost" $$
             text "requires " <> permApp perm $$
+            text "decreases" $$
             text "pure " <> functionDefDoc (text n) termsWithType (text retTermWithType)
         functionDefPerm _ _ _ _ = error "functionDefPerm called with wrong arguments."
 getPermDef _ = error "getPermDef called with wrong arguments."
@@ -278,6 +279,7 @@ internBIO p@(TID.IOSFpred (TID.Perm TID.Internal_R name) ts) =
         text "requires token(" <> placeSrc <> text ") && " <> permApp p $$
         text "ensures token(" <> placeDst <> text ") && " <> placeDst <> text " == old(" <>
         (getPermApp p !! 0) <> text ")" $$ 
+        text "decreases" $$
         functionDefDoc (text $ "internBIO_" ++ name) argsWithType (parens retTermWithType)
 internBIO _ = error "internBIO not called with the right argument."
 

specification-generator/src/lib/tamigloo-compiler/src/PrettyIOSpecs/Gobra/Utils.hs

@@ -337,7 +337,7 @@ importHeader config importedPackages =
 
 domain :: Document d => String -> d -> d
 domain name doc = 
-    braces' (text ("type " ++ name ++ " domain")) doc
+    braces' (text ("ghost type " ++ name ++ " domain")) doc
 
 
 forallWithTriggerSetting :: Document d => TriggerSetting -> d -> [d] -> d -> d