polyseq (empty) → 0.1.1
raw patch · 18 files changed
+1686/−0 lines, 18 filesdep +arraydep +basedep +bytestringsetup-changed
Dependencies added: array, base, bytestring, cgi, containers, free-theorems, haskell-src, mtl, network, old-locale, old-time, parsec, pretty, syb, utf8-string, xhtml
Files
- README +41/−0
- Setup.hs +5/−0
- polyseq.cabal +68/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs +314/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs +18/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs +165/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs +23/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs +354/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs +129/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs +174/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs +76/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs +64/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/TimeOut.hs +35/−0
- src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs +26/−0
- src/Tests.hs +24/−0
- src/polyseq-cgi.hs +150/−0
- test.sh +2/−0
- testcgi.py +18/−0
+ README view
@@ -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 <mail@joachim-breitner.de>.++Thanks!
+ Setup.hs view
@@ -0,0 +1,5 @@+#!/usr/bin/runhaskell++import Distribution.Simple++main = defaultMain
+ polyseq.cabal view
@@ -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
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/ConstraintSolver.hs view
@@ -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
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/Debug.hs view
@@ -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 ()++
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/Highlight.hs view
@@ -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")+ +
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/M.hs view
@@ -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))])
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/Parser/ParseTerm.hs view
@@ -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"
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeq.hs view
@@ -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' })"
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/PolySeqAlg.hs view
@@ -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)+ }
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/PrettyPrint.hs view
@@ -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"
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/TheoremGen.hs view
@@ -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))+
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/TimeOut.hs view
@@ -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)
+ src/Language/Haskell/FreeTheorems/Variations/PolySeq/TypeTranslator.hs view
@@ -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")) []
+ src/Tests.hs view
@@ -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}"
+ src/polyseq-cgi.hs view
@@ -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 ("<![CDATA[\n"++ s ++ "\n]]>")++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; }"+ ]
+ test.sh view
@@ -0,0 +1,2 @@+#!/bin/bash+./testcgi.py ./dist/build/polyseq.cgi/polyseq.cgi
+ testcgi.py view
@@ -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()