forked from GitHub/gf-core
def and List
This commit is contained in:
@@ -5,9 +5,9 @@
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/04/21 16:22:18 $
|
||||
-- > CVS $Author: bringert $
|
||||
-- > CVS $Revision: 1.7 $
|
||||
-- > CVS $Date: 2005/10/02 20:50:19 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.8 $
|
||||
--
|
||||
-- computation in abstract syntax w.r.t. explicit definitions.
|
||||
--
|
||||
@@ -72,12 +72,15 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
|
||||
Ok (Just EData) -> Nothing -- canonical --- should always be QC
|
||||
Ok md -> md
|
||||
_ -> Nothing
|
||||
Eqs _ -> return t ---- for nested fn
|
||||
_ -> Nothing
|
||||
|
||||
beta :: [Ident] -> Exp -> Exp
|
||||
beta vv c = case c of
|
||||
App (Abs x b) a -> beta vv $ substTerm vv [xvv] (beta (x:vv) b)
|
||||
where xvv = (x,beta vv a)
|
||||
Let (x,(_,a)) b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b)
|
||||
where xvv = (x,beta vv a)
|
||||
App f a -> let (a',f') = (beta vv a, beta vv f) in
|
||||
(if a'==a && f'==f then id else beta vv) $ App f' a'
|
||||
Prod x a b -> Prod x (beta vv a) (beta (x:vv) b)
|
||||
|
||||
@@ -5,9 +5,9 @@
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/06/03 21:51:58 $
|
||||
-- > CVS $Date: 2005/10/02 20:50:19 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.22 $
|
||||
-- > CVS $Revision: 1.23 $
|
||||
--
|
||||
-- Macros for constructing and analysing source code terms.
|
||||
--
|
||||
@@ -655,6 +655,10 @@ composOp co trm =
|
||||
i' <- changeTableType co i
|
||||
return (TSh i' cc')
|
||||
|
||||
Eqs cc ->
|
||||
do cc' <- mapPairListM (co . snd) cc
|
||||
return (Eqs cc')
|
||||
|
||||
V ty vs ->
|
||||
do ty' <- co ty
|
||||
vs' <- mapM co vs
|
||||
|
||||
@@ -5,9 +5,9 @@
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/09/15 16:22:02 $
|
||||
-- > CVS $Date: 2005/10/02 20:50:19 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.10 $
|
||||
-- > CVS $Revision: 1.11 $
|
||||
--
|
||||
-- Thierry Coquand's type checking algorithm that creates a trace
|
||||
-----------------------------------------------------------------------------
|
||||
@@ -261,6 +261,9 @@ checkPatt th tenv exp val = do
|
||||
checkExpP tenv@(k,rho,gamma) exp val = case exp of
|
||||
Meta m -> return $ (AMeta m val, val, [])
|
||||
Vr x -> return $ (AVr x val, val, [])
|
||||
EInt i -> return (AInt i, valAbsInt, [])
|
||||
K s -> return (AStr s, valAbsString, [])
|
||||
|
||||
Q m c -> do
|
||||
typ <- lookupConst th (m,c)
|
||||
return $ (ACn (m,c) typ, typ, [])
|
||||
|
||||
Reference in New Issue
Block a user