mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
restructure ResParam and ResValue
This commit is contained in:
@@ -207,9 +207,9 @@ checkInfo gr (m,mo) c info = do
|
|||||||
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
|
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
|
||||||
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
||||||
|
|
||||||
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
|
ResParam (Just pcs) _ -> chIn "parameter type" $ do
|
||||||
ts <- checkErr $ lookupParamValues gr m c
|
ts <- checkErr $ lookupParamValues gr m c
|
||||||
return (ResParam (Just (pcs, Just ts)))
|
return (ResParam (Just pcs) (Just ts))
|
||||||
|
|
||||||
_ -> return info
|
_ -> return info
|
||||||
where
|
where
|
||||||
@@ -293,7 +293,7 @@ allDependencies ism b =
|
|||||||
opty _ = []
|
opty _ = []
|
||||||
pts i = case i of
|
pts i = case i of
|
||||||
ResOper pty pt -> [pty,pt]
|
ResOper pty pt -> [pty,pt]
|
||||||
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,_,t) <- cont]
|
ResParam (Just ps) _ -> [Just t | (_,cont) <- ps, (_,_,t) <- cont]
|
||||||
CncCat pty _ _ -> [pty]
|
CncCat pty _ _ -> [pty]
|
||||||
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
||||||
AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
|
AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
|
||||||
|
|||||||
@@ -309,8 +309,8 @@ canon2canon opts abs cg0 =
|
|||||||
|
|
||||||
-- flatten record arguments of param constructors
|
-- flatten record arguments of param constructors
|
||||||
p2p (f,j) = case j of
|
p2p (f,j) = case j of
|
||||||
ResParam (Just (ps,v)) ->
|
ResParam (Just ps) _ ->
|
||||||
ResParam (Just ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
|
ResParam (Just [(c,concatMap unRec cont) | (c,cont) <- ps]) Nothing
|
||||||
_ -> j
|
_ -> j
|
||||||
unRec (bt,x,ty) = case ty of
|
unRec (bt,x,ty) = case ty of
|
||||||
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)]
|
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)]
|
||||||
@@ -355,7 +355,7 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
ty <- typsFrom ty0
|
ty <- typsFrom ty0
|
||||||
] ++ [
|
] ++ [
|
||||||
Q m ty |
|
Q m ty |
|
||||||
(m,(ty,ResParam _)) <- jments
|
(m,(ty,ResParam _ _)) <- jments
|
||||||
] ++ [ty |
|
] ++ [ty |
|
||||||
(_,(_,CncFun _ (Just tr) _)) <- jments,
|
(_,(_,CncFun _ (Just tr) _)) <- jments,
|
||||||
ty <- err (const []) snd $ appSTM (typsFromTrm tr) []
|
ty <- err (const []) snd $ appSTM (typsFromTrm tr) []
|
||||||
|
|||||||
@@ -107,7 +107,7 @@ info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
|
|||||||
info2status mq (c,i) = case i of
|
info2status mq (c,i) = case i of
|
||||||
AbsFun _ _ Nothing -> maybe Con QC mq
|
AbsFun _ _ Nothing -> maybe Con QC mq
|
||||||
ResValue _ -> maybe Con QC mq
|
ResValue _ -> maybe Con QC mq
|
||||||
ResParam _ -> maybe Con QC mq
|
ResParam _ _ -> maybe Con QC mq
|
||||||
AnyInd True m -> maybe Con (const (QC m)) mq
|
AnyInd True m -> maybe Con (const (QC m)) mq
|
||||||
AnyInd False m -> maybe Cn (const (Q m)) mq
|
AnyInd False m -> maybe Cn (const (Q m)) mq
|
||||||
_ -> maybe Cn Q mq
|
_ -> maybe Cn Q mq
|
||||||
@@ -148,12 +148,12 @@ renameInfo mo status i info = checkIn
|
|||||||
ResOverload os tysts ->
|
ResOverload os tysts ->
|
||||||
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
||||||
|
|
||||||
ResParam (Just (pp,m)) -> do
|
ResParam (Just pp) m -> do
|
||||||
pp' <- mapM (renameParam status) pp
|
pp' <- mapM (renameParam status) pp
|
||||||
return $ ResParam $ Just (pp',m)
|
return (ResParam (Just pp') m)
|
||||||
ResValue (Just (t,m)) -> do
|
ResValue t -> do
|
||||||
t' <- rent t
|
t <- rent t
|
||||||
return $ ResValue $ Just (t',m)
|
return (ResValue t)
|
||||||
CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
|
CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
|
||||||
CncFun mt ptr ppr -> liftM2 (CncFun mt) (ren ptr) (ren ppr)
|
CncFun mt ptr ppr -> liftM2 (CncFun mt) (ren ptr) (ren ppr)
|
||||||
_ -> return info
|
_ -> return info
|
||||||
|
|||||||
@@ -162,7 +162,7 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
|
|||||||
indirInfo n info = AnyInd b n' where
|
indirInfo n info = AnyInd b n' where
|
||||||
(b,n') = case info of
|
(b,n') = case info of
|
||||||
ResValue _ -> (True,n)
|
ResValue _ -> (True,n)
|
||||||
ResParam _ -> (True,n)
|
ResParam _ _ -> (True,n)
|
||||||
AbsFun _ _ Nothing -> (True,n)
|
AbsFun _ _ Nothing -> (True,n)
|
||||||
AnyInd b k -> (b,k)
|
AnyInd b k -> (b,k)
|
||||||
_ -> (False,n) ---- canonical in Abs
|
_ -> (False,n) ---- canonical in Abs
|
||||||
@@ -174,9 +174,11 @@ unifyAnyInfo m i j = case (i,j) of
|
|||||||
(AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) ->
|
(AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) ->
|
||||||
liftM3 AbsFun (unifMaybe mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
|
liftM3 AbsFun (unifMaybe mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
|
||||||
|
|
||||||
(ResParam mt1, ResParam mt2) -> liftM ResParam $ unifMaybe mt1 mt2
|
(ResParam mt1 mv1, ResParam mt2 mv2) ->
|
||||||
(ResValue mt1, ResValue mt2) ->
|
liftM2 ResParam (unifMaybe mt1 mt2) (unifMaybe mv1 mv2)
|
||||||
liftM ResValue $ unifMaybe mt1 mt2
|
(ResValue t1, ResValue t2)
|
||||||
|
| t1==t2 -> return (ResValue t1)
|
||||||
|
| otherwise -> fail ""
|
||||||
(_, ResOverload ms t) | elem m ms ->
|
(_, ResOverload ms t) | elem m ms ->
|
||||||
return $ ResOverload ms t
|
return $ ResOverload ms t
|
||||||
(ResOper mt1 m1, ResOper mt2 m2) ->
|
(ResOper mt1 m1, ResOper mt2 m2) ->
|
||||||
|
|||||||
@@ -89,7 +89,7 @@ instance Binary Options where
|
|||||||
instance Binary Info where
|
instance Binary Info where
|
||||||
put (AbsCat x y) = putWord8 0 >> put (x,y)
|
put (AbsCat x y) = putWord8 0 >> put (x,y)
|
||||||
put (AbsFun x y z) = putWord8 1 >> put (x,y,z)
|
put (AbsFun x y z) = putWord8 1 >> put (x,y,z)
|
||||||
put (ResParam x) = putWord8 2 >> put x
|
put (ResParam x y) = putWord8 2 >> put (x,y)
|
||||||
put (ResValue x) = putWord8 3 >> put x
|
put (ResValue x) = putWord8 3 >> put x
|
||||||
put (ResOper x y) = putWord8 4 >> put (x,y)
|
put (ResOper x y) = putWord8 4 >> put (x,y)
|
||||||
put (ResOverload x y)= putWord8 5 >> put (x,y)
|
put (ResOverload x y)= putWord8 5 >> put (x,y)
|
||||||
@@ -100,7 +100,7 @@ instance Binary Info where
|
|||||||
case tag of
|
case tag of
|
||||||
0 -> get >>= \(x,y) -> return (AbsCat x y)
|
0 -> get >>= \(x,y) -> return (AbsCat x y)
|
||||||
1 -> get >>= \(x,y,z) -> return (AbsFun x y z)
|
1 -> get >>= \(x,y,z) -> return (AbsFun x y z)
|
||||||
2 -> get >>= \x -> return (ResParam x)
|
2 -> get >>= \(x,y) -> return (ResParam x y)
|
||||||
3 -> get >>= \x -> return (ResValue x)
|
3 -> get >>= \x -> return (ResValue x)
|
||||||
4 -> get >>= \(x,y) -> return (ResOper x y)
|
4 -> get >>= \(x,y) -> return (ResOper x y)
|
||||||
5 -> get >>= \(x,y) -> return (ResOverload x y)
|
5 -> get >>= \(x,y) -> return (ResOverload x y)
|
||||||
@@ -122,72 +122,72 @@ instance Binary Term where
|
|||||||
put (Vr x) = putWord8 0 >> put x
|
put (Vr x) = putWord8 0 >> put x
|
||||||
put (Cn x) = putWord8 1 >> put x
|
put (Cn x) = putWord8 1 >> put x
|
||||||
put (Con x) = putWord8 2 >> put x
|
put (Con x) = putWord8 2 >> put x
|
||||||
put (Sort x) = putWord8 4 >> put x
|
put (Sort x) = putWord8 3 >> put x
|
||||||
put (EInt x) = putWord8 5 >> put x
|
put (EInt x) = putWord8 4 >> put x
|
||||||
put (EFloat x) = putWord8 6 >> put x
|
put (EFloat x) = putWord8 5 >> put x
|
||||||
put (K x) = putWord8 7 >> put x
|
put (K x) = putWord8 6 >> put x
|
||||||
put (Empty) = putWord8 8
|
put (Empty) = putWord8 7
|
||||||
put (App x y) = putWord8 9 >> put (x,y)
|
put (App x y) = putWord8 8 >> put (x,y)
|
||||||
put (Abs x y z) = putWord8 10 >> put (x,y,z)
|
put (Abs x y z) = putWord8 9 >> put (x,y,z)
|
||||||
put (Meta x) = putWord8 11 >> put x
|
put (Meta x) = putWord8 10 >> put x
|
||||||
put (Prod w x y z)= putWord8 12 >> put (w,x,y,z)
|
put (Prod w x y z)= putWord8 11 >> put (w,x,y,z)
|
||||||
put (Typed x y) = putWord8 14 >> put (x,y)
|
put (Typed x y) = putWord8 12 >> put (x,y)
|
||||||
put (Example x y) = putWord8 15 >> put (x,y)
|
put (Example x y) = putWord8 13 >> put (x,y)
|
||||||
put (RecType x) = putWord8 16 >> put x
|
put (RecType x) = putWord8 14 >> put x
|
||||||
put (R x) = putWord8 17 >> put x
|
put (R x) = putWord8 15 >> put x
|
||||||
put (P x y) = putWord8 18 >> put (x,y)
|
put (P x y) = putWord8 16 >> put (x,y)
|
||||||
put (ExtR x y) = putWord8 20 >> put (x,y)
|
put (ExtR x y) = putWord8 17 >> put (x,y)
|
||||||
put (Table x y) = putWord8 21 >> put (x,y)
|
put (Table x y) = putWord8 18 >> put (x,y)
|
||||||
put (T x y) = putWord8 22 >> put (x,y)
|
put (T x y) = putWord8 19 >> put (x,y)
|
||||||
put (V x y) = putWord8 24 >> put (x,y)
|
put (V x y) = putWord8 20 >> put (x,y)
|
||||||
put (S x y) = putWord8 25 >> put (x,y)
|
put (S x y) = putWord8 21 >> put (x,y)
|
||||||
put (Let x y) = putWord8 27 >> put (x,y)
|
put (Let x y) = putWord8 22 >> put (x,y)
|
||||||
put (Q x y) = putWord8 29 >> put (x,y)
|
put (Q x y) = putWord8 23 >> put (x,y)
|
||||||
put (QC x y) = putWord8 30 >> put (x,y)
|
put (QC x y) = putWord8 24 >> put (x,y)
|
||||||
put (C x y) = putWord8 31 >> put (x,y)
|
put (C x y) = putWord8 25 >> put (x,y)
|
||||||
put (Glue x y) = putWord8 32 >> put (x,y)
|
put (Glue x y) = putWord8 26 >> put (x,y)
|
||||||
put (EPatt x) = putWord8 33 >> put x
|
put (EPatt x) = putWord8 27 >> put x
|
||||||
put (EPattType x) = putWord8 34 >> put x
|
put (EPattType x) = putWord8 28 >> put x
|
||||||
put (FV x) = putWord8 35 >> put x
|
put (FV x) = putWord8 29 >> put x
|
||||||
put (Alts x) = putWord8 36 >> put x
|
put (Alts x) = putWord8 30 >> put x
|
||||||
put (Strs x) = putWord8 37 >> put x
|
put (Strs x) = putWord8 31 >> put x
|
||||||
put (ELin x y) = putWord8 38 >> put (x,y)
|
put (ELin x y) = putWord8 32 >> put (x,y)
|
||||||
|
|
||||||
get = do tag <- getWord8
|
get = do tag <- getWord8
|
||||||
case tag of
|
case tag of
|
||||||
0 -> get >>= \x -> return (Vr x)
|
0 -> get >>= \x -> return (Vr x)
|
||||||
1 -> get >>= \x -> return (Cn x)
|
1 -> get >>= \x -> return (Cn x)
|
||||||
2 -> get >>= \x -> return (Con x)
|
2 -> get >>= \x -> return (Con x)
|
||||||
4 -> get >>= \x -> return (Sort x)
|
3 -> get >>= \x -> return (Sort x)
|
||||||
5 -> get >>= \x -> return (EInt x)
|
4 -> get >>= \x -> return (EInt x)
|
||||||
6 -> get >>= \x -> return (EFloat x)
|
5 -> get >>= \x -> return (EFloat x)
|
||||||
7 -> get >>= \x -> return (K x)
|
6 -> get >>= \x -> return (K x)
|
||||||
8 -> return (Empty)
|
7 -> return (Empty)
|
||||||
9 -> get >>= \(x,y) -> return (App x y)
|
8 -> get >>= \(x,y) -> return (App x y)
|
||||||
10 -> get >>= \(x,y,z) -> return (Abs x y z)
|
9 -> get >>= \(x,y,z) -> return (Abs x y z)
|
||||||
11 -> get >>= \x -> return (Meta x)
|
10 -> get >>= \x -> return (Meta x)
|
||||||
12 -> get >>= \(w,x,y,z)->return (Prod w x y z)
|
11 -> get >>= \(w,x,y,z)->return (Prod w x y z)
|
||||||
14 -> get >>= \(x,y) -> return (Typed x y)
|
12 -> get >>= \(x,y) -> return (Typed x y)
|
||||||
15 -> get >>= \(x,y) -> return (Example x y)
|
13 -> get >>= \(x,y) -> return (Example x y)
|
||||||
16 -> get >>= \x -> return (RecType x)
|
14 -> get >>= \x -> return (RecType x)
|
||||||
17 -> get >>= \x -> return (R x)
|
15 -> get >>= \x -> return (R x)
|
||||||
18 -> get >>= \(x,y) -> return (P x y)
|
16 -> get >>= \(x,y) -> return (P x y)
|
||||||
20 -> get >>= \(x,y) -> return (ExtR x y)
|
17 -> get >>= \(x,y) -> return (ExtR x y)
|
||||||
21 -> get >>= \(x,y) -> return (Table x y)
|
18 -> get >>= \(x,y) -> return (Table x y)
|
||||||
22 -> get >>= \(x,y) -> return (T x y)
|
19 -> get >>= \(x,y) -> return (T x y)
|
||||||
24 -> get >>= \(x,y) -> return (V x y)
|
20 -> get >>= \(x,y) -> return (V x y)
|
||||||
25 -> get >>= \(x,y) -> return (S x y)
|
21 -> get >>= \(x,y) -> return (S x y)
|
||||||
27 -> get >>= \(x,y) -> return (Let x y)
|
22 -> get >>= \(x,y) -> return (Let x y)
|
||||||
29 -> get >>= \(x,y) -> return (Q x y)
|
23 -> get >>= \(x,y) -> return (Q x y)
|
||||||
30 -> get >>= \(x,y) -> return (QC x y)
|
24 -> get >>= \(x,y) -> return (QC x y)
|
||||||
31 -> get >>= \(x,y) -> return (C x y)
|
25 -> get >>= \(x,y) -> return (C x y)
|
||||||
32 -> get >>= \(x,y) -> return (Glue x y)
|
26 -> get >>= \(x,y) -> return (Glue x y)
|
||||||
33 -> get >>= \x -> return (EPatt x)
|
27 -> get >>= \x -> return (EPatt x)
|
||||||
34 -> get >>= \x -> return (EPattType x)
|
28 -> get >>= \x -> return (EPattType x)
|
||||||
35 -> get >>= \x -> return (FV x)
|
29 -> get >>= \x -> return (FV x)
|
||||||
36 -> get >>= \x -> return (Alts x)
|
30 -> get >>= \x -> return (Alts x)
|
||||||
37 -> get >>= \x -> return (Strs x)
|
31 -> get >>= \x -> return (Strs x)
|
||||||
38 -> get >>= \(x,y) -> return (ELin x y)
|
32 -> get >>= \(x,y) -> return (ELin x y)
|
||||||
_ -> decodingError
|
_ -> decodingError
|
||||||
|
|
||||||
instance Binary Patt where
|
instance Binary Patt where
|
||||||
|
|||||||
@@ -20,7 +20,6 @@ module GF.Grammar.Grammar (SourceGrammar,
|
|||||||
SourceModule,
|
SourceModule,
|
||||||
mapSourceModule,
|
mapSourceModule,
|
||||||
Info(..),
|
Info(..),
|
||||||
PValues,
|
|
||||||
Type,
|
Type,
|
||||||
Cat,
|
Cat,
|
||||||
Fun,
|
Fun,
|
||||||
@@ -37,7 +36,6 @@ module GF.Grammar.Grammar (SourceGrammar,
|
|||||||
Labelling,
|
Labelling,
|
||||||
Assign,
|
Assign,
|
||||||
Case,
|
Case,
|
||||||
Cases,
|
|
||||||
LocalDef,
|
LocalDef,
|
||||||
Param,
|
Param,
|
||||||
Altern,
|
Altern,
|
||||||
@@ -66,9 +64,6 @@ type SourceModule = (Ident, SourceModInfo)
|
|||||||
mapSourceModule :: (SourceModInfo -> SourceModInfo) -> (SourceModule -> SourceModule)
|
mapSourceModule :: (SourceModInfo -> SourceModInfo) -> (SourceModule -> SourceModule)
|
||||||
mapSourceModule f (i,mi) = (i, f mi)
|
mapSourceModule f (i,mi) = (i, f mi)
|
||||||
|
|
||||||
-- this is created in CheckGrammar, and so are Val and PVal
|
|
||||||
type PValues = [Term]
|
|
||||||
|
|
||||||
-- | the constructors are judgements in
|
-- | the constructors are judgements in
|
||||||
--
|
--
|
||||||
-- - abstract syntax (/ABS/)
|
-- - abstract syntax (/ABS/)
|
||||||
@@ -84,8 +79,8 @@ data Info =
|
|||||||
| AbsFun (Maybe Type) (Maybe Int) (Maybe [Equation]) -- ^ (/ABS/) type, arrity and definition of function
|
| AbsFun (Maybe Type) (Maybe Int) (Maybe [Equation]) -- ^ (/ABS/) type, arrity and definition of function
|
||||||
|
|
||||||
-- judgements in resource
|
-- judgements in resource
|
||||||
| ResParam (Maybe ([Param],Maybe PValues)) -- ^ (/RES/)
|
| ResParam (Maybe [Param]) (Maybe [Term]) -- ^ (/RES/) the second parameter is list of all possible values
|
||||||
| ResValue (Maybe (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
| ResValue Type -- ^ (/RES/) to mark parameter constructors for lookup
|
||||||
| ResOper (Maybe Type) (Maybe Term) -- ^ (/RES/)
|
| ResOper (Maybe Type) (Maybe Term) -- ^ (/RES/)
|
||||||
|
|
||||||
| ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited
|
| ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited
|
||||||
|
|||||||
@@ -33,8 +33,7 @@ module GF.Grammar.Lookup (
|
|||||||
lookupAbsDef,
|
lookupAbsDef,
|
||||||
lookupLincat,
|
lookupLincat,
|
||||||
lookupFunType,
|
lookupFunType,
|
||||||
lookupCatContext,
|
lookupCatContext
|
||||||
opersForType
|
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
@@ -93,7 +92,7 @@ lookupResDefKind gr m c
|
|||||||
CncFun _ (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
|
CncFun _ (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
|
||||||
|
|
||||||
AnyInd _ n -> look False n c
|
AnyInd _ n -> look False n c
|
||||||
ResParam _ -> return (QC m c,2)
|
ResParam _ _ -> return (QC m c,2)
|
||||||
ResValue _ -> return (QC m c,2)
|
ResValue _ -> return (QC m c,2)
|
||||||
_ -> Bad $ render (ppIdent c <+> text "is not defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppIdent c <+> text "is not defined in resource" <+> ppIdent m)
|
||||||
lookExt m c =
|
lookExt m c =
|
||||||
@@ -113,8 +112,8 @@ lookupResType gr m c = do
|
|||||||
return $ mkProd cont val' []
|
return $ mkProd cont val' []
|
||||||
CncFun _ _ _ -> lookFunType m m c
|
CncFun _ _ _ -> lookFunType m m c
|
||||||
AnyInd _ n -> lookupResType gr n c
|
AnyInd _ n -> lookupResType gr n c
|
||||||
ResParam _ -> return $ typePType
|
ResParam _ _ -> return $ typePType
|
||||||
ResValue (Just (t,_)) -> return $ qualifAnnotPar m t
|
ResValue t -> return $ qualifAnnotPar m t
|
||||||
_ -> Bad $ render (ppIdent c <+> text "has no type defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppIdent c <+> text "has no type defined in resource" <+> ppIdent m)
|
||||||
where
|
where
|
||||||
lookFunType e m c = do
|
lookFunType e m c = do
|
||||||
@@ -152,15 +151,15 @@ lookupOrigInfo gr m c = do
|
|||||||
AnyInd _ n -> lookupOrigInfo gr n c
|
AnyInd _ n -> lookupOrigInfo gr n c
|
||||||
i -> return (m,i)
|
i -> return (m,i)
|
||||||
|
|
||||||
lookupParams :: SourceGrammar -> Ident -> Ident -> Err ([Param],Maybe PValues)
|
lookupParams :: SourceGrammar -> Ident -> Ident -> Err ([Param],Maybe [Term])
|
||||||
lookupParams gr = look True where
|
lookupParams gr = look True where
|
||||||
look isTop m c = do
|
look isTop m c = do
|
||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
ResParam (Just psm) -> return psm
|
ResParam (Just psm) m -> return (psm,m)
|
||||||
AnyInd _ n -> look False n c
|
AnyInd _ n -> look False n c
|
||||||
_ -> Bad $ render (ppIdent c <+> text "has no parameters defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppIdent c <+> text "has no parameters defined in resource" <+> ppIdent m)
|
||||||
lookExt m c =
|
lookExt m c =
|
||||||
checks [look False n c | n <- allExtensions gr m]
|
checks [look False n c | n <- allExtensions gr m]
|
||||||
|
|
||||||
@@ -261,22 +260,3 @@ lookupCatContext gr m c = do
|
|||||||
AbsCat (Just co) _ -> return co
|
AbsCat (Just co) _ -> return co
|
||||||
AnyInd _ n -> lookupCatContext gr n c
|
AnyInd _ n -> lookupCatContext gr n c
|
||||||
_ -> Bad (render (text "unknown category" <+> ppIdent c))
|
_ -> Bad (render (text "unknown category" <+> ppIdent c))
|
||||||
|
|
||||||
-- The first type argument is uncomputed, usually a category symbol.
|
|
||||||
-- This is a hack to find implicit (= reused) opers.
|
|
||||||
|
|
||||||
opersForType :: SourceGrammar -> Type -> Type -> [(QIdent,Term)]
|
|
||||||
opersForType gr orig val =
|
|
||||||
[((i,f),ty) | (i,m) <- modules gr, (f,ty) <- opers i m val] where
|
|
||||||
opers i m val =
|
|
||||||
[(f,ty) |
|
|
||||||
(f,ResOper (Just ty) _) <- tree2list $ jments m,
|
|
||||||
elem (valTypeCnc ty) [val,orig]
|
|
||||||
] ++
|
|
||||||
let cat = snd (valCat orig) in --- ignore module
|
|
||||||
[(f,ty) |
|
|
||||||
Ok a <- [abstractOfConcrete gr i >>= lookupModule gr],
|
|
||||||
(f, AbsFun (Just ty0) _ _) <- tree2list $ jments a,
|
|
||||||
let ty = redirectTerm i ty0,
|
|
||||||
cat == snd (valCat ty) ---
|
|
||||||
]
|
|
||||||
|
|||||||
@@ -254,9 +254,9 @@ DataDef
|
|||||||
|
|
||||||
ParamDef :: { [(Ident,SrcSpan,Info)] }
|
ParamDef :: { [(Ident,SrcSpan,Info)] }
|
||||||
ParamDef
|
ParamDef
|
||||||
: Posn Ident '=' ListParConstr Posn { ($2, ($1,$5), ResParam (Just ($4,Nothing))) :
|
: Posn Ident '=' ListParConstr Posn { ($2, ($1,$5), ResParam (Just $4) Nothing) :
|
||||||
[(f, ($1,$5), ResValue (Just (mkProdSimple co (Cn $2),Nothing))) | (f,co) <- $4] }
|
[(f, ($1,$5), ResValue (mkProdSimple co (Cn $2))) | (f,co) <- $4] }
|
||||||
| Posn Ident Posn { [($2, ($1,$3), ResParam Nothing)] }
|
| Posn Ident Posn { [($2, ($1,$3), ResParam Nothing Nothing)] }
|
||||||
|
|
||||||
OperDef :: { [(Ident,SrcSpan,Info)] }
|
OperDef :: { [(Ident,SrcSpan,Info)] }
|
||||||
OperDef
|
OperDef
|
||||||
@@ -684,14 +684,14 @@ checkInfoType MTAbstract (id,pos,info) =
|
|||||||
_ -> failLoc (fst pos) "illegal definition in abstract module"
|
_ -> failLoc (fst pos) "illegal definition in abstract module"
|
||||||
checkInfoType MTResource (id,pos,info) =
|
checkInfoType MTResource (id,pos,info) =
|
||||||
case info of
|
case info of
|
||||||
ResParam _ -> return ()
|
ResParam _ _ -> return ()
|
||||||
ResValue _ -> return ()
|
ResValue _ -> return ()
|
||||||
ResOper _ _ -> return ()
|
ResOper _ _ -> return ()
|
||||||
ResOverload _ _ -> return ()
|
ResOverload _ _ -> return ()
|
||||||
_ -> failLoc (fst pos) "illegal definition in resource module"
|
_ -> failLoc (fst pos) "illegal definition in resource module"
|
||||||
checkInfoType MTInterface (id,pos,info) =
|
checkInfoType MTInterface (id,pos,info) =
|
||||||
case info of
|
case info of
|
||||||
ResParam _ -> return ()
|
ResParam _ _ -> return ()
|
||||||
ResValue _ -> return ()
|
ResValue _ -> return ()
|
||||||
ResOper _ _ -> return ()
|
ResOper _ _ -> return ()
|
||||||
ResOverload _ _ -> return ()
|
ResOverload _ _ -> return ()
|
||||||
@@ -700,14 +700,14 @@ checkInfoType (MTConcrete _) (id,pos,info) =
|
|||||||
case info of
|
case info of
|
||||||
CncCat _ _ _ -> return ()
|
CncCat _ _ _ -> return ()
|
||||||
CncFun _ _ _ -> return ()
|
CncFun _ _ _ -> return ()
|
||||||
ResParam _ -> return ()
|
ResParam _ _ -> return ()
|
||||||
ResValue _ -> return ()
|
ResValue _ -> return ()
|
||||||
ResOper _ _ -> return ()
|
ResOper _ _ -> return ()
|
||||||
ResOverload _ _ -> return ()
|
ResOverload _ _ -> return ()
|
||||||
_ -> failLoc (fst pos) "illegal definition in concrete module"
|
_ -> failLoc (fst pos) "illegal definition in concrete module"
|
||||||
checkInfoType (MTInstance _) (id,pos,info) =
|
checkInfoType (MTInstance _) (id,pos,info) =
|
||||||
case info of
|
case info of
|
||||||
ResParam _ -> return ()
|
ResParam _ _ -> return ()
|
||||||
ResValue _ -> return ()
|
ResValue _ -> return ()
|
||||||
ResOper _ _ -> return ()
|
ResOper _ _ -> return ()
|
||||||
_ -> failLoc (fst pos) "illegal definition in instance module"
|
_ -> failLoc (fst pos) "illegal definition in instance module"
|
||||||
|
|||||||
@@ -91,11 +91,11 @@ ppJudgement q (id, AbsFun ptype _ pexp) =
|
|||||||
Just [] -> empty
|
Just [] -> empty
|
||||||
Just eqs -> text "def" <+> vcat [ppIdent id <+> hsep (map (ppPatt q 2) ps) <+> equals <+> ppTerm q 0 e <+> semi | (ps,e) <- eqs]
|
Just eqs -> text "def" <+> vcat [ppIdent id <+> hsep (map (ppPatt q 2) ps) <+> equals <+> ppTerm q 0 e <+> semi | (ps,e) <- eqs]
|
||||||
Nothing -> empty)
|
Nothing -> empty)
|
||||||
ppJudgement q (id, ResParam pparams) =
|
ppJudgement q (id, ResParam pparams _) =
|
||||||
text "param" <+> ppIdent id <+>
|
text "param" <+> ppIdent id <+>
|
||||||
(case pparams of
|
(case pparams of
|
||||||
Just (ps,_) -> equals <+> fsep (intersperse (char '|') (map (ppParam q) ps))
|
Just ps -> equals <+> fsep (intersperse (char '|') (map (ppParam q) ps))
|
||||||
_ -> empty) <+> semi
|
_ -> empty) <+> semi
|
||||||
ppJudgement q (id, ResValue pvalue) = empty
|
ppJudgement q (id, ResValue pvalue) = empty
|
||||||
ppJudgement q (id, ResOper ptype pexp) =
|
ppJudgement q (id, ResOper ptype pexp) =
|
||||||
text "oper" <+> ppIdent id <+>
|
text "oper" <+> ppIdent id <+>
|
||||||
|
|||||||
Reference in New Issue
Block a user