forked from GitHub/gf-core
Compare commits
7 Commits
c-runtime
...
compact-pg
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
320ead943c | ||
|
|
529635e0e9 | ||
|
|
9e3512db81 | ||
|
|
e989cc69a2 | ||
|
|
5c5af8df79 | ||
|
|
400aad1d07 | ||
|
|
12912299be |
@@ -259,18 +259,30 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
||||||
|
|
||||||
ResParam (Just (L loc pcs)) _ -> do
|
ResParam (Just (L loc pcs)) _ -> do
|
||||||
ts <- chIn loc "parameter type" $
|
(vs,pcs) <- chIn loc "parameter type" $
|
||||||
liftM concat $ mapM mkPar pcs
|
mkParams 0 [] pcs
|
||||||
return (ResParam (Just (L loc pcs)) (Just ts))
|
return (ResParam (Just (L loc pcs)) (Just vs))
|
||||||
|
|
||||||
|
ResValue (L loc ty) _ ->
|
||||||
|
chIn loc "operation" $ do
|
||||||
|
let (_,Cn x) = typeFormCnc ty
|
||||||
|
is = case Map.lookup x (jments mo) of
|
||||||
|
Just (ResParam (Just (L _ pcs)) _) -> [i | (f,_,i) <- pcs, f == c]
|
||||||
|
_ -> []
|
||||||
|
case is of
|
||||||
|
[i] -> return (ResValue (L loc ty) i)
|
||||||
|
_ -> checkError (pp "Failed to find the value index for parameter" <+> pp c)
|
||||||
|
|
||||||
_ -> return info
|
_ -> return info
|
||||||
where
|
where
|
||||||
gr = prependModule sgr (m,mo)
|
gr = prependModule sgr (m,mo)
|
||||||
chIn loc cat = checkInModule cwd mo loc ("Happened in" <+> cat <+> c)
|
chIn loc cat = checkInModule cwd mo loc ("Happened in" <+> cat <+> c)
|
||||||
|
|
||||||
mkPar (f,co) = do
|
mkParams i vs [] = return (vs,[])
|
||||||
vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
|
mkParams i vs ((f,co,_):pcs) = do
|
||||||
return $ map (mkApp (QC (m,f))) vs
|
vs0 <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
|
||||||
|
(vs,pcs) <- mkParams (i + length vs0) (vs ++ map (mkApp (QC (m,f))) vs0) pcs
|
||||||
|
return (vs,(f,co,i):pcs)
|
||||||
|
|
||||||
checkUniq xss = case xss of
|
checkUniq xss = case xss of
|
||||||
x:y:xs
|
x:y:xs
|
||||||
|
|||||||
@@ -353,9 +353,9 @@ paramType gr q@(_,n) =
|
|||||||
[ParamAliasDef ((gQId m n)) (convType t)])
|
[ParamAliasDef ((gQId m n)) (convType t)])
|
||||||
_ -> ((S.empty,S.empty),[])
|
_ -> ((S.empty,S.empty),[])
|
||||||
where
|
where
|
||||||
param m (n,ctx) = Param ((gQId m n)) [toParamId t|(_,_,t)<-ctx]
|
param m (n,ctx,_) = Param ((gQId m n)) [toParamId t|(_,_,t)<-ctx]
|
||||||
argTypes = S.unions . map argTypes1
|
argTypes = S.unions . map argTypes1
|
||||||
argTypes1 (n,ctx) = S.unions [paramTypes gr t|(_,_,t)<-ctx]
|
argTypes1 (n,ctx,_) = S.unions [paramTypes gr t|(_,_,t)<-ctx]
|
||||||
|
|
||||||
lblId = LabelId . render -- hmm
|
lblId = LabelId . render -- hmm
|
||||||
modId (MN m) = ModId (showIdent m)
|
modId (MN m) = ModId (showIdent m)
|
||||||
|
|||||||
@@ -110,7 +110,7 @@ renameIdentTerm' env@(act,imps) t0 =
|
|||||||
info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
|
info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
|
||||||
info2status mq c i = case i of
|
info2status mq c i = case i of
|
||||||
AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq
|
AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq
|
||||||
ResValue _ -> maybe Con (curry QC) mq
|
ResValue _ _ -> maybe Con (curry QC) mq
|
||||||
ResParam _ _ -> maybe Con (curry QC) mq
|
ResParam _ _ -> maybe Con (curry QC) mq
|
||||||
AnyInd True m -> maybe Con (const (curry QC m)) mq
|
AnyInd True m -> maybe Con (const (curry QC m)) mq
|
||||||
AnyInd False m -> maybe Cn (const (curry Q m)) mq
|
AnyInd False m -> maybe Cn (const (curry Q m)) mq
|
||||||
@@ -148,9 +148,9 @@ renameInfo cwd status (m,mi) i info =
|
|||||||
ResParam (Just pp) m -> do
|
ResParam (Just pp) m -> do
|
||||||
pp' <- renLoc (mapM (renParam status)) pp
|
pp' <- renLoc (mapM (renParam status)) pp
|
||||||
return (ResParam (Just pp') m)
|
return (ResParam (Just pp') m)
|
||||||
ResValue t -> do
|
ResValue ty offset -> do
|
||||||
t <- renLoc (renameTerm status []) t
|
t <- renLoc (renameTerm status []) ty
|
||||||
return (ResValue t)
|
return (ResValue ty offset)
|
||||||
CncCat mcat mdef mref mpr mpmcfg -> liftM5 CncCat (renTerm mcat) (renTerm mdef) (renTerm mref) (renTerm mpr) (return mpmcfg)
|
CncCat mcat mdef mref mpr mpmcfg -> liftM5 CncCat (renTerm mcat) (renTerm mdef) (renTerm mref) (renTerm mpr) (return mpmcfg)
|
||||||
CncFun mty mtr mpr mpmcfg -> liftM3 (CncFun mty) (renTerm mtr) (renTerm mpr) (return mpmcfg)
|
CncFun mty mtr mpr mpmcfg -> liftM3 (CncFun mty) (renTerm mtr) (renTerm mpr) (return mpmcfg)
|
||||||
_ -> return info
|
_ -> return info
|
||||||
@@ -178,9 +178,9 @@ renameInfo cwd status (m,mi) i info =
|
|||||||
return (ps',t')
|
return (ps',t')
|
||||||
|
|
||||||
renParam :: Status -> Param -> Check Param
|
renParam :: Status -> Param -> Check Param
|
||||||
renParam env (c,co) = do
|
renParam env (c,co,i) = do
|
||||||
co' <- renameContext env co
|
co' <- renameContext env co
|
||||||
return (c,co')
|
return (c,co',i)
|
||||||
|
|
||||||
renameTerm :: Status -> [Ident] -> Term -> Check Term
|
renameTerm :: Status -> [Ident] -> Term -> Check Term
|
||||||
renameTerm env vars = ren vars where
|
renameTerm env vars = ren vars where
|
||||||
|
|||||||
@@ -31,7 +31,7 @@ getLocalTags x (m,mi) =
|
|||||||
getLocations (AbsFun mb_type _ mb_eqs _) = maybe (ltype "fun") mb_type ++
|
getLocations (AbsFun mb_type _ mb_eqs _) = maybe (ltype "fun") mb_type ++
|
||||||
maybe (list (loc "def")) mb_eqs
|
maybe (list (loc "def")) mb_eqs
|
||||||
getLocations (ResParam mb_params _) = maybe (loc "param") mb_params
|
getLocations (ResParam mb_params _) = maybe (loc "param") mb_params
|
||||||
getLocations (ResValue mb_type) = ltype "param-value" mb_type
|
getLocations (ResValue mb_type _) = ltype "param-value" mb_type
|
||||||
getLocations (ResOper mb_type mb_def) = maybe (ltype "oper-type") mb_type ++
|
getLocations (ResOper mb_type mb_def) = maybe (ltype "oper-type") mb_type ++
|
||||||
maybe (loc "oper-def") mb_def
|
maybe (loc "oper-def") mb_def
|
||||||
getLocations (ResOverload _ defs) = list (\(x,y) -> ltype "overload-type" x ++
|
getLocations (ResOverload _ defs) = list (\(x,y) -> ltype "overload-type" x ++
|
||||||
|
|||||||
@@ -8,7 +8,7 @@ typPredefined :: Ident -> Maybe Type
|
|||||||
typPredefined f = case Map.lookup f primitives of
|
typPredefined f = case Map.lookup f primitives of
|
||||||
Just (ResOper (Just (L _ ty)) _) -> Just ty
|
Just (ResOper (Just (L _ ty)) _) -> Just ty
|
||||||
Just (ResParam _ _) -> Just typePType
|
Just (ResParam _ _) -> Just typePType
|
||||||
Just (ResValue (L _ ty)) -> Just ty
|
Just (ResValue (L _ ty) _) -> Just ty
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
|
|
||||||
primitives = Map.fromList
|
primitives = Map.fromList
|
||||||
@@ -16,9 +16,9 @@ primitives = Map.fromList
|
|||||||
, (cInt , ResOper (Just (noLoc typePType)) Nothing)
|
, (cInt , ResOper (Just (noLoc typePType)) Nothing)
|
||||||
, (cFloat , ResOper (Just (noLoc typePType)) Nothing)
|
, (cFloat , ResOper (Just (noLoc typePType)) Nothing)
|
||||||
, (cInts , fun [typeInt] typePType)
|
, (cInts , fun [typeInt] typePType)
|
||||||
, (cPBool , ResParam (Just (noLoc [(cPTrue,[]),(cPFalse,[])])) (Just [QC (cPredef,cPTrue), QC (cPredef,cPFalse)]))
|
, (cPBool , ResParam (Just (noLoc [(cPTrue,[],0),(cPFalse,[],1)])) (Just [QC (cPredef,cPTrue), QC (cPredef,cPFalse)]))
|
||||||
, (cPTrue , ResValue (noLoc typePBool))
|
, (cPTrue , ResValue (noLoc typePBool) 0)
|
||||||
, (cPFalse , ResValue (noLoc typePBool))
|
, (cPFalse , ResValue (noLoc typePBool) 1)
|
||||||
, (cError , fun [typeStr] typeError) -- non-can. of empty set
|
, (cError , fun [typeStr] typeError) -- non-can. of empty set
|
||||||
, (cLength , fun [typeTok] typeInt)
|
, (cLength , fun [typeTok] typeInt)
|
||||||
, (cDrop , fun [typeInt,typeTok] typeTok)
|
, (cDrop , fun [typeInt,typeTok] typeTok)
|
||||||
|
|||||||
@@ -166,7 +166,7 @@ extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jme
|
|||||||
indirInfo :: ModuleName -> Info -> Info
|
indirInfo :: ModuleName -> Info -> Info
|
||||||
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)
|
||||||
@@ -177,7 +177,7 @@ globalizeLoc fpath i =
|
|||||||
AbsCat mc -> AbsCat (fmap gl mc)
|
AbsCat mc -> AbsCat (fmap gl mc)
|
||||||
AbsFun mt ma md moper -> AbsFun (fmap gl mt) ma (fmap (fmap gl) md) moper
|
AbsFun mt ma md moper -> AbsFun (fmap gl mt) ma (fmap (fmap gl) md) moper
|
||||||
ResParam mt mv -> ResParam (fmap gl mt) mv
|
ResParam mt mv -> ResParam (fmap gl mt) mv
|
||||||
ResValue t -> ResValue (gl t)
|
ResValue t offset -> ResValue (gl t) offset
|
||||||
ResOper mt m -> ResOper (fmap gl mt) (fmap gl m)
|
ResOper mt m -> ResOper (fmap gl mt) (fmap gl m)
|
||||||
ResOverload ms os -> ResOverload ms (map (\(x,y) -> (gl x,gl y)) os)
|
ResOverload ms os -> ResOverload ms (map (\(x,y) -> (gl x,gl y)) os)
|
||||||
CncCat mc md mr mp mpmcfg-> CncCat (fmap gl mc) (fmap gl md) (fmap gl mr) (fmap gl mp) mpmcfg
|
CncCat mc md mr mp mpmcfg-> CncCat (fmap gl mc) (fmap gl md) (fmap gl mr) (fmap gl mp) mpmcfg
|
||||||
@@ -199,9 +199,9 @@ unifyAnyInfo m i j = case (i,j) of
|
|||||||
|
|
||||||
(ResParam mt1 mv1, ResParam mt2 mv2) ->
|
(ResParam mt1 mv1, ResParam mt2 mv2) ->
|
||||||
liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
|
liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
|
||||||
(ResValue (L l1 t1), ResValue (L l2 t2))
|
(ResValue (L l1 t1) i1, ResValue (L l2 t2) i2)
|
||||||
| t1==t2 -> return (ResValue (L l1 t1))
|
| t1==t2 && i1 == i2 -> return (ResValue (L l1 t1) i1)
|
||||||
| otherwise -> fail ""
|
| 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) ->
|
||||||
|
|||||||
@@ -29,7 +29,7 @@ stripInfo i = case i of
|
|||||||
AbsCat _ -> i
|
AbsCat _ -> i
|
||||||
AbsFun mt mi me mb -> AbsFun mt mi Nothing mb
|
AbsFun mt mi me mb -> AbsFun mt mi Nothing mb
|
||||||
ResParam mp mt -> ResParam mp Nothing
|
ResParam mp mt -> ResParam mp Nothing
|
||||||
ResValue lt -> i ----
|
ResValue _ lt -> i ----
|
||||||
ResOper mt md -> ResOper mt Nothing
|
ResOper mt md -> ResOper mt Nothing
|
||||||
ResOverload is fs -> ResOverload is [(lty, L loc (EInt 0)) | (lty,L loc _) <- fs]
|
ResOverload is fs -> ResOverload is [(lty, L loc (EInt 0)) | (lty,L loc _) <- fs]
|
||||||
CncCat mty mte _ mtf mpmcfg -> CncCat mty Nothing Nothing Nothing Nothing
|
CncCat mty mte _ mtf mpmcfg -> CncCat mty Nothing Nothing Nothing Nothing
|
||||||
@@ -107,8 +107,8 @@ sizeInfo i = case i of
|
|||||||
AbsFun mt mi me mb -> 1 + msize mt +
|
AbsFun mt mi me mb -> 1 + msize mt +
|
||||||
sum [sum (map (sizeTerm . patt2term) ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
|
sum [sum (map (sizeTerm . patt2term) ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
|
||||||
ResParam mp mt ->
|
ResParam mp mt ->
|
||||||
1 + sum [1 + sum [1 + sizeTerm ty | (_,_,ty) <- co] | Just (L _ ps) <- [mp], (_,co) <- ps]
|
1 + sum [1 + sum [1 + sizeTerm ty | (_,_,ty) <- co] | Just (L _ ps) <- [mp], (_,co,_) <- ps]
|
||||||
ResValue lt -> 0
|
ResValue _ lt -> 0
|
||||||
ResOper mt md -> 1 + msize mt + msize md
|
ResOper mt md -> 1 + msize mt + msize md
|
||||||
ResOverload is fs -> 1 + sum [sizeTerm ty + sizeTerm tr | (L _ ty, L _ tr) <- fs]
|
ResOverload is fs -> 1 + sum [sizeTerm ty + sizeTerm tr | (L _ ty, L _ tr) <- fs]
|
||||||
CncCat mty _ _ _ _ -> 1 + msize mty -- ignoring lindef, linref and printname
|
CncCat mty _ _ _ _ -> 1 + msize mty -- ignoring lindef, linref and printname
|
||||||
|
|||||||
@@ -25,7 +25,7 @@ import GF.Grammar.Grammar
|
|||||||
import PGF2.Internal(Literal(..),Symbol(..))
|
import PGF2.Internal(Literal(..),Symbol(..))
|
||||||
|
|
||||||
-- Please change this every time when the GFO format is changed
|
-- Please change this every time when the GFO format is changed
|
||||||
gfoVersion = "GF04"
|
gfoVersion = "GF05"
|
||||||
|
|
||||||
instance Binary Ident where
|
instance Binary Ident where
|
||||||
put id = put (ident2utf8 id)
|
put id = put (ident2utf8 id)
|
||||||
@@ -119,7 +119,7 @@ instance Binary Info where
|
|||||||
put (AbsCat x) = putWord8 0 >> put x
|
put (AbsCat x) = putWord8 0 >> put x
|
||||||
put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
|
put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
|
||||||
put (ResParam x y) = putWord8 2 >> put (x,y)
|
put (ResParam x y) = putWord8 2 >> put (x,y)
|
||||||
put (ResValue x) = putWord8 3 >> put x
|
put (ResValue x y) = putWord8 3 >> put (x,y)
|
||||||
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)
|
||||||
put (CncCat v w x y z)=putWord8 6 >> put (v,w,x,y,z)
|
put (CncCat v w x y z)=putWord8 6 >> put (v,w,x,y,z)
|
||||||
@@ -130,7 +130,7 @@ instance Binary Info where
|
|||||||
0 -> get >>= \x -> return (AbsCat x)
|
0 -> get >>= \x -> return (AbsCat x)
|
||||||
1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
|
1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
|
||||||
2 -> get >>= \(x,y) -> return (ResParam x y)
|
2 -> get >>= \(x,y) -> return (ResParam x y)
|
||||||
3 -> get >>= \x -> return (ResValue x)
|
3 -> get >>= \(x,y) -> return (ResValue x y)
|
||||||
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)
|
||||||
6 -> get >>= \(v,w,x,y,z)->return (CncCat v w x y z)
|
6 -> get >>= \(v,w,x,y,z)->return (CncCat v w x y z)
|
||||||
|
|||||||
@@ -330,7 +330,7 @@ data Info =
|
|||||||
|
|
||||||
-- judgements in resource
|
-- judgements in resource
|
||||||
| ResParam (Maybe (L [Param])) (Maybe [Term]) -- ^ (/RES/) the second parameter is list of all possible values
|
| ResParam (Maybe (L [Param])) (Maybe [Term]) -- ^ (/RES/) the second parameter is list of all possible values
|
||||||
| ResValue (L Type) -- ^ (/RES/) to mark parameter constructors for lookup
|
| ResValue (L Type) Int -- ^ (/RES/) to mark parameter constructors for lookup
|
||||||
| ResOper (Maybe (L Type)) (Maybe (L Term)) -- ^ (/RES/)
|
| ResOper (Maybe (L Type)) (Maybe (L Term)) -- ^ (/RES/)
|
||||||
|
|
||||||
| ResOverload [ModuleName] [(L Type,L Term)] -- ^ (/RES/) idents: modules inherited
|
| ResOverload [ModuleName] [(L Type,L Term)] -- ^ (/RES/) idents: modules inherited
|
||||||
@@ -459,7 +459,7 @@ type Case = (Patt, Term)
|
|||||||
--type Cases = ([Patt], Term)
|
--type Cases = ([Patt], Term)
|
||||||
type LocalDef = (Ident, (Maybe Type, Term))
|
type LocalDef = (Ident, (Maybe Type, Term))
|
||||||
|
|
||||||
type Param = (Ident, Context)
|
type Param = (Ident, Context, Int)
|
||||||
type Altern = (Term, [(Term, Term)])
|
type Altern = (Term, [(Term, Term)])
|
||||||
|
|
||||||
type Substitution = [(Ident, Term)]
|
type Substitution = [(Ident, Term)]
|
||||||
|
|||||||
@@ -23,10 +23,11 @@ module GF.Grammar.Lookup (
|
|||||||
lookupResType,
|
lookupResType,
|
||||||
lookupOverload,
|
lookupOverload,
|
||||||
lookupOverloadTypes,
|
lookupOverloadTypes,
|
||||||
lookupParamValues,
|
lookupParamValues,
|
||||||
allParamValues,
|
allParamValues,
|
||||||
lookupAbsDef,
|
lookupParamValueIndex,
|
||||||
lookupLincat,
|
lookupAbsDef,
|
||||||
|
lookupLincat,
|
||||||
lookupFunType,
|
lookupFunType,
|
||||||
lookupCatContext,
|
lookupCatContext,
|
||||||
allOpers, allOpersTo
|
allOpers, allOpersTo
|
||||||
@@ -83,7 +84,7 @@ lookupResDefLoc gr (m,c)
|
|||||||
|
|
||||||
AnyInd _ n -> look n c
|
AnyInd _ n -> look n c
|
||||||
ResParam _ _ -> return (noLoc (QC (m,c)))
|
ResParam _ _ -> return (noLoc (QC (m,c)))
|
||||||
ResValue _ -> return (noLoc (QC (m,c)))
|
ResValue _ _ -> return (noLoc (QC (m,c)))
|
||||||
_ -> raise $ render (c <+> "is not defined in resource" <+> m)
|
_ -> raise $ render (c <+> "is not defined in resource" <+> m)
|
||||||
|
|
||||||
lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
||||||
@@ -99,7 +100,7 @@ lookupResType gr (m,c) = do
|
|||||||
return $ mkProd cont val' []
|
return $ mkProd cont val' []
|
||||||
AnyInd _ n -> lookupResType gr (n,c)
|
AnyInd _ n -> lookupResType gr (n,c)
|
||||||
ResParam _ _ -> return typePType
|
ResParam _ _ -> return typePType
|
||||||
ResValue (L _ t) -> return t
|
ResValue (L _ t) _-> return t
|
||||||
_ -> raise $ render (c <+> "has no type defined in resource" <+> m)
|
_ -> raise $ render (c <+> "has no type defined in resource" <+> m)
|
||||||
|
|
||||||
lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)]
|
lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)]
|
||||||
@@ -113,8 +114,8 @@ lookupOverloadTypes gr id@(m,c) = do
|
|||||||
CncFun (Just (cat,cont,val)) _ _ _ -> do
|
CncFun (Just (cat,cont,val)) _ _ _ -> do
|
||||||
val' <- lock cat val
|
val' <- lock cat val
|
||||||
ret $ mkProd cont val' []
|
ret $ mkProd cont val' []
|
||||||
ResParam _ _ -> ret typePType
|
ResParam _ _ -> ret typePType
|
||||||
ResValue (L _ t) -> ret t
|
ResValue (L _ t) _ -> ret t
|
||||||
ResOverload os tysts -> do
|
ResOverload os tysts -> do
|
||||||
tss <- mapM (\x -> lookupOverloadTypes gr (x,c)) os
|
tss <- mapM (\x -> lookupOverloadTypes gr (x,c)) os
|
||||||
return $ [(tr,ty) | (L _ ty,L _ tr) <- tysts] ++
|
return $ [(tr,ty) | (L _ ty,L _ tr) <- tysts] ++
|
||||||
@@ -176,6 +177,13 @@ allParamValues cnc ptyp =
|
|||||||
-- to normalize records and record types
|
-- to normalize records and record types
|
||||||
sortByFst = sortBy (\ x y -> compare (fst x) (fst y))
|
sortByFst = sortBy (\ x y -> compare (fst x) (fst y))
|
||||||
|
|
||||||
|
lookupParamValueIndex :: ErrorMonad m => Grammar -> QIdent -> m Int
|
||||||
|
lookupParamValueIndex gr c = do
|
||||||
|
(_,info) <- lookupOrigInfo gr c
|
||||||
|
case info of
|
||||||
|
ResValue _ i -> return i
|
||||||
|
_ -> raise $ render (ppQIdent Qualified c <+> "has no parameter index defined")
|
||||||
|
|
||||||
lookupAbsDef :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m (Maybe Int,Maybe [Equation])
|
lookupAbsDef :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m (Maybe Int,Maybe [Equation])
|
||||||
lookupAbsDef gr m c = errIn (render ("looking up absdef of" <+> c)) $ do
|
lookupAbsDef gr m c = errIn (render ("looking up absdef of" <+> c)) $ do
|
||||||
info <- lookupQIdentInfo gr (m,c)
|
info <- lookupQIdentInfo gr (m,c)
|
||||||
@@ -226,7 +234,7 @@ allOpers gr =
|
|||||||
typesIn info = case info of
|
typesIn info = case info of
|
||||||
AbsFun (Just ltyp) _ _ _ -> [ltyp]
|
AbsFun (Just ltyp) _ _ _ -> [ltyp]
|
||||||
ResOper (Just ltyp) _ -> [ltyp]
|
ResOper (Just ltyp) _ -> [ltyp]
|
||||||
ResValue ltyp -> [ltyp]
|
ResValue ltyp _ -> [ltyp]
|
||||||
ResOverload _ tytrs -> [ltyp | (ltyp,_) <- tytrs]
|
ResOverload _ tytrs -> [ltyp | (ltyp,_) <- tytrs]
|
||||||
CncFun (Just (i,ctx,typ)) _ _ _ ->
|
CncFun (Just (i,ctx,typ)) _ _ _ ->
|
||||||
[L NoLoc (mkProdSimple ctx (lock' i typ))]
|
[L NoLoc (mkProdSimple ctx (lock' i typ))]
|
||||||
|
|||||||
@@ -47,7 +47,7 @@ typeForm t =
|
|||||||
Q c -> ([],c,[])
|
Q c -> ([],c,[])
|
||||||
QC c -> ([],c,[])
|
QC c -> ([],c,[])
|
||||||
Sort c -> ([],(MN identW, c),[])
|
Sort c -> ([],(MN identW, c),[])
|
||||||
_ -> error (render ("no normal form of type" <+> ppTerm Unqualified 0 t))
|
_ -> error (render ("no normal form of type" <+> show t))
|
||||||
|
|
||||||
typeFormCnc :: Type -> (Context, Type)
|
typeFormCnc :: Type -> (Context, Type)
|
||||||
typeFormCnc t =
|
typeFormCnc t =
|
||||||
@@ -614,13 +614,15 @@ allDependencies ism b =
|
|||||||
opersIn t = case t of
|
opersIn t = case t of
|
||||||
Q (n,c) | ism n -> [c]
|
Q (n,c) | ism n -> [c]
|
||||||
QC (n,c) | ism n -> [c]
|
QC (n,c) | ism n -> [c]
|
||||||
|
Cn c -> [c]
|
||||||
_ -> collectOp opersIn t
|
_ -> collectOp opersIn t
|
||||||
opty (Just (L _ ty)) = opersIn ty
|
opty (Just (L _ ty)) = opersIn ty
|
||||||
opty _ = []
|
opty _ = []
|
||||||
pts i = case i of
|
pts i = case i of
|
||||||
ResOper pty pt -> [pty,pt]
|
ResOper pty pt -> [pty,pt]
|
||||||
ResOverload _ tyts -> concat [[Just ty, Just tr] | (ty,tr) <- tyts]
|
ResOverload _ tyts -> concat [[Just ty, Just tr] | (ty,tr) <- tyts]
|
||||||
ResParam (Just (L loc ps)) _ -> [Just (L loc t) | (_,cont) <- ps, (_,_,t) <- cont]
|
ResParam (Just (L loc ps)) _ -> [Just (L loc t) | (_,cont,_) <- ps, (_,_,t) <- cont]
|
||||||
|
ResValue pty _ -> [Just pty]
|
||||||
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
|
||||||
|
|||||||
@@ -267,7 +267,7 @@ DataDef
|
|||||||
ParamDef :: { [(Ident,Info)] }
|
ParamDef :: { [(Ident,Info)] }
|
||||||
ParamDef
|
ParamDef
|
||||||
: Posn LhsIdent '=' ListParConstr Posn { ($2, ResParam (Just (mkL $1 $5 [param | L loc param <- $4])) Nothing) :
|
: Posn LhsIdent '=' ListParConstr Posn { ($2, ResParam (Just (mkL $1 $5 [param | L loc param <- $4])) Nothing) :
|
||||||
[(f, ResValue (L loc (mkProdSimple co (Cn $2)))) | L loc (f,co) <- $4] }
|
[(f, ResValue (L loc (mkProdSimple co (Cn $2))) i) | L loc (f,co,i) <- $4] }
|
||||||
| Posn LhsIdent Posn { [($2, ResParam Nothing Nothing)] }
|
| Posn LhsIdent Posn { [($2, ResParam Nothing Nothing)] }
|
||||||
|
|
||||||
OperDef :: { [(Ident,Info)] }
|
OperDef :: { [(Ident,Info)] }
|
||||||
@@ -302,7 +302,7 @@ ListDataConstr
|
|||||||
|
|
||||||
ParConstr :: { L Param }
|
ParConstr :: { L Param }
|
||||||
ParConstr
|
ParConstr
|
||||||
: Posn Ident ListDDecl Posn { mkL $1 $4 ($2,$3) }
|
: Posn Ident ListDDecl Posn { mkL $1 $4 ($2,$3,0) }
|
||||||
|
|
||||||
ListLinDef :: { [(Ident,Info)] }
|
ListLinDef :: { [(Ident,Info)] }
|
||||||
ListLinDef
|
ListLinDef
|
||||||
@@ -774,7 +774,7 @@ checkInfoType mt jment@(id,info) =
|
|||||||
CncCat pty pd pr ppn _->ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh pr ++ locPerh ppn)
|
CncCat pty pd pr ppn _->ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh pr ++ locPerh ppn)
|
||||||
CncFun _ pd ppn _ -> ifConcrete mt (locPerh pd ++ locPerh ppn)
|
CncFun _ pd ppn _ -> ifConcrete mt (locPerh pd ++ locPerh ppn)
|
||||||
ResParam pparam _ -> ifResource mt (locPerh pparam)
|
ResParam pparam _ -> ifResource mt (locPerh pparam)
|
||||||
ResValue ty -> ifResource mt (locL ty)
|
ResValue ty _ -> ifResource mt (locL ty)
|
||||||
ResOper pty pt -> ifOper mt pty pt
|
ResOper pty pt -> ifOper mt pty pt
|
||||||
ResOverload _ xs -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
|
ResOverload _ xs -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
|
||||||
where
|
where
|
||||||
|
|||||||
@@ -106,8 +106,8 @@ ppJudgement q (id, ResParam pparams _) =
|
|||||||
(case pparams of
|
(case pparams of
|
||||||
Just (L _ ps) -> '=' <+> ppParams q ps
|
Just (L _ ps) -> '=' <+> ppParams q ps
|
||||||
_ -> empty) <+> ';'
|
_ -> empty) <+> ';'
|
||||||
ppJudgement q (id, ResValue pvalue) =
|
ppJudgement q (id, ResValue pvalue i) =
|
||||||
"-- param constructor" <+> id <+> ':' <+>
|
"-- param constructor" <+> "[index" <+> i <> "]" <+> id <+> ':' <+>
|
||||||
(case pvalue of
|
(case pvalue of
|
||||||
(L _ ty) -> ppTerm q 0 ty) <+> ';'
|
(L _ ty) -> ppTerm q 0 ty) <+> ';'
|
||||||
ppJudgement q (id, ResOper ptype pexp) =
|
ppJudgement q (id, ResOper ptype pexp) =
|
||||||
@@ -322,7 +322,7 @@ ppBind (Implicit,v) = braces v
|
|||||||
ppAltern q (x,y) = ppTerm q 0 x <+> '/' <+> ppTerm q 0 y
|
ppAltern q (x,y) = ppTerm q 0 x <+> '/' <+> ppTerm q 0 y
|
||||||
|
|
||||||
ppParams q ps = fsep (intersperse (pp '|') (map (ppParam q) ps))
|
ppParams q ps = fsep (intersperse (pp '|') (map (ppParam q) ps))
|
||||||
ppParam q (id,cxt) = id <+> hsep (map (ppDDecl q) cxt)
|
ppParam q (id,cxt,_) = id <+> hsep (map (ppDDecl q) cxt)
|
||||||
|
|
||||||
ppProduction (Production fid funid args) =
|
ppProduction (Production fid funid args) =
|
||||||
ppFId fid <+> "->" <+> ppFunId funid <>
|
ppFId fid <+> "->" <+> ppFunId funid <>
|
||||||
|
|||||||
@@ -119,7 +119,7 @@ convCncJment (name,jment) =
|
|||||||
case jment of
|
case jment of
|
||||||
ResParam ops _ ->
|
ResParam ops _ ->
|
||||||
return $ Pa $ Param i (maybe "" (render . ppParams q . unLoc) ops)
|
return $ Pa $ Param i (maybe "" (render . ppParams q . unLoc) ops)
|
||||||
ResValue _ -> return Ignored
|
ResValue _ _ -> return Ignored
|
||||||
CncCat (Just (L _ typ)) Nothing Nothing pprn _ -> -- ignores printname !!
|
CncCat (Just (L _ typ)) Nothing Nothing pprn _ -> -- ignores printname !!
|
||||||
return $ LC $ Lincat i (render $ ppTerm q 0 typ)
|
return $ LC $ Lincat i (render $ ppTerm q 0 typ)
|
||||||
ResOper oltyp (Just lterm) -> return $ Op $ Oper lhs rhs
|
ResOper oltyp (Just lterm) -> return $ Op $ Oper lhs rhs
|
||||||
|
|||||||
Reference in New Issue
Block a user