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

git.iko.soy/Idris-dev

Fixed unification; added well-typed interpreter

commit019faba82c9e362bf4e8347bd74be7575cab4eea authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 10 Oct 2011, 11:14 (15 years ago) parent739e0b5

6 files changed+89−16

compare with master

unifiedsplit

interp.mi+61 src/Core/Elaborate.hs+1−1 src/Core/TT.hs+5−1 src/Core/Unify.hs+18−10 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+3−3

interp.minew file+61

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

1+data Nat = O | S Nat;

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

4+plus O y = y;

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

7+data Ty = TyNat | TyFun Ty Ty;

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

268268 case runStateT t1 s of

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

270270 return v

271− _ -> t2

271+ _ -> do put s; t2

272272

src/Core/TT.hs+5−1

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

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

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

195195

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+

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

197201

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

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

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

219223unApply t = ua [] t where

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

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

225+ ua args t = (t, args)

222226

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

224228mkApp f [] = f

src/Core/Unify.hs+18−10

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

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

2−

31module Core.Unify(unify) where

53import Core.TT

64import Core.Evaluate

86import Control.Monad

7+import Debug.Trace

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

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

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

1615

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

1817unify ctxt env x y

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

20− OK v -> return v

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

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

19+ -- OK v -> return v

20+ -- _ ->

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

2222 OK v -> return v

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

2424 where

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

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

6262 (okToUnify xnt && holeIn env y)

6363 = do h <- un' bnames xp yp

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

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

66− combine bnames h h'

64+ uArgs bnames h xargs yargs

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

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

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

70− foldM (combine bnames) [] hargs

67+ uArgs bnames [] xargs yargs

7168

7269 okToUnify (DCon _ _) = True

7370 okToUnify (TCon _) = True

7471 okToUnify _ = False

7572

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+

7684 combine bnames as [] = return as

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

7886 = case lookup n as of

src/Idris/AbsSyntax.hs+1−1

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

261261 imps env (PPi Imp n ty sc)

262262 = do imps env ty

263263 (impdecls, a, ns) <- get

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

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

265265 imps (n:env) sc

266266 imps env (PPi Exp n ty sc)

267267 = do imps env ty

src/Idris/ElabDecls.hs+3−3

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

151151 elab' sc

152152 solve

153153 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)

157155 solve

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

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

158+ solve)

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

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

161161 solve