Interpretation (#298): code

Pinafore/pinafore-language/lib/Pinafore/Language.hs

@@ -38,48 +38,11 @@ module Pinafore.Language
 import Import
 import Pinafore.Language.Convert
 import Pinafore.Language.Error
-import Pinafore.Language.Expression
 import Pinafore.Language.Interpret
 import Pinafore.Language.Interpreter
 import Pinafore.Language.Library
-import Pinafore.Language.Type
 import Pinafore.Language.Var
 
-runPinaforeScoped :: (?library :: LibraryContext) => String -> QInterpreter a -> InterpretResult a
-runPinaforeScoped sourcename ma =
-    runInterpreter (initialPos sourcename) ?library spvals $ do
-        sd <- interpretImportDeclaration builtInModuleName
-        withScopeDocs sd ma
-
-spvals :: (?library :: LibraryContext) => QSpecialVals
-spvals = let
-    specialEvaluate :: forall t. QType 'Positive t -> Text -> IO (Result QError t)
-    specialEvaluate t text = do
-        ier <- evaluate $ runPinaforeScoped "<evaluate>" $ parseToValueSubsume t text
-        runInterpretResult ier
-    in MkQSpecialVals {..}
-
-parseToValue :: Text -> [(ImplicitName, QValue)] -> QInterpreter QValue
-parseToValue text args = do
-    expr <- parseTopExpression text
-    let argExprs = fmap (fmap qConstValue) args
-    expr' <- qImply argExprs expr
-    qEvalExpr expr'
-
-parseToValueUnify ::
-       forall t. (HasQType QPolyShim 'Negative t)
-    => Text
-    -> [(ImplicitName, QValue)]
-    -> QInterpreter t
-parseToValueUnify text args = do
-    val <- parseToValue text args
-    qUnifyValue val
-
-parseToValueSubsume :: forall t. QType 'Positive t -> Text -> QInterpreter t
-parseToValueSubsume t text = do
-    val <- parseToValue text []
-    tsSubsumeValue @QTypeSystem t val
-
 interact :: (?library :: LibraryContext) => Handle -> Handle -> Bool -> View ()
 interact inh outh echo = do
     liftIO $ hSetBuffering outh NoBuffering

Pinafore/pinafore-language/lib/Pinafore/Language/Convert/HasType.hs

@@ -64,6 +64,11 @@ class (CoercibleKind (CCRVariancesKind dv), dv ~ HetCCRVariancesOf f, HasCCRVari
     where
     qGroundType :: QGroundType dv f
 
+qSomeGroundType ::
+       forall dv (t :: CCRVariancesKind dv). HasQGroundType dv t
+    => QSomeGroundType
+qSomeGroundType = MkSomeGroundType $ qGroundType @dv @t
+
 type HasQArgumentType :: PolyShimKind -> Polarity -> forall (sv :: CCRVariance) -> CCRVarianceKind sv -> Constraint
 class Is PolarityType polarity => HasQArgumentType pshim polarity sv t | t -> sv where
     qArgumentType :: CCRPolarArgumentShimWit (pshim Type) QType polarity sv t

Pinafore/pinafore-language/lib/Pinafore/Language/Expression.hs

@@ -160,6 +160,9 @@ qEvalExpr ::
     -> m QValue
 qEvalExpr expr = tsEval @QTypeSystem expr
 
+qUnifyRigid :: forall a b. QShimWit 'Positive a -> QShimWit 'Negative b -> QInterpreter (QShim a b)
+qUnifyRigid = tsUnifyRigid @QTypeSystem
+
 qUnifyValueTo :: forall t. QShimWit 'Negative t -> QValue -> QInterpreter t
 qUnifyValueTo = tsUnifyValueTo @QTypeSystem
 

Pinafore/pinafore-language/lib/Pinafore/Language/Interpret.hs

@@ -2,13 +2,19 @@ module Pinafore.Language.Interpret
     ( parseTopExpression
     , parseModule
     , parseType
+    , parseToValue
+    , parseToValueUnify
+    , parseToValueSubsume
     , interpretImportDeclaration
+    , runPinaforeScoped
     , runInteract
     , showPinaforeModel
     ) where
 
 import Import
+import Pinafore.Language.Convert
 import Pinafore.Language.Error
+import Pinafore.Language.Expression
 import Pinafore.Language.Interpret.Expression
 import Pinafore.Language.Interpret.Interact
 import Pinafore.Language.Interpreter
@@ -36,3 +42,38 @@ parseType ::
 parseType text = do
     st <- parseScopedReaderWhole (fmap return readType) text
     interpretType st
+
+parseToValue :: Text -> [(ImplicitName, QValue)] -> QInterpreter QValue
+parseToValue text args = do
+    expr <- parseTopExpression text
+    let argExprs = fmap (fmap qConstValue) args
+    expr' <- qImply argExprs expr
+    qEvalExpr expr'
+
+parseToValueUnify ::
+       forall t. (HasQType QPolyShim 'Negative t)
+    => Text
+    -> [(ImplicitName, QValue)]
+    -> QInterpreter t
+parseToValueUnify text args = do
+    val <- parseToValue text args
+    qUnifyValue val
+
+parseToValueSubsume :: forall t. QType 'Positive t -> Text -> QInterpreter t
+parseToValueSubsume t text = do
+    val <- parseToValue text []
+    tsSubsumeValue @QTypeSystem t val
+
+spvals :: (?library :: LibraryContext) => QSpecialVals
+spvals = let
+    specialEvaluate :: forall t. QType 'Positive t -> Text -> IO (Result QError t)
+    specialEvaluate t text = do
+        ier <- evaluate $ runPinaforeScoped "<evaluate>" $ parseToValueSubsume t text
+        runInterpretResult ier
+    in MkQSpecialVals {..}
+
+runPinaforeScoped :: (?library :: LibraryContext) => String -> QInterpreter a -> InterpretResult a
+runPinaforeScoped sourcename ma =
+    runInterpreter (initialPos sourcename) ?library spvals $ do
+        sd <- interpretImportDeclaration builtInModuleName
+        withScopeDocs sd ma

Pinafore/pinafore-language/lib/Pinafore/Language/Interpreter/Interpreter.hs

@@ -7,6 +7,7 @@ module Pinafore.Language.Interpreter.Interpreter
     , sourcePosParam
     , varIDStateParam
     , scopeParam
+    , loadModuleParam
     , currentNamespaceParam
     , appNotationVarRef
     , appNotationBindsProd
@@ -90,6 +91,15 @@ newtype QInterpreter a = MkQInterpreter
                , MonadTunnelIO
                )
 
+instance RepresentationalRole QInterpreter where
+    representationalCoercion MkCoercion = MkCoercion
+
+instance MaybeRepresentational QInterpreter where
+    maybeRepresentational = Just Dict
+
+instance HasVariance QInterpreter where
+    type VarianceOf QInterpreter = 'Covariance
+
 instance MonadCoroutine QInterpreter where
     coroutineSuspend pqmr =
         hoist MkQInterpreter $ coroutineSuspend $ \pmq -> unInterpreter $ pqmr $ \p -> MkQInterpreter $ pmq p

Pinafore/pinafore-language/lib/Pinafore/Language/Library.hs

@@ -17,7 +17,6 @@ import Pinafore.Language.Library.Action
 import Pinafore.Language.Library.Debug
 import Pinafore.Language.Library.Entity
 import Pinafore.Language.Library.Env
-import Pinafore.Language.Library.Eval
 import Pinafore.Language.Library.Function
 import Pinafore.Language.Library.Interpret
 import Pinafore.Language.Library.LibraryModule
@@ -29,6 +28,7 @@ import Pinafore.Language.Library.Maybe
 import Pinafore.Language.Library.Model
 import Pinafore.Language.Library.ModelOrder
 import Pinafore.Language.Library.Optics
+import Pinafore.Language.Library.Pinafore
 import Pinafore.Language.Library.Product
 import Pinafore.Language.Library.Result
 import Pinafore.Language.Library.Storage
@@ -61,7 +61,7 @@ pinaforeLibrary =
     , storageLibSection
     , undoLibSection
     , envLibSection
-    , evalLibSection
+    , pinaforeLibSection
     , debugLibSection
     ]
 

Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs

@@ -0,0 +1,122 @@
+{-# OPTIONS -fno-warn-orphans #-}
+
+module Pinafore.Language.Library.Pinafore
+    ( pinaforeLibSection
+    ) where
+
+import Import
+import Pinafore.Language.Convert
+import Pinafore.Language.Error
+import Pinafore.Language.Expression
+import Pinafore.Language.Interpret
+import Pinafore.Language.Interpreter
+import Pinafore.Language.Library.Convert ()
+import Pinafore.Language.Library.Defs
+import Pinafore.Language.Library.LibraryModule
+import Pinafore.Language.Library.Types
+import Pinafore.Language.SpecialForm
+import Pinafore.Language.Type
+import Pinafore.Language.Var
+
+-- QContext
+newtype QContext =
+    MkQContext LibraryContext
+
+instance HasQGroundType '[] QContext where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily QContext)|]) "Context.Pinafore."
+
+thisContext :: QSpecialForm
+thisContext =
+    MkQSpecialForm NilListType $ \() -> do
+        lm <- paramAsk loadModuleParam
+        let
+            sval :: QContext
+            sval = MkQContext $ MkLibraryContext lm
+        return $ constSealedExpression $ MkSomeOf qType sval
+
+-- QInterpreter
+instance HasQGroundType '[ CoCCRVariance] QInterpreter where
+    qGroundType =
+        stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily QInterpreter)|]) "Interpreter.Pinafore."
+
+langRunInterpreter :: QContext -> QInterpreter A -> Action (Result Text A)
+langRunInterpreter (MkQContext lc) ia = let
+    ?library = lc
+    in do
+           rea <- runInterpretResult $ runPinaforeScoped "<evaluate>" ia
+           return $ mapResultFailure showText rea
+
+-- LangType
+data LangType (pq :: (Type, Type)) =
+    forall a. MkLangType (QRange a pq)
+                         (QNonpolarType a)
+
+instance CatFunctor (CatRange (->)) (->) LangType where
+    cfmap f (MkLangType r v) = MkLangType (cfmap f r) v
+
+instance ShowText (LangType pq) where
+    showText (MkLangType _ v) = toText $ exprShow v
+
+instance MaybeRepresentational LangType where
+    maybeRepresentational = Nothing
+
+instance HasCCRVariance 'RangeCCRVariance LangType
+
+instance HasQGroundType '[ RangeCCRVariance] LangType where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangType)|]) "Type.Pinafore."
+
+langTypePositive :: LangType '( p, q) -> QShimWit 'Positive p
+langTypePositive (MkLangType 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
+
+langUnifyTypes :: LangType '( A, TopType) -> LangType '( BottomType, B) -> QInterpreter (A -> B)
+langUnifyTypes ta tb = fmap shimToFunction $ qUnifyRigid (langTypePositive ta) (langTypeNegative tb)
+
+-- LangValue
+newtype LangValue =
+    MkLangValue QValue
+
+instance HasQGroundType '[] LangValue where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangValue)|]) "Value.Pinafore."
+
+mkLangValue :: LangType '( A, TopType) -> A -> LangValue
+mkLangValue t v = MkLangValue $ MkSomeOf (langTypePositive t) v
+
+interpretToValue :: Text -> QInterpreter LangValue
+interpretToValue src = fmap MkLangValue $ parseToValue src []
+
+langUnifyValue :: LangType '( BottomType, A) -> LangValue -> QInterpreter A
+langUnifyValue t (MkLangValue v) = qUnifyValueTo (langTypeNegative t) v
+
+pinaforeLibSection :: LibraryStuff
+pinaforeLibSection =
+    headingBDS "Pinafore" "" $
+    pure $
+    namespaceBDS
+        "Pinafore"
+        [ typeBDS "Context" "" (qSomeGroundType @_ @QContext) []
+        , namespaceBDS
+              "Context"
+              [specialFormBDS "this" "The context at this point in source." [] "Context.Pinafore" thisContext]
+        , typeBDS "Interpreter" "" (qSomeGroundType @_ @QInterpreter) []
+        , namespaceBDS "Interpreter" $ monadEntries @Interpreter <> [valBDS "run" "" langRunInterpreter]
+        , typeBDS "Type" "" (qSomeGroundType @_ @LangType) []
+        , specialFormBDS "const.Type" "" ["@A"] "Type.Pinafore A" $
+          MkQSpecialForm (ConsListType AnnotNonpolarType NilListType) $ \(MkSome (tw :: _ t), ()) -> let
+              stype :: QShimWit 'Positive (LangType '( t, t))
+              stype = rangeShimWit qGroundType (nonpolarToNegative @QTypeSystem tw) (nonpolarToPositive @QTypeSystem tw)
+              sval :: LangType '( t, t)
+              sval = MkLangType identityRange tw
+              in return $ constSealedExpression $ MkSomeOf stype sval
+        , hasSubtypeRelationBDS @(LangType '( P, Q)) @Showable Verify "" $ functionToShim "show" textShowable
+        , namespaceBDS "Type" [valBDS "unify" "Unify two types." langUnifyTypes]
+        , typeBDS "Value" "" (qSomeGroundType @_ @LangValue) []
+        , namespaceBDS
+              "Value"
+              [ valBDS "mk" "" mkLangValue
+              , valBDS "unify" "Unify type with value." langUnifyValue
+              , valBDS "interpret" "Interpret Pinafore source." interpretToValue
+              ]
+        ]