forked from GitHub/gf-core
shifted to use general trees and types (with macros for c-f)
This commit is contained in:
@@ -1,8 +1,8 @@
|
||||
module GF.GFCC.CheckGFCC where
|
||||
|
||||
import GF.GFCC.Macros
|
||||
import GF.GFCC.DataGFCC
|
||||
import GF.GFCC.AbsGFCC
|
||||
import GF.GFCC.PrintGFCC
|
||||
import GF.GFCC.ErrM
|
||||
|
||||
import qualified Data.Map as Map
|
||||
@@ -24,7 +24,7 @@ checkGFCC gfcc = do
|
||||
|
||||
checkConcrete :: GFCC -> (CId,Concr) -> IO ((CId,Concr),Bool)
|
||||
checkConcrete gfcc (lang,cnc) =
|
||||
labelBoolIO ("happened in language " ++ printTree lang) $ do
|
||||
labelBoolIO ("happened in language " ++ prt lang) $ do
|
||||
(rs,bs) <- mapM checkl (Map.assocs (lins cnc)) >>= return . unzip
|
||||
return ((lang,cnc{lins = Map.fromAscList rs}),and bs)
|
||||
where
|
||||
@@ -32,11 +32,11 @@ checkConcrete gfcc (lang,cnc) =
|
||||
|
||||
checkLin :: GFCC -> CId -> (CId,Term) -> IO ((CId,Term),Bool)
|
||||
checkLin gfcc lang (f,t) =
|
||||
labelBoolIO ("happened in function " ++ printTree f) $ do
|
||||
labelBoolIO ("happened in function " ++ prt f) $ do
|
||||
(t',b) <- checkTerm (lintype gfcc lang f) t --- $ inline gfcc lang t
|
||||
return ((f,t'),b)
|
||||
|
||||
inferTerm :: [Tpe] -> Term -> Err (Term,Tpe)
|
||||
inferTerm :: [CType] -> Term -> Err (Term,CType)
|
||||
inferTerm args trm = case trm of
|
||||
K _ -> returnt str
|
||||
C i -> returnt $ ints i
|
||||
@@ -81,22 +81,21 @@ inferTerm args trm = case trm of
|
||||
where
|
||||
returnt ty = return (trm,ty)
|
||||
infer = inferTerm args
|
||||
prt = printTree
|
||||
|
||||
checkTerm :: LinType -> Term -> IO (Term,Bool)
|
||||
checkTerm (args,val) trm = case inferTerm args trm of
|
||||
Ok (t,ty) -> if eqType ty val
|
||||
then return (t,True)
|
||||
else do
|
||||
putStrLn $ "term: " ++ printTree trm ++
|
||||
"\nexpected type: " ++ printTree val ++
|
||||
"\ninferred type: " ++ printTree ty
|
||||
putStrLn $ "term: " ++ prt trm ++
|
||||
"\nexpected type: " ++ prt val ++
|
||||
"\ninferred type: " ++ prt ty
|
||||
return (t,False)
|
||||
Bad s -> do
|
||||
putStrLn s
|
||||
return (trm,False)
|
||||
|
||||
eqType :: Tpe -> Tpe -> Bool
|
||||
eqType :: CType -> CType -> Bool
|
||||
eqType inf exp = case (inf,exp) of
|
||||
(C k, C n) -> k <= n -- only run-time corr.
|
||||
(R rs,R ts) -> length rs == length ts && and [eqType r t | (r,t) <- zip rs ts]
|
||||
@@ -104,21 +103,21 @@ eqType inf exp = case (inf,exp) of
|
||||
|
||||
-- should be in a generic module, but not in the run-time DataGFCC
|
||||
|
||||
type Tpe = Term
|
||||
type LinType = ([Tpe],Tpe)
|
||||
type CType = Term
|
||||
type LinType = ([CType],CType)
|
||||
|
||||
tuple :: [Tpe] -> Tpe
|
||||
tuple :: [CType] -> CType
|
||||
tuple = R
|
||||
|
||||
ints :: Int -> Tpe
|
||||
ints :: Int -> CType
|
||||
ints = C
|
||||
|
||||
str :: Tpe
|
||||
str :: CType
|
||||
str = S []
|
||||
|
||||
lintype :: GFCC -> CId -> CId -> LinType
|
||||
lintype gfcc lang fun = case lookType gfcc fun of
|
||||
Typ cs c -> (map linc cs, linc c)
|
||||
lintype gfcc lang fun = case catSkeleton (lookType gfcc fun) of
|
||||
(cs,c) -> (map linc cs, linc c) ---- HOAS
|
||||
where
|
||||
linc = lookLincat gfcc lang
|
||||
|
||||
|
||||
@@ -52,7 +52,7 @@ mkGFCC (Grm a cs ab@(Abs afls fs cts) ccs) = GFCC {
|
||||
lcats = [(c,hyps) | Cat c hyps <- cts]
|
||||
cats = fromAscList lcats
|
||||
catfuns = fromAscList
|
||||
[(cat,[f | (f, (Typ _ c,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
|
||||
[(cat,[f | (f, (DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
|
||||
in Abstr aflags funs cats catfuns,
|
||||
concretes = fromAscList (lmap mkCnc ccs)
|
||||
}
|
||||
|
||||
@@ -11,16 +11,16 @@ import System.Random
|
||||
generate :: GFCC -> CId -> [Exp]
|
||||
generate gfcc cat = concatMap (\i -> gener i cat) [0..]
|
||||
where
|
||||
gener 0 c = [tree (AC f) [] | (f, Typ [] _) <- fns c]
|
||||
gener 0 c = [tree (AC f) [] | (f, ([],_)) <- fns c]
|
||||
gener i c = [
|
||||
tr |
|
||||
(f, Typ cs _) <- fns c,
|
||||
(f, (cs,_)) <- fns c,
|
||||
let alts = map (gener (i-1)) cs,
|
||||
ts <- combinations alts,
|
||||
let tr = tree (AC f) ts,
|
||||
depth tr >= i
|
||||
]
|
||||
fns = functionsToCat gfcc
|
||||
fns c = [(f,catSkeleton ty) | (f,ty) <- functionsToCat gfcc c]
|
||||
|
||||
|
||||
-- generate an infinite list of trees randomly
|
||||
@@ -55,7 +55,7 @@ genRandom gen gfcc cat = genTrees (randomRs (0.0, 1.0) gen) cat where
|
||||
in (t:ts, k + ks)
|
||||
_ -> ([],0)
|
||||
|
||||
fns cat = [(f,cs) | (f, Typ cs _) <- functionsToCat gfcc cat]
|
||||
fns cat = [(f,(fst (catSkeleton ty))) | (f,ty) <- functionsToCat gfcc cat]
|
||||
|
||||
|
||||
{-
|
||||
|
||||
@@ -38,6 +38,20 @@ depth tr = case tr of
|
||||
tree :: Atom -> [Exp] -> Exp
|
||||
tree = DTr []
|
||||
|
||||
cftype :: [CId] -> CId -> Type
|
||||
cftype args val = DTyp [Hyp wildCId (cftype [] arg) | arg <- args] val []
|
||||
|
||||
catSkeleton :: Type -> ([CId],CId)
|
||||
catSkeleton ty = case ty of
|
||||
DTyp hyps val _ -> ([valCat ty | Hyp _ ty <- hyps],val)
|
||||
|
||||
valCat :: Type -> CId
|
||||
valCat ty = case ty of
|
||||
DTyp _ val _ -> val
|
||||
|
||||
wildCId :: CId
|
||||
wildCId = CId "_"
|
||||
|
||||
exp0 :: Exp
|
||||
exp0 = Tr (AM 0) []
|
||||
|
||||
|
||||
Reference in New Issue
Block a user