Tue Apr 17 19:38:48 WEST 2007 Daniel Mendes <danielgomesmendes@gmail.com>
* Automatic transformation of lambda terms into interaction nets.***END OF DESCRIPTION***
Place the long patch description above the ***END OF DESCRIPTION*** marker.
The first line of this file will be the patch name.
This patch contains the following changes:
M ./src/NetworkUI.hs -5 +64
{
adddir ./lib/animLC
hunk ./INblobs.cabal 5
-Maintainer: jmvilaca@di.uminho.pt
+Maintainer: jmvilaca@di.uminho.pt, danielgomesmendes@gmail.com
hunk ./INblobs.cabal 19
-Hs-Source-Dirs: src lib/DData
+Hs-Source-Dirs: src lib/DData lib/animLC
hunk ./Makefile 37
- src/INReductionStrategies.hs \
+ src/INReductionStrategies.hs src/LambdaC.hs \
hunk ./Makefile 42
- lib/DData/Seq.hs lib/DData/Set.hs
+ lib/DData/Seq.hs lib/DData/Set.hs \
+ lib/animLC/Bruijn.hs lib/animLC/Consts.hs \
+ lib/animLC/Schonfinkel.hs lib/animLC/Closure.hs \
+ lib/animLC/LambdaS.hs lib/animLC/ParseLib.hs lib/animLC/Types.hs
hunk ./Makefile 49
-IFACES = src:lib/DData
+IFACES = src:lib/DData:lib/animLC
hunk ./Makefile 121
+src/EnableGUI.o : src/EnableGUI.hs
+lib/animLC/ParseLib.o : lib/animLC/ParseLib.hs
+lib/animLC/LambdaS.o : lib/animLC/LambdaS.hs
+lib/animLC/LambdaS.o : lib/animLC/ParseLib.hi
+lib/animLC/Closure.o : lib/animLC/Closure.hs
+lib/animLC/Consts.o : lib/animLC/Consts.hs
+lib/animLC/Consts.o : lib/animLC/LambdaS.hi
+lib/animLC/Schonfinkel.o : lib/animLC/Schonfinkel.hs
+lib/animLC/Schonfinkel.o : lib/animLC/Closure.hi
+lib/animLC/Schonfinkel.o : lib/animLC/Consts.hi
+lib/animLC/Schonfinkel.o : lib/animLC/LambdaS.hi
+lib/animLC/Bruijn.o : lib/animLC/Bruijn.hs
+lib/animLC/Bruijn.o : lib/animLC/Closure.hi
+lib/animLC/Bruijn.o : lib/animLC/Consts.hi
+lib/animLC/Bruijn.o : lib/animLC/LambdaS.hi
+lib/animLC/Types.o : lib/animLC/Types.hs
+lib/animLC/Types.o : lib/animLC/Bruijn.hi
+lib/animLC/Types.o : lib/animLC/Consts.hi
+lib/animLC/Types.o : lib/animLC/LambdaS.hi
hunk ./Makefile 285
+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 331
+src/LambdaC.o : src/LambdaC.hs
+src/LambdaC.o : src/Common.hi
+src/LambdaC.o : src/INRule.hi
+src/LambdaC.o : src/INReduction.hi
+src/LambdaC.o : src/Math.hi
+src/LambdaC.o : src/Ports.hi
+src/LambdaC.o : src/StateUtil.hi
+src/LambdaC.o : src/State.hi
+src/LambdaC.o : src/Document.hi
+src/LambdaC.o : src/PDDefaults.hi
+src/LambdaC.o : src/PersistentDocument.hi
+src/LambdaC.o : src/Palette.hi
+src/LambdaC.o : src/InfoKind.hi
+src/LambdaC.o : lib/DData/IntMap.hi
+src/LambdaC.o : src/Network.hi
+src/LambdaC.o : lib/animLC/Consts.hi
+src/LambdaC.o : lib/animLC/LambdaS.hi
+src/LambdaC.o : lib/animLC/Bruijn.hi
hunk ./Makefile 350
+src/NetworkUI.o : src/LambdaC.hi
hunk ./Makefile 375
-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 376
+src/Main.o : src/EnableGUI.hi
addfile ./lib/animLC/Bruijn.hs
hunk ./lib/animLC/Bruijn.hs 1
+module Bruijn where
+
+import List
+import Maybe
+import Monad
+
+import LambdaS
+import Consts
+import Closure
+
+
+data Term = Ref Int
+ | Abs Term
+ | App Term Term deriving (Eq,Show)
+
+
+
+freeVarsTerm = fv 0
+ where fv i (Ref n) = if n<i then [] else [n]
+ fv i (Abs m) = map (\x->x-1) (fv (i+1) m)
+ fv i (App m n) = nub $ (fv i m) ++ (fv i n)
+
+
+--instance Show Term where
+ -- showsPrec i t = showsPrec i (term2expr t)
+
+
+----------------------------------------
+--
+-- Bound Vars: x0, x1, x2, ...
+-- Free Vars: u0, u1, u2, ...
+--
+
+bound_var n = 'x':(show n)
+free_var n = 'u':(show n)
+
+nth l n = head $ drop (n-1) l
+
+term2expr = expression []
+ where expression free_vars = expr free_vars (length free_vars)
+ expr env depth (Ref n) = Var $ if n>=depth
+ then free_var (n-depth)
+ else (nth env (n+1))
+ expr env depth (App t1 t2) = Apply (expr env depth t1)
+ (expr env depth t2)
+ expr env depth (Abs t) = let x=bound_var depth
+ in Lambda x (expr (x:env) (depth+1) t)
+
+
+-------------------------
+
+
+
+valid_at_depth n (Ref m) = m < n
+valid_at_depth n (Abs t) = valid_at_depth (n+1) t
+valid_at_depth n (App t1 t2) = valid_at_depth n t1 && valid_at_depth n t2
+
+
+closed_term = valid_at_depth 0
+
+
+min_context_depth = min_rec 0
+ where min_rec n (Ref m) = m-n+1
+ min_rec n (Abs t) = min_rec (n+1) t
+ min_rec n (App t1 t2) = max (min_rec n t1) (min_rec n t2)
+
+
+--closure t = until closed_term Abs
+
+
+
+
+index_of_fv id [] = error "Variável livre não encontrada"
+index_of_fv id (x:xs) = if id==x then 0 else 1 + index_of_fv id xs
+
+
+
+expr2term :: Expr -> Term
+expr2term e = convert_aux (freeVars e) [] e
+ where convert_aux fv bv (Var x) = case findIndex (==x) bv of
+ Nothing -> Ref ((length bv)+
+ (index_of_fv x fv))
+ (Just i) -> Ref i
+ convert_aux fv bv (Lambda x e) = Abs (convert_aux fv (x:bv) e)
+ convert_aux fv bv (Apply e f) = App (convert_aux fv bv e)
+ (convert_aux fv bv f)
+
+
+--REDUÇÃO BETA: (App (Abs M) N) --> M[0<-N]
+-- subst m d n <- m[d<-n]
+subst :: Term -> Int -> Term -> Term
+subst (Abs m) d t = Abs (subst m (d+1) t)
+subst (App m n) d t = App (subst m d t) (subst n d t)
+subst (Ref n) d t | n<d = Ref n
+ | n>d = Ref (n-1)
+ | n==d = rename n 0 t
+ where rename i j (Ref n) | n<j = Ref n
+ | True = Ref (n+i)
+ rename i j (App m n) = App (rename i j m) (rename i j n)
+ rename i j (Abs m) = Abs (rename i (j+1) m)
+
+--
+-- função de substituição onde se divide a "promoção" da substituição...
+promove :: Int -> Term -> Term
+promove n = promoveAux 0
+ where promoveAux k (Ref i) = if i<k then Ref i
+ else Ref (n+i)
+ promoveAux k (Abs m) = Abs (promoveAux (k+1) m)
+ promoveAux k (App m n) = App (promoveAux k m) (promoveAux k n)
+
+subst' :: Term -> Term -> Term
+subst' t = subst'aux 0
+ where subst'aux n (Ref k) = if k==n then promove n t
+ else if k<n then Ref k
+ else Ref (k-1)
+ subst'aux n (Abs t') = Abs (subst'aux (n+1) t')
+ subst'aux n (App t' t'') = App (subst'aux n t') (subst'aux n t'')
+
+-----
+
+{-
+ Redução BETA - retorna Nothing se o termo estiver na forma normal
+-}
+-- betaOL m <- outermost-leftmost one step beta red.
+betaOL :: Term -> Maybe Term
+betaOL (Ref _) = Nothing
+betaOL (App (Abs m) n) = Just $ subst m 0 n
+betaOL (App m1 m2) = do {r1 <- betaOL m1;return (App r1 m2)}
+ `mplus`
+ do {r2 <- betaOL m2;return (App m1 r2)}
+betaOL (Abs m) = do {r <- (betaOL m);return (Abs r)}
+
+
+--betaLI m <- innermost-leftmost one step beta red.
+betaLI :: Term -> Maybe Term
+betaLI (Ref n) = Nothing
+betaLI (App (Abs m) n) = do {r<-betaLI m;return (App (Abs r) n)}
+ `mplus`
+ (Just $ subst m 0 n)
+betaLI (App m1 m2) = do {r1 <- betaLI m1;return (App r1 m2)}
+ `mplus`
+ do {r2 <- betaLI m2;return (App m1 r2)}
+betaLI (Abs m) = do {r <- (betaLI m);return (Abs r)}
+
+
+
+--instance Rewrite Term where
+-- rewrite = betaOL
+
addfile ./lib/animLC/Closure.hs
hunk ./lib/animLC/Closure.hs 1
+module Closure where
+
+----
+-- Fecho reflexivo e transitivo de uma RELAÇÃO
+-- recebe: limite de reduções (-1 sem limite)
+-- função de redução - 1 passo
+-- termo a reduzir
+-- retorna forma normal e contador de reduções
+-- (pode entrar em ciclo...)
+closure :: Int -> (a->Maybe a) -> a -> (Int,a)
+closure max beta expr = closureAux max beta 0 expr
+ where closureAux max beta cont expr
+ | max==cont = (max,expr)
+ | True = case (beta expr) of
+ Nothing -> (cont,expr)
+ (Just e) -> closureAux max beta (cont+1) e
+
+
+
+-- Equipa o tipo com uma noção de re-escrita...
+class Rewrite a where
+ rewrite :: a -> Maybe a [_$_]
+ rstar :: Int -> a -> (Int,a)
+ rstar max x = rstarAux max 0 x
+ where rstarAux max c x | c==max = (max,x)
+ | True = case (rewrite x) of
+ Nothing -> (c,x)
+ (Just x') -> rstarAux max (c+1) x'
+ nform :: a -> a
+ nform x = snd (rstar (-1) x)
addfile ./lib/animLC/Consts.hs
hunk ./lib/animLC/Consts.hs 1
+module Consts where
+
+import List
+
+import LambdaS
+import Monad
+
+
+--Assume-se que as constantes são termos fechados...
+freeVars :: Expr -> [String]
+freeVars (Var x) = [x]
+freeVars (Const _) = []
+freeVars (Lambda i e) = delete i (freeVars e)
+freeVars (Apply e1 e2) = nub $ (freeVars e1) ++ (freeVars e2)
+
+--Assume-se que as constantes já foram expandidas...
+boundVars :: Expr -> [String]
+boundVars (Var _) = []
+boundVars (Const _) = error "Termo com constantes"
+boundVars (Lambda v m) = nub $ v:(boundVars m)
+boundVars (Apply m n) = nub $ boundVars m ++ boundVars n
+
+
+--Verifica se um termo satisfaz a convenção das variáveis...
+chkConvVar :: Expr -> Bool
+chkConvVar (Var _) = True
+chkConvVar (Const _) = error "Termo com constantes"
+chkConvVar (Lambda _ m) = chkConvVar m
+chkConvVar (Apply m n) = chkConvVar m && chkConvVar n &&
+ null (union
+ (intersect (boundVars m) (freeVars n))
+ (intersect (boundVars n) (freeVars m)))
+--o último teste não é estritamente necessário (mas é coerente com a
+--apresentação corrente da convenção: as variáveis ligadas são distintas
+--das variáveis livres).
+
+
+--Predicados...
+closedTerm t = freeVars t == []
+
+--Função que expande as CONSTANTES (de acordo com lista de DEFINIÇÕES)
+-- ...Aproveita-se a travessia para aplicar CONVENÇÃO DAS VARIÁVEIS...
+expandExpr :: Defs -> Expr -> Expr
+expandExpr defs (Var v) = Var v
+expandExpr defs (Const c) = expandExpr defs (lookup_def c defs)
+expandExpr defs (Lambda v e) = Lambda v (expandExpr defs e)
+expandExpr defs (Apply m n) = Apply (expandExpr defs m) (expandExpr defs n)
+
+
+-------------------------------
+-- TRATAMENTO DAS CONSTANTES...
+
+
+data Defs = Defs [(String,Expr)]
+
+-- i=0 : iniciar...
+-- i<>0 : continuar...
+instance Show Defs where
+ showsPrec 0 (Defs []) = showString "------- Não Existem -------\n"
+ showsPrec _ (Defs []) = showString "---------------------------\n"
+ showsPrec 0 defs = showString "------- DEFINIÇÕES --------\n" .
+ showsPrec 1 defs
+ showsPrec _ (Defs ((c,t):xs)) = showString c . showString " = " .
+ shows t . showChar '\n' .
+ showsPrec 1 (Defs xs)
+
+nullEnv = Defs []
+
+lookup_def c (Defs []) = error ("Constante "++ show c++" não encontrada")
+lookup_def c (Defs ((x,y):xs)) = if c==x then y else lookup_def c (Defs xs)
+
+remove_def c (Defs []) = Defs []
+remove_def c (Defs ((x,y):xs)) | c==x = Defs xs
+ | True = let (Defs d) = remove_def c (Defs xs)
+ in Defs ((x,y):d)
+
+-- Assume-se (sem efectuar teste) que as constantes não são
+--recursivas (directa ou indirectamente)
+addDef :: Defs -> String -> Expr -> Defs
+addDef defs const expr = addDef' (remove_def const defs) const expr
+ where addDef' (Defs defs) const expr | closedTerm expr =
+ Defs ((const,expr):defs)
+ addDef' _ c _ = error ("Constante "++(show c)++
+ " não é um termo fechado")
+
+
+addDefs :: Defs -> [(String,String)] -> Defs
+addDefs defs l = foldl (\d (c,e)->addDef d c (parseExpr e)) defs l
+
+
+sampleDefsTxt = [("K","[x,y]x"),
+ ("S","[x,y,z]x z(y z)"),
+ --
+ ("I","[x]x"), --I = SKK
+ ("B","S (K S) K"),
+ ("C","S (B S (B K S)) (K K)"),
+ --
+ ("W","[x]x x"),
+ ("Omega","W W"),
+ ----------------
+ ("Pair","[x,y,p]p x y"),
+ ("Proj1","[p]p ([x,y]x)"),
+ ("Proj2","[p]p ([x,y]y)"),
+ -------------
+ ("True","[x,y]x"),
+ ("False","[x,y]y"),
+ ("Or","[x,y]x True y"),
+ ("And","[x,y]x y False"),
+ -------------------------
+ ("Zero","[s,z]z"),
+ ("Succ","[n,s,z]s (n s z)"),
+ ("IsZero","[x]x ([r]False) True"),
+ ("Plus","[x,y]x Succ y"),
+ ("Mult","[x,y]x (Plus y) Zero"),
+ ("PrimRecNat","[n,f,z]Proj2 (n ([p]Pair (Succ (Proj1 p)) (f (Proj1 p) (Proj2 p))) (Pair Zero z) )"),
+ ("Pred","[n]PrimRecNat n ([p,r]p) Zero"),
+ ("Factorial","[n]PrimRecNat n ([p,r]Mult (Succ p) r) (Succ Zero)"),
+ --------------------------------
+ ("Y","[f]([x]f (x x)) [x]f (x x)"),
+ ("Fix","Y"),
+ ------------
+ ("FactorialR","Fix [f,n](IsZero n) (Succ Zero) (Mult n (f (Pred n)))")
+ ]
+
+sampleDefs = addDefs nullEnv sampleDefsTxt
+
+------------------------------
+--
addfile ./lib/animLC/LambdaS.hs
hunk ./lib/animLC/LambdaS.hs 1
+module LambdaS
+where
+
+import List
+import ParseLib
+
+data Expr = Var String
+ | Const String
+ | Lambda String Expr
+ | Apply Expr Expr deriving (Eq)
+
+
+-- i==0 : normal
+-- i>0 : precisa parênteses
+-- i<0 : precisa fechar abstracção
+--
+--
+
+instance Show Expr where
+ showsPrec i (Lambda v t) | i>= 0 = showString "([" .
+ showString v .
+ showsPrec (-1) t .
+ showChar ')'
+ showsPrec i (Lambda v t ) = showChar ',' .
+ showString v .
+ showsPrec i t
+ showsPrec i (Var v) | i>=0 = showString v
+ showsPrec i (Var v) = showChar ']' . showString v
+ showsPrec i (Const c) | i>=0 = showString c
+ showsPrec i (Const c) = showChar ']' . showString c
+ showsPrec 0 (Apply m n) = showsPrec 0 m . showChar ' ' . showsPrec 1 n
+ showsPrec i (Apply m n) | i>0 = showChar '(' .
+ showsPrec 0 (Apply m n) .
+ showChar ')'
+ showsPrec i (Apply m n) = showChar ']' . showsPrec 0 (Apply m n)
+
+
+------------------------------------------
+-- Parsing...
+--
+
+ospaces = many (sat (==' '))
+
+parse_var =
+ do --Parser
+ ospaces
+ c <- lower
+ rest <- many alphanum
+ return (Var (c:rest))
+
+parse_const =
+ do --Parser
+ ospaces
+ c <- upper
+ rest <- many alphanum
+ return (Const (c:rest))
+
+parse_num =
+ do --Parser
+ ospaces
+ m <- char '#'
+ i <- int
+ return (iter i)
+ where iter 0 = Const "Zero"
+ iter n = Apply (Const "Succ") (iter (n-1))
+
+parse_abs =
+ do --Parser
+ ospaces
+ char '['
+ lv <- sepby (ospaces>>ident) (char ',')
+ ospaces
+ char ']'
+ t <- parse_term
+ return (foldr Lambda t lv)
+
+parse_apps =
+ do --Parser
+ ospaces
+-- ts <- sepby1 parse_term' spaces
+ ts <- many1 parse_term'
+ return (foldl1 Apply ts)
+
+parse_term' =
+ do --Parser
+ do {ospaces;char '(';t<-parse_term;ospaces;char ')';return t} +++
+ parse_var +++ parse_const +++ parse_num +++ parse_abs
+
+parse_term =
+ do --Parser
+ parse_apps +++ parse_term'
+
+
+parseExpr x = let [(t,r)] = papply parse_term x in
+ if r==[] then t else error "Erro no PARSING"
+
+
+
addfile ./lib/animLC/Main.hs
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)
+
+
addfile ./lib/animLC/ParseLib.hs
hunk ./lib/animLC/ParseLib.hs 1
+{-----------------------------------------------------------------------------
+
+ A LIBRARY OF MONADIC PARSER COMBINATORS
+
+ 29th July 1996
+ Revised, October 1996
+ Revised again, November 1998
+
+ Graham Hutton Erik Meijer
+ University of Nottingham University of Utrecht
+
+This Haskell 98 script defines a library of parser combinators, and is taken
+from sections 1-6 of our article "Monadic Parser Combinators". Some changes
+to the library have been made in the move from Gofer to Haskell:
+
+ * Do notation is used in place of monad comprehension notation;
+
+ * The parser datatype is defined using "newtype", to avoid the overhead
+ of tagging and untagging parsers with the P constructor.
+
+-----------------------------------------------------------------------------}
+
+module ParseLib
+ (Parser, item, papply, (+++), sat, many, many1, sepby, sepby1, chainl,
+ chainl1, chainr, chainr1, ops, bracket, char, digit, lower, upper,
+ letter, alphanum, string, ident, nat, int, spaces, comment, junk,
+ parse, token, natural, integer, symbol, identifier, module Monad) where
+
+import Char
+import Monad
+
+infixr 5 +++
+
+--- The parser monad ---------------------------------------------------------
+
+newtype Parser a = P (String -> [(a,String)])
+
+instance Functor Parser where
+ -- map :: (a -> b) -> (Parser a -> Parser b)
+ fmap f (P p) = P (\inp -> [(f v, out) | (v,out) <- p inp])
+
+instance Monad Parser where
+ -- return :: a -> Parser a
+ return v = P (\inp -> [(v,inp)])
+
+ -- >>= :: Parser a -> (a -> Parser b) -> Parser b
+ (P p) >>= f = P (\inp -> concat [papply (f v) out | (v,out) <- p inp])
+
+instance MonadPlus Parser where
+ -- mzero :: Parser a
+ mzero = P (\inp -> [])
+
+ -- mplus :: Parser a -> Parser a -> Parser a
+ (P p) `mplus` (P q) = P (\inp -> (p inp ++ q inp))
+
+--- Other primitive parser combinators ---------------------------------------
+
+item :: Parser Char
+item = P (\inp -> case inp of
+ [] -> []
+ (x:xs) -> [(x,xs)])
+
+force :: Parser a -> Parser a
+force (P p) = P (\inp -> let x = p inp in
+ (fst (head x), snd (head x)) : tail x)
+
+first :: Parser a -> Parser a
+first (P p) = P (\inp -> case p inp of
+ [] -> []
+ (x:xs) -> [x])
+
+papply :: Parser a -> String -> [(a,String)]
+papply (P p) inp = p inp
+
+--- Derived combinators ------------------------------------------------------
+
+(+++) :: Parser a -> Parser a -> Parser a
+p +++ q = first (p `mplus` q)
+
+sat :: (Char -> Bool) -> Parser Char
+sat p = do {x <- item; if p x then return x else mzero}
+
+many :: Parser a -> Parser [a]
+many p = force (many1 p +++ return [])
+
+many1 :: Parser a -> Parser [a]
+many1 p = do {x <- p; xs <- many p; return (x:xs)}
+
+sepby :: Parser a -> Parser b -> Parser [a]
+p `sepby` sep = (p `sepby1` sep) +++ return []
+
+sepby1 :: Parser a -> Parser b -> Parser [a]
+p `sepby1` sep = do {x <- p; xs <- many (do {sep; p}); return (x:xs)}
+
+chainl :: Parser a -> Parser (a -> a -> a) -> a -> Parser a
+chainl p op v = (p `chainl1` op) +++ return v
+
+chainl1 :: Parser a -> Parser (a -> a -> a) -> Parser a
+p `chainl1` op = do {x <- p; rest x}
+ where
+ rest x = do {f <- op; y <- p; rest (f x y)}
+ +++ return x
+
+chainr :: Parser a -> Parser (a -> a -> a) -> a -> Parser a
+chainr p op v = (p `chainr1` op) +++ return v
+
+chainr1 :: Parser a -> Parser (a -> a -> a) -> Parser a
+p `chainr1` op = do {x <- p; rest x}
+ where
+ rest x = do {f <- op; y <- p `chainr1` op; return (f x y)}
+ +++ return x
+
+ops :: [(Parser a, b)] -> Parser b
+ops xs = foldr1 (+++) [do {p; return op} | (p,op) <- xs]
+
+bracket :: Parser a -> Parser b -> Parser c -> Parser b
+bracket open p close = do {open; x <- p; close; return x}
+
+--- Useful parsers -----------------------------------------------------------
+
+char :: Char -> Parser Char
+char x = sat (\y -> x == y)
+
+digit :: Parser Char
+digit = sat isDigit
+
+lower :: Parser Char
+lower = sat isLower
+
+upper :: Parser Char
+upper = sat isUpper
+
+letter :: Parser Char
+letter = sat isAlpha
+
+alphanum :: Parser Char
+alphanum = sat isAlphaNum
+
+string :: String -> Parser String
+string "" = return ""
+string (x:xs) = do {char x; string xs; return (x:xs)}
+
+ident :: Parser String
+ident = do {x <- lower; xs <- many alphanum; return (x:xs)}
+
+nat :: Parser Int
+nat = do {x <- digit; return (digitToInt x)} `chainl1` return op
+ where
+ m `op` n = 10*m + n
+
+int :: Parser Int
+int = do {char '-'; n <- nat; return (-n)} +++ nat
+
+--- Lexical combinators ------------------------------------------------------
+
+spaces :: Parser ()
+spaces = do {many1 (sat isSpace); return ()}
+
+comment :: Parser ()
+comment = do {string "--"; many (sat (\x -> x /= '\n')); return ()}
+
+junk :: Parser ()
+junk = do {many (spaces +++ comment); return ()}
+
+parse :: Parser a -> Parser a
+parse p = do {junk; p}
+
+token :: Parser a -> Parser a
+token p = do {v <- p; junk; return v}
+
+--- Token parsers ------------------------------------------------------------
+
+natural :: Parser Int
+natural = token nat
+
+integer :: Parser Int
+integer = token int
+
+symbol :: String -> Parser String
+symbol xs = token (string xs)
+
+identifier :: [String] -> Parser String
+identifier ks = token (do {x <- ident; if not (elem x ks) then return x
+ else mzero})
+
+------------------------------------------------------------------------------
addfile ./lib/animLC/Schonfinkel.hs
hunk ./lib/animLC/Schonfinkel.hs 1
+module Schonfinkel where
+
+import Monad
+
+import LambdaS
+import Consts
+import Closure
+
+
+schonfinkel :: Expr -> Expr
+schonfinkel (Var x) = Var x
+schonfinkel (Const x) = Const x
+schonfinkel (Apply m n) = Apply (schonfinkel m) (schonfinkel n)
+schonfinkel (Lambda x (Var y)) | x==y = Const "I"
+ | True = Apply (Const "K") (Var y)
+schonfinkel (Lambda x (Const y)) = Apply (Const "K") (Const y)
+schonfinkel (Lambda x (Apply m n)) =
+ Apply (Apply (Const "S") (schonfinkel (Lambda x m)))
+ (schonfinkel (Lambda x n))
+schonfinkel (Lambda x (Lambda y m)) =
+ (schonfinkel . Lambda x . schonfinkel . Lambda y) m
+
+
+--realiza UM PASSO da optimização... (estrategia outermost-leftmost)
+opt_schon :: Expr -> Maybe Expr
+-- S (K M) I = M
+opt_schon (Apply (Apply (Const "S") (Apply (Const "K") m))
+ (Const "I")) = Just m
+-- S (K M) (K N) = K (M N)
+opt_schon (Apply (Apply (Const "S") (Apply (Const "K") m))
+ (Apply (Const "K") n)) =
+ Just $ Apply (Const "K") (Apply m n)
+-- S (K M) N = B M N
+opt_schon (Apply (Apply (Const "S") (Apply (Const "K") m)) n) =
+ Just $ Apply (Apply (Const "B") m) n
+-- S M (K N) = C M N
+opt_schon (Apply (Apply (Const "S") m) (Apply (Const "K") n)) =
+ Just $ Apply (Apply (Const "C") m) n
+opt_schon (Apply m1 m2) = do {r1 <- opt_schon m1;return (Apply r1 m2)}
+ `mplus`
+ do {r2 <- opt_schon m2;return (Apply m1 r2)}
+opt_schon _ = Nothing
+
+
addfile ./lib/animLC/Types.hs
hunk ./lib/animLC/Types.hs 1
+module Types where
+
+import Monad
+import Char
+
+import LambdaS
+import Consts
+import Bruijn
+
+
+data Type = TVar Int | TArrow Type Type deriving Eq
+
+varsInType :: Type -> [Int]
+varsInType (TVar i) = [i]
+varsInType (TArrow t1 t2) = (varsInType t1) ++ (varsInType t2)
+
+-- p>0 necessita parênteses
+-- p==0 não necessita...
+instance Show Type where
+ showsPrec _ (TVar i) = showChar (chr (97+i))
+ showsPrec p (TArrow t1 t2) | p>0 = showChar '(' .
+ showsPrec 0 (TArrow t1 t2) .
+ showChar ')'
+ | True = showsPrec 1 t1 .
+ showString "->" .
+ showsPrec 0 t2
+
+
+-- Representamos substituições como morfismos...
+type Subst = Int -> Type
+
+--Substituição nula...
+nullSubst :: Subst
+nullSubst = TVar
+
+--Substituição unitária... (igual à identidade excepto num ponto)
+unSubst :: Int -> Type -> Subst
+unSubst i t n | n==i = t
+ | True = TVar n
+
+--Aplicação de substituições...
+appSubst :: Type -> Subst -> Type
+appSubst (TVar i) s = s i
+appSubst (TArrow t1 t2) s = TArrow (appSubst t1 s) (appSubst t2 s)
+
+--Composição de substituições... (s1 . s2)
+compSubst :: Subst -> Subst -> Subst
+compSubst s1 s2 v = appSubst (s2 v) s1
+
+--Unificação de termos...
+unifType :: Type -> Type -> Maybe Subst
+unifType (TVar v1) (TVar v2) = [_$_]
+ Just $ if v1<v2 then unSubst v1 (TVar v2) [_$_]
+ else unSubst v2 (TVar v1)
+unifType (TVar v) t =
+ if v `notElem` varsInType t then Just $ unSubst v t else Nothing
+unifType t (TVar v) =
+ if v `notElem` varsInType t then Just $ unSubst v t else Nothing
+unifType (TArrow t1 t2) (TArrow t3 t4) = do --Maybe
+ s <- unifType t1 t3
+ s' <- unifType (appSubst t2 s)
+ (appSubst t4 s)
+ return (compSubst s' s)
+
+
+-----
+-- CONTEXTOS...
+--
+-- são representados como listas [Type]
+
+appCtxt :: [Type] -> Subst -> [Type]
+appCtxt c s = map (flip appSubst s) c
+
+
+getNth l n = head $ drop n l
+
+
+-----
+-- INFERÊNCIA DE TIPOS...
+
+--tInf realiza a inferencia de tipos...
+-- ... dado um contexto inicial, um termo e um tipo, procura uma
+-- substituição que satisfaça a asserção \Sigma\vdash t: T
+--tInf :: [(Int,Type)] -> Term -> Type -> Maybe Subst
+tInf t = do --Maybe
+ (_,s) <- tInfAux (nfv+1) (take nfv [TVar i|i<-[1..]]) t (TVar 0)
+ return (appSubst (TVar 0) s)
+ where fv = freeVarsTerm t
+ nfv = length fv
+tInfAux i ctxt (Ref v) t = do --Maybe
+ s <- unifType t (getNth ctxt v)
+ return (i,s)
+tInfAux i ctxt (Abs m) t = do let t1=TVar i
+ let t2=TVar (i+1)
+ s <- unifType t (TArrow t1 t2)
+ (i',s') <- tInfAux (i+2) (appCtxt (t1:ctxt) s)
+ m (appSubst t2 s)
+ return (i',compSubst s' s)
+tInfAux i ctxt (App m n) t = do let t1=TVar i
+ (i',s) <- tInfAux (i+1) ctxt n t1
+ (i'',s') <- tInfAux i' (appCtxt ctxt s) m
+ (appSubst (TArrow t1 t) s)
+ return (i'',compSubst s' s)
+
+
+-- renameType produz uma renomeação de forma aparecerem as primeiras
+-- variáveis de tipos...
+renameType Nothing = Nothing
+renameType (Just t) = Just $ rtAux (varsInType t) t
+ where rtAux vs (TVar i) = TVar $ getIndex i vs
+ rtAux vs (TArrow m n) = TArrow (rtAux vs m) (rtAux vs n)
+
+getIndex _ [] = error "ERRO IMPREVISTO (renomeação)..."
+getIndex i (x:xs) | i==x = 0
+ | True = 1 + getIndex i xs
+
hunk ./makeclean.bat 6
+del lib\animLC\*.hi
hunk ./makeclean.bat 10
+del lib\animLC\*.o
hunk ./src/NetworkUI.hs 38
+import LambdaC
hunk ./src/NetworkUI.hs 365
+ [_$_]
+ ; menuItem opsMenu [text := "Lambda term to Net" , on command := do {b <- lambdaDialog g n e state; return() } ]
hunk ./src/NetworkUI.hs 1551
-
-
-
-
-
+lambdaDialog :: (InfoKind n g, InfoKind e g,Show g) => g -> n -> e -> State g n e -> IO (Maybe Int)
+lambdaDialog g n e state = [_$_]
+ do ;theFrame <- getNetworkFrame state
+ ;pDoc <- getDocument state
+ ;doc <- PD.getDocument pDoc
+ ;let pal = getPalette doc
+ ;dial <- dialog theFrame [text := "Lambda term to Net", position := pt 200 20]
+ ;p <- panel dial []
+ ;termbox <- textCtrl p [text := "[x]x"]
+ ;help <- button p [text := "Help"]
+ ;goNet <- button p [text := "Create Net"]
+ ;ok <- button p [text := "Done"]
+ ;can <- button p [text := "Cancel" ]
+ ;sc1 <- checkBox p [text := "Add Token", checked := False]
+ ;set dial [ layout := container p $ [_$_]
+ margin 10 $ [_$_]
+ column 5 [ label "Lambda term input"
+ , row 2 [hfill $ widget termbox, column 10 [widget help ,widget goNet]]
+ , hrule 350
+ , row 5 [widget ok, widget can,widget sc1]
+ ]
+ ]
+ ;showModal dial $ \stop -> [_$_]
+ do set goNet [on command := do {;ex <- get termbox text
+ ;safetyNet theFrame $ do { ;sele <- get sc1 checked[_^I_][_$_]
+ ;s <- drawLambda g n e state pal ex sele
+ ;case s of [_$_]
+ Nothing -> do ;let rep = getlambdaReport ex
+ ;case rep of
+ Nothing -> return ()
+ Just i -> errorDialog dial "Lambda Terms" $ i [_$_]
+ ;return ()
+ Just nt -> do ;PD.updateDocument "Draw Lambda" ( updateNetwork (\a -> nt)) pDoc
+ ;repaintAll state
+ ;return ()
+ }
+ -- ;stop Nothing
+ }
+ ]
+ set help [on command := do infoDialog dial "Help" $ helpString
+ ]
+ set ok [on command := stop Nothing]
+ set can [on command := stop Nothing]
+ [_$_]
+ where helpString = "Before starting to create Nets you must load the LambdaC palette in your Palettes folder.\n"
+ ++ "To change the agent palette go to Symbols -> Change shape palettes and choose the LambdaC Palette\n\n"
+ ++ "************* Lambda Term Gramar: ***************\n\n"
+ ++ "Term -> \'[\' ListOfVars \']\' Term \n"
+ ++ " | \'(\' Term \')\' \n"
+ ++ " | Term Term \n"
+ ++ " | Var\n\n"
+ ++ "ListOfVars -> Var\n"
+ ++ " | Var \',\' ListOfVars \n"
+ ++ " \n"
+ ++ "Var -> String \n\n\n************* Some Examples: *************** \n\n\n"
+ ++ "Lambda Notation INblobs Lambda Notation\n\n"
+ ++ " \\x.x [x]x\n"
+ ++ " \\x y.x y [x,y]x y or [x][y]x y \n"
+ ++ " (\\x.x x) (\\x. x x) ([x]x x) ([x]x x)\n"
+ ++ " x x \n"
+ [_$_]
hunk ./startghc.bat 1
-ghc -ffi -package wx -package HaXml -Wall -fglasgow-exts -ilib\DData:src src\Main.hs --make -o INblobs.exe -ignore-package network-1.0
+ghc -ffi -package wx -package HaXml -Wall -fglasgow-exts -ilib\DData:lib\animLC:src src\Main.hs --make -o INblobs.exe -ignore-package network-1.0
hunk ./startghci.bat 1
-ghci -ffi -package wx -package HaXml -Wall -fglasgow-exts -ilib\DData:src src\Main.hs -ignore-package network-1.0
+ghci -ffi -package wx -package HaXml -Wall -fglasgow-exts -ilib\DData:lib\animLC:src src\Main.hs -ignore-package network-1.0
}