git.iko.soy/Idris-dev
on master help sign in
Undo unification changes... because it's broken...
commit187f42feedae6d21f74e88cdf89e409838f79cb6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jan 2013, 16:58 (14 years ago) parentb1684a7
3 files changed+19−21
compare with master
unifiedsplit
src/Core/Elaborate.hs+1−1 src/Core/Unify.hs+9−8 src/Idris/ElabTerm.hs+9−12
src/Core/Elaborate.hs+1−1
@@ -410,7 +410,7 @@ apply_elab n args =
410410 do ty <- get_type (Var n)
411411 ctxt <- get_context
412412 env <- get_env
413− claims <- doClaims (finalise ty) args []
413+ claims <- doClaims (hnf ctxt env ty) args []
414414 prep_fill n (map fst claims)
415415 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
416416 elabClaims [] False claims
src/Core/Unify.hs+9−8
@@ -69,12 +69,13 @@ unify ctxt env topx topy =
6969 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
7070 StateT UInfo
7171 TC [(Name, TT Name)]
72− un fn names x y
73− = let (xf, _) = unApply x
74− (yf, _) = unApply y in
75− if headDiff xf yf then unifyFail x y else
76− uplus (un' fn names x y)
77− (un' fn names (hnf ctxt env x) (hnf ctxt env y))
72+ un = un'
73+-- un fn names x y
74+-- = let (xf, _) = unApply x
75+-- (yf, _) = unApply y in
76+-- if headDiff xf yf then unifyFail x y else
77+-- uplus (un' fn names x y)
78+-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
7879
7980 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
8081 StateT UInfo
@@ -119,10 +120,10 @@ unify ctxt env topx topy =
119120 (do hf <- un' True bnames fx fy
120121 let ax' = hnormalise hf ctxt env (substNames hf ax)
121122 let ay' = hnormalise hf ctxt env (substNames hf ay)
122− ha <- un False bnames ax' ay'
123+ ha <- un' False bnames ax' ay'
123124 sc 1
124125 combine bnames hf ha)
125− (do ha <- un False bnames ax ay
126+ (do ha <- un' False bnames ax ay
126127 let fx' = hnormalise ha ctxt env (substNames ha fx)
127128 let fy' = hnormalise ha ctxt env (substNames ha fy)
128129 hf <- un' False bnames fx' fy'
src/Idris/ElabTerm.hs+9−12
@@ -289,27 +289,24 @@ elab ist info pattern tcgen fn tm
289289 ctxt <- get_context
290290 let guarded = isConName Nothing f ctxt
291291-- when True
292− (ns, committed) <- tryWhen True
292+ tryWhen True
293293 (do ns <- apply (Var f) (map isph args)
294− return (ns, True)) -- commit to this branch here
295− (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
296− mkSpecialised ist fc f (map getTm args') tm
297− solve
298− return ([], False))
299− when committed $
300− do ptm <- get_term
301− let (ns', eargs) = unzip $
294+ ptm <- get_term
295+ let (ns', eargs) = unzip $
302296 sortBy (\(_,x) (_,y) ->
303297 compare (priority x) (priority y))
304298 (zip ns args)
305− tryWhen True
299+ tryWhen True
306300 (elabArgs (ina || not isinf, guarded)
307301 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
308302 (elabArgs (ina || not isinf, guarded)
309303 [] False (reverse ns')
310304 (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))
311− mkSpecialised ist fc f (map getTm args') tm
312− solve
305+ mkSpecialised ist fc f (map getTm args') tm
306+ solve)
307+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
308+ mkSpecialised ist fc f (map getTm args') tm
309+ solve)
313310-- ptm <- get_term
314311-- elog (show ptm)
315312 ivs' <- get_instances