diff options
Diffstat (limited to 'src/GF/Grammar/LookAbs.hs')
| -rw-r--r-- | src/GF/Grammar/LookAbs.hs | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/src/GF/Grammar/LookAbs.hs b/src/GF/Grammar/LookAbs.hs new file mode 100644 index 000000000..5e0994d46 --- /dev/null +++ b/src/GF/Grammar/LookAbs.hs @@ -0,0 +1,125 @@ +module LookAbs where + +import Operations +import qualified GFC as C +import Abstract +import Ident + +import Modules + +import List (nub) +import Monad + +type GFCGrammar = C.CanonGrammar + +lookupAbsDef :: GFCGrammar -> Ident -> Ident -> Err (Maybe Term) +lookupAbsDef gr m c = do + mi <- lookupModule gr m + case mi of + ModMod mo -> do + info <- lookupInfo mo c + case info of + C.AbsFun _ t -> return $ return t + C.AnyInd _ n -> lookupAbsDef gr n c + _ -> return Nothing + _ -> Bad $ prt m +++ "is not an abstract module" + +lookupFunType :: GFCGrammar -> Ident -> Ident -> Err Type +lookupFunType gr m c = do + mi <- lookupModule gr m + case mi of + ModMod mo -> do + info <- lookupInfo mo c + case info of + C.AbsFun t _ -> return t + C.AnyInd _ n -> lookupFunType gr n c + _ -> prtBad "cannot find type of" c + _ -> Bad $ prt m +++ "is not an abstract module" + +lookupCatContext :: GFCGrammar -> Ident -> Ident -> Err Context +lookupCatContext gr m c = do + mi <- lookupModule gr m + case mi of + ModMod mo -> do + info <- lookupInfo mo c + case info of + C.AbsCat co _ -> return co + C.AnyInd _ n -> lookupCatContext gr n c + _ -> prtBad "unknown category" c + _ -> Bad $ prt m +++ "is not an abstract module" + +---- should be revised (20/9/2003) +isPrimitiveFun :: GFCGrammar -> Fun -> Bool +isPrimitiveFun gr (m,c) = case lookupAbsDef gr m c of + Ok (Just (Eqs [])) -> True -- is canonical + Ok (Just _) -> False -- has defining clauses + _ -> True -- has no definition + + +-- looking up refinement terms + +lookupRef :: GFCGrammar -> Binds -> Term -> Err Val +lookupRef gr binds at = case at of + Q m f -> lookupFunType gr m f >>= return . vClos + Vr i -> maybeErr ("unknown variable" +++ prt at) $ lookup i binds + _ -> prtBad "cannot refine with complex term" at --- + +refsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Binds -> Val -> [(Term,Val)] +refsForType compat gr binds val = + [(vr i, t) | (i,t) <- binds, Ok ty <- [val2exp t], compat val ty] ++ + [(qq f, vClos t) | (f,t) <- funsForType compat gr val] + + +funRulesOf :: GFCGrammar -> [(Fun,Type)] +funRulesOf gr = +---- funRulesForLiterals ++ + [((i,f),typ) | (i, ModMod m) <- modules gr, + mtype m == MTAbstract, + (f, C.AbsFun typ _) <- tree2list (jments m)] + +allCatsOf :: GFCGrammar -> [(Cat,Context)] +allCatsOf gr = + [((i,c),cont) | (i, ModMod m) <- modules gr, + isModAbs m, + (c, C.AbsCat cont _) <- tree2list (jments m)] + +funsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [(Fun,Type)] +funsForType compat gr val = [(fun,typ) | (fun,typ) <- funRulesOf gr, + compat val typ] + +funsOnType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [((Fun,Int),Type)] +funsOnType compat gr = funsOnTypeFs compat (funRulesOf gr) + +funsOnTypeFs :: (Val -> Type -> Bool) -> [(Fun,Type)] -> Val -> [((Fun,Int),Type)] +funsOnTypeFs compat fs val = [((fun,i),typ) | + (fun,typ) <- fs, + Ok (args,_,_) <- [typeForm typ], + (i,arg) <- zip [0..] (map snd args), + compat val arg] + + +-- this is needed at compile time + +lookupFunTypeSrc :: Grammar -> Ident -> Ident -> Err Type +lookupFunTypeSrc gr m c = do + mi <- lookupModule gr m + case mi of + ModMod mo -> do + info <- lookupInfo mo c + case info of + AbsFun (Yes t) _ -> return t + AnyInd _ n -> lookupFunTypeSrc gr n c + _ -> prtBad "cannot find type of" c + _ -> Bad $ prt m +++ "is not an abstract module" + +lookupCatContextSrc :: Grammar -> Ident -> Ident -> Err Context +lookupCatContextSrc gr m c = do + mi <- lookupModule gr m + case mi of + ModMod mo -> do + info <- lookupInfo mo c + case info of + AbsCat (Yes co) _ -> return co + AnyInd _ n -> lookupCatContextSrc gr n c + _ -> prtBad "unknown category" c + _ -> Bad $ prt m +++ "is not an abstract module" |
