Multithreaded type checking and inference

brat/Brat/Checker/SolveHoles.hs

@@ -1,23 +1,25 @@
-module Brat.Checker.SolveHoles (typeEq) where
+module Brat.Checker.SolveHoles (typeEq, typesEq) where
 
-import Brat.Checker.Helpers (buildConst)
+import Brat.Checker.Helpers (mineToSolve, solveSem)
 import Brat.Checker.Monad
+import Brat.Checker.SolveNumbers
 import Brat.Checker.Types (kindForMode)
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval
+import Brat.Naming (FreshMonad(..))
 import Brat.Syntax.Common
-import Brat.Syntax.Simple (SimpleTerm(..))
+-- import Brat.Syntax.Simple (SimpleTerm(..))
 import Brat.Syntax.Value
 import Control.Monad.Freer
 import Bwd
 import Hasochism
+-- import Brat.Syntax.Port (toEnd)
 
-import Control.Monad (when)
+import Control.Monad (unless)
 import Data.Bifunctor (second)
 import Data.Foldable (sequenceA_)
 import Data.Functor
-import Data.Maybe (mapMaybe)
-import qualified Data.Map as M
+import qualified Data.Set as S
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 
 -- Demand that two closed values are equal, we're allowed to solve variables in the
@@ -28,7 +30,20 @@ typeEq :: String -- String representation of the term for error reporting
        -> Val Z -- Expected
        -> Val Z -- Actual
        -> Checking ()
-typeEq str = typeEq' str (Zy :* S0 :* S0)
+typeEq str k exp act = do
+  prefix <- whoAmI
+  trackM ("typeEq: Who am I: " ++ show prefix)
+  typeEq' str (Zy :* S0 :* S0) k exp act
+
+typesEq :: String -- String representation of the term for error reporting
+        -> [TypeKind] -- The kinds we're comparing at
+        -> [Val Z] -- Expected
+        -> [Val Z] -- Actual
+        -> Checking ()
+typesEq str k exp act = do
+  prefix <- whoAmI
+  trackM ("typesEq: Who am I: " ++ show prefix)
+  typeEqs str (Zy :* S0 :* S0) k exp act
 
 
 -- Internal version of typeEq with environment for non-closed values
@@ -38,83 +53,53 @@ typeEq' :: String -- String representation of the term for error reporting
         -> Val n -- Expected
         -> Val n -- Actual
         -> Checking ()
-typeEq' str stuff@(_ny :* _ks :* sems) k exp act = do
-  hopes <- req AskHopes
+typeEq' str stuff@(ny :* _ks :* sems) k exp act = do
+  mine <- mineToSolve
   exp <- sem sems exp
   act <- sem sems act
-  typeEqEta str stuff hopes k exp act
-
-isNumVar :: Sem -> Maybe SVar
-isNumVar (SNum (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v))))) = Just v
-isNumVar _ = Nothing
+  qexp <- quote ny exp
+  qact <- quote ny act
+  trackM ("typeEq' exp: " ++ show qexp)
+  trackM ("typeEq' act: " ++ show qact)
+  typeEqEta str stuff mine k exp act
 
 -- Presumes that the hope set and the two `Sem`s are up to date.
 typeEqEta :: String -- String representation of the term for error reporting
           -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
-          -> Hopes -- A map from the hope set to corresponding FCs
+          -> (End -> Maybe String) -- Tells us if we can solve a given End
           -> TypeKind -- The kind we're comparing at
           -> Sem -- Expected
           -> Sem -- Actual
           -> Checking ()
-typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do
+typeEqEta tm (lvy :* kz :* sems) mine (TypeFor m ((_, k):ks)) exp act = do
   -- Higher kinded things
   let nextSem = semLvl lvy
   let xz = B0 :< nextSem
   exp <- applySem exp xz
   act <- applySem act xz
-  typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopes (TypeFor m ks) exp act
+  typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) mine (TypeFor m ks) exp act
 -- Not higher kinded - check for flex terms
 -- (We don't solve under binders for now, so we only consider Zy here)
 -- 1. "easy" flex cases
-typeEqEta _tm (Zy :* _ks :* _sems) hopes k (SApp (SPar (InEnd e)) B0) act
-  | M.member e hopes = solveHope k e act
-typeEqEta _tm (Zy :* _ks :* _sems) hopes k exp (SApp (SPar (InEnd e)) B0)
-  | M.member e hopes = solveHope k e exp
-typeEqEta _ (Zy :* _ :* _) hopes Nat exp act
-  | Just (SPar (InEnd e)) <- isNumVar exp, M.member e hopes = solveHope Nat e act
-  | Just (SPar (InEnd e)) <- isNumVar act, M.member e hopes = solveHope Nat e exp
+typeEqEta _tm (Zy :* _ks :* _sems) mine k (SApp (SPar e) B0) act
+  | Just _ <- mine e = solveSem k e act
+typeEqEta _tm (Zy :* _ks :* _sems) mine k exp (SApp (SPar e) B0)
+  | Just _ <- mine e = solveSem k e exp
+typeEqEta _ (Zy :* _ :* _) mine Nat (SNum exp) (SNum act) = unifyNum mine (quoteNum Zy exp) (quoteNum Zy act)
 -- 2. harder cases, neither is in the hope set, so we can't define it ourselves
-typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
+typeEqEta tm stuff@(ny :* _ks :* _sems) _ k exp act = do
   exp <- quote ny exp
   act <- quote ny act
-  let ends = mapMaybe getEnd [exp,act]
-  -- sanity check: we've already dealt with either end being in the hopeset
-  when (or [M.member ie hopes | InEnd ie <- ends]) $ typeErr "ends were in hopeset"
-  case ends of
+  unless (exp == act) $ case flexes act ++ flexes exp of
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
-    -- variables are trivially the same, even if undefined, but the values may
-    -- be different! E.g. X =? 1 + X
-    [_, _] | exp == act -> pure ()
-    -- TODO: Once we have scheduling, we must wait for one or the other to become more defined, rather than failing
-    _  -> err (TypeMismatch tm (show exp) (show act))
- where
-  getEnd (VApp (VPar e) _) = Just e
-  getEnd (VNum n) = getNumVar n
-  getEnd _ = Nothing
-
--- This will update the `hopes`, potentially invalidating things that have
--- been eval'd.
--- The Sem is closed, for now.
-solveHope :: TypeKind -> InPort -> Sem -> Checking ()
-solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of
-  Right () -> do
-    defineEnd (InEnd hope) v
-    dangling <- case (k, v) of
-      (Nat, VNum _v) -> err $ Unimplemented "Nat hope solving" []
-      (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
-      _ -> buildConst Unit TUnit
-    req (Wire (end dangling, kindType k, hope))
-    req (RemoveHope hope)
-  Left msg -> case v of
-    VApp (VPar (InEnd end)) B0 | hope == end -> pure ()
-    -- TODO: Not all occurrences are toxic. The end could be in an argument
-    -- to a hoping variable which isn't used.
-    -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1.
-    _ -> err msg
+    -- tricky: must wait for one or other to become more defined
+    es -> mkYield "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
 
 typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking ()
 typeEqs _ _ [] [] [] = pure ()
-typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = typeEqs tm stuff ks exps acts <* typeEq' tm stuff k exp act
+typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = do
+  mkFork "typeEqsTail" $ typeEqs tm stuff ks exps acts
+  typeEq' tm stuff k exp act
 typeEqs _ _ _ _ _ = typeErr "arity mismatch"
 
 typeEqRow :: Modey m
@@ -145,7 +130,7 @@ typeEqRigid tm (_ :* _ :* semz) Nat exp act = do
   act <- sem semz act
   if getNum exp == getNum act
   then pure ()
-  else err $ TypeMismatch tm (show exp) (show act)
+  else err $ TypeMismatch tm ("TYPEEQRIGID " ++ show exp) ("TODO " ++ show act)
 typeEqRigid tm stuff@(_ :* kz :* _) (TypeFor m []) (VApp f args) (VApp f' args') | f == f' =
   svKind f >>= \case
     TypeFor m' ks | m == m' -> typeEqs tm stuff (snd <$> ks) (args <>> []) (args' <>> [])

brat/Brat/Checker/SolveNumbers.hs

@@ -0,0 +1,209 @@
+module Brat.Checker.SolveNumbers (unifyNum) where
+
+import Brat.Checker.Monad
+import Brat.Checker.Helpers
+import Brat.Syntax.Value
+import Brat.Syntax.Common
+import Brat.Syntax.Port
+import Brat.Error
+import Brat.Eval
+import Brat.Graph (NodeType(..))
+import Brat.Naming
+import Hasochism
+import Control.Monad.Freer
+
+-- import Debug.Trace
+import qualified Data.Set as S
+
+trailM :: Applicative f => String -> f ()
+trailM = const (pure ())
+trail = const id
+--trail = trace
+
+-- This is currently lifted from SolvePatterns, which still imports it.
+-- It is also used in SolveHoles, where it does the right mathematics
+-- but the wrong wiring.
+
+-- Solve a Nat kinded metavariable. Unlike `instantiateMeta`, this function also
+-- makes the dynamic wiring for a metavariable. This only needs to happen for
+-- numbers because they have nontrivial runtime behaviour.
+--
+-- We assume that the caller has done the occurs check and rules out trivial equations.
+-- The caller also must check we have the right to solve the End
+solveNumMeta :: (End -> Maybe String) -> End -> NumVal (VVar Z) -> Checking ()
+solveNumMeta _ e nv | trail ("solveNumMeta " ++ show e ++ " " ++ show nv) False = undefined
+solveNumMeta mine e nv = case (e, numVars nv) of
+ -- Compute the thing that the rhs should be based on the src, and instantiate src to that
+ (ExEnd src,  [InEnd _tgt]) -> do
+   -- Compute the value of the `tgt` variable from the known `src` value by inverting nv
+   tgtSrc <- invertNatVal nv
+   instantiateMeta "solveNumExIn" (ExEnd src) (VNum (nVar (VPar (toEnd tgtSrc))))
+   wire (NamedPort src "", TNat, tgtSrc)
+
+ (ExEnd src, _) -> instantiateMeta "solveNumEx_" (ExEnd src) (VNum nv)
+
+ -- Both targets, we need to create the thing that they both derive from
+ (InEnd bigTgt, [InEnd weeTgt]) -> do
+     (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0))
+                                         (REx ("n", Nat) R0) (REx ("n", Nat) R0)
+     defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt))))
+     let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace
+     bigSrc <- buildNatVal nv'
+     nv' <- quoteNum Zy <$> numEval S0 nv'
+     instantiateMeta "solveNumInIn" (InEnd bigTgt) (VNum nv')
+     wire (bigSrc, TNat, NamedPort bigTgt "")
+     unifyNum mine (nVar (VPar (toEnd idSrc))) (nVar (VPar (toEnd weeTgt)))
+
+
+
+ -- RHS is constant or Src, wire it into tgt
+ (InEnd tgt,  _) -> do
+   src <- buildNatVal nv
+   instantiateMeta "solveNumIn_" (InEnd tgt) (VNum nv)
+   wire (src, TNat, NamedPort tgt "")
+
+unifyNum :: (End -> Maybe String) -> NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
+unifyNum mine nv0 nv1 = do
+  trailM $ ("unifyNum In\n  " ++ show nv0 ++ "\n  " ++ show nv1)
+  nv0 <- numEval S0 nv0
+  nv1 <- numEval S0 nv1
+  unifyNum' mine (quoteNum Zy nv0) (quoteNum Zy nv1)
+  nv0 <- numEval S0 (quoteNum Zy nv0)
+  nv1 <- numEval S0 (quoteNum Zy nv1)
+  trailM $ ("unifyNum Out\n  " ++ show (quoteNum Zy nv0) ++ "\n  " ++ show (quoteNum Zy nv1))
+
+-- Need to keep track of which way we're solving - which side is known/unknown
+-- Things which are dynamically unknown must be Tgts - information flows from Srcs
+-- ...But we don't need to do any wiring here, right?
+unifyNum' :: (End -> Maybe String) -> NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
+unifyNum' _ a b | trail ("unifyNum'\n  " ++ show a ++ "\n  " ++ show b) False = undefined
+unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
+  | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro)
+  | otherwise  = lhsFun00 rgro (NumValue (lup - rup) lgro)
+ where
+  lhsFun00 :: Fun00 (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsFun00 Constant0 num = demand0 num
+  -- Both sides are variables
+  lhsFun00 (StrictMonoFun (StrictMono 0 (Linear v))) (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v')))) = flexFlex v v'
+  -- There's just a variable on the right - move it to the left
+  lhsFun00 sm (NumValue 0 (StrictMonoFun smv@(StrictMono 0 (Linear _)))) = lhsStrictMono smv (NumValue 0 sm)
+  lhsFun00 (StrictMonoFun sm) num = lhsStrictMono sm num
+
+  flexFlex :: VVar Z -> VVar Z -> Checking ()
+  flexFlex v v' = case compare v v' of
+    GT -> flexFlex v' v
+    EQ -> pure ()
+    LT -> case (v, v') of
+      (VPar e@(ExEnd p), VPar e'@(ExEnd p'))
+       | Just _ <- mine e -> defineSrc (NamedPort p "") (VNum (nVar v'))
+       | Just _ <- mine e' -> defineSrc (NamedPort p' "") (VNum (nVar v))
+       | otherwise -> typeErr $ "Can't force " ++ show v ++ " to be " ++ show v'
+      (VPar e@(InEnd p), VPar e'@(ExEnd dangling))
+       | Just _ <- mine e -> do
+          req (Wire (dangling, TNat, p))
+          defineTgt' ("flex-flex In Ex") (NamedPort p "") (VNum (nVar v'))
+       | Just _ <- mine e' -> do
+          req (Wire (dangling, TNat, p))
+          defineSrc' ("flex-flex In Ex") (NamedPort dangling "") (VNum (nVar v))
+       | otherwise -> mkYield "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
+      (VPar e@(InEnd p), VPar e'@(InEnd p'))
+       | Just _ <- mine e -> defineTgt' "flex-flex In In1" (NamedPort p "") (VNum (nVar v'))
+       | Just _ <- mine e' -> defineTgt' "flex-flex In In0"(NamedPort p' "") (VNum (nVar v))
+       | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
+
+  lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
+  lhsStrictMono (StrictMono n mono) num = do
+    num <- traceChecking "lhsSM demandEven" demandEven num
+    unifyNum mine (NumValue 0 (StrictMonoFun (StrictMono (n - 1) mono))) num
+
+  lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsMono (Linear (VPar e)) num | x <- mine e, trail ("lhsMono\n  " ++ show e ++ "\n  " ++ show num ++ "\n  " ++ show x) False = undefined
+  -- x = f(x) has 3 solutions, otherwise we should complain!
+  lhsMono lhs@(Linear (VPar e)) num | [e'] <- numVars num, e == e' = case num of
+    (NumValue 0 (StrictMonoFun sm)) -> case anyDoubsAnyFulls sm of
+      (True, _) -> lhsMono lhs (nConstant 0)
+      (False, True) -> mkYield "lhsMono2Sols" (S.singleton e) >>
+                       unifyNum mine (nVar (VPar e)) num
+      (False, False) -> pure ()
+    _ -> err . UnificationError $ "Can't make " ++ show e ++ " = " ++ show num
+  lhsMono (Linear (VPar e)) num = case mine e of
+    Just loc -> loc -! solveNumMeta mine e num
+    _ -> mkYield "lhsMono" (S.singleton e) >>
+         unifyNum mine (nVar (VPar e)) num
+  lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm'))))
+    = lhsFun00 (StrictMonoFun sm) (NumValue 0 (StrictMonoFun sm'))
+  lhsMono m@(Full _) (NumValue 0 gro) = trail "lhsMono swaps" $ lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m)))
+  lhsMono (Full sm) (NumValue up gro) = do
+    smPred <- traceChecking "lhsMono demandSucc" demandSucc (NumValue 0 (StrictMonoFun sm))
+    _ <- numEval S0 sm
+    -- trailM $ "succ now " ++ show (quoteNum Zy sm)
+    unifyNum mine (n2PowTimes 1 (nFull smPred)) (NumValue (up - 1) gro)
+
+  anyDoubsAnyFulls :: StrictMono (VVar Z) -> (Bool, Bool)
+  anyDoubsAnyFulls (StrictMono k (Full rest)) = let (ds,_) = anyDoubsAnyFulls rest in (k > 0 || ds, True)
+  anyDoubsAnyFulls (StrictMono k (Linear _)) = (k > 0, False)
+
+  demand0 :: NumVal (VVar Z) -> Checking ()
+  demand0 (NumValue 0 Constant0) = pure ()
+  demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of
+    Linear (VPar e) | Just _ <- mine e -> solveNumMeta mine e (nConstant 0)
+    Full sm -> demand0 (NumValue 0 (StrictMonoFun sm))
+    _ -> err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
+  demand0 n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
+
+  -- Complain if a number isn't a successor, else return its predecessor
+  demandSucc :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
+      --   2^k * x
+      -- = 2^k * (y + 1)
+      -- = 2^k + 2^k * y
+      -- Hence, the predecessor is (2^k - 1) + (2^k * y)
+  demandSucc (NumValue k x) | k > 0 = pure (NumValue (k - 1) x)
+  demandSucc (NumValue 0 (StrictMonoFun (mono@(StrictMono k (Linear (VPar e))))))
+    | Just loc <- mine e = do
+      pred <- loc -! traceChecking "makePred" makePred e
+      pure (nPlus ((2^k) - 1) (nVar (VPar pred)))
+
+  --   2^k * full(n + 1)
+  -- = 2^k * (1 + 2 * full(n))
+  -- = 2^k + 2^(k + 1) * full(n)
+
+    | otherwise = do
+      mkYield "demandSucc" (S.singleton e)
+      nv <- quoteNum Zy <$> numEval S0 mono
+      demandSucc nv
+
+  -- if it's not "mine" should we wait?
+  demandSucc (NumValue 0 (StrictMonoFun (StrictMono k (Full nPlus1)))) = do
+    n <- traceChecking "demandSucc" demandSucc (NumValue 0 (StrictMonoFun nPlus1))
+    -- foo <- numEval S0 x
+    -- trailM $ "ds: " ++ show x ++ " -> " ++ show (quoteNum Zy foo)
+    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes (k + 1) $ nFull n
+  demandSucc n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be a successor"
+
+  -- Complain if a number isn't even, otherwise return half
+  demandEven :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
+  demandEven (NumValue up gro) = case up `divMod` 2 of
+    (up, 0) -> nPlus up <$> traceChecking "evenGro" evenGro gro
+    (up, 1) -> nPlus (up + 1) <$> traceChecking "oddGro" oddGro (NumValue 0 gro)
+   where
+    evenGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z))
+    evenGro Constant0 = pure $ nConstant 0
+    evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
+      Linear (VPar e)
+        | Just loc <- mine e -> loc -! do
+          -- trailM $ "Calling makeHalf (" ++ show e ++ ")"
+          half <- traceChecking "makeHalf" makeHalf e
+          pure (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar half)))))
+        | otherwise -> do
+          mkYield "evenGro" (S.singleton e)
+          nv <- quoteNum Zy <$> numEval S0 mono
+          demandEven nv
+      Full sm -> nConstant 0 <$ demand0 (NumValue 0 (StrictMonoFun sm))
+    evenGro (StrictMonoFun (StrictMono n mono)) = pure (NumValue 0 (StrictMonoFun (StrictMono (n - 1) mono)))
+
+    -- Check a numval is odd, and return its rounded down half
+    oddGro :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
+    oddGro x = do
+     pred <- demandSucc x
+     demandEven pred