msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

now in the command shell the primary type in the pipe is Expr not Tree. This makes the pt -compute and pt -typecheck more interesting

Browse Source
This commit is contained in:
krasimir
2009-05-23 21:33:52 +00:00
parent f9c877eec6
commit 0c46a129e6
10 changed files with 110 additions and 95 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/GF/Command/Abstract.hs
View File

@@ -25,7 +25,7 @@ data Value
deriving (Eq,Ord,Show) deriving (Eq,Ord,Show)
data Argument data Argument
= ATree Tree = AExpr Expr
| ANoArg | ANoArg
| AMacro Ident | AMacro Ident
deriving (Eq,Ord,Show) deriving (Eq,Ord,Show)

43
src/GF/Command/Commands.hs
View File

@@ -39,10 +39,10 @@ import Text.PrettyPrint
import Debug.Trace import Debug.Trace
type CommandOutput = ([Tree],String) ---- errors, etc type CommandOutput = ([Expr],String) ---- errors, etc
data CommandInfo = CommandInfo { data CommandInfo = CommandInfo {
exec :: [Option] -> [Tree] -> IO CommandOutput, exec :: [Option] -> [Expr] -> IO CommandOutput,
synopsis :: String, synopsis :: String,
syntax :: String, syntax :: String,
explanation :: String, explanation :: String,
@@ -117,8 +117,9 @@ allCommands cod env@(pgf, mos) = Map.fromList [
"by the flag. The target format is postscript, unless overridden by the", "by the flag. The target format is postscript, unless overridden by the",
"flag -format." "flag -format."
], ],
exec = \opts ts -> do exec = \opts es -> do
let grph = if null ts then [] else alignLinearize pgf (head ts) let ts = toTrees es
grph = if null ts then [] else alignLinearize pgf (head ts)
if isFlag "view" opts || isFlag "format" opts then do if isFlag "view" opts || isFlag "format" opts then do
let file s = "_grph." ++ s let file s = "_grph." ++ s
let view = optViewGraph opts ++ " " let view = optViewGraph opts ++ " "
@@ -261,7 +262,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
_ | isOpt "changes" opts -> changesMsg _ | isOpt "changes" opts -> changesMsg
_ | isOpt "coding" opts -> codingMsg _ | isOpt "coding" opts -> codingMsg
_ | isOpt "license" opts -> licenseMsg _ | isOpt "license" opts -> licenseMsg
[t] -> let co = getCommandOp (showTree t) in [t] -> let co = getCommandOp (showExpr t) in
case lookCommand co (allCommands cod env) of ---- new map ??!! case lookCommand co (allCommands cod env) of ---- new map ??!!
Just info -> commandHelp True (co,info) Just info -> commandHelp True (co,info)
_ -> "command not found" _ -> "command not found"
@@ -306,7 +307,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
"gr -lang=LangHin -cat=Cl | l -table -to_devanagari -to_utf8 -- hindi table", "gr -lang=LangHin -cat=Cl | l -table -to_devanagari -to_utf8 -- hindi table",
"l -unlexer=\"LangSwe=to_utf8 LangHin=to_devanagari,to_utf8\" -- different lexers" "l -unlexer=\"LangSwe=to_utf8 LangHin=to_devanagari,to_utf8\" -- different lexers"
], ],
exec = \opts -> return . fromStrings . map (optLin opts), exec = \opts -> return . fromStrings . map (optLin opts) . toTrees,
options = [ options = [
("all","show all forms and variants"), ("all","show all forms and variants"),
("bracket","show tree structure with brackets and paths to nodes"), ("bracket","show tree structure with brackets and paths to nodes"),
@@ -443,7 +444,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
"pt -compute (plus one two) -- compute value", "pt -compute (plus one two) -- compute value",
"p \"foo\" | pt -typecheck -- type check parse results" "p \"foo\" | pt -typecheck -- type check parse results"
], ],
exec = \opts -> returnFromTrees . treeOps (map prOpt opts), exec = \opts -> returnFromExprs . treeOps (map prOpt opts),
options = treeOpOptions pgf options = treeOpOptions pgf
}), }),
("q", emptyCommandInfo { ("q", emptyCommandInfo {
@@ -464,7 +465,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
("lines","return the list of lines, instead of the singleton of all contents"), ("lines","return the list of lines, instead of the singleton of all contents"),
("tree","convert strings into trees") ("tree","convert strings into trees")
], ],
exec = \opts arg -> do exec = \opts _ -> do
let file = valStrOpts "file" "_gftmp" opts let file = valStrOpts "file" "_gftmp" opts
s <- readFile file s <- readFile file
return $ case opts of return $ case opts of
@@ -524,7 +525,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
("ut", emptyCommandInfo { ("ut", emptyCommandInfo {
longname = "unicode_table", longname = "unicode_table",
synopsis = "show a transliteration table for a unicode character set", synopsis = "show a transliteration table for a unicode character set",
exec = \opts arg -> do exec = \opts _ -> do
let t = concatMap prOpt (take 1 opts) let t = concatMap prOpt (take 1 opts)
let out = maybe "no such transliteration" characterTable $ transliteration t let out = maybe "no such transliteration" characterTable $ transliteration t
return $ fromString out, return $ fromString out,
@@ -548,8 +549,9 @@ allCommands cod env@(pgf, mos) = Map.fromList [
"by the flag. The target format is postscript, unless overridden by the", "by the flag. The target format is postscript, unless overridden by the",
"flag -format." "flag -format."
], ],
exec = \opts ts -> do exec = \opts es -> do
let funs = not (isOpt "nofun" opts) let ts = toTrees es
funs = not (isOpt "nofun" opts)
let cats = not (isOpt "nocat" opts) let cats = not (isOpt "nocat" opts)
let grph = visualizeTrees pgf (funs,cats) ts -- True=digraph let grph = visualizeTrees pgf (funs,cats) ts -- True=digraph
if isFlag "view" opts || isFlag "format" opts then do if isFlag "view" opts || isFlag "format" opts then do
@@ -599,7 +601,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
], ],
exec = \opts arg -> do exec = \opts arg -> do
case arg of case arg of
[Fun id []] -> case Map.lookup id (funs (abstract pgf)) of [EVar id] -> case Map.lookup id (funs (abstract pgf)) of
Just (ty,_,eqs) -> return $ fromString $ Just (ty,_,eqs) -> return $ fromString $
render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$ render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$
if null eqs if null eqs
@@ -679,16 +681,21 @@ allCommands cod env@(pgf, mos) = Map.fromList [
optNum opts = valIntOpts "number" 1 opts optNum opts = valIntOpts "number" 1 opts
optNumInf opts = valIntOpts "number" 1000000000 opts ---- 10^9 optNumInf opts = valIntOpts "number" 1000000000 opts ---- 10^9
fromTrees ts = (ts,unlines (map showTree ts)) fromTrees ts = (map tree2expr ts,unlines (map showTree ts))
fromStrings ss = (map (Lit . LStr) ss, unlines ss) fromStrings ss = (map (ELit . LStr) ss, unlines ss)
fromString s = ([Lit (LStr s)], s) fromString s = ([ELit (LStr s)], s)
toTrees = map expr2tree
toStrings = map showAsString toStrings = map showAsString
toString = unwords . toStrings toString = unwords . toStrings
returnFromTrees ts = return $ case ts of returnFromTrees ts = return $ case ts of
[] -> (ts, "no trees found") [] -> ([], "no trees found")
_ -> fromTrees ts _ -> fromTrees ts
returnFromExprs es = return $ case es of
[] -> ([], "no trees found")
_ -> (es,unlines (map showExpr es))
prGrammar opts prGrammar opts
| isOpt "cats" opts = return $ fromString $ unwords $ map showType $ categories pgf | isOpt "cats" opts = return $ fromString $ unwords $ map showType $ categories pgf
| isOpt "fullform" opts = return $ fromString $ concatMap (prFullFormLexicon . morpho) $ optLangs opts | isOpt "fullform" opts = return $ fromString $ concatMap (prFullFormLexicon . morpho) $ optLangs opts
@@ -715,8 +722,8 @@ allCommands cod env@(pgf, mos) = Map.fromList [
app f = maybe id id (treeOp pgf f) app f = maybe id id (treeOp pgf f)
showAsString t = case t of showAsString t = case t of
Lit (LStr s) -> s ELit (LStr s) -> s
_ -> "\n" ++ showTree t --- newline needed in other cases than the first _ -> "\n" ++ showExpr t --- newline needed in other cases than the first
stringOpOptions = [ stringOpOptions = [
("bind","bind tokens separated by Prelude.BIND, i.e. &+"), ("bind","bind tokens separated by Prelude.BIND, i.e. &+"),

22
src/GF/Command/Interpreter.hs
View File

@@ -27,7 +27,7 @@ data CommandEnv = CommandEnv {
morphos :: Map.Map Language Morpho, morphos :: Map.Map Language Morpho,
commands :: Map.Map String CommandInfo, commands :: Map.Map String CommandInfo,
commandmacros :: Map.Map String CommandLine, commandmacros :: Map.Map String CommandLine,
expmacros :: Map.Map String Tree expmacros :: Map.Map String Expr
} }
mkCommandEnv :: Encoding -> PGF -> CommandEnv mkCommandEnv :: Encoding -> PGF -> CommandEnv
@@ -72,18 +72,20 @@ interpretPipe enc env cs = do
appLine es = map (map (appCommand es)) appLine es = map (map (appCommand es))
-- macro definition applications: replace ?i by (exps !! i) -- macro definition applications: replace ?i by (exps !! i)
appCommand :: [Tree] -> Command -> Command appCommand :: [Expr] -> Command -> Command
appCommand xs c@(Command i os arg) = case arg of appCommand xs c@(Command i os arg) = case arg of
ATree e -> Command i os (ATree (app e)) AExpr e -> Command i os (AExpr (app e))
_ -> c _ -> c
where where
app e = case e of app e = case e of
Meta i -> xs !! i EAbs x e -> EAbs x (app e)
Fun f as -> Fun f (map app as) EApp e1 e2 -> EApp (app e1) (app e2)
Abs x b -> Abs x (app b) ELit l -> ELit l
EMeta i -> xs !! i
EVar x -> EVar x
-- return the trees to be sent in pipe, and the output possibly printed -- return the trees to be sent in pipe, and the output possibly printed
interpret :: (String -> String) -> CommandEnv -> [Tree] -> Command -> IO CommandOutput interpret :: (String -> String) -> CommandEnv -> [Expr] -> Command -> IO CommandOutput
interpret enc env trees0 comm = case lookCommand co comms of interpret enc env trees0 comm = case lookCommand co comms of
Just info -> do Just info -> do
checkOpts info checkOpts info
@@ -108,15 +110,15 @@ interpret enc env trees0 comm = case lookCommand co comms of
-- analyse command parse tree to a uniform datastructure, normalizing comm name -- analyse command parse tree to a uniform datastructure, normalizing comm name
--- the env is needed for macro lookup --- the env is needed for macro lookup
getCommand :: CommandEnv -> Command -> [Tree] -> (String,[Option],[Tree]) getCommand :: CommandEnv -> Command -> [Expr] -> (String,[Option],[Expr])
getCommand env co@(Command c opts arg) ts = getCommand env co@(Command c opts arg) ts =
(getCommandOp c,opts,getCommandArg env arg ts) (getCommandOp c,opts,getCommandArg env arg ts)
getCommandArg :: CommandEnv -> Argument -> [Tree] -> [Tree] getCommandArg :: CommandEnv -> Argument -> [Expr] -> [Expr]
getCommandArg env a ts = case a of getCommandArg env a ts = case a of
AMacro m -> case Map.lookup m (expmacros env) of AMacro m -> case Map.lookup m (expmacros env) of
Just t -> [t] Just t -> [t]
_ -> [] _ -> []
ATree t -> [t] -- ignore piped AExpr t -> [t] -- ignore piped
ANoArg -> ts -- use piped ANoArg -> ts -- use piped

2
src/GF/Command/Parse.hs
View File

@@ -51,7 +51,7 @@ pFilename = liftM2 (:) (RP.satisfy isFileFirst) (RP.munch (not . isSpace)) where
pArgument = pArgument =
RP.option ANoArg RP.option ANoArg
(fmap ATree (pTree False) (fmap AExpr pExpr
RP.<++ RP.<++
(RP.munch isSpace >> RP.char '%' >> fmap AMacro pIdent)) (RP.munch isSpace >> RP.char '%' >> fmap AMacro pIdent))

16
src/GF/Command/TreeOperations.hs
View File

@@ -6,13 +6,9 @@ module GF.Command.TreeOperations (
import GF.Compile.TypeCheck import GF.Compile.TypeCheck
import PGF import PGF
--import GF.Compile.GrammarToGFCC (mkType,mkExp)
import qualified GF.Grammar.Grammar as G
import qualified GF.Grammar.Macros as M
import Data.List import Data.List
type TreeOp = [Tree] -> [Tree] type TreeOp = [Expr] -> [Expr]
treeOp :: PGF -> String -> Maybe TreeOp treeOp :: PGF -> String -> Maybe TreeOp
treeOp pgf f = fmap snd $ lookup f $ allTreeOps pgf treeOp pgf f = fmap snd $ lookup f $ allTreeOps pgf
@@ -20,20 +16,20 @@ treeOp pgf f = fmap snd $ lookup f $ allTreeOps pgf
allTreeOps :: PGF -> [(String,(String,TreeOp))] allTreeOps :: PGF -> [(String,(String,TreeOp))]
allTreeOps pgf = [ allTreeOps pgf = [
("compute",("compute by using semantic definitions (def)", ("compute",("compute by using semantic definitions (def)",
map (expr2tree pgf . tree2expr))), map (compute pgf))),
("paraphrase",("paraphrase by using semantic definitions (def)", ("paraphrase",("paraphrase by using semantic definitions (def)",
nub . concatMap (paraphrase pgf))), map tree2expr . nub . concatMap (paraphrase pgf . expr2tree))),
("smallest",("sort trees from smallest to largest, in number of nodes", ("smallest",("sort trees from smallest to largest, in number of nodes",
smallest)), smallest)),
("typecheck",("type check and solve metavariables; reject if incorrect", ("typecheck",("type check and solve metavariables; reject if incorrect",
concatMap (typecheck pgf))) concatMap (typecheck pgf)))
] ]
smallest :: [Tree] -> [Tree] smallest :: [Expr] -> [Expr]
smallest = sortBy (\t u -> compare (size t) (size u)) where smallest = sortBy (\t u -> compare (size t) (size u)) where
size t = case t of size t = case t of
Abs _ b -> size b + 1 EAbs _ e -> size e + 1
Fun f ts -> sum (map size ts) + 1 EApp e1 e2 -> size e1 + size e2 + 1
_ -> 1 _ -> 1
{- {-

2
src/GFI.hs
View File

@@ -141,7 +141,7 @@ loop opts gfenv0 = do
_ -> putStrLn "command definition not parsed" >> loopNewCPU gfenv _ -> putStrLn "command definition not parsed" >> loopNewCPU gfenv
"dt":f:ws -> do "dt":f:ws -> do
case readTree (unwords ws) of case readExpr (unwords ws) of
Just exp -> loopNewCPU $ gfenv { Just exp -> loopNewCPU $ gfenv {
commandenv = env { commandenv = env {
expmacros = Map.insert f exp (expmacros env) expmacros = Map.insert f exp (expmacros env)

11
src/PGF.hs
View File

@@ -48,7 +48,7 @@ module PGF(
parse, canParse, parseAllLang, parseAll, parse, canParse, parseAllLang, parseAll,
-- ** Evaluation -- ** Evaluation
tree2expr, PGF.expr2tree, paraphrase, typecheck, tree2expr, expr2tree, PGF.compute, paraphrase, typecheck,
-- ** Word Completion (Incremental Parsing) -- ** Word Completion (Incremental Parsing)
complete, complete,
@@ -287,9 +287,6 @@ complete pgf from typ input =
| otherwise = (init ws, last ws) | otherwise = (init ws, last ws)
where ws = words s where ws = words s
-- | Converts an expression to tree. The expression -- | Converts an expression to normal form
-- is first reduced to beta-eta-alfa normal form and compute :: PGF -> Expr -> Expr
-- after that converted to tree. The function definitions compute pgf = PGF.Data.normalForm (funs (abstract pgf))
-- are used in the computation.
expr2tree :: PGF -> Expr -> Tree
expr2tree pgf = PGF.Data.expr2tree (funs (abstract pgf))

89
src/PGF/Expr.hs
View File

@@ -4,7 +4,7 @@ module PGF.Expr(Tree(..), Literal(..),
Expr(..), Patt(..), Equation(..), Expr(..), Patt(..), Equation(..),
readExpr, showExpr, pExpr, ppExpr, ppPatt, readExpr, showExpr, pExpr, ppExpr, ppPatt,
tree2expr, expr2tree, tree2expr, expr2tree, normalForm,
-- needed in the typechecker -- needed in the typechecker
Value(..), Env, eval, apply, eqValue, Value(..), Env, eval, apply, eqValue,
@@ -42,9 +42,7 @@ data Tree =
deriving (Eq, Ord) deriving (Eq, Ord)
-- | An expression represents a potentially unevaluated expression -- | An expression represents a potentially unevaluated expression
-- in the abstract syntax of the grammar. It can be evaluated with -- in the abstract syntax of the grammar.
-- the 'expr2tree' function and then linearized or it can be used
-- directly in the dependent types.
data Expr = data Expr =
EAbs CId Expr -- ^ lambda abstraction EAbs CId Expr -- ^ lambda abstraction
| EApp Expr Expr -- ^ application | EApp Expr Expr -- ^ application
@@ -111,7 +109,7 @@ pTrees :: RP.ReadP [Tree]
pTrees = liftM2 (:) (pTree True) pTrees RP.<++ (RP.skipSpaces >> return []) pTrees = liftM2 (:) (pTree True) pTrees RP.<++ (RP.skipSpaces >> return [])
pTree :: Bool -> RP.ReadP Tree pTree :: Bool -> RP.ReadP Tree
pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Lit pLit RP.<++ pMeta) pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Lit pLit RP.<++ fmap Meta pMeta)
where where
pParen = RP.between (RP.char '(') (RP.char ')') (pTree False) pParen = RP.between (RP.char '(') (RP.char ')') (pTree False)
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')) pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
@@ -120,9 +118,6 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
pApp = do f <- pCId pApp = do f <- pCId
ts <- (if isNested then return [] else pTrees) ts <- (if isNested then return [] else pTrees)
return (Fun f ts) return (Fun f ts)
pMeta = do RP.char '?'
n <- fmap read (RP.munch1 isDigit)
return (Meta n)
pExpr :: RP.ReadP Expr pExpr :: RP.ReadP Expr
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm) pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
@@ -135,12 +130,14 @@ pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
pFactor = fmap EVar pCId pFactor = fmap EVar pCId
RP.<++ fmap ELit pLit RP.<++ fmap ELit pLit
RP.<++ pMeta RP.<++ fmap EMeta pMeta
RP.<++ RP.between (RP.char '(') (RP.char ')') pExpr RP.<++ RP.between (RP.char '(') (RP.char ')') pExpr
where
pMeta = do RP.char '?' pMeta = do RP.char '?'
n <- fmap read (RP.munch1 isDigit) cs <- RP.look
return (EMeta n) case cs of
(c:_) | isDigit c -> fmap read (RP.munch1 isDigit)
_ -> return 0
pLit :: RP.ReadP Literal pLit :: RP.ReadP Literal
pLit = pNum RP.<++ liftM LStr pStr pLit = pNum RP.<++ liftM LStr pStr
@@ -166,7 +163,7 @@ ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
ppTree d (Fun f []) = PP.text (prCId f) ppTree d (Fun f []) = PP.text (prCId f)
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts)) ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts))
ppTree d (Lit l) = ppLit l ppTree d (Lit l) = ppLit l
ppTree d (Meta n) = PP.char '?' PP.<> PP.int n ppTree d (Meta n) = ppMeta n
ppTree d (Var id) = PP.text (prCId id) ppTree d (Var id) = PP.text (prCId id)
@@ -181,7 +178,7 @@ ppExpr d (EAbs x e) = let (xs,e1) = getVars (EAbs x e)
getVars e = ([],e) getVars e = ([],e)
ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2)) ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
ppExpr d (ELit l) = ppLit l ppExpr d (ELit l) = ppLit l
ppExpr d (EMeta n) = PP.char '?' PP.<+> PP.int n ppExpr d (EMeta n) = ppMeta n
ppExpr d (EVar f) = PP.text (prCId f) ppExpr d (EVar f) = PP.text (prCId f)
ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps)) ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
@@ -193,15 +190,20 @@ ppLit (LStr s) = PP.text (show s)
ppLit (LInt n) = PP.integer n ppLit (LInt n) = PP.integer n
ppLit (LFlt d) = PP.double d ppLit (LFlt d) = PP.double d
ppMeta n
| n == 0 = PP.char '?'
| otherwise = PP.char '?' PP.<> PP.int n
ppParens True = PP.parens ppParens True = PP.parens
ppParens False = id ppParens False = id
----------------------------------------------------- -----------------------------------------------------
-- Evaluation -- Conversion Expr <-> Tree
----------------------------------------------------- -----------------------------------------------------
-- | Converts a tree to expression. -- | Converts a tree to expression. The conversion
-- is always total, every tree is a valid expression.
tree2expr :: Tree -> Expr tree2expr :: Tree -> Expr
tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts) tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts)
tree2expr (Lit l) = ELit l tree2expr (Lit l) = ELit l
@@ -209,29 +211,40 @@ tree2expr (Meta n) = EMeta n
tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
tree2expr (Var x) = EVar x tree2expr (Var x) = EVar x
-- | Converts an expression to tree. The expression -- | Converts an expression to tree. The conversion is only partial.
-- is first reduced to beta-eta-alfa normal form and -- Variables and meta variables of function type and beta redexes are not allowed.
-- after that converted to tree. expr2tree :: Expr -> Tree
expr2tree :: Funs -> Expr -> Tree expr2tree e = abs [] e
expr2tree funs e = value2tree [] (eval funs Map.empty e)
where where
value2tree xs (VApp f vs) = case Map.lookup f funs of abs xs (EAbs x e) = abs (x:xs) e
Just (DTyp hyps _ _,_,_) -> -- eta conversion abs xs e = case xs of
let a1 = length hyps [] -> app [] e
a2 = length vs xs -> Abs (reverse xs) (app [] e)
a = a1 - a2
i = length xs app as (EApp e1 e2) = app ((abs [] e2) : as) e1
xs' = [var i | i <- [i..i+a-1]] app as (ELit l)
in ret (reverse xs'++xs) | null as = Lit l
(Fun f (map (value2tree []) vs++map Var xs')) | otherwise = error "literal of function type encountered"
Nothing -> error ("unknown variable "++prCId f) app as (EMeta n)
value2tree xs (VGen i vs) | null vs = ret xs (Var (var i)) | null as = Meta n
| otherwise = error "variable of function type" | otherwise = error "meta variables of function type are not allowed in trees"
value2tree xs (VMeta n vs) | null vs = ret xs (Meta n) app as (EAbs x e) = error "beta redexes are not allowed in trees"
| otherwise = error "meta variable of function type" app as (EVar x) = Fun x as
value2tree xs (VLit l) = ret xs (Lit l)
value2tree xs (VClosure env (EAbs x e)) = let i = length xs
in value2tree (var i:xs) (eval funs (Map.insert x (VGen i []) env) e) -----------------------------------------------------
-- Computation
-----------------------------------------------------
-- | Compute an expression to normal form
normalForm :: Funs -> Expr -> Expr
normalForm funs e = value2expr 0 (eval funs Map.empty e)
where
value2expr i (VApp f vs) = foldl EApp (EVar f) (map (value2expr i) vs)
value2expr i (VGen j vs) = foldl EApp (EVar (var j)) (map (value2expr i) vs)
value2expr i (VMeta n vs) = foldl EApp (EMeta n) (map (value2expr i) vs)
value2expr i (VLit l) = ELit l
value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (eval funs (Map.insert x (VGen i []) env) e))
var i = mkCId ('v':show i) var i = mkCId ('v':show i)

2
src/PGF/Paraphrase.hs
View File

@@ -49,7 +49,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
[(ps,p) | (p,d@(Fun g ps)) <- equs, g==f, [(ps,p) | (p,d@(Fun g ps)) <- equs, g==f,
isClosed d || (length equs == 1 && isLinear d)] isClosed d || (length equs == 1 && isLinear d)]
equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | equss = [(f,[(Fun f (map patt2tree ps), expr2tree d) | (Equ ps d) <- eqs]) |
(f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True

6
src/PGF/TypeCheck.hs
View File

@@ -26,9 +26,9 @@ import Data.List (partition,sort,groupBy)
import Debug.Trace import Debug.Trace
typecheck :: PGF -> Tree -> [Tree] typecheck :: PGF -> Expr -> [Expr]
typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of typecheck pgf e = case inferExpr pgf (newMetas e) of
Ok t -> [expr2tree (funs (abstract pgf)) t] Ok e -> [e]
Bad s -> trace s [] Bad s -> trace s []
inferExpr :: PGF -> Expr -> Err Expr inferExpr :: PGF -> Expr -> Err Expr