e613365 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

All names introduced by nachine should be MN, to avoid clashes

e613365Edwin Brady15 years ago

interp.mi+1−1

compare with master

unifiedsplit

@@ -27,7 +27,7 @@ data Env : Vect Ty n -> Set where

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

29lookup fO (x :: xs) = x;

30−lookup (fS i) (x :: xs) = lookup i xs;

30+lookup (fS k) (x :: xs) = lookup k xs;

32envLookup : {xs : Vect Ty n} ->

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

src/Core/Elaborate.hs+8−2

@@ -189,7 +189,7 @@ prepare_apply fn imps =

189 return claims

190 where

191 doClaims (Bind n' (Pi t) sc) (i : is) claims =

192− do n <- unique_hole n'

192+ do n <- unique_hole (mkMN n')

193 when (null claims) (start_unify n)

194 let sc' = instantiate (P Bound n t) sc

195 claim n (forget t)

@@ -198,6 +198,9 @@ prepare_apply fn imps =

198 doClaims t [] claims = return (reverse claims)

199 doClaims _ _ _ = fail "Wrong number of arguments"

200

201+ mkMN n@(MN _ _) = n

202+ mkMN n@(UN [x]) = MN 0 x

203+

201apply :: Raw -> [Bool] -> Elab [Name]

204apply :: Raw -> [Bool] -> Elab [Name]

202apply fn imps =

205apply fn imps =

203 do args <- prepare_apply fn imps

206 do args <- prepare_apply fn imps

@@ -224,7 +227,7 @@ apply_elab n args =

224 end_unify

227 end_unify

225 where

228 where

226 doClaims (Bind n' (Pi t) sc) (i : is) claims =

229 doClaims (Bind n' (Pi t) sc) (i : is) claims =

227− do n <- unique_hole n'

230+ do n <- unique_hole (mkMN n')

228 when (null claims) (start_unify n)

231 when (null claims) (start_unify n)

229 let sc' = instantiate (P Bound n t) sc

232 let sc' = instantiate (P Bound n t) sc

230 claim n (forget t)

233 claim n (forget t)

@@ -238,6 +241,9 @@ apply_elab n args =

238 do (p, _) <- get

241 do (p, _) <- get

239 focus n; elaboration; elabClaims xs

242 focus n; elaboration; elabClaims xs

240

243

244+ mkMN n@(MN _ _) = n

245+ mkMN n@(UN [x]) = MN 0 x

246+

241simple_app :: Elab () -> Elab () -> Elab ()

247simple_app :: Elab () -> Elab () -> Elab ()

242simple_app fun arg =

248simple_app fun arg =

243 do a <- unique_hole (MN 0 "a")

249 do a <- unique_hole (MN 0 "a")

src/Idris/ElabDecls.hs+1

@@ -76,6 +76,7 @@ elabClause (PClause _ lhs rhs)

76 (build True (infTerm lhs))

77 let lhs_tm = getInferTerm lhs'

78 let lhs_ty = getInferType lhs'

79+ logLvl 3 (show lhs_tm)

79 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

80 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

80 -- Now build the RHS, using the type of the LHS as the goal.

81 -- Now build the RHS, using the type of the LHS as the goal.

81 iLOG (showImp True rhs)

82 iLOG (showImp True rhs)