free-theorems-counterexamples-0.3.1.0: Language/Haskell/FreeTheorems/Variations/CounterExamples/Common/AlgCommon.hs
module Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
(TermVar(..), Term(..), TypedVar, TermCont, Cont(..), TrackCont, M, Rule(..), History(..),
trace, traceIOStart, traceIOFile, traceIO, traceSimplify, traceTemp,
first, isFst, second, isSnd, listhead, isHead, fromJust, isFromJust, fromLeft, isFromLeft, fromRight, isFromRight,
firstApp, isFstApp, secondApp, isSndApp, listheadApp, isHeadApp, fromJustApp, isFromJustApp, fromLeftApp, isFromLeftApp,
fromRightApp, isFromRightApp,
emptyCont, emptyTermCont, removeVar, removeVarStar, updateTVarStar, updateTVar, updateVar, updateVarStar,
unpointed, isElementaryType, findfirstSpecialType, findfirstWithTVars, findallWithTVars,
findfirst, findall,
typeCheckArrowListArg, typeCheckArrowMaybeArg, typeCheckList, typeCheckMaybe, typeCheckArrowUnPointedArgPointedRes, typeCheckArrowArgArrow,
typeCheckArrow, typeCheckInt, typeCheckNat, typeCheckBrace, typeCheckBool, typeCheckPair, typeCheckArrowPairArg,
typeCheckArrowEitherArg, typeCheckEither,
insertArgument, subst, substAllInt, makePlusPair, makePlusElem, makeFuncPair,
initialiseTermCont, mergeTermCont,
simplifyTerm, simplifyAppOnly, simplifyTermCont, simplifyTrackCont,
insertTermsInTrackCont, applyTrackCont, assignTypeRelFuncs, getTypeRelFuncNamesNonStrict,
showVarList, prependRelFunc, getTrackContWithFuncNames, showFuncNames, renumberVariables,
getVarNums, renumberVars, mapDisRelFuncsToNames, showTermCont, printTermCont, showTermContList,
printResult, printTyp, showCont, showTerm, showTermWithNames, showTyp, showTrackCont, showRawTrackCont,
showTrackContApplication, showTrackContApplicationWithNames, getTrackContApplicationSolved, showTrackContApplicationSolved,
showFuncNamesInt, makeTrackString, trackAll, trackRules) where
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
-- * Debugging options
----------------------------------------------------------------------------------------------
--------------------------DEBUG-TOOLS---------------------------------------------------------
----------------------------------------------------------------------------------------------
import System.IO.Unsafe
-- |set debugging functions from the below list
trace :: String -> a -> a
trace = trace_ignore
--trace = trace_toShell
---- OutputFile options ----
-- |set file where debug output of traceIO is send to
--traceIOStart = traceIOStart_makeFile
traceIOStart = traceIOStart_ignore
traceIOFile = "./traceIO.log.hs"
---- traceIO settings ----
-- | trace informations on every rule, gives context and typ before and after rule application
-- exception: Bottom and Var*
traceIO :: String -> Typ -> Cont -> Typ -> Cont -> a -> a
traceIO = traceIO_ignore
--traceIO = traceIO_ordDiff
--traceIO = traceIO_ord2shell
--traceIO = traceIO_checkOrderInc
--traceIO = traceIO_cont2shell
--traceIO = \rule tauIn gammaIn tauOut gammaOut -> (traceIO_ord2shell rule tauIn gammaIn tauOut gammaOut) . traceIO_checkOrderInc rule tauIn gammaIn tauOut gammaOut
-- |some more special purpose trace functions
--traceSimplify = trace_toShell
traceSimplify = trace_ignore
--traceTemp = trace_toShell
traceTemp = trace_ignore
---- show settings ---
-- |show settings for the trace functions
showContTrace = showCont
---- trace functions ----
-- |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++"\n")) == () then a else a
traceIO_ignore rule tauIn gammaIn tauOut gammaOut a = a
traceIO_order2shell rule tauIn gammaIn tauOut gammaOut a =
if unsafePerformIO (putStr (rule ++ ":\t" ++ (show (count gammaOut tauOut)) ++ "\n")) == () then a else 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 rule ++ ":\n" ++ (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 || (not . and) (map (==0) 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 for the order check
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)) --lists and maybe are counted together.
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])
TNat -> (depth,zeros,[0,0,0,0])
TBrace -> (depth,zeros,[0,0,0,0])
TBool -> (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)
TMaybe tau1 -> let (d,el,ol) = countTyp' tau1 (depth+1) in
(d,el,zipWith (+) [0,0,1,0] ol)
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----------------------------------------------------
----------------------------------------------------------------------------------------------
-- *Data type declarations
-- |Termvariable is taken to be a number. Monad M will keep track of the numbering when new
-- Termvariables are produced.
newtype TermVar = TermVar Int deriving (Show, Eq, Ord)
-- |Syntax of the terms used in the algorithm. The term set is a bit smaller than the whole
-- set of PolyFix*, because Case statements are restricted to make only the kinds used in
-- the algorithm possible.
data Term = Var TermVar
| Abs TermVar Typ Term
| App Term Term
| TAbs TypVar Term
| Nil Typ
| Cons Term Term
-- |Case statement for lists
-- Case l v t1 <==> Case l of {[] => _|_; v:_ => t1}
| LCase Term TermVar Term
| Bottom Typ -- statt Fix
| Brace
-- |integer case-statement
-- ICase t0 t1 <==> Case t0 of {0 => t1; _ => _|_}
| ICase Term Term
-- |integer case-statement
-- NCase t0 t1 <==> Case t0 of {0 => t1; _ => _|_}
| NCase Term Term
-- |brace case-statement
-- BCase t0 t1 <==> Case t0 of {() => t1}
| BCase Term Term
-- |bool case-statement
-- BoolCase t0 t1 <==> Case t0 of {False => t1; _ => _|_}
| BoolCase Term Term
| Fls
| Zero
| Pair Term Term
-- |case-statement for pairs
-- PCase p v1 v2 t <==> Case p of {(v1,v2) ==> t}
| PCase Term TermVar TermVar Term
-- |case-statement for either
-- ECase e v1 t1 v2 t2 <==> Case e of {Left(v1) => t1; Right(v2) => t2}
| ECase Term TermVar Term TermVar Term
| Right Term
| Left Term
-- Terms of TMaybe
| MJust Term
-- | MNothing
| MCase Term TermVar Term
deriving (Show, Eq)
-- |abbreviation for the pair (TermVar,Typ)
type TypedVar = (TermVar,Typ)
-- |represents the sigma environments sigma_1 and sigma^+_2. sigma_2 is not tracked.
type TermCont = Map.Map TermVar ((Term,Term),History)
-- |representation of \Gamma and \Sigma, both devided in a stared and unstared part,
-- as necessary regarding an \internalinput.
data Cont = Cont { tVars :: [TypVar], tVarsStar :: [TypVar], vars :: [TypedVar], varsStar :: [TypedVar] } deriving (Show,Eq)
-- |the list of the disrelater. The type has not to be tracked, because it is always clear.
type TrackCont = (Typ,[(Term,Term)])
type M = Mona.M Term
-- we introduce just the rules needed -> where term variables are produced in a non trivial way.
-- if the stared and the unstared variant are equal in historical behaviour, we introduce just the unstared one.
data Rule = WrapTo | MaybeTo | Head | RJust | PairTo | Proj | EitherTo | BottomToStripe | ArrowToStar | Dist1 | Dist2 |BottomTo deriving(Show,Eq)
data History = Branch Rule History | Split Rule History History | Leaf deriving(Show)
-- | some abbreviations for special functions.
-- They are used in the paper as well
-- |\p -> Case p of {(v1,v2) ==> v1}
first :: Typ -> M Term
first tau= do {i<-newInt;
j<-newInt;
k<-newInt;
let x = TermVar i
y = TermVar j
p = TermVar k in
return (Abs p tau (PCase (Var p) x y (Var x)))
}
-- |Check if a term t is of form "fst"
isFst :: Term -> Bool
-- isFst t =
-- case t of
-- Abs _ _ (PCase _ x _ t1) ->
-- if Var x == t1 then True else False
-- _ -> False
isFst (Abs v _ (PCase t x _ (Var y))) | x == y && Var v == t = True
| otherwise = False
isFst _ = False
-- |\p -> Case p of {(v1,v2) ==> v2}
second :: Typ -> M Term
second tau = do {i<-newInt;
j<-newInt;
k<-newInt;
let x = TermVar i
y = TermVar j
p = TermVar k in
return (Abs p tau (PCase (Var p) x y (Var y)))
}
-- |Check if a term t is of form "snd"
isSnd :: Term -> Bool
-- isSnd t =
-- case t of
-- Abs _ _ (PCase _ _ y t1) ->
-- if Var y == t1 then True else False
-- _ -> False
isSnd (Abs v _ (PCase t _ x (Var y))) | x == y && Var v == t = True
| otherwise = False
isSnd _ = False
-- |\l -> Case l of {[] => _|_; x:_ => x}
listhead :: Typ -> M Term
listhead tau = do {i<-newInt;
j<-newInt;
let x = TermVar i
l = TermVar j in
return (Abs l (List tau) (LCase (Var l) x (Var x)))
}
-- |Check if a term t is of form "head"
isHead :: Term -> Bool
-- isHead t =
-- case t of
-- Abs _ _ (LCase _ v t2) ->
-- if Var v == t2 then True else False
-- _ -> False
isHead (Abs v _ (LCase t x (Var y))) | x == y && Var v == t = True
| otherwise = False
isHead _ = False
-- |\l -> Case l of {Just x => x}
fromJust :: Typ -> M Term
fromJust tau = do {i<-newInt;
j<-newInt;
let x = TermVar i
l = TermVar j in
return (Abs l (TMaybe tau) (MCase (Var l) x (Var x)))
}
-- |Check if a term t is of form "fromJust"
isFromJust :: Term -> Bool
-- isFromJust t =
-- case t of
-- Abs _ _ (MCase _ v t2) ->
-- if Var v == t2 then True else False
-- _ -> False
isFromJust (Abs v _ (MCase t x (Var y))) | x == y && Var v == t = True
| otherwise = False
isFromJust _ = False
-- |\e -> Case e of {Left x => x; Right x => _|_}
fromLeft :: Typ -> Typ -> M Term
fromLeft tau tau' = do {i<-newInt;
j<-newInt;
k<-newInt;
let x = TermVar i
y = TermVar j
e = TermVar k in
return (Abs e (TEither tau tau') (ECase (Var e) x (Var x) y (Bottom tau)))
}
-- |Check if a term t is of form "fromLeft"
isFromLeft :: Term -> Bool
-- isFromLeft t =
-- case t of
-- Abs _ _ (ECase _ v1 t1 _ t2) ->
-- if Var v1 == t1
-- then case t2 of
-- Bottom _ -> True
-- _ -> False
-- else False
-- _ -> False
isFromLeft (Abs v _ (ECase t x (Var y) _ _)) | x == y && Var v == t = True
| otherwise = False
isFromLeft _ = False
-- |\e -> Case e of {Left x => _|_; Right x => x}
fromRight :: Typ -> Typ -> M Term
fromRight tau tau' = do {i<-newInt;
j<-newInt;
k<-newInt;
let x = TermVar i
y = TermVar j
e = TermVar k in
return (Abs e (TEither tau tau') (ECase (Var e) x (Bottom tau') y (Var y)))
}
-- |Check if a term t is of form "fromRight"
isFromRight :: Term -> Bool
-- isFromRight t =
-- case t of
-- Abs _ _ (ECase _ _ t1 v2 t2) ->
-- if Var v2 == t2
-- then case t1 of
-- Bottom _ -> True
-- _ -> False
-- else False
-- _ -> False
isFromRight (Abs v _ (ECase t _ _ x (Var y))) | x == y && Var v == t = True
| otherwise = False
isFromRight _ = False
-- | some abbreviations for special cases of the Case-statements.
-- They are used in the paper as well
-- |Case p of {(v1,v2) ==> v1}
firstApp :: Term -> M Term
firstApp p = do {i<-newInt;
j<-newInt;
let x = TermVar i
y = TermVar j in
return (PCase p x y (Var x))
}
-- |Check if a term t is of form "fst t'"
isFstApp :: Term -> Bool
isFstApp t =
case t of
PCase _ x _ t1 -> if Var x == t1 then True else False
_ -> False
-- |Case p of {(v1,v2) ==> v2}
secondApp :: Term -> M Term
secondApp p = do {i<-newInt;
j<-newInt;
let x = TermVar i
y = TermVar j in
return (PCase p x y (Var y))
}
-- |Check if a term t is of form "snd t'"
isSndApp :: Term -> Bool
isSndApp t =
case t of
PCase _ _ y t1 -> if Var y == t1 then True else False
_ -> False
-- |Case l of {[] => _|_; x:_ => x}
listheadApp :: Term -> Typ -> M Term
listheadApp l tau = do {i<-newInt;
let x = TermVar i in
return (LCase l x (Var x))
}
-- |Check if a term t is of form "head t'"
isHeadApp :: Term -> Bool
isHeadApp t =
case t of
LCase _ v t2 -> if Var v == t2 then True else False
_ -> False
-- |Case l of {Just x => x}
fromJustApp :: Term -> Typ -> M Term
fromJustApp l tau = do {i<-newInt;
let x = TermVar i in
return (MCase l x (Var x))
}
-- |Check if a term t is of form "fromJust t'"
isFromJustApp :: Term -> Bool
isFromJustApp t =
case t of
MCase _ v t2 -> if Var v == t2 then True else False
_ -> False
-- |Case e of {Left x => x; Right x => _|_}
fromLeftApp :: Term -> Typ -> M Term
fromLeftApp e tau = do {i<-newInt;
j<-newInt;
let x = TermVar i
y = TermVar j in
return (ECase e x (Var x) y (Bottom tau))
}
-- |Check if a term t is of form "fromLeft t'"
isFromLeftApp :: Term -> Bool
isFromLeftApp t =
case t of
ECase _ v1 t1 _ t2 -> if Var v1 == t1
then case t2 of
Bottom _ -> True
_ -> False
else False
_ -> False
-- |Case e of {Left x => _|_; Right x => x}
fromRightApp :: Term -> Typ -> M Term
fromRightApp e tau = do {i<-newInt;
j<-newInt;
let x = TermVar i
y = TermVar j in
return (ECase e x (Bottom tau) y (Var y))
}
-- |Check if a term t is of form "fromLeft t'"
isFromRightApp :: Term -> Bool
isFromRightApp t =
case t of
ECase _ _ t1 v2 t2 -> if Var v2 == t2
then case t1 of
Bottom _ -> True
_ -> False
else False
_ -> False
-- *global constants
-- |global constant: the empty context \Gamma;\Sigma
emptyCont :: Cont
emptyCont = Cont [] [] [] []
-- |global constant: the empty term environments
emptyTermCont :: TermCont
emptyTermCont = Map.empty
-- *Context update functions
updateTVarStar (Cont tVars tVarsStar vars varsStar) tv = Cont tVars (tv:tVarsStar) vars varsStar
updateTVar (Cont tVars tVarsStar vars varsStar) tv = Cont (tv:tVars) tVarsStar vars varsStar
updateVar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar ((v,tau):vars) varsStar
removeVar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar (filter ((/= var).fst) vars) varsStar
updateVarStar (Cont tVars tVarsStar vars varsStar) v tau = Cont tVars tVarsStar vars ((v,tau):varsStar)
removeVarStar (Cont tVars tVarsStar vars varsStar) var = Cont tVars tVarsStar vars (filter ((/= var).fst) varsStar)
-- |check for pointedness.
-- the function implements the class membership rules for PolyFix*
unpointed :: [TypVar] -> Typ -> Bool
unpointed tvars tau = case tau of
TVar tvar -> case find (== tvar) tvars of
Nothing -> False
_ -> True
Arrow _ tau' -> unpointed tvars tau'
All tvar tau' -> unpointed (tvar:tvars) tau'
AllStar _ tau' -> unpointed tvars tau'
List _ -> False
Int -> False
TNat -> False
TPair _ _ -> False
TEither _ _ -> False
TBool -> False
TBrace -> False
TMaybe _ -> False
isElementaryType :: Typ -> Bool
isElementaryType tau =
case tau of
Int -> True
TNat -> True
TVar _ -> True
TBrace -> True
TBool -> True
_ -> False
-- *check functions for special typed variables in the term variable part of the context Cont
-- they usually take just one part of the context, i.e. a list [TypedVar]
-- |searches for a variable of type typ in vars
findfirstSpecialType :: [TypedVar] -> Typ -> Maybe TypedVar
findfirstSpecialType vars typ =
case vars of
[] -> Nothing
(x:xs) -> if snd x == typ
then Just x
else findfirstSpecialType xs typ
-- |returns the first entry of vars, whose type passes the typecheckfunction
-- It uses the type variables for pointed checks
findfirstWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [TypedVar] -> Maybe TypedVar
findfirstWithTVars typecheckfunction tvars vars =
case vars of
[] -> Nothing
(x:xs) -> if typecheckfunction tvars (snd x)
then Just x
else findfirstWithTVars typecheckfunction tvars xs
-- |returns the list of all entries of vars, whose types pass the typecheckfunction
-- It uses the type variables for pointed checks
findallWithTVars :: ([TypVar] -> Typ -> Bool) -> [TypVar] -> [(TypedVar)] -> [TypedVar]
findallWithTVars typecheckfunction tvars vars =
case vars of
[] -> []
(x:xs) -> if typecheckfunction tvars (snd x)
then (x:(findallWithTVars typecheckfunction tvars xs))
else findallWithTVars typecheckfunction tvars xs
-- |returns the first entry of vars, whose type passes the typecheckfunction
findfirst :: (Typ -> Bool) -> [TypedVar] -> Maybe TypedVar
findfirst typecheckfunction vars = case vars of
[] -> Nothing
(x:xs) -> if typecheckfunction (snd x)
then Just x
else findfirst typecheckfunction xs
-- |returns the list of all entries of vars, whose types pass the typecheckfunction
findall :: (Typ -> Bool) -> [TypedVar] -> [TypedVar]
findall typecheckfunction vars = case vars of
[] -> []
(x:xs) -> if typecheckfunction (snd x)
then (x:(findall typecheckfunction xs))
else findall typecheckfunction xs
-- ** typecheckfunctions
-- | used for (Wrap->)
typeCheckArrowListArg :: Typ -> Bool
typeCheckArrowListArg tau = case tau of
Arrow tau1 _ -> case tau1 of
List _ -> True
_ -> False
_ -> False
-- | used for (MaybeWrap->)
typeCheckArrowMaybeArg :: Typ -> Bool
typeCheckArrowMaybeArg tau = case tau of
Arrow tau1 _ -> case tau1 of
TMaybe _ -> True
_ -> False
_ -> False
-- | used for (Head), (Head*)
typeCheckList :: Typ -> Bool
typeCheckList tau = case tau of
List _ -> True
_ -> False
-- | used for (Just), (Just*)
typeCheckMaybe :: Typ -> Bool
typeCheckMaybe tau = case tau of
TMaybe _ -> True
_ -> False
-- | used for (Bottom->*1)
typeCheckArrowUnPointedArgPointedRes :: [TypVar] -> Typ -> Bool
typeCheckArrowUnPointedArgPointedRes tvars tau = case tau of
Arrow tau1 tau2 -> unpointed tvars tau1 && (not (unpointed tvars tau2))
_ -> False
-- | used for (L->->*)
typeCheckArrowArgArrow :: Typ -> Bool
typeCheckArrowArgArrow tau = case tau of
Arrow tau1 _ -> case tau1 of
Arrow _ _ -> True
_ -> False
_ -> False
-- | used for (Bottom->), (Bottom->*2), (App'*)
typeCheckArrow :: Typ -> Bool
typeCheckArrow tau = case tau of
Arrow _ _ -> True
_ -> False
-- | used for (Drop1)
typeCheckInt :: Typ -> Bool
typeCheckInt tau = case tau of
Int -> True
_ -> False
-- | used for (Drop5)
typeCheckNat :: Typ -> Bool
typeCheckNat tau = case tau of
TNat -> True
_ -> False
-- | used for (Drop2)
typeCheckBrace :: Typ -> Bool
typeCheckBrace tau = case tau of
TBrace -> True
_ -> False
-- | used for (Drop4)
typeCheckBool :: Typ -> Bool
typeCheckBool tau = case tau of
TBool -> True
_ -> False
-- | used for (Proj), (Proj*)
typeCheckPair :: Typ -> Bool
typeCheckPair tau = case tau of
TPair _ _ -> True
_ -> False
-- | used for (Pair->)
typeCheckArrowPairArg :: Typ -> Bool
typeCheckArrowPairArg tau = case tau of
Arrow tau1 _ -> case tau1 of
TPair _ _ -> True
_ -> False
_ -> False
-- | used for (LE->)
typeCheckArrowEitherArg :: Typ -> Bool
typeCheckArrowEitherArg tau = case tau of
Arrow tau1 _ -> case tau1 of
TEither _ _ -> True
_ -> False
_ -> False
-- | used for (Dist1), (Dist2), (Dist1*), (Dist2*)
typeCheckEither :: Typ -> Bool
typeCheckEither tau = case tau of
TEither _ _ -> True
_ -> False
-- * support functions
-- | Application of an argument to a function
insertArgument :: Term -> Term -> Term
insertArgument f x = case f of
Abs v _ t -> subst t x v
Bottom (Arrow tau1 tau2) -> Bottom tau2
_ -> error ("unexpected termstructure" ++ (showTerm f))
-- | substitutes new (Term) for old (TermVar) in the term m
subst :: Term -> Term -> TermVar -> Term
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)
App m1 m2 -> App (subst m1 new old) (subst m2 new old)
TAbs tau m' -> TAbs tau (subst m' new old)
Cons m1 m2 -> Cons (subst m1 new old) (subst m2 new old)
LCase m0 v2 m2 -> LCase (subst m0 new old) v2 (subst m2 new old)
Pair m1 m2 -> Pair (subst m1 new old) (subst m2 new old)
PCase m0 v1 v2 m1 -> PCase (subst m0 new old) v1 v2 (subst m1 new old)
Right m -> Right (subst m new old)
Left m -> Left (subst m new old)
ECase m0 v1 m1 v2 m2 -> ECase (subst m0 new old) v1 (subst m1 new old) v2 (subst m2 new old)
ICase m0 m1 -> ICase (subst m0 new old) (subst m1 new old)
NCase m0 m1 -> NCase (subst m0 new old) (subst m1 new old)
BCase m0 m1 -> BCase (subst m0 new old) (subst m1 new old)
BoolCase m0 m1 -> BoolCase (subst m0 new old) (subst m1 new old)
MJust m0 -> MJust (subst m0 new old)
MCase m0 v2 m2 -> MCase (subst m0 new old) v2 (subst m2 new old)
_ -> m
-- | calls subst for a list of termVariables (with according to the numbers) to be substituted
substAllInt :: Term -> [(Int,Term)] -> Term
substAllInt t l =
case l of
[] -> t
(i,t'):xs -> substAllInt (subst t t' (TermVar i)) xs
-- | produces a Pair (p^+,p^+) of the given type, with p+ as described in the plus-term definition of the paper
makePlusPair :: Typ -> M (Maybe (Term, Term))
makePlusPair tau = do {x <- makePlusElem tau;
case x of
Just t -> return (Just (t,t))
_ -> return Nothing
}
-- | produces a Term p^+ of the given type, as described in the plus-term definition of the paper
makePlusElem :: Typ -> M (Maybe Term)
makePlusElem tau = case tau of
TVar var -> return (Just Brace)
Arrow tau1 tau2 -> do {x <- makePlusElem tau2;
i <- newInt;
let erg = case x of
Just t -> Just (Abs (TermVar i) tau1 t)
_ -> Nothing
in
return erg
}
List tau -> do {x <- makePlusElem tau;
let erg = case x of
Just t -> Just (Cons t (Nil tau))
_ -> Nothing
in
return erg
}
TMaybe tau -> do {x <- makePlusElem tau;
let erg = case x of
Just t -> Just (MJust t)
_ -> Nothing
in
return erg
}
Int -> return (Just Zero)
TNat -> return (Just Zero)
TBrace -> return (Just Brace)
TBool -> return (Just Fls)
TPair tau1 tau2 -> do {x <- makePlusElem tau1;
y <- makePlusElem tau2;
let erg = case x of
Just t1 -> case y of
Just t2 -> Just (Pair t1 t2)
Nothing -> Nothing
Nothing -> Nothing
in
return erg
}
TEither tau1 tau2 -> do {x <- makePlusElem tau1;
y <- makePlusElem tau2;
let erg = case x of
Just t1 -> Just (Left t1)
_ -> case y of
Just t2 -> Just (Right t2)
_ -> Nothing
in
return erg
}
_ -> return Nothing
-- |the function equals the lemma about the function construction (g(x_1),g(x_2))^{\Gamma,\tau}_{\varpi}
makeFuncPair :: Typ -> TrackCont -> Cont -> (Term,Term) -> M (Term,Term)
makeFuncPair tau trc' gamma resPair =
let (z,z') = resPair
(ctau,trc) = trc' in
case tau of
TVar beta -> do {i <- newInt;
let w = TermVar i
g' = Abs w tau (BCase (Var w) z') in
if unpointed (tVars gamma) tau
then return (Abs w tau z, g')
else return (Abs w tau (BCase (Var w) z), g')
}
Int -> do {i <- newInt;
let w = TermVar i in
return (Abs w tau (ICase (Var w) z), Abs w tau (ICase (Var w) z'))
}
TNat -> do {i <- newInt;
let w = TermVar i in
return (Abs w tau (NCase (Var w) z), Abs w tau (NCase (Var w) z'))
}
TBrace -> do {i <- newInt;
let w = TermVar i in
return (Abs w tau (BCase (Var w) z), Abs w tau (BCase (Var w) z'))
}
TBool -> do {i <- newInt;
let w = TermVar i in
return (Abs w tau (BoolCase (Var w) z), Abs w tau (BoolCase (Var w) z'))
}
List tau' -> case trc of
[] -> do{i <- newInt;
j <- newInt;
let w = TermVar i
h = TermVar j
in
return (Abs w tau (LCase (Var w) h z), Abs w tau (LCase (Var w) h z'))
}
_:xs -> do{i <- newInt;
j <- newInt;
(g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
let w = TermVar i
u = TermVar j in
return (Abs w tau (LCase (Var w) u (App g (Var u))),
Abs w tau (LCase (Var w) u (App g' (Var u))))
}
TMaybe tau' -> case trc of
[] -> do{i <- newInt;
j <- newInt;
let w = TermVar i
h = TermVar j
in
return (Abs w tau (MCase (Var w) h z), Abs w tau (MCase (Var w) h z'))
}
_:xs -> do{i <- newInt;
j <- newInt;
(g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
let w = TermVar i
u = TermVar j in
return (Abs w tau (MCase (Var w) u (App g (Var u))),
Abs w tau (MCase (Var w) u (App g' (Var u))))
}
TPair tau' tau'' -> case trc of
[] -> do{i <- newInt;
j <- newInt;
k <- newInt;
let w = TermVar i
x = TermVar j
y = TermVar k
in
return (Abs w tau (PCase (Var w) x y z), Abs w tau (PCase (Var w) x y z'))
}
(Abs _ _ (PCase _ v _ (Var v')),_):xs ->
if v == v' then
do{i <- newInt;
j <- newInt;
m <- newInt;
n <- newInt;
let x = TermVar j
y = TermVar m
u = TermVar n
w = TermVar i
(k,k') = (Abs u tau'' z, Abs u tau'' z')
in
do{(h,h') <- makeFuncPair tau' (ctau,xs) gamma (k,k');
return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))
}
}
else
do{i <- newInt;
j <- newInt;
m <- newInt;
n <- newInt;
(k,k') <- makeFuncPair tau'' (ctau,xs) gamma resPair;
let x = TermVar j
y = TermVar m
u = TermVar n
w = TermVar i
(h,h') = (Abs x tau' (Abs y tau'' (App k (Var y))), Abs x tau' (Abs y tau'' (App k' (Var y))))
in
return (Abs w tau (PCase (Var w) x y (App (App h (Var x)) (Var y))), Abs w tau (PCase (Var w) x y (App (App h' (Var x)) (Var y))))
}
TEither tau' tau'' -> do{i <- newInt;
j <- newInt;
let w = TermVar i
x = TermVar j
in
case trc of
[] -> return (Abs w tau (ECase (Var w) x (fst resPair) x (fst resPair)),
Abs w tau (ECase (Var w) x (fst resPair) x (snd resPair)))
(Abs _ _ (ECase _ _ (Var _) _ _),_):xs ->
do{(g,g') <- makeFuncPair tau' (ctau,xs) gamma resPair;
return (Abs w tau (ECase (Var w) x (App g (Var x)) x (fst resPair)),
Abs w tau (ECase (Var w) x (App g' (Var x)) x (snd resPair)))
}
(Abs _ _ (ECase _ _ _ _ (Var _)),_):xs ->
do{(g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;
return (Abs w tau (ECase (Var w) x (fst resPair) x (App g (Var x))),
Abs w tau (ECase (Var w) x (snd resPair) x (App g' (Var x))))
}
}
Arrow tau' tau'' -> case trc of
[] -> do{ i <- newInt;
(g,g') <- makeFuncPair tau'' (ctau,[]) gamma resPair;
Just (u,u') <- makePlusPair tau';
let x = TermVar i in
return (Abs x tau' (App g (App (Var x) u)), Abs x tau' (App g' (App (Var x) u')))
}
(f,f'):xs -> do {i <- newInt;
(g,g') <- makeFuncPair tau'' (ctau,xs) gamma resPair;
let x = TermVar i in
return (Abs x tau' (App g (App f (Var x))), Abs x tau' (App g' (App f' (Var x))))
}
-- |support function for the term variable environment initialisation by the rules (Bottom) and (Ax*)
initialiseTermCont :: [TypedVar] -> M TermCont
initialiseTermCont varlist =
case varlist of
[] -> return Map.empty
(x,tau):xs -> do{map <- initialiseTermCont xs;
Just p <- makePlusPair tau;
return (Map.insert x (p,Leaf) map)
}
-- |tries to melt down the two TermCont from the premise of Arrow->* to one single suitable context. Uses the history therefore
mergeTermCont :: TermCont -> TermCont -> Maybe TermCont
mergeTermCont c1 c2 =
let difference = Map.union (Map.difference c1 c2) (Map.difference c2 c1) in
if Map.filter (\x->x==False) (Map.intersectionWith checkCompareTerm c1 c2) == Map.empty
then
Just (Map.union (Map.intersectionWith compareTerm c1 c2) difference)
else
Nothing
compareTerm :: ((Term,Term),History) -> ((Term,Term),History) -> ((Term,Term),History)
compareTerm c1 c2 =
let (_,his1) = c1
(_,his2) = c2
in
if firstIsBetter his1 his2 then c1 else c2
checkCompareTerm c1 c2 =
let (_,his1) = c1
(_,his2) = c2
in
if firstIsBetter his1 his2 || firstIsBetter his2 his1 then True else False
firstIsBetter :: History -> History -> Bool
firstIsBetter his1 his2 =
case his1 of
Leaf -> case his2 of
Leaf -> True
_ -> False
Branch rule his ->
case his2 of
Leaf -> True
Branch rule' his' -> if rule == rule' then firstIsBetter his his' else False
_ -> False
Split rule hisa hisb ->
case his2 of
Leaf -> True
Split rule' hisa' hisb' -> if rule == rule' then (firstIsBetter hisa hisa' && firstIsBetter hisb hisb') else False
_ -> False
-- *simplifications
-- |removes App in terms. Resolves case statements if possible. Destroys the typing information.
simplifyTerm :: Term -> Term
simplifyTerm t =
case t of
Abs v tau t1 -> traceSimplify "Simpl: Abs v tau t1" (Abs v tau (simplifyTerm t1))
App t1 t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom _ -> traceSimplify "Simpl: App _|_ t2" (Bottom (error "Typ not valid anymore."))
Abs v tau t1'' -> traceSimplify "Simpl: App (Abs _) t2" (simplifyTerm (subst t1'' (simplifyTerm t2) v))
--case-statements can appear.
_ -> traceSimplify "Simpl: App not reduced." (App t1' (simplifyTerm t2))
TAbs v t1 -> traceSimplify "Simpl: TAbs eliminated." (simplifyTerm t1)
Cons t1 t2 -> traceSimplify "Simpl: Cons." (Cons (simplifyTerm t1) (simplifyTerm t2))
LCase t1 v t3 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom _ -> traceSimplify "Simpl: List Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
Nil _ -> error "LCase with []! This should not appear!"
Cons t (Nil _) -> traceSimplify "Simpl: List Case with x:_ to t3[t/v]" (simplifyTerm (subst t3 t v))
Cons t _ -> error "List with mor than one element! This should not appear!"
_ -> traceSimplify "Simpl: List Case not reduced." (LCase t1' v (simplifyTerm t3))
ICase t1 t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom tau -> traceSimplify "Simpl: ICase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
Zero -> traceSimplify "Simpl: ICase with 0 to t1" (simplifyTerm t2)
_ -> traceSimplify "Simpl: ICase not reduced." (ICase (simplifyTerm t1) (simplifyTerm t2))
NCase t1 t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom tau -> traceSimplify "Simpl: NCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
Zero -> traceSimplify "Simpl: NCase with 0 to t1" (simplifyTerm t2)
_ -> traceSimplify "Simpl: NCase not reduced." (NCase (simplifyTerm t1) (simplifyTerm t2))
BCase t1 t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom tau -> traceSimplify "Simpl: BCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
Brace -> traceSimplify "Simpl: BCase with () to t1" (simplifyTerm t2)
_ -> traceSimplify "Simpl: BCase not reduced." (BCase (simplifyTerm t1) (simplifyTerm t2))
BoolCase t1 t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom tau -> traceSimplify "Simpl: BoolCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
Fls -> traceSimplify "Simpl: BoolCase with Fls to t1" (simplifyTerm t2)
_ -> traceSimplify "Simpl: BoolCase not reduced." (BoolCase (simplifyTerm t1) (simplifyTerm t2))
Pair t1 t2 -> traceSimplify "Simpl: Pair: reducing components." (Pair (simplifyTerm t1) (simplifyTerm t2))
PCase t1 v1 v2 t2 -> case simplifyTerm t1 of
Pair t11 t12 -> traceSimplify "Simpl: PCase with Pair to t2[t11/v1,t12/v2]" (simplifyTerm (subst (subst t2 t11 v1) t12 v2))
Bottom _ -> traceSimplify "Simpl: PCase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
_ -> traceSimplify "Simpl: PCase not reduced." (PCase (simplifyTerm t1) v1 v2 (simplifyTerm t2))
ECase t1 v1 t2 v2 t3 -> case simplifyTerm t1 of
Left t1' -> traceSimplify "Simpl: ECase with Left t1' to t2[t1'/v1]" (simplifyTerm (subst t2 t1' v1))
Right t1' -> traceSimplify "Simpl: ECase with Left t1' to t3[t1'/v2]" (simplifyTerm (subst t3 t1' v2))
Bottom _ -> traceSimplify "Simpl: ECase with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
_ -> traceSimplify "Simpl: ECase not reduced." (ECase (simplifyTerm t1) v1 (simplifyTerm t2) v2 (simplifyTerm t3))
Right t1 -> traceSimplify "Simpl: Right" (Right (simplifyTerm t1))
Left t1 -> traceSimplify "Simpl: Left" (Left (simplifyTerm t1))
Var _ -> t
Nil _ -> t
Bottom _ -> t
Zero -> Zero
Brace -> Brace
Fls -> Fls
MJust t1 -> traceSimplify "Simpl: MJust." (MJust (simplifyTerm t1))
MCase t1 v t2 -> let t1' = simplifyTerm t1 in
case t1' of
Bottom _ -> traceSimplify "Simpl: Maybe Case with _|_ to _|_" (Bottom (error "Typ not valid anymore."))
MJust t -> traceSimplify "Simpl: Maybe Case with Just x to t2[t1/v]" (simplifyTerm (subst t2 t v))
_ -> traceSimplify "Simpl: Maybe Case not reduced." (MCase t1' v (simplifyTerm t2))
-- |simplifier for terms, just inserting function arguments, if possible. It does not resolve case-statements, but removes type abstractions.
simplifyAppOnly :: Term -> Term
simplifyAppOnly t =
case t of
Abs v tau t1 -> Abs v tau (simplifyAppOnly t1)
App t1 t2 -> let t1' = simplifyAppOnly t1 in
case t1' of
Bottom _ -> Bottom (error "Typ not valid anymore.")
Abs v tau t1'' -> simplifyAppOnly (subst t1'' (simplifyAppOnly t2) v)
_ -> App t1' (simplifyAppOnly t2) --for App, Var and Case-statements
TAbs v t1 -> simplifyAppOnly t1
Cons t1 t2 -> Cons (simplifyAppOnly t1) (simplifyAppOnly t2)
LCase t1 v t3 -> LCase (simplifyAppOnly t1) v (simplifyAppOnly t3)
ICase t1 t2 -> ICase (simplifyAppOnly t1) (simplifyAppOnly t2)
NCase t1 t2 -> NCase (simplifyAppOnly t1) (simplifyAppOnly t2)
BCase t1 t2 -> BCase (simplifyAppOnly t1) (simplifyAppOnly t2)
BoolCase t1 t2 -> BoolCase (simplifyAppOnly t1) (simplifyAppOnly t2)
Pair t1 t2 -> Pair (simplifyAppOnly t1) (simplifyAppOnly t2)
PCase t1 v1 v2 t2 -> PCase (simplifyAppOnly t1) v1 v2 (simplifyAppOnly t2)
ECase t1 v1 t2 v2 t3 -> ECase (simplifyAppOnly t1) v1 (simplifyAppOnly t2) v2 (simplifyAppOnly t3)
Right t1 -> Right (simplifyAppOnly t1)
Left t1 -> Left (simplifyAppOnly t1)
Var _ -> t
Nil _ -> t
Bottom _ -> t
Zero -> Zero
Brace -> Brace
Fls -> Fls
MJust t1 -> MJust (simplifyAppOnly t1)
MCase t1 v t2 -> MCase (simplifyAppOnly t1) v (simplifyAppOnly t2)
-- _ -> error ("unexpected Term structure during simplification: " ++ (showTerm t))
-- |calls simplifyTerm for all Terms in the TermCont (term variable environments)
simplifyTermCont :: TermCont -> TermCont
simplifyTermCont c =
let simplifyPair ((t1,t2),his) = ((simplifyTerm t1, simplifyTerm t2),his) in
Map.map simplifyPair c
-- | calls simplifyTerm for all Terms in the list of the disrelater, i.e. for all entries of TrackCont
simplifyTrackCont :: TrackCont -> TrackCont
simplifyTrackCont trc =
let (ctau,l) = trc in
(ctau,simplifyTrackCont' l)
simplifyTrackCont' trc =
case trc of
[] -> []
(v1,v2):xs -> (simplifyTerm v1, simplifyTerm v2):(simplifyTrackCont' xs)
-- | replaces term variables in the disrelater by the terms they represent (given in the map)
-- maybe buggy
insertTermsInTrackCont :: TrackCont -> (Map.Map Int Term) -> TrackCont
insertTermsInTrackCont trc substs =
let (ctau,ls) = trc in
(ctau,map sub ls)
where sub t = let (t1,t2) = t in (sub' t1, sub' t2)
sub' t =
case t of
Abs x tau (App y (Var (TermVar i))) ->
if Var x == y && Map.member i substs
then Abs x tau (App y (substs Map.! i))
else t
_ -> t
-- | applies the disrelater to a term. This should lead to (p+,_|_) or (_|_._|_) for a term with a corresponding disrelater
-- and all termvariables substituted by the corresponding terms.
applyTrackCont :: Term -> TrackCont -> (Term,Term)
applyTrackCont t trc =
let (_,l) = trc in applyTrackCont' (t,t) l
applyTrackCont' :: (Term,Term) -> [(Term,Term)] -> (Term,Term)
applyTrackCont' (t1,t2) trc =
case trc of
[] -> (t1,t2)
x:xs -> applyTrackCont' (App (fst x) t1, App (snd x) t2) xs
-- *output enhancement and synchronisation with free-theorems package
-- | instantiate type relating functions.
-- | input is the type and a list of functionnames, representing the sequence in which they should be used
assignTypeRelFuncs :: Typ -> [String] -> String
assignTypeRelFuncs tau names = foldr (\x y -> ((getAt names (fst x)) ++ " = " ++ (snd x)) ++ y) "" (sort (assignTypeRelFuncs' tau))
assignTypeRelFuncs' :: Typ -> [(Int,String)]
assignTypeRelFuncs' tau =
case tau of
All (TypVar i) tau' -> (i-1, "const ()\t"):assignTypeRelFuncs' tau'
AllStar (TypVar i) tau' -> (i-1, "id\t\t"):assignTypeRelFuncs' tau'
_ -> []
-- | get a list of names of the type variables that can be interpreted non-strict.
getTypeRelFuncNamesNonStrict :: Typ -> [String] -> [String]
getTypeRelFuncNamesNonStrict tau names =
snd.unzip.sort.getList $ tau
where getList tau =
case tau of
All (TypVar i) tau' -> (i-1, getAt names (i-1)):getList tau'
AllStar (TypVar i) tau' -> getList tau'
_ -> []
showVarList l =
case l of
[] -> ""
[v] -> v
v:vs -> v ++ "," ++ showVarList vs
prependRelFunc :: [String] -> Typ -> String -> String
prependRelFunc names tau str =
case tau of
TVar (TypVar i) -> getAt names (i-1) ++ " " ++ str
_ -> str -- an elementary type (TBool, Int, TBrace). Relation is id and therefore dropped.
getTrackContWithFuncNames :: [String] -> TrackCont -> ([(String,Term)],String)
getTrackContWithFuncNames names trc =
let (_,l) = trc
(funcs,dis1,dis2) = getTrackContWithFuncNames' names l in
(funcs,dis1 ++ " $ t = " ++ dis2 ++ " $ t")
getTrackContWithFuncNames' :: [String] -> [(Term,Term)] -> ([(String,Term)],String,String)
getTrackContWithFuncNames' names l =
case l of
[] -> ([],"","")
[(t1,t2)] -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)
then ([], showTerm t1, showTerm t2)
else ([(head names,t1),(head (tail names),t2)], head names, head (tail names))
(t1,t2):xs -> if (isHead t1 || isFromLeft t1 || isFromRight t1 || isFst t1 || isSnd t1)
then
let (dis,str1,str2) = getTrackContWithFuncNames' names xs in
(dis, showTerm t1 ++ "." ++ str1, showTerm t2 ++ "." ++ str2)
else
let (dis,str1,str2) = getTrackContWithFuncNames' (drop 2 names) xs in
([(head names,t1),(head (tail names),t2)] ++ dis,str1 ++ " . " ++ head names, str2 ++ " . " ++ head (tail names))
showFuncNames :: [(String,Term)] -> String
showFuncNames funcNames =
case funcNames of
[] -> ""
(name,func):xs -> name ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNames xs
-- | renumbers term variables in a list of terms, such that different numbers stay different, but numbers are
-- decreased as far as possible
renumberVariables::[Term] -> [Term]
renumberVariables input =
let vars = nub (getNums input)
varNum = length vars
varMap = Map.fromList (zip vars [1..varNum]) in
renumber input varMap
where getNums terms =
case terms of
[] -> []
x:xs -> getVarNums x ++ getNums xs
renumber terms varMap =
case terms of
[] -> []
x:xs -> renumberVars x varMap : renumber xs varMap
-- | returns a list with all variable numbers used in a term.
getVarNums term =
case term of
Var (TermVar i) -> if i == 0 then [] else [i]
Abs (TermVar i) _ t' -> i:getVarNums t'
App t1 t2 -> getVarNums t1 ++ getVarNums t2
Nil _ -> []
Cons t1 t2 -> getVarNums t1 ++ getVarNums t2
LCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2
Bottom _ -> []
TAbs (TypVar i) t -> getVarNums t
Brace -> []
ICase t1 t2 -> getVarNums t1 ++ getVarNums t2
NCase t1 t2 -> getVarNums t1 ++ getVarNums t2
BCase t1 t2 -> getVarNums t1 ++ getVarNums t2
BoolCase t1 t2 -> getVarNums t1 ++ getVarNums t2
Pair t1 t2 -> getVarNums t1 ++ getVarNums t2
PCase t0 (TermVar i) (TermVar j) t1 -> getVarNums t0 ++ [i,j] ++ getVarNums t1
ECase t0 (TermVar i) t1 (TermVar j) t2 -> getVarNums t0 ++ [i,j] ++ getVarNums t1 ++ getVarNums t2
Left t -> getVarNums t
Right t -> getVarNums t
Zero -> []
Fls -> []
MJust t -> getVarNums t
MCase t0 (TermVar i) t2 -> getVarNums t0 ++ [i] ++ getVarNums t2
-- | renumbers term variables in a term as stated in the given map.
renumberVars term varMap =
case term of
Var (TermVar i) -> if i == 0 then term else Var (TermVar (varMap Map.! i))
Abs (TermVar i) tau t' -> Abs (TermVar (varMap Map.! i)) tau (renumberVars t' varMap)
App t1 t2 -> App (renumberVars t1 varMap) (renumberVars t2 varMap)
Nil _ -> term
Cons t1 t2 -> Cons (renumberVars t1 varMap) (renumberVars t2 varMap)
LCase t0 (TermVar i) t2 -> LCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)
Bottom _ -> term
TAbs tv t -> TAbs tv (renumberVars t varMap)
Brace -> Brace
ICase t1 t2 -> ICase (renumberVars t1 varMap) (renumberVars t2 varMap)
NCase t1 t2 -> NCase (renumberVars t1 varMap) (renumberVars t2 varMap)
BCase t1 t2 -> BCase (renumberVars t1 varMap) (renumberVars t2 varMap)
BoolCase t1 t2 -> BoolCase (renumberVars t1 varMap) (renumberVars t2 varMap)
Pair t1 t2 -> Pair (renumberVars t1 varMap) (renumberVars t2 varMap)
PCase t0 (TermVar i) (TermVar j) t1 -> PCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (TermVar (varMap Map.! j)) (renumberVars t1 varMap)
ECase t0 (TermVar i) t1 (TermVar j) t2 -> ECase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t1 varMap) (TermVar (varMap Map.! j)) (renumberVars t2 varMap)
Left t -> Left (renumberVars t varMap)
Right t -> Right (renumberVars t varMap)
Zero -> Zero
Fls -> Fls
MJust t1 -> MJust (renumberVars t1 varMap)
MCase t0 (TermVar i) t2 -> MCase (renumberVars t0 varMap) (TermVar (varMap Map.! i)) (renumberVars t2 varMap)
-- | takes a list with pairs (Int,Term), a list of function names and variable names and returns a list of (Int,String),
-- mapping each Int in the input list to a name out of the function or variable names
mapDisRelFuncsToNames :: [(Int,Term)] -> [String] -> [String] -> [(Int,String)]
mapDisRelFuncsToNames funcList funcs vars =
case funcList of
[] -> []
(i,t1):(j,t2):ls -> case t1 of
Abs _ _ _ -> (i,head funcs):(j,head.tail $ funcs):mapDisRelFuncsToNames ls (tail.tail $ funcs) vars
_ -> (i,head vars):(j,(head vars ++ "'")):mapDisRelFuncsToNames ls funcs (tail vars)
-- *show and print functions
-- |returns the number of and a string with the term variable environment entries
showTermCont :: TermCont -> String
showTermCont tc = "Number of entries: " ++ (show (Map.size tc)) ++ "\n\n" ++ (showTermContList (Map.toList tc))
-- |prints the number of and the term variable environments entries
printTermCont :: TermCont -> IO()
printTermCont tc = putStr (showTermCont tc)
-- |returns a string with the term context entries followed by "Nothing left.". It takes the context in form of a list.
showTermContList :: [(TermVar,((Term,Term),History))] -> String
showTermContList l = case l of
[] -> "Nothing left.\n"
(v,((x,x'),_)):xs -> (showTerm (Var v)) ++ " = " ++ (showTerm x) ++ "\n"
++ (showTerm (Var v)) ++ "' = " ++ (showTerm x') ++ "\n\n"
++ (showTermContList xs)
-- |prints the term with prefix "result term: "
printResult :: Term -> IO ()
printResult t = putStr ("result term: " ++ (showTerm t) ++ "\n\n")
-- |prints the typ with prefix "input type: "
printTyp :: Typ -> IO ()
printTyp t = putStr ("input type: " ++ showTyp t ++ "\n")
-- |returns a string with the \Gamma and \Sigma - context entries
showCont :: Cont -> String
showCont gamma = let showVars =
let vs = vars gamma in
case vs of
[] -> "]"
_ -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs))
showVarsStar =
let vs = varsStar gamma in
case vs of
[] -> "]"
_ -> foldr (\x -> \y -> x ++ "," ++ y) "\b]" (map (\v -> showTerm (Var (fst v)) ++ "::" ++ showTyp (snd v)) (vs))
in
"Cont = {vars = [" ++ showVars ++ ", varsStar = [" ++ showVarsStar ++ "}"
-- | pretty printer for Term.
-- All term variables are named by 'x' followed by a number.
showTerm :: Term -> String
showTerm t = showTermWithNames t Map.empty
-- | pretty printer for Term, where a map with special names for term variables can be given.
-- A term variable i with i in the map is is printed as the name provided for i in the map.
-- All other term variables are printed as 'x' followed by their number.
showTermWithNames :: Term -> (Map.Map Int String) -> String
showTermWithNames t m =
case t of
Var (TermVar i) -> if i == 0 then termName
else if Map.member i m then m Map.! i else 'x':(show i)
Abs v _ t' -> if isHead t then "head"
else if isFst t then "fst"
else if isSnd t then "snd"
else if isFromLeft t then "fromLeft"
else if isFromRight t then "fromRight"
else if isFromJust t then "fromJust"
else "(\\" ++ showTermWithNames (Var v) m ++ " -> " ++ showTermWithNames t' m ++ ")"
App t1 t2 -> "(" ++ showTermWithNames t1 m ++ " " ++ showTermWithNames t2 m ++ ")"
Nil _ -> "[]"
Cons t1 t2 -> case t2 of
Nil _ -> "[" ++ showTermWithNames t1 m ++ "]"
_ -> "(" ++ showTermWithNames t1 m ++ ":" ++ showTermWithNames t2 m ++ ")"
LCase t0 v2 t2 -> if isHeadApp t
then "(head " ++ showTermWithNames t0 m ++ ")"
else "(case " ++ showTermWithNames t0 m ++ " of {[" ++ showTermWithNames (Var v2) m ++ "] -> " ++ showTermWithNames t2 m ++"})"
Bottom _ -> "_|_"
TAbs (TypVar i) t -> showTermWithNames t m
Brace -> "()"
Fls -> "False"
ICase t1 t2 -> "(case " ++ showTermWithNames t1 m ++ " of {0 -> " ++ showTermWithNames t2 m ++ "})"
NCase t1 t2 -> "(case " ++ showTermWithNames t1 m ++ " of {0 -> " ++ showTermWithNames t2 m ++ "})"
BCase t1 t2 -> "(case " ++ showTermWithNames t1 m ++ " of {() -> " ++ showTermWithNames t2 m ++ "})"
BoolCase t1 t2 -> "(case " ++ showTermWithNames t1 m ++ " of {False -> " ++ showTermWithNames t2 m ++ "})"
Pair t1 t2 -> "(" ++ showTermWithNames t1 m ++ "," ++ showTermWithNames t2 m ++ ")"
PCase t0 v1 v2 t1 -> if isFstApp t
then "(fst " ++ showTermWithNames t0 m ++ ")"
else if isSndApp t
then "(snd " ++ showTermWithNames t0 m ++ ")"
else "(case " ++ showTermWithNames t0 m ++ " of {(" ++ showTermWithNames (Var v1) m ++ "," ++ showTermWithNames (Var v2) m ++ ") -> " ++ showTermWithNames t1 m ++ "})"
ECase t0 v1 t1 v2 t2 -> if isFromLeftApp t
then "(fromLeft " ++ showTermWithNames t0 m ++ ")"
else if isFromRightApp t
then "(fromRight " ++ showTermWithNames t0 m ++ ")"
else "(case " ++ showTermWithNames t0 m ++ " of {Left " ++ showTermWithNames (Var v1) m ++ " -> " ++ showTermWithNames t1 m ++ "})"
--right branch should be unnecessary, since pLusVal always returns Left-value and, if
--not fromLeft/fromRight, it should be always "case pLusVal of", and hence Left.
-- ; Right " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++ "})"
Left t -> "(Left " ++ showTermWithNames t m ++ ")"
Right t -> "(Right " ++ showTermWithNames t m ++ ")"
Zero -> "0"
MJust t1 -> "(Just " ++ showTermWithNames t1 m ++ ")"
MCase t0 v2 t2 -> if isFromJustApp t
then "(fromJust " ++ showTermWithNames t0 m ++ ")"
else "(case " ++ showTermWithNames t0 m ++ " of {Just " ++ showTermWithNames (Var v2) m ++ " -> " ++ showTermWithNames t2 m ++"})"
-- |pretty printer for Typ
showTyp :: Typ -> String
showTyp t = case t of
TVar (TypVar i) -> ('v':(show i))
Arrow t1 t2 -> "(" ++ showTyp t1 ++ " -> " ++ showTyp t2 ++ ")"
All v t1 -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1
AllStar v t1 -> "\\" ++ showTyp (TVar v) ++ "." ++ showTyp t1
List t1 -> "[" ++ showTyp t1 ++ "]"
Int -> "Int"
TNat -> "Nat"
TPair t1 t2 -> "(" ++ showTyp t1 ++ "," ++ showTyp t2 ++ ")"
TEither t1 t2 -> "(Either " ++ showTyp t1 ++ " " ++ showTyp t2 ++ ")"
TBrace -> "()"
TBool -> "Bool"
TMaybe t1 -> "(Maybe " ++ showTyp t1 ++ ")"
-- | returns a string with the disrelater entries with pretty printing
showTrackCont :: TrackCont -> String
showTrackCont trackCont =
let (ctau,trc) = trackCont in
showTrackCont' trc ++ "The type is: " ++ showTyp ctau ++ "\n\n"
showTrackCont' trc =
case trc of
[] -> ""
(x1,x2):xs -> (showTerm x1) ++ "\n" ++
(showTerm x2) ++ "\n\n" ++
showTrackCont' xs
-- | returns a string with the disrelater entries _without_ pretty printing
showRawTrackCont :: TrackCont -> String
showRawTrackCont trackCont =
let (ctau,trc) = trackCont in
showRawTrackCont' trc ++ "The type is: " ++ show ctau ++ "\n\n"
showRawTrackCont' trc =
case trc of
[] -> ""
(x1,x2):xs -> (show x1) ++ "\n" ++
(show x2) ++ "\n\n" ++
showRawTrackCont' xs
-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2
showTrackContApplication :: TrackCont -> Term -> String
showTrackContApplication tc t = showTrackContApplicationWithNames tc [] t
-- | applies the disrelater to the term and shows the simplified result as equation t1 = t2
-- Furthermore variables in the nameList are printed by the given name instead of 'x' and
-- there number.
showTrackContApplicationWithNames :: TrackCont ->[(Int,String)] -> Term -> String
showTrackContApplicationWithNames tc nameList t =
let (t1,t2) = applyTrackCont t tc
names = Map.fromList nameList in
showTermWithNames (simplifyTerm t1) names ++ " = " ++ showTermWithNames (simplifyTerm t2) names
-- | replaces the term variables with number i by the respective Term given in the (Int,Term)-list
-- and then applies the disrelater to the term and simplifies the result.
getTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> (Term,Term)
getTrackContApplicationSolved tc substs t =
let (t1',t2') = (applyTrackCont t tc)
(t1,t2) = (substAllInt t1' substs, substAllInt t2' substs) in
(simplifyTerm t1,simplifyTerm t2)
showTrackContApplicationSolved :: TrackCont -> [(Int,Term)] -> Term -> String
showTrackContApplicationSolved tc substs t =
let (t1,t2) = getTrackContApplicationSolved tc substs t in
showTerm t1 ++ " = " ++ showTerm t2
showFuncNamesInt :: [(Int,Term)] -> String
showFuncNamesInt funcNames =
case funcNames of
[] -> ""
(i,func):xs -> "x"++ show i ++ "\t = " ++ showTerm (head.renumberVariables $[simplifyTerm func]) ++ "\n" ++ showFuncNamesInt xs
-- *Set of functions for calling the algorithm
-- ** Monad features
-- | set the information the monad should return
makeTrackString :: String -> Cont -> Typ -> String
makeTrackString = trackRules
-- | return the applied rules with input contexts and type
trackAll :: String -> Cont -> Typ -> String
trackAll rule gamma tau = rule ++ ": " ++ showCont gamma ++ ", Type = " ++ showTyp tau
-- | return the applied rules
trackRules :: String -> Cont -> Typ -> String
trackRules rule gamma tau = rule