e613365 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commite613365f9300449da9bad01c2befcb462ac19424 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 10 Oct 2011, 12:34 (15 years ago) parent2378a62

3 files changed+10−3

compare with master

unifiedsplit

interp.mi+1−1 src/Core/Elaborate.hs+8−2 src/Idris/ElabDecls.hs+1

interp.mi+1−1

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

2727

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

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

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

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

3131

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

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

src/Core/Elaborate.hs+8−2

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

189189 return claims

190190 where

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

192− do n <- unique_hole n'

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

193193 when (null claims) (start_unify n)

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

195195 claim n (forget t)

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

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

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

200200

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

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

203+

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

202205apply fn imps =

203206 do args <- prepare_apply fn imps

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

224227 end_unify

225228 where

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

227− do n <- unique_hole n'

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

228231 when (null claims) (start_unify n)

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

230233 claim n (forget t)

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

238241 do (p, _) <- get

239242 focus n; elaboration; elabClaims xs

240243

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

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

246+

241247simple_app :: Elab () -> Elab () -> Elab ()

242248simple_app fun arg =

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

src/Idris/ElabDecls.hs+1

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

7676 (build True (infTerm lhs))

7777 let lhs_tm = getInferTerm lhs'

7878 let lhs_ty = getInferType lhs'

79+ logLvl 3 (show lhs_tm)

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

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

8182 iLOG (showImp True rhs)