187f42f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Undo unification changes... because it's broken...

187f42fEdwin Brady14 years ago

src/Core/Elaborate.hs+1−1

compare with master

unifiedsplit

@@ -410,7 +410,7 @@ apply_elab n args =

410 do ty <- get_type (Var n)

411 ctxt <- get_context

412 env <- get_env

413− claims <- doClaims (finalise ty) args []

413+ claims <- doClaims (hnf ctxt env ty) args []

414 prep_fill n (map fst claims)

415 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

416 elabClaims [] False claims

src/Core/Unify.hs+9−8

@@ -69,12 +69,13 @@ unify ctxt env topx topy =

69 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

70 StateT UInfo

71 TC [(Name, TT Name)]

72+ un = un'

72− un fn names x y

73+-- un fn names x y

73− = let (xf, _) = unApply x

74+-- = let (xf, _) = unApply x

74− (yf, _) = unApply y in

75+-- (yf, _) = unApply y in

75− if headDiff xf yf then unifyFail x y else

76+-- if headDiff xf yf then unifyFail x y else

76− uplus (un' fn names x y)

77+-- uplus (un' fn names x y)

77− (un' fn names (hnf ctxt env x) (hnf ctxt env y))

78+-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

79 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

80 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

80 StateT UInfo

81 StateT UInfo

@@ -119,10 +120,10 @@ unify ctxt env topx topy =

119 (do hf <- un' True bnames fx fy

120 (do hf <- un' True bnames fx fy

120 let ax' = hnormalise hf ctxt env (substNames hf ax)

121 let ax' = hnormalise hf ctxt env (substNames hf ax)

121 let ay' = hnormalise hf ctxt env (substNames hf ay)

122 let ay' = hnormalise hf ctxt env (substNames hf ay)

122− ha <- un False bnames ax' ay'

123+ ha <- un' False bnames ax' ay'

123 sc 1

124 sc 1

124 combine bnames hf ha)

125 combine bnames hf ha)

125− (do ha <- un False bnames ax ay

126+ (do ha <- un' False bnames ax ay

126 let fx' = hnormalise ha ctxt env (substNames ha fx)

127 let fx' = hnormalise ha ctxt env (substNames ha fx)

127 let fy' = hnormalise ha ctxt env (substNames ha fy)

128 let fy' = hnormalise ha ctxt env (substNames ha fy)

128 hf <- un' False bnames fx' fy'

129 hf <- un' False bnames fx' fy'

src/Idris/ElabTerm.hs+9−12

@@ -289,27 +289,24 @@ elab ist info pattern tcgen fn tm

289 ctxt <- get_context

290 let guarded = isConName Nothing f ctxt

291-- when True

292− (ns, committed) <- tryWhen True

292+ tryWhen True

293 (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

294+ ptm <- get_term

301− let (ns', eargs) = unzip $

295+ let (ns', eargs) = unzip $

302 sortBy (\(_,x) (_,y) ->

296 sortBy (\(_,x) (_,y) ->

303 compare (priority x) (priority y))

297 compare (priority x) (priority y))

304 (zip ns args)

298 (zip ns args)

305− tryWhen True

299+ tryWhen True

306 (elabArgs (ina || not isinf, guarded)

300 (elabArgs (ina || not isinf, guarded)

307 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

301 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

308 (elabArgs (ina || not isinf, guarded)

302 (elabArgs (ina || not isinf, guarded)

309 [] False (reverse ns')

303 [] False (reverse ns')

310 (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

304 (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

305+ mkSpecialised ist fc f (map getTm args') tm

306+ solve)

307+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

311− mkSpecialised ist fc f (map getTm args') tm

308+ mkSpecialised ist fc f (map getTm args') tm

312− solve

309+ solve)

313-- ptm <- get_term

310-- ptm <- get_term

314-- elog (show ptm)

311-- elog (show ptm)

315 ivs' <- get_instances

312 ivs' <- get_instances