Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
---=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-- -- -- -- A TOOL FOR RELATIONAL PROGRAMMERS -- -- --------------------------------- -- -- -- -- Graham Hutton Erik Meijer Ed Voermans -- -- Chalmers University Utrecht University Eindhoven University -- -- graham@cs.chalmers.se erik@cs.ruu.nl wsinedv@win.tue.nl -- -- -- -- 21st January, 1994 -- -- -- ---=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-- -- Type definitions -------------------------------------------------- type Parser a b = [a] -> [(b,[a])] data Term = Cell String -- primitives | Id -- identity | Top -- top | Exl -- project left | Exr -- project right | Wok Term -- reciprocation | Cap Term Term -- intersection | Comp Term Term -- composition | Split Term Term -- split (derived op) | Prod Term Term -- product (derived op) | Dom Term -- domain (derived op) | Rng Term -- range (derived op) type Subst = Int -> Name type Net = ([Node],Name,Name) type Node = (String,Name,Name) data Name = Basic Int | Pair Name Name -- Equality definitions ---------------------------------------------- nameeq :: Name -> Name -> Bool termeq :: Term -> Term -> Bool nodeeq :: Node -> Node -> Bool nameeq (Basic a) (Basic b) = a == b nameeq (Pair x y) (Pair x' y') = (x `nameeq` x') && (y `nameeq` y') nameeq other1 other2 = False termeq (Cell x) (Cell y) = x == y termeq Id Id = True termeq Top Top = True termeq Exl Exl = True termeq Exr Exr = True termeq (Wok x) (Wok y) = termeq x y termeq (Dom x) (Dom y) = termeq x y termeq (Rng x) (Rng y) = termeq x y termeq (a `Cap` b) (c `Cap` d) = (termeq a c) && (termeq b d) termeq (a `Comp` b) (c `Comp` d) = (termeq a c) && (termeq b d) termeq (a `Split` b) (c `Split` d) = (termeq a c) && (termeq b d) termeq (a `Prod` b) (c `Prod` d) = (termeq a c) && (termeq b d) termeq a b = False nodeeq (r,x,y) (r',x',y') = (r==r') && (x==x') && (y==y') instance Eq Name where (==) = nameeq instance Eq Term where (==) = termeq instance Eq Node where (==) = nodeeq -- Parsing combinators ----------------------------------------------- -- -- Taken from Graham Hutton, Higher-order functions for parsing, -- Journal of Functional Programming, 2(3):323-343, July 1992. infixr `next` infixr `xnext` infixr `nextx` infixr `alt` infixr `using` infixr `return` succeed :: b -> Parser a b fail :: Parser a b satisfy :: (a -> Bool) -> Parser a a literal :: Eq a => a -> Parser a a string :: Eq a => [a] -> Parser a [a] alt :: Parser a b -> Parser a b -> Parser a b next :: Parser a b -> Parser a c -> Parser a (b,c) opt :: Parser a b -> b -> Parser a b many :: Parser a b -> Parser a [b] some :: Parser a b -> Parser a [b] using :: Parser a b -> (b -> c) -> Parser a c xnext :: Parser a b -> Parser a c -> Parser a c nextx :: Parser a b -> Parser a c -> Parser a b return :: Parser a b -> c -> Parser a c number :: Parser Char [Char] word :: Parser Char [Char] anyof :: (a -> Parser b c) -> [a] -> Parser b c sepby :: String -> Parser Char a -> Parser Char [a] nibble :: Parser Char a -> Parser Char a symbol :: [Char] -> Parser Char [Char] succeed v inp = [(v,inp)] fail inp = [] satisfy p [] = fail [] satisfy p (x:xs) = succeed x xs , p x = fail xs , otherwise literal x = satisfy (==x) string [] = succeed [] string (x:xs) = (literal x `next` string xs) `using` uncurry (:) (p1 `alt` p2) inp = p1 inp ++ p2 inp (p1 `next` p2) inp = [((v1,v2),out2) | (v1,out1) <- p1 inp, (v2,out2) <- p2 out1] (p `opt` v) inp = [(v',out)] where (v',out) = head ((p `alt` succeed v) inp) many p = ((p `next` many p) `using` uncurry (:)) `opt` [] some p = (p `next` many p) `using` uncurry (:) (p `using` f) inp = [(f v,out) | (v,out) <- p inp] p1 `xnext` p2 = (p1 `next` p2) `using` snd p1 `nextx` p2 = (p1 `next` p2) `using` fst p `return` v = p `using` (const v) where const x y = x number = some (satisfy digit) where digit x = ('0' <= x) && (x <= '9') word = some (satisfy letter) where letter x = ('A' <= x) && (x <= 'Z') anyof p = foldr (alt.p) fail sepby xs p = (p `next` ((symbol xs `xnext` sepby xs p) `opt` [])) `using` (uncurry (:)) nibble p = white `xnext` p `nextx` white where white = many (anyof literal " \t\n") symbol = nibble.string -- Parsers for equations and terms ----------------------------------- equation :: String -> (Term,(String,Term)) eqtn :: Parser Char (Term,(String,Term)) termify :: String -> Term term :: Parser Char Term equation xs = parse xs eqtn eqtn = term `next` (symbol "=" `alt` symbol "<=" `alt` symbol ">=") `next` term termify xs = parse xs term term = (sepby "n" term2) `using` foldr1 Cap term2 = (sepby ";" term3) `using` foldr1 Comp term3 = (sepby "x" term4) `using` foldr1 Prod term4 = ((symbol "dom" `xnext` term4) `using` Dom) `alt` ((symbol "rng" `xnext` term4) `using` Rng) `alt` ((term5 `nextx` symbol "'") `using` Wok) `alt` term5 term5 = (symbol "id" `return` Id) `alt` (symbol "top" `return` Top) `alt` (symbol "p0" `return` Exl) `alt` (symbol "p1" `return` Exr) `alt` (word `using` Cell) `alt` ((symbol "<" `xnext` term `next` symbol "," `xnext` term `nextx` symbol ">") `using` uncurry Split) `alt` (symbol "(" `xnext` term `nextx` symbol ")") parse xs p = case (take 1 (p xs)) of [] -> error "Can't parse input string" [(x,[])] -> x [(x,ys)] -> error ("Can't parse " ++ ys) -- Pretty printing --------------------------------------------------- showterm :: Term -> String showname :: Name -> String shownet :: Net -> String showterm (Cell xs) = xs showterm Id = "id" showterm Top = "top" showterm Exl = "p0" showterm Exr = "p1" showterm (Wok t) = showterm t ++ "'" showterm (Cap t t') = bracket (showterm t ++ " n " ++ showterm t') showterm (Comp t t') = bracket (showterm t ++ " ; " ++ showterm t') showterm (Split t t') = "<" ++ showterm t ++ "," ++ showterm t' ++ ">" showterm (Prod t t') = bracket (showterm t ++ " x " ++ showterm t') showterm (Dom t) = "dom " ++ showterm t showterm (Rng t) = "rng " ++ showterm t showname (Basic n) = show n showname (Pair x y) = bracket (showname x ++ "," ++showname y) shownet (ns,x,y) = bracket ("["++layout (map f ns) ++"]," ++ showname x ++","++ showname y) where f (r,a,b) = bracket (r ++"," ++ showname a++","++showname b) layout [] = [] layout [a] = a layout (a:as) = a ++"," ++ layout as bracket xs = "(" ++ xs ++ ")" -- Normalisation of names and nets ----------------------------------- norm :: Name -> Name normnet :: Net -> Net vars :: Name -> [Int] netvars :: Net -> [Int] norm n = app (zip (nub (vars n)) [0..]) n normnet n = (map f ns, app s x, app s y) where (ns,x,y) = n s = zip (netvars n) [0..] f (r,a,b) = (r, app s a, app s b) vars (Basic a) = [a] vars (Pair x y) = (vars x) ++ (vars y) netvars (ns,x,y) = nub (concat (map f ns) ++ vars x ++ vars y) where f (r,a,b) = vars a ++ vars b lookup a xs = head [b | (a',b) <- xs, a==a'] app xs (Basic a) = Basic (lookup a xs) app xs (Pair x y) = Pair (app xs x) (app xs y) -- Unification of names ---------------------------------------------- ident :: Subst delta :: Int -> Name -> Subst apply :: Subst -> Name -> Name compose :: Subst -> Subst -> Subst extend :: Subst -> Int -> Name -> Subst unify :: Subst -> (Name,Name) -> Subst ident = Basic delta a x a' = if a==a' then x else Basic a' apply s (Basic a) = s a apply s (Pair x y) = Pair (apply s x) (apply s y) compose s s' a = apply s (s' a) extend s a x = s, x == Basic a = error "occurs-check failed in unification", elem a (vars x) = compose (delta a x) s, otherwise unify s (Basic a, x) = if s a == Basic a then extend s a (apply s x) else unify s (s a, x) unify s (x, Basic a) = unify s (Basic a, x) unify s (Pair x y, Pair x' y') = unify (unify s (x,x')) (y,y') -- Network compiler -------------------------------------------------- compile :: Term -> Net compile' :: Int -> Term -> (Int,Net) applynet :: Subst -> Net -> Net compile t = f (snd (compile' 0 t)) where f (ns,x,y) = normnet (nub ns,x,y) compile' a (Cell xs) = (a+2,([(xs,Basic a,Basic (a+1))],Basic a,Basic (a+1))) compile' a Id = (a+1,([],Basic a,Basic a)) compile' a Top = (a+2,([],Basic a,Basic (a+1))) compile' a Exl = (a+2,([],Pair (Basic a) (Basic (a+1)),Basic a)) compile' a Exr = (a+2,([],Pair (Basic a) (Basic (a+1)),Basic (a+1))) compile' a (Wok t) = let (b,(n,x,y)) = compile' a t in (b,(n,y,x)) compile' a (Cap t t') = (c, applynet s (n++n',x,y)) where (b,(n,x,y)) = compile' a t (c,(n',x',y')) = compile' b t' s = unify ident (Pair x y, Pair x' y') compile' a (Comp t t') = (c, applynet s (n++n',x,y')) where (b,(n,x,y)) = compile' a t (c,(n',x',y')) = compile' b t' s = unify ident (y,x') compile' a (Split t t') = compile' a ((t `Comp` (Wok Exl)) `Cap` (t' `Comp` (Wok Exr))) compile' a (Prod t t') = compile' a ((Exl `Comp` t) `Split` (Exr `Comp` t')) compile' a (Dom t) = compile' a ((t `Comp` Top) `Cap` Id) compile' a (Rng t) = compile' a (Dom (Wok t)) applynet s (n,x,y) = (map f n, apply s x, apply s y) where f (xs,i,j) = (xs, apply s i, apply s j) -- Homomorphism finder ----------------------------------------------- findhomo :: Net -> Net -> [(Int,Int)] funcs :: [Int] -> [Int] -> [[(Int,Int)]] findhomo n n' = first (filter homo (funcs (netvars n) (netvars n'))) where (ns,x,y) = n (ns',x',y') = n' homo f = (app f x == x') && (app f y == y') && and [elem (r, app f a, app f b) ns' | (r,a,b) <- ns] first [] = [] first (x:xs) = x funcs [] ys = [[]] funcs (a:as) ys = [(a,b):xs | b <- ys, xs <- funcs as ys] -- Driver code ------------------------------------------------------- prove :: String -> String tprove :: Term -> Term -> String prove xs = "\n net 1 : " ++ shownet n ++ "\n net 2 : " ++ shownet n' ++ case op of "=" -> "\n\n homo 1-2 : " ++ show h ++ "\n homo 2-1 : " ++ show h' ++ case (null h, null h') of (True,True) -> "\n\n The equation " ++ showterm t ++ " = " ++ showterm t' ++ " is FALSE\n" (True,False) -> "\n\n Only the inclusion " ++ showterm t ++ " <= " ++ showterm t' ++ " is TRUE\n" (False,True) -> "\n\n Only the inclusion " ++ showterm t ++ " >= " ++ showterm t' ++ " is TRUE\n" (False,False) -> "\n\n The equation " ++ showterm t ++ " = " ++ showterm t' ++ " is TRUE\n" "<=" -> "\n\n homo 2-1 : " ++ show h' ++ "\n\n The inclusion " ++ showterm t ++ " <= " ++ showterm t' ++ " is " ++ (if null h' then "FALSE\n" else "TRUE\n") ">=" -> "\n\n homo 1-2 : " ++ show h' ++ "\n\n The inclusion " ++ showterm t ++ " >= " ++ showterm t' ++ " is " ++ (if null h then "FALSE\n" else "TRUE\n") where (t,(op,t')) = equation xs n = compile t n' = compile t' h = findhomo n n' h' = findhomo n' n tprove t t' = "\n net 1 : " ++ shownet n ++ "\n net 2 : " ++ shownet n' ++ "\n\n homo 1-2 : " ++ show h ++ "\n homo 2-1 : " ++ show h' ++ case (null h, null h') of (True,True) -> "\n\n The equation " ++ showterm t ++ " = " ++ showterm t' ++ " is FALSE\n" (True,False) -> "\n\n Only the inclusion " ++ showterm t ++ " <= " ++ showterm t' ++ " is TRUE\n" (False,True) -> "\n\n Only the inclusion " ++ showterm t ++ " >= " ++ showterm t' ++ " is TRUE\n" (False,False) -> "\n\n The equation " ++ showterm t ++ " = " ++ showterm t' ++ " is TRUE\n" where n = compile t n' = compile t' h = findhomo n n' h' = findhomo n' n -- Put your own operator definitions here ----------------------------- r = termify "R" s = termify "S" t = termify "T" feed t = Wok Exl `Comp` (t `Cap` Exr) --=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=