Tue May 22 15:57:44 WEST 2007 Miguel Vilaca <jmvilaca@di.uminho.pt>
* Bug Fix: lambda-terms to IN
{
hunk ./Makefile 94
+ $(RM) lib/animLC/*.o
+ $(RM) lib/animLC/*.hi
hunk ./Makefile 123
-src/EnableGUI.o : src/EnableGUI.hs
hunk ./Makefile 286
-src/INTextualUI.o : src/INTextualUI.hs
-src/INTextualUI.o : src/State.hi
-src/INTextualUI.o : src/InfoKind.hi
-src/INTextualUI.o : src/INTextual.hi
-src/INTextualUI.o : src/SafetyNet.hi
-src/INTextualUI.o : src/Operations.hi
hunk ./Makefile 370
+src/INTextualUI.o : src/INTextualUI.hs
+src/INTextualUI.o : src/State.hi
+src/INTextualUI.o : src/InfoKind.hi
+src/INTextualUI.o : src/INTextual.hi
+src/INTextualUI.o : src/SafetyNet.hi
+src/INTextualUI.o : src/Operations.hi
hunk ./Makefile 377
-src/Main.o : src/EnableGUI.hi
hunk ./lib/animLC/Bruijn.hs 73
-index_of_fv id [] = error "Variável livre não encontrada"
+index_of_fv id [] = error "free variable not found"
hunk ./lib/animLC/Bruijn.hs 89
---REDUÇÃO BETA: (App (Abs M) N) --> M[0<-N]
+--BETA REDUCTION: (App (Abs M) N) --> M[0<-N]
hunk ./lib/animLC/Bruijn.hs 103
--- função de substituição onde se divide a "promoção" da substituição...
+-- funcao de substituicao onde se divide a "promocao" da substituicao...
hunk ./lib/animLC/Bruijn.hs 122
- Redução BETA - retorna Nothing se o termo estiver na forma normal
+ Beta Reduction - return Nothing if the term is already a canonical form
hunk ./lib/animLC/Consts.hs 19
-boundVars (Const _) = error "Termo com constantes"
+boundVars (Const _) = error "Term with constants"
hunk ./lib/animLC/Consts.hs 27
-chkConvVar (Const _) = error "Termo com constantes"
+chkConvVar (Const _) = error "Term with constants"
hunk ./lib/animLC/Consts.hs 59
- showsPrec 0 (Defs []) = showString "------- Não Existem -------\n"
+ showsPrec 0 (Defs []) = showString "------- Do not exist -------\n"
hunk ./lib/animLC/Consts.hs 61
- showsPrec 0 defs = showString "------- DEFINIÇÕES --------\n" .
+ showsPrec 0 defs = showString "------- DEFINITIONS --------\n" .
hunk ./lib/animLC/Consts.hs 69
-lookup_def c (Defs []) = error ("Constante "++ show c++" não encontrada")
+lookup_def c (Defs []) = error ("Constant "++ show c++" not found")
hunk ./lib/animLC/Consts.hs 83
- addDef' _ c _ = error ("Constante "++(show c)++
- " não é um termo fechado")
+ addDef' _ c _ = error ("Constant "++(show c)++
+ " is not a closed term")
hunk ./lib/animLC/Main.hs 1
-module Main where
-
-import Monad
-import IO
-import Data.IORef
-import qualified ParseLib as P
-
-import LambdaS
-import Consts
-import Types
-import Bruijn
-import Closure
-import Schonfinkel
-
-introMsg = ["\n Animador do LAMBDA-CALCULUS em Haskell",
- " ======================================",
- " Março 2000",
- " ELP2",
- "(digite \"ajuda\"...)\n"
- ]
-
-helpMsg = ["Sintaxe: <COMANDO> <ARGUMENTOS>",
- "",
- "Descrição dos comandos:",
- " ajuda - Visualiza esta mensagem",
- " sair - Sair do programa",
- " ctxt - Visualiza constantes definidas",
- " iniCtxt - Reinicializa definições das constantes",
- " tipo <TERMO> - infere tipo para o termo",
- " expande <TERMO> - expande constantes do termo",
- " def <CONST> <TERMO> - adiciona definição da constante",
- " redLI <TERMO> - Reduz termo c/estratégia \"leftmost-innermost\"",
- " redOL <TERMO> - Reduz termo c/estratégia \"outermost-leftmost\"",
- " redLIn <LIM> <TERMO> - Redução com limite máximo",
- " redOLn <LIM> <TERMO> - Redução com limite máximo",
- " sk <TERMO> - Aplica algoritmo Schonfinkel/Barendreght",
- " simplSK <TERMO> - Simplifica com leis SK",
- "",
- "último resultado é armazenado na constante \"RPREV\""
- ]
-
-
-data Cmd = AJUDA
- | SAIR
- | CTXT
- | INICTXT
- | DEF String Expr
- | EXPANDE Expr
- | TIPO Expr
- | REDLI Expr
- | REDLIN Int Expr
- | REDOL Expr
- | REDOLN Int Expr
- | SK Expr
- | SIMPLSK Expr
-
-
-parseAjuda = do --Parser
- ospaces
- P.string "ajuda"
- ospaces
- return AJUDA
-
-parseSair = do --Parser
- ospaces
- P.string "sair"
- ospaces
- return SAIR
-
-parseCtxt = do --Parser
- ospaces
- P.string "ctxt"
- ospaces
- return CTXT
-
-parseIniCtxt = do --Parser
- ospaces
- P.string "iniCtxt"
- ospaces
- return INICTXT
-
-parseDef = do --Parser
- ospaces
- P.string "def"
- P.spaces
- (Const const) <- parse_const
- P.spaces
- term <- parse_term
- ospaces
- return (DEF const term)
-
-parseExpande = do --Parser
- ospaces
- P.string "expande"
- P.spaces
- term <- parse_term
- ospaces
- return (EXPANDE term)
-
-parseTipo = do --Parser
- ospaces
- P.string "tipo"
- P.spaces
- term <- parse_term
- ospaces
- return (TIPO term)
-
-parseRedLI = do --Parser
- ospaces
- P.string "redLI"
- P.spaces
- term <- parse_term
- ospaces
- return (REDLI term)
-
-parseRedLIn = do --Parser
- ospaces
- P.string "redLIn"
- P.spaces
- max <- P.int
- P.spaces
- term <- parse_term
- ospaces
- return (REDLIN max term)
-
-parseRedOL = do --Parser
- ospaces
- P.string "redOL"
- P.spaces
- term <- parse_term
- ospaces
- return (REDOL term)
-
-parseRedOLn = do --Parser
- ospaces
- P.string "redOLn"
- P.spaces
- max <- P.int
- P.spaces
- term <- parse_term
- ospaces
- return (REDOLN max term)
-
-parseSK = do --Parser
- ospaces
- P.string "sk"
- P.spaces
- term <- parse_term
- ospaces
- return (SK term)
-
-parseSimplSK = do --Parser
- ospaces
- P.string "simplSK"
- P.spaces
- term <- parse_term
- ospaces
- return (SIMPLSK term)
-
-parseCmd = parseAjuda P.+++ parseSair P.+++ parseCtxt P.+++
- parseIniCtxt P.+++ parseDef P.+++ [_$_]
- parseExpande P.+++ parseTipo P.+++ parseRedLI P.+++
- parseRedLIn P.+++ parseRedOL P.+++ parseRedOLn P.+++
- parseSK P.+++ parseSimplSK
-
--------------------------------------------------
-
-showMsg = foldr (\a r->putStrLn a>>r) (return ())
-
-main = do --IO
- showMsg introMsg [_$_]
- ds <- newIORef sampleDefs
- ciclo ds
-
-ciclo ds = do --IO
- putStr "> "
- ln <- getLine
- let parsed = P.papply parseCmd ln
- if null parsed
- then putStrLn "Erro no PARSING..\n"
- else case parsed of [(t,[])] -> case t of SAIR -> return ()
- t -> procCmd ds t >>
- ciclo ds
- _ -> putStrLn "Erro no PARSING...\n"
-
-resultLn :: Expr -> Maybe Type -> Maybe Int -> IO ()
-resultLn e t c = do --IO
- putStr "=> "
- putStr (show e)
- putStr " : "
- putStr (case t of Nothing -> "(não tem tipo)"
- (Just t') -> show t')
- case c of Nothing -> return ()
- (Just c') -> putStr (" - ("++(show c')++
- " reds.)")
- putStrLn ""
-[_^I_][_^I_][_^I_][_^I_][_^I_] [_$_]
-
-
-procCmd _ AJUDA = showMsg helpMsg
-procCmd ctxt CTXT = [_$_]
- do --IO
- defs <- readIORef ctxt
- putStrLn (show defs)
-procCmd ctxt INICTXT =
- do --IO
- writeIORef ctxt sampleDefs
-procCmd ctxt (DEF c t) =
- do --IO
- defs <- readIORef ctxt
- writeIORef ctxt (addDef defs c t)
-procCmd ctxt (EXPANDE t) =
- do --IO
- defs <- readIORef ctxt
- let res = expandExpr defs t
- term = expr2term res
- tipo = renameType (tInf term)
- writeIORef ctxt (addDef defs "RPREV" res)
- resultLn res tipo Nothing
-procCmd ctxt (TIPO t) =
- do --IO
- defs <- readIORef ctxt
- let res = expandExpr defs t
- term = expr2term res
- tipo = renameType (tInf term)
- writeIORef ctxt (addDef defs "RPREV" res)
- resultLn t tipo Nothing
-procCmd ctxt (REDLI expr) =
- do --IO
- defs <- readIORef ctxt
- let term = expr2term $ expandExpr defs expr
- (c,res) = closure (-1) betaLI term
- tipo = renameType (tInf res)
- resE = term2expr res
- writeIORef ctxt (addDef defs "RPREV" resE)
- resultLn resE tipo (Just c)
-procCmd ctxt (REDOL expr) =
- do --IO
- defs <- readIORef ctxt
- let term = expr2term $ expandExpr defs expr
- (c,res) = closure (-1) betaOL term
- tipo = renameType (tInf res)
- resE = term2expr res
- writeIORef ctxt (addDef defs "RPREV" resE)
- resultLn resE tipo (Just c)
-procCmd ctxt (REDLIN max expr) =
- do --IO
- defs <- readIORef ctxt
- let term = expr2term $ expandExpr defs expr
- (c,res) = closure max betaLI term
- tipo = renameType (tInf res)
- resE = term2expr res
- writeIORef ctxt (addDef defs "RPREV" resE)
- resultLn resE tipo (Just c)
-procCmd ctxt (REDOLN max expr) =
- do --IO
- defs <- readIORef ctxt
- let term = expr2term $ expandExpr defs expr
- (c,res) = closure max betaOL term
- tipo = renameType (tInf res)
- resE = term2expr res
- writeIORef ctxt (addDef defs "RPREV" resE)
- resultLn resE tipo (Just c)
-procCmd ctxt (SK e) =
- do --IO
- defs <- readIORef ctxt
- let res = schonfinkel (expandExpr defs e)
- term = expr2term (expandExpr defs res)
- tipo = renameType (tInf term)
- writeIORef ctxt (addDef defs "RPREV" res)
- resultLn res tipo Nothing
-procCmd ctxt (SIMPLSK (Const "RPREV")) =
- do --IO
- defs <- readIORef ctxt
- let (c,res) = closure (-1) opt_schon (lookup_def "RPREV" defs)
- term = expr2term (expandExpr defs res)
- tipo = renameType (tInf term)
- writeIORef ctxt (addDef defs "RPREV" res)
- resultLn res tipo (Just c)
-procCmd ctxt (SIMPLSK e) =
- do --IO
- defs <- readIORef ctxt
- let (c,res) = closure (-1) opt_schon e
- term = expr2term (expandExpr defs res)
- tipo = renameType (tInf term)
- writeIORef ctxt (addDef defs "RPREV" res)
- resultLn res tipo (Just c)
-
-
rmfile ./lib/animLC/Main.hs
hunk ./lib/animLC/Types.hs 113
-getIndex _ [] = error "ERRO IMPREVISTO (renomeação)..."
+getIndex _ [] = error "UNPREDICTABLE ERROR (renaming)..."
addfile ./src/LambdaC.hs
hunk ./src/LambdaC.hs 1
+module LambdaC where
+
+
+import Bruijn
+import LambdaS
+import Consts
+import Network
+import IntMap hiding (map,filter)
+import InfoKind
+import Palette
+import Maybe
+import qualified PersistentDocument as PD
+import qualified PDDefaults as PD
+import Document
+import State
+import StateUtil
+import Ports
+import Math
+import List
+import INReduction
+import INRule
+import Common
+import Control.Exception
+
+type VarId = String [_$_]
+type Side = Int
+type NrFree = Int
+type Context = [(VarId,NodeNr,Side,NrFree)]
+
+
+
+drawLambda ::(InfoKind n g, InfoKind e g,Show g) => g -> n -> e -> State g n e -> Palette n ->String -> Bool ->IO(Maybe (Network g n e))
+drawLambda g n e state pal term b = [_$_]
+ do expr <- getTermOrError term
+ let n_term = expr2term expr
+ closed = closed_term n_term
+ if ( not closed) [_$_]
+ then return Nothing [_$_]
+ else do let n_termo = term2expr $ expr2term expr
+ (nt,ctx) = draw n_termo pal (Network.empty g n e) b
+ nt1 = closeEpsilon pal ctx nt
+ ntn = display nt1
+ return (Just ntn)
+
+
+getTermOrError :: String -> IO Expr
+getTermOrError s = return $ parseExpr s
+
+ [_$_]
+getlambdaReport :: String -> Maybe String
+getlambdaReport s = let e = parseExpr s
+ n_term = expr2term e
+ closed = closed_term n_term
+ in if (not closed) then Just ("The Lamda-Term is not closed.\nThe variables " ++ (show (freeVars e)++" are free "))
+ else Nothing [_$_]
+
+
+draw ::(InfoKind n g, InfoKind e g) => Expr -> Palette n -> Network g n e -> Bool -> (Network g n e,Context)
+draw t p network b = let (x,net) = addNode "interface" p network
+ in if b then let [_$_]
+ (n,n_nt) = addNode "evaluation" p net
+ nnn = setNodePosition n (DoublePoint 10 10) n_nt
+ nn_nt = connectNode (x,0) (n,1) nnn
+ in iso t (nn_nt,[]) (n,0) p
+ else iso t (net,[]) (x,0) p
+[_^I_][_^I_][_^I_][_^I_] [_$_]
+iso ::(InfoKind n g, InfoKind e g) => Expr -> (Network g n e,Context) -> (NodeNr,Side) ->Palette n -> (Network g n e,Context)
+iso (Lambda v t) (nt,ctx) (prev,side) plt = let ;(node_nr, n_nt) = addNode "lambda" plt nt
+ ;nn_nt = connectNode (prev,side) (node_nr,0) n_nt
+ ;n_ctx = (v,node_nr,1,countfree v t) : ctx
+ in iso t (nn_nt,n_ctx) (node_nr,2) plt
+
+
+iso (Apply m n) (nt,ctx) (prev,side) plt = let ;(node_nr, n_nt) = addNode "beforeApplication" plt nt
+ ;nn_nt = connectNode (prev,side) (node_nr,0) n_nt
+ ;lsn_ctx = iso m (nn_nt,ctx) (node_nr,2) plt
+ in iso n lsn_ctx (node_nr,1) plt
+
+iso (Var c) (nt,ctx) (prev,side) plt = if (make_node c ctx) [_$_]
+ then let ;(node_nr, n_nt) = addNode "copy" plt nt
+ ;nn_nt = connectNode (prev,side) (node_nr,1) n_nt
+ ;(no,si) = getVarPort ctx c
+ ;nnn_nt = connectNode (no,si) (node_nr,0) nn_nt
+ ;n_ctx = update_ctx ctx c (node_nr,2)
+ in (nnn_nt,n_ctx)
+ else let ;(no,si) = getVarPort ctx c
+ ;nnn_nt = connectNode (no,si) (prev,side) nt
+ ;n_ctx = update_ctx ctx c (-1,-1)
+ in (nnn_nt,n_ctx)
+ [_$_]
+connectNode ::InfoKind e g => (NodeNr,Side) -> (NodeNr,Side) -> Network g n e -> Network g n e
+connectNode (prev,p1) (nxt,p2) nt = let previous = getNode prev nt
+ next = getNode nxt nt
+ up = getPortIndexed p1 previous
+ down = getPortIndexed p2 next
+ in addEdgesWithJustPort [((prev,up),(nxt,down))] nt
+[_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_] [_$_]
+getPortIndexed :: Int -> Node n -> Port [_$_]
+getPortIndexed i n = head $ drop i $ fromJust $ getPorts n
+
+countfree :: String -> Expr -> Int
+countfree x t = length $ filter (==x) $ allfreeVars t
+
+allfreeVars :: Expr -> [String]
+allfreeVars (Var x) = [x]
+allfreeVars (Const _) = []
+allfreeVars (Lambda i e) = List.delete i (allfreeVars e)
+allfreeVars (Apply e1 e2) = (allfreeVars e1) ++ (allfreeVars e2)
+
+make_node:: VarId -> Context -> Bool
+make_node v c = not . null $ filter (\(a,_,_,l) -> (a==v) && (l>1)) c
+
+update_ctx :: Context -> VarId -> (Int,Int) -> Context
+update_ctx ctx v (node_nr,side) = let (q,w,e,r) = head $ filter (\(a,_,_,_) -> (a==v)) ctx
+ in if (r-1 == 0 || r == 0) then List.delete (q,w,e,r) ctx [_$_]
+ else (q,node_nr,side,r-1):(List.delete (q,w,e,r) ctx)
+
+getVarPort :: Context -> VarId -> (Int,Int)
+getVarPort c v = let (_,w,e,_) = head $ filter (\(a,_,_,_) -> (a==v)) c
+ in (w,e)
+[_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_$_]
+closeEpsilon ::(InfoKind n g, InfoKind e g) => Palette n -> Context -> Network g n e -> Network g n e
+closeEpsilon _ [] nt = nt
+closeEpsilon pal ((a,b,c,d):t) nt = let ;(node_nr, n_nt) = addNode "Erase" pal nt
+ ;nn_nt = connectNode (b,c) (node_nr,0) n_nt
+ in closeEpsilon pal t nn_nt
+
+
+
+-- Display [_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_$_]
+
+display :: Network g n e -> Network g n e
+display n = let nl = walk [getInterface n] n 1 []
+ levels = groupBylevel nl
+ pos = setBylevel (10,0) levels
+ in assign n pos
+
+
+
+walk :: [NodeNr] -> Network g n e -> Int -> [NodeNr] -> [(Int,Int)]
+walk [] _ _ _ = []
+walk (x:xs) nt l v = if (x `elem` v)[_^I_][_$_]
+ then walk xs nt l v
+ else let p = getChildrenAll nt x;
+ in [(x,l)] ++ ( walk xs nt l (x:v)) ++ ( walk p nt (l+1) (x:v))
+
+
+getChildrenAll :: Network g n e -> NodeNr -> [NodeNr]
+getChildrenAll network parent = let ;por = fromMaybe [] $ getPorts $ getNode parent network
+ ;ed = map (\(Just a) -> (getEdge a network)) $ [_$_]
+ filter (/=Nothing) $ [_$_]
+ map (edgeConnectedOnPort network parent ) por [_$_]
+ ;che = map getEdgeFrom (filter (\x -> (getEdgeTo x == parent)) (getEdges network))
+ in che ++ (map getEdgeTo ed )
+
+
+getInterface :: Network g n e -> NodeNr
+getInterface nt = (fst . head ) (filter isInterfaceNode $ getNodeAssocs nt) [_$_]
+
+
+
+
+groupBylevel :: [(Int,Int)] -> [[(Int,Int)]]
+groupBylevel = (groupBy (\(a,c) (b,n) -> c==n )) . [_$_]
+ (map swap). sort .(map swap) . (foldr (++) []) . [_$_]
+ (map (take 1)) . (groupBy (\(a,c) (b,n) -> a==b )) . sort [_$_]
+
+
+
+--Comprimento medio de um agente : 1,5
+--espacamento : 0,5
+
+
+specialFoldl2 :: DoublePoint -> [NodeNr] -> Network g n e -> Network g n e
+specialFoldl2 startingPoint nodes net = snd $ foldl gene2 (startingPoint, net) nodes
+gene2 :: (DoublePoint, Network g n e) -> NodeNr -> (DoublePoint, Network g n e)
+gene2 (actual, oldNet) nNr = (translate actual diff2, setNodePosition nNr actual oldNet)
+diff2 = DoublePoint 1.0 0.0
+
+
+setBylevel ::(Double,Double) -> [[(Int,Int)]] -> [(DoublePoint,[Int])]
+setBylevel _ [] = []
+setBylevel (x,y) (h:t) = let l = fromInteger(toInteger(length h))::Double
+ startX = (x - (( (0.5 * l-1 ) + (l * 1.5))/2) ) [_$_]
+ in if (startX < 0)
+ then [(DoublePoint 0 (y+2) , map fst h )] ++ setBylevel (x,y+2) t
+ else [(DoublePoint startX (y+2) , map fst h )] ++ setBylevel (x,y+2) t [_$_]
+
+assign :: Network g n e -> [(DoublePoint,[Int])] -> Network g n e
+assign n [] = n
+assign n ((p,nr):t) = assign (specialFoldl2 p nr n) t
+
+[_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_$_]
+[_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_^I_][_$_]
+[_^I_][_$_]
}