Fix bug with multi-argument polymorphic datatypes (#357)

*Description of changes:*

There is a bug where when a datatype involves multiple polymorphic type
arguments, using a constructor that does not involve both of these
arguments (e.g. `Either`) gives an invalid SMT encoding. This PR fixes
the bug and adds a test case that formerly failed and now passes.


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Josh Cohen <cohenjo@amazon.com>

Author: joscoh

Strata/DL/SMT/Encoder.lean

@@ -202,7 +202,7 @@ def defineApp (inBinder : Bool) (tyEnc : String) (op : Op) (tEncs : List String)
     if tEncs.isEmpty then
       defineTerm inBinder tyEnc s!"(as {name} {tyEnc})"
     else
-      defineTerm inBinder tyEnc s!"({name} {args})"
+      defineTerm inBinder tyEnc s!"((as {name} {tyEnc}) {args})"
   | .datatype_op _ _ =>
     defineTerm inBinder tyEnc s!"({encodeOp op} {args})"
   | _ =>

StrataTest/Languages/Core/PolymorphicDatatypeTest.lean

@@ -176,7 +176,7 @@ assert [lValue] (((~Either..l : (arrow (Either int bool) int)) (x : (Either int
 #eval Core.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram eitherUsePgm)).fst
 
 ---------------------------------------------------------------------
--- Test 9: Nested Polymorphic Types (Option of List)
+-- Test 5: Nested Polymorphic Types (Option of List)
 ---------------------------------------------------------------------
 
 def nestedPolyPgm : Program :=
@@ -316,4 +316,58 @@ Result: ✅ pass
 #guard_msgs in
 #eval verify "cvc5" multiInstSMTPgm Inhabited.default Options.quiet
 
+
+---------------------------------------------------------------------
+-- Test 8: Multiple polymorphic arguments, constructor only needs 1
+---------------------------------------------------------------------
+
+def eitherHavocPgm : Program :=
+#strata
+program Core;
+
+datatype Either (a : Type, b : Type) { Left(l: a), Right(r: b) };
+
+procedure TestEitherHavoc() returns ()
+spec {
+  ensures true;
+}
+{
+  var x : Either int bool;
+
+  x := Left(0);
+  havoc x;
+
+  assume (x == Left(42));
+
+  assert [isLeft]: Either..isLeft(x);
+  assert [notRight]: !Either..isRight(x);
+  assert [leftVal]: Either..l(x) == 42;
+};
+#end
+
+/-- info: true -/
+#guard_msgs in
+#eval TransM.run Inhabited.default (translateProgram eitherHavocPgm) |>.snd |>.isEmpty
+
+/--
+info:
+Obligation: isLeft
+Property: assert
+Result: ✅ pass
+
+Obligation: notRight
+Property: assert
+Result: ✅ pass
+
+Obligation: leftVal
+Property: assert
+Result: ✅ pass
+
+Obligation: TestEitherHavoc_ensures_0
+Property: assert
+Result: ✅ pass
+-/
+#guard_msgs in
+#eval verify "cvc5" eitherHavocPgm Inhabited.default Options.quiet
+
 end Strata.PolymorphicDatatypeTest

StrataTest/Languages/Core/SMTEncoderDatatypeTest.lean

@@ -227,7 +227,7 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestOption (par (α) (
   (None)
   (Some (TestOption..val α)))))
-(define-fun t0 () (TestOption Int) (Some 42))
+(define-fun t0 () (TestOption Int) ((as Some (TestOption Int)) 42))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -240,7 +240,7 @@ info: (declare-datatype TestList (par (α) (
   (Nil)
   (Cons (TestList..head α) (TestList..tail (TestList α))))))
 (define-fun t0 () (TestList Int) (as Nil (TestList Int)))
-(define-fun t1 () (TestList Int) (Cons 1 t0))
+(define-fun t1 () (TestList Int) ((as Cons (TestList Int)) 1 t0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes