ecd9ead · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master' into providers

Conflicts: Setup.hs config.mk

commitecd9ead0ce5a532fc393d10d1949b62d9041dd13 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 5 Apr 2013, 17:47 (14 years ago) parent1f5ff74 d1cb783

16 files changed+835−81

compare with master

unifiedsplit

Setup.hs+23−12 config.mk+5−1 contribs/tool-support/vim/syntax/idris.vim+1−1 effects/Effects.idr+10−10 idris.cabal+4−1 lib/Language/Reflection.idr+166−9 lib/Prelude/Maybe.idr+1−1 samples/reflection.idr+151 src/Idris/AbsSyntaxTree.hs+6−1 src/Idris/Completion.hs+2 src/Idris/ElabTerm.hs+406−33 src/Idris/IBC.hs+12−4 src/Idris/Parser.hs+27−8 test/reg016/expected+6 test/reg016/reg016.idr+11 test/reg016/run+4

Setup.hs+23−12

@@ -47,7 +47,7 @@ cleanJavaLib verbosity

4747 execPomExists <- doesFileExist ("java" </> "executable_pom.xml")

4848 when pomExists $ removeFile ("java" </> "executable_pom.xml")

4949

50−installStdLib pkg local verbosity copy

50+installStdLib pkg local withoutEffects verbosity copy

5151 = do let dirs = L.absoluteInstallDirs pkg local copy

5252 let idir = datadir dirs

5353 let icmd = idrisCmd local

@@ -58,12 +58,13 @@ installStdLib pkg local verbosity copy

5858 , "IDRIS=" ++ icmd

5959 , "RTS=" ++ rtsDir local

6060 ]

61− make verbosity

62− [ "-C", "effects", "install"

63− , "TARGET=" ++ idir

64− , "IDRIS=" ++ icmd

65− , "RTS=" ++ rtsDir local

66− ]

61+ unless withoutEffects $

62+ make verbosity

63+ [ "-C", "effects", "install"

64+ , "TARGET=" ++ idir

65+ , "IDRIS=" ++ icmd

66+ , "RTS=" ++ rtsDir local

67+ ]

6768 let idirRts = idir </> "rts"

6869 putStrLn $ "Installing run time system in " ++ idirRts

6970 make verbosity

@@ -99,7 +100,7 @@ removeLibIdris local verbosity

99100 , "IDRIS=" ++ icmd

100101 ]

101102

102−checkStdLib local verbosity

103+checkStdLib local withoutEffects verbosity

103104 = do let icmd = idrisCmd local

104105 putStrLn $ "Building libraries..."

105106 make verbosity

@@ -107,7 +108,8 @@ checkStdLib local verbosity

107108 , "IDRIS=" ++ icmd

108109 , "RTS=" ++ rtsDir local

109110 ]

110− make verbosity

111+ unless withoutEffects $

112+ make verbosity

111113 [ "-C", "effects", "check"

112114 , "IDRIS=" ++ icmd

113115 , "RTS=" ++ rtsDir local

@@ -132,6 +134,12 @@ javaFlag flags =

132134 Just False -> False

133135 Nothing -> False

134136

137+noEffectsFlag flags =

138+ case lookup (FlagName "noeffects") (S.configConfigurationsFlags flags) of

139+ Just True -> True

140+ Just False -> False

141+ Nothing -> False

142+

135143preparePoms version

136144 = do pomTemplate <- TIO.readFile ("java" </> "pom_template.xml")

137145 TIO.writeFile ("java" </> "pom.xml") (insertVersion pomTemplate)

@@ -147,11 +155,13 @@ main = do

147155 defaultMainWithHooks $ simpleUserHooks

148156 { postCopy = \ _ flags pkg lbi -> do

149157 let verb = S.fromFlag $ S.copyVerbosity flags

150− installStdLib pkg lbi verb

158+ let withoutEffects = noEffectsFlag $ configFlags lbi

159+ installStdLib pkg lbi withoutEffects verb

151160 (S.fromFlag $ S.copyDest flags)

152161 , postInst = \ _ flags pkg lbi -> do

153162 let verb = (S.fromFlag $ S.installVerbosity flags)

154− installStdLib pkg lbi verb

163+ let withoutEffects = noEffectsFlag $ configFlags lbi

164+ installStdLib pkg lbi withoutEffects verb

155165 NoCopyDest

156166 when (javaFlag $ configFlags lbi)

157167 (installJavaLib pkg

@@ -172,6 +182,7 @@ main = do

172182 let verb = S.fromFlag $ S.buildVerbosity flags

173183 let distdir = buildDir lbi

174184 buildRTS distdir verb

175− checkStdLib lbi verb

185+ let withoutEffects = noEffectsFlag $ configFlags lbi

186+ checkStdLib lbi withoutEffects verb

176187 when (javaFlag $ configFlags lbi) (checkJavaLib verb)

177188 }

config.mk+5−1

@@ -1,9 +1,12 @@

11GMP_INCLUDE_DIR :=

22CC :=gcc

33CABAL :=cabal

4−CABALFLAGS :=

4+#CABALFLAGS :=

55## Enable Java RTS:

66#CABALFLAGS :=-f Java

7+## Disable building of Effects

8+#CABALFLAGS :=-f NoEffects

710

811MACHINE := $(shell $(CC) -dumpmachine)

912ifneq (, $(findstring darwin, $(MACHINE)))

@@ -29,3 +32,4 @@ else

2932 SHLIB_SUFFIX :=.so

3033endif

3134endif

35+

contribs/tool-support/vim/syntax/idris.vim+1−1

1515syn match idrisStatement "\<$do\|case\|of\|rewrite\|let\|in\|with$\>"

1616syn match idrisSyntax "$pattern \+\|term \+$\?syntax"

1717syn match idrisConditional "\<$if\|then\|else$\>"

1919syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"

2020syn match idrisFloat "\<[0-9]\+\.[0-9]\+$[eE][-+]\=[0-9]\+$\=\>"

2121syn match idrisDelimiter "(\|)\|\[\|\]\|,\|;\|_\|{\|}"

effects/Effects.idr+10−10

@@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

5959---- The Effect EDSL itself ----

6060

6161-- some proof automation

62−findEffElem : Nat -> Tactic -- Nat is maximum search depth

63−findEffElem O = Refine "Here" `Seq` Solve

64−findEffElem (S n) = GoalType "EffElem"

62+findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth

63+findEffElem O ctxt goal = Refine "Here" `Seq` Solve

64+findEffElem (S n) ctxt goal = GoalType "EffElem"

6565 (Try (Refine "Here" `Seq` Solve)

66− (Refine "There" `Seq` (Solve `Seq` findEffElem n)))

66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))

6767

68−findSubList : Nat -> Tactic

69−findSubList O = Refine "SubNil" `Seq` Solve

70−findSubList (S n)

68+findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic

69+findSubList O ctxt goal = Refine "SubNil" `Seq` Solve

70+findSubList (S n) ctxt goal

7171 = GoalType "SubList"

7272 (Try (Refine "subListId" `Seq` Solve)

7373 ((Try (Refine "Keep" `Seq` Solve)

74− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))

74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))

7575

7676updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

7777 List EFFECT

@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->

116116-- Eff : List (EFFECT m) -> Type -> Type

117117

118118implicit

119−lift' : {default tactics { reflect findSubList 100; solve; }

119+lift' : {default tactics { applyTactic findSubList 100; solve; }

120120 prf : SubList ys xs} ->

121121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t

122122lift' {prf} e = lift prf e

123123

124124implicit

125125effect' : {a, b: _} -> {e : Effect} ->

126− {default tactics { reflect findEffElem 100; solve; }

126+ {default tactics { applyTactic findEffElem 100; solve; }

127127 prf : EffElem e a xs} ->

128128 (eff : e a b t) ->

129129 EffM m xs (updateResTy xs prf eff) t

idris.cabal+4−1

@@ -65,7 +65,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

6565 config.mk

6666 rts/*.c rts/*.h rts/Makefile

6767 js/*.js

68− java/org/idris/rts/*.java

68+ java/org/idris/rts/*.java

6969

7070source-repository head

7171 type: git

@@ -75,6 +75,9 @@ Flag Java

7575 Description: Build the Java RTS

7676 Default: False

7777

78+Flag NoEffects

79+ Description: Do not build the effects package

80+ Default: False

7881

7982Executable idris

8083 Main-is: Main.hs

lib/Language/Reflection.idr+166−9

@@ -1,19 +1,176 @@

11module Language.Reflection

3−TTName : Type

4−TTName = String -- needs to capture namespaces too...

3+%access public

6−data TT = Var TTName

7− | Lam TTName TT TT

8− | Pi TTName TT TT

9− | Let TTName TT TT TT

10− | App TTName TT TT

5+data TTName = UN String

6+ -- ^ User-provided name

7+ | NS TTName (List String)

8+ -- ^ Root, namespaces

9+ | MN Int String

10+ -- ^ Machine chosen names

11+ | NErased

12+ -- ^ Name of somethng which is never used in scope

13+

14+implicit

15+userSuppliedName : String -> TTName

16+userSuppliedName = UN

17+

18+data TTUExp = UVar Int

19+ -- ^ universe variable

20+ | UVal Int

21+ -- ^ explicit universe variable

22+

23+-- | Primitive constants

24+data Const = I Int | BI Nat | Fl Float | Ch Char | Str String

26+ | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

27+ | B8Type | B16Type | B32Type | B64Type

28+ | PtrType | VoidType | Forgot

29+

30+abstract class ReflConst (a : Type) where

31+ toConst : a -> Const

32+

33+instance ReflConst Int where

34+ toConst x = I x

35+

36+instance ReflConst Nat where

37+ toConst = BI

38+

39+instance ReflConst Float where

40+ toConst = Fl

41+

42+instance ReflConst Char where

43+ toConst = Ch

44+

45+instance ReflConst String where

46+ toConst = Str

47+

48+instance ReflConst Bits8 where

49+ toConst = B8

50+

51+instance ReflConst Bits16 where

52+ toConst = B16

53+

54+instance ReflConst Bits32 where

55+ toConst = B32

56+

57+instance ReflConst Bits64 where

58+ toConst = B64

59+

60+implicit

61+reflectConstant: (ReflConst a) => a -> Const

62+reflectConstant = toConst

63+

64+

65+-- | Types of named references

66+data NameType = Bound

67+ -- ^ reference which is just bound, e.g. by intro

68+ | Ref

69+ -- ^ reference to a variable

70+ | DCon Int Int

71+ -- ^ constructor with tag and number

72+ | TCon Int Int

73+ -- ^ type constructor with tag and number

74+

75+-- | Types annotations for bound variables in different

76+-- binding contexts

77+data Binder a = Lam a

78+ | Pi a

79+ | Let a a

80+ | NLet a a

81+ | Hole a

82+ | GHole a

83+ | Guess a a

84+ | PVar a

85+ | PVTy a

86+

87+

88+instance Functor Binder where

89+ fmap f (Lam x) = Lam (f x)

90+ fmap f (Pi x) = Pi (f x)

91+ fmap f (Let x y) = Let (f x) (f y)

92+ fmap f (NLet x y) = NLet (f x) (f y)

93+ fmap f (Hole x) = Hole (f x)

94+ fmap f (GHole x) = GHole (f x)

95+ fmap f (Guess x y) = Guess (f x) (f y)

96+ fmap f (PVar x) = PVar (f x)

97+ fmap f (PVTy x) = PVTy (f x)

98+

99+total

100+traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)

101+traverse f (Lam x) = [| Lam (f x) |]

102+traverse f (Pi x) = [| Pi (f x) |]

103+traverse f (Let x y) = [| Let (f x) (f y) |]

104+traverse f (NLet x y) = [| NLet (f x) (f y) |]

105+traverse f (Hole x) = [| Hole (f x) |]

106+traverse f (GHole x) = [| GHole (f x) |]

107+traverse f (Guess x y) = [| Guess (f x) (f y) |]

108+traverse f (PVar x) = [| PVar (f x) |]

109+traverse f (PVTy x) = [| PVTy (f x) |]

110+

111+

112+-- | Reflection of the well typed core language

113+data TT = P NameType TTName TT

114+ -- ^ named binders

115+ | V Int

116+ -- ^ variables

117+ | Bind TTName (Binder TT) TT

118+ -- ^ type annotated named bindings

119+ | App TT TT

120+ -- ^ (named) application of a function to a value

121+ | TConst Const

122+ -- ^ constants

123+ | Proj TT Int

124+ -- ^ argument projection; runtime only

125+ | Erased

126+ -- ^ erased terms

127+ | Impossible

128+ -- ^ impossible terms

129+ | TType TTUExp

130+ -- ^ types

131+

132+-- | Raw terms without types

133+data Raw = Var TTName

134+ | RBind TTName (Binder Raw) Raw

135+ | RApp Raw Raw

136+ | RType

137+ | RForce Raw

138+ | RConstant Const

11139

12140data Tactic = Try Tactic Tactic

13− | GoalType TTName Tactic -- only run if the goal has the right type

141+ -- ^ try the first tactic and resort to the second one on failure

142+ | GoalType String Tactic

143+ -- ^ only run if the goal has the right type

14144 | Refine TTName

145+ -- ^ resolve function name, find matching arguments in the

146+ -- context and compute the proof target

15147 | Seq Tactic Tactic

148+ -- ^ apply both tactics in sequence

16149 | Trivial

150+ -- ^ intelligently construct the proof target from the context

17151 | Solve

18− | Exact TT -- not yet implemented

152+ -- ^ infer the proof target from the context

153+ | Intros

154+ -- ^ introduce all variables into the context

155+ | Intro TTName

156+ -- ^ introduce a named variable into the context, use the

157+ -- first one if the given name is not found

158+ | ApplyTactic TT

159+ -- ^ invoke the reflected rep. of another tactic

160+ | Reflect TT

161+ -- ^ turn a value into its reflected representation

162+ | Fill Raw

163+ -- ^ turn a raw value back into a term

164+ | Exact TT

165+ -- ^ use the given value to conclude the proof

166+ | Focus TTName

167+ -- ^ focus a named hole

168+ | Rewrite TT

169+ -- ^ rewrite using the reflected rep. of a equality proof

170+ | LetTac TTName TT

171+ -- ^ name a reflected term

172+ | LetTacTy TTName TT TT

173+ -- ^ name a reflected term and type it

174+ | Compute

175+ -- ^ normalise the context

19176

lib/Prelude/Maybe.idr+1−1

@@ -66,7 +66,7 @@ instance (Eq a) => Eq (Maybe a) where

6666-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to

6767-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be

6868-- turned into a monoid simply by adjoining an element i not in S

69−-- and defining i+i = i and i+s = s = s+i for all s ∈ S."

69+-- and defining i+i = i and i+s = s = s+i for all s in S."

7070

7171instance (Semigroup a) => Semigroup (Maybe a) where

7272 Nothing <+> m = m

samples/reflection.idrnew file+151

@@ -0,0 +1,151 @@

1+module ReflectionExamples

3+import Language.Reflection

5+-- | The reflected term for (\ x => reverse "bba")

6+reflectVal : TT

7+reflectVal = ?valPrf

9+-- | intEq for the integers 3 and 3

10+applyTac1 : Int

11+applyTac1 = ?tacPrf1

12+

13+-- | intEq for the integers 3 and 42

14+applyTac0 : Int

15+applyTac0 = ?tacPrf0

16+

17+-- | intEq for the two arguments

18+applyTacDyn : Int -> Int -> Int

19+applyTacDyn x y = ?tacPrfDyn

20+

21+-- | Restored version for RConstant (I 42)

22+fill : Int

23+fill = ?fillPrf

24+

25+-- | The type (TTName, TT) computed from its reflected raw rep.

26+envTuple : Type

27+envTuple = ?envTuplePrf

28+

29+-- | The type List (TTName, TT) computed from its reflected raw rep.

30+envList : List (TTName, TT)

31+envList = ?envListPrf

32+

33+-- | Reflected raw rep. for the type (TTName, TT)

34+tupleType : Raw

35+tupleType = RApp (RApp (Var (MN 0 "__Pair"))

36+ (Var (NS (UN "TTName") ["Reflection", "Language"])))

37+ (Var (NS (UN "TT") ["Reflection", "Language"]))

38+

39+-- | Reflected raw rep for the type List (TTName, TT)

40+mkTuple : Raw

41+mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))

42+ (Var (NS (UN "TTName") ["Reflection", "Language"])))

43+ (Var (NS (UN "TT") ["Reflection", "Language"]))

44+

45+-- | Reflected raw rep for Prelude.List.Nil

46+nil : Raw

47+nil = (Var (NS (UN "Nil") ["List", "Prelude"]))

48+

49+-- | Reflected raw rep for Prelude.List.::

50+cons : Raw

51+cons = (Var (NS (UN "::") ["List", "Prelude"]))

52+

53+-- | 1 if the two arguments are equal, 0 otherwise

54+-- This function is chosen as simple as possible for

55+-- demo purposes.

56+intEq : Int -> Int -> Int

57+intEq x y = case x == y of

58+ True => 1

59+ False => 0

60+

61+-- | A tactic script to run intEq on two let-bound or introduced

62+-- arguments of the current (otherwise empty) proof context

63+firstEq : List (TTName, Binder TT) -> TT -> Tactic

64+firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)

65+firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))

66+firstEq xs _ = Exact (TConst (I 0))

67+

68+-- | Skip 1 argument of the proof context and return the second one which

69+-- has to be introduced. Used for the tactical dispatch example, which

70+-- will push dispatch, as first env agrument.

71+innerTac : List (TTName, Binder TT) -> TT -> Tactic

72+innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)

73+

74+-- | Returns the reflected representation of innerTac

75+innerTacTT : TT

76+innerTacTT = ?innerTacTTPrf

77+

78+-- | Dispatch to the reflected rep. of innerTac

79+dispatch : List (TTName, Binder TT) -> TT -> Tactic

80+dispatch xs _ = ApplyTactic (innerTacTT)

81+

82+-- | Call dispatch which will then dispatch to innerTac.

83+tacticalDispatch : Int -> Int

84+tacticalDispatch = ?tacticalDispatchPrf

85+

86+-- | A tactic to get the representation of its goal

87+studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic

88+studyGoalTac _ goal = Reflect goal

89+

90+-- | Returns the representation of its goal, TT

91+-- (so this is reflect on the type TT)

92+studyGoal : TT

93+studyGoal = ?studyGoalPrf

94+

95+---------- Proofs ----------

96+

97+ReflectionExamples.studyGoalPrf = proof {

98+ applyTactic studyGoalTac;

99+}

100+

101+ReflectionExamples.envTuplePrf = proof {

102+ let x = tupleType;

103+ fill x;

104+}

105+

106+ReflectionExamples.envListPrf = proof {

107+ let x : Raw = RApp nil tupleType;

108+ fill x;

109+}

110+

111+

112+ReflectionExamples.valPrf = proof {

113+ let x : (List String -> String) = (\ x => reverse "bba");

114+ reflect x;

115+}

116+

117+

118+ReflectionExamples.tacPrf1 = proof {

119+ let f : (Int -> Int -> Int) = intEq;

120+ let x : Int = 3;

121+ let y : Int = 3;

122+ applyTactic firstEq;

123+}

124+

125+ReflectionExamples.tacPrf0 = proof {

126+ let f : (Int -> Int -> Int) = intEq;

127+ let x : Int = 3;

128+ let y : Int = 42;

129+ applyTactic firstEq;

130+}

131+

132+ReflectionExamples.tacPrfDyn = proof {

133+ let f : (Int -> Int -> Int) = intEq;

134+ intros;

135+ applyTactic firstEq;

136+}

137+

138+ReflectionExamples.fillPrf = proof {

139+ let x : Raw = RConstant (I 42);

140+ fill x;

141+}

142+

143+ReflectionExamples.innerTacTTPrf = proof {

144+ reflect innerTac;

145+}

146+

147+ReflectionExamples.tacticalDispatchPrf = proof {

148+ intros;

149+ applyTactic dispatch;

150+}

151+

src/Idris/AbsSyntaxTree.hs+6−1

@@ -530,7 +530,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

530530 | ProofState | ProofTerm | Undo

531531 | Try (PTactic' t) (PTactic' t)

532532 | TSeq (PTactic' t) (PTactic' t)

533− | ReflectTac t -- see Language.Reflection module

533+ | ApplyTactic t -- see Language.Reflection module

534+ | Reflect t

535+ | Fill t

534536 | GoalType String (PTactic' t)

535537 | Qed | Abandon

536538 deriving (Show, Eq, Functor)

@@ -555,6 +557,9 @@ instance Sized a => Sized (PTactic' a) where

555557 size Undo = 1

556558 size (Try l r) = 1 + size l + size r

557559 size (TSeq l r) = 1 + size l + size r

560+ size (ApplyTactic t) = 1 + size t

561+ size (Reflect t) = 1 + size t

562+ size (Fill t) = 1 + size t

558563 size Qed = 1

559564 size Abandon = 1

560565

src/Idris/Completion.hs+2

@@ -35,7 +35,9 @@ tacticArgs = [ ("intro", Nothing)

3535 , ("let", Nothing) -- FIXME syntax for let

3636 , ("focus", Just ExprTArg)

3737 , ("exact", Just ExprTArg)

38+ , ("applyTactic", Just ExprTArg)

3839 , ("reflect", Just ExprTArg)

40+ , ("fill", Just ExprTArg)

3941 , ("try", Just AltsTArg)

4042 ] ++ map (\x -> (x, Nothing)) [

4143 "intro", "intros", "compute", "trivial", "solve", "attack",

src/Idris/ElabTerm.hs+406−33

@@ -13,6 +13,7 @@ import Core.Evaluate

1313import Control.Monad

1414import Control.Monad.State

1515import Data.List

16+

1617import Debug.Trace

1718

1819-- Data to pass to recursively called elaborators; e.g. for where blocks,

@@ -774,22 +775,67 @@ runTac autoSolve ist tac = do env <- get_env

774775 runT Solve = solve

775776 runT (Try l r) = do try' (runT l) (runT r) True

776777 runT (TSeq l r) = do runT l; runT r

777− runT (ReflectTac tm) = do attack -- let x : Tactic = tm in ...

778− valn <- unique_hole (MN 0 "tacval")

779− claim valn (Var tacticTy)

780− tacn <- unique_hole (MN 0 "tacn")

781− letbind tacn (Var tacticTy) (Var valn)

782− focus valn

783− elab ist toplevel False False (MN 0 "tac") tm

784− (tm', ty') <- get_type_val (Var tacn)

785− ctxt <- get_context

786− env <- get_env

787− let tactic = normalise ctxt env tm'

788− runReflected tactic

789−-- p <- get_term

790−-- trace (show p ++ "\n\n") $

791− return ()

792− where tacticTy = tacm "Tactic"

778+ runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

779+ tgoal <- goal -- store the goal

780+ attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

781+ script <- unique_hole (MN 0 "script")

782+ claim script scriptTy

783+ scriptvar <- unique_hole (MN 0 "scriptvar" )

784+ letbind scriptvar scriptTy (Var script)

785+ focus script

786+ elab ist toplevel False False (MN 0 "tac") tm

787+ (script', _) <- get_type_val (Var scriptvar)

788+ -- now that we have the script apply

789+ -- it to the reflected goal and context

790+ restac <- unique_hole (MN 0 "restac")

791+ claim restac tacticTy

792+ focus restac

793+ fill (raw_apply (forget script')

794+ [reflectEnv tenv, reflect tgoal])

795+ restac' <- get_guess

796+ solve

797+ -- normalise the result in order to

798+ -- reify it

799+ ctxt <- get_context

800+ env <- get_env

801+ let tactic = normalise ctxt env restac'

802+ runReflected tactic

803+ where tacticTy = Var (reflm "Tactic")

804+ listTy = Var (NS (UN "List") ["List", "Prelude"])

805+ scriptTy = (RBind (UN "__pi_arg")

806+ (Pi (RApp listTy envTupleType))

807+ (RBind (UN "__pi_arg1")

808+ (Pi (Var $ reflm "TT")) tacticTy))

809+

810+ runT (Reflect v) = do attack -- let x = reflect v in ...

811+ tyn <- unique_hole (MN 0 "letty")

812+ claim tyn RType

813+ valn <- unique_hole (MN 0 "letval")

814+ claim valn (Var tyn)

815+ letn <- unique_hole (MN 0 "letvar")

816+ letbind letn (Var tyn) (Var valn)

817+ focus valn

818+ elab ist toplevel False False (MN 0 "tac") v

819+ (value, _) <- get_type_val (Var letn)

820+ ctxt <- get_context

821+ env <- get_env

822+ let value' = hnf ctxt env value

823+ runTac autoSolve ist (Exact $ PQuote (reflect value'))

824+ runT (Fill v) = do attack -- let x = fill x in ...

825+ tyn <- unique_hole (MN 0 "letty")

826+ claim tyn RType

827+ valn <- unique_hole (MN 0 "letval")

828+ claim valn (Var tyn)

829+ letn <- unique_hole (MN 0 "letvar")

830+ letbind letn (Var tyn) (Var valn)

831+ focus valn

832+ elab ist toplevel False False (MN 0 "tac") v

833+ (value, _) <- get_type_val (Var letn)

834+ ctxt <- get_context

835+ env <- get_env

836+ let value' = normalise ctxt env value

837+ rawValue <- reifyRaw value'

838+ runTac autoSolve ist (Exact $ PQuote rawValue)

793839 runT (GoalType n tac) = do g <- goal

794840 case unApply g of

795841 (P _ n' _, _) ->

@@ -799,24 +845,351 @@ runTac autoSolve ist tac = do env <- get_env

799845 _ -> fail "Wrong goal type"

800846 runT x = fail $ "Not implemented " ++ show x

801847

802− runReflected t = do t' <- reify t

848+ runReflected t = do t' <- reify ist t

803849 runTac autoSolve ist t'

804− tacm n = NS (UN n) ["Reflection", "Language"]

805−

806− reify :: Term -> ElabD PTactic

807− reify (P _ n _) | n == tacm "Trivial" = return Trivial

808− reify (P _ n _) | n == tacm "Solve" = return Solve

809− reify f@(App _ _)

810− | (P _ f _, args) <- unApply f = reifyAp f args

811− reify t = fail ("Unknown tactic " ++ show t)

812−

813− reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

814− reifyAp t [Constant (Str x)]

815− | t == tacm "Refine" = return $ Refine (UN x) []

816− reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

817− reifyAp t [Constant (Str n), x]

818− | t == tacm "GoalType" = liftM (GoalType n) (reify x)

819− reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

850+

851+-- | Prefix a name with the "Reflection.Language" namespace

852+reflm :: String -> Name

853+reflm n = NS (UN n) ["Reflection", "Language"]

854+

855+

856+-- | Reify tactics from their reflected representation

857+reify :: IState -> Term -> ElabD PTactic

858+reify _ (P _ n _) | n == reflm "Intros" = return Intros

859+reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

860+reify _ (P _ n _) | n == reflm "Solve" = return Solve

861+reify _ (P _ n _) | n == reflm "Compute" = return Compute

862+reify ist t@(App _ _)

863+ | (P _ f _, args) <- unApply t = reifyApp ist f args

864+reify _ t = fail ("Unknown tactic " ++ show t)

865+

866+reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

867+reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

868+reifyApp _ t [x]

869+ | t == reflm "Refine" = do n <- reifyTTName x

870+ return $ Refine n []

871+reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

872+reifyApp ist t [Constant (Str n), x]

873+ | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

874+reifyApp _ t [Constant (Str n)]

875+ | t == reflm "Intro" = return $ Intro [UN n]

876+reifyApp ist t [t']

877+ | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

878+reifyApp ist t [t']

879+ | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

880+reifyApp _ t [t']

881+ | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

882+reifyApp ist t [t']

883+ | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')

884+reifyApp ist t [x]

885+ | t == reflm "Focus" = liftM Focus (reifyTTName x)

886+reifyApp ist t [t']

887+ | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')

888+reifyApp ist t [n, t']

889+ | t == reflm "LetTac" = do n' <- reifyTTName n

890+ t'' <- reifyTT t'

891+ return $ LetTac n' (delab ist t')

892+reifyApp ist t [n, tt', t']

893+ | t == reflm "LetTacTy" = do n' <- reifyTTName n

894+ tt'' <- reifyTT tt'

895+ t'' <- reifyTT t'

896+ return $ LetTacTy n' (delab ist tt'') (delab ist t'')

897+reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

898+

899+-- | Reify terms from their reflected representation

900+reifyTT :: Term -> ElabD Term

901+reifyTT t@(App _ _)

902+ | (P _ f _, args) <- unApply t = reifyTTApp f args

903+reifyTT t@(P _ n _)

904+ | n == reflm "Erased" = return $ Erased

905+reifyTT t@(P _ n _)

906+ | n == reflm "Impossible" = return $ Impossible

907+reifyTT t = fail ("Unknown reflection term: " ++ show t)

908+

909+reifyTTApp :: Name -> [Term] -> ElabD Term

910+reifyTTApp t [nt, n, x]

911+ | t == reflm "P" = do nt' <- reifyTTNameType nt

912+ n' <- reifyTTName n

913+ x' <- reifyTT x

914+ return $ P nt' n' x'

915+reifyTTApp t [Constant (I i)]

916+ | t == reflm "V" = return $ V i

917+reifyTTApp t [n, b, x]

918+ | t == reflm "Bind" = do n' <- reifyTTName n

919+ b' <- reifyTTBinder reifyTT (reflm "TT") b

920+ x' <- reifyTT x

921+ return $ Bind n' b' x'

922+reifyTTApp t [f, x]

923+ | t == reflm "App" = do f' <- reifyTT f

924+ x' <- reifyTT x

925+ return $ App f' x'

926+reifyTTApp t [c]

927+ | t == reflm "TConst" = liftM Constant (reifyTTConst c)

928+reifyTTApp t [t', Constant (I i)]

929+ | t == reflm "Proj" = do t'' <- reifyTT t'

930+ return $ Proj t'' i

931+reifyTTApp t [tt]

932+ | t == reflm "TType" = liftM TType (reifyTTUExp tt)

933+reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

934+

935+-- | Reify raw terms from their reflected representation

936+reifyRaw :: Term -> ElabD Raw

937+reifyRaw t@(App _ _)

938+ | (P _ f _, args) <- unApply t = reifyRawApp f args

939+reifyRaw t@(P _ n _)

940+ | n == reflm "RType" = return $ RType

941+reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)

942+

943+reifyRawApp :: Name -> [Term] -> ElabD Raw

944+reifyRawApp t [n]

945+ | t == reflm "Var" = liftM Var (reifyTTName n)

946+reifyRawApp t [n, b, x]

947+ | t == reflm "RBind" = do n' <- reifyTTName n

948+ b' <- reifyTTBinder reifyRaw (reflm "Raw") b

949+ x' <- reifyRaw x

950+ return $ RBind n' b' x'

951+reifyRawApp t [f, x]

952+ | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)

953+reifyRawApp t [t']

954+ | t == reflm "RForce" = liftM RForce (reifyRaw t')

955+reifyRawApp t [c]

956+ | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

957+reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

958+

959+reifyTTName :: Term -> ElabD Name

960+reifyTTName t@(App _ _)

961+ | (P _ f _, args) <- unApply t = reifyTTNameApp f args

962+reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

963+

964+reifyTTNameApp :: Name -> [Term] -> ElabD Name

965+reifyTTNameApp t [Constant (Str n)]

966+ | t == reflm "UN" = return $ UN n

967+reifyTTNameApp t [n, ns]

968+ | t == reflm "NS" = do n' <- reifyTTName n

969+ ns' <- reifyTTNamespace ns

970+ return $ NS n' ns'

971+reifyTTNameApp t [Constant (I i), Constant (Str n)]

972+ | t == reflm "MN" = return $ MN i n

973+reifyTTNameApp t []

974+ | t == reflm "NErased" = return NErased

975+reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

976+

977+reifyTTNamespace :: Term -> ElabD [String]

978+reifyTTNamespace t@(App _ _)

979+ = case unApply t of

980+ (P _ f _, [Constant StrType])

981+ | f == NS (UN "Nil") ["List", "Prelude"] -> return []

982+ (P _ f _, [Constant StrType, Constant (Str n), ns])

983+ | f == NS (UN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

984+ _ -> fail ("Unknown reflection namespace arg: " ++ show t)

985+reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

986+

987+reifyTTNameType :: Term -> ElabD NameType

988+reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

989+reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

990+reifyTTNameType t@(App _ _)

991+ = case unApply t of

992+ (P _ f _, [Constant (I tag), Constant (I num)])

993+ | f == reflm "DCon" -> return $ DCon tag num

994+ | f == reflm "TCon" -> return $ TCon tag num

995+ _ -> fail ("Unknown reflection name type: " ++ show t)

996+reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

997+

998+reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

999+reifyTTBinder reificator binderType t@(App _ _)

1000+ = case unApply t of

1001+ (P _ f _, bt:args) | forget bt == Var binderType

1002+ -> reifyTTBinderApp reificator f args

1003+ _ -> fail ("Mismatching binder reflection: " ++ show t)

1004+reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

1005+

1006+reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

1007+reifyTTBinderApp reif f [t]

1008+ | f == reflm "Lam" = liftM Lam (reif t)

1009+reifyTTBinderApp reif f [t]

1010+ | f == reflm "Pi" = liftM Pi (reif t)

1011+reifyTTBinderApp reif f [x, y]

1012+ | f == reflm "Let" = liftM2 Let (reif x) (reif y)

1013+reifyTTBinderApp reif f [x, y]

1014+ | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)

1015+reifyTTBinderApp reif f [t]

1016+ | f == reflm "Hole" = liftM Hole (reif t)

1017+reifyTTBinderApp reif f [t]

1018+ | f == reflm "GHole" = liftM GHole (reif t)

1019+reifyTTBinderApp reif f [x, y]

1020+ | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

1021+reifyTTBinderApp reif f [t]

1022+ | f == reflm "PVar" = liftM PVar (reif t)

1023+reifyTTBinderApp reif f [t]

1024+ | f == reflm "PVTy" = liftM PVTy (reif t)

1025+reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

1026+

1027+reifyTTConst :: Term -> ElabD Const

1028+reifyTTConst (P _ n _) | n == reflm "IType" = return $ IType

1029+reifyTTConst (P _ n _) | n == reflm "BIType" = return $ BIType

1030+reifyTTConst (P _ n _) | n == reflm "FlType" = return $ FlType

1031+reifyTTConst (P _ n _) | n == reflm "ChType" = return $ ChType

1032+reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

1033+reifyTTConst (P _ n _) | n == reflm "B8Type" = return $ B8Type

1034+reifyTTConst (P _ n _) | n == reflm "B16Type" = return $ B16Type

1035+reifyTTConst (P _ n _) | n == reflm "B32Type" = return $ B32Type

1036+reifyTTConst (P _ n _) | n == reflm "B64Type" = return $ B64Type

1037+reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType

1038+reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

1039+reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

1040+reifyTTConst t@(App _ _)

1041+ | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

1042+reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

1043+

1044+reifyTTConstApp :: Name -> Term -> ElabD Const

1045+reifyTTConstApp f (Constant c@(I _))

1046+ | f == reflm "I" = return $ c

1047+reifyTTConstApp f (Constant c@(BI _))

1048+ | f == reflm "BI" = return $ c

1049+reifyTTConstApp f (Constant c@(Fl _))

1050+ | f == reflm "Fl" = return $ c

1051+reifyTTConstApp f (Constant c@(I _))

1052+ | f == reflm "Ch" = return $ c

1053+reifyTTConstApp f (Constant c@(Str _))

1054+ | f == reflm "Str" = return $ c

1055+reifyTTConstApp f (Constant c@(B8 _))

1056+ | f == reflm "B8" = return $ c

1057+reifyTTConstApp f (Constant c@(B16 _))

1058+ | f == reflm "B16" = return $ c

1059+reifyTTConstApp f (Constant c@(B32 _))

1060+ | f == reflm "B32" = return $ c

1061+reifyTTConstApp f (Constant c@(B64 _))

1062+ | f == reflm "B64" = return $ c

1063+reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

1064+

1065+reifyTTUExp :: Term -> ElabD UExp

1066+reifyTTUExp t@(App _ _)

1067+ = case unApply t of

1068+ (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

1069+ (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

1070+ _ -> fail ("Unknown reflection type universe expression: " ++ show t)

1071+reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

1072+

1073+-- | Create a reflected call to a named function/constructor

1074+reflCall :: String -> [Raw] -> Raw

1075+reflCall funName args

1076+ = raw_apply (Var (reflm funName)) args

1077+

1078+-- | Lift a term into its Language.Reflection.TT representation

1079+reflect :: Term -> Raw

1080+reflect (P nt n t)

1081+ = reflCall "P" [reflectNameType nt, reflectName n, reflect t]

1082+reflect (V n)

1083+ = reflCall "V" [RConstant (I n)]

1084+reflect (Bind n b x)

1085+ = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]

1086+reflect (App f x)

1087+ = reflCall "App" [reflect f, reflect x]

1088+reflect (Constant c)

1089+ = reflCall "TConst" [reflectConstant c]

1090+reflect (Proj t i)

1091+ = reflCall "Proj" [reflect t, RConstant (I i)]

1092+reflect (Erased) = Var (reflm "Erased")

1093+reflect (Impossible) = Var (reflm "Impossible")

1094+reflect (TType exp) = reflCall "TType" [reflectUExp exp]

1095+

1096+reflectNameType :: NameType -> Raw

1097+reflectNameType (Bound) = Var (reflm "Bound")

1098+reflectNameType (Ref) = Var (reflm "Ref")

1099+reflectNameType (DCon x y)

1100+ = reflCall "DCon" [RConstant (I x), RConstant (I y)]

1101+reflectNameType (TCon x y)

1102+ = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1103+

1104+reflectName :: Name -> Raw

1105+reflectName (UN str)

1106+ = reflCall "UN" [RConstant (Str str)]

1107+reflectName (NS n ns)

1108+ = reflCall "NS" [ reflectName n

1109+ , foldr (\ n s ->

1110+ raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )

1111+ [ RConstant StrType, RConstant (Str n), s ])

1112+ ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )

1113+ [ RConstant StrType ])

1114+ ns

1115+ ]

1116+reflectName (MN i n)

1117+ = reflCall "MN" [RConstant (I i), RConstant (Str n)]

1118+reflectName (NErased) = Var (reflm "NErased")

1119+

1120+reflectBinder :: Binder Term -> Raw

1121+reflectBinder (Lam t)

1122+ = reflCall "Lam" [Var (reflm "TT"), reflect t]

1123+reflectBinder (Pi t)

1124+ = reflCall "Pi" [Var (reflm "TT"), reflect t]

1125+reflectBinder (Let x y)

1126+ = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]

1127+reflectBinder (NLet x y)

1128+ = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]

1129+reflectBinder (Hole t)

1130+ = reflCall "Hole" [Var (reflm "TT"), reflect t]

1131+reflectBinder (GHole t)

1132+ = reflCall "GHole" [Var (reflm "TT"), reflect t]

1133+reflectBinder (Guess x y)

1134+ = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]

1135+reflectBinder (PVar t)

1136+ = reflCall "PVar" [Var (reflm "TT"), reflect t]

1137+reflectBinder (PVTy t)

1138+ = reflCall "PVTy" [Var (reflm "TT"), reflect t]

1139+

1140+reflectConstant :: Const -> Raw

1141+reflectConstant c@(I _) = reflCall "I" [RConstant c]

1142+reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

1143+reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

1144+reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

1145+reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

1146+reflectConstant (IType) = Var (reflm "IType")

1147+reflectConstant (BIType) = Var (reflm "BIType")

1148+reflectConstant (FlType) = Var (reflm "FlType")

1149+reflectConstant (ChType) = Var (reflm "ChType")

1150+reflectConstant (StrType) = Var (reflm "StrType")

1151+reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

1152+reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

1153+reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

1154+reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

1155+reflectConstant (B8Type) = Var (reflm "B8Type")

1156+reflectConstant (B16Type) = Var (reflm "B16Type")

1157+reflectConstant (B32Type) = Var (reflm "B32Type")

1158+reflectConstant (B64Type) = Var (reflm "B64Type")

1159+reflectConstant (PtrType) = Var (reflm "PtrType")

1160+reflectConstant (VoidType) = Var (reflm "VoidType")

1161+reflectConstant (Forgot) = Var (reflm "Forgot")

1162+

1163+reflectUExp :: UExp -> Raw

1164+reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

1165+reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

1166+

1167+-- | Reflect the environment of a proof into a List (TTName, Binder TT)

1168+reflectEnv :: Env -> Raw

1169+reflectEnv = foldr consToEnvList emptyEnvList

1170+ where

1171+ consToEnvList :: (Name, Binder Term) -> Raw -> Raw

1172+ consToEnvList (n, b) l

1173+ = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))

1174+ [ envTupleType

1175+ , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

1176+ , (RApp (Var $ reflm "Binder")

1177+ (Var $ reflm "TT"))

1178+ , reflectName n

1179+ , reflectBinder b

1180+ ]

1181+ , l

1182+ ]

1183+

1184+ emptyEnvList :: Raw

1185+ emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))

1186+ [envTupleType]

1187+

1188+envTupleType :: Raw

1189+envTupleType

1190+ = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

1191+ , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

1192+ ]

8201193

8211194solveAll = try (do solve; solveAll) (return ())

8221195

src/Idris/IBC.hs+12−4

@@ -21,7 +21,7 @@ import System.Directory

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 28

24+ibcVersion = 29

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -1390,8 +1390,12 @@ instance (Binary t) => Binary (PTactic' t) where

13901390 put x1

13911391 put x2

13921392 Qed -> putWord8 15

1393− ReflectTac x1 -> do putWord8 16

1394− put x1

1393+ ApplyTactic x1 -> do putWord8 16

1394+ put x1

1395+ Reflect x1 -> do putWord8 17

1396+ put x1

1397+ Fill x1 -> do putWord8 18

1398+ put x1

13951399 get

13961400 = do i <- getWord8

13971401 case i of

@@ -1424,7 +1428,11 @@ instance (Binary t) => Binary (PTactic' t) where

14241428 return (TSeq x1 x2)

14251429 15 -> return Qed

14261430 16 -> do x1 <- get

1427− return (ReflectTac x1)

1431+ return (ApplyTactic x1)

1432+ 17 -> do x1 <- get

1433+ return (Reflect x1)

1434+ 18 -> do x1 <- get

1435+ return (Fill x1)

14281436 _ -> error "Corrupted binary data for PTactic'"

14291437

14301438

src/Idris/Parser.hs+27−8

@@ -1,4 +1,4 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}

22-- | Parse the full Idris language.

33module Idris.Parser where

@@ -800,16 +800,30 @@ pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })

800800 symbol "=>"; rhs <- pExpr syn

801801 return (lhs, rhs)

802802

803+-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

804+-- big integer, otherwise try fromInteger and the constants as alternatives.

805+-- a better solution would be to fix fromInteger to work with Integer, as the

806+-- name suggests, rather than Int

807+

803808modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

804−modifyConst syn fc (PConstant (I x))

809+modifyConst syn fc (PConstant (BI x))

810+ | not (fitsInt x) = PAlternative False

811+ [PConstant (BI x),

812+ PApp fc (PRef fc (UN "fromInteger"))

813+ [pexp (PConstant (I (fromInteger x)))]]

805814 | not (inPattern syn)

806815 = PAlternative False

807− [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],

808− PConstant (I x), PConstant (BI (toEnum x))]

816+ [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I (fromInteger x)))],

817+ PConstant (I (fromInteger x)), PConstant (BI x)]

809818 | otherwise = PAlternative False

810− [PConstant (I x), PConstant (BI (toEnum x))]

819+ [PConstant (I (fromInteger x)), PConstant (BI x)]

811820modifyConst syn fc x = x

812821

822+fitsInt :: Integer -> Bool

823+fitsInt x = let xInt :: Int = fromInteger x

824+ xInteger :: Integer = toInteger xInt in

825+ x == xInteger

826+

813827pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

814828 return (mkList fc xs)

815829 where

@@ -1106,8 +1120,7 @@ pConstant = do reserved "Integer";return BIType

11061120 <|> do reserved "Bits32"; return B32Type

11071121 <|> do reserved "Bits64"; return B64Type

11081122 <|> try (do f <- float; return $ Fl f)

1109−-- <|> try (do i <- natural; lchar 'L'; return $ BI i)

1110− <|> try (do i <- natural; return $ I (fromInteger i))

1123+ <|> try (do i <- natural; return $ BI i)

11111124 <|> try (do s <- strlit; return $ Str s)

11121125 <|> try (do c <- chlit; return $ Ch c)

11131126

@@ -1537,9 +1550,15 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

15371550 <|> do reserved "exact"; t <- pExpr syn;

15381551 i <- getState

15391552 return $ Exact (desugar syn i t)

1553+ <|> do reserved "applyTactic"; t <- pExpr syn;

1554+ i <- getState

1555+ return $ ApplyTactic (desugar syn i t)

15401556 <|> do reserved "reflect"; t <- pExpr syn;

15411557 i <- getState

1542− return $ ReflectTac (desugar syn i t)

1558+ return $ Reflect (desugar syn i t)

1559+ <|> do reserved "fill"; t <- pExpr syn;

1560+ i <- getState

1561+ return $ Fill (desugar syn i t)

15431562 <|> do reserved "try"; t <- pTactic syn;

15441563 lchar '|';

15451564 t1 <- pTactic syn

test/reg016/expectednew file+6

@@ -0,0 +1,6 @@

1+4294967295

2+4294967296

3+4294967297

4+-1

5+0

6+1

test/reg016/reg016.idrnew file+11

@@ -0,0 +1,11 @@

1+module Main

3+main : IO ()

4+main = do print $ the Integer 4294967295

5+ print $ the Integer 4294967296

6+ print $ the Integer 4294967297

7+ print $ the Int 4294967295

8+ print $ the Int 4294967296

9+ print $ the Int 4294967297

10+

11+

test/reg016/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ reg016.idr -o reg016

3+./reg016

4+rm -f reg016 *.ibc