diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,41 @@ +The module polyseq-0.1.1 can be installed the following way: + +runhaskell Setup.hs configure --user +runhaskell Setup.hs build +runhaskell Setup.hs haddock +runhaskell Setup.hs install + +runhaskell Setup.hs haddock builds the documentation. +This step is not necessary. + +After installation the modules + PolySeq + PrettyPrint + TypeTranslator + TheoremGen + ParseTerm +are available. + +To start the webinterface do + +$ ./test.sh + +then it runs under http://localhost:8002/ + +The webinterface can also be found under + +http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi + +Enjoy. + + + +Acknowledgements. +================= + +Most of the webinterface' code (./src/polyseq-cgi.hs) and the script testcgi.py +are written by + +Joachim Breitner . + +Thanks! diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,5 @@ +#!/usr/bin/runhaskell + +import Distribution.Simple + +main = defaultMain diff --git a/polyseq.cabal b/polyseq.cabal new file mode 100644 --- /dev/null +++ b/polyseq.cabal @@ -0,0 +1,68 @@ +name: polyseq +version: 0.1.1 +license: PublicDomain +author: Daniel Seidel +maintainer: ds@iai.uni-bonn.de +synopsis: Counter examples to Free Theorems +description: + Given a term, this program calculates a set of optimal Free Theorems + that hold in a lambda calculus with Seq. It drops bottom-reflectingness + (or totality) restrictions when possible. + The theory behind the algorithm is described in the paper + \"Taming Selective Strictness\" (ATPS'09) by Daniel Seidel and Janis + Voigtländer. +category: Language +tested-with: GHC==6.8.2 +build-type: Simple +cabal-version: >= 1.2.3 + +extra-source-files: + src/Tests.hs + testcgi.py + test.sh + README + +library + build-depends: + array >= 0.1.0.0 + , bytestring >= 0.9.0.1 + , cgi >= 3001.1.5.1 + , containers >= 0.1.0.1 + , free-theorems >= 0.3.1 + , haskell-src >= 1.0.1.1 + , mtl >= 1.1.0.0 + , network >= 2.1.0.0 + , old-locale >= 1.0.0.0 + , old-time >= 1.0.0.0 + , parsec >= 3.0.0 + , pretty >= 1.0.0.0 + , utf8-string >= 0.3.1.1 + , xhtml >= 3000.0.2.1 + if impl(ghc >= 6.10) + build-depends: + base >= 4 + , syb >= 0.1.0.0 + else + build-depends: + base >= 1 && < 4 + exposed-modules: + Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq + Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint + Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator + Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen + Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm + other-modules: + Language.Haskell.FreeTheorems.Variations.PolySeq.M + Language.Haskell.FreeTheorems.Variations.PolySeq.TimeOut + Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver + Language.Haskell.FreeTheorems.Variations.PolySeq.Debug + Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight + Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg + hs-source-dirs: src + +executable polyseq.cgi + main-is: + polyseq-cgi.hs + hs-source-dirs: src + build-depends: + xhtml, cgi, utf8-string, free-theorems >= 0.3.1 diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs @@ -0,0 +1,314 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint(prettyConstraint) --only for debugging +import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax +import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon + ( collectOne + , substLabel + , getUsedLabels + , getUsedExtraLabels + , removeTrue + ) +import qualified Data.List as List +import qualified Data.Map as Map +import Data.Generics(everywhere, mkQ, mkT) +import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug +import Control.Monad(mplus) +import Data.Function + +--debuging stuff +trace2 = trace_ignore +trace = trace_ignore +trace1 = trace_ignore + +-- | simplifies the initial constraint and replaces variables in term and type +simplifyConstraint :: (Term,Typ,Constraint) -> (Term,Typ,Constraint) +simplifyConstraint (t',tau',c') = + let (t,tau,c) = simpConstraint (t',tau',c') in + (t,tau,checkContradiction (removeTrue c)) + +-- | subfunction of simplifyConstraint +simpConstraint :: (Term,Typ,Constraint) -> (Term,Typ,Constraint) +simpConstraint (t,tau,c') = + let c = removeUseless c' in + case findEq c of + Just (Eq l1 l2) -> trace "found Eq by findEq" (if l1 /= (LVal Epsilon) + then simpConstraint (substLabel l2 l1 t, substLabel l2 l1 tau, substLabel l2 l1 c) + else simpConstraint (substLabel l1 l2 t, substLabel l1 l2 tau, substLabel l1 l2 c)) + Nothing -> + case findGtEpsilon c of + Just (Leq _ l) -> trace "found GtEpsilon" (simpConstraint (substLabel (LVal Epsilon) l t, substLabel (LVal Epsilon) l tau, substLabel (LVal Epsilon) l c)) + Nothing -> + case findLtNbr c of + Just (Leq l _) -> trace "found LtNbr" (simpConstraint (substLabel (LVal Nbr) l t, substLabel (LVal Nbr) l tau, substLabel (LVal Nbr) l c)) + Nothing -> (t,tau,c) + +-- | removes Equations and InEquations, that are always fulfilled +removeUseless :: Constraint -> Constraint +removeUseless = everywhere (mkT rmUseLess) + +-- | generic function for removing trivial parts of the constraint +rmUseLess c = + case c of + Conj c1 c2 -> if useLess c1 then c2 else if useLess c2 then c1 else Conj c1 c2 + Impl (Eq (LVal (Epsilon)) (LVal (Epsilon))) c2 -> c2 + Impl (Eq (LVal (Nbr)) (LVal (Epsilon))) _ -> Tru + _ -> if useLess c then Tru else c + +-- | checks if a constraint is trivial +useLess c = + case c of + Eq c1 c2 -> if c1 == c2 then True else False + Leq _ (LVal (Epsilon)) -> True + Leq (LVal (Nbr)) _ -> True + Leq (LVar (LabVar i)) (LVar (LabVar j)) -> if i == j then True else False + _ -> False + +-- | returns the first Equation part of a constraint. Does not consider Equations in the body of an implication +findEq :: Constraint -> Maybe Constraint +findEq c = + case c of + Conj c1 c2 -> findEq c1 `mplus` findEq c2 + Eq _ _ -> Just c + _ -> Nothing + + +-- | returns the first "epsilon <= x" inequation part of a constraint. Does consider Equations in the body of an implication +findGtEpsilon = collectOne (mkQ Nothing fndGtEpsilon) + + +-- | generic function for findGtEpsilon +fndGtEpsilon :: Constraint -> Maybe Constraint +fndGtEpsilon c = + case c of + Leq (LVal (Epsilon)) _ -> Just c + _ -> Nothing + + +-- | returns the first "x <= nbr" inequation part of a constraint. Does consider Equations in the body of an implication +findLtNbr = collectOne (mkQ Nothing fndLtNbr) + + +-- | generic function for findLtNbr +fndLtNbr :: Constraint -> Maybe Constraint +fndLtNbr c = + case c of + Leq _ (LVal (Nbr)) -> Just c + _ -> Nothing + + +-- | returns Fls if the constraint is has no solution, otherwise the whole constraint +checkContradiction :: Constraint -> Constraint +checkContradiction c = + case fndContr c of + Just _ -> Fls + Nothing -> c + + +-- | auxiliar function, used in checkContradiction +fndContr :: Constraint -> Maybe Constraint +fndContr c = + case c of + Eq (LVal Nbr) (LVal Epsilon) -> Just c + Eq (LVal Epsilon) (LVal Nbr) -> Just c + Leq (LVal Epsilon) (LVal Nbr) -> Just c + Conj c1 c2 -> fndContr c1 `mplus` fndContr c2 + _ -> Nothing + + +-- | the first component of the returned tuple are the label variable numbers of the instantiated labels and the second +-- component is an array of all possible instantiation. For each instantiation the order matches the order of the +-- variables in the first component of the tuple. +solveConstraint :: Constraint -> ([Int],[[LabVal]]) +solveConstraint c = + let labConstr = getUsedLabels$c + vars = List.sort labConstr + vals = (map (snd.unzip.(Map.toAscList)) (slvConstr labConstr Map.empty c)) + in + trace1 ("solveConstraint produces\n"++ show vars ++ "with values\n" ++ show vals ++ "n") (vars,vals) + + +-- | Used by solveConstraint. Kind of breadth-first search for valid variable instantiations, aborting whenever a +-- partial instantiation leads to a contradiction in the constraint. +-- The map keeps track of all already instantiated variables and the list as first argument are the still free +-- variables. +-- The final result is a list of all possible complete (first argument is []) instantiations in form of a map +-- with variable number as key and concrete LabVal (Epsilon or Nbr) as value. +slvConstr :: [Int] -> Map.Map Int LabVal -> Constraint -> [Map.Map Int LabVal] +slvConstr vars map c = + case vars of + [] -> [map] + i:is -> let c1 = substLabel (LVal Nbr) (LVar (LabVar i)) c + c2 = substLabel (LVal Epsilon) (LVar (LabVar i)) c in + solve Nbr c1 ++ solve Epsilon c2 + where + solve lab c' = trace1 ("starting solve with " ++ show (prettyConstraint c')) ( + case reduceConstraint [(i,lab)] c' of + Nothing -> [] + Just (as,c'') -> + let map' = Map.union map (Map.fromList as) + asvars = fst.unzip$as + vars' = filter (flip notElem asvars) is + in + slvConstr vars' map' c'') + + +-- | takes a list of variable instantiations, allready done in the constraint, and the constraint. It adds further +-- variable instantiations, if possible, after reducing the constraint. +-- It is called recursively until no further instantiation is possible. +reduceConstraint :: [(Int,LabVal)] -> Constraint -> Maybe ([(Int,LabVal)],Constraint) +reduceConstraint as c' = + let c = removeTrue.removeUseless$c' in + if checkContradiction c == Fls then Nothing + else + case findEq c of + Just (Eq l1 l2) -> trace "found Eq by findEq"( + case l1 of + LVar (LabVar i) -> let LVal w = l2 in reduceConstraint ((i,w):as) (substLabel l2 l1 c) + LVal w -> let LVar (LabVar i) = l2 in reduceConstraint ((i,w):as) (substLabel l1 l2 c)) + Nothing -> + case findGtEpsilon c of + Just (Leq _ (LVar (LabVar i))) -> trace "found GtEpsilon" ( + reduceConstraint ((i,Epsilon):as) (substLabel (LVal Epsilon) (LVar (LabVar i)) c)) + Just c' -> error ("strange Constraint: " ++ show c' ++ "\n") + Nothing -> + case findLtNbr c of + Just (Leq (LVar (LabVar i)) _) -> trace "found LtNbr" (reduceConstraint ((i,Nbr):as) (substLabel (LVal Nbr) (LVar (LabVar i)) c)) + Just c' -> error ("strange Constraint: " ++ show c' ++ "\n") + Nothing -> case checkContradiction c of + Fls -> Nothing + _ -> Just (as,c) + + +-- | reduces the possible type instantiations to the variables that appear in the given term and type. +-- Also removing duplicates. +filterTermAndTyp :: Term -> Typ -> ([Int],[[LabVal]]) -> ([Int],[[LabVal]]) +filterTermAndTyp t tau res = + let labTerm = getUsedLabels t + labTermTyp = getUsedExtraLabels labTerm tau + (varList,resList) = filterLabVars labTermTyp res + in + (varList,List.nub resList) + + +-- | reduces the possible type instantiations to the variables that appear in the given type. +-- Also removing duplicates. +filterTyp :: Typ -> ([Int],[[LabVal]]) -> ([Int],[[LabVal]]) +filterTyp tau res = + let labTyp = getUsedLabels tau + (varList,resList) = filterLabVars labTyp res + in + (varList,List.nub resList) + + +-- | auxiliar function used by filterTermAndTyp and filterTyp +filterLabVars varList (vars,vals) = + case vars of + [] -> (vars,vals) + x:xs -> let (vrs, vls) = filterLabVars varList (xs,map tail vals) in + if x `elem` varList then + (x:vrs,zipWith (:) (map head vals) vls) + else (vrs,vls) + + +-- | takes a type and an array of instantiations (second component of the input tuple) for a subset of label +-- variables present in that type (first component of the input variable) and returns a list of types, +-- all partly instantiated by the one of the given instantiations. +makeTypes :: Typ -> ([Int],[[LabVal]]) -> [Typ] +makeTypes tau (vars, res) = + map (\x->substLabFromList tau (zip vars x)) res + where substLabFromList tau' l = + case l of + [] -> tau' + (i,val):xs -> substLabFromList (substLabel (LVal val) (LVar (LabVar i)) tau') xs + + +-- | takes a type and an array of instantiations (second component of the input tuple) for a subset of label +-- variables present in that type (first component of the input variable) and returns a list of types, +-- all completely instantiated and including one of the partial instantiation given, such that no other +-- complete instantiation, including one of the given partial instantiations as a subset of the logical relation. +-- as logical relation. +makeMinimalTypes :: Typ -> ([Int],[[LabVal]]) -> [Typ] +makeMinimalTypes tau (vars,valss) = + let (setVarOpt,unsetVarOpt) = List.partition (\x->(fst x) `elem` vars) (getOptimal tau) --should still be sorted + types = makeTypes tau (vars, + getMinimal (snd.unzip$ + (trace2 ("the setOptVars are: " ++ show setVarOpt ++ "\n\n") + setVarOpt)) + valss) + in + concat (map (getOptTypes unsetVarOpt) types) + where + --lessEqual. returns True if the logical relation of vals1 is a subset of the logical relation of vals2 + leq opts vals1 vals2 = --smaller is better -> opts has the smallest logical relation + case opts of + [] -> True + o:os -> let v1:vs1 = vals1 + v2:vs2 = vals2 + in + if o == Non then leq os vs1 vs2 + else if LVal v1 == o && LVal v2 /= o then False + else leq os vs1 vs2 + --notGreaterEqual, returns false if the logical relation of vals2 is a superset of the logical relation of vals1 + --Note: Since we have only a partial order leq /= notgeq. + notgeq opts vals1 vals2 = --smaller is better -> opts has the smallest logical relation + case opts of + [] -> False + o:os -> let v1:vs1 = vals1 + v2:vs2 = vals2 + in + if o == Non then notgeq os vs1 vs2 + else if LVal v2 == o && LVal v1 /= o then True + else notgeq os vs1 vs2 + -- sorts out the optimal (minimal logical relation) from all instantiations produced by the constraint + -- notice that this is for normally the instantiation of just a part of all label variables in the type. + getMinimal opts valss = + case valss of + [] -> [] + x:xs -> case List.find (leq opts x) xs of + Nothing -> x : getMinimal opts (filter (notgeq opts x) xs) + Just _ -> getMinimal opts xs + -- instantiates label variables with no previous restriction on it and returns a set of optimal instantiations. + getOptTypes opts typ = + case opts of + [] -> [typ] + (i,opt):xs -> case opt of + Non -> (getOptTypes xs (substLabel (LVal Epsilon) (LVar (LabVar i)) typ)) + ++ (getOptTypes xs (substLabel (LVal Nbr) (LVar (LabVar i)) typ)) + LVal Nbr -> getOptTypes xs (substLabel (LVal Nbr) (LVar (LabVar i)) typ) + LVal Epsilon -> getOptTypes xs (substLabel (LVal Epsilon) (LVar (LabVar i)) typ) + + +-- |returns the optimal (minimal logical relations) instantiation of a type in the form +-- LVal Epsilon, LVal Nbr or Non. Where Non stands for both, Epsilon and Nbr, would lead +-- to a minimal type. +-- Note that first there might be several optimal instantiations for the same label variable, which are +-- afterwards removed by resolveConflicts. This actually is the first time Non can appear. +getOptimal :: Typ -> [(Int,Label)] +getOptimal tau = resolveConflicts (List.sortBy (compare `on` fst) (getOpt True tau)) + where resolveConflicts l = + case l of + [] -> [] + [x] -> [x] + (i,l1):(j,l2):xs -> if i == j then + if l1 /= l2 then resolveConflicts ((i,Non):xs) + else resolveConflicts ((i,l1):xs) + else (i,l1):(resolveConflicts ((j,l2):xs)) + + +-- | returns the optimal instantiation for a label variable. It is always LVal Nbr or LVal Epsilon. +-- the first parameter marks if the logical relation has to be minimised (True) or maximised (False) +getOpt :: Bool -> Typ -> [(Int,Label)] +getOpt min tau = + case tau of + TVar _ -> [] + TArrow (LVar (LabVar i)) tau1 tau2 -> ((i,opt):(getOpt (not min) tau1)) ++ (getOpt min tau2) + TArrow _ tau1 tau2 -> (getOpt (not min) tau1) ++ (getOpt min tau2) + TAll (LVar (LabVar i)) _ tau1 -> (i,notOpt):(getOpt min tau1) + TAll _ _ tau1 -> getOpt min tau1 + TList tau1 -> getOpt min tau1 + TInt -> [] + TBool -> [] + where + opt = if min == False then LVal Nbr else LVal Epsilon + notOpt = if min == True then LVal Nbr else LVal Epsilon diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs @@ -0,0 +1,18 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.Debug + (trace_ignore, trace_toShell, + traceM_ignore, traceM_toShell) where + +import System.IO.Unsafe + +trace_ignore :: String -> a -> a +trace_ignore str a = a + +trace_toShell str a = if unsafePerformIO (putStr (str++"\n")) == () then a else a + +traceM_ignore :: (Monad m) => String -> m () +traceM_ignore str = return () + +traceM_toShell :: (Monad m) => String -> m () +traceM_toShell str = if unsafePerformIO (putStr (str++"\n")) == () then return () else return () + + diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs @@ -0,0 +1,165 @@ +{-OPTIONS_GHC -XFlexibleInstances -XFlexibleContexts -} +module Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight (highlight,highlightWith) where + +import Text.XHtml +import Text.PrettyPrint.HughesPJ hiding (char,style) +import Text.Parsec.String(Parser) +--import Text.Parsec.Token as P +import Text.Parsec.Combinator(manyTill, lookAhead, eof) +import Text.Parsec.Prim(ParsecT,Stream,(<|>),try,parse,getParserState) +import Text.ParserCombinators.Parsec.Char(oneOf,char,anyChar,string) +--import Text.ParserCombinators.Parsec.Language(emptyDef) +import Text.Parsec + +import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug + +--traceM = traceM_toShell +--traceM = traceM_ignore +--traceState = do state <- getParserState; +-- traceM ("with the Parser state " ++ show (stateInput state) ++ "\n"); + +-- data What = Keyword String +-- | BottomReflectionRestriction + +-- data HighLightMode = Color String +-- | BgColor String + +makeHglt :: String -> (Html -> Html) +makeHglt mode = thespan![thestyle (mode)] + + +highlightWith :: String -> String -> Html +highlightWith hgltMode str = + let hglt = makeHglt hgltMode + res = parse (highlt hglt) "" str in + case res of + Left err -> toHtml (show err) + Right html -> html + +highlight :: String -> Html +highlight = highlightWith "background-color:yellow;color:red" + +-- myLanguage = +-- emptyDef +-- { opStart = oneOf "<" +-- , opLetter = oneOf "<=>" +-- , reservedOpNames = ["<=>"] +-- -- , reservedNames = ["total", "bottom-reflecting"] +-- , caseSensitive = True +-- } + +-- lexer = P.makeTokenParser emptyDef + +-- par = P.parens lexer +-- resOp = P.reservedOp lexer + + +highlt :: (Html -> Html) -> Parser Html +highlt hglt = + parEOF + <|> do{ str <- ((try (parsBotRefRestriction hglt)) <|> (parAnything hglt)); +-- traceM "highlt: from braced entry"; +-- traceState; +-- traceM "enter highlt ..."; +-- traceState; + str' <- highlt hglt; +-- traceM "exit highlt ..."; +-- traceState; + return (str+++str') +-- return str + } + <|> try (do{ str <- keyword; +-- traceM "highlt: read keyword"; +-- traceState; + str' <- highlt hglt; +-- traceState; + return ((hglt << (toHtml str)) +++ str') + }) + <|> do{ str <- anythingElse; +-- traceM "highlt: from anythingElse"; +-- traceState; + str' <- highlt hglt; + return (str+++str') + } + +tillEndOfBrace hglt = + do{ char ')'; + return (toHtml "") + } + <|> do{ str <- ((try (parsBotRefRestriction hglt)) <|> (parAnything hglt)); +-- traceM "tillEndOfBrace: braced entry"; +-- traceState; + str' <- tillEndOfBrace hglt; + return (str+++str') +-- return str + } + <|> try (do{ str <- keyword; +-- traceM "tillEndOfBrace: read keyword"; +-- traceState; + str' <- tillEndOfBrace hglt; + return ((hglt << (toHtml str)) +++ str') + }) + <|> do{ str <- anythingElse; +-- traceM "tillEndOfBrace anythingElse"; +-- traceState; + str' <- tillEndOfBrace hglt; + return (str+++str') + } + +parEOF :: Parser Html +parEOF = do{ eof; + return (toHtml "") + } + + +strEOF :: Parser String +strEOF = do{ eof; + return "" + } + + +parAnything :: (Html -> Html) -> Parser Html +parAnything hglt = + do{ char '('; + str <- tillEndOfBrace hglt; +-- traceState; + return ("("+++str+++")") + } + + +parsBotRefRestriction :: (Html -> Html) -> Parser Html +parsBotRefRestriction hglt = + do{ restrict <- do { char '('; +-- traceState; + char '('; + s1 <- tillEndOfBrace hglt; +-- traceState; + spaces; + string "<=>"; + spaces; +-- traceState; + char '('; + s2 <- tillEndOfBrace hglt; +-- traceState; + char ')'; +-- traceM "read highlight restriction."; +-- traceState; + return ("("+++s1+++")"+++" <=> "+++"("+++s2+++")") + }; + return (hglt << ("("+++restrict+++")")) + } + +brace = (lookAhead (string "(")) <|> (lookAhead (string ")")) + +anythingElse :: Parser Html +anythingElse = + do{ str <- manyTill anyChar (brace <|> (try keywordCheck) <|> strEOF); +-- traceM "read anythingElse"; +-- traceState; + return (toHtml str) + } + +keywordCheck = (lookAhead (string "total")) <|> (lookAhead (string "bottom-reflecting")) +keyword = (try (string "total")) <|> (string "bottom-reflecting") + + diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs @@ -0,0 +1,23 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.M (M,runM,newLab,abort,track) where + +type State = (Int,[String]) + +data M a = M (State -> [(a,State)]) + +instance Monad M where + return a = M (\s -> [(a,s)]) + M m >>= k = M (\s -> concatMap (\(a,s') -> case k a of M l -> l s') (m s)) + +runM :: M a -> Maybe (a, [String]) +runM (M m) = case m (1,[]) of + [] -> Nothing + ((a,(_,ls)):_) -> Just (a,reverse ls) + +newLab :: M Int +newLab = M(\(i,ls) -> [(i,(i+1,ls))]) + +abort :: M a +abort = M (\s -> []) + +track :: String -> M () +track l = M (\(i,ls) -> [((),(i,l:ls))]) diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs @@ -0,0 +1,354 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm) where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax + +import Control.Monad.Identity +import Data.List ( nub ) + +import Text.Parsec +import Text.Parsec.Expr +import Text.Parsec.String(Parser) +import Text.Parsec.Combinator +import Text.Parsec.Token as P +import Text.Parsec.Language(emptyDef) +import Text.ParserCombinators.Parsec.Prim(getParserState) +import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug + +-- | ParseCont keeps track of all currently available term and type variable during parsing a term +data ParseCont = ParseCont { pcTVar :: [String], pcVar :: [String] } deriving (Show, Eq) + +emptyParseCont = ParseCont [] [] + +-- * debug functions, are set to a function defined in Debug, (un)comment the definitions as necessary for debug + +--trace1 = trace_toShell +trace1 = trace_ignore +--traceM = traceM_toShell +traceM = traceM_ignore +--traceM1 = traceM_toShell +traceM1 = traceM_ignore +--traceState = do state <- getParserState; +-- traceM ("with the Parser state " ++ show (stateInput state) ++ "\n"); +traceState = return () + +-- * auxiliar functions +insertTVarPC (ParseCont tv v) str = + if elem str tv + then ParseCont tv v + else ParseCont (str:tv) (filter (\x->x /= str) v) + +checkOrInsertTVarState (ParseCont tv v) str = + if elem str tv + then return () + else modifyState (str:) + +-- checkTVarPC (ParseCont tv v) str = +-- if elem str tv +-- then return () +-- else parserZero "unbound type variable" + +insertVarPC (ParseCont tv v) str = + if elem str v + then ParseCont tv v + else ParseCont (filter (\x->x /= str) tv) (str:v) + +checkVarPC (ParseCont tv v) str = + if elem str v + then return () + else parserZero "unbound term variable" + +myLanguage = + emptyDef + { identStart = letter + , identLetter = alphaNum <|> oneOf "'" + , opStart = oneOf ":\\-+=" + , opLetter = oneOf ":\\->+=_" + , reservedOpNames = [":","::","=","->","\\","/\\","_","+"] + , reservedNames = ["forall","Int", "Bool", "if", "then", "else", "True", "False", "case","of","let!","in","fix","let","seq","undefined"] + , caseSensitive = True + } + +lexer = P.makeTokenParser myLanguage + +int = P.integer lexer +res = P.reserved lexer +resOp = P.reservedOp lexer +whiteSpc = P.whiteSpace lexer +lexe = P.lexeme lexer +par = P.parens lexer +brack = P.brackets lexer +symb = P.symbol lexer +ident = P.identifier lexer +brace = P.braces lexer +nat = P.natural lexer + + +type MyState = [String] + + +termParser :: ParseCont -> ParsecT String MyState Identity Term +termParser pc = do + whiteSpc + x <- (term1 pc) + eof + return x + +term1 :: ParseCont -> ParsecT String MyState Identity Term +term1 pc = do + do{ traceM "Enter term1\n"; + traceState; + do{ resOp "\\"; + str <- ident; + resOp "::"; + tau <- typ pc; + symb "."; + t <- term1 (insertVarPC pc str); + return (Abs (TermVar str) tau t) + } + <|> do{ resOp "/\\"; + str <- ident; + symb "."; + traceM1 ("scanned /\\ " ++ str ++ ".\n"); + t <- (term1 (insertTVarPC pc str)); + return (TAbs (TypVar str) t) + } + <|> do{ res "case"; + t <- (term1 pc); + res "of"; + symb "{"; + (do{ symb "["; + symb "]"; + resOp "->"; + t1 <- (term1 pc); + resOp ";"; + v1 <- ident; + resOp ":"; + v2 <- ident; + resOp "->"; + t2 <- term1 (insertVarPC (insertVarPC pc v1) v2); + symb "}"; + return (LCase t t1 (TermVar v1) (TermVar v2) t2) + } + <|> do{ res "True"; + resOp "->"; + t1 <- term1 pc; + resOp ";"; + res "False"; + resOp "->"; + t2 <- term1 pc; + symb "}"; + return (BCase t t1 t2) + } + <|> do{ res "False"; + resOp "->"; + t1 <- term1 pc; + resOp ";"; + res "True"; + resOp "->"; + t2 <- term1 pc; + symb "}"; + return (BCase t t2 t1) + }) + } + <|> ifParser pc + <|> do{ res "let!"; + v <- ident; + let pc' = insertVarPC pc v in + do{ resOp "="; + t <- (term1 pc'); + res "in"; + t' <- (term1 pc'); + return (LSeq (TermVar v) t t') + } + } + <|> do{ res "let"; + v <- ident; + let pc' = insertVarPC pc v in + do{ resOp "="; + t <- (term1 pc'); + res "in"; + t' <- (term1 pc'); + return (Let (TermVar v) t t') + } + } + <|> term2 pc + } + +ifParser :: ParseCont -> ParsecT String MyState Identity Term +ifParser pc = do + res "if" + t <- term1 pc + res "then" + t1 <- term1 pc + res "else" + t2 <- term1 pc + return (BCase t t1 t2) + +term2 :: ParseCont -> ParsecT String MyState Identity Term +term2 pc = + do{ traceM "Enter term2\n"; + traceState; + l <- sepBy1 (term3 pc) (resOp ":"); + traceState; + trace1 "returned from term2" + return (foldr1 (\x y -> Cons x y) l) + } + +term3 :: ParseCont -> ParsecT String MyState Identity Term +term3 pc = do{traceM "Enter term3\n"; + traceState; + h <- (do{ i<-int; + return (I (fromInteger i)) + } + <|> term4 pc); + l <- (do{ resOp "+"; + sepBy (term4 pc) (resOp "+") + } + <|> return []); + trace1 "returned from term3" + return (foldl1 (\x y -> Add x y) (h:l)) + } + +term4 :: ParseCont -> ParsecT String MyState Identity Term +term4 pc = + do{ traceM "Enter term4\n"; + traceState; + do{ t <- (term6 pc); + traceM ("term4 scanned term6: " ++ show t ++ "\n"); + args <- many (term5 pc); + traceM ("term4 with args = " ++ show (length args) ++ "\n"); + traceM ("where the arguments are " ++ show (map ($(Var (TermVar "fake"))) args) ++ "\n"); + let t' = ((foldl (.) id (reverse args))$t) in + do{ traceM ("term4 is " ++ show t' ++ "\n"); + return t' + } + } + } + +term5 pc = + do{traceM "Enter term5\n"; + traceState; + do{ t' <- term7 pc; + traceM ("returned in term5 with " ++ show t' ++ "\n"); + state <- getParserState; + traceM ("with the Parser state " ++ show (stateInput state) ++ "\n"); + return (\t -> App t t') + } + } + +term6 pc = + do{ traceM "Enter term6\n"; + traceState; + do{ res "fix"; + t <- (term7 pc) "the previous \"fix\" to be applied to an argument"; + return (Fix t) + } + <|> do{ res "seq"; + t <- (term7 pc) "the previous \"seq\" to be applied to two arguments"; + t'<- (term7 pc) "the previous \"seq\" to be applied to two arguments"; + return (Seq t t') + } + <|> term7 pc + } + + +term7 pc = + do{ traceM "Enter term7\n"; + traceState; + t <- term8 pc; + do{ resOp "_"; + tau <- brace (typ pc); + return (TApp t tau) + } + <|> return t + } + +term8 pc = + do{ traceM "Enter term8\n"; + traceState; + par (term1 pc) + <|> do{ tl <- brack (sepBy (term1 pc) (symb ",")); + trace1 "scanned [t1, ..., tn], trying : ...\n" resOp "_"; + tau <- trace1 "scanned :, trying typ\n" (brace (typ pc)); + return (foldr (\x y -> Cons x y) (Nil tau) tl) + } + <|> do{ i <- (lexe nat); + return (I (fromInteger i)) + } + <|> do{ str <- ident; + traceM ("term8: identified " ++ str ++ "\n"); + checkVarPC pc str; + traceM ("term8: Variable, checkVarPC successful\n"); + return (Var (TermVar str)) + } + <|> do{ res "True"; + return T + } + <|> do{ res "False"; + return F; + } + <|> do{ res "undefined"; + resOp "_" "undefined has to be instantiated to a type."; + tau <- brace (typ pc); + return (Fix (Abs (TermVar "x") tau (Var (TermVar "x")))) + } + <|> do{ res "fix"; + parserZero "the previous \"fix\" to be immediately applied to a term and not to be the argument to a function" + } + <|> do{ res "seq"; + parserZero "the previous \"seq\" to be immediately applied to two terms and not to be the argument to a function" + } + } + +typ :: ParseCont -> ParsecT String MyState Identity Typ +typ pc = buildExpressionParser tableTyp (typ1 pc) + +tableTyp = [ [op "->" (\x y -> TArrow Non x y) AssocRight] ] + where op s f assoc = Infix (do{ resOp s; return f} "operator") assoc + +typ1 :: ParseCont -> ParsecT String MyState Identity Typ +typ1 pc = + do{ + traceM "Enter typ1\n"; + traceState; + par (typ pc) + <|> do{ symb "["; + tau <- (typ pc); + symb "]"; + return (TList tau) + } + <|> do{ str <- ident; + traceM ("identifier TypeVariable " ++ str); + checkOrInsertTVarState pc str; + traceM "checked TVar identifier."; + return (TVar (TypVar str)) + } + <|> do{ res "Int"; + return TInt + } + <|> do{ res "forall"; + str <- ident; + resOp "."; + tau <- (typ (insertTVarPC pc str)); + return (TAll Non (TypVar str) tau) + } + <|> do{ res "Bool"; + return TBool + } + } + +cTermParser = termParser emptyParseCont +testParser = termParser (ParseCont ["a","b"] ["f","g"]) + +addFreeTVar :: [String] -> Term -> Term +addFreeTVar [] t = t +addFreeTVar (x:xs) t = addFreeTVar xs (TAbs (TypVar x) t) + +addTVarParser :: ParseCont -> ParsecT String MyState Identity Term +addTVarParser pc = do + res <- termParser pc + tvars <- getState + return (addFreeTVar (nub tvars) res) + +parseTerm :: String -> Either ParseError Term +parseTerm = runP (addTVarParser emptyParseCont) [] "user input term" diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs @@ -0,0 +1,129 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg +import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon(removeTrue,getEquals,instantiateWithEpsilon) +import Language.Haskell.FreeTheorems.Variations.PolySeq.M +import Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen +import Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver +import Text.PrettyPrint(renderStyle,Style(..),Mode(..),(<+>),text) +import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint +import Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm) +import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight +import Text.XHtml hiding(text) + +--polySeq :: Term -> Maybe (Constraint,Typ) +polySeq = runM.algPolySeq + +shellStyle = Style PageMode 80 0.2 +webStyle = Style PageMode 80 0.2 + +--getItT :: Term -> IO() +getItT t = + case polySeq t of + Just ((t',c,tau),_) -> do{ putStr "The term: "; + putStr (renderStyle shellStyle (prettyMarkedTerm t')); + putStr "\n\nThe Constraint: "; + putStr (renderStyle shellStyle (prettyConstraint (removeTrue c))); + putStr "\n\nWith the equations: "; + putStr (show (getEquals c)); + putStr "\n\nThe Type:"; + putStr (renderStyle shellStyle (prettyMarkedTyp tau)); + putStr "\n\nUsed Label Variables: "; + putStr "\n\n newSimplify:\n\n"; + let (ts,taus,cs) = simplifyConstraint (t',tau,c) in + do{putStr "The term: "; + putStr (renderStyle shellStyle (prettyMarkedTerm ts)); + putStr "\n\nThe Constraint: "; + putStr (renderStyle shellStyle (prettyConstraint cs)); + putStr "\n\nThe Type:"; + putStr (renderStyle shellStyle (prettyMarkedTyp taus)); + putStr "\n\nWhich optimal would be:"; + putStr (show (getOpt True taus)); + putStr "\n\nThat means, it is typable to the following concrete Types\n\n"; + putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n"++y) "" + (makeTypes taus ((filterTyp taus).solveConstraint$cs))); + putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n"; + putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n\n"++y) "" + (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs))); + }; + putStr "\n\n"; + } + Nothing -> putStr "Term is not typable at all.\n" + +--getItTRaw :: Term -> IO() +getItTRaw t = + case polySeq t of + Just ((t',c,tau),_) -> do{ putStr "The term: "; + putStr (renderStyle shellStyle (prettyMarkedTerm t')); + putStr "\n\nThe Constraint: "; + putStr (renderStyle shellStyle (prettyConstraint (removeTrue c))); + putStr "\n\nWith the equations: "; + putStr (show (getEquals c)); + putStr "\n\nThe Type:"; + putStr (renderStyle shellStyle (prettyMarkedTyp tau)); + putStr "\n\nUsed Label Variables: "; + putStr "\n\n newSimplify:\n\n"; + let (ts,taus,cs) = simplifyConstraint (t',tau,c) in + do{putStr "The term: "; + putStr (renderStyle shellStyle (prettyMarkedTerm ts)); + putStr "\n\nThe Constraint: "; + putStr (renderStyle shellStyle (prettyConstraint cs)); + putStr "\n\nThe Type:"; + putStr (renderStyle shellStyle (prettyMarkedTyp taus)); + putStr "\n\nWhich optimal would be:"; + putStr (show (getOpt True taus)); + putStr "\n\nThat means, it is typable to the following concrete Types\n\n"; + putStr (foldr (\x y->(show x)++"\n\n"++y) "" + (makeTypes taus ((filterTyp taus).solveConstraint$cs))); + putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n"; + putStr (foldr (\x y->(show x)++"\n\n"++y) "" + (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs))); + }; + putStr "\n\n"; + } + Nothing -> putStr "Term is not typable at all.\n" + +getIt str = + case parseTerm str of + Left err -> putStr (show err) + Right t -> getItT t + +getItRaw str = + case parseTerm str of + Left err -> putStr (show err) + Right t -> getItTRaw t + + +-- termstring (ErrType,ErrMsg) (Term ,Constraint,Typ ,NormalFT, [(MinTyp,FT)]) +getForWebInterface :: String -> Either (String, String) (String,String, String,String, [(String,String)]) +getForWebInterface termstr = + case parseTerm termstr of + Left err -> Left ("ParseError",(show err)) + Right t -> case polySeq t of + Just ((t'',c',tau'),_) -> + let (t',tau,c) = simplifyConstraint (t'',tau',c') + minTypes = makeMinimalTypes tau ((filterTyp tau).solveConstraint$c) + optFT = map (fromRight.makeFTFullFunc) minTypes + minTypFTList = zip (map ((renderStyle webStyle).prettyMarkedTyp) minTypes) optFT + normalFT = fromRight.makeFTFullFunc.instantiateWithEpsilon$ tau' + termStr = renderStyle webStyle (text "t =" <+> prettyUnMarkedTerm t') + constStr = renderStyle webStyle (prettyConstraint c) + tauStr = renderStyle webStyle (prettyMarkedTyp tau) + in + Right (termStr, constStr, tauStr,normalFT,minTypFTList) + Nothing -> Left ("NotTypable",renderStyle webStyle (prettyUnMarkedTerm t)) + where fromRight (Right x) = x + + + +testTerm = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs }))" + +test = case getForWebInterface testTerm of + Left _ -> putStr "shit happened." + Right (t,c,tau,nft,l) -> do{ putStr "\n\nThe normal Theorem:\n\n"; + putStr nft; + putStr "\n\nThe highlighted version:\n\n"; + putStr (show.highlight$nft); + } + +foldl'' = "/\\a./\\b.\\c :: a -> b -> a.let! c' = c in fix ( \\h :: a -> [b] -> a.\\n :: a.\\ys :: [b].let c'' = c n in case ys of {[] -> n; x:xs -> let! xs' = xs in let! x' = x in let n' = c'' x' in h n' xs' })" diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs @@ -0,0 +1,174 @@ +-- | contains all rule systems +module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg (algPolySeq) where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.M +import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon +import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax + +-- * Typing algorithm + +polySeqTyping :: Cont -> Term -> M (Constraint,Typ) +polySeqTyping gamma t = + case t of + Var v -> do{ tau <- getTypVarInCont gamma v; + superType tau + } + Abs v tau t' -> do{ (c1,tau2) <- polySeqTyping (addTermVar gamma (v,tau)) t'; + (c2,tau1) <- subType tau; + lab <- makeLabel; + return (Conj c1 c2, TArrow lab tau1 tau2) + } + App t1 t2 -> do{ (c1,tau12) <- polySeqTyping gamma t1; + (tau1,tau2)<- getArrowComps tau12; + (c2,tau1') <- polySeqTyping gamma t2; + c3 <- makeEqual tau1 tau1'; + return (Conj (Conj c1 c2) c3,tau2) + } + TAbs tv t' -> do{ lv <- makeLabel; + (c,tau) <- polySeqTyping (addTypVar gamma (tv,lv)) t'; + return (c,TAll lv tv tau) + } + TApp t' tau -> do{ c1 <- seqable gamma tau; + (c2,atau) <- polySeqTyping gamma t'; + (lab,tv,tau1)<- getAllComps atau; + (c3,tau3) <- superType (substTyp tau1 tau tv); + return (Conj (Conj c2 c3) (Impl (Eq lab (LVal Epsilon)) c1),tau3) + } + Nil tau -> do{ (c,tau') <- superType tau; + return (c,TList tau') + } + Cons t1 t2 -> do{ (c1,tau) <- polySeqTyping gamma t1; + (c2,ltau)<- polySeqTyping gamma t2; + tau' <- getElemType ltau; + c3 <- makeEqual tau tau'; + return (Conj (Conj c1 c2) c3,TList tau) + } + LCase t1 t2 v1 v2 t3 -> + do{ (c1,ltau)<- polySeqTyping gamma t1; + tau1 <- getElemType ltau; + (c2,tau2)<- polySeqTyping gamma t2; + (c3,tau2')<- polySeqTyping (addTermVar (addTermVar gamma (v1,tau1)) (v2,ltau)) t3; + c4 <- makeEqual tau2 tau2'; + return (Conj (Conj (Conj c1 c2) c3) c4,tau2) + } + Fix t' -> do{ (c1,tau) <- polySeqTyping gamma t'; + (tau1,tau2)<- getArrowComps tau; + c2 <- makeEqual tau1 tau2; + return (Conj c1 c2,tau1) + } + LSeq v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1; + c2 <- seqable gamma tau1; + (c3,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2; + return (Conj (Conj c1 c2) c3, tau2) + } + Let v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1; + (c2,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2; + return (Conj c1 c2, tau2) + } + Seq t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1; + c2 <- seqable gamma tau1; + (c3,tau2) <- polySeqTyping gamma t2; + return (Conj (Conj c1 c2) c3, tau2) + } + I _ -> return (Tru,TInt) + Add t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1; + isInt tau1; + (c2,tau2) <- polySeqTyping gamma t2; + isInt tau2; + return (Conj c1 c2,TInt) + } + T -> return (Tru,TBool) + F -> return (Tru,TBool) + BCase t1 t2 t3 -> do{ (_,tau1) <- polySeqTyping gamma t1; --the constraint will always be Tru + isBool tau1; + (c2,tau2) <- polySeqTyping gamma t2; + (c3,tau3) <- polySeqTyping gamma t3; + c4 <- makeEqual tau2 tau3; + return (Conj (Conj c2 c3) c4,tau2) + } + +-- * seqable check + +seqable :: Cont -> Typ -> M Constraint +seqable gamma tau = + case tau of + TVar tv -> do{ lab <- getLabTVar gamma tv; + return (Eq (lab) (LVal Epsilon)) + } + TArrow lab _ _ -> return (Eq lab (LVal Epsilon)) + TAll _ tv tau' -> seqable (addTypVar gamma (tv,LVal Epsilon)) tau' + TList _ -> return Tru + TInt -> return Tru + TBool -> return Tru + +-- * typ comparison + +superType :: Typ -> M (Constraint,Typ) +superType tau = + case tau of + TVar tv -> return (Tru,tau) + TArrow lab tau1 tau2 -> do{ (c1,tau) <- subType tau1; + (c2,tau')<- superType tau2; + lab' <- makeLabel; + return (Conj (Conj c1 c2) (Leq lab' lab),TArrow lab' tau tau') + } + TAll lab tv tau -> do{ (c,tau') <- superType tau; + lab' <- makeLabel; + return (Conj c (Leq lab lab'), TAll lab' tv tau') + } + TList tau -> do{ (c,tau') <- superType tau; + return (c,TList tau') + } + TInt -> return (Tru,TInt) + TBool -> return (Tru,TBool) + +subType :: Typ -> M (Constraint,Typ) +subType tau = + case tau of + TVar tv -> return (Tru,tau) + TArrow lab tau1 tau2 -> do{ (c1,tau) <- superType tau1; + (c2,tau')<- subType tau2; + lab' <- makeLabel; + return (Conj (Conj c1 c2) (Leq lab lab'),TArrow lab' tau tau') + } + TAll lab tv tau -> do{ (c,tau') <- subType tau; + lab' <- makeLabel; + return (Conj c (Leq lab' lab), TAll lab' tv tau') + } + TList tau -> do{ (c,tau') <- subType tau; + return (c,TList tau') + } + TInt -> return (Tru,TInt) + TBool -> return (Tru,TBool) + +makeEqual :: Typ -> Typ -> M Constraint +makeEqual tau tau' = + case tau of + TVar tv -> if tau' == TVar tv then return Tru else abort + TArrow lab tau1 tau2 -> case tau' of + TArrow lab' tau1' tau2' -> do{ c1 <- makeEqual tau1 tau1'; + c2 <- makeEqual tau2 tau2'; + return (Conj (Conj c1 c2) (Eq lab lab')) + } + _ -> abort + TAll lab tv tau1 -> case tau' of + TAll lab' tv' tau1' -> if tv == tv' + then + do{ c <- makeEqual tau1 tau1'; + return (Conj c (Eq lab lab')) + } + else abort + _ -> abort + TList tau1 -> case tau' of + TList tau1' -> makeEqual tau1 tau1' + _ -> abort + TInt -> if tau' == TInt then return Tru else abort + TBool -> if tau' == TBool then return Tru else abort + +-- * main function + +algPolySeq :: Term -> M (Term,Constraint,Typ) +algPolySeq t = do{ t' <- annotate t; + (c,tau) <- polySeqTyping emptyCont t'; + return (t',c,tau) + } diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs @@ -0,0 +1,76 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint (prettyMarkedTyp, prettyUnMarkedTyp, prettyMarkedTerm, prettyUnMarkedTerm, prettyConstraint, prettyLabel) where + +import Text.PrettyPrint + +import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax + +prettyLabel :: Label -> Doc +prettyLabel l = + case l of + LVar (LabVar i) -> text ("v" ++ show i) + LVal Nbr -> text "n" + LVal Epsilon -> text "e" + Non -> text "?" + + +prettyMarkedTyp = prettyTyp True +prettyUnMarkedTyp = prettyTyp False + +prettyTyp :: Bool -> Typ -> Doc +prettyTyp mark tau = + case tau of + TVar (TypVar s) -> text s + TArrow l tau1 tau2 -> parens (fsep [prettyTyp mark tau1, if mark then text "->^" <> prettyLabel l else text "->", + (prettyTyp mark tau2)]) + TAll l (TypVar s) tau' -> parens (fsep [text "forall" <> if mark then text "^" <> (prettyLabel l) else empty, + text s <> text ".", prettyTyp mark tau']) + TList tau' -> brackets (prettyTyp mark tau') + TInt -> text "Int" + TBool -> text "Bool" + + +prettyMarkedTerm = prettyTerm True +prettyUnMarkedTerm = prettyTerm False + +prettyTerm :: Bool -> Term -> Doc +prettyTerm mark t = + case t of + Var (TermVar s) -> text s + Abs (TermVar s) tau t' -> parens (fsep [text ("\\" ++ s ++ "::") <> prettyTyp mark tau <> text ".", + prettyTerm mark t']) + App t1 t2 -> parens (fsep [prettyTerm mark t1,prettyTerm mark t2]) + TAbs (TypVar s) t' -> parens (fsep [text ("/\\" ++ s ++ "."),prettyTerm mark t']) + TApp t' tau -> prettyTerm mark t' <> text "_" <> braces (prettyTyp mark tau) + Nil tau -> text "[]_" <> braces (prettyTyp mark tau) + Cons t1 t2 -> parens (prettyTerm mark t1 <> text ":" <> prettyTerm mark t2) + LCase t1 t2 (TermVar s1) (TermVar s2) t3 + -> parens (fsep [text "case" <+> prettyTerm mark t1<+> text "of {[] ->", + prettyTerm mark t2 <> semi, text (s1 ++ ":" ++ s2 ++ " ->"), + prettyTerm mark t3 <> text "}"]) + Fix t' -> case t' of + Abs x tau (Var y) -> if x == y + then text "undefined_" <> braces (prettyTyp mark tau) + else parens (text "fix" <+> prettyTerm mark t') + _ -> parens (text "fix" <+> prettyTerm mark t') + LSeq (TermVar s) t1 t2 -> parens (fsep [text "let!", text s, equals, prettyTerm mark t1, text "in", + prettyTerm mark t2]) + Let (TermVar s) t1 t2 -> parens (fsep [text "let", text s, equals, prettyTerm mark t1, + text "in",prettyTerm mark t2]) + Seq t1 t2 -> parens (text "seq" <+> prettyTerm mark t1 <+> prettyTerm mark t2) + I i -> text (show i) + Add t1 t2 -> parens (fsep [prettyTerm mark t1, text "+", prettyTerm mark t2]) + T -> text "True" + F -> text "False" + BCase t1 t2 t3 -> parens (fsep [text "if", prettyTerm mark t1, text "then", prettyTerm mark t2, + text "else", prettyTerm mark t3]) + + +prettyConstraint :: Constraint -> Doc +prettyConstraint c = + case c of + Conj c1 c2 -> fsep [prettyConstraint c1, text " ^ ", prettyConstraint c2] + Impl c1 c2 -> parens (fsep [prettyConstraint c1, text " -> ", prettyConstraint c2]) + Leq l1 l2 -> parens (fsep [prettyLabel l1, text " <= ", prettyLabel l2]) + Eq l1 l2 -> parens (fsep [prettyLabel l1, text " == ", prettyLabel l2]) + Tru -> text "T" + Fls -> text "F" diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs @@ -0,0 +1,64 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc) where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator(translate) + +import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP +import Language.Haskell.FreeTheorems + ( runChecks + , check + , prettyTheorem + , asCompleteTheorem + , interpret + , unfoldLifts + , prettyUnfoldedLift + , LanguageSubset(SubsetWithSeq) + , TheoremType(EquationalTheorem) + , PrettyTheoremOption({-OmitTypeInstantiations,-}OmitLanguageSubsets) + , specialise + , relationVariables + ) + +import Language.Haskell.FreeTheorems.BasicSyntax(Signature(..),Identifier(..)) +import Language.Haskell.FreeTheorems.ValidSyntax(ValidSignature(..)) +import Text.PrettyPrint.HughesPJ (render) + + +--makeFTFull :: Typ -> Either String String +makeFTFull tau = + let sig = ValidSignature (Signature (Ident "t") (translate tau)) + bool = "data Bool = False | True" + parse_input = unlines [bool] + (ds,es) = runChecks (parse parse_input >>= check) + in if null es + then case interpret ds (SubsetWithSeq EquationalTheorem) sig of + Nothing -> Left "interpret returned nothing" + Just i -> let i' = foldl specialise i (relationVariables i) in + Right $ render (prettyTheorem [OmitLanguageSubsets] (asCompleteTheorem i)) ++ + case unfoldLifts ds i of + [] -> "" + ls -> (if length ls == 1 + then "\n\nThe structural lifting occuring therein is defined as follows:\n\n " + else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++ + unlines (map (render . prettyUnfoldedLift [OmitLanguageSubsets]) ls) + else Left (unlines (map render es)) + + +--makeFTFullFunc :: Typ -> Either String String +makeFTFullFunc tau = + let sig = ValidSignature (Signature (Ident "t") (translate tau)) + bool = "data Bool = False | True" + parse_input = unlines [bool] + (ds,es) = runChecks (parse parse_input >>= check) + in if null es + then case interpret ds (SubsetWithSeq EquationalTheorem) sig of + Nothing -> Left "interpret returned nothing" + Just i -> let i' = foldl specialise i (relationVariables i) in + Right $ render (prettyTheorem [OmitLanguageSubsets] (asCompleteTheorem i')) ++ + case unfoldLifts ds i' of + [] -> "" + ls -> (if length ls == 1 + then "\n\nThe structural lifting occuring therein is defined as follows:\n\n " + else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++ + unlines (map (render . prettyUnfoldedLift [OmitLanguageSubsets]) ls) + else Left (unlines (map render es)) + diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TimeOut.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TimeOut.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TimeOut.hs @@ -0,0 +1,35 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.TimeOut where + +import Control.Concurrent +--import Distribution.Simple.Utils +watchdogIO :: (Show a) => + Int -- milliseconds + -> IO a -- expensive computation + -> IO a -- cheap computation + -> IO a +watchdogIO millis expensive cheap = + do mvar <- newEmptyMVar + tid1 <- forkIO $ do x <- expensive + (if (length (show x) >= 0) then x else x) `seq` putMVar mvar (Just x) + tid2 <- forkIO $ do threadDelay (millis * 1000) + putMVar mvar Nothing + res <- takeMVar mvar + case res of + Just x -> + do --info ("EXPENSIVE was used") + killThread tid2 --`catch` (\e -> warn (show e)) + return x + Nothing -> + do --info ("WATCHDOG after " ++ show millis ++ " milliseconds") + killThread tid1 --`catch` (\e -> warn (show e)) + cheap + +watchdog1 :: (Show a) => Int -> a -> IO (Maybe a) +watchdog1 millis x = + watchdogIO millis (return (Just x)) + (return Nothing) + +watchdog2 :: (Show a) => Int -> a -> IO (Maybe a) +watchdog2 millis x = + watchdogIO millis (x `seq` return (Just x)) + (return Nothing) diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs @@ -0,0 +1,26 @@ +module Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax + ( Typ(..) + , Label(..) + , LabVal(..) + , TypVar(..) + ) +import Language.Haskell.FreeTheorems.Syntax + ( TypeExpression(..) + , Identifier(..) + , TypeVariable(..) + , TypeConstructor(..) + ) + +translate :: Typ -> TypeExpression +translate tau = + case tau of + TVar (TypVar s) -> TypeVar (TV (Ident s)) + TArrow (LVal Epsilon) tau1 tau2 -> TypeFun (translate tau1) (translate tau2) + TArrow (LVal Nbr ) tau1 tau2 -> TypeFunLab (translate tau1) (translate tau2) + TAll (LVal Epsilon) (TypVar s) tau1 -> TypeAbs (TV (Ident s)) [] (translate tau1) + TAll (LVal Nbr ) (TypVar s) tau1 -> TypeAbsLab (TV (Ident s)) [] (translate tau1) + TList tau1 -> TypeCon ConList [translate tau1] + TInt -> TypeCon ConInt [] + TBool -> TypeCon (Con (Ident "Bool")) [] diff --git a/src/Tests.hs b/src/Tests.hs new file mode 100644 --- /dev/null +++ b/src/Tests.hs @@ -0,0 +1,24 @@ +-- | contains terms and other useful things, imports PolySeq +module Tests where + +import PolySeq +import Syntax + +term1 = TAbs (TypVar "a") + (Abs (TermVar "x") (TArrow Non (TArrow Non (TVar (TypVar "a")) TInt) TInt) + (Abs (TermVar "y") (TArrow Non (TVar (TypVar "a")) TInt) + (App (Var (TermVar "x")) (Var (TermVar "y"))))) + +testInput1 = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []::[a]; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs}))" + +testInput2 = "\\f::((Int->Int)->Int)->Int.\\g::(Int->Int)->Int.\\c::Int->Int. f g + g c + (f (\\h::Int->Int.let! h' = h in 3))" +testTyp1 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a"))))) + +testTyp2 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a"))))) + +testTyp3 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a"))))) + +testTyp4 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Nbr) (TVar (TypVar "a")) TBool) (TArrow (LVal Nbr) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a"))))) + + +testTerm = "/\a.\p::a->Bool.p:[]_{a->Bool}" diff --git a/src/polyseq-cgi.hs b/src/polyseq-cgi.hs new file mode 100644 --- /dev/null +++ b/src/polyseq-cgi.hs @@ -0,0 +1,150 @@ +module Main where + +import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq (getForWebInterface) +import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight(highlight) + +import Network.CGI +import Data.ByteString.Lazy.UTF8 (fromString) +import Text.XHtml +import Control.Monad +import Data.Maybe +import Text.PrettyPrint.HughesPJ (render) +import qualified Data.Map as M +import Data.Generics +import Language.Haskell.FreeTheorems.Variations.PolySeq.TimeOut + +askDiv v e = maindiv << ( + p << ("To get a quick impression about the influence of strictness, toggle the let expressions between strict " +++ tt << "let!" +++ " and non-strict " +++ tt << "let" +++ ".") +++ + p << ( "You can also enter your own term, " +++ + "e.g. " +++ primHtmlChar "ldquo" +++ tt << "/\\a.\\x::a.\\f::forall b.b->Int.seq f_{Int} (f_{a} x)" +++ primHtmlChar "rdquo" +++ "." +++ + p << (textarea ! [name "term", cols "80", rows "11"] << v +++ + submit "submit" "Generate" )) +++ + e + ) + + +askTypeForm = askDiv (--"/\\a./\\b.\n" ++ + "\\c :: a -> b -> a.\n" ++ + " let c' = c in\n" ++ + " fix ( \\h :: a -> [b] -> a.\n" ++ + " \\n :: a. \\ys :: [b].\n" ++ + " let! c'' = c' n in\n" ++ + " case ys of {\n" ++ + " [] -> n;\n" ++ + " x:xs -> let! xs' = xs in\n" ++ + " let! x' = x in\n" ++ + " let n' = c'' x' in\n" ++ + " h n' xs' })") noHtml + +-- ("/\\a.\\p::a->Bool.\n" ++ +-- " let p' = p in \n" ++ +-- " (fix \n" ++ +-- " (\\f::[a]->[a]. \\ys::[a].\n" ++ +-- " case ys of {[] -> []_{a};\n" ++ +-- " x:xs-> let! x' = x in \n" ++ +-- " if p x then\n" ++ +-- " (let! xs' = xs in x):(f xs)\n" ++ +-- " else f xs\n" ++ +-- " }))") noHtml + +--generateResult :: (MonadIO t) => [Char] -> t Html +generateResult termStr = + do run_algorithm <- run_algorithmM + return(askDiv termStr noHtml +++ + maindiv << (case run_algorithm of + Left (err,msg) -> p << case err of + "TimeOut" -> msg +++ "" + "ParseError" -> "A parse error occured:" +++ pre << msg + "NotTypable" -> "The term" +++ pre << tt << msg +++ "is not typable." + Right result -> + let (term,constraint,typ,normalFT,minTypeFTList) = result + l = length minTypeFTList + in + p << "The term" +++ + pre << tt << term +++ +-- p << "can be typed to " +++ tt << typ +++ +-- p << "if the constraint " +++ +-- pre << tt << constraint +++ "is satisfied, which leads to the optimal type(s)" +++ + p << (if l > 1 + then "can be typed to the optimal types" +++ + (if l == 2 + then printTypeAndFT (head minTypeFTList) +++ "and" + else (foldr (\x y -> y +++ (printTypeAndFT x) +++ ",") (""+++"") (init $ minTypeFTList)) +++ " and") + +++ printTypeAndFT (last minTypeFTList) + else "can be typed to the optimal type" +++ + printTypeAndFT (head minTypeFTList)) + +++ + p << "The normal free theorem for the type without marks would be:" +++ + pre << tt << (highlight normalFT))) + where run_algorithmM = do res <- liftIO (watchdog2 3000 (getForWebInterface termStr)) + return (case res of + Nothing -> Left ("TimeOut","Unfortunately the generator the type generator timed out. Time was restricted to 3 seconds.") + Just x -> x) + printTypeAndFT (tau,ft) = p << pre << tt << tau +++ + p << "with the free theorem" +++ + pre << tt << (highlight ft) + +main = runCGI (handleErrors cgiMain) + +--cgiMain :: CGI CGIResult +cgiMain = do + setHeader "Content-type" "text/xml; charset=UTF-8" + + mTypeStr <- getInput "term" + + + let content = case mTypeStr of + Nothing -> return askTypeForm + Just typeStr -> generateResult typeStr + con <- content + outputFPS $ fromString $ showHtml $ + header ( + thetitle << "Taming Selective Strictness" +++ + style ! [ thetype "text/css" ] << cdata cssStyle + ) +++ + body ( form ! [method "POST", action "#"] << ( + thediv ! [theclass "top"] << ( + thespan ! [theclass "title"] << "Haskell" +++ + thespan ! [theclass "subtitle"] << "Taming Selective Strictness" + ) +++ + maindiv ( p << ("This tool allows you to experiment with the method described in the paper " + +++ primHtmlChar "ldquo" + +++ hotlink "http://www.iai.uni-bonn.de/~jv/atps09.pdf" + << "Taming Selective Strictness" + +++ primHtmlChar "rdquo" + +++ " (ATPS'09) by Daniel Seidel and " + +++ hotlink "http://www.iai.uni-bonn.de/~jv" + << (toHtml "Janis Voigtländer") + +++ ".")) +++ + con +++ + maindiv ( p << ("The source code is available for " +++ +-- hotlink "http://www-ps.iai.uni-bonn.de/downloads/polyseq.tar.gz" << "download" +++ + hotlink "http://hackage.haskell.org/package/polyseq" << "download" +++ + ".") +++ + p << ("© 2009 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ ">") + ) + )) + +maindiv = thediv ! [theclass "main"] + +cdata s = primHtml ("") + +cssStyle = unlines + [ "body { padding:0px; margin: 0px; }" + , "div.top { margin:0px; padding:10px; margin-bottom:20px;" + , " background-color:#efefef;" + , " border-bottom:1px solid black; }" + , "span.title { font-size:xx-large; font-weight:bold; }" + , "span.subtitle { padding-left:30px; font-size:large; }" + , "div.main { border:1px dotted black;" + , " padding:10px; margin:10px; }" + , "div.submain { padding:10px; margin:11px; }" + , "p.subtitle { font-size:large; font-weight:bold; }" + , "input.type { font-family:monospace; }" + , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }" + , "span.mono { font-family:monospace; }" + , "pre { margin:10px; margin-left:20px; padding:10px;" + , " border:1px solid black; }" + , "textarea { margin:10px; margin-left:20px; padding:10px; }" + , "p { text-align:justify; }" + ] diff --git a/test.sh b/test.sh new file mode 100644 --- /dev/null +++ b/test.sh @@ -0,0 +1,2 @@ +#!/bin/bash +./testcgi.py ./dist/build/polyseq.cgi/polyseq.cgi diff --git a/testcgi.py b/testcgi.py new file mode 100644 --- /dev/null +++ b/testcgi.py @@ -0,0 +1,18 @@ +#!/usr/bin/python + +from BaseHTTPServer import HTTPServer +from CGIHTTPServer import CGIHTTPRequestHandler +import sys + +class MyRequestHandler(CGIHTTPRequestHandler): + def is_cgi(self): + self.cgi_info = ("","") + return True + + def translate_path(self, path): + return sys.argv[1] + + +server_address = ('', 8002) +http = HTTPServer(server_address, MyRequestHandler) +http.serve_forever()