forked from GitHub/gf-core
use ByteString internally in Ident, CId and Label
This commit is contained in:
@@ -53,13 +53,13 @@ typPredefined c@(IC f) = case f of
|
||||
"plus" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "Int")
|
||||
---- "read" -> (P : Type) -> Tok -> P
|
||||
"show" -> return $ mkProds -- (P : PType) -> P -> Tok
|
||||
([(identC "P",typePType),(wildIdent,Vr (identC "P"))],typeStr,[])
|
||||
([(identC "P",typePType),(identW,Vr (identC "P"))],typeStr,[])
|
||||
"toStr" -> return $ mkProds -- (L : Type) -> L -> Str
|
||||
([(identC "L",typeType),(wildIdent,Vr (identC "L"))],typeStr,[])
|
||||
([(identC "L",typeType),(identW,Vr (identC "L"))],typeStr,[])
|
||||
"mapStr" ->
|
||||
let ty = identC "L" in
|
||||
return $ mkProds -- (L : Type) -> (Str -> Str) -> L -> L
|
||||
([(ty,typeType),(wildIdent,mkFunType [typeStr] typeStr),(wildIdent,Vr ty)],Vr ty,[])
|
||||
([(ty,typeType),(identW,mkFunType [typeStr] typeStr),(identW,Vr ty)],Vr ty,[])
|
||||
"take" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
|
||||
"tk" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
|
||||
_ -> prtBad "unknown in Predef:" c
|
||||
|
||||
@@ -81,7 +81,7 @@ typeSkeleton typ = do
|
||||
-- construct types and terms
|
||||
|
||||
mkFunType :: [Type] -> Type -> Type
|
||||
mkFunType tt t = mkProd ([(wildIdent, ty) | ty <- tt]) t -- nondep prod
|
||||
mkFunType tt t = mkProd ([(identW, ty) | ty <- tt]) t -- nondep prod
|
||||
|
||||
mkApp :: Term -> [Term] -> Term
|
||||
mkApp = foldl App
|
||||
@@ -121,7 +121,7 @@ unzipR :: [Assign] -> ([Label],[Term])
|
||||
unzipR r = (ls, map snd ts) where (ls,ts) = unzip r
|
||||
|
||||
mkDecl :: Term -> Decl
|
||||
mkDecl typ = (wildIdent, typ)
|
||||
mkDecl typ = (identW, typ)
|
||||
|
||||
mkLet :: [LocalDef] -> Term -> Term
|
||||
mkLet defs t = foldr Let t defs
|
||||
@@ -336,7 +336,7 @@ changeTableType co i = case i of
|
||||
patt2term :: Patt -> Term
|
||||
patt2term pt = case pt of
|
||||
PV x -> Vr x
|
||||
PW -> Vr wildIdent --- not parsable, should not occur
|
||||
PW -> Vr identW --- not parsable, should not occur
|
||||
PC c pp -> mkApp (Con c) (map patt2term pp)
|
||||
PP p c pp -> mkApp (QC p c) (map patt2term pp)
|
||||
PR r -> R [assign l (patt2term p) | (l,p) <- r]
|
||||
|
||||
@@ -71,7 +71,7 @@ prModule :: SourceModule -> String
|
||||
prModule = cprintTree . trModule
|
||||
|
||||
instance Print Judgement where
|
||||
prt j = cprintTree $ trAnyDef (wildIdent, j)
|
||||
prt j = cprintTree $ trAnyDef (identW, j)
|
||||
---- prt_ = prExp
|
||||
|
||||
instance Print Term where
|
||||
|
||||
Reference in New Issue
Block a user