adding a explicit check for sequence size and surjectivity - fixes #446…

… (#611)
conjure-cp · Nov 13, 2023 · da5e5f3 · da5e5f3
1 parent 2ffcff2
commit da5e5f3
Show file tree

Hide file tree

Showing 6 changed files with 56 additions and 7 deletions.
diff --git a/src/Conjure/Process/ValidateConstantForDomain.hs b/src/Conjure/Process/ValidateConstantForDomain.hs
@@ -19,7 +19,7 @@ import Conjure.Language.Constant
       Constant(ConstantEnum, TypedConstant, ConstantInt, ConstantBool) )
 import Conjure.Language.Definition
     ( Name,
-      NameGen )
+      NameGen, forgetRepr )
 import Conjure.Language.Domain
     ( Domain(DomainBool, DomainUnnamed, DomainEnum, DomainPartition,
              DomainTuple, DomainRecord, DomainVariant, DomainMatrix, DomainInt,
@@ -35,16 +35,16 @@ import Conjure.Language.Domain
       SizeAttr(SizeAttr_MinMaxSize, SizeAttr_None, SizeAttr_Size,
                SizeAttr_MinSize, SizeAttr_MaxSize),
       SetAttr(SetAttr),
-      binRelToAttrName )
+      binRelToAttrName, SequenceAttr (SequenceAttr), JectivityAttr (JectivityAttr_Surjective, JectivityAttr_Bijective) )
 import Conjure.Language.Pretty 
 import Conjure.Language.Type ( TypeCheckerMode )
+import Conjure.Language.Expression
 import Conjure.Language.Instantiate ( instantiateExpression )
 import Conjure.Process.AttributeAsConstraints ( mkAttributeToConstraint )
-import Conjure.Process.Enumerate ( EnumerateDomain )
+import Conjure.Process.Enumerate ( EnumerateDomain, enumerateDomain )
 
 -- containers
-import Data.Set as S ( size, size, toList )
-import Conjure.Language.Expression
+import Data.Set as S ( size, size, fromList, toList, toAscList, difference )
 
 
 -- | Assuming both the value and the domain are normalised
@@ -197,8 +197,29 @@ validateConstantForDomain name
 
 validateConstantForDomain name
     c@(viewConstantSequence -> Just vals)
-    d@(DomainSequence _ _ dInner) = nested c d $
-        mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
+    d@(DomainSequence _ attr dInner) = do
+        case attr of
+            SequenceAttr sizeAttr@(SizeAttr_Size (ConstantInt _ s)) _ | s /= genericLength vals ->
+                failDoc $ vcat
+                    [ "The value is not a member of the domain."
+                    , "Value :" <+> pretty c
+                    , "Domain:" <+> pretty d
+                    , "Reason: Domain attributes are not satisfied."
+                    , "Specifically:" <+> pretty sizeAttr
+                    ]
+            SequenceAttr _ jectivity | jectivity `elem` [JectivityAttr_Surjective, JectivityAttr_Bijective] -> do
+                constants <- enumerateDomain (forgetRepr dInner)
+                let missing = S.toAscList (S.fromList constants `S.difference` S.fromList vals)
+                unless (null missing) $  failDoc $ vcat
+                    [ "The value is not a member of the domain."
+                    , "Value :" <+> pretty c
+                    , "Domain:" <+> pretty d
+                    , "Reason: Domain attributes are not satisfied."
+                    , "Specifically:" <+> pretty JectivityAttr_Surjective
+                    ]
+            _ -> return () 
+        nested c d $
+            mapM_ (\ val -> validateConstantForDomain name val dInner ) vals
 
 validateConstantForDomain name
     c@(viewConstantRelation -> Just valss)

diff --git a/tests/custom/issues/446/inst.param b/tests/custom/issues/446/inst.param
@@ -0,0 +1 @@
+letting s be sequence(1,2,3,4,5)
diff --git a/tests/custom/issues/446/inst2.param b/tests/custom/issues/446/inst2.param
@@ -0,0 +1 @@
+letting s be sequence(1,2,3,4)
diff --git a/tests/custom/issues/446/model.essence b/tests/custom/issues/446/model.essence
@@ -0,0 +1 @@
+given s: sequence (size 5, surjective) of int(1..10)
diff --git a/tests/custom/issues/446/run.sh b/tests/custom/issues/446/run.sh
@@ -0,0 +1,5 @@
+rm -rf conjure-output *.solution
+conjure solve model.essence inst.param 2>&1
+rm -rf conjure-output *.solution
+conjure solve model.essence inst2.param 2>&1
+rm -rf conjure-output *.solution
diff --git a/tests/custom/issues/446/stdout.expected b/tests/custom/issues/446/stdout.expected
@@ -0,0 +1,20 @@
+Generating models for model.essence
+Generated models: model000001.eprime
+Saved under: conjure-output
+Savile Row: model000001.eprime inst.param
+Error:
+    The value is not a member of the domain.
+    Value : sequence(1, 2, 3, 4, 5)
+    Domain: sequence {ExplicitBounded} (size 5, surjective) of int(1..10)
+    Reason: Domain attributes are not satisfied.
+    Specifically: surjective
+Generating models for model.essence
+Generated models: model000001.eprime
+Saved under: conjure-output
+Savile Row: model000001.eprime inst2.param
+Error:
+    The value is not a member of the domain.
+    Value : sequence(1, 2, 3, 4)
+    Domain: sequence {ExplicitBounded} (size 5, surjective) of int(1..10)
+    Reason: Domain attributes are not satisfied.
+    Specifically: size 5