-module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,showTerm,showUsedTermCont,getCompleteRaw,getWithDebug,getIt) where
+module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,showTerm,showUsedTermCont,getCompleteRaw,getWithDebug,getIt,showTyp,printTyp) where
import Prelude hiding (Either(..))
import qualified Prelude as E (Either(..))
import Control.Monad
import M
import ParseType
---import Debug.Trace
-trace string a = a
--- newInt :: M Int
--- runM :: M a -> a
+
+-- * Debugging options
+--------------------------DEBUG-TOOLS---------------------------------------------------------
+import System.IO.Unsafe
+-- |set debugging functions from the below list
+trace :: String -> a -> a
+trace = trace_ignore
+--trace = trace_2shell
+
+---- OutputFile options ----
+--traceIOStart = traceIOStart_makeFile
+-- |set file where debug output of traceIO is send to
+traceIOStart = traceIOStart_ignore
+traceIOFile = "./traceIO.log.hs"
+
+---- traceIO settings ----
+-- | trace informations on every rule, gives context and typ before and after rule application
+-- exception: RFix and AX*
+traceIO :: String -> Typ -> Cont -> Typ -> Cont -> a -> a
+traceIO = traceIO_ignore
+--traceIO = traceIO_ordDiff
+--traceIO = traceIO_ord2shell
+--traceIO = traceIO_checkOrderInc
+--traceIO = traceIO_cont2shell
+
+---- show settings ---
+showContTrace = showCont
+
+
+---- trace functions ----
+
+---- output file variants ----
+traceIOStart_ignore file a = a
+traceIOStart_makeFile file a = if unsafePerformIO (writeFile traceIOFile "traceIO-File\n\n") == () then a else a
+
+---- trace and traceIO variants ----
+trace_ignore str a = a
+trace_toShell str a = if unsafePerformIO (putStr str) == () then a else a
+
+traceIO_ignore rule tauIn gammaIn tauOut gammaOut a = a
+
+traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff =
+ unsafePerformIO (appendFile traceIOFile (rule ++ ":\n\tIN Type: " ++ (showTyp tauIn) ++ "\n\tIN Cont: " ++ (showContTrace gammaIn) ++ "\n\tOUT Type: " ++ (showTyp tauOut) ++ "\n\tOUT Cont: " ++ (showContTrace gammaOut) ++"\n\tOrder Difference: " ++ (show ordDiff) ++ "\n"))
+
+--traceIO variants
+--outputs a file with input and output types, contexts and the orderdifference (out - in) for every rule applied
+traceIO_ordDiff rule tauIn gammaIn tauOut gammaOut a =
+ let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut)
+ ordDiff = zipWith (-) ordOut ordIn
+ good = firstNegative ordDiff
+ in
+ if (if traceIOOutPut rule tauIn gammaIn tauOut gammaOut ordDiff == () then good else good)
+ then a
+ else error ("Order increased by Rule " ++ rule ++ "\n\tInput Type: " ++ (showTyp tauIn) ++ "\n\tInput Cont: " ++ (show gammaIn) ++ "\n\tOutPut Type: " ++ (showTyp tauOut) ++ "\n\tOutput Cont: " ++ (show gammaOut) ++ "\n" ++ "OrderDifference: " ++ (show ordDiff))
+
+--outputs pairs of input order ander output order to the shell
+traceIO_ord2shell rule tauIn gammaIn tauOut gammaOut a =
+ let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut) in
+ if unsafePerformIO (putStr ((show ordIn) ++ "\n" ++ (show ordOut) ++ "\n\n")) == () then a else a
+
+--outputs context before and after rule application to the shell
+traceIO_cont2shell rule tauIn gammaIn tauOut gammaOut a =
+ if unsafePerformIO (putStr (rule ++ ":\n" ++ (showContTrace gammaIn) ++ "\n" ++ (showContTrace gammaOut) ++ "\n\n")) == () then a else a
+
+--stay calm until order increases during a rule and then throw an error
+traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut a =
+ let (ordIn,ordOut) = makeSameLength (count gammaIn tauIn) (count gammaOut tauOut)
+ ordDiff = zipWith (-) ordOut ordIn in
+ if firstNegative ordDiff
+ then a
+ else error ("Order increased by Rule " ++ rule ++ "\n\tInput Type: " ++ (showTyp tauIn) ++ "\n\tInput Cont: " ++ (show gammaIn) ++ "\n\tOutPut Type: " ++ (showTyp tauOut) ++ "\n\tOutput Cont: " ++ (show gammaOut) ++ "\n" ++ "OrderDifference: " ++ (show ordDiff))
+
+--helpfunctions
+zeros = 0:zeros
+
+updateAt l idx elem = (take idx l) ++ (elem:(drop (idx+1) l))
+
+getAt l idx = head (drop idx l)
+
+makeSameLength l1 l2 = let len1 = length l1
+ len2 = length l2 in
+ if len1 < len2
+ then (prependZeros len2 l1,l2)
+ else (l1,prependZeros len1 l2)
+ where prependZeros len l = if length l < len
+ then prependZeros len (0:l)
+ else l
+
+count gamma tau = let (l1,l2) = makeSameLength (countCont gamma) ((countTyp tau) ++ [0]) in
+ zipWith (+) l1 l2
+
+countCont :: Cont -> [Int]
+countCont gamma =
+ let varlist = ((vars gamma) ++ (varsStar gamma)) in
+ (countCont' varlist) ++ [(length varlist)]
+
+countCont' vl =
+ case vl of
+ [] -> [0,0,0,0,0]
+ x:xs -> let (l1,l2) = makeSameLength (countCont' xs) (countTyp (snd x)) in
+ zipWith (+) l1 l2
+
+countTyp :: Typ -> [Int]
+countTyp tau = let (d,el,ol) = countTyp' tau 0 in
+ (reverse (take (d+1) el)) ++ ol
+
+-- tau depth eitherlist (maxdepth,(eitherlist,orderlist))
+countTyp' :: Typ -> Int -> (Int,[Int],[Int])
+countTyp' tau depth =
+ case tau of
+ TVar _ -> (depth,zeros,[0,0,0,0])
+ Arrow tau1 tau2 -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
+ (d2,el2,ol2) = countTyp' tau2 (d1+1) in
+ (max d1 d2, zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,0,0,1] ol1) ol2)
+ All _ tau1 -> let (d,el,ol) = countTyp' tau1 (depth+1) in
+ (d,el,zipWith (+) [1,0,0,0] ol)
+ AllStar _ tau1 -> let (d,el,ol) = countTyp' tau1 (depth+1) in
+ (d,el,zipWith (+) [1,0,0,0] ol)
+ List tau1 -> let (d,el,ol) = countTyp' tau1 (depth+1) in
+ (d,el,zipWith (+) [0,0,1,0] ol)
+ Int -> (depth,zeros,[0,0,0,0])
+ TPair tau1 tau2 -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
+ (d2,el2,ol2) = countTyp' tau2 (d1+1) in
+ (max d1 d2,zipWith (+) el1 el2, zipWith (+) (zipWith (+) [0,1,0,0] ol1) ol2)
+ TEither tau1 tau2 -> let (d1,el1,ol1) = countTyp' tau1 (depth+1)
+ (d2,el2,ol2) = countTyp' tau2 (depth+1) in
+ (max d1 d2,zipWith (+) (updateAt el1 depth ((getAt el1 depth)+1)) el2, zipWith (+) ol1 ol2)
+
+firstNegative l = case l of
+ [] -> False
+ x:xs -> if x == 0 then firstNegative xs
+ else (if x < 0 then True else False)
+
+
+--------------------------END: DEBUG-TOOLS----------------------------------------------------
type TypedVar = (TermVar,Typ)
type TermCont = Map.Map TermVar (TermPlus,TermPlus)
Pair t1 t2 -> Pair (term2PlusTerm t1) (term2PlusTerm t2)
PCase t1 v1 v2 t2 -> PCase (term2PlusTerm t1) v1 v2 (term2PlusTerm t2)
ECase t1 v1 t2 v2 t3 -> ECase (term2PlusTerm t1) v1 (term2PlusTerm t2) v2 (term2PlusTerm t3)
- Right t1 -> term2PlusTerm t1
- Left t1 -> term2PlusTerm t1
+ Right t1 -> Right (term2PlusTerm t1)
+ Left t1 -> Left (term2PlusTerm t1)
updateTVarStar (Cont tVars tVarsStar vars varsStar) tv = Cont tVars (tv:tVarsStar) vars varsStar
[] -> f
x:xs -> apply (App f x) xs
-subst :: Term -> Term -> TermVar -> Term
+insertArgument :: AbsTerm a -> AbsTerm a -> AbsTerm a
+insertArgument f x = case f of
+ Abs v _ t -> subst t x v
+ Bottom (Arrow tau1 tau2) -> Bottom tau2
+ _ -> error ("unexpected termstructure" ++ (showAbsTerm f))
+
+subst :: AbsTerm a -> AbsTerm a -> TermVar -> AbsTerm a
subst m new old = case m of
Var var -> if(var == old) then new else m
Abs v tau m' -> Abs v tau (subst m' new old)
-- GoalTerm _ _ -> Subst m new old
-- Subst _ _ _ -> Subst m new old
-- Alg2 _ _ -> Subst m new old
+ Case1 m0 m1 m2 m3 -> Case1 (subst m0 new old) (subst m1 new old) (subst m2 new old) (subst m3 new old)
_ -> m
makePlusPair :: Typ -> Maybe (AbsTerm PlusElem, AbsTerm PlusElem)
makeFuncPair' :: TermCont -> Cont -> (TermPlus,TermPlus) -> Typ -> Typ -> Typ -> ([TermPlus],[TermPlus]) -> (TermPlus,TermPlus) -> M (TermPlus,TermPlus)
makeFuncPair' tc gamma resPair resTyp tauAll tau args terms =
+ trace ("makeFuncPair' called with\n\ttype : " ++ showTyp tau ++ "\n\tterm1: " ++ (showTermPlus False (fst terms)) ++ "\n\t\term2: " ++ (showTermPlus True (snd terms))) (
let (z,z') = resPair in
case tau of
TVar beta -> case makePlusPair tau of
}
Left t1 -> return (Abs w tauAll (ECase (apply (Var w) (fst args)) x (fst resPair) x (Bottom resTyp)),
Abs w tauAll (ECase (apply (Var w) (fst args)) x (snd resPair) x (Bottom resTyp)))
+ App t21 t22 -> let App t11 t12 = fst terms in
+ makeFuncPair' tc gamma resPair resTyp tauAll tau args (insertArgument t11 t12, insertArgument t21 t22)
+ ECase t21 _ _ _ _ -> let ECase t11 _ _ _ _ = fst terms in
+ makeFuncPair' tc gamma resPair resTyp tauAll tau args (t21, t11)
+ t -> error ("Term has unexpected termstructure " ++ (showTermPlus False t) ++ "as type" ++ (showTyp tau))
}
- Arrow tau' tau'' -> let Abs x _ t1 = fst terms
- t2 = case snd terms of
- Abs _ _ t -> t
- Bottom _ -> Bottom tau''
- Just (u,u') = if Map.member x tc then Just (fst (trace "Map.!-check: lArrowArrow g-construct fst y (list case Arrow)" (tc Map.! x)),snd (trace "Map.!-check: lArrowArrow g-construct snd y (list case Arrow)" (tc Map.! x)))
- else makePlusPair tau'
- in
- makeFuncPair' tc gamma resPair resTyp tauAll tau'' (u:(fst args),u':(snd args)) (t1,t2)
-
+--T commented out for testing reasons
+-- Arrow tau' tau'' -> let Abs x _ t1 = fst terms
+-- t2 = case snd terms of
+-- Abs _ _ t -> t
+-- Bottom _ -> Bottom tau''
+-- Just (u,u') = if Map.member x tc then Just (fst (trace "Map.!-check: lArrowArrow g-construct fst y (list case Arrow)" (tc Map.! x)),snd (trace "Map.!-check: lArrowArrow g-construct snd y (list case Arrow)" (tc Map.! x)))
+-- else makePlusPair tau'
+-- in
+-- makeFuncPair' tc gamma resPair resTyp tauAll tau'' (u:(fst args),u':(snd args)) (t1,t2)
+
+--T inserted for testing reasons
+ Arrow tau' tau'' -> case fst terms of
+ Abs x _ t1 -> let t2 = case snd terms of
+ Abs _ _ t -> t
+ Bottom _ -> Bottom tau''
+ Just (u,u') = if Map.member x tc then Just (fst (trace "Map.!-check: lArrowArrow g-construct fst y (list case Arrow)" (tc Map.! x)),snd (trace "Map.!-check: lArrowArrow g-construct snd y (list case Arrow)" (tc Map.! x)))
+ else makePlusPair tau'
+ in
+ makeFuncPair' tc gamma resPair resTyp tauAll tau'' (u:(fst args),u':(snd args)) (t1,t2)
+ Bottom _ -> let t2 = Bottom tau''
+ Just (u,u') = makePlusPair tau'
+ in
+ do{ (_,g') <- makeFuncPair' tc gamma resPair resTyp tauAll tau'' (u:(fst args),u':(snd args)) (t2,t2);
+ i <- newInt;
+ let x = TermVar i in
+ return (Abs x tau' (fst resPair), g')
+ }
+ )
-------Regeln der ersten Phase-------------
Just (u,u') = if Map.member (fst h) tc then Just (fst (trace "Map.!-check: lEArrow fst h" (tc Map.! (fst h))), snd (trace "Map.!-check: lEArrow snd h" (tc Map.! (fst h))))
else makePlusPair $ snd h
in
- return (Map.insert (fst f) (Abs e tau (ECase (Var e) x z y u), Abs e tau (ECase (Var e) x z' y u')) tc)
+ return (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)))) tc)
}
------Regeln mit backtracking -----------------
alg :: Cont -> Typ -> TermCont -> M (Term,TermCont)
alg gamma tau termCont = do track (makeTrackString "Start Conf" gamma tau)
- alg1 gamma tau termCont
+ (t,tc) <- alg1 gamma tau termCont
+ return (simplifyAbsTerm t, simplifyTermCont tc)
alg1 :: Cont -> Typ -> TermCont -> M (Term,TermCont)
-alg1 = alg1_RFix
+alg1 = traceIOStart traceIOFile alg1_RFix
alg1_RFix :: Cont -> Typ -> TermCont -> M (Term,TermCont)
alg1_RFix gamma tau termCont = case rFix gamma tau of
Nothing -> alg1_RAll gamma tau termCont
Just (gamma', tau', f) -> do track (makeTrackString "RAllStar" gamma' tau')
(t,c) <- (alg1 gamma' tau' termCont)
- return (f t, c)
+ traceIO "RAll*" tau gamma tau' gamma' (return (f t, c))
alg1_RAll :: Cont -> Typ -> TermCont -> M (Term,TermCont)
alg1_RAll gamma tau termCont = case rAll gamma tau of
Nothing -> alg1_LFix gamma tau termCont
Just (gamma', tau', f) -> do track (makeTrackString "RAll" gamma' tau')
(t,c) <- (alg1 gamma' tau' termCont)
- return (f t,c)
+ traceIO "RAll" tau gamma tau' gamma' (return (f t,c))
alg1_LFix :: Cont -> Typ -> TermCont -> M (Term,TermCont)
alg1_LFix gamma tau termCont = case lFix gamma of
Nothing -> alg1_LInt gamma tau termCont
Just gamma' -> do track (makeTrackString "LFix" gamma' tau)
- alg1 gamma' tau termCont
+ traceIO "LFix" tau gamma tau gamma' (alg1 gamma' tau termCont)
alg1_LInt gamma tau termCont = case lInt gamma of
Nothing -> alg1_RArrow gamma tau termCont
Just gamma' -> do track (makeTrackString "LInt" gamma' tau)
- alg1 gamma' tau termCont
+ traceIO "LInt" tau gamma tau gamma' (alg1 gamma' tau termCont)
alg1_RArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
alg1_RArrow gamma tau termCont = case rArrow gamma tau of
Nothing -> alg1_RI gamma tau termCont
Just (comp, tau') -> do {(gamma', f) <- comp;
track (makeTrackString "R->" gamma' tau');
- (t,c) <- (alg1 gamma' tau' termCont);
+ (t,c) <- (traceIO "R->" tau gamma tau' gamma' (alg1 gamma' tau' termCont));
return (f t,c)
}
alg1_RI gamma tau termCont = case rI tau of
Nothing -> alg1_LIArrow gamma tau termCont
Just (tau', f) -> do track (makeTrackString "RI" gamma tau')
- (t,c) <- (alg1 gamma tau' termCont)
+ (t,c) <- traceIO "RI" tau gamma tau' gamma (alg1 gamma tau' termCont)
return (f t,c)
alg1_LIArrow :: Cont -> Typ -> TermCont -> M (Term,TermCont)
Nothing -> alg1_LI gamma tau termCont
Just comp -> do {((gamma',f),(g,k)) <- comp;
track (makeTrackString "LI->" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LI->" tau gamma tau gamma' (alg1 gamma' tau termCont);
i <- newInt;
j <- newInt;
let l = TermVar i
Nothing -> alg1_LPArrow gamma tau termCont
Just comp -> do {((gamma',f),(h,l)) <- comp;
track (makeTrackString "LI" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LI" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, lI_tc_update c h l)
}
Nothing -> alg1_LP gamma tau termCont
Just comp -> do {((gamma',f),(g,h)) <- comp;
track(makeTrackString "LP->" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LP->" tau gamma tau gamma' (alg1 gamma' tau termCont);
termCont' <- lPArrow_tc_update c g h;
return (f t, termCont')
}
Nothing -> alg1_LEArrow gamma tau termCont
Just comp -> do {((gamma',f),(varIn,p)) <- comp;
track(makeTrackString "LP" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LP" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, lP_tc_update c varIn p)
}
Nothing -> alg1_LE1 gamma tau termCont
Just comp -> do {((gamma',f),(varIn,g)) <- comp;
track (makeTrackString "LE->" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LE->" tau gamma tau gamma' (alg1 gamma' tau termCont);
termCont' <- lEArrow_tc_update c varIn g;
return (f t, termCont')
}
Just comp -> do {((gamma',f),(x,e)) <- comp;
let subderivation =
do track (makeTrackString "LE1" gamma' tau)
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LE1" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, lE1_tc_update c x e)
in
choice subderivation (alg1_LE2 gamma tau termCont);
Nothing -> alg1_RP1 gamma tau termCont --should never be reached
Just comp -> do {((gamma',f),(y,e)) <- comp;
track (makeTrackString "LE2" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LE2" tau gamma tau gamma' (alg1 gamma' tau termCont);
return (f t, lE2_tc_update c y e)
}
Nothing -> alg1_RE1 gamma tau termCont
Just (tau', f) -> choice subderivation (alg1_RP2 gamma tau termCont)
where subderivation = do {track (makeTrackString "RP1" gamma tau');
- (t,c) <- (alg1 gamma tau' termCont);
+ (t,c) <- traceIO "RP1" tau gamma tau' gamma (alg1 gamma tau' termCont);
return (f t, c)
}
alg1_RP2 gamma tau termCont = case rP2 tau of
Nothing -> alg1_RE1 gamma tau termCont
Just (tau', f) -> do {track (makeTrackString "RP2" gamma tau');
- (t,c) <- (alg1 gamma tau' termCont);
+ (t,c) <- traceIO "RP2" tau gamma tau' gamma (alg1 gamma tau' termCont);
return (f t,c)
}
Nothing -> alg1_LFixArrowStar gamma tau termCont
Just (tau', f) -> choice subderivation (alg1_RE2 gamma tau termCont)
where subderivation = do {track (makeTrackString "RE1" gamma tau');
- (t,c) <- (alg1 gamma tau' termCont);
+ (t,c) <- traceIO "RE1" tau gamma tau' gamma (alg1 gamma tau' termCont);
return (f t,c)
}
alg1_RE2 gamma tau termCont = case rE2 tau of
Nothing -> alg1_LFixArrowStar gamma tau termCont
Just (tau', f) -> do {track (makeTrackString "RE2" gamma tau');
- (t,c) <- (alg1 gamma tau' termCont);
+ (t,c) <- traceIO "RE2" tau gamma tau' gamma (alg1 gamma tau' termCont);
return (f t,c)
}
alg1_LFixArrowStar gamma tau termCont = foldr choice (alg1_LArrowArrow gamma tau termCont) (map trysubderivations (lFixArrowStar gamma))
where trysubderivations = \l -> do {((gamma', f),(y,g)) <- l;
track (makeTrackString "LFix->*" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "LFix->*" tau gamma tau gamma' (alg2 gamma' tau termCont);
i <- newInt;
let x = TermVar i in
do{tc <- lFixArrowStar_tc_update c gamma x y g;
where trysubderivations = \l -> do {(((gamma1, tau1), gamma2, f),([w,y],g)) <- l;
track (makeTrackString "L->-> (fst)" gamma1 tau1);
track (makeTrackString "L->-> (snd)" gamma2 tau);
- (t1,c1) <- (alg1 gamma1 tau1 termCont);
- (t2,c2) <- (alg2 gamma2 tau termCont);
+ (t1,c1) <- traceIO "L->-> (fst)" tau gamma tau1 gamma1 (alg1 gamma1 tau1 termCont);
+ (t2,c2) <- traceIO "L->-> (snd)" tau gamma tau gamma2 (alg2 gamma2 tau termCont);
termCont' <- lArrowArrow_tc_update (Map.union c1 c2) gamma t1 w y g;
return (f t1 t2, termCont')
}
foldr choice (do {track "LFix->: !!FAIL!!"; abort}) (map trysubderivations (lFixArrow gamma))
where trysubderivations = \l -> do {((gamma', f),(x,g)) <- l;
track (makeTrackString "LFix->" gamma' tau);
- (t,c) <- (alg1 gamma' tau termCont);
+ (t,c) <- traceIO "LFix->" tau gamma tau gamma' (alg1 gamma' tau termCont);
i <- newInt;
let z = TermVar i in
return (f t,lFixArrow_tc_update c z x g)
Just (comp)
-> do {((gamma', f),(varIn,varOut)) <- comp;
track (makeTrackString "La->*1" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "La->*1" tau gamma tau gamma' (alg2 gamma' tau termCont);
i <- newInt;
let x = TermVar i in
return (f t, laArrowStar1_tc_update c x varIn varOut)
Nothing -> alg2_LIStar gamma tau termCont
Just comp -> do {((gamma', f),([x,y],g)) <- comp;
track (makeTrackString "La->*2" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "La->*2" tau gamma tau gamma' (alg2 gamma' tau termCont);
i <- newInt;
let u = TermVar i in
do{tc <- laArrowStar2_tc_update c gamma u x y g;
Nothing -> alg2_LPStar gamma tau termCont
Just comp -> do {((gamma', f),(h,l)) <- comp;
track (makeTrackString "LI*" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "LI*" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, lIStar_tc_update c h l)
}
Nothing -> alg2_LEStar1 gamma tau termCont
Just comp -> do {((gamma', f),(h,p)) <- comp;
track (makeTrackString "LP*" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "LP*" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, lPStar_tc_update c h p)
}
Just comp -> do {((gamma',f),(x,e)) <- comp;
let subderivation =
do {track (makeTrackString "LE*1" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "LE*1" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, lEStar1_tc_update c x e)
}
in
}
Just comp -> do {((gamma',f),(y,e)) <- comp;
track (makeTrackString "LE*2" gamma' tau);
- (t,c) <- (alg2 gamma' tau termCont);
+ (t,c) <- traceIO "LE*2" tau gamma tau gamma' (alg2 gamma' tau termCont);
return (f t, lEStar2_tc_update c y e)
}
}
}
+-- *simplifications
+
+-- |removes App in terms
+simplifyAbsTerm :: AbsTerm a -> AbsTerm a
+simplifyAbsTerm t =
+ case t of
+ Abs v tau t1 -> Abs v tau (simplifyAbsTerm t1)
+ App (Abs v tau t1) t2 -> subst (simplifyAbsTerm t1) t2 v
+ App (Var v1) t1 -> App (Var v1) (simplifyAbsTerm t1)
+ TAbs v t1 -> TAbs v (simplifyAbsTerm t1)
+ Cons t1 t2 -> Cons (simplifyAbsTerm t1) (simplifyAbsTerm t2)
+ Case t1 t2 v t3 -> Case (simplifyAbsTerm t1) (simplifyAbsTerm t2) v (simplifyAbsTerm t3)
+ Case1 t1 t2 t3 t4 -> Case1 (simplifyAbsTerm t1) (simplifyAbsTerm t2) (simplifyAbsTerm t3) (simplifyAbsTerm t4)
+ Pair t1 t2 -> Pair (simplifyAbsTerm t1) (simplifyAbsTerm t2)
+ PCase t1 v1 v2 t2 -> PCase (simplifyAbsTerm t1) v1 v2 (simplifyAbsTerm t2)
+ ECase t1 v1 t2 v2 t3 -> ECase (simplifyAbsTerm t1) v1 (simplifyAbsTerm t2) v2 (simplifyAbsTerm t3)
+ Right t1 -> Right (simplifyAbsTerm t1)
+ Left t1 -> Left (simplifyAbsTerm t1)
+ Var v -> Var v
+ Nil tau -> Nil tau
+ Bottom tau -> Bottom tau
+ Zero -> Zero
+ Extra a -> Extra a
+ _ -> error ("unexpected Term structure during simplification: " ++ (showAbsTerm t))
+
+-- |calls simplifyAbsTerm for all Terms in the TermCont
+simplifyTermCont :: TermCont -> TermCont
+simplifyTermCont c =
+ let simplifyPair (t1,t2) = (simplifyAbsTerm t1, simplifyAbsTerm t2) in
+ Map.map simplifyPair c
+
+-- *show and print functions
+
printUsedTermCont :: (Term, TermCont) -> IO()
printUsedTermCont p =
let (t,tc) = p in
case t of
Extra _ -> "ERROR. Extra as Term."
Case1 _ _ _ _ -> "ERROR. Case1 as Term."
- _ -> (showAbsTerm t showTerm)
+ _ -> (showAbsTermAs t showTerm)
showTermPlus :: Bool -> TermPlus -> String
showTermPlus strip t =
then "(p" ++ (show i) ++ "(" ++ show j ++ "))"
else "(p" ++ (show i) ++ "'(" ++ show j ++ "))"
_ -> if strip == False
- then showAbsTerm t (showTermPlus False)
- else showAbsTerm t (showTermPlus True )
+ then showAbsTermAs t (showTermPlus False)
+ else showAbsTermAs t (showTermPlus True )
-showAbsTerm :: (AbsTerm a) -> ((AbsTerm a) -> String) -> String
-showAbsTerm t showTerm = case t of
+showAbsTermAs :: (AbsTerm a) -> ((AbsTerm a) -> String) -> String
+showAbsTermAs t showTerm = case t of
Var (TermVar i) -> 'x':(show i)
Abs v _ t' -> "(\\" ++ (showTerm (Var v)) ++ "." ++ (showTerm t') ++ ")"
App t1 t2 -> "(" ++ (showTerm t1) ++ " " ++ (showTerm t2) ++ ")"
ECase t0 v1 t1 v2 t2 -> "(case " ++ showTerm t0 ++ " of { Left(" ++ showTerm (Var v1) ++ ") => " ++ showTerm t1 ++ "; Right(" ++ showTerm (Var v2) ++ ") => " ++ showTerm t2 ++ "})"
Left t -> "Left(" ++ showTerm t ++ ")"
Right t -> "Right(" ++ showTerm t ++ ")"
+ Zero -> "0"
+
+showAbsTerm :: (AbsTerm a) -> String
+showAbsTerm t = case t of
+ Var (TermVar i) -> 'x':(show i)
+ Abs v _ t' -> "(\\" ++ (showAbsTerm (Var v)) ++ "." ++ (showAbsTerm t') ++ ")"
+ App t1 t2 -> "(" ++ (showAbsTerm t1) ++ " " ++ (showAbsTerm t2) ++ ")"
+ Nil _ -> "[]"
+ Cons t1 t2 -> "(" ++ (showAbsTerm t1) ++ ":" ++ (showAbsTerm t2) ++ ")"
+ Case t0 t1 v2 t2 -> "(case " ++ (showAbsTerm t0) ++ " of {[] => " ++ (showAbsTerm t1) ++ "; " ++ showAbsTerm (Var v2) ++ ":_ => " ++ (showAbsTerm t2) ++"})"
+ Bottom _ -> "_|_"
+ TAbs (TypVar i) t -> (showAbsTerm t)
+ Extra a -> "No show-function implemented."
+ Case1 t1 t2 t3 t4 -> "(case " ++ (showAbsTerm t1) ++ " of {" ++ (showAbsTerm t2) ++ " => " ++ (showAbsTerm t3) ++ "; _ => " ++ (showAbsTerm t4) ++ "})"
+ Pair t1 t2 -> "(" ++ showAbsTerm t1 ++ "," ++ showAbsTerm t2 ++ ")"
+ PCase t0 v1 v2 t1 -> "(case " ++ showAbsTerm t0 ++ " of {(" ++ showAbsTerm (Var v1) ++ "," ++ showAbsTerm (Var v2) ++ ") => " ++ showAbsTerm t1 ++ "})"
+ ECase t0 v1 t1 v2 t2 -> "(case " ++ showAbsTerm t0 ++ " of { Left(" ++ showAbsTerm (Var v1) ++ ") => " ++ showAbsTerm t1 ++ "; Right(" ++ showAbsTerm (Var v2) ++ ") => " ++ showAbsTerm t2 ++ "})"
+ Left t -> "Left(" ++ showAbsTerm t ++ ")"
+ Right t -> "Right(" ++ showAbsTerm t ++ ")"
Zero -> "0"
showTyp :: Typ -> String
-- |This module uses "Test.Quickcheck" to test the PolyFix package by generating randomly 100 different types
-- running ExFind with that type and then simplifying the generated free theorem
--- to a antilogy of the kind \"_|_ = ()\" or \"_|_ = 0\".
+-- to a antilogy of the kind \"() = _|_\" or \"0 = _|_\".
module TestGen where
import Test.QuickCheck
--import ParseType (parseType')
import SimpleFT (freeTheorem)
-import Expr (specialize)
-import ExFindExtended (getCompleteRaw, showTerm, showUsedTermCont)
+import Expr (specialize,BoolExpr(..),Expr(..))
+import ExFindExtended (getCompleteRaw, showTerm, showUsedTermCont,Typ(..),TypVar(..),showTyp,printTyp,testTerm)
+
+import Foreign
--import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
--import Language.Haskell.FreeTheorems
-- ( runChecks
-- )
import Term2Expr (term2Expr, termCond2Exprs, insertTermsInCondition)
+import List (sort,nub)
+import Control.Monad (liftM, liftM2)
+import Debug.Trace
import TestItExt
testrun typ = case getCompleteRaw typ of
Left _ -> Left "Error in type."
Right p -> Right (insertTermsInCondition p (specialize (freeTheorem typ)))
+
+-- *Generation of example types
+
+newtype UnpointedVar = UnpointedVar Int
+newtype PointedVar = PointedVar Int
+
+-- |restricting the range of unpointed type variables
+--instance Arbitrary UnpointedVar where
+-- arbitrary = oneof [1,2,3]
+
+-- |restricting the range of pointed type variables
+--instance Arbitrary PointedVar where
+-- arbitrary = oneof [4,5,6]
+
+-- |TypVar generator
+instance Arbitrary TypVar where
+-- arbitrary = oneof [UnpointedVar arbitrary, PointedVar arbitrary]
+ arbitrary = oneof [return (TypVar 1), return (TypVar 2), return(TypVar 3), return(TypVar 4), return (TypVar 5), return (TypVar 6)]
+
+-- |recursive type generator
+instance Arbitrary Typ where
+ arbitrary = quantify (sized typ')
+ where typ' 0 = frequency [(1, return Int), (6, liftM TVar arbitrary)]
+ typ' n | n>0 =
+ frequency [(1, liftM TVar arbitrary), (2,liftM2 Arrow subtyp1 subtyp1), (1,liftM List subtyp2),
+ (1,return Int), (1,liftM2 TPair subtyp1 subtyp1), (1,liftM2 TEither subtyp1 subtyp1)]
+ where subtyp1 = typ' (n `div` 2)
+ subtyp2 = typ' (n-1)
+ quantify t = do {tau <- t;
+ return (addquantifiers tau (usedvars tau []))
+ }
+ usedvars tau vars = case tau of
+ TVar (TypVar i) -> (i:vars)
+ Arrow t1 t2 -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
+ List t1 -> (usedvars t1 []) ++ vars
+ Int -> vars
+ TPair t1 t2 -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
+ TEither t1 t2 -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
+-- _ -> vars
+ addquantifiers tau l = case reverse.sort.nub $ l of
+ [] -> tau
+ x:xs -> if x < 4
+ then addquantifiers (AllStar (TypVar x) tau) xs
+ else addquantifiers (All (TypVar x) tau) xs
+
+
+-- *test properties
+-- |returns only True if the free theorem with the example produced leads to the contradiction "() == _|_"
+-- or "0 == _|_"
+prop_CompletelySolved::Typ -> Bool
+prop_CompletelySolved typ =
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal Zero Bottom -> True
+ Equal EUnit Bottom -> True
+ _ -> False
+
+
+-- |returns only True if the free theorem with the example produced leads to the an expression of the form "expr1 == expr2"
+prop_DownToEqual typ =
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal _ _ -> True
+ _ -> False
+
+prop_Test typ = trace (showTyp typ) True
+
+--prop_Classified :: Typ -> IO Property
+prop_Classified typ =
+-- do {print typ;
+--error (showTyp typ)
+-- return (
+ trace (showTyp typ)
+ (classify (noTerm) "No Term." $
+ classify (equal) "Reduced to Equal" $
+ classify (precond) "Still with Precondition" $
+ classify (true) "True" $
+ True)
+-- }
+ where noTerm = case testTerm typ of
+ Nothing -> True
+ _ -> False
+ equal = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal _ _ -> True
+ _ -> False
+ else False
+ precond = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal _ _ -> False
+ And [] -> False
+ _ -> True
+ else False
+ true = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ And [] -> True
+ _ -> False
+ else False
+
+check_Classified typ test = case test of
+ 1 -> noTerm
+ 2 -> equal
+ 3 -> precond
+ 4 -> true
+ where noTerm = case testTerm typ of
+ Nothing -> True
+ _ -> False
+ equal = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal _ _ -> True
+ _ -> False
+ else False
+ precond = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ Equal _ _ -> False
+ And [] -> False
+ _ -> True
+ else False
+ true = if not noTerm
+ then
+ case getCompleteRaw typ of
+ Left _ -> False
+ Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
+ And [] -> True
+ _ -> False
+ else False
+
+prop_HowManyTerms typ =
+ classify (findsTerm) "Term" $
+ classify (not findsTerm) "No Term" $
+ True
+ where findsTerm = if (testTerm typ) == Nothing then False else True
+
+mainTest = quickCheck prop_Classified
projects / darcs-mirror-polyfix.git / commitdiff