Refine unification algorithm

New settings for graphic constraint

1. Binding edge no longer rely on a number to identify
   its binding scope. It is now fully dynamic.
2. A topsort implementation has been added to the toolset.
3. Fixed a bug about least common ancestor in unification.
4. A instance relation "merge*" has been added by operator '|->'.
5. A new type instance relation named phantom node has been
   added, which is dedicated to solve self binding problem.
   It is now integrated into unification.

bootstrap/bootstrap.cabal

@@ -60,10 +60,13 @@ library
       Graph.Data
       Graph.Extension.GraphicType
       Graph.Syntax
+      Graph.Tree
       JIT.FFI
       JIT.LLVM
       Language.Constraint.Graphic
       Language.Constraint.Kind
+      Language.Constraint.Relation.Error
+      Language.Constraint.Relation.Phantom
       Language.Constraint.Unification
       Language.Core
       Language.Core.Class
@@ -147,7 +150,6 @@ library
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
       QuickCheck
-    , algebraic-graphs ==0.7
     , base >=4.9 && <5
     , bifunctors
     , bytestring
@@ -215,7 +217,6 @@ executable yo
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       QuickCheck
-    , algebraic-graphs ==0.7
     , base >=4.9 && <5
     , bifunctors
     , bootstrap
@@ -290,7 +291,6 @@ test-suite bootstrap-test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       QuickCheck
-    , algebraic-graphs ==0.7
     , base >=4.9 && <5
     , bifunctors
     , bootstrap

bootstrap/fourmolu.yaml

@@ -0,0 +1,17 @@
+# Generated from web app, for more information, see: https://fourmolu.github.io/config/
+indentation: 2
+column-limit: 70
+function-arrows: leading
+comma-style: leading
+import-export-style: leading
+indent-wheres: true
+record-brace-space: true
+newlines-between-decls: 1
+haddock-style: single-line
+haddock-style-module: multi-line
+let-style: auto
+in-style: right-align
+single-constraint-parens: auto
+single-deriving-parens: auto
+unicode: detect
+respectful: true

bootstrap/package.yaml

@@ -39,7 +39,6 @@ dependencies:
 - QuickCheck
 - tasty-quickcheck
 - capability
-- algebraic-graphs == 0.7
 - prettyprinter
 - lens
 - random

bootstrap/src/Compiler/TypeChecking.hs

@@ -14,30 +14,31 @@ where
 import qualified Driver.Constraint as DGC
 import Driver.Constraint (SolverErr)
 import Driver.Transform.GraphType (runGraphType, syntacticType)
-import Driver.Transform (UnifyGNodes, UnifyGEdges)
 
 import Driver.Unification (unify, GraphUnifyError)
 
-import Language.Core (ExprF, Name, Label, ExprSurface, ExprSurfaceExt, TypSurface)
+import Language.Core (ExprF, Name, Label, ExprSurface, ExprSurfaceExt, TypSurface, ConstraintSurface, ConstraintNodesSurface, ConstraintEdgesSurface)
 import Graph.Core (Hole, CoreG)
 import Graph.Extension.GraphicType
 import Language.Generic
 import Language.Constraint.Graphic
 import Data.Text (Text)
 import Transform.GraphType (GraphToTypeErr)
+import Language.Setting (HasGraphShow)
 
 data TypeCheckingErr
-  = TCSolverErr (SolverErr Name (Hole UnifyGNodes Int) (CoreG UnifyGNodes UnifyGEdges Int) (GraphUnifyError (Hole UnifyGNodes Int)))
-  | TCToSyntacticTyp (GraphToTypeErr (Hole UnifyGNodes Int))
+  = TCSolverErr (SolverErr Name (Hole ConstraintNodesSurface Int) ConstraintSurface (GraphUnifyError (Hole ConstraintNodesSurface Int)))
+  | TCToSyntacticTyp (GraphToTypeErr (Hole ConstraintNodesSurface Int))
   deriving (Show, Eq)
 
 tcExprToGraphciType
   :: forall nodes edges m target
    . ( target ~ (ExprF (ExprSurfaceExt TypSurface) Name |: Hole nodes Int)
      , ConstrainGraphic (ExprSurfaceExt TypSurface) target (DGC.GCGen Name nodes m) nodes edges Int
      , edges :>+: '[Pht O, Pht Sub, Pht NDOrderLink, T (Binding Name), T Unify, T Instance, T Sub]
-     , nodes :>+: '[NDOrder, G, T NodeBot, NodePht, T NodeSum, T NodeRec, Histo, T (NodeLit Integer), T (NodeLit Text), T (NodeHas Label)]
+     , nodes :>+: '[NDOrder, G, T NodeBot, NodePht, T NodeSum, T NodeRec, R [], T (NodeLit Integer), T (NodeLit Text), T (NodeHas Label)]
      , Monad m
+     , HasGraphShow nodes edges Int
      )
   => BindingTable Name nodes -> Int
   -> ExprSurface TypSurface
@@ -46,12 +47,12 @@ tcExprToGraphciType env i = DGC.infer env i unify
 
 tcExprToSyntacticType
   :: Monad m
-  => BindingTable Name UnifyGNodes
+  => BindingTable Name ConstraintNodesSurface
   -> Int -> (String, Int)
   -> ExprSurface TypSurface
   -> m (Either TypeCheckingErr (TypSurface, Int))
 tcExprToSyntacticType env i s e =
-  tcExprToGraphciType @UnifyGNodes @UnifyGEdges env i e >>= \case
+  tcExprToGraphciType @ConstraintNodesSurface @ConstraintEdgesSurface env i e >>= \case
   Left err -> return $ Left $ TCSolverErr err
   Right (source, i') -> transfromType s source >>= \case
     Left err -> return $ Left $ TCToSyntacticTyp err

bootstrap/src/Driver/Constraint.hs

@@ -29,7 +29,7 @@ import Language.Generic ((:>+:), type (|:) (..))
 import Language.Core (ExprF (..), Expr (..))
 import Language.Setting
 
-import Graph.Core (Hole (..), CoreG, HasOrderEdge, HasOrderGraph)
+import Graph.Core (Hole (..), CoreG, HasOrderGraph)
 import Graph.Extension.GraphicType
 
 

bootstrap/src/Driver/Graph.hs

@@ -2,50 +2,27 @@
 -}
 
 module Driver.Graph
-  ( parseTypeGrpah
+  ( -- parseTypeGrpah
   )
 where
 
-import Driver.Parser ( driveParser, surfaceType )
-import Text.Megaparsec
-import Data.Void (Void)
-
-import Language.Core ( builtinStore, Name)
+import Language.Core (builtinStore, Name)
 
 import Data.Text (Text)
 
-import Driver.Transform
 import Graph.Core (induceLink, isLinkOf)
 import Graph.Extension.GraphicType
 
--- | save graph as png file
--- saveGraph :: (Show label, Show name, Labellable name, Ord name)
---           => (Node, Gr (GNode (GNodeLabel lit label name)) (GEdge name))
---           -> FilePath -> IO ()
--- saveGraph (root, g) name = do
---   dot <- runDotGraph g root
---   void $ runGraphviz dot Png (name <> ".png")
---   writeDotFile (name <> ".dot") dot
+import Compiler.SourceParsing (getGraphicType)
 
-parseTypeGrpah :: Text -> IO SurfaceG
-parseTypeGrpah typ = do
-   (res, _) <- driveParser builtinStore (surfaceType eof) "stdin" typ
-   case res of
-     Right t -> do
-        g <- toGraphicTypeMock mempty 0 t >>= \case
-          Left err -> fail $ show err
-          Right ((_, g :: SurfaceG), _) -> return g
-        dumpTypegraph Nothing g
-        return g
-     Left (err :: ParseErrorBundle Text Void) -> putStrLn (errorBundlePretty err) >> fail "see previous message"
+dumpGraphType :: Maybe Integer -> Text -> IO ()
+dumpGraphType suffix typ = do
+  ((root, g), _) <- getGraphicType mempty 0 builtinStore "stdin" typ
+  let nameS = "graph-s" <> maybe "" show suffix <> ".dot"
+      nameB = "graph-b" <> maybe "" show suffix <> ".dot"
+  writeFile nameS $ exportViaShow root (induceLink (isLinkOf @(T Sub)) g)
+  writeFile nameB $ exportViaShow root (induceLink (isLinkOf @(T (Binding Name))) g)
 
 -- | TODO
 exportViaShow :: a
 exportViaShow = undefined
-
-dumpTypegraph :: Maybe Integer -> SurfaceG -> IO ()
-dumpTypegraph suffix g = do
-  let nameS = "graph-s" <> maybe "" show suffix <> ".dot"
-      nameB = "graph-b" <> maybe "" show suffix <> ".dot"
-  writeFile nameS $ exportViaShow (induceLink (isLinkOf @(T Sub)) g)
-  writeFile nameB $ exportViaShow (induceLink (isLinkOf @(T (Binding Name))) g)

bootstrap/src/Driver/Transform.hs

@@ -1,49 +1,12 @@
 module Driver.Transform
   (
 
-  -- ** default definition for Graphic Type
-    SurfaceG
-  , SurfaceGNodes
-  , SurfaceGEdges
-
-  , UnifyGNodes
-  , UnifyGEdges
-  , UnifyG
-
   -- ** re-export subfunctionality
-  , module GraphType
+    module GraphType
   , module TypeGraph
   )
 where
 
 import Driver.Transform.GraphType as GraphType
 import Driver.Transform.TypeGraph as TypeGraph
 
-import Language.Core (Name, Label)
-import Language.Generic ((:+:))
-import Graph.Extension.GraphicType
-import Graph.Core
-
-import Data.Text (Text)
-
-
-type SurfaceGNodes
-  = T NodeBot :+: T (NodeLit Integer) :+: T (NodeLit Text)
-    :+: T NodeTup :+: T NodeSum :+: T NodeRec :+: T (NodeRef Name)
-    :+: T NodeApp :+: T (NodeHas Label) :+: T NodeArr
-    :+: NodePht
-type SurfaceGEdges = T Sub :+: T (Binding Name)
-
-type SurfaceG = CoreG SurfaceGNodes SurfaceGEdges Int
-
-type UnifyGNodes
-  = SurfaceGNodes
-    :+: NDOrder
-    :+: Histo :+: G
-
-type UnifyGEdges
-  = SurfaceGEdges
-    :+: Pht O :+: Pht Sub :+: Pht NDOrderLink
-    :+: T Unify :+: T Instance
-
-type UnifyG = CoreG UnifyGNodes UnifyGEdges Int

bootstrap/src/Driver/Transform/Desugar.hs

@@ -22,7 +22,7 @@ import Capability.State (HasState)
 
 import Graph.Core ( CoreG, Hole, HasOrderGraph )
 import Language.Setting (GraphState)
-import Transform.Desugar (runSugarRule, treeSugarRule, case01, case10)
+import Transform.Desugar (runSugarRule, foldSugarRule, case01, case10)
 import Language.Core (Name)
 import Language.Generic
 import Graph.Extension.GraphicType
@@ -40,11 +40,12 @@ newtype TypeGraphSugar nodes edges info m a = TypeGraphSugar
 driveTypeGraphSugar :: TypeGraphSugar nodes edges info m a -> CoreG nodes edges info -> m (a, CoreG nodes edges info)
 driveTypeGraphSugar m = runStateT (runTypeGraphSugar m)
 
--- | Graphic type constraint requires every node should have exactly one __binder__, which this function serves.
+-- | Graphic type constraint requires each node should have exactly one __binder__, which is the purpose
+-- this function serves.
 addBindingToType
   :: (HasOrderGraph nodes edges info, nodes :>+: '[T NodeApp, T NodeTup], edges :>+: '[T (Binding Name), T Sub], Monad m)
-  => CoreG nodes edges info -> Hole nodes info -> m (Bool, CoreG nodes edges info)
-addBindingToType gr g = driveTypeGraphSugar (runSugarRule (treeSugarRule rules) g) gr
+  => Hole nodes info -> CoreG nodes edges info -> m (Bool, CoreG nodes edges info)
+addBindingToType root = driveTypeGraphSugar (runSugarRule (foldSugarRule rules) root)
   where rules = 
           [ case01 @Name, case10 @Name
           ]

bootstrap/src/Driver/Transform/TypeGraph.hs

@@ -28,7 +28,7 @@ import Data.Bifunctor (first)
 import Data.String (IsString (..))
 import Capability.Error ( HasCatch, HasThrow, MonadError(..) )
 
--- | shofthand for monad
+-- | shorthand for monad
 type M name nodes edges m
   = ReaderT (TypeContextTable name nodes edges Int)
       (StateT Int (ExceptT (ToGraphicTypeErr name) m))
@@ -111,9 +111,9 @@ mockGlobalConstraint name = do
   g <- node (G 1)
   r <- if fromString "->" == name
   then node (T NodeArr)
-  else node (T $ NodeRef False name)
+  else node (T $ NodeRef mempty name)
   return . Just . (g, ) $ overlays
-    [ r -<< T (Binding Flexible 1 $ Nothing @name) >>- g
+    [ r -<< T (Binding Flexible $ Nothing @name) >>- g
     , g -<< T (Sub 1) >>- r
     ]
 
@@ -128,5 +128,5 @@ mockGlobal
 mockGlobal name = do
   r <- if fromString "->" == name
     then node (T NodeArr)
-    else node (T $ NodeRef False name)
+    else node (T $ NodeRef mempty name)
   return $ Just (r, Vertex r)

bootstrap/src/Driver/Unification.hs

@@ -19,7 +19,7 @@ import Data.Text (Text)
 import Language.Constraint.Unification
 import Graph.Core ( CoreG, Hole, HasOrderGraph )
 import Language.Core (Label, Name)
-import Language.Setting ( GraphState )
+import Language.Setting ( GraphState, HasGraphShow )
 import Language.Generic ((:>+:))
 
 import Capability.Sink (HasSink)
@@ -44,23 +44,32 @@ runUnify
 runUnify u g a b = runExceptT $ runStateT (runGraphUnify $ runUnifier u a b) g
 
 unify
-  :: ( Monad m, HasOrderGraph ns es Int
+  :: ( Monad m, HasOrderGraph ns es Int, HasGraphShow ns es Int
      , ns :>+: '[T NodeTup, T NodeSum, T NodeRec, T (NodeHas Label), T (NodeRef Name), T NodeArr, NodePht]
-     , ns :>+: '[T (NodeLit Integer), T (NodeLit Text), T NodeApp, T NodeBot, Histo, G]
+     , ns :>+: '[T (NodeLit Integer), T (NodeLit Text), T NodeApp, T NodeBot, R [], G]
      , es :>+: '[T (Binding Name), T Sub, Pht O]
      )
   => CoreG ns es Int
   -> Hole ns Int -> Hole ns Int
   -> m (Either (GraphUnifyError (Hole ns Int)) (Hole ns Int, CoreG ns es Int))
 unify = runUnify . hook1 . foldCase $ Case
-  [ case1, case2
+  [
+
+  -- bottom variable node
+    case1, case2
+
+  -- tuple
   , case10
+
   , case20, case21, case25 @Label
   , case30, case31
-  , case40 @Integer
-  , case40 @Text
+
+  -- type literal node
+  , case40 @Integer , case40 @Text
+
   -- phantom node
-  , case50, case51, case52
+  , caseNodePht
+  -- type name node
   , case60 @Name
   ]
 

bootstrap/src/EvalLoop/Loop.hs

@@ -1,4 +1,4 @@
-{-| * User interface module
+{- | * 
 -}
 
 module EvalLoop.Loop