diff --git a/README b/README --- a/README +++ b/README @@ -1,4 +1,4 @@ -The module polyseq-0.1.1 can be installed the following way: +The module polyseq-0.1.2 can be installed the following way: runhaskell Setup.hs configure --user runhaskell Setup.hs build @@ -9,11 +9,11 @@ This step is not necessary. After installation the modules - PolySeq - PrettyPrint - TypeTranslator - TheoremGen - ParseTerm + 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 are available. To start the webinterface do diff --git a/polyseq.cabal b/polyseq.cabal --- a/polyseq.cabal +++ b/polyseq.cabal @@ -1,16 +1,15 @@ name: polyseq -version: 0.1.1 +version: 0.1.2 license: PublicDomain author: Daniel Seidel maintainer: ds@iai.uni-bonn.de -synopsis: Counter examples to Free Theorems +synopsis: Taming Selective Strictness 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. + Given a term, this program calculates a set of \"optimal\" free theorems + that hold in a lambda calculus with selective strictness. It omits + totality (in general, bottom-reflection) and other restrictions when + possible. The underlying theory 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 diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs --- a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs @@ -144,10 +144,17 @@ char ')'; -- traceM "read highlight restriction."; -- traceState; - return ("("+++s1+++")"+++" <=> "+++"("+++s2+++")") + return (if (showHtml s1) == (showHtml s2) then noHtml else("("+++s1+++")"+++" <=> "+++"("+++s2+++")")) }; - return (hglt << ("("+++restrict+++")")) + ret <- if isNoHtml restrict then removeAnds else (return (toHtml "("+++restrict+++")")); + return (hglt << ret) } + +removeAnds :: Parser Html +removeAnds = do spaces + try (string "&&") + spaces + return noHtml brace = (lookAhead (string "(")) <|> (lookAhead (string ")")) diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs --- a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs @@ -1,4 +1,4 @@ -module Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm) where +module Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag) where import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax @@ -352,3 +352,14 @@ parseTerm :: String -> Either ParseError Term parseTerm = runP (addTVarParser emptyParseCont) [] "user input term" + +-- the additional Bool is a flag to see if type abstraction is explicit (Bool = True) + +addTVarParserWithFlag :: ParseCont -> ParsecT String MyState Identity (Term,Bool) +addTVarParserWithFlag pc = do + res <- termParser pc + tvars <- getState + return (if tvars == [] then (res, True) else (addFreeTVar (nub tvars) res, False)) + +parseTermWithFlag :: String -> Either ParseError (Term,Bool) +parseTermWithFlag = runP (addTVarParserWithFlag emptyParseCont) [] "user input term" diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs --- a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs @@ -7,7 +7,7 @@ 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.Parser.ParseTerm(parseTerm, parseTermWithFlag) import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight import Text.XHtml hiding(text) @@ -95,23 +95,23 @@ -- termstring (ErrType,ErrMsg) (Term ,Constraint,Typ ,NormalFT, [(MinTyp,FT)]) -getForWebInterface :: String -> Either (String, String) (String,String, String,String, [(String,String)]) +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)) + case parseTermWithFlag termstr of + Left err -> Left ("ParseError",(show err)) + Right (t,flag) -> 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.(makeFTFullFuncWithFlag flag)) minTypes + minTypFTList = zip (map ((renderStyle webStyle).prettyMarkedTyp) minTypes) optFT + normalFT = fromRight.(makeFTFullFuncWithFlag flag).instantiateWithEpsilon$ tau' + termStr = renderStyle webStyle (text "t =" <+> prettyUnMarkedTerm (adjustTypAbstraction flag 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 diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs --- a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs @@ -1,4 +1,4 @@ -module Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint (prettyMarkedTyp, prettyUnMarkedTyp, prettyMarkedTerm, prettyUnMarkedTerm, prettyConstraint, prettyLabel) where +module Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint (prettyMarkedTyp, prettyUnMarkedTyp, prettyMarkedTerm, prettyUnMarkedTerm, prettyConstraint, prettyLabel, adjustTypAbstraction) where import Text.PrettyPrint @@ -31,6 +31,13 @@ prettyMarkedTerm = prettyTerm True prettyUnMarkedTerm = prettyTerm False + +adjustTypAbstraction :: Bool -> Term -> Term +adjustTypAbstraction True t = t +adjustTypAbstraction _ t = + case t of + TAbs _ t' -> adjustTypAbstraction False t' + _ -> t prettyTerm :: Bool -> Term -> Doc prettyTerm mark t = diff --git a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs --- a/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs +++ b/src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs @@ -1,4 +1,4 @@ -module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc) where +module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc, makeFTFullWithFlag, makeFTFullFuncWithFlag) where import Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator(translate) @@ -7,13 +7,14 @@ ( runChecks , check , prettyTheorem + , asTheorem , asCompleteTheorem , interpret , unfoldLifts , prettyUnfoldedLift , LanguageSubset(SubsetWithSeq) , TheoremType(EquationalTheorem) - , PrettyTheoremOption({-OmitTypeInstantiations,-}OmitLanguageSubsets) + , PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets) , specialise , relationVariables ) @@ -24,41 +25,50 @@ --makeFTFull :: Typ -> Either String String -makeFTFull tau = - let sig = ValidSignature (Signature (Ident "t") (translate tau)) - bool = "data Bool = False | True" +makeFTFull = makeFTFullWithFlag True + +--makeFTFullWithFlag :: Typ -> Either String String +makeFTFullWithFlag flag 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) + (ds,es) = runChecks (parse parse_input >>= check) + thmopts = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations] 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)) ++ + Right $ render (prettyTheorem thmopts (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) + unlines (map (render . prettyUnfoldedLift thmopts) 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" + +--makeFTFullFuncWithFlag :: Typ -> Either String String +makeFTFullFunc = makeFTFullFuncWithFlag True + +--makeFTFullFunc :: Bool -> Typ -> Either String String +makeFTFullFuncWithFlag flag 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) + (ds,es) = runChecks (parse parse_input >>= check) + thmopts = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations] 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')) ++ + Right $ render (prettyTheorem thmopts (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) + unlines (map (render . prettyUnfoldedLift thmopts) ls) else Left (unlines (map render es)) diff --git a/src/polyseq-cgi.hs b/src/polyseq-cgi.hs --- a/src/polyseq-cgi.hs +++ b/src/polyseq-cgi.hs @@ -23,18 +23,17 @@ ) -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 +askTypeForm = askDiv ("\\c :: a -> b -> a.\n" ++ + " let c' = c in\n" ++ + " fix (\\h :: a -> [b] -> a.\n" ++ + " \\n :: a. \\ys :: [b].\n" ++ + " let! z = 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' n x' in\n" ++ + " h n' xs'})") noHtml -- ("/\\a.\\p::a->Bool.\n" ++ -- " let p' = p in \n" ++