git.iko.soy/Idris-dev
on master help sign in
Add a 'compute' before elaboration to expand type synonyms etc

Useful for giving unification a hint when inferring types of lambda, case expressions, etc

commitdb96d75a3e05cba5598392ab8be253bff3af2991 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 13 Oct 2013, 15:21 (13 years ago) parent0d5c5b6
6 files changed+31−5
compare with master
unifiedsplit
idris.cabal+3 src/Core/ProofState.hs+6−4 src/Idris/ElabTerm.hs+1−1 test/reg022/expected test/reg022/reg022.idr+18 test/reg022/run+3
idris.cabal+3
@@ -160,6 +160,9 @@ Extra-source-files:
160160 test/reg020/run
161161 test/reg020/*.idr
162162 test/reg020/expected
163+ test/reg021/run
164+ test/reg021/*.idr
165+ test/reg021/expected
163166 test/test001/run
164167 test/test001/*.idr
165168 test/test001/expected
src/Core/ProofState.hs+6−4
@@ -176,13 +176,15 @@ unify' :: Context -> Env -> TT Name -> TT Name ->
176176unify' ctxt env topx topy =
177177 do ps <- get
178178 let dont = dontunify ps
179− (u, fails) <- traceWhen (unifylog ps) ("Trying " ++ show (topx, topy)) $
179+ (u, fails) <- traceWhen (unifylog ps)
180+ ("Trying " ++ show (topx, topy) ++
181+ " in " ++ show env ++
182+ "\nHoles: " ++ show (holes ps) ++ "\n") $
180183 lift $ unify ctxt env topx topy dont (holes ps)
181184 traceWhen (unifylog ps)
182185 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
183− " in " ++ show env ++
184− "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails ++ "\nCurrent problems:\n"
185− ++ qshow (problems ps) ++ "\nHoles: " ++ show (holes ps) ++ "\n"
186+ "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
187+ ++ "\nCurrent problems:\n" ++ qshow (problems ps)
186188-- ++ show (pterm ps)
187189 ++ "\n----------") $
188190 case fails of
src/Idris/ElabTerm.hs+1−1
@@ -97,6 +97,7 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
9797elab ist info pattern tcgen fn tm
9898 = do let loglvl = opt_logLevel (idris_options ist)
9999 when (loglvl > 5) $ unifyLog True
100+ compute -- expand type synonyms, etc
100101 elabE (False, False) tm -- (in argument, guarded)
101102 end_unify
102103 when pattern -- convert remaining holes to pattern vars
@@ -493,7 +494,6 @@ elab ist info pattern tcgen fn tm
493494 (caseBlock fc cname' (reverse args) opts)
494495 -- elaborate case
495496 env <- get_env
496− g <- goal
497497 updateAux (newdef : )
498498 -- if we haven't got the type yet, hopefully we'll get it later!
499499 movelast tyn
test/reg022/expectednew file

No changes to the content.

test/reg022/reg022.idrnew file+18
@@ -0,0 +1,18 @@
1+module reg022
2+
3+data Result str a = Success str a | Failure String
4+
5+instance Functor (Result str) where
6+ map f (Success s x) = Success s (f x)
7+ map f (Failure e ) = Failure e
8+
9+ParserT : (Type -> Type) -> Type -> Type -> Type
10+ParserT m str a = str -> m (Result str a)
11+
12+ap : Monad m => ParserT m str (a -> b) -> ParserT m str a ->
13+ ParserT m str b
14+ap f x = \s => do f' <- f s
15+ case f' of
16+ Failure e => (pure (Failure e))
17+ Success s' g => x s' >>= pure . map g
18+
test/reg022/runnew file+3
@@ -0,0 +1,3 @@
1+#!/bin/bash
2+idris $@ reg022.idr --check
3+rm -f *.ibc