ef3aed2 · Idris-dev · git.iko.soy

rts/idris_rts.h+1−1

@@ -98,7 +98,7 @@ typedef intptr_t i_int;

98#define ISINT(x) ((((i_int)x)&1) == 1)

99

100#define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))

101−#define FLOATOP(op,x,y) MKFLOAT(((GETFLOAT(x)) op (GETFLOAT(y))))

101+#define FLOATOP(op,x,y) MKFLOAT(vm, ((GETFLOAT(x)) op (GETFLOAT(y))))

102#define FLOATBOP(op,x,y) MKINT((i_int)(((GETFLOAT(x)) op (GETFLOAT(y)))))

103#define ADD(x,y) (void*)(((i_int)x)+(((i_int)y)-1))

104#define MULT(x,y) (MKINT((((i_int)x)>>1) * (((i_int)y)>>1)))

src/Core/Elaborate.hs+6−1

@@ -441,7 +441,12 @@ try t1 t2 = do s <- get

441 Error e2 -> if score e1 > score e2

442 then lift (tfail e1)

443 else lift (tfail e2)

444−

444+

445+tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

446+tryWhen True a b = try a b

447+tryWhen False a b = a

448+

449+

445-- Try a selection of tactics. Exactly one must work, all others must fail

450-- Try a selection of tactics. Exactly one must work, all others must fail

446tryAll :: [(Elab' aux a, String)] -> Elab' aux a

451tryAll :: [(Elab' aux a, String)] -> Elab' aux a

447tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

452tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

src/Idris/ElabTerm.hs+1−1

@@ -235,7 +235,7 @@ elab ist info pattern tcgen fn tm

235 ctxt <- get_context

236 let guarded = isConName Nothing f ctxt

237-- when True

238− try

238+ tryWhen True

239 (do ns <- apply (Var f) (map isph args)

240 let (ns', eargs)

241 = unzip $