git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of Idris-dev into issue3796
8afc195Edmund Smith
idris.cabal+3−9
compare with master
unifiedsplit
@@ -269,7 +269,7 @@ Library
269 , blaze-html >= 0.6.1.3 && < 0.10
269 , blaze-html >= 0.6.1.3 && < 0.10
270 , blaze-markup >= 0.5.2.1 && < 0.9
270 , blaze-markup >= 0.5.2.1 && < 0.9
271 , bytestring < 0.11
271 , bytestring < 0.11
272− , cheapskate < 0.2
272+ , cheapskate < 0.1.1
273 , code-page >= 0.1 && < 0.2
273 , code-page >= 0.1 && < 0.2
274 , containers >= 0.5 && < 0.6
274 , containers >= 0.5 && < 0.6
275 , deepseq < 1.5
275 , deepseq < 1.5
@@ -304,17 +304,11 @@ Library
304
304
305 ghc-prof-options: -auto-all -caf-all
305 ghc-prof-options: -auto-all -caf-all
306
306
307− if os(linux)
308− build-depends: unix < 2.8
309− if os(freebsd)
310− build-depends: unix < 2.8
311− if os(dragonfly)
312− build-depends: unix < 2.8
313− if os(darwin)
314− build-depends: unix < 2.8
315 if os(windows)
307 if os(windows)
316 build-depends: mintty >= 0.1 && < 0.2
308 build-depends: mintty >= 0.1 && < 0.2
317 , Win32 < 2.4
309 , Win32 < 2.4
310+ else
311+ build-depends: unix < 2.8
318 if flag(FFI)
312 if flag(FFI)
319 build-depends: libffi < 0.2
313 build-depends: libffi < 0.2
320 cpp-options: -DIDRIS_FFI
314 cpp-options: -DIDRIS_FFI
jsrts/Runtime-node.js+1−1
@@ -22,7 +22,7 @@ $JSRTS.prim_readStr = function () {
22 }
22 }
23 i++;
23 i++;
24 if (i == b.length) {
24 if (i == b.length) {
25− nb = new Buffer(b.length * 2);
25+ var nb = new Buffer(b.length * 2);
26 b.copy(nb)
26 b.copy(nb)
27 b = nb;
27 b = nb;
28 }
28 }
libs/pruviloj/Pruviloj/Core.idr+48−2
@@ -225,13 +225,16 @@ refine tm =
225 countPi (RBind _ (Pi _ _) body) = S (countPi body)
225 countPi (RBind _ (Pi _ _) body) = S (countPi body)
226 countPi _ = Z
226 countPi _ = Z
227
227
228+||| A helper to extract the type representation for term.
229+getTTType : Raw -> Elab TT
230+getTTType r = snd <$> check !getEnv r
228
231
229||| Split a pair into its projections, binding them in the context
232||| Split a pair into its projections, binding them in the context
230||| with the supplied names. A special case of Coq's `inversion`.
233||| with the supplied names. A special case of Coq's `inversion`.
231both : Raw -> TTName -> TTName -> Elab ()
234both : Raw -> TTName -> TTName -> Elab ()
232both tm n1 n2 =
235both tm n1 n2 =
233 do -- We don't know that the term is canonical, so let-bind projections applied to it
236 do -- We don't know that the term is canonical, so let-bind projections applied to it
234− (A, B) <- isPairTy (snd !(check !getEnv tm))
237+ (A, B) <- isPairTy !(getTTType tm)
235 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
238 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
236 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
239 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
237 where
240 where
@@ -253,7 +256,6 @@ unproduct tm =
253 try (unproduct (Var n1))
256 try (unproduct (Var n1))
254 try (unproduct (Var n2))
257 try (unproduct (Var n2))
255
258
256−
257||| A special-purpose tactic that attempts to solve a goal using
259||| A special-purpose tactic that attempts to solve a goal using
258||| `Refl`. This is useful for ensuring that goals in fact are trivial
260||| `Refl`. This is useful for ensuring that goals in fact are trivial
259||| when developing or testing other tactics; otherwise, consider
261||| when developing or testing other tactics; otherwise, consider
@@ -268,3 +270,47 @@ reflexivity =
268 , NamePart `{reflexivity}
270 , NamePart `{reflexivity}
269 , TextPart "is not applicable."
271 , TextPart "is not applicable."
270 ]
272 ]
273+
274+||| Attempt to swap the sides of equality in a goal. If the goal is `x = y`,
275+||| after the invocation the focus will be on a hole of type `y = x`.
276+symmetry : Elab ()
277+symmetry =
278+ do [_,_,_,_,res] <- apply (Var `{{sym}}) [True, True, True, True, False]
279+ | _ => fail [TextPart "Failed while applying", NamePart `{symmetry}]
280+ solve
281+ focus res
282+
283+||| Swap the sides of an equality, saving the result in a `let`-binding.
284+||| Returns the generated name.
285+|||
286+||| @ t the equality proof to swap
287+||| @ hint a hint to use for generating the variable name for the result
288+symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName
289+symmetryAs t hint =
290+ case !(getTTType t) of
291+ `((=) {A=~A} {B=~B} ~l ~r) =>
292+ do af <- forget A
293+ bf <- forget B
294+ lf <- forget l
295+ rf <- forget r
296+ let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)
297+ n <- gensym hint
298+ letbind n !(forget !(getTTType ts)) ts
299+ pure n
300+ tt => fail [TermPart tt, TextPart "is not an equality"]
301+
302+||| Apply a function term to an argument term, saving the result in a
303+||| `let`-binding. Returns the generated name.
304+|||
305+||| @ f the function to apply
306+||| @ x the term to apply to
307+||| @ hint a hint to use for generating the variable name for the result
308+applyAs : (f : Raw) -> (x : Raw) -> (hint : String) -> Elab TTName
309+applyAs f x hint =
310+ case !(getTTType f) of
311+ `(~xty -> ~yty) =>
312+ do let fx = RApp f x
313+ n <- gensym hint
314+ letbind n !(forget !(getTTType fx)) fx
315+ pure n
316+ ftt => fail [TermPart ftt, TextPart "is not a function"]