b048140 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -5,6 +5,9 @@ New in 0.9.17:

5* A new tactic "claim N TY" that introduces a new hole named N with type TY

6* A new tactic "unfocus" that moves the current hole to the bottom of the

7 hole stack

8+* Quasiquotation supports the generation of Language.Reflection.Raw terms

9+ in addition to Language.Reflection.TT. Types are used for disambiguation,

10+ defaulting to TT at the REPL.

8

11

9New in 0.9.16:

12New in 0.9.16:

10--------------

13--------------

idris.cabal+3

@@ -513,6 +513,9 @@ Extra-source-files:

513 test/quasiquote004/run

514 test/quasiquote004/*.idr

515 test/quasiquote004/expected

516+ test/quasiquote005/run

517+ test/quasiquote005/*.idr

518+ test/quasiquote005/expected

516

519

517

520

518 test/records001/run

521 test/records001/run

src/Idris/ElabTerm.hs+5−2

@@ -940,10 +940,13 @@ elab ist info emode opts fn tm

940 elab' ina fc (PQuasiquote t goal)

941 = do -- First extract the unquoted subterms, replacing them with fresh

942 -- names in the quasiquoted term. Claim their reflections to be

943− -- of type TT.

943+ -- an inferred type (to support polytypic quasiquotes).

944 (t, unq) <- extractUnquotes 0 t

945 let unquoteNames = map fst unq

946+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

947+ claim uqh RType

948+ movelast uqh

946− mapM_ (flip claim (Var tt)) unquoteNames

949+ claim uqn (Var uqh)) unquoteNames

947

950

948

951

949 -- Save the old state - we need a fresh proof state to avoid

952 -- Save the old state - we need a fresh proof state to avoid

test/quasiquote005/Quasiquote005.idrnew file+9

@@ -0,0 +1,9 @@

1+module Quasiquote005

2+

3+test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =

4+ RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))

5+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

6+ (Var (NS (UN "Z") ["Nat", "Prelude"]))))

7+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

8+ (Var (NS (UN "Z") ["Nat", "Prelude"])))

9+test = Refl

test/quasiquote005/expectednew file

No changes to the content.

test/quasiquote005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --check --nocolour Quasiquote005.idr

3+rm -f *.ibc