mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-11 20:22:51 -06:00
70 lines
1.5 KiB
Haskell
70 lines
1.5 KiB
Haskell
module Values where
|
|
|
|
import Operations
|
|
import Zipper
|
|
|
|
import Grammar
|
|
import Ident
|
|
|
|
-- values used in TC type checking
|
|
|
|
type Exp = Term
|
|
|
|
data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VType | VClos Env Exp
|
|
deriving (Eq,Show)
|
|
|
|
type Env = [(Ident,Val)]
|
|
|
|
-- annotated tree used in editing
|
|
|
|
type Tree = Tr TrNode
|
|
|
|
newtype TrNode = N (Binds,Atom,Val,(Constraints,MetaSubst),Bool)
|
|
deriving (Eq,Show)
|
|
|
|
data Atom = AtC Fun | AtM MetaSymb | AtV Ident | AtL String | AtI Int
|
|
deriving (Eq,Show)
|
|
|
|
type Binds = [(Ident,Val)]
|
|
type Constraints = [(Val,Val)]
|
|
type MetaSubst = [(MetaSymb,Val)]
|
|
|
|
-- for TC
|
|
|
|
valAbsInt, valAbsString :: Val
|
|
valAbsInt = VCn (cPredefAbs, cInt)
|
|
valAbsString = VCn (cPredefAbs, cString)
|
|
|
|
vType :: Val
|
|
vType = VType
|
|
|
|
cType,cPredefAbs,cInt,cString :: Ident
|
|
cType = identC "Type" --- #0
|
|
cPredefAbs = identC "PredefAbs"
|
|
cInt = identC "Int"
|
|
cString = identC "String"
|
|
|
|
isPredefCat c = elem c [cInt,cString]
|
|
|
|
eType :: Exp
|
|
eType = Sort "Type"
|
|
|
|
tree2exp :: Tree -> Exp
|
|
tree2exp (Tr (N (bi,at,_,_,_),ts)) = foldr Abs (foldl App at' ts') bi' where
|
|
at' = case at of
|
|
AtC (m,c) -> Q m c
|
|
AtV i -> Vr i
|
|
AtM m -> Meta m
|
|
AtL s -> K s
|
|
AtI s -> EInt s
|
|
bi' = map fst bi
|
|
ts' = map tree2exp ts
|
|
|
|
loc2treeFocus :: Loc TrNode -> Tree
|
|
loc2treeFocus (Loc (Tr (a,ts),p)) =
|
|
loc2tree (Loc (Tr (mark a, map (mapTr nomark) ts), mapPath nomark p))
|
|
where
|
|
(mark, nomark) = (\(N (a,b,c,d,_)) -> N(a,b,c,d,True),
|
|
\(N (a,b,c,d,_)) -> N(a,b,c,d,False))
|
|
|