867f092 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed evaluator

867f092Edwin Brady15 years ago

src/Core.hs+12−7

compare with master

unifiedsplit

@@ -69,10 +69,12 @@ type RProgram = [(Name, RDef)]

69data NameType = Ref | DCon Int Int | TCon Int

70 deriving (Show, Eq)

72+-- FIXME: Consider changing this to birectional, with type annotations.

73+

72data TT n = P NameType n (TT n) -- embed type

74data TT n = P NameType n (TT n) -- embed type

73 | V Int

75 | V Int

74 | Bind n (Binder (TT n)) (TT n)

76 | Bind n (Binder (TT n)) (TT n)

75− | App (TT n) (TT n) (TT n) -- function, function type, arg

77+ | App (TT n) (TT n) -- function, function type, arg

76 | Set Int

78 | Set Int

77 deriving (Functor, Eq)

79 deriving (Functor, Eq)

@@ -105,7 +107,7 @@ showEnv' env t dbg = se 10 env t where

105 if dbg then "{" ++ show i ++ "}" else ""

107 if dbg then "{" ++ show i ++ "}" else ""

106 | otherwise = "!!V " ++ show i ++ "!!"

108 | otherwise = "!!V " ++ show i ++ "!!"

107 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

109 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

108− se p env (App f t a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

110+ se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

109 se p env (Set i) = "Set" ++ show i

111 se p env (Set i) = "Set" ++ show i

110

112

111 sb env n (Lam t) = showb env "\\ " " => " n t

113 sb env n (Lam t) = showb env "\\ " " => " n t

@@ -125,7 +127,7 @@ showEnv' env t dbg = se 10 env t where

125-- Check whether a term has any holes in it - impure if so

127-- Check whether a term has any holes in it - impure if so

126

128

127pureTerm :: TT n -> Bool

129pureTerm :: TT n -> Bool

128−pureTerm (App f t a) = pureTerm f && pureTerm t && pureTerm a

130+pureTerm (App f a) = pureTerm f && pureTerm a

129pureTerm (Bind n b sc) = pureBinder b && pureTerm sc where

131pureTerm (Bind n b sc) = pureBinder b && pureTerm sc where

130 pureBinder (Hole _) = False

132 pureBinder (Hole _) = False

131 pureBinder (Guess _ _) = False

133 pureBinder (Guess _ _) = False

@@ -138,7 +140,7 @@ pureTerm _ = True

138weakenTm :: Int -> TT n -> TT n

140weakenTm :: Int -> TT n -> TT n

139weakenTm i t = wk i 0 t

141weakenTm i t = wk i 0 t

140 where wk i min (V x) | x >= min = V (i + x)

142 where wk i min (V x) | x >= min = V (i + x)

141− wk i m (App f t a) = App (wk i m f) (wk i m t) (wk i m a)

143+ wk i m (App f a) = App (wk i m f) (wk i m a)

142 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)

144 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)

143 wk i m t = t

145 wk i m t = t

144 wkb i m (Let t v) = Let (wk i m t) (wk i m v)

146 wkb i m (Let t v) = Let (wk i m t) (wk i m v)

@@ -148,7 +150,7 @@ weakenTm i t = wk i 0 t

148-- weaken an environment so that all the de Bruijn indices are correct according

150-- weaken an environment so that all the de Bruijn indices are correct according

149-- to the latest bound variable

151-- to the latest bound variable

150

152

151−weakenEnv :: Show n => EnvTT n -> EnvTT n

153+weakenEnv :: EnvTT n -> EnvTT n

152weakenEnv env = wk (length env - 1) env

154weakenEnv env = wk (length env - 1) env

153 where wk i [] = []

155 where wk i [] = []

154 wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs

156 wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs

@@ -156,12 +158,15 @@ weakenEnv env = wk (length env - 1) env

156 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)

158 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)

157 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }

159 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }

158

160

161+weakenTmEnv :: Int -> EnvTT n -> EnvTT n

162+weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

163+

159-- WELL TYPED TERMS AS HOAS -------------------------------------------------

164-- WELL TYPED TERMS AS HOAS -------------------------------------------------

160

165

161data HTT = HP NameType Name HTT

166data HTT = HP NameType Name HTT

162 | HV Int

167 | HV Int

163 | HBind Name (Binder HTT) (HTT -> HTT)

168 | HBind Name (Binder HTT) (HTT -> HTT)

164− | HApp HTT HTT HTT

169+ | HApp HTT HTT

165 | HSet Int

170 | HSet Int

166 | HTmp Int

171 | HTmp Int

167

172

@@ -179,7 +184,7 @@ hoas env (Bind n b sc) = HBind n (hbind b) (\x -> hoas (x:env) sc)

179 hbind (PVar t) = PVar (hoas env t)

184 hbind (PVar t) = PVar (hoas env t)

180 hbind (Let v t) = Let (hoas env v) (hoas env t)

185 hbind (Let v t) = Let (hoas env v) (hoas env t)

181 hbind (Guess v t) = Guess (hoas env v) (hoas env t)

186 hbind (Guess v t) = Guess (hoas env v) (hoas env t)

182−hoas env (App f t a) = HApp (hoas env f) (hoas env t) (hoas env a)

187+hoas env (App f a) = HApp (hoas env f) (hoas env a)

183hoas env (Set i) = HSet i

188hoas env (Set i) = HSet i

184

189

185-- CONTEXTS -----------------------------------------------------------------

190-- CONTEXTS -----------------------------------------------------------------

src/CoreParser.hs+1

@@ -96,6 +96,7 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

96 x <- iName; lchar ':'; ty <- pTerm

97 lchar '=';

98 val <- pTerm

99+ reserved "in";

99 sc <- pTerm

100 sc <- pTerm

100 return (RBind x (Let ty val) sc))

101 return (RBind x (Let ty val) sc))

101 <|> try (do lchar '_';

102 <|> try (do lchar '_';

src/Evaluate.hs+119−69

@@ -6,79 +6,129 @@ import Debug.Trace

6import Core

8normalise :: Context -> Env -> TT Name -> TT Name

9−normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))

9+normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)

10−

11−type HEnv = [(Name, Binder HTT)]

13−evalEnv :: Env -> HEnv

11+data Value = VP NameType Name Value

14−evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))

12+ | VV Int

13+ | VBind Name (Binder Value) (Value -> Value)

14+ | VApp Value Value

15+ | VSet Int

16+ | VTmp Int

16−-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher

17−-- level things, so, if we remove a binder, we need to strengthen the

18−-- indices appropriately.

19−

20−eval :: Context -> HEnv -> HTT -> HTT

18+eval :: Context -> Env -> TT Name -> Value

21−eval ctxt env t = ev t where

19+eval ctxt genv tm = ev [] tm where

22− ev (HP Ref n ty)

20+-- ev env (P Ref n ty)

23− | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling

21+-- | Just v <- lookupP n ctxt = v -- FIXME! Needs evalling

24− ev (HP nt n ty) = HP nt n (ev ty)

22+ ev env (P nt n ty) = VP nt n (ev env ty)

25−{-

23+ ev env (V i) | i < length env = env !! i

26− ev (HV i)

27− | i < length env = case env!! i of

24+ | i < length env + length genv

25+ = case genv !! (i - length env) of

28− (n, Let t v) -> ev v

26+ (_, Let t v) -> ev env v

29− _ -> HV i

27+ _ -> VV i

30− | otherwise = HV i

28+ | otherwise = error $ "Internal error: V" ++ show i

31−-}

29+ ev env (Bind n (Let t v) sc)

32− ev (HApp f t a)

30+ = ev (ev env v : env) sc

33− = evSpine f [(a, t)]

31+ ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

34− where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)

35− evSpine f sp = evAp f sp

36− ev (HBind n (Let t v) sc) = weaken (-1) (ev (sc (weaken 1 (ev v))))

37− ev (HBind n b sc)

38− = HBind n (evB b) (\x -> ev (sc x))

39− where evB (Lam t) = Lam (ev t)

32+ where vbind env (Lam t) = Lam (ev env t)

40− evB (Pi t) = Pi (ev t)

33+ vbind env (Pi t) = Pi (ev env t)

41− evB (Hole t) = Hole (ev t)

34+ vbind env (Hole t) = Hole (ev env t)

42− evB (Guess t v) = Guess (ev t) (ev v)

35+ vbind env (PVar t) = PVar (ev env t)

43− evB (PVar t) = PVar (ev t)

36+ vbind env (Guess v t) = Guess (ev env v) (ev env t)

44− ev tm = tm -- Constructors + constants

37+ ev env (App f a) = evApply env [a] f

38+ ev env (Set i) = VSet i

39+

40+ evApply env args (App f a) = evApply env (a:args) f

41+ evApply env args f = apply env (ev env f) (reverse args)

46− -- TODO:add PE magic here - nothing is evaluated yet

43+ apply env (VBind n (Lam t) sc) (a:as) = apply env (sc (ev env a)) as

44+ apply env f (a:as) = unload env f (a:as)

45+ apply env f [] = f

48− evAp f sp = evAp' (ev f) sp

47+ unload env f [] = f

49− evAp' (HBind n (Lam ty) sc) ((a, t):sp)

48+ unload env f (a:as) = unload env (VApp f (ev env a)) as

50− = weaken (-1) (evAp' (sc (weaken 1 (ev a))) sp)

51− evAp' f sp = apply f (map (\ (a, t) -> (ev a, ev t)) sp)

53− apply f [] = f

50+quote :: Int -> Value -> TT Name

54− apply f ((a, t):xs) = apply (HApp f t a) xs

51+quote i (VP nt n v) = P nt n (quote i v)

52+quote i (VV x) = V x

53+quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp (i+1))))

54+ where quoteB t = fmap (quote i) t

55+quote i (VApp f a) = App (quote i f) (quote i a)

56+quote i (VSet u) = Set u

57+quote i (VTmp x) = V (i - x)

56−-- Adjust de Bruijn indices across a term

59+-- normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))

57−

60+--

58−weaken :: Int -> HTT -> HTT

61+-- type HEnv = [(Name, Binder HTT)]

59−weaken w (HV i) = HV (i + w)

62+--

60−weaken w (HBind n b sc)

63+-- evalEnv :: Env -> HEnv

61− = HBind n (weakenB b) (\x -> weaken w (sc x))

64+-- evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))

62− where weakenB (Lam t) = Lam (weaken w t)

65+--

63− weakenB (Pi t) = Pi (weaken w t)

66+-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher

64− weakenB (Let t v) = Let (weaken w t) (weaken w v)

67+-- level things, so, if we remove a binder, we need to strengthen the

65− weakenB (Hole t) = Hole (weaken w t)

68+-- indices appropriately.

66− weakenB (Guess t v) = Guess (weaken w t) (weaken w v)

67− weakenB (PVar t) = PVar (weaken w t)

68−weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)

69−weaken w tm = tm

70+-- eval :: Context -> HEnv -> HTT -> HTT

71+-- eval ctxt env t = ev t where

72+-- ev (HP Ref n ty)

73+-- | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling

74+-- ev (HP nt n ty) = HP nt n (ev ty)

75+-- {-

76+-- ev (HV i)

77+-- | i < length env = case env!! i of

78+-- (n, Let t v) -> ev v

79+-- _ -> HV i

80+-- | otherwise = HV i

81+-- -}

82+-- ev (HApp f t a)

83+-- = evSpine f [(a, t)]

84+-- where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)

85+-- evSpine f sp = evAp f sp

86+-- ev (HBind n (Let t v) sc) = weaken (-1) (ev (sc (weaken 1 (ev v))))

87+-- ev (HBind n b sc)

88+-- = HBind n (evB b) (\x -> ev (sc x))

89+-- where evB (Lam t) = Lam (ev t)

90+-- evB (Pi t) = Pi (ev t)

91+-- evB (Hole t) = Hole (ev t)

92+-- evB (Guess t v) = Guess (ev t) (ev v)

93+-- evB (PVar t) = PVar (ev t)

94+-- ev tm = tm -- Constructors + constants

95+--

96+-- -- TODO:add PE magic here - nothing is evaluated yet

97+--

98+-- evAp f sp = evAp' (ev f) sp

99+-- evAp' (HBind n (Lam ty) sc) ((a, t):sp)

100+-- = weaken (-1) (evAp' (sc (weaken 1 (ev a))) sp)

101+-- evAp' f sp = apply f (map (\ (a, t) -> (ev a, ev t)) sp)

102+--

103+-- apply f [] = f

104+-- apply f ((a, t):xs) = apply (HApp f t a) xs

105+--

106+-- -- Adjust de Bruijn indices across a term

107+--

108+-- weaken :: Int -> HTT -> HTT

109+-- weaken w (HV i) = HV (i + w)

110+-- weaken w (HBind n b sc)

111+-- = HBind n (weakenB b) (\x -> weaken w (sc x))

112+-- where weakenB (Lam t) = Lam (weaken w t)

113+-- weakenB (Pi t) = Pi (weaken w t)

114+-- weakenB (Let t v) = Let (weaken w t) (weaken w v)

115+-- weakenB (Hole t) = Hole (weaken w t)

116+-- weakenB (Guess t v) = Guess (weaken w t) (weaken w v)

117+-- weakenB (PVar t) = PVar (weaken w t)

118+-- weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)

119+-- weaken w tm = tm

120+--

71−quote :: Int -> HTT -> TT Name

121+-- quote :: Int -> HTT -> TT Name

72−quote env (HP nt n t) = P nt n (quote env t)

122+-- quote env (HP nt n t) = P nt n (quote env t)

73−quote env (HV i) = V i

123+-- quote env (HV i) = V i

74−quote env (HBind n b sc)

124+-- quote env (HBind n b sc)

75− = Bind n (quoteB b) (quote (env+1) (sc (HTmp (env+1))))

125+-- = Bind n (quoteB b) (quote (env+1) (sc (HTmp (env+1))))

76− where quoteB (Lam t) = Lam (quote env t)

126+-- where quoteB (Lam t) = Lam (quote env t)

77− quoteB (Pi t) = Pi (quote env t)

127+-- quoteB (Pi t) = Pi (quote env t)

78− quoteB (Let t v) = Let (quote env t) (quote env v)

128+-- quoteB (Let t v) = Let (quote env t) (quote env v)

79− quoteB (Hole t) = Hole (quote env t)

129+-- quoteB (Hole t) = Hole (quote env t)

80− quoteB (Guess t v) = Guess (quote env t) (quote env v)

130+-- quoteB (Guess t v) = Guess (quote env t) (quote env v)

81− quoteB (PVar t) = PVar (quote env t)

131+-- quoteB (PVar t) = PVar (quote env t)

82−quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)

132+-- quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)

83−quote env (HSet i) = Set i

133+-- quote env (HSet i) = Set i

84−quote env (HTmp i) = V (env-i)

134+-- quote env (HTmp i) = V (env-i)

src/Main.hs+5−3

@@ -10,6 +10,8 @@ import ProofShell

10main = do f <- readFile "test.mi"

11 let Right defs = parseFile f

12 print defs

13− let OK ctxt = checkProgram [] defs

13+ case checkProgram [] defs of

14− print ctxt

14+ OK ctxt -> do print ctxt

15− runShell (initState ctxt)

15+ runShell (initState ctxt)

16+ return ()

17+ err -> print err

src/ProofShell.hs+4−3

@@ -27,9 +27,10 @@ processCommand (Theorem n ty) state

27processCommand Quit state = (state { exitNow = True }, "Bye bye")

28processCommand (Eval t) state =

29 case check (ctxt state) [] t of

30− OK (val, _) ->

30+ OK (val, ty) ->

31− let nf = normalise (ctxt state) [] val in

31+ let nf = normalise (ctxt state) [] val

32+ tnf = normalise (ctxt state) [] ty in

32− (state, show nf)

33+ (state, show nf ++ " : " ++ show ty)

33 err -> (state, show err)

34 err -> (state, show err)

34processCommand (Tac t) state

35processCommand (Tac t) state

35 | Just ps <- prf state = case processTactic t ps of

36 | Just ps <- prf state = case processTactic t ps of

src/ProofState.hs+2−2

@@ -89,7 +89,7 @@ goal :: Hole -> Term -> Context -> TC Goal

89goal h tm ctxt = g [] tm where

90 g env (Bind n b sc) | hole b && same h n = return $ GD env b

91 | otherwise = gb env b `mplus` g ((n,b):env) sc

92− g env (App f t a) = g env f `mplus` g env t `mplus` g env a

92+ g env (App f a) = g env f `mplus` g env a

93 g env t = Error "Can't find hole"

95 gb env (Let t v) = g env t `mplus` g env v

@@ -104,7 +104,7 @@ tactic h ps ctxt f = do let tm = pterm ps

104 atH env binder@(Bind n b sc)

105 | hole b && same h n = f ctxt (weakenEnv env) binder

106 | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc

107− atH env (App f t a) = pure App <*> atH env f <*> atH env t <*> atH env a

107+ atH env (App f a) = pure App <*> atH env f <*> atH env a

108 atH env t = return t

109

110 atHb env (Let t v) = pure Let <*> atH env t <*> atH env v

src/Typecheck.hs+4−5

@@ -55,8 +55,8 @@ check ctxt env (RApp f a)

55 case fty' of

56 Bind x (Pi s) t ->

57 do converts ctxt env s aty

58− return (App fv fty av,

58+ return (App fv av,

59− normalise ctxt env (Bind x (Let av aty) t))

59+ normalise ctxt env (Bind x (Let aty av) t))

60 t -> fail "Can't apply a non-function type"

61check ctxt env (RSet i) = return (Set i, Set (i+1))

62check ctxt env (RBind n b sc)

@@ -123,9 +123,8 @@ check ctxt env (RBind n b sc)

123

124 checkNotHoley i (V v)

125 | v == i = fail "You can't put a hole where a hole don't belong"

126− checkNotHoley i (App f t a) = do checkNotHoley i f

126+ checkNotHoley i (App f a) = do checkNotHoley i f

127− checkNotHoley i t

128− checkNotHoley i a

127+ checkNotHoley i a

129 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc

128 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc

130 checkNotHoley _ _ = return ()

129 checkNotHoley _ _ = return ()

131

130

src/test.mi+1−1

@@ -3,7 +3,7 @@ O : N;

3S : N -> N;

5one : N = S O;

6−two : N = S one;

6+two : N = S (S O);

7three : N = S two;

9Vect : (A:Set 0) -> (n:N) -> Set 0;