019faba · Idris-dev · git.iko.soy

interp.minew file+61

compare with master

unifiedsplit

@@ -0,0 +1,61 @@

1+data Nat = O | S Nat;

2+

3+plus : Nat -> Nat -> Nat;

4+plus O y = y;

5+plus (S k) y = S (plus k y);

6+

7+data Ty = TyNat | TyFun Ty Ty;

8+

9+interpTy : Ty -> Set;

10+interpTy TyNat = Nat;

11+interpTy (TyFun s t) = interpTy s -> interpTy t;

12+

13+data Fin : Nat -> Set where

14+ fO : Fin (S k)

15+ | fS : Fin k -> Fin (S k);

16+

17+infixr 7 :: ;

18+

19+data Vect : Set -> Nat -> Set where

20+ VNil : Vect a O

21+ | (::) : a -> Vect a k -> Vect a (S k);

22+

23+data Env : Vect Ty n -> Set where

24+ Empty : Env VNil

25+ | Extend : {xs : Vect Ty n} -> interpTy a -> Env xs -> Env (a :: xs);

26+

27+lookup : (i : Fin n) -> Vect a n -> a;

28+lookup fO (x :: xs) = x;

29+lookup (fS i) (x :: xs) = lookup i xs;

30+

31+envLookup : {xs : Vect Ty n} ->

32+ (i : Fin n) -> Env xs -> interpTy (lookup i xs);

33+envLookup fO (Extend x xs) = x;

34+envLookup (fS i) (Extend x xs) = envLookup i xs;

35+

36+data Expr : Vect Ty n -> Ty -> Set where

37+ Var : {G : Vect Ty n} ->

38+ (i : Fin n) -> Expr G (lookup i G)

39+ | Val : {G : Vect Ty n} ->

40+ Nat -> Expr G TyNat

41+ | Lam : {G : Vect Ty n} ->

42+ Expr (a :: G) t -> Expr G (TyFun a t)

43+ | App : {G : Vect Ty n} ->

44+ Expr G (TyFun a t) -> Expr G a -> Expr G t

45+ | Add : {G : Vect Ty n} ->

46+ Expr G TyNat -> Expr G TyNat -> Expr G TyNat;

47+

48+interp : {G : Vect Ty n} ->

49+ Env G -> Expr G t -> interpTy t;

50+interp env (Var i) = envLookup i env;

51+interp env (Val x) = x;

52+interp env (Lam sc) = \x => interp (Extend x env) sc;

53+interp env (App f s) = (interp env f) (interp env s);

54+interp env (Add x y) = plus (interp env x) (interp env y);

55+

56+eAdd : {G : Vect Ty n} ->

57+ Expr G (TyFun TyNat (TyFun TyNat TyNat));

58+eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));

59+

60+test : Nat;

61+test = interp Empty eAdd (S (S O)) (S (S O));

src/Core/Elaborate.hs+1−1

@@ -268,5 +268,5 @@ try t1 t2 = do s <- get

268 case runStateT t1 s of

269 OK (v, s') -> do put s'

270 return v

271− _ -> t2

271+ _ -> do put s; t2

272

src/Core/TT.hs+5−1

@@ -193,6 +193,10 @@ finalise t = t

193subst :: Eq n => n -> TT n -> TT n -> TT n

194subst n v tm = instantiate v (pToV n tm)

195

196+substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

197+substNames [] t = t

198+substNames ((n, tm) : xs) t = subst n tm (substNames xs t)

199+

196-- Returns true if V 0 and bound name n do not occur in the term

200-- Returns true if V 0 and bound name n do not occur in the term

197

201

198noOccurrence :: Eq n => n -> TT n -> Bool

202noOccurrence :: Eq n => n -> TT n -> Bool

@@ -218,7 +222,7 @@ arity _ = 0

218unApply :: TT n -> (TT n, [TT n])

222unApply :: TT n -> (TT n, [TT n])

219unApply t = ua [] t where

223unApply t = ua [] t where

220 ua args (App f a) = ua (a:args) f

224 ua args (App f a) = ua (a:args) f

221− ua args t = (t, reverse args)

225+ ua args t = (t, args)

222

226

223mkApp :: TT n -> [TT n] -> TT n

227mkApp :: TT n -> [TT n] -> TT n

224mkApp f [] = f

228mkApp f [] = f

src/Core/Unify.hs+18−10

@@ -1,11 +1,10 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

2−

3module Core.Unify(unify) where

1module Core.Unify(unify) where

4

2

5import Core.TT

3import Core.TT

6import Core.Evaluate

4import Core.Evaluate

7

5

8import Control.Monad

6import Control.Monad

7+import Debug.Trace

9

8

10-- Unification is applied inside the theorem prover. We're looking for holes

9-- Unification is applied inside the theorem prover. We're looking for holes

11-- which can be filled in, by matching one term's normal form against another.

10-- which can be filled in, by matching one term's normal form against another.

@@ -16,9 +15,10 @@ import Control.Monad

16

15

17unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

16unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

18unify ctxt env x y

17unify ctxt env x y

19− = case un' [] x y of -- try without normalising first, for speed

18+ = --case un' [] x y of -- try without normalising first, for speed

20− OK v -> return v

19+ -- OK v -> return v

20+ -- _ ->

21− _ -> case un' [] (normalise ctxt env x) (normalise ctxt env y) of

21+ case un' [] (normalise ctxt env x) (normalise ctxt env y) of

22 OK v -> return v

23 _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y

24 where

@@ -61,18 +61,26 @@ unify ctxt env x y

61 (holeIn env x && okToUnify ynt) ||

62 (okToUnify xnt && holeIn env y)

63 = do h <- un' bnames xp yp

64− hargs <- zipWithM (un' bnames) xargs yargs

64+ uArgs bnames h xargs yargs

65− h' <- foldM (combine bnames) [] hargs

66− combine bnames h h'

67 uApp bnames (xf, xargs) (yf, yargs)

65 uApp bnames (xf, xargs) (yf, yargs)

68 = do un' bnames xf yf -- ignore result

66 = do un' bnames xf yf -- ignore result

69− hargs <- zipWithM (un' bnames) xargs yargs

67+ uArgs bnames [] xargs yargs

70− foldM (combine bnames) [] hargs

71

68

72 okToUnify (DCon _ _) = True

69 okToUnify (DCon _ _) = True

73 okToUnify (TCon _) = True

70 okToUnify (TCon _) = True

74 okToUnify _ = False

71 okToUnify _ = False

75

72

73+ uArgs bnames h [] [] = return h

74+ uArgs bnames h (x:xs) (y:ys) =

75+ case un' bnames x y of

76+ OK h' -> do next <- combine bnames h h'

77+ uArgs bnames next xs ys

78+ _ -> do let x' = normalise ctxt env (substNames h x)

79+ let y' = normalise ctxt env (substNames h y)

80+ h' <- un' bnames x' y'

81+ next <- combine bnames h h'

82+ uArgs bnames next xs ys

83+

76 combine bnames as [] = return as

84 combine bnames as [] = return as

77 combine bnames as ((n, t) : bs)

85 combine bnames as ((n, t) : bs)

78 = case lookup n as of

86 = case lookup n as of

src/Idris/AbsSyntax.hs+1−1

@@ -261,7 +261,7 @@ implicitise ist tm

261 imps env (PPi Imp n ty sc)

262 = do imps env ty

263 (impdecls, a, ns) <- get

264− put (n:impdecls, a+1, ns)

264+ put (n:impdecls, a, ns)

265 imps (n:env) sc

266 imps env (PPi Exp n ty sc)

267 = do imps env ty

src/Idris/ElabDecls.hs+3−3

@@ -151,11 +151,11 @@ elab pattern tm = do elab' tm

151 elab' sc

152 solve

153 elab' (PApp (PRef f) imps args)

154− = try (do apply_elab f (map toElab imps ++ map (Just . elab') args)

155− solve)

156− (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

154+ = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

157 solve

155 solve

158 elabArgs ns (map snd imps ++ args))

156 elabArgs ns (map snd imps ++ args))

157+ (do apply_elab f (map toElab imps ++ map (Just . elab') args)

158+ solve)

159 elab' (PApp f [] [arg])

160 = do simple_app (elab' f) (elab' arg)

161 solve