polyseq 0.1.1 → 0.1.2
raw patch · 8 files changed
+95/−62 lines, 8 files
Files
- README +6/−6
- polyseq.cabal +7/−8
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs +9/−2
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs +12/−1
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs +17/−17
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs +8/−1
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs +25/−15
- src/polyseq-cgi.hs +11/−12
README view
@@ -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
polyseq.cabal view
@@ -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
src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs view
@@ -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 ")"))
src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs view
@@ -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"
src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs view
@@ -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
src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs view
@@ -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 =
src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs view
@@ -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))
src/polyseq-cgi.hs view
@@ -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" ++