free-theorems-counterexamples-0.3: Language/Haskell/FreeTheorems/Variations/CounterExamples/Internal/ExFindExtended.hs
-- * The module contains all rules of ExFind and the algorithm itself (the sequence in which the rules are used).
module Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended (alg) where
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
import Prelude hiding (Either(..))
import qualified Prelude as E (Either(..))
import Data.List
import qualified Data.Map as Map
import Control.Monad
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)
import qualified Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M as Mona (M)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync
-------Regeln der ersten Phase-------------
-- * The rules of the algorithm
-- The rules have at most three parts:
-- - rule == term construction
-- - rule_tc_update == alternation of the term environments (TermCont)
-- - rule_trackCont_update == alternation of the disrelater (TrackCont)
-- | auxiliary function for tc update
pLusVal_tc_update :: TermCont -> TypedVar -> M TermCont
pLusVal_tc_update tc var =
let (v,tau) = var in
do {Just p <- makePlusPair tau;
return (Map.insert v (p,Leaf) tc)
}
-- ** first phase
-- *** rules without backtracking
bOttom :: Cont -> Typ -> Maybe Term
bOttom gamma tau = if isElementaryType tau && unpointed (tVars gamma) tau
then Just (Bottom tau)
else Nothing
-- |initialises the term environments with plus-terms for each term variable in the term variable context
bOttom_tc_update :: Cont -> M TermCont
bOttom_tc_update gamma = initialiseTermCont (vars gamma)
rAllStar :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
rAllStar gamma tau = case tau of
AllStar tv tau' -> Just (updateTVarStar gamma tv, tau', \m -> TAbs tv m)
_ -> Nothing
rAll :: Cont -> Typ -> Maybe (Cont, Typ, Term -> Term)
rAll gamma tau = case tau of
All tv tau' -> Just (updateTVar gamma tv, tau', \m -> TAbs tv m)
_ -> Nothing
aBs :: Cont -> Typ -> Maybe (M (Cont, TermVar, Term -> Term), Typ)
aBs gamma tau = case tau of
Arrow tau1 tau2 -> Just (do {i <- newInt;
let x = TermVar i in
return (updateVar gamma x tau1, x, \m -> Abs x tau1 m)
}
, tau2)
_ -> Nothing
aBs_tc_update :: TermCont -> TermVar -> TermCont
aBs_tc_update tc v = Map.delete v tc
aBs_trackCont_update :: TrackCont -> Typ -> TermCont -> TermVar -> M TrackCont
aBs_trackCont_update trackCont tau tc v =
let (tau,trc) = trackCont
((x1,x2),_) = trace "Map.! abs_trackCont_update" (tc Map.! v) in
do{i <- newAux;
j <- newAux;
k <- newAux;
assoc k x2;
assoc j x1;
let u = TermVar i in
return (tau,(Abs u tau (App (Var u) (Var (TermVar j))), Abs u tau (App (Var u) (Var (TermVar k)))):trc)
}
wRap :: Typ -> Maybe (Typ, Term -> Term)
wRap tau = case tau of
List tau' -> Just (tau', \m -> Cons m (Nil tau'))
_ -> Nothing
wRap_trackCont_update :: TrackCont -> Typ -> M TrackCont
wRap_trackCont_update trackCont tau =
let (ctau,trc) = trackCont
List tau' = tau in
do{f <- listhead tau';
return (ctau,(f,f):trc)
}
mAybe :: Typ -> Maybe (Typ, Term -> Term)
mAybe tau = case tau of
TMaybe tau' -> Just (tau', \m -> MJust m)
_ -> Nothing
mAybe_trackCont_update :: TrackCont -> Typ -> M TrackCont
mAybe_trackCont_update trackCont tau =
let (ctau,trc) = trackCont
TMaybe tau' = tau in
do{f <- fromJust tau';
return (ctau,(f,f):trc)
}
wRapTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))
wRapTo gamma = let f = findfirst typeCheckArrowListArg (vars gamma) in
case f of
Nothing -> Nothing
Just (v, (Arrow (List tau1) tau2)) ->
Just (do {i <- newAux; --g in the new context
j <- newInt; --y for substitution
let g = TermVar i
y = TermVar j in
return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),
\m -> subst m (Abs y tau1 (App (Var v) (Cons (Var y) (Nil tau1)))) g),
((g,Arrow tau1 tau2), (v, Arrow (List tau1) tau2)))
})
wRapTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont
wRapTo_tc_update tc l h g f =
let Arrow (List t1) t2 = snd f
((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))
in
Map.delete (fst g) (Map.insert (fst f) ((Abs l (List t1) (LCase (Var l) h (App x (Var h))),Abs l (List t1) (LCase (Var l) h (App y (Var h)))),Branch WrapTo his) tc)
mAybeTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar, TypedVar)))
mAybeTo gamma = let f = findfirst typeCheckArrowMaybeArg (vars gamma) in
case f of
Nothing -> Nothing
Just (v, (Arrow (TMaybe tau1) tau2)) ->
Just (do {i <- newAux; --g in the new context
j <- newInt; --y for substitution
let g = TermVar i
y = TermVar j in
return ((updateVar (removeVar gamma v) g (Arrow tau1 tau2),
\m -> subst m (Abs y tau1 (App (Var v) (MJust (Var y)))) g),
((g,Arrow tau1 tau2), (v, Arrow (TMaybe tau1) tau2)))
})
mAybeTo_tc_update :: TermCont -> TermVar -> TermVar -> TypedVar -> TypedVar -> TermCont
mAybeTo_tc_update tc l h g f =
let Arrow (TMaybe t1) t2 = snd f
((x,y),his) = (trace "Map.!-check: wRapTo g" (tc Map.! (fst g)))
in
Map.delete (fst g) (Map.insert (fst f) ((Abs l (TMaybe t1) (MCase (Var l) h (App x (Var h))),Abs l (TMaybe t1) (MCase (Var l) h (App y (Var h)))),Branch MaybeTo his) tc)
hEad :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
hEad gamma tau' = let l = findfirst typeCheckList (vars gamma) in
case l of
Nothing -> Nothing
Just (v,List tau) -> Just (do {lh <- listheadApp (Var v) tau;
i <- newInt; --h
let h = TermVar i in
return ((updateVar (removeVar gamma v) h tau,
\m -> subst m lh h),
((h,tau),(v,List tau)))
})
hEad_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
hEad_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: hEad h" (tc Map.! (fst h))) in
Map.delete (fst h) (Map.insert (fst l) ((Cons x (Nil (snd h)), Cons y (Nil (snd h))),Branch Head his) tc)
jUst :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
jUst gamma tau' = let l = findfirst typeCheckMaybe (vars gamma) in
case l of
Nothing -> Nothing
Just (v,TMaybe tau) -> Just (do {lh <- fromJustApp (Var v) tau;
i <- newInt; --h
let h = TermVar i in
return ((updateVar (removeVar gamma v) h tau,
\m -> subst m lh h),
((h,tau),(v,TMaybe tau)))
})
jUst_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
jUst_tc_update tc h l = let ((x,y),his) = (trace "Map.!-check: jUst h" (tc Map.! (fst h))) in
Map.delete (fst h) (Map.insert (fst l) ((MJust x, MJust y),Branch RJust his) tc)
dRop1 :: Cont -> Maybe (Cont,TermVar)
dRop1 gamma = let l = findfirst typeCheckInt (vars gamma) in
case l of
Nothing -> Nothing
Just var -> Just ((removeVar gamma (fst var)),fst var)
dRop1_tc_update :: TermCont -> TermVar -> TermCont
dRop1_tc_update tc v = Map.insert v ((Zero,Zero),Leaf) tc
dRop2 :: Cont -> Maybe (Cont,TermVar)
dRop2 gamma = let l = findfirst typeCheckBrace (vars gamma) in
case l of
Nothing -> Nothing
Just var -> Just ((removeVar gamma (fst var)),fst var)
dRop2_tc_update :: TermCont -> TermVar -> TermCont
dRop2_tc_update tc v = Map.insert v ((Brace,Brace),Leaf) tc
dRop4 :: Cont -> Maybe (Cont,TermVar)
dRop4 gamma = let l = findfirst typeCheckBool (vars gamma) in
case l of
Nothing -> Nothing
Just var -> Just ((removeVar gamma (fst var)),fst var)
dRop4_tc_update :: TermCont -> TermVar -> TermCont
dRop4_tc_update tc v = Map.insert v ((Fls,Fls),Leaf) tc
dRop3 :: Cont -> Maybe (Cont,TypedVar)
dRop3 gamma = let l = findfirstWithTVars unpointed (tVars gamma) (vars gamma) in
case l of
Nothing -> Nothing
Just var -> Just ((removeVar gamma (fst var)),var)
dRop3_tc_update :: TermCont -> TypedVar -> M TermCont
dRop3_tc_update = pLusVal_tc_update
pAirTo :: Cont -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
pAirTo gamma = let l = findfirst typeCheckArrowPairArg (vars gamma) in
case l of
Nothing -> Nothing
Just (f, (Arrow (TPair tau1 tau2) tau3)) ->
Just (do {i <- newAux; --g in the new context
j <- newInt;
k <- newInt;
let g = TermVar i
x = TermVar j
y = TermVar k in
return ((updateVar (removeVar gamma f) g (Arrow tau1 (Arrow tau2 tau3)),
\m -> subst m (Abs x tau1 (Abs y tau2 (App (Var f) (Pair (Var x) (Var y))))) g),((g,Arrow tau1 (Arrow tau2 tau3)),(f,(Arrow (TPair tau1 tau2) tau3))))
})
pAirTo_tc_update :: TermCont -> TypedVar -> TypedVar -> M (TermCont)
pAirTo_tc_update tc g f = do {i <- newInt;
j <- newInt;
k <- newInt;
let p = TermVar i
x = TermVar j
y = TermVar k
Arrow tau tau3 = snd f
((z,z'),his) = (trace "Map.!-check: pAirTo g" (tc Map.! (fst g)))
in
return (Map.delete (fst g) (Map.insert (fst f) ((Abs p tau (PCase (Var p) x y (App (App z (Var x)) (Var y))),Abs p tau (PCase (Var p) x y (App (App z' (Var x)) (Var y)))),Branch PairTo his) tc))
}
pRoj :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
pRoj gamma = let l = findfirst typeCheckPair (vars gamma) in
case l of
Nothing -> Nothing
Just (p, TPair tau1 tau2) ->
Just (do {i <- newInt;
j <- newInt;
let x = TermVar i
y = TermVar j in
do {f <- firstApp (Var p);
s <- secondApp (Var p);
return ((updateVar (updateVar (removeVar gamma p) x tau1) y tau2,
\m -> subst (subst m f x) s y),
([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
}
})
pRoj_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
pRoj_tc_update tc varIn p =
let [x,y] = varIn
((z,z'),his1) = (trace "Map.!-check: pRoj x" (tc Map.! (fst x)))
((u,u'),his2) = (trace "Map.!-check: pRoj y" (tc Map.! (fst y)))
in
Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'), Split Proj his1 his2) tc))
eItherTo :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
eItherTo gamma = let l = findfirst typeCheckArrowEitherArg (vars gamma) in
case l of
Nothing -> Nothing
Just (f, (Arrow (TEither tau1 tau2) tau3)) ->
Just (do {i <- newAux; --g in the new context
j <- newAux; --h in the new context
k <- newInt; --x in the term
l <- newInt; --y in the term
let g = TermVar i
h = TermVar j
x = TermVar k
y = TermVar l in
return ((updateVar (updateVar (removeVar gamma f) g (Arrow tau1 tau3)) h (Arrow tau2 tau3),
\m -> subst (subst m (Abs x tau1 (App (Var f) (Left (Var x)))) g) (Abs y tau2 (App (Var f) (Right (Var y)))) h),
([(g,Arrow tau1 tau3),(h,Arrow tau2 tau3)],(f,(Arrow (TEither tau1 tau2) tau3))))
})
eItherTo_tc_update :: TermCont -> [TypedVar] -> TypedVar -> M (TermCont)
eItherTo_tc_update tc varIn f = let [g,h] = varIn in
do{i <- newInt;
j <- newInt;
k <- newInt;
let e = TermVar i
x = TermVar j
y = TermVar k
Arrow tau tau3 = snd f
((z,z'),his1) = (trace "Map.!-check: eItherTo g" (tc Map.! (fst g)))
((u,u'),his2) = (trace "Map.!-check: eItherTo h" (tc Map.! (fst h)))
in
return (Map.delete (fst g) (Map.delete (fst h) (Map.insert (fst f) ((Abs e tau (ECase (Var e) x (App z (Var x)) y (App u (Var y))), Abs e tau (ECase (Var e) x (App z' (Var x)) y (App u' (Var y)))),Split EitherTo his1 his2) tc)))
}
-- *** rules with backtracking
dIst1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIst1 gamma tau = case findfirst typeCheckEither (vars gamma) of
Nothing -> Nothing
Just (e, TEither tau1 tau2) ->
Just (do {i <- newInt;
l <- fromLeftApp (Var e) tau1;
let x = TermVar i in
return ((updateVar (removeVar gamma e) x tau1,
\m -> subst m l x),
((x,tau1),(e, TEither tau1 tau2)))
})
dIst1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIst1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIst1 x" (tc Map.! (fst x)))
in
Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)
dIst2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIst2 gamma tau = case findfirst typeCheckEither (vars gamma) of
Nothing -> Nothing
Just (e, TEither tau1 tau2) ->
Just (do {r <- fromRightApp (Var e) tau2;
i <- newInt;
let y = TermVar i in
return ((updateVar (removeVar gamma e) y tau2,
\m -> subst m r y),
((y,tau2),(e,TEither tau1 tau2)))
})
dIst2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIst2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIst2 fst y" (tc Map.! (fst y)))
in
Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)
pAir1 :: Typ -> Maybe (Typ, Term -> Term)
pAir1 tau = case tau of
TPair tau1 tau2 -> Just (tau1, \m -> Pair m (Bottom tau2))
_ -> Nothing
pAir1_trackCont_update :: TrackCont -> Typ -> M TrackCont
pAir1_trackCont_update trackCont tau =
let (ctau,trc) = trackCont in
do{f <- first tau;
return (ctau,(f,f):trc)
}
pAir2 :: Typ -> Maybe (Typ, Term -> Term)
pAir2 tau = case tau of
TPair tau1 tau2 -> Just (tau2,\m -> Pair (Bottom tau1) m)
_ -> Nothing
pAir2_trackCont_update :: TrackCont -> Typ -> M TrackCont
pAir2_trackCont_update trackCont tau =
let (ctau,trc) = trackCont in
do{f <- second tau;
return (ctau,(f,f):trc)
}
lEft :: Typ -> Maybe (Typ, Term -> Term)
lEft tau = case tau of
TEither tau1 _ -> Just(tau1, \m -> Left m)
_ -> Nothing
lEft_trackCont_update :: TrackCont -> Typ -> M TrackCont
lEft_trackCont_update trackCont tau =
let (ctau,trc) = trackCont
TEither tau' tau'' = tau in
do{f <- fromLeft tau' tau'';
return (ctau,(f,f):trc)
}
rIght :: Typ -> Maybe (Typ, Term -> Term)
rIght tau = case tau of
TEither _ tau2 -> Just(tau2, \m -> Right m)
_ -> Nothing
rIght_trackCont_update :: TrackCont -> Typ -> M TrackCont
rIght_trackCont_update trackCont tau =
let (ctau,trc) = trackCont
TEither tau' tau'' = tau in
do{f <- fromRight tau' tau'';
return (ctau,(f,f):trc)
}
bOttomToStripe :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
bOttomToStripe gamma = let l = findallWithTVars typeCheckArrowUnPointedArgPointedRes (tVars gamma) (vars gamma) in
map makeone l
where makeone = \var -> let Arrow tau1 tau2 = snd var in
do {i <- newAux;
let x = TermVar i in
return (((updateVarStar (removeVar gamma (fst var)) x tau2)
, \m -> subst m (App (Var (fst var)) (Bottom tau1)) x),((x,tau2),var))
}
bOttomToStripe_tc_update :: TermCont -> Cont -> TypedVar -> TypedVar -> M TermCont
bOttomToStripe_tc_update tc gamma x f = let Arrow t1 t2 = snd f
((u,u'),his) = trace "Map.! bOttomToStripe_tc_update" (tc Map.! (fst x))
in
do{(g,g') <- makeFuncPair t1 (error "type of disrelater used, which is not set",[]) gamma (u,u');
return (Map.delete (fst x) (Map.insert (fst f) ((g,g'),Branch BottomToStripe his) tc))
}
aRrowToStar :: Cont -> [M (((Cont, Typ), Cont, Term -> Term -> Term), ([TypedVar],TypedVar))]
aRrowToStar gamma =
let l = findall typeCheckArrowArgArrow (vars gamma) in
map makeone l
where makeone var = let Arrow (Arrow tau1 tau2) tau3 = snd var in
do {i <- newInt;
j <- newInt;
let x = TermVar i
y = TermVar j in
return ((((updateVar (removeVar gamma (fst var)) x tau1),
tau2),
updateVarStar (removeVar gamma (fst var)) y tau3,
\m1 -> \m2 -> subst m2 (App (Var (fst var)) (Abs x tau1 m1)) y),
([(x,tau1),(y,tau3)],var))
}
------------------------ TermContext M_1 w y f TermContext -----
aRrowToStar_tc_update :: TrackCont -> TermCont -> Cont -> Term -> TypedVar -> TypedVar -> TypedVar -> M TermCont
aRrowToStar_tc_update trackCont tc gamma m1 w y f =
let (_,trc) = trackCont
Arrow t12 t3 = snd f
Arrow t1 t2 = t12
(resPair,hisy) = (trace "Map.!-check: aRrowToStar g-construct y (else)" (tc Map.! (fst y)))
in
do {i <- newInt;
(g,g') <- makeFuncPair t2 trackCont gamma resPair;
let u = TermVar i
((z,z'),hisw) = (trace "Map.!-check: aRrowToStar w" (tc Map.! (fst w)))
in
return (Map.delete (fst w) (Map.delete (fst y) (Map.insert (fst f) ((Abs u t12 (App g (App (Var u) z)), Abs u t12 (App g' (App (Var u) z'))),Split ArrowToStar hisw hisy) tc)))
}
bOttomTo :: Cont -> [M ((Cont, Term -> Term),(TypedVar,TypedVar))]
bOttomTo gamma =
let l = findall typeCheckArrow (vars gamma) in
map makeone l
where makeone var = let Arrow tau1 tau2 = snd var in
do {i <- newAux;
let x = TermVar i in
return ((updateVar (removeVar gamma (fst var)) x tau2,
\m -> subst m (App (Var (fst var)) (Bottom tau1)) x),
((x,tau2),var))
}
bOttomTo_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont
bOttomTo_tc_update tc z x f =
let Arrow t1 t2 = snd f
((u,u'),his) = (trace "Map.!-check: bOttomTo x" (tc Map.! (fst x)))
in
Map.delete (fst x) (Map.insert (fst f) ((Abs z t1 u, Abs z t1 u'), Branch BottomTo his) tc)
-- ** rules of the second phase
-- *** rules without backtracking
vArStar :: Cont -> Typ -> Maybe (Term, (TermVar,Typ))
vArStar gamma tau = if isElementaryType tau
then case findfirstSpecialType (varsStar gamma) tau of
Nothing -> Nothing
Just x -> Just (Var (fst x), x)
else Nothing
-- | creates the initial term variable environment.
vArStar_tc_update :: Cont -> M TermCont
vArStar_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))
bOttomToStar :: Cont -> Maybe (M ((Cont, Term -> Term),((TermVar,Typ),(TermVar,Typ))))
bOttomToStar gamma = case findfirst typeCheckArrow (varsStar gamma) of
Nothing -> Nothing
Just (f, Arrow tau1 tau2) -> Just (do {i <- newAux;
let y = TermVar i in
return ((updateVarStar (removeVarStar gamma f) y tau2, \m -> subst m (App (Var f) (Bottom tau1)) y),((y, tau2),(f, Arrow tau1 tau2) ));
})
bOttomToStar_tc_update :: TermCont -> TermVar -> TypedVar -> TypedVar -> TermCont
bOttomToStar_tc_update tc x varIn varOut = case (snd varOut) of
Arrow tau1 _ ->
let ((z,z'),his) = (trace "Map.!-check: bOttomToStar varIn" (tc Map.!(fst varIn)))
in
Map.delete (fst varIn) (Map.insert (fst varOut) ((Abs x tau1 z, Abs x tau1 z'),Branch BottomTo his) tc)
aPpStripStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
aPpStripStar gamma = checkall (findall typeCheckArrow (vars gamma))
where checkall xs =
case xs of
[] -> Nothing
((f, Arrow tau1 tau2):ys) -> if unpointed (tVars gamma) tau2
then checkall ys
else case findfirstSpecialType (varsStar gamma) tau1 of
Nothing -> checkall ys
Just (x,_) -> Just (do {i <- newAux;
let y = TermVar i in
return ((updateVarStar (removeVar gamma f) y tau2, \m -> subst m (App (Var f) (Var x)) y),([(x,tau1),(y,tau2)],(f,Arrow tau1 tau2)))
})
----------------------------------- x* y* f --------
aPpStripStar_tc_update :: TermCont -> Cont -> TermVar -> TypedVar -> TypedVar -> TypedVar -> M TermCont
aPpStripStar_tc_update tc gamma z x y f = let ((v,v'),his) = (trace "Map.!-check: aPpStripStar y (TVar)" (tc Map.! (fst y)))
in
do{fPair <- makeFuncPair (snd x) (error "unset disrelater type used",[]) gamma (v,v');
return (Map.delete (fst y) (Map.insert (fst f) (fPair,Branch BottomToStripe his) tc))
}
hEadStar :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
hEadStar gamma tau = case findfirst typeCheckList (varsStar gamma) of
Nothing -> Nothing
Just (l,List tau') -> Just (do {i <- newInt;
lh <- listheadApp (Var l) tau';
let h = TermVar i in
return ((updateVarStar (removeVarStar gamma l) h tau',
\m -> subst m lh h),
((h, tau'),(l,List tau')))
})
hEadStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: hEadStar fst h" (tc Map.!(fst h)))
in
Map.delete (fst h) (Map.insert (fst l) ((Cons u (Nil (snd h)), Cons u' (Nil (snd h))),Branch Head his) tc)
jUstStar :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
jUstStar gamma tau = case findfirst typeCheckList (varsStar gamma) of
Nothing -> Nothing
Just (l,TMaybe tau') -> Just (do {i <- newInt;
lh <- fromJustApp (Var l) tau';
let h = TermVar i in
return ((updateVarStar (removeVarStar gamma l) h tau',
\m -> subst m lh h),
((h, tau'),(l,TMaybe tau')))
})
jUstStar_tc_update tc h l = let ((u,u'),his) = (trace "Map.!-check: jUstStar h" (tc Map.!(fst h)))
in
Map.delete (fst h) (Map.insert (fst l) ((MJust u, MJust u'),Branch RJust his) tc)
pRojStar :: Cont -> Maybe (M ((Cont, Term -> Term),([TypedVar],TypedVar)))
pRojStar gamma = let l = findfirst typeCheckPair (varsStar gamma) in
case l of
Nothing -> Nothing
Just (p, TPair tau1 tau2) ->
Just (do {i <- newInt;
j <- newInt;
k <- newInt;
l <- newInt;
let x = TermVar i
y = TermVar j
u = TermVar k
v = TermVar l in
return ((updateVarStar (updateVarStar (removeVarStar gamma p) x tau1) y tau2,
\m -> subst (subst m (PCase (Var p) u v (Var u)) x) (PCase (Var p) u v (Var v)) y),
([(x,tau1),(y,tau2)],(p,TPair tau1 tau2)))
})
pRojStar_tc_update :: TermCont -> [TypedVar] -> TypedVar -> TermCont
pRojStar_tc_update tc varIn p =
let [x,y] = varIn
((z,z'),his1) = (trace "Map.!-check: pRojStar fst x" (tc Map.! (fst x)))
((u,u'),his2) = (trace "Map.!-check: pRojStar fst y" (tc Map.! (fst y)))
in
Map.delete (fst x) (Map.delete (fst y) (Map.insert (fst p) ((Pair z u, Pair z' u'),Split Proj his1 his2) tc))
iNtStar :: Cont -> Maybe (Cont,Term -> Term, TypedVar)
iNtStar gamma = case findfirstSpecialType (varsStar gamma) Int of
Nothing -> Nothing
Just x -> Just (removeVarStar gamma (fst x), \m -> ICase (Var (fst x)) m, x)
iNtStar_tc_update :: TermCont -> TermVar -> TermCont
iNtStar_tc_update tc var = Map.insert var ((Zero,Zero),Leaf) tc
bRaceStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)
bRaceStar gamma = case findfirstSpecialType (varsStar gamma) Int of
Nothing -> Nothing
Just x -> Just (removeVarStar gamma (fst x), \m -> BCase (Var (fst x)) m, x)
bRaceStar_tc_update :: TermCont -> TermVar -> TermCont
bRaceStar_tc_update tc var = Map.insert var ((Brace,Brace),Leaf) tc
bOolStar :: Cont -> Maybe (Cont, Term -> Term, TypedVar)
bOolStar gamma = case findfirstSpecialType (varsStar gamma) Int of
Nothing -> Nothing
Just x -> Just (removeVarStar gamma (fst x), \m -> BoolCase (Var (fst x)) m, x)
bOolStar_tc_update :: TermCont -> TermVar -> TermCont
bOolStar_tc_update tc var = Map.insert var ((Fls,Fls),Leaf) tc
lIstStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
lIstStar gamma = case findfirst typeCheckList (varsStar gamma) of
Nothing -> Nothing
Just x -> Just (do {i <- newInt;
let y = TermVar i in
return (removeVarStar gamma (fst x), \m -> LCase (Var (fst x)) y m, x)
})
lIstStar_tc_update :: TermCont -> TypedVar -> M TermCont
lIstStar_tc_update = pLusVal_tc_update
mAybeStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
mAybeStar gamma = case findfirst typeCheckMaybe (varsStar gamma) of
Nothing -> Nothing
Just x -> Just (do {i <- newInt;
let y = TermVar i in
return (removeVarStar gamma (fst x), \m -> MCase (Var (fst x)) y m, x)
})
mAybeStar_tc_update :: TermCont -> TypedVar -> M TermCont
mAybeStar_tc_update = pLusVal_tc_update
pAirStar :: Cont -> Maybe (M (Cont, Term -> Term, TypedVar))
pAirStar gamma = case findfirst typeCheckPair (varsStar gamma) of
Nothing -> Nothing
Just x -> Just (do {i <- newInt;
j <- newInt;
let y = TermVar i
z = TermVar j in
return (removeVarStar gamma (fst x), \m -> PCase (Var (fst x)) y z m, x)
})
pAirStar_tc_update :: TermCont -> TypedVar -> M TermCont
pAirStar_tc_update = pLusVal_tc_update
eItherStar :: Cont -> Typ -> Maybe (M (Cont, Term -> Term, TypedVar))
eItherStar gamma tau = case findfirst typeCheckEither (varsStar gamma) of
Nothing -> Nothing
Just x -> Just (do {i <- newInt;
j <- newInt;
let y = TermVar i
z = TermVar j in
return (removeVarStar gamma (fst x), \m -> ECase (Var (fst x)) y m z (Bottom tau), x)
})
eItherStar_tc_update :: TermCont -> TypedVar -> M TermCont
eItherStar_tc_update = pLusVal_tc_update
-- *** rules with backtracking
dIstStar1 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIstStar1 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
Nothing -> Nothing
Just (e, TEither tau1 tau2) ->
Just (do {i <- newInt;
j <- newInt;
let x = TermVar i
y = TermVar j in
return ((updateVarStar (removeVarStar gamma e) x tau1,
\m -> subst m (ECase (Var e) x (Var x) y (Bottom tau1)) x),
((x,tau1),(e,TEither tau1 tau2)))
})
dIstStar1_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIstStar1_tc_update tc x e = let ((z,z'),his) = (trace "Map.!-check: dIstStar1 x" (tc Map.! (fst x)))
in
Map.delete (fst x) (Map.insert (fst e) ((Left z, Left z'),Branch Dist1 his) tc)
dIstStar2 :: Cont -> Typ -> Maybe (M ((Cont, Term -> Term),(TypedVar,TypedVar)))
dIstStar2 gamma tau = case findfirst typeCheckEither (varsStar gamma) of
Nothing -> Nothing
Just (e, TEither tau1 tau2) ->
Just (do {i <- newInt;
j <- newInt;
let x = TermVar i
y = TermVar j in
return ((updateVarStar (removeVarStar gamma e) y tau2,
\m -> subst m (ECase (Var e) x (Bottom tau1) y (Var y)) y),
((y,tau2),(e,TEither tau1 tau2)))
})
dIstStar2_tc_update :: TermCont -> TypedVar -> TypedVar -> TermCont
dIstStar2_tc_update tc y e = let ((z,z'),his) = (trace "Map.!-check: dIstStar2 y" (tc Map.! (fst y)))
in
Map.delete (fst y) (Map.insert (fst e) ((Right z, Right z'),Branch Dist2 his) tc)
-- ** last phase for plus term search
vArStripe :: Cont -> Typ -> Maybe (Term, TypedVar)
vArStripe gamma tau = case findfirstSpecialType (vars gamma) tau of
Nothing -> Nothing
Just x -> Just (Var (fst x), x)
iNtStripe :: Typ -> Maybe Term
iNtStripe tau = if tau == Int then Just Zero else Nothing
bRaceStripe :: Typ -> Maybe Term
bRaceStripe tau = if tau == TBrace then Just Brace else Nothing
bOolStripe :: Typ -> Maybe Term
bOolStripe tau = if tau == TBool then Just Fls else Nothing
lIstStripe :: Typ -> Maybe Term
lIstStripe tau = if typeCheckList tau then let List tau' = tau in Just (Cons (Bottom tau') (Nil tau')) else Nothing
mAybeStripe :: Typ -> Maybe Term
mAybeStripe tau = if typeCheckMaybe tau then let TMaybe tau' = tau in Just (MJust (Bottom tau')) else Nothing
pAirStripe :: Typ -> Maybe Term
pAirStripe tau = if typeCheckPair tau then let TPair tau1 tau2 = tau in Just (Pair (Bottom tau1) (Bottom tau2)) else Nothing
eItherStripe :: Typ -> Maybe Term
eItherStripe tau = if typeCheckEither tau then let TEither tau1 tau2 = tau in Just (Left (Bottom tau1)) else Nothing
-- | creates the initial term variable environment.
stripePhase_tc_update :: Cont -> M TermCont
stripePhase_tc_update gamma = initialiseTermCont ((vars gamma) ++ (varsStar gamma))
-- * The algorithm
--Note: pointed checks are omitted whenever possible, because pointedness is clear out of the rules order, especially because (Drop_3) is used very early
-- ** first phase
alg :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg gamma tau termCont = do track (makeTrackString "Start Conf" gamma tau)
(t,tc,trc) <- alg1 gamma tau termCont
-- return (simplifyTerm t, simplifyTermCont tc, simplifyTrackCont trc) --returns simplified terms
return (t, tc, trc) --returns the terms without simplification
alg1 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1 = traceIOStart traceIOFile alg1_Bottom
alg1_Bottom :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Bottom gamma tau termCont = case bOttom gamma tau of
Nothing -> alg1_RAllStar gamma tau termCont
Just t -> do track ((makeTrackString "Bottom" gamma tau) ++ " !!END OF BRANCH!!")
tc <- bOttom_tc_update gamma
return (t,tc,(tau,[]))
alg1_RAllStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_RAllStar gamma tau termCont = case rAllStar gamma tau of
Nothing -> alg1_RAll gamma tau termCont
Just (gamma', tau', f) -> do track (makeTrackString "RAllStar" gamma' tau')
(t,c,trc) <- (alg1 gamma' tau' termCont)
traceIO "RAll*" tau gamma tau' gamma' (return (f t, c, trc))
alg1_RAll :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_RAll gamma tau termCont = case rAll gamma tau of
Nothing -> alg1_Drop3 gamma tau termCont
Just (gamma', tau', f) -> do {track (makeTrackString "RAll" gamma' tau');
(t,c, trc) <- (alg1 gamma' tau' termCont);
traceIO "RAll" tau gamma tau' gamma' (return (f t,c,trc))
}
alg1_Drop3 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Drop3 gamma tau termCont = case dRop3 gamma of
Nothing -> alg1_Drop1 gamma tau termCont
Just (gamma',v) -> do{track (makeTrackString "Drop_3" gamma' tau);
(t,c,trc) <- (traceIO "Drop_3" tau gamma tau gamma' (alg1 gamma' tau termCont));
tc <- dRop3_tc_update c v;
return (t,tc,trc)
}
alg1_Drop1 gamma tau termCont = case dRop1 gamma of
Nothing -> alg1_Drop2 gamma tau termCont
Just (gamma',v) -> do{track (makeTrackString "Drop_1" gamma' tau);
(t,c,trc) <- (traceIO "Drop_1" tau gamma tau gamma' (alg1 gamma' tau termCont));
return (t,dRop1_tc_update c v,trc)
}
alg1_Drop2 gamma tau termCont = case dRop2 gamma of
Nothing -> alg1_Drop4 gamma tau termCont
Just (gamma',v) -> do{track (makeTrackString "Drop_2" gamma' tau);
(t,c,trc) <- (traceIO "Drop_2" tau gamma tau gamma' (alg1 gamma' tau termCont));
return (t,dRop2_tc_update c v,trc)
}
alg1_Drop4 gamma tau termCont = case dRop4 gamma of
Nothing -> alg1_Abs gamma tau termCont
Just (gamma',v) -> do{track (makeTrackString "Drop_4" gamma' tau);
(t,c,trc) <- (traceIO "Drop_4" tau gamma tau gamma' (alg1 gamma' tau termCont));
return (t,dRop4_tc_update c v,trc)
}
alg1_Abs :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Abs gamma tau termCont = case aBs gamma tau of
Nothing -> alg1_WrapTo gamma tau termCont
Just (comp, tau') -> do {(gamma', x, f) <- comp;
track (makeTrackString "Abs" gamma' tau');
(t,c,trc) <- (traceIO "Abs" tau gamma tau' gamma' (alg1 gamma' tau' termCont));
trc' <- aBs_trackCont_update trc tau c x;
return (f t,aBs_tc_update c x,trc')
}
alg1_WrapTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_WrapTo gamma tau termCont = case wRapTo gamma of
Nothing -> alg1_MaybeTo gamma tau termCont
Just comp -> do {((gamma',f),(g,k)) <- comp;
track (makeTrackString "Wrap->" gamma' tau);
(t,c, trc) <- traceIO "Wrap->" tau gamma tau gamma' (alg1 gamma' tau termCont);
i <- newInt;
j <- newInt;
let l = TermVar i
h = TermVar j in
return (f t,wRapTo_tc_update c l h g k, trc)
}
alg1_MaybeTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_MaybeTo gamma tau termCont = case mAybeTo gamma of
Nothing -> alg1_Head gamma tau termCont
Just comp -> do {((gamma',f),(g,k)) <- comp;
track (makeTrackString "Maybe->" gamma' tau);
(t,c, trc) <- traceIO "Maybe->" tau gamma tau gamma' (alg1 gamma' tau termCont);
i <- newInt;
j <- newInt;
let l = TermVar i
h = TermVar j in
return (f t,mAybeTo_tc_update c l h g k, trc)
}
alg1_Head :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Head gamma tau termCont = case hEad gamma tau of
Nothing -> alg1_Just gamma tau termCont
Just comp -> do {((gamma',f),(h,l)) <- comp;
track (makeTrackString "Head" gamma' tau);
(t,c,trc) <- traceIO "Head" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, hEad_tc_update c h l, trc)
}
alg1_Just :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Just gamma tau termCont = case jUst gamma tau of
Nothing -> alg1_PairTo gamma tau termCont
Just comp -> do {((gamma',f),(h,l)) <- comp;
track (makeTrackString "Just" gamma' tau);
(t,c,trc) <- traceIO "Just" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, jUst_tc_update c h l, trc)
}
alg1_PairTo gamma tau termCont = case pAirTo gamma of
Nothing -> alg1_Proj gamma tau termCont
Just comp -> do {((gamma',f),(g,h)) <- comp;
track(makeTrackString "Pair->" gamma' tau);
(t,c,trc) <- traceIO "Pair->" tau gamma tau gamma' (alg1 gamma' tau termCont);
termCont' <- pAirTo_tc_update c g h;
return (f t, termCont',trc)
}
alg1_Proj gamma tau termCont = case pRoj gamma of
Nothing -> alg1_EitherTo gamma tau termCont
Just comp -> do {((gamma',f),(varIn,p)) <- comp;
track(makeTrackString "Proj" gamma' tau);
(t,c,trc) <- traceIO "Proj" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, pRoj_tc_update c varIn p,trc)
}
alg1_EitherTo gamma tau termCont = case eItherTo gamma of
Nothing -> alg1_Dist1 gamma tau termCont
Just comp -> do {((gamma',f),(varIn,g)) <- comp;
track (makeTrackString "LE->" gamma' tau);
(t,c,trc) <- traceIO "LE->" tau gamma tau gamma' (alg1 gamma' tau termCont);
termCont' <- eItherTo_tc_update c varIn g;
return (f t, termCont',trc)
}
alg1_Dist1 gamma tau termCont = case dIst1 gamma tau of
Nothing -> alg1_BottomToStripe gamma tau termCont
Just comp -> do {((gamma',f),(x,e)) <- comp;
let subderivation =
do track (makeTrackString "Dist1" gamma' tau)
(t,c,trc) <- traceIO "Dist1" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, dIst1_tc_update c x e,trc)
in
choice subderivation (alg1_Dist2 gamma tau termCont);
}
alg1_Dist2 gamma tau termCont = case dIst2 gamma tau of
Nothing -> alg1_BottomToStripe gamma tau termCont --should never be reached
Just comp -> do {((gamma',f),(y,e)) <- comp;
track (makeTrackString "Dist2" gamma' tau);
(t,c,trc) <- traceIO "Dist2" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, dIst2_tc_update c y e,trc)
}
alg1_BottomToStripe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_BottomToStripe gamma tau termCont = foldr choice (alg1_ArrowToStar gamma tau termCont) (map trysubderivations (bOttomToStripe gamma))
where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;
track (makeTrackString "Bottom->'" gamma' tau);
(t,c,trc) <- traceIO "Bottom->'" tau gamma tau gamma' (alg2 gamma' tau termCont);
tc <- bOttomToStripe_tc_update c gamma x g;
return (f t, tc, trc)
}
alg1_ArrowToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_ArrowToStar gamma tau termCont =
foldr choice (alg1_Wrap gamma tau termCont) (map trysubderivations (aRrowToStar gamma))
where trysubderivations = \l -> do {(((gamma1, tau1), gamma2, f),([w,y],g)) <- l;
track (makeTrackString "Arrow->* (fst)" gamma1 tau1);
track (makeTrackString "Arrow->* (snd)" gamma2 tau);
(t1,c1,trc1) <- traceIO "Arrow->* (fst)" tau gamma tau1 gamma1 (alg1 gamma1 tau1 termCont);
(t2,c2,trc2) <- traceIO "Arrow->* (snd)" tau gamma tau gamma2 (alg2 gamma2 tau termCont);
let cont = mergeTermCont c1 c2 in
(case cont of
Nothing -> abort
Just c -> do {tc <- aRrowToStar_tc_update trc1 c gamma t1 w y g;
return (f t1 t2,tc,trc2)
}
)
}
alg1_Wrap :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Wrap gamma tau termCont = case wRap tau of
Nothing -> alg1_Maybe gamma tau termCont
Just (tau', f) -> do track (makeTrackString "Wrap" gamma tau')
(t,c,trc) <- traceIO "Wrap" tau gamma tau' gamma (alg1 gamma tau' termCont)
trc' <- wRap_trackCont_update trc tau
return (f t,c,trc')
alg1_Maybe :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_Maybe gamma tau termCont = case mAybe tau of
Nothing -> alg1_Pair1 gamma tau termCont
Just (tau', f) -> do track (makeTrackString "Maybe" gamma tau')
(t,c,trc) <- traceIO "Maybe" tau gamma tau' gamma (alg1 gamma tau' termCont)
trc' <- mAybe_trackCont_update trc tau
return (f t,c,trc')
alg1_Pair1 gamma tau termCont = case pAir1 tau of
Nothing -> alg1_Left gamma tau termCont
Just (tau', f) -> choice subderivation (alg1_Pair2 gamma tau termCont)
where subderivation = do {track (makeTrackString "Pair1" gamma tau');
(t,c,trc) <- traceIO "Pair1" tau gamma tau' gamma (alg1 gamma tau' termCont);
trc' <-pAir1_trackCont_update trc tau;
return (f t, c, trc')
}
alg1_Pair2 gamma tau termCont = case pAir2 tau of
Nothing -> alg1_Left gamma tau termCont
Just (tau', f) -> do {track (makeTrackString "Pair2" gamma tau');
(t,c,trc) <- traceIO "Pair2" tau gamma tau' gamma (alg1 gamma tau' termCont);
trc' <- pAir2_trackCont_update trc tau;
return (f t,c,trc')
}
alg1_Left gamma tau termCont = case lEft tau of
Nothing -> alg1_BottomTo gamma tau termCont
Just (tau', f) -> choice subderivation (alg1_Right gamma tau termCont)
where subderivation = do {track (makeTrackString "Left" gamma tau');
(t,c,trc) <- traceIO "Left" tau gamma tau' gamma (alg1 gamma tau' termCont);
trc' <- lEft_trackCont_update trc tau;
return (f t,c, trc')
}
alg1_Right gamma tau termCont = case rIght tau of
Nothing -> alg1_BottomTo gamma tau termCont
Just (tau', f) -> do {track (makeTrackString "Right" gamma tau');
(t,c,trc) <- traceIO "Right" tau gamma tau' gamma (alg1 gamma tau' termCont);
trc' <- rIght_trackCont_update trc tau;
return (f t,c,trc')
}
alg1_BottomTo :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg1_BottomTo gamma tau termCont =
foldr choice (do {track "Bottom->: !!FAIL!!"; abort}) (map trysubderivations (bOttomTo gamma))
where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;
track (makeTrackString "Bottom->" gamma' tau);
(t,c,trc) <- traceIO "Bottom->" tau gamma tau gamma' (alg1 gamma' tau termCont);
i <- newInt;
let z = TermVar i in
return (f t,bOttomTo_tc_update c z x g,trc)
}
-- ** second phase
alg2 :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2 = alg2_VarStar
alg2_VarStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_VarStar gamma tau termCont = case vArStar gamma tau of
Nothing -> alg2_BottomToStar gamma tau termCont
Just (t,v) -> do track ((makeTrackString "Var*" gamma tau) ++ " !!END OF BRANCH!!")
tc <- vArStar_tc_update gamma
return (t, tc, (tau,[]))
alg2_BottomToStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_BottomToStar gamma tau termCont = case bOttomToStar gamma of
Nothing -> alg2_AppStripStar gamma tau termCont
Just (comp)
-> do {((gamma', f),(varIn,varOut)) <- comp;
track (makeTrackString "Bottom->*" gamma' tau);
(t,c,trc) <- traceIO "Bottom->*" tau gamma tau gamma' (alg2 gamma' tau termCont);
i <- newInt;
let x = TermVar i in
return (f t, bOttomToStar_tc_update c x varIn varOut, trc)
}
alg2_AppStripStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_AppStripStar gamma tau termCont = case aPpStripStar gamma of
Nothing -> alg2_IntStar gamma tau termCont
Just comp -> do {((gamma', f),([x,y],g)) <- comp;
track (makeTrackString "App'*" gamma' tau);
(t,c,trc) <- traceIO "App'*" tau gamma tau gamma' (alg2 gamma' tau termCont);
i <- newInt;
let u = TermVar i in
do{tc <- aPpStripStar_tc_update c gamma u x y g;
return (f t, tc,trc)
}
}
alg2_IntStar gamma tau termCont =
case iNtStar gamma of
Nothing -> alg2_BraceStar gamma tau termCont
Just (gamma',f,v) -> do {let subderivation =
do {track (makeTrackString "Int*" gamma' tau);
(t,c,trc) <- traceIO "Int*" tau gamma tau gamma' (alg3 gamma' tau termCont);
return (f t, iNtStar_tc_update c (fst v), trc)
}
in
choice subderivation (alg2_HeadStar gamma tau termCont)
}
alg2_BraceStar gamma tau termCont =
case bRaceStar gamma of
Nothing -> alg2_BoolStar gamma tau termCont
Just (gamma',f,v) -> do {let subderivation =
do {track (makeTrackString "Brace*" gamma' tau);
(t,c,trc) <- traceIO "Brace*" tau gamma tau gamma' (alg3 gamma' tau termCont);
return (f t, bRaceStar_tc_update c (fst v), trc)
}
in
choice subderivation (alg2_HeadStar gamma tau termCont)
}
alg2_BoolStar gamma tau termCont =
case bOolStar gamma of
Nothing -> alg2_ListStar gamma tau termCont
Just (gamma',f,v) -> do {let subderivation =
do {track (makeTrackString "Bool*" gamma' tau);
(t,c,trc) <- traceIO "Bool*" tau gamma tau gamma' (alg3 gamma' tau termCont);
return (f t, bOolStar_tc_update c (fst v), trc)
}
in
choice subderivation (alg2_HeadStar gamma tau termCont)
}
alg2_ListStar gamma tau termCont = case lIstStar gamma of
Nothing -> alg2_MaybeStar gamma tau termCont
Just comp -> do {(gamma',f,v) <- comp;
let subderivation =
do {track (makeTrackString "List*" gamma' tau);
(t,c,trc) <- traceIO "List*" tau gamma tau gamma' (alg3 gamma' tau termCont);
cont <- lIstStar_tc_update c v;
return (f t, cont, trc)
}
in
choice subderivation (alg2_HeadStar gamma tau termCont)
}
alg2_MaybeStar gamma tau termCont = case mAybeStar gamma of
Nothing -> alg2_PairStar gamma tau termCont
Just comp -> do {(gamma',f,v) <- comp;
let subderivation =
do {track (makeTrackString "Maybe*" gamma' tau);
(t,c,trc) <- traceIO "Maybe*" tau gamma tau gamma' (alg3 gamma' tau termCont);
cont <- mAybeStar_tc_update c v;
return (f t, cont, trc)
}
in
choice subderivation (alg2_JustStar gamma tau termCont)
}
alg2_PairStar gamma tau termCont = case pAirStar gamma of
Nothing -> alg2_EitherStar gamma tau termCont
Just comp -> do {(gamma',f,v) <- comp;
let subderivation =
do {track (makeTrackString "Pair*" gamma' tau);
(t,c,trc) <- traceIO "Pair*" tau gamma tau gamma' (alg3 gamma' tau termCont);
cont <- pAirStar_tc_update c v;
return (f t, cont, trc)
}
in
choice subderivation (alg2_ProjStar gamma tau termCont)
}
alg2_EitherStar gamma tau termCont = case eItherStar gamma tau of
Nothing -> do {track "abort: Either*";
abort
}
Just comp -> do {(gamma',f,v) <- comp;
let subderivation =
do {track (makeTrackString "Either*" gamma' tau);
(t,c,trc) <- traceIO "Either*" tau gamma tau gamma' (alg3 gamma' tau termCont);
cont <- eItherStar_tc_update c v;
return (f t, cont, trc)
}
in
choice subderivation (alg2_DistStar1 gamma tau termCont)
}
alg2_HeadStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_HeadStar gamma tau termCont = case hEadStar gamma tau of
Nothing -> alg2_JustStar gamma tau termCont
Just comp -> do {((gamma', f),(h,l)) <- comp;
track (makeTrackString "Head*" gamma' tau);
(t,c,trc) <- traceIO "Head*" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, hEadStar_tc_update c h l, trc)
}
alg2_JustStar :: Cont -> Typ -> TermCont -> M (Term,TermCont,TrackCont)
alg2_JustStar gamma tau termCont = case jUstStar gamma tau of
Nothing -> alg2_ProjStar gamma tau termCont
Just comp -> do {((gamma', f),(h,l)) <- comp;
track (makeTrackString "Just*" gamma' tau);
(t,c,trc) <- traceIO "Just*" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, jUstStar_tc_update c h l, trc)
}
alg2_ProjStar gamma tau termCont = case pRojStar gamma of
Nothing -> alg2_DistStar1 gamma tau termCont
Just comp -> do {((gamma', f),(h,p)) <- comp;
track (makeTrackString "Proj*" gamma' tau);
(t,c,trc) <- traceIO "Proj*" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, pRojStar_tc_update c h p, trc)
}
alg2_DistStar1 gamma tau termCont = case dIstStar1 gamma tau of
Nothing -> do {track "abort: Dist*1"; --should never be reached
abort
}
Just comp -> do {((gamma',f),(x,e)) <- comp;
let subderivation =
do {track (makeTrackString "Dist*1" gamma' tau);
(t,c,trc) <- traceIO "Dist*1" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, dIstStar1_tc_update c x e, trc)
}
in
choice subderivation (alg2_DistStar2 gamma tau termCont)
}
alg2_DistStar2 gamma tau termCont = case dIstStar2 gamma tau of
Nothing -> do {track "abort: Dist*2"; --should never be reached
abort
}
Just comp -> do {((gamma',f),(y,e)) <- comp;
track (makeTrackString "Dist*2" gamma' tau);
(t,c,trc) <- traceIO "Dist*2" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, dIstStar2_tc_update c y e, trc)
}
-- ** third phase
alg3 = alg3_VarStripe
alg3_VarStripe gamma tau termCont =
case vArStripe gamma tau of
Nothing -> alg3_IntStripe gamma tau termCont
Just (t,var) -> do {track ((makeTrackString "Var'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_IntStripe gamma tau termCont =
case iNtStripe tau of
Nothing -> alg3_BraceStripe gamma tau termCont
Just t -> do {track ((makeTrackString "Int'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_BraceStripe gamma tau termCont =
case bRaceStripe tau of
Nothing -> alg3_BoolStripe gamma tau termCont
Just t -> do {track ((makeTrackString "Brace'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_BoolStripe gamma tau termCont =
case bOolStripe tau of
Nothing -> alg3_ListStripe gamma tau termCont
Just t -> do {track ((makeTrackString "Bool'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_ListStripe gamma tau termCont =
case lIstStripe tau of
Nothing -> alg3_MaybeStripe gamma tau termCont
Just t -> do {track ((makeTrackString "List'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_MaybeStripe gamma tau termCont =
case mAybeStripe tau of
Nothing -> alg3_PairStripe gamma tau termCont
Just t -> do {track ((makeTrackString "Maybe'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_PairStripe gamma tau termCont =
case pAirStripe tau of
Nothing -> alg3_EitherStripe gamma tau termCont
Just t -> do {track ((makeTrackString "Pair'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}
alg3_EitherStripe gamma tau termCont =
case lIstStripe tau of
Nothing -> do {track "Either': FAIL";
abort
}
Just t -> do {track ((makeTrackString "Either'" gamma tau) ++ " !!END OF BRANCH!!");
tc <- stripePhase_tc_update gamma;
return (t, tc, (tau,[]))
}