summaryrefslogtreecommitdiff
path: root/src/runtime/haskell
diff options
context:
space:
mode:
Diffstat (limited to 'src/runtime/haskell')
-rw-r--r--src/runtime/haskell/PGF.hs11
-rw-r--r--src/runtime/haskell/PGF/Check.hs2
-rw-r--r--src/runtime/haskell/PGF/Data.hs8
-rw-r--r--src/runtime/haskell/PGF/Expr.hs39
-rw-r--r--src/runtime/haskell/PGF/Macros.hs6
-rw-r--r--src/runtime/haskell/PGF/Paraphrase.hs2
-rw-r--r--src/runtime/haskell/PGF/Printer.hs13
-rw-r--r--src/runtime/haskell/PGF/TypeCheck.hs18
8 files changed, 56 insertions, 43 deletions
diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs
index 9bc5c6567..2ca152db9 100644
--- a/src/runtime/haskell/PGF.hs
+++ b/src/runtime/haskell/PGF.hs
@@ -298,11 +298,12 @@ browse :: PGF -> CId -> Maybe (String,[CId],[CId])
browse pgf id = fmap (\def -> (def,producers,consumers)) definition
where
definition = case Map.lookup id (funs (abstract pgf)) of
- Just (ty,_,eqs) -> Just $ render (text "fun" <+> ppCId id <+> colon <+> ppType 0 [] ty $$
- if null eqs
- then empty
- else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
- in ppCId id <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs])
+ Just (ty,_,Just eqs) -> Just $ render (text "fun" <+> ppCId id <+> colon <+> ppType 0 [] ty $$
+ if null eqs
+ then empty
+ else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
+ in ppCId id <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs])
+ Just (ty,_,Nothing ) -> Just $ render (text "data" <+> ppCId id <+> colon <+> ppType 0 [] ty)
Nothing -> case Map.lookup id (cats (abstract pgf)) of
Just hyps -> Just $ render (text "cat" <+> ppCId id <+> hsep (snd (mapAccumL ppHypo [] hyps)))
Nothing -> Nothing
diff --git a/src/runtime/haskell/PGF/Check.hs b/src/runtime/haskell/PGF/Check.hs
index 6ac8c9b20..8f3b82eb7 100644
--- a/src/runtime/haskell/PGF/Check.hs
+++ b/src/runtime/haskell/PGF/Check.hs
@@ -38,7 +38,7 @@ checkConcrete pgf (lang,cnc) =
checkl = checkLin pgf lang
-}
-type PGFSig = (Map.Map CId (Type,Int,[Equation]),Map.Map CId Term,Map.Map CId Term)
+type PGFSig = (Map.Map CId (Type,Int,Maybe [Equation]),Map.Map CId Term,Map.Map CId Term)
checkLin :: PGFSig -> CId -> (CId,Term) -> Err ((CId,Term),Bool)
checkLin pgf lang (f,t) =
diff --git a/src/runtime/haskell/PGF/Data.hs b/src/runtime/haskell/PGF/Data.hs
index f2b4b913c..a23958d82 100644
--- a/src/runtime/haskell/PGF/Data.hs
+++ b/src/runtime/haskell/PGF/Data.hs
@@ -24,10 +24,10 @@ data PGF = PGF {
}
data Abstr = Abstr {
- aflags :: Map.Map CId Literal, -- value of a flag
- funs :: Map.Map CId (Type,Int,[Equation]), -- type, arrity and definition of function
- cats :: Map.Map CId [Hypo], -- context of a cat
- catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup)
+ aflags :: Map.Map CId Literal, -- value of a flag
+ funs :: Map.Map CId (Type,Int,Maybe [Equation]), -- type, arrity and definition of function
+ cats :: Map.Map CId [Hypo], -- context of a cat
+ catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup)
}
data Concr = Concr {
diff --git a/src/runtime/haskell/PGF/Expr.hs b/src/runtime/haskell/PGF/Expr.hs
index 674422217..19fc8f627 100644
--- a/src/runtime/haskell/PGF/Expr.hs
+++ b/src/runtime/haskell/PGF/Expr.hs
@@ -269,6 +269,7 @@ normalForm funs k env e = value2expr k (eval funs env e)
value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)
value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs)
value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs))
+ value2expr i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs)
value2expr i (VLit l) = ELit l
value2expr i (VClosure env (EAbs b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))
value2expr i (VImplArg v) = EImplArg (value2expr i v)
@@ -279,20 +280,23 @@ data Value
| VMeta {-# UNPACK #-} !MetaId Env [Value]
| VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)
| VGen {-# UNPACK #-} !Int [Value]
+ | VConst CId [Value]
| VClosure Env Expr
| VImplArg Value
-type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
+type Funs = Map.Map CId (Type,Int,Maybe [Equation]) -- type and def of a fun
type Env = [Value]
eval :: Funs -> Env -> Expr -> Value
eval funs env (EVar i) = env !! i
eval funs env (EFun f) = case Map.lookup f funs of
- Just (_,a,eqs) -> if a == 0
- then case eqs of
- Equ [] e : _ -> eval funs [] e
- _ -> VApp f []
- else VApp f []
+ Just (_,a,meqs) -> case meqs of
+ Just eqs -> if a == 0
+ then case eqs of
+ Equ [] e : _ -> eval funs [] e
+ _ -> VConst f []
+ else VApp f []
+ Nothing -> VApp f []
Nothing -> error ("unknown function "++showCId f)
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
eval funs env (EAbs b x e) = VClosure env (EAbs b x e)
@@ -305,10 +309,11 @@ apply :: Funs -> Env -> Expr -> [Value] -> Value
apply funs env e [] = eval funs env e
apply funs env (EVar i) vs = applyValue funs (env !! i) vs
apply funs env (EFun f) vs = case Map.lookup f funs of
- Just (_,a,eqs) -> if a <= length vs
- then let (as,vs') = splitAt a vs
- in match funs f eqs as vs'
- else VApp f vs
+ Just (_,a,meqs) -> case meqs of
+ Just eqs -> if a <= length vs
+ then match funs f eqs vs
+ else VApp f vs
+ Nothing -> VApp f vs
Nothing -> error ("unknown function "++showCId f)
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
apply funs env (EAbs _ x e) (v:vs) = apply funs (v:env) e vs
@@ -323,6 +328,7 @@ applyValue funs (VLit _) vs = error "literal of function
applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs)
applyValue funs (VGen i vs0) vs = VGen i (vs0++vs)
applyValue funs (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue funs (k v) vs)
+applyValue funs (VConst f vs0) vs = VConst f (vs0++vs)
applyValue funs (VClosure env (EAbs b x e)) (v:vs) = apply funs (v:env) e vs
applyValue funs (VImplArg _) vs = error "implicit argument in function position"
@@ -330,22 +336,23 @@ applyValue funs (VImplArg _) vs = error "implicit argument in
-- Pattern matching
-----------------------------------------------------
-match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value
-match funs f eqs as0 vs0 =
+match :: Funs -> CId -> [Equation] -> [Value] -> Value
+match funs f eqs as0 =
case eqs of
- [] -> VApp f (as0++vs0)
+ [] -> VConst f as0
(Equ ps res):eqs -> tryMatches eqs ps as0 res []
where
- tryMatches eqs [] [] res env = apply funs env res vs0
+ tryMatches eqs [] as res env = apply funs env res as
tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
where
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (v:env)
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
tryMatch (p ) (VMeta i envi vs ) env = VSusp i envi vs (\v -> tryMatch p v env)
- tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
+ tryMatch (p ) (VGen i vs ) env = VConst f as0
tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env)
+ tryMatch (p ) v@(VConst _ _ ) env = VConst f as0
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
tryMatch (PImplArg p ) (VImplArg v ) env = tryMatch p v env
- tryMatch _ _ env = match funs f eqs as0 vs0
+ tryMatch _ _ env = match funs f eqs as0
diff --git a/src/runtime/haskell/PGF/Macros.hs b/src/runtime/haskell/PGF/Macros.hs
index 03c5d0fe4..34f32c386 100644
--- a/src/runtime/haskell/PGF/Macros.hs
+++ b/src/runtime/haskell/PGF/Macros.hs
@@ -22,7 +22,7 @@ lookType pgf f =
case lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) of
(ty,_,_) -> ty
-lookDef :: PGF -> CId -> [Equation]
+lookDef :: PGF -> CId -> Maybe [Equation]
lookDef pgf f =
case lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) of
(_,a,eqs) -> eqs
@@ -30,8 +30,8 @@ lookDef pgf f =
isData :: PGF -> CId -> Bool
isData pgf f =
case Map.lookup f (funs (abstract pgf)) of
- Just (_,_,[]) -> True -- the encoding of data constrs
- _ -> False
+ Just (_,_,Nothing) -> True -- the encoding of data constrs
+ _ -> False
lookValCat :: PGF -> CId -> CId
lookValCat pgf = valCat . lookType pgf
diff --git a/src/runtime/haskell/PGF/Paraphrase.hs b/src/runtime/haskell/PGF/Paraphrase.hs
index 58d15b2e8..3835b73c7 100644
--- a/src/runtime/haskell/PGF/Paraphrase.hs
+++ b/src/runtime/haskell/PGF/Paraphrase.hs
@@ -53,7 +53,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
isClosed d || (length equs == 1 && isLinear d)]
equss = [(f,[(Fun f (map patt2tree ps), expr2tree d) | (Equ ps d) <- eqs]) |
- (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
+ (f,(_,_,Just eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True
diff --git a/src/runtime/haskell/PGF/Printer.hs b/src/runtime/haskell/PGF/Printer.hs
index ee0fd4070..d458eb1a7 100644
--- a/src/runtime/haskell/PGF/Printer.hs
+++ b/src/runtime/haskell/PGF/Printer.hs
@@ -27,12 +27,13 @@ ppAbs name a = text "abstract" <+> ppCId name <+> char '{' $$
ppCat :: CId -> [Hypo] -> Doc
ppCat c hyps = text "cat" <+> ppCId c <+> hsep (snd (mapAccumL ppHypo [] hyps))
-ppFun :: CId -> (Type,Int,[Equation]) -> Doc
-ppFun f (t,_,eqs) = text "fun" <+> ppCId f <+> colon <+> ppType 0 [] t $$
- if null eqs
- then empty
- else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
- in ppCId f <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs]
+ppFun :: CId -> (Type,Int,Maybe [Equation]) -> Doc
+ppFun f (t,_,Just eqs) = text "fun" <+> ppCId f <+> colon <+> ppType 0 [] t $$
+ if null eqs
+ then empty
+ else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
+ in ppCId f <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs]
+ppFun f (t,_,Nothing) = text "data" <+> ppCId f <+> colon <+> ppType 0 [] t
ppCnc :: Language -> Concr -> Doc
ppCnc name cnc =
diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs
index 937c21786..4e91827aa 100644
--- a/src/runtime/haskell/PGF/TypeCheck.hs
+++ b/src/runtime/haskell/PGF/TypeCheck.hs
@@ -409,12 +409,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
e1 <- mkLam i scopei env2 vs2 v1
setMeta i (MBound e1)
sequence_ [c e1 | c <- cs]
- eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
- eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
- eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
+ eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
+ eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
+ eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
+ eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
in eqExpr (k+1) (v:env1) e1 (v:env2) e2
- eqValue' k v1 v2 = raiseTypeMatchError
+ eqValue' k v1 v2 = raiseTypeMatchError
mkLam i scope env vs0 v = do
let k = scopeSize scope
@@ -452,6 +453,8 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
Just i -> do vs <- mapM (occurCheck i0 k xs) vs
return (VGen i vs)
Nothing -> raiseTypeMatchError
+ occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs
+ return (VConst f vs)
occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
return (VClosure env e)
@@ -516,9 +519,10 @@ refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
-value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
-value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
-value2expr sig i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
+value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
+value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
+value2expr sig i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
+value2expr sig i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
value2expr sig i (VSusp j env vs k) = value2expr sig i (k (VGen j vs))
value2expr sig i (VLit l) = ELit l
value2expr sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 06:25:06 +0000