Interpretation (#298): Type & OpenType

AshleyYakeley · Oct 20, 2024 · da008d0 · da008d0
1 parent 263dd9f
commit da008d0
Show file tree

Hide file tree

Showing 3 changed files with 58 additions and 39 deletions.
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/Pinafore.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/Pinafore.hs
@@ -8,31 +8,43 @@ import Pinafore.Language.Interpreter
 import Pinafore.Language.Library.Types
 import Pinafore.Language.Type
 
--- LangType
-data LangType (pq :: (Type, Type)) =
-    forall a. MkLangType (QRange a pq)
-                         (QNonpolarType a)
+data LangType =
+    forall a. MkLangType (QNonpolarType a)
 
-instance CatFunctor (CatRange (->)) (->) LangType where
-    cfmap f (MkLangType r v) = MkLangType (cfmap f r) v
+instance HasQGroundType '[] LangType where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangType)|]) "Type.Pinafore."
+
+instance ShowText LangType where
+    showText (MkLangType t) = toText $ exprShow t
+
+-- LangOpenType
+data LangOpenType (pq :: (Type, Type)) =
+    forall a. MkLangOpenType (QRange a pq)
+                             (QNonpolarType a)
 
-instance ShowText (LangType pq) where
-    showText (MkLangType _ v) = toText $ exprShow v
+instance CatFunctor (CatRange (->)) (->) LangOpenType where
+    cfmap f (MkLangOpenType r v) = MkLangOpenType (cfmap f r) v
 
-instance MaybeRepresentational LangType where
+instance ShowText (LangOpenType pq) where
+    showText (MkLangOpenType _ v) = toText $ exprShow v
+
+instance MaybeRepresentational LangOpenType where
     maybeRepresentational = Nothing
 
-instance HasCCRVariance 'RangeCCRVariance LangType
+instance HasCCRVariance 'RangeCCRVariance LangOpenType
 
-instance HasQGroundType '[ RangeCCRVariance] LangType where
-    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangType)|]) "Type.Pinafore."
+instance HasQGroundType '[ RangeCCRVariance] LangOpenType where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangOpenType)|]) "OpenType.Pinafore."
+
+openLangTypeToType :: forall p q. LangOpenType '( p, q) -> LangType
+openLangTypeToType (MkLangOpenType _ t) = MkLangType t
 
 mkLangTypeValue :: Some QNonpolarType -> QValue
 mkLangTypeValue (MkSome (tw :: _ t)) = let
-    stype :: QShimWit 'Positive (LangType '( t, t))
+    stype :: QShimWit 'Positive (LangOpenType '( t, t))
     stype = rangeShimWit qGroundType (nonpolarToNegative @QTypeSystem tw) (nonpolarToPositive @QTypeSystem tw)
-    sval :: LangType '( t, t)
-    sval = MkLangType identityRange tw
+    sval :: LangOpenType '( t, t)
+    sval = MkLangOpenType identityRange tw
     in MkSomeOf stype sval
 
 -- QInterpreter

diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs
@@ -41,14 +41,14 @@ langRunInterpreter (MkQContext lc) ia = let
            rea <- runInterpretResult $ runPinaforeScoped "<evaluate>" ia
            return $ mapResultFailure showText rea
 
-langTypePositive :: LangType '( p, q) -> QShimWit 'Positive p
-langTypePositive (MkLangType r t) = mapShimWit (MkPolarShim $ rangeContra r) $ nonpolarToPositive @QTypeSystem t
+langTypePositive :: LangOpenType '( p, q) -> QShimWit 'Positive p
+langTypePositive (MkLangOpenType r t) = mapShimWit (MkPolarShim $ rangeContra r) $ nonpolarToPositive @QTypeSystem t
 
-langTypeNegative :: LangType '( p, q) -> QShimWit 'Negative q
-langTypeNegative (MkLangType r t) = mapShimWit (MkPolarShim $ rangeCo r) $ nonpolarToNegative @QTypeSystem t
+langTypeNegative :: LangOpenType '( p, q) -> QShimWit 'Negative q
+langTypeNegative (MkLangOpenType r t) = mapShimWit (MkPolarShim $ rangeCo r) $ nonpolarToNegative @QTypeSystem t
 
-langUnifyTypes :: LangType '( A, TopType) -> LangType '( BottomType, B) -> QInterpreter (A -> B)
-langUnifyTypes ta tb = fmap shimToFunction $ qUnifyRigid (langTypePositive ta) (langTypeNegative tb)
+langUnifyOpenTypes :: LangOpenType '( A, TopType) -> LangOpenType '( BottomType, B) -> QInterpreter (A -> B)
+langUnifyOpenTypes ta tb = fmap shimToFunction $ qUnifyRigid (langTypePositive ta) (langTypeNegative tb)
 
 -- LangValue
 newtype LangValue = MkLangValue
@@ -58,7 +58,7 @@ newtype LangValue = MkLangValue
 instance HasQGroundType '[] LangValue where
     qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangValue)|]) "Value.Pinafore."
 
-mkLangValue :: LangType '( A, TopType) -> A -> LangValue
+mkLangValue :: LangOpenType '( A, TopType) -> A -> LangValue
 mkLangValue t v = MkLangValue $ MkSomeOf (langTypePositive t) v
 
 interpretToExpression :: Text -> QInterpreter LangExpression
@@ -74,7 +74,7 @@ interpretToValue src = do
     expr <- interpretToExpression src
     evaluateLangExpression expr
 
-langUnifyValue :: LangType '( BottomType, A) -> LangValue -> QInterpreter A
+langUnifyValue :: LangOpenType '( BottomType, A) -> LangValue -> QInterpreter A
 langUnifyValue t (MkLangValue v) = qUnifyValueTo (langTypeNegative t) v
 
 langWithScope :: QScopeDocs -> QInterpreter A -> QInterpreter A
@@ -120,19 +120,26 @@ pinaforeLibSection =
               "Type"
               ""
               [ typeBDS "Type" "A (concrete nonpolar) Pinafore type." (qSomeGroundType @_ @LangType) []
-              , specialFormBDS "const.Type" "A `Type` for a given type." ["@A"] "Type.Pinafore A" $
+              , hasSubtypeRelationBDS @LangType @Showable Verify "" $ functionToShim "show" textShowable
+              ]
+        , headingBDS
+              "OpenType"
+              ""
+              [ typeBDS "OpenType" "A (concrete nonpolar) Pinafore type." (qSomeGroundType @_ @LangOpenType) []
+              , specialFormBDS "const.OpenType" "An `OpenType` for a given type." ["@A"] "OpenType.Pinafore A" $
                 MkQSpecialForm (ConsListType AnnotType NilListType) $ \(MkSome (tw :: _ t), ()) -> let
-                    stype :: QShimWit 'Positive (LangType '( t, t))
+                    stype :: QShimWit 'Positive (LangOpenType '( t, t))
                     stype =
                         rangeShimWit
                             qGroundType
                             (nonpolarToNegative @QTypeSystem tw)
                             (nonpolarToPositive @QTypeSystem tw)
-                    sval :: LangType '( t, t)
-                    sval = MkLangType identityRange tw
+                    sval :: LangOpenType '( t, t)
+                    sval = MkLangOpenType identityRange tw
                     in return $ constSealedExpression $ MkSomeOf stype sval
-              , hasSubtypeRelationBDS @(LangType '( P, Q)) @Showable Verify "" $ functionToShim "show" textShowable
-              , namespaceBDS "Type" [valBDS "unify" "Unify two `Type`s." langUnifyTypes]
+              , hasSubtypeRelationBDS @(LangOpenType '( P, Q)) @LangType Verify "" $
+                functionToShim "openLangTypeToType" openLangTypeToType
+              , namespaceBDS "OpenType" [valBDS "unify" "Unify two `OpenType`s." langUnifyOpenTypes]
               ]
         , headingBDS
               "Expression"

diff --git a/Pinafore/pinafore-language/test/Test/Entity.hs b/Pinafore/pinafore-language/test/Test/Entity.hs
@@ -1762,22 +1762,22 @@ testEntity =
           tGroup
               "evaluate"
               [ testExpectSuccess "pass"
-              , testExpectSuccess "testaction (Success True) $ evaluate (const.Type @Boolean) \"True\""
-              , testExpectSuccess "testaction (Success 5) $ evaluate (const.Type @Integer) \"5\""
-              , testExpectSuccess "testaction (Success 5) $ evaluate (const.Type @Integer) \"let {x = 5} x\""
+              , testExpectSuccess "testaction (Success True) $ evaluate (const.OpenType @Boolean) \"True\""
+              , testExpectSuccess "testaction (Success 5) $ evaluate (const.OpenType @Integer) \"5\""
+              , testExpectSuccess "testaction (Success 5) $ evaluate (const.OpenType @Integer) \"let {x = 5} x\""
               , testExpectSuccess
-                    "do {ar <- evaluate (const.Type @(Integer -> Integer)) \"fn x => x +.Integer 1\"; ar >- fn {Failure err => fail err; Success f => testeq 8 $ f 7}}"
+                    "do {ar <- evaluate (const.OpenType @(Integer -> Integer)) \"fn x => x +.Integer 1\"; ar >- fn {Failure err => fail err; Success f => testeq 8 $ f 7}}"
               , testExpectSuccess
-                    "testaction (Failure \"<evaluate>:1:1: syntax: expecting: expression\") $ evaluate (const.Type @Integer) \"\""
+                    "testaction (Failure \"<evaluate>:1:1: syntax: expecting: expression\") $ evaluate (const.OpenType @Integer) \"\""
               , testExpectSuccess
-                    "testaction (Failure \"<evaluate>:1:1: undefined: f: a\") $ evaluate (const.Type @Integer) \"f\""
-              , testExpectSuccess "testFailure $ evaluate (const.Type @Integer) \"\\\"hello\\\"\""
+                    "testaction (Failure \"<evaluate>:1:1: undefined: f: a\") $ evaluate (const.OpenType @Integer) \"f\""
+              , testExpectSuccess "testFailure $ evaluate (const.OpenType @Integer) \"\\\"hello\\\"\""
               , testExpectSuccess
-                    "do {r <- newMem.WholeModel; ar <- evaluate (const.Type @(WholeModel Integer -> Action Unit)) \"fn r => r :=.WholeModel 45\"; runresult ar r; a <- get r; testeq 45 a;}"
+                    "do {r <- newMem.WholeModel; ar <- evaluate (const.OpenType @(WholeModel Integer -> Action Unit)) \"fn r => r :=.WholeModel 45\"; runresult ar r; a <- get r; testeq 45 a;}"
               , testExpectSuccess
-                    "testaction 569 $ evaluate (const.Type @(a -> a)) \"fn x => x\" >>= fn Success f => pure $ f 569"
+                    "testaction 569 $ evaluate (const.OpenType @(a -> a)) \"fn x => x\" >>= fn Success f => pure $ f 569"
               , testExpectSuccess
-                    "testaction 570 $ evaluate (const.Type @(Integer -> Integer)) \"fn x => x\" >>= fn Success f => pure $ f 570"
+                    "testaction 570 $ evaluate (const.OpenType @(Integer -> Integer)) \"fn x => x\" >>= fn Success f => pure $ f 570"
               ]
         , tGroup
               "text-sort"