Simplify special form annotations (for #317)

AshleyYakeley · Oct 19, 2024 · e365252 · e365252
1 parent 34a4bd0
commit e365252
Show file tree

Hide file tree

Showing 9 changed files with 38 additions and 35 deletions.
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret/SpecialForm.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret/SpecialForm.hs
@@ -11,9 +11,7 @@ import Pinafore.Language.Type
 
 specialFormArg :: QAnnotation t -> SyntaxAnnotation -> ComposeInner Maybe QInterpreter t
 specialFormArg AnnotAnchor (SAAnchor anchor) = return anchor
-specialFormArg AnnotNonpolarType (SAType st) = lift $ interpretNonpolarType st
-specialFormArg AnnotPositiveType (SAType st) = lift $ interpretType @'Positive st
-specialFormArg AnnotNegativeType (SAType st) = lift $ interpretType @'Negative st
+specialFormArg AnnotType (SAType st) = lift $ interpretNonpolarType st
 specialFormArg _ _ = liftInner Nothing
 
 specialFormArgs :: ListType QAnnotation lt -> [SyntaxAnnotation] -> ComposeInner Maybe QInterpreter (ListProduct lt)
@@ -30,9 +28,7 @@ showSA (SAAnchor _) = "anchor"
 
 showAnnotation :: QAnnotation a -> NamedText
 showAnnotation AnnotAnchor = "anchor"
-showAnnotation AnnotNonpolarType = "type"
-showAnnotation AnnotPositiveType = "type"
-showAnnotation AnnotNegativeType = "type"
+showAnnotation AnnotType = "type"
 
 interpretSpecialForm :: FullNameRef -> Maybe QSpecialForm -> [SyntaxAnnotation] -> QInterpreter QExpression
 interpretSpecialForm name msf annotations = do

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Entity/Open.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Entity/Open.hs
@@ -22,7 +22,7 @@ openEntityLibSection =
                     "An open entity for this anchor. `A` is an open entity type."
                     ["@A", "<anchor>"]
                     "A" $
-                MkQSpecialForm (ConsListType AnnotPositiveType $ ConsListType AnnotAnchor NilListType) $ \(t, (anchor, ())) -> do
+                MkQSpecialForm (ConsListType AnnotType $ ConsListType AnnotAnchor NilListType) $ \(t, (anchor, ())) -> do
                     mtp <- getOpenEntityType t
                     return $
                         case mtp of
@@ -32,7 +32,7 @@ openEntityLibSection =
                                 pt = MkOpenEntity $ MkEntity anchor
                                 in constSealedExpression $ MkSomeOf typef pt
               , specialFormBDS "new" "Generate an open entity. `A` is an open entity type." ["@A"] "Action A" $
-                MkQSpecialForm (ConsListType AnnotPositiveType NilListType) $ \(t, ()) -> do
+                MkQSpecialForm (ConsListType AnnotType NilListType) $ \(t, ()) -> do
                     mtp <- getOpenEntityType t
                     return $
                         case mtp of

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Function.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Function.hs
@@ -36,15 +36,19 @@ functionLibSection =
                 (seq :: TopType -> A -> A)
           , addNameInRootBDS $
             specialFormBDS "check" "Check from a dynamic supertype." ["@A"] "D(A) -> Maybe A" $
-            MkQSpecialForm (ConsListType AnnotNegativeType NilListType) $ \(MkSome tn, ()) -> do
-                MkShimWit dtw (MkPolarShim (MkComposeShim expr)) <- getGreatestDynamicSupertype tn
-                tpw <- invertType tn
-                return $ MkSealedExpression (funcShimWit (mkShimWit dtw) $ maybeShimWit tpw) $ fmap shimToFunction expr
+            MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome npt, ()) -> do
+                let
+                    tn = nonpolarToNegative @QTypeSystem npt
+                    tp = nonpolarToPositive @QTypeSystem npt
+                MkShimWit dtw (MkPolarShim (MkComposeShim expr)) <- getGreatestDynamicSupertypeSW tn
+                return $ MkSealedExpression (funcShimWit (mkShimWit dtw) $ maybeShimWit tp) $ fmap shimToFunction expr
           , addNameInRootBDS $
             specialFormBDS "coerce" "Coerce from a dynamic supertype." ["@A"] "D(A) -> A" $
-            MkQSpecialForm (ConsListType AnnotNegativeType NilListType) $ \(MkSome tn, ()) -> do
-                MkShimWit dtw (MkPolarShim (MkComposeShim expr)) <- getGreatestDynamicSupertype tn
-                tpw <- invertType tn
+            MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome npt, ()) -> do
+                let
+                    tn = nonpolarToNegative @QTypeSystem npt
+                    tp = nonpolarToPositive @QTypeSystem npt
+                MkShimWit dtw (MkPolarShim (MkComposeShim expr)) <- getGreatestDynamicSupertypeSW tn
                 let
                     fromJustOrError :: forall t. Maybe t -> t
                     fromJustOrError =
@@ -54,7 +58,7 @@ functionLibSection =
                                 error $
                                 unpack $ toText $ "coercion from " <> exprShow dtw <> " to " <> exprShow tn <> " failed"
                 return $
-                    MkSealedExpression (funcShimWit (mkShimWit dtw) tpw) $
+                    MkSealedExpression (funcShimWit (mkShimWit dtw) tp) $
                     fmap (\conv t -> fromJustOrError $ shimToFunction conv t) expr
           ]
         ]
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Optics.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Optics.hs
@@ -101,10 +101,12 @@ opticsLibSection =
                           "Prism from greatest dynamic supertype of the given type."
                           ["@T"]
                           "Prism {a,-D(T)} {-a,+T}" $
-                      MkQSpecialForm (ConsListType AnnotNegativeType NilListType) $ \(MkSome (tn :: _ t), ()) -> do
+                      MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome (npt :: _ t), ()) -> do
+                          let
+                              tn = nonpolarToNegative @QTypeSystem npt
+                              tp = nonpolarToPositive @QTypeSystem npt
                           (MkShimWit (dtn :: _ dt) (MkPolarShim (MkComposeShim convexpr))) <-
-                              getGreatestDynamicSupertype tn
-                          tpw <- invertType tn
+                              getGreatestDynamicSupertypeSW tn
                           let
                               vtype :: QShimWit 'Positive (LangPrism '( MeetType A dt, A) '( A, t))
                               vtype =
@@ -115,7 +117,7 @@ opticsLibSection =
                                       (rangeCCRArgument (joinMeetShimWit qType (mkShimWit dtn)) qType) $
                                   consCCRPolarArgumentsShimWit
                                       (nextCCRVariancesMap $ qgtVarianceMap qGroundType)
-                                      (rangeCCRArgument qType tpw) $
+                                      (rangeCCRArgument qType tp) $
                                   nilCCRPolarArgumentsShimWit
                               toVal :: QShim dt (Maybe t) -> LangPrism '( MeetType A dt, A) '( A, t)
                               toVal conv =

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs
@@ -138,7 +138,7 @@ pinaforeLibSection =
               ""
               [ typeBDS "Type" "A (concrete nonpolar) Pinafore type." (qSomeGroundType @_ @LangType) []
               , specialFormBDS "const.Type" "A `Type` for a given type." ["@A"] "Type.Pinafore A" $
-                MkQSpecialForm (ConsListType AnnotNonpolarType NilListType) $ \(MkSome (tw :: _ t), ()) -> let
+                MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome (tw :: _ t), ()) -> let
                     stype :: QShimWit 'Positive (LangType '( t, t))
                     stype =
                         rangeShimWit

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Storage.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Storage.hs
@@ -77,8 +77,7 @@ storageLibSection =
                 "A property for this anchor. `A` and `B` are types that are subtypes of `Entity`."
                 ["@A", "@B", "<anchor>"]
                 "Store -> Property A B" $
-            MkQSpecialForm
-                (ConsListType AnnotNonpolarType $ ConsListType AnnotNonpolarType $ ConsListType AnnotAnchor NilListType) $ \(MkSome ta, (MkSome tb, (anchor, ()))) -> do
+            MkQSpecialForm (ConsListType AnnotType $ ConsListType AnnotType $ ConsListType AnnotAnchor NilListType) $ \(MkSome ta, (MkSome tb, (anchor, ()))) -> do
                 eta <- getMonoStorableType ta
                 etb <- getMonoStorableType tb
                 saaexpr <- monoStoreAdapter eta
@@ -113,7 +112,7 @@ storageLibSection =
                 "Storage of a single value, of the given type, identified by the given anchor. Actually equivalent to `fn store => property @Unit @A <anchor> store !$ {()}`"
                 ["@A", "<anchor>"]
                 "Store -> WholeModel A" $
-            MkQSpecialForm (ConsListType AnnotNonpolarType $ ConsListType AnnotAnchor NilListType) $ \(MkSome ta, (anchor, ())) -> do
+            MkQSpecialForm (ConsListType AnnotType $ ConsListType AnnotAnchor NilListType) $ \(MkSome ta, (anchor, ())) -> do
                 eta <- getMonoStorableType ta
                 saaexpr <- monoStoreAdapter eta
                 MkShimWit rtap (MkPolarShim praContra) <- return $ nonpolarToNegative @QTypeSystem ta
@@ -145,7 +144,7 @@ storageLibSection =
                 "Storage of a set of values, of the given type, identified by the given anchor. Actually equivalent to `fn store => property @A @Unit <anchor> store !@ {()}`"
                 ["@A", "<anchor>"]
                 "Store -> FiniteSetModel {-Entity,A}" $
-            MkQSpecialForm (ConsListType AnnotNonpolarType $ ConsListType AnnotAnchor NilListType) $ \(MkSome (ta :: _ a), (anchor, ())) -> do
+            MkQSpecialForm (ConsListType AnnotType $ ConsListType AnnotAnchor NilListType) $ \(MkSome (ta :: _ a), (anchor, ())) -> do
                 eta <- getMonoStorableType ta
                 saaexpr <- monoStoreAdapter eta
                 MkShimWit rtap (MkPolarShim praContra) <- return $ nonpolarToNegative @QTypeSystem ta
@@ -185,7 +184,7 @@ storageLibSection =
                 "Fetch the full value of an `Entity` from storage, or stop. Note values are removed from storage when no triple refers to them."
                 ["@A"]
                 "Store -> Entity -> Action A" $
-            MkQSpecialForm (ConsListType AnnotNonpolarType NilListType) $ \(MkSome (ta :: _ a), ()) -> do
+            MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome (ta :: _ a), ()) -> do
                 eta <- getMonoStorableType ta
                 saaexpr <- monoStoreAdapter eta
                 let

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/SpecialForm.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/SpecialForm.hs
@@ -6,6 +6,4 @@ import Pinafore.Language.Type.Ground
 type QAnnotation :: Type -> Type
 data QAnnotation t where
     AnnotAnchor :: QAnnotation Anchor
-    AnnotNonpolarType :: QAnnotation (Some (TSNonpolarWitness QTypeSystem))
-    AnnotPositiveType :: QAnnotation (Some (QType 'Positive))
-    AnnotNegativeType :: QAnnotation (Some (QType 'Negative))
+    AnnotType :: QAnnotation (Some QNonpolarType)
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Type/GetDynamicSupertype.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Type/GetDynamicSupertype.hs
@@ -3,6 +3,7 @@ module Pinafore.Language.Type.GetDynamicSupertype
     , QExprShimWit
     , QExprGroundedShimWit
     , getGreatestDynamicSupertype
+    , getGreatestDynamicSupertypeSW
     , getGroundedShimWitGreatestDynamicSupertype
     , getOptGreatestDynamicSupertype
     , getOptGreatestDynamicSupertypeSW
@@ -72,6 +73,11 @@ getGreatestDynamicSupertype (ConsDolanType t1 tr) = do
     tr' <- getGreatestDynamicSupertype tr
     return $ mapShimWit zip2 $ joinMeetShimWit t1' tr'
 
+getGreatestDynamicSupertypeSW :: QShimWit 'Negative t -> Interpreter (QExprShimWit 'Negative (Maybe t))
+getGreatestDynamicSupertypeSW (MkShimWit t (MkPolarShim conv)) = do
+    t' <- getGreatestDynamicSupertype t
+    return $ mapShimWit (MkPolarShim $ pureComposeShim $ cfmap conv) t'
+
 getOptGreatestDynamicSupertype :: QType 'Negative t -> Interpreter (Maybe (QExprShimWit 'Negative (Maybe t)))
 getOptGreatestDynamicSupertype (ConsDolanType t1 NilDolanType) = do
     mt1' <- getOptSingleGreatestDynamicSupertype t1

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Type/Storable/OpenEntity.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Type/Storable/OpenEntity.hs
@@ -57,9 +57,7 @@ openEntityGroundType oet = let
     props = singleGroundProperty storabilityProperty storability
     in singleGroundType' (MkFamilialType openEntityFamilyWitness $ MkOpenEntityFamily oet) props $ exprShowPrec oet
 
-getOpenEntityType :: Some (QType 'Positive) -> QInterpreter (Some OpenEntityType)
-getOpenEntityType (MkSome tm) =
-    case dolanToMaybeType @QGroundType @_ @_ @QShim tm of
-        Just (MkShimWit (MkDolanGroundedType gt NilCCRArguments) _)
-            | Just (MkOpenEntityFamily oet) <- getGroundFamily openEntityFamilyWitness gt -> return $ MkSome oet
-        _ -> throw $ InterpretTypeNotOpenEntityError $ exprShow tm
+getOpenEntityType :: Some QNonpolarType -> QInterpreter (Some OpenEntityType)
+getOpenEntityType (MkSome (GroundedNonpolarType (MkNonpolarGroundedType gt NilCCRArguments)))
+    | Just (MkOpenEntityFamily oet) <- getGroundFamily openEntityFamilyWitness gt = return $ MkSome oet
+getOpenEntityType tm = throw $ InterpretTypeNotOpenEntityError $ exprShow tm