Stack machine2/missing

brat/Brat/Checker/Helpers.hs

@@ -634,7 +634,10 @@ solveVal Nat it@(InEnd inn) v@(VNum nv) = do
   dangling <- buildNatVal nv
   req (Wire (end dangling, TNat, inn))
   defineEnd "solveValNat" it v
-solveVal _ it v = defineEnd "solveVal" it v
+solveVal k@(TypeFor _ _) it@(InEnd inn) v = do
+  (_, _, [(dummySrc, _)], _) <- anext "" (Dummy k) (S0, Some (Zy :* S0)) R0 (REx ("dummy", k) R0)
+  req $ Wire (end dummySrc, kindType k, inn)
+  defineEnd "solveVal" it v
   -- Do we also need dummy wiring here?
 
 solveSem :: TypeKind -> End -> Sem -> Checking ()

brat/Brat/Checker/Monad.hs

@@ -22,18 +22,18 @@ import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.Set as S
 
--- import Debug.Trace
+import Debug.Trace
 
 -- Used for messages about thread forking / spawning
 thTrace = const id
 --thTrace = trace
 
 trackM :: Monad m => String -> m ()
-trackM = const (pure ())
---trackM = traceM
+--trackM = const (pure ())
+trackM = traceM
 
-track = const id
---track = trace
+--track = const id
+track = trace
 trackShowId x = track (show x) x
 
 -- Data for using a type alias. E.g.
@@ -120,6 +120,7 @@ data CheckingSig ty where
   ANewDynamic :: InPort -> FC -> CheckingSig ()
   AskDynamics :: CheckingSig (M.Map InPort FC)
   AddCapture :: Name -> (QualName, [(Src, BinderType Brat)]) -> CheckingSig ()
+  WiresIn :: Name -> CheckingSig [Wire]
 
 wrapper :: (forall a. CheckingSig a -> Checking (Maybe a)) -> Checking v -> Checking v
 wrapper _ (Ret v) = Ret v
@@ -319,6 +320,8 @@ handler (Req s k) ctx g
       AddCapture n (var, ends) ->
         handler (k ()) ctx {captureSets=M.insertWith M.union n (M.singleton var ends) (captureSets ctx)} g
 
+      WiresIn n -> handler (k (wiresTo n g)) ctx g
+
 handler (Define lbl end v k) ctx g = let st@Store{typeMap=tm, valueMap=vm} = store ctx in
   case track ("Define(" ++ lbl ++ ")" ++ show end ++ " = " ++ show v) $ M.lookup end vm of
       Just _ -> Left $ dumbErr (InternalError $ "Redefining " ++ show end)

brat/Brat/Checker/SolveNumbers.hs

@@ -12,13 +12,14 @@ import Brat.Naming
 import Hasochism
 import Control.Monad.Freer
 
--- import Debug.Trace
+import Debug.Trace
 import qualified Data.Set as S
 
 trailM :: Applicative f => String -> f ()
-trailM = const (pure ())
-trail = const id
---trail = trace
+--trailM = const (pure ())
+trailM = traceM
+--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
@@ -90,15 +91,18 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
   lhsFun00 (StrictMonoFun sm) num = lhsStrictMono sm num
 
   flexFlex :: VVar Z -> VVar Z -> Checking ()
+  flexFlex v v' | trace ("flexFlex " ++ show v ++ " " ++ show v') False = undefined
   flexFlex v v' = case compare v v' of
-    GT -> flexFlex v' v
-    EQ -> pure ()
+    GT | trace "GT" False -> undefined | otherwise -> flexFlex v' v
+    EQ | trace "EQ" False -> undefined | otherwise -> pure ()
     LT -> case (v, v') of
       (VPar e@(ExEnd p), VPar e'@(ExEnd p'))
+       | trace "ExEx" False -> undefined
        | 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))
+       | trace "InEx" False -> undefined
        | Just _ <- mine e -> do
           req (Wire (dangling, TNat, p))
           defineTgt' ("flex-flex In Ex") (NamedPort p "") (VNum (nVar v'))
@@ -107,10 +111,36 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
           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))
+       | trace "InIn" False -> undefined
+       | Just _ <- mine e -> solveInIn p p'
+       | Just _ <- mine e' -> solveInIn p' p
        | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
 
+  -- INVARIANT: The first argument is ours to solve
+  solveInIn :: InPort -> InPort -> Checking ()
+  solveInIn e0@(In node0 _) e1@(In node1  _) = do
+    ws0 <- req $ WiresIn node0
+    ws1 <- req $ WiresIn node1
+    mine <- mineToSolve
+    me <- whoAmI
+    case (ws0, ws1) of
+      ([], [(dangling, ty, _)]) -> do
+        req $ Wire (dangling, ty, e0)
+        defineTgt' "solveInIn" (NamedPort e0 "") (VNum (nVar (VPar (toEnd e1))))
+      ([], [])
+       | Just _ <- mine (InEnd e1) -> do
+        (_, [(tgt,_)], [(src0, _), (src1, _)], _) <- anext "copyInIn" Copy (S0, Some (Zy :* S0)) (REx ("clonee", Nat) R0) (REx ("clone0", Nat) (REx ("clone1", Nat) R0))
+        defineTgt' "solveInInCopy" (NamedPort e0 "") (VNum (nVar (VPar (toEnd tgt))))
+        defineTgt' "solveInInCopy" (NamedPort e1 "") (VNum (nVar (VPar (toEnd tgt))))
+        req $ Wire (end src0, TNat, e0)
+        req $ Wire (end src1, TNat, e1)
+       | otherwise -> error $ "solveInIn: rhs not ours to solve: " ++ show e1 ++ "\n we are " ++ show me
+      (_, []) -> err (Unimplemented  "solveInIn: ours defined; other not" [])
+      -- Both things already wired up; just do the statics
+      _ -> defineTgt' "solveInInStatic" (NamedPort e0 "") (VNum (nVar (VPar (toEnd e1))))
+
+
+
   lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
   lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
   lhsStrictMono (StrictMono n mono) num = do