cleaning duties

This commit is contained in:
crumbtoo
2023-11-23 01:34:31 -07:00
parent d84fe56fbb
commit f4d88e9478
2 changed files with 25 additions and 22 deletions

View File

@@ -78,10 +78,14 @@ facExample = [coreProg|
main = fac 3;
|]
pairExample = [coreProg|
pairExample1 = [coreProg|
main = fst (snd (fst (MkPair (MkPair 1 (MkPair 2 3)) 4)));
|]
pairExample2 = [coreProg|
main = (if# False fst snd) (MkPair 2 3);
|]
corePrelude :: Module
corePrelude = Module (Just ("Prelude", [])) $ Program
[ ScDef "id" ["x"] $ "x"

View File

@@ -262,27 +262,26 @@ step st =
primStep _ IntDivP st = primArith (div) st
primStep _ IntEqP st = primComp (==) st
primStep _ IfP (TiState s d h g sts) = TiState s' d' h' g sts
primStep _ IfP (TiState s d h g sts) =
case needsEval cn of
True -> TiState s' d' h g sts
where
-- the condition is evaluated if it is not in normal form
s' | needsEval cn = [c]
| otherwise = drop 3 s
d' | needsEval cn = drop 1 s : d
| otherwise = d
h' | needsEval cn = h
| otherwise =
update rootAddr (NInd $ if isTrue then t else f) h
[cn,tn,fn] = hViewUnsafe h <$> [c,t,f]
[c,t,f] = getArgs h s
s' = [c]
d' = drop 1 s : d
False -> TiState s' d h' g sts
where
s' = drop 3 s
h' = update rootAddr res h
res = NInd $ if isTrue then t else f
rootAddr = head s'
isTrue = case cn of
-- see Core.Examples.corePrelude; True and False are defined
-- as Con 1 0 and Con 0 0, respectively
-- see Core.Examples.corePrelude; True and False are
-- defined as Con 1 0 and Con 0 0, respectively
NData 0 [] -> False
NData 1 [] -> True
where
cn = hLookupUnsafe c h
(c:t:f:_) = getArgs h s
primStep _ CasePairP (TiState s d h g sts) =
case needsEval pn of
@@ -300,7 +299,7 @@ step st =
a2 = s' !! 1
NData 0 [x,y] = pn
where
[p,f] = getArgs h s
(p:f:_) = getArgs h s
pn = hLookupUnsafe p h
primStep n (ConP t a) (TiState s d h g sts) =