Added unification to interpreter + tui

app/InteractiveCli.hs

@@ -48,8 +48,8 @@ data Command
   | Quit
   | Malformed SigilDoc
 
-interactive_cli :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e)
-  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> InteractiveCliOpts -> IO ()
+interactive_cli :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e)
+  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> InteractiveCliOpts -> IO ()
 interactive_cli interp@(Interpreter {..}) opts = do
     s <- if not (null (ifile opts)) then eval_file "sigil-user" (ifile opts) start_state else pure start_state
     loop s (InteractiveState ("sigil-user", []))

app/InteractiveTui.hs

@@ -41,8 +41,8 @@ data InteractiveTuiOpts = InteractiveTuiOpts
   deriving (Show, Read, Eq)
 
 
-interactive_tui :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> InteractiveTuiOpts -> IO ()
+interactive_tui :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> InteractiveTuiOpts -> IO ()
 interactive_tui interpreter _ = do
   let app = App { appDraw = draw
                 , appChooseCursor  = choose_cursor
@@ -182,7 +182,7 @@ change_focus _ v = v
 choose_cursor :: InteractiveState s -> [T.CursorLocation ID] -> Maybe (T.CursorLocation ID)
 choose_cursor st locs = find (liftEq (==) (Just $ st^.focus) . T.cursorLocationName) locs
 
-app_handle_event :: forall m e s t ev. Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+app_handle_event :: forall m e s t f ev. Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
   -> T.BrickEvent ID ev -> T.EventM ID (InteractiveState s) ()
 app_handle_event _ = \case
   (T.VtyEvent (V.EvKey V.KUp    [V.MCtrl])) -> focus %= change_focus DUp

app/InterpretUtils.hs

@@ -1,5 +1,6 @@
 module InterpretUtils
   ( eval_expr
+  , eval_formula
   , eval_mod ) where
 
 import Prelude hiding (mod)
@@ -13,15 +14,18 @@ import Prettyprinter.Render.Sigil
 
 import Sigil.Parse
 import Sigil.Abstract.Names
+import Sigil.Abstract.Unify
 import Sigil.Abstract.Syntax
+import Sigil.Abstract.Substitution
 import Sigil.Abstract.Environment
 import Sigil.Interpret.Interpreter
 import Sigil.Analysis.Typecheck
+import Sigil.Analysis.FormulaCheck
 import Sigil.Analysis.NameResolution
 import Sigil.Concrete.Internal (InternalCore, InternalModule)
 
-eval_expr :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> Text -> [ImportDef] -> Text -> m (InternalCore, InternalCore)
+eval_expr :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> Text -> [ImportDef] -> Text -> m (InternalCore, InternalCore)
 eval_expr i@(Interpreter {..}) package_name imports line = do
   env <- get_env package_name imports
   precs <- get_precs package_name imports
@@ -35,8 +39,8 @@ eval_expr i@(Interpreter {..}) package_name imports line = do
     `catchError` (throwError . (<+>) "Normalization:")
   pure (norm, ty)
 
-eval_mod :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> Text -> Text -> Text -> m InternalModule
+eval_mod :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> Text -> Text -> Text -> m InternalModule
 eval_mod i@(Interpreter {..}) package_name modulename modul = do
   parsed <- mod (get_precs package_name) modulename modul -- TODO: eof??
     `catchError` (throwError . (<+>) "Parse:")
@@ -52,18 +56,42 @@ eval_mod i@(Interpreter {..}) package_name modulename modul = do
   check_module (CheckInterp (interp_eval i) (interp_eq i) spretty) env resolved
     `catchError` (throwError . (<+>) "Inference:")
 
+
+eval_formula :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> Text -> [ImportDef] -> Text -> m (Substitution Name InternalCore)
+eval_formula i@(Interpreter {..}) package_name imports line = do
+  env <- get_env package_name imports
+  precs <- get_precs package_name imports
+  resolution <- get_resolve package_name imports
+  parsed <- formula precs "playground" line  -- TODO: eof??
+  resolved <- resolve_closed (("unbound name" <+>) . pretty) resolution parsed
+    `catchError` (throwError . (<+>) "Resolution:")
+  checked <- check_formula (CheckInterp (interp_eval i) (interp_eq i) spretty) env resolved
+    `catchError` (throwError . (<+>) "Inference:")
+  solution <- (interp_solve i) id env checked
+    `catchError` (throwError . (<+>) "Unification:")
+  pure solution
+
 -- Internal Use only 
-interp_eval :: forall m e s t. (MonadError SigilDoc m) =>
-          Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+interp_eval :: forall m e s t f. (MonadError SigilDoc m) =>
+          Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
             -> (SigilDoc -> SigilDoc) -> e (Maybe InternalCore, InternalCore) -> InternalCore -> InternalCore -> m InternalCore
 interp_eval (Interpreter {..}) f env ty val = do
     ty' <- reify ty
     val' <- reify val
     result <- eval f env ty' val'
     reflect result
 
-interp_eq :: forall m e s t. (MonadError SigilDoc m) =>
-          Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+interp_solve :: forall m e s t f. (MonadError SigilDoc m) =>
+          Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
+            -> (SigilDoc -> SigilDoc) -> e (Maybe InternalCore, InternalCore) -> Formula Name InternalCore -> m (Substitution Name InternalCore)
+interp_solve (Interpreter {..}) f env formula = do
+    formula' <- reify_formula formula
+    subst <- solve_formula f env formula'
+    mapM reflect subst 
+
+interp_eq :: forall m e s t f. (MonadError SigilDoc m) =>
+          Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
             -> (SigilDoc -> SigilDoc) -> e (Maybe InternalCore, InternalCore) -> InternalCore -> InternalCore -> InternalCore -> m Bool
 interp_eq (Interpreter {..}) f env ty l r = do
     ty' <- reify ty

app/Main.hs

@@ -11,6 +11,7 @@ import Options.Applicative
 import Prettyprinter.Render.Sigil
 
 import Sigil.Abstract.Names (Name, MonadGen)
+import Sigil.Abstract.Unify (Formula)
 import Sigil.Abstract.Environment (Environment, Env)
 import Sigil.Interpret.Interpreter 
 import Sigil.Interpret.Canonical 
@@ -110,10 +111,10 @@ main = do
 
 run_with_backend ::
   Backend
-  -> (forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-      Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> a -> IO ())
+  -> (forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+      Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> a -> IO ())
   -> a -> IO ()
 run_with_backend backend func val = case backend of
   Native -> func (canonical_interpreter spretty
-                  :: Interpreter (CanonM SigilDoc) SigilDoc (Env (Maybe InternalCore, InternalCore)) Context InternalCore) val
+                  :: Interpreter (CanonM SigilDoc) SigilDoc (Env (Maybe InternalCore, InternalCore)) Context InternalCore (Formula Name InternalCore)) val
   b -> putStrLn $ pack ("Cannot run with backend:" <> show b)

app/Server.hs

@@ -41,8 +41,8 @@ data ServerOpts = ServerOpts
   deriving (Show, Read, Eq)
 
 
-server :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> ServerOpts -> IO ()
+server :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+  Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> ServerOpts -> IO ()
 server interpreter opts = do
   putStrLn "starting server!"
   runTCPServer Nothing (show $ port opts) (threadWorker interpreter)
@@ -75,8 +75,8 @@ runTCPServer mhost port worker = withSocketsDo $ do
             forkFinally (worker conn) (const $ gracefulClose conn 5000)
 
 
-threadWorker :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e)
-  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> Socket -> IO ()
+threadWorker :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e)
+  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> Socket -> IO ()
 threadWorker interpreter socket = putStrLn "worker started!" >> loop (packetProducer socket) (start_state interpreter)
   where
     loop :: Producer Bs.ByteString IO () -> s -> IO ()
@@ -95,8 +95,8 @@ threadWorker interpreter socket = putStrLn "worker started!" >> loop (packetProd
       = either (>> pure state) id .  bimap (putStrLn . ("Error: " <>) . pack . show) (processMessage interpreter state socket)
 
 
-processMessage :: forall m e s t. (MonadError SigilDoc m, MonadGen m, Environment Name e)
-  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t -> s -> Socket -> InMessage -> IO s
+processMessage :: forall m e s t f. (MonadError SigilDoc m, MonadGen m, Environment Name e)
+  => Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f -> s -> Socket -> InMessage -> IO s
 processMessage interp@(Interpreter {..}) state socket = \case
   EvalExpr uid _ code -> do
     (result, state') <- run state $ eval_expr interp "sigil-user" [] code

app/Tui/Defaults/EditorKeymap.hs

@@ -78,8 +78,8 @@ default_keymap self = \case
   Structural -> []
 
 
-module_keymap :: forall m e s t id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+module_keymap :: forall m e s t f id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
               -> Lens' (InteractiveState s) (Editor (InteractiveState s) id) -> EditMode -> Keymap (T.EventM id (InteractiveState s) ())
 module_keymap interpreter self = \case 
             -- Movement
@@ -125,9 +125,10 @@ module_keymap interpreter self = \case
             , ([(V.KChar 'O', [])], self.mode .= Insert >> self %= applyEdit (Z.moveUp . Z.breakLine . Z.gotoBOL))
 
             -- Evaluate
-            , ([(V.KChar ' ', []), (V.KChar 'e', [])], eval_text interpreter (getText . view self))
-            , ([(V.KChar ' ', []), (V.KChar 'm', []), (V.KChar 'f', [])], load_file interpreter)
-            , ([(V.KChar ' ', []), (V.KChar 'm', []), (V.KChar 'i', [])], add_import)
+            , ([(V.KChar ';', []), (V.KChar 'e', []), (V.KChar 'e', [])], eval_text interpreter (getText . view self))
+            , ([(V.KChar ';', []), (V.KChar 'e', []), (V.KChar 'q', [])], query_text interpreter (getText . view self))
+            , ([(V.KChar ';', []), (V.KChar 'm', []), (V.KChar 'f', [])], load_file interpreter)
+            , ([(V.KChar ';', []), (V.KChar 'm', []), (V.KChar 'i', [])], add_import)
 
             -- Quit
             , ([(V.KChar ' ', []), (V.KChar 'q', []), (V.KChar 'q', [])], halt)

app/Tui/Interaction.hs

@@ -1,5 +1,6 @@
 module Tui.Interaction
   ( eval_text
+  , query_text
   , load_file
   , add_import
   ) where
@@ -34,8 +35,8 @@ import Sigil.Concrete.Internal (InternalCore)
 import InterpretUtils
 import Tui.Types
 
-eval_text :: forall m e s t id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+eval_text :: forall m e s t f id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
           -> (InteractiveState s -> Text) -> T.EventM id (InteractiveState s) ()
 eval_text interpreter getText = do
   istate <- use interpreterState
@@ -49,8 +50,22 @@ eval_text interpreter getText = do
                                  , "type:" <+> nest 2 (pretty ty) ])
     Left err -> outputState .= show err
 
-load_file :: forall m e s t id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
-                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t
+query_text :: forall m e s t f id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
+          -> (InteractiveState s -> Text) -> T.EventM id (InteractiveState s) ()
+query_text interpreter getText = do
+  istate <- use interpreterState
+  this <- get
+  (pname, _, imports) <- use location
+  (result, state') <- liftIO $ (run interpreter) istate (eval_formula interpreter pname imports (getText this))
+  interpreterState .= state'
+  case result of
+    Right subst -> do
+      outputState .= (show $ vsep ["solved", pretty subst])
+    Left err -> outputState .= show err
+
+load_file :: forall m e s t f id. (MonadError SigilDoc m, MonadGen m, Environment Name e) =>
+                    Interpreter m SigilDoc (e (Maybe InternalCore, InternalCore)) s t f
           -> T.EventM id (InteractiveState s) ()
 load_file interpreter = do
   focus .= Palette

src/Sigil/Abstract/Substitution.hs

@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -XDeriveTraversable #-}
 module Sigil.Abstract.Substitution
   ( Substitution
   , Subst(..)
@@ -26,12 +27,17 @@ import Data.Set (Set)
 import qualified Data.Map as Map
 import Data.Map (Map)
 
+import Prettyprinter
+
 import Sigil.Abstract.Syntax
 import Sigil.Abstract.Names
 
 
 newtype Substitution n a = Substitution (Map n a)
-  deriving (Functor, Foldable)
+  deriving (Functor, Foldable, Traversable)
+
+instance (Pretty n, Pretty a) => Pretty (Substitution n a) where
+  pretty (Substitution subst) = vsep $ fmap (\(n,a) -> pretty n <+> "↦" <+> pretty a) $ Map.toList subst
 
 class Subst n s a | a -> s n where
   substitute :: Set n -> Substitution n s -> a -> a

src/Sigil/Analysis/FormulaCheck.hs

@@ -0,0 +1,55 @@
+module Sigil.Analysis.FormulaCheck
+  ( check_formula ) where
+
+import Control.Monad.Except (MonadError, throwError)
+
+import Prettyprinter
+
+import Sigil.Abstract.Names
+import Sigil.Abstract.Unify
+import Sigil.Abstract.Environment
+import Sigil.Analysis.Typecheck
+import Sigil.Concrete.Resolved
+import Sigil.Concrete.Decorations.Range
+import Sigil.Concrete.Internal
+
+
+check_formula :: (MonadGen m, MonadError err m, Environment Name e)
+  => CheckInterp m err e InternalCore -> e (Maybe InternalCore,InternalCore)
+  -> Formula Name ResolvedCore -> m (Formula Name InternalCore)
+check_formula interp@(CheckInterp {..}) env formula = case formula of 
+  Conj scons -> Conj <$> mapM (check_scons interp env) scons
+  And l r -> And <$> check_formula interp env l <*> check_formula interp env r
+  Bind q n ty f -> do
+    (ty', kind) <- infer interp env ty
+    ty_norm <- normalize (lift_err . flip NormErr mempty) env kind ty'
+    let env' = insert n (Nothing, ty_norm) env
+    Bind q n ty_norm <$> check_formula interp env' f 
+
+
+check_scons :: (MonadGen m, MonadError err m, Environment Name e)
+  => CheckInterp m err e InternalCore -> e (Maybe InternalCore,InternalCore)
+  -> SingleConstraint ResolvedCore -> m (SingleConstraint InternalCore)
+check_scons interp@(CheckInterp {..}) env cons = case cons of
+  (l :≗: r) -> do
+    (l', lty) <- infer interp env l
+    (r', rty) <- infer interp env r
+    (_, kind) <- infer interp env lty
+    check_eq mempty interp env kind lty rty
+    l_norm <- normalize (lift_err . flip NormErr mempty) env lty l'
+    r_norm <- normalize (lift_err . flip NormErr mempty) env rty r'
+    pure $ (l_norm :≗: r_norm)
+  (val :∈: ty) -> do
+    (ty', kind) <- infer interp env ty
+    ty_norm <- normalize (lift_err . flip NormErr mempty) env kind ty'
+    val' <- check interp env val ty_norm
+    val_norm <- normalize (lift_err . flip NormErr mempty) env ty_norm val'
+    pure $ (val_norm :≗: ty_norm)
+
+
+check_eq :: (MonadError err m, Pretty a) => Range -> (CheckInterp m err e a) -> e (Maybe a, a) -> a -> a -> a -> m ()
+check_eq range (CheckInterp {..}) env ty l r
+ = 
+  αβη_eq (lift_err . flip NormErr range) env ty l r >>= \case
+    True -> pure ()
+    False -> throwError $ lift_err $ PrettyErr ("not-equal:" <+> pretty l <+> "and" <+> pretty r) range

src/Sigil/Interpret/Canonical.hs

@@ -32,6 +32,7 @@ import Prettyprinter
 
 import Sigil.Abstract.Names
 import Sigil.Abstract.Syntax
+import Sigil.Abstract.Unify
 import Sigil.Abstract.Environment
 import Sigil.Parse.Mixfix
 import Sigil.Concrete.Internal
@@ -63,10 +64,12 @@ default_precs = Precedences
 
 
 canonical_interpreter :: forall err. (InterpreterErr -> err)
-  -> Interpreter (CanonM err) err (Env (Maybe InternalCore, InternalCore)) Context InternalCore
+  -> Interpreter (CanonM err) err (Env (Maybe InternalCore, InternalCore)) Context InternalCore (Formula Name InternalCore)
 canonical_interpreter liftErr = Interpreter
   { reify = pure
   , reflect = pure
+  , reify_formula = pure
+  , reflect_formula = pure
 
   -- eval :: (err -> err) -> env -> t -> t -> m t
   , eval = \f env ty term ->

src/Sigil/Interpret/Interpreter.hs

@@ -47,18 +47,21 @@ type Restarts a = [IO a]
 -- env = environment
 -- s = state
 -- t = term representation
-data Interpreter m err env s t = Interpreter
+data Interpreter m err env s t f = Interpreter
   -- Converting to/from the term representation, 't'
   { reify :: InternalCore -> m t
   , reflect :: t -> m InternalCore
 
+  , reify_formula :: Formula Name InternalCore -> m f
+  , reflect_formula :: f -> m (Formula Name InternalCore)
+
   {--------------------- Term Queries and Transformations ----------------------}
   -- Evaluate a term t in the environment e
   , eval :: (err -> err) -> env -> t -> t -> m t
   -- Return true if two terms are canonically equal, false otherwise 
   , norm_eq :: (err -> err) -> env -> t -> t -> t -> m Bool
   -- Higher Order Unification algorithm implementation
-  , solve_formula :: (err -> err) -> env -> Formula Name t -> m (Substitution Name t)
+  , solve_formula :: (err -> err) -> env -> f -> m (Substitution Name t)
 
   {------------------------- Environment Manipulation --------------------------}
   -- Load a module into the interpreter's state