cleaning / erasure occasionally results in poor warnings

[marklemay]

the nieve way erasure and cleaning is carried out makes it is possible for an elaborated term like

TyU   1    TyU  2
   \     /        \   /
   Same    Same 
         \       /
         Same  

to give a warning like * =?= *

this would be solved is cleaning checked endpoints and end turned the root same into a union

TyU   1    TyU  2
   \     /        \   /
   Same    Same 
         \       /
         Union  

this is actually obnoxious to handle efficiently, but a "many holed context" that partially extracts the endpoints would probably be the best way to do it...

what I have so far

-- InplaceEndpoints
data IE = IE {endpointsl :: [Exp], endpointsr :: [Exp], reconstruct:: [Exp]->[Exp]->Exp} 
-- probly need a way to norm this that allows holes to expand


toExp :: IE -> Exp
toExp (IE lrest1 lrest reconstruct) = reconstruct lrest1 lrest

expHole :: Exp -> IE
expHole e = IE [] [e] $ \ [] [x] -> x

bakeHead :: IE -> IE
bakeHead (IE lrest1 (l:lrest) reconstruct) = IE lrest1 lrest $ (\ holes1 holes -> reconstruct holes1 $ l : holes )

pass :: IE -> IE
pass (IE lrest1 (l:lrest) reconstruct) = IE (lrest1++[l]) lrest $ (\ (snoc -> (holes1,hole)) holes -> reconstruct holes1 $ hole : holes )

restartHead :: IE -> IE
restartHead (IE lrest1 (lrest) reconstruct) = IE [] (lrest1++lrest) $ (\ [] holes -> let
  (holes1, holes2) = splitAt (length lrest1) holes
  in reconstruct holes1 holes2)

atEnd :: IE -> Bool
atEnd (IE lrest1 [] reconstruct) = True
atEnd _ = False


head :: IE -> Exp
head (IE lrest1 (e:lrest) reconstruct) = e

updateHead :: IE -> Exp -> IE
updateHead  (IE lrest1 (_:lrest) reconstruct) e = IE lrest1 (e:lrest) reconstruct

normHead :: (MonadState Integer m, WithDynDefs m, Fresh m) =>
  IE -> m IE
normHead (IE erest1 (e:erest) reconstruct) = do
  e' <- safeWhnf' e
  case e' of
    C l lc -> normHead $ IE erest1 (l:erest) (\ holes1 (hole:holes) -> reconstruct holes1 ((C hole lc):holes))
    Same l1 info lc l2 -> normHead $ IE  erest1 (l1:l2:erest) (\ holes1 (hole1:hole2:holes) -> reconstruct holes1 ((Same hole1 info lc hole2):holes))
    Union l1 lc l2 -> normHead $ IE erest1 (l1:l2:erest) (\ holes1 (hole1:hole2:holes) -> reconstruct holes1 ((Union hole1 lc hole2):holes))
    _ -> pure $ IE erest1 (e':erest) reconstruct


e1 = toExp $ bakeHead $  IE [V $ s2n "x"] [V $ s2n "y", V $ s2n "z"] (\ [x] [y,z] -> Same x dummyInfo y z)
e2 = toExp $ pass $  IE [V $ s2n "x"] [V $ s2n "y", V $ s2n "z"] (\ [x] [y,z] -> Same x dummyInfo y z)
e3 = toExp $ restartHead $  IE [V $ s2n "x"] [V $ s2n "y", V $ s2n "z"] (\ [x] [y,z] -> Same x dummyInfo y z)


-- caleanSame ::  (MonadState Integer m, WithDynDefs m, Fresh m) =>
--   IE -> Info -> Exp -> IE -> m Exp
-- caleanSame (IE [] ((C l lc):lrest) reconstruct) info ty r = caleanSame (IE (l:lrest) (\ (hole:holes) -> reconstruct ((C hole lc):holes))) info ty r
-- caleanSame l info ty (IE ((C r rc):rrest) reconstruct) = caleanSame l info ty (IE (r:rrest) (\ (hole:holes) -> reconstruct ((C hole rc):holes))) 
-- caleanSame (IE (l:lrest) lreconstruct) info ty (IE (r:rrest) rreconstruct) = do
--   l' <- safeWhnf' l
--   r' <- safeWhnf' r
--   case (l', r') of

-- check if 2 expressions share an endpoint, with lazily normalize the epressions in-place
-- precondition assume left head is normewd as much as sensable
-- this took an embarassingly long time to come up with and is an affront to good taste... this might be a hackty version of lenses?
shareEnpoint' ::  (MonadState Integer m, WithDynDefs m, Fresh m) =>
  IE -> IE -> m (IE, IE, Bool)

  -- TODO do a quick erase check
shareEnpoint' l@(atEnd-> True) r@(atEnd-> True) = pure (l, r, False)
shareEnpoint' l r@(atEnd-> True) = shareEnpoint' (pass l) (restartHead r)

shareEnpoint' l@(head-> TyU) r = do
  r' <- normHead r
  case r' of
    (head-> TyU) -> pure (l, r', True)
    _ -> shareEnpoint' l (pass r')

shareEnpoint' l@(head-> (Pi laTy bndlBod)) r = do
  r' <- normHead r
  case r' of
    (head-> (Pi raTy bndrBod)) -> do
      (laTy', raTy', match) <- shareEnpoint' (expHole laTy) (expHole raTy)
      -- consider Pis not injective
      -- if match
      -- then undefined
      -- else shareEnpoint' (updateHead l (Pi laTy' bndlBod))
      undefined
    _ -> shareEnpoint' l (pass r')