6c4deb2 · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Elab.idr+21−16

compare with master

unifiedsplit

@@ -37,8 +37,8 @@ data Plicity =

37||| used for functions.

38record FunArg where

39 constructor MkFunArg

40− argName : TTName

40+ name : TTName

41− argTy : Raw

41+ type : Raw

42 plicity : Plicity

43 erasure : Erasure

44

@@ -54,25 +54,30 @@ data TyConArg =

54 TyConIndex FunArg

55

56||| A type declaration

57−data TyDecl : Type where

57+record TyDecl where

58− ||| A type declaration.

58+ constructor Declare

59− |||

59+

60+ ||| The name of the function being declared.

61+ name : TTName

62+

60− ||| Each argument is in the scope of the names of previous

63+ ||| Each argument is in the scope of the names of previous arguments.

61− ||| arguments, and the return type is in the scope of all the

64+ arguments : List FunArg

62− ||| argument names.

65+

63− |||

66+ ||| The return type is in the scope of all the argument names.

64− ||| @ fn the name to be declared, fully-qualified

67+ returnType : Raw

65− ||| @ args the arguments to the function

68+

66− ||| @ ret the final return type

67− Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl

68

69

70+-- Note: FunClause is not a record because impossible clauses may be

71+-- added at some point.

69||| A single pattern-matching clause

72||| A single pattern-matching clause

70data FunClause : Type where

73data FunClause : Type where

71 MkFunClause : (lhs, rhs : Raw) -> FunClause

74 MkFunClause : (lhs, rhs : Raw) -> FunClause

72

75

73||| A reflected function definition.

76||| A reflected function definition.

74−data FunDefn : Type where

77+record FunDefn where

78+ constructor DefineFun

79+ name : TTName

75− DefineFun : TTName -> List FunClause -> FunDefn

80+ clauses : List FunClause

76

81

77

82

78data CtorArg = CtorParameter FunArg | CtorField FunArg

83data CtorArg = CtorParameter FunArg | CtorField FunArg

@@ -82,7 +87,7 @@ record Datatype where

82 constructor MkDatatype

87 constructor MkDatatype

83

88

84 ||| The name of the type constructor

89 ||| The name of the type constructor

85− familyName : TTName

90+ name : TTName

86

91

87 ||| The arguments to the type constructor

92 ||| The arguments to the type constructor

88 tyConArgs : List TyConArg

93 tyConArgs : List TyConArg

libs/pruviloj/Pruviloj/Core.idr+16

@@ -222,3 +222,19 @@ unproduct tm =

222 both tm n1 n2

223 try (unproduct (Var n1))

224 try (unproduct (Var n2))

225+

226+

227+||| A special-purpose tactic that attempts to solve a goal using

228+||| `Refl`. This is useful for ensuring that goals in fact are trivial

229+||| when developing or testing other tactics; otherwise, consider

230+||| using `search`.

231+reflexivity : Elab ()

232+reflexivity =

233+ case !goalType of

234+ `((=) {A=~A} {B=~_} ~x ~_) =>

235+ do fill `(Refl {A=~A} {x=~x})

236+ solve

237+ _ => fail [ TextPart "The goal is not an equality, so"

238+ , NamePart `{reflexivity}

239+ , TextPart "is not applicable."

240+ ]

libs/pruviloj/Pruviloj/Derive/Eliminators.idr+9−9

@@ -86,10 +86,10 @@ elabMethodTy info motiveName [] res ctorApp =

86 focus argH; fill ctorApp; solve

87 solve

88elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =

89− elabMethodTy info motiveName args res (RApp ctorApp (Var (argName arg)))

89+ elabMethodTy info motiveName args res (RApp ctorApp (Var (name arg)))

90elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =

91− do let n = argName arg

91+ do let n = name arg

92− let t = argTy arg

92+ let t = type arg

93 attack; forall n t

94 mkIh info motiveName n t (result info)

95 elabMethodTy info motiveName args res (RApp ctorApp (Var n))

@@ -153,8 +153,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

153 for {b=()} args $ \arg =>

154 case arg of

155 CtorParameter _ => return ()

156− CtorField arg => do claim (argName arg) (argTy arg)

156+ CtorField arg => do claim (name arg) (type arg)

157− unfocus (argName arg)

157+ unfocus (name arg)

158

159 -- Establish a hole for the scrutinee (infer type)

160 scrutinee <- newHole "scrutinee" resTy

@@ -177,8 +177,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

177 focus scrutinee

178 apply (mkApp (Var cn) $

179 map (\x => case x of

180− CtorParameter param => Var (argName param)

180+ CtorParameter param => Var (name param)

181− CtorField arg => Var (argName arg))

181+ CtorField arg => Var (name arg))

182 args)

183 []

184 solve)

@@ -195,8 +195,8 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

195 case x of

196 CtorParameter _ => return List.Nil

197 CtorField arg =>

198− do let n = argName arg

198+ do let n = name arg

199− let t = argTy arg

199+ let t = type arg

200 (argArgs, argRes) <- stealBindings t (const Nothing)

201 if headsMatch argRes (result info) --recursive

202 then return [ NormalArgument n

libs/pruviloj/Pruviloj/Injective.idr+4−4

@@ -43,10 +43,10 @@ getInjectivity cn = exists <|> declare

43 let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)

44 `(() : Type)

45 (map (\(a1, a2) =>

46− `((=) {A=~(argTy a1)}

46+ `((=) {A=~(type a1)}

47− {B=~(argTy a2)}

47+ {B=~(type a2)}

48− ~(Var (argName a1))

48+ ~(Var (name a1))

49− ~(Var (argName a2))))

49+ ~(Var (name a2))))

50 (zip impls1 impls2))

51

52 declareType $ Declare fn (impls1 ++ impls2 ++

libs/pruviloj/Pruviloj/Internals.idr+6−6

@@ -9,20 +9,20 @@ import Data.Vect

9

10||| Get the name of a reflected type constructor argument.

11tyConArgName : TyConArg -> TTName

12−tyConArgName (TyConParameter a) = argName a

12+tyConArgName (TyConParameter a) = name a

13−tyConArgName (TyConIndex a) = argName a

13+tyConArgName (TyConIndex a) = name a

14

15||| Modify the name of a reflected type constructor argument.

16setTyConArgName : TyConArg -> TTName -> TyConArg

17−setTyConArgName (TyConParameter a) n = TyConParameter (record {argName = n} a)

17+setTyConArgName (TyConParameter a) n = TyConParameter (record {name = n} a)

18−setTyConArgName (TyConIndex a) n = TyConIndex (record {argName = n} a)

18+setTyConArgName (TyConIndex a) n = TyConIndex (record {name = n} a)

19

20||| Modify the type of a reflected type constructor argument using some function.

21updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg

22updateTyConArgTy f (TyConParameter a) =

23− TyConParameter (record {argTy = f (argTy a) } a)

23+ TyConParameter (record {type = f (type a) } a)

24updateTyConArgTy f (TyConIndex a) =

25− TyConIndex (record {argTy = f (argTy a) } a)

25+ TyConIndex (record {type = f (type a) } a)

26

27unApply : Raw -> (Raw, List Raw)

28unApply tm = unApply' tm []

libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+11−11

@@ -23,13 +23,13 @@ record TyConInfo where

23getParams : TyConInfo -> List (TTName, Raw)

24getParams info = mapMaybe param (args info)

25 where param : TyConArg -> Maybe (TTName, Raw)

26− param (TyConParameter a) = Just (argName a, argTy a)

26+ param (TyConParameter a) = Just (name a, type a)

27 param _ = Nothing

28

29getIndices : TyConInfo -> List (TTName, Raw)

30getIndices info = mapMaybe index (args info)

31 where index : TyConArg -> Maybe (TTName, Raw)

32− index (TyConIndex a) = Just (argName a, argTy a)

32+ index (TyConIndex a) = Just (name a, type a)

33 index _ = Nothing

34

35||| Rename a bound variable across a telescope

@@ -75,7 +75,7 @@ processCtorArgs info (cn, cargs, resTy) =

75 findParam : TTName -> List Raw -> List TyConArg -> Elab TTName

76 findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =

77 if n == paramN

78− then return (argName a)

78+ then return (name a)

79 else findParam paramN args tcArgs

80 findParam paramN (_ :: args) (_ :: tcArgs) =

81 findParam paramN args tcArgs

@@ -89,20 +89,20 @@ processCtorArgs info (cn, cargs, resTy) =

89 TyConInfo -> Elab (List CtorArg, Raw)

90 convert' subst [] ty info = return ([], alphaRaw subst ty)

91 convert' subst (CtorField a :: args) ty info =

92− do n' <- nameFrom (argName a)

92+ do n' <- nameFrom (name a)

93 let a' = record {

94− argName = n'

94+ name = n'

95− , argTy = alphaRaw subst (argTy a)

95+ , type = alphaRaw subst (type a)

96 } a

97− let subst' = extend subst (argName a) n'

97+ let subst' = extend subst (name a) n'

98 (args', ty') <- convert' subst' args ty info

99 return (CtorField a' :: args', ty')

100 convert' subst (CtorParameter a :: ctorArgs) ty info =

101− do n' <- findParam (argName a) (snd (unApply ty)) (args info)

101+ do n' <- findParam (name a) (snd (unApply ty)) (args info)

102 let a' = record {

103− argName = n'

103+ name = n'

104− , argTy = alphaRaw subst (argTy a)

104+ , type = alphaRaw subst (type a)

105 } a

106− let subst' = extend subst (argName a) n'

106+ let subst' = extend subst (name a) n'

107 (args', ty') <- convert' subst' ctorArgs ty info

108 return (CtorParameter a' :: args', ty')

src/Idris/Core/Binary.hs+3−1

@@ -190,7 +190,8 @@ instance Binary a => Binary (Err' a) where

190 put e

191 put (ElabScriptStaging n) = do putWord8 43

192 put n

193−

193+ put (FancyMsg xs) = do putWord8 44

194+ put xs

194 get = do i <- getWord8

195 get = do i <- getWord8

195 case i of

196 case i of

196 0 -> fmap Msg get

197 0 -> fmap Msg get

@@ -262,6 +263,7 @@ instance Binary a => Binary (Err' a) where

262 41 -> fmap NoValidAlts get

263 41 -> fmap NoValidAlts get

263 42 -> fmap RunningElabScript get

264 42 -> fmap RunningElabScript get

264 43 -> fmap ElabScriptStaging get

265 43 -> fmap ElabScriptStaging get

266+ 44 -> fmap FancyMsg get

265 _ -> error "Corrupted binary data for Err'"

267 _ -> error "Corrupted binary data for Err'"

266----- Generated by 'derive'

268----- Generated by 'derive'

267

269

src/Idris/Core/DeepSeq.hs+1

@@ -157,6 +157,7 @@ instance NFData Err where

157 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

158 rnf (RunningElabScript x1) = rnf x1 `seq` ()

159 rnf (ElabScriptStaging x1) = rnf x1 `seq` ()

160+ rnf (FancyMsg x1) = rnf x1 `seq` ()

160

161

161instance NFData ErrorReportPart where

162instance NFData ErrorReportPart where

162 rnf (TextPart x1) = rnf x1 `seq` ()

163 rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+1

@@ -298,6 +298,7 @@ data Err' t

298 | ElabScriptStuck t

299 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

300 | ElabScriptStaging Name

301+ | FancyMsg [ErrorReportPart]

301 deriving (Eq, Functor, Data, Typeable)

302 deriving (Eq, Functor, Data, Typeable)

302

303

303type Err = Err' Term

304type Err = Err' Term

src/Idris/Delaborate.hs+2

@@ -507,6 +507,8 @@ pprintErr' i (ElabScriptStaging n) =

507 text "Can't run elaboration script because it contains pattern matching that has not yet been elaborated." <$>

508 text "Try lifting the script to a top-level definition." <$>

509 text "In particular, the problem is caused by:" <+> annName n

510+pprintErr' i (FancyMsg parts) =

511+ fillSep (map (showPart i) parts)

510

512

511showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

513showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

512showPart ist (TextPart str) = fillSep . map text . words $ str

514showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 123

43+ibcVersion = 124

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+14−5

@@ -196,7 +196,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

196 Nothing -> -- local variable, go for it

197 return True

198 TType _ -> return True

199− _ -> fail "Not a data type"

199+ _ -> typeNotSearchable ty

200

201 conReady :: [Term] -> Name -> ElabD Bool

202 conReady as n

@@ -282,8 +282,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

282 -- since that's part of the point...)

283 $ checkConstructor ist others

284 tryCons d locs tys (others ++ getFn d fn)

285− Nothing -> fail "Not a data type"

285+ Nothing -> typeNotSearchable t

286− _ -> fail "Not a data type"

286+ _ -> typeNotSearchable t

287

288 -- if there are local variables which have a function type, try

289 -- applying them too

@@ -326,11 +326,20 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

326 let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)

327 mapM_ (\ (_, h) -> do focus h

328 aty <- goal

329− psRec True d locs tys) newhs

329+ psRec True d locs tys) newhs

330 solve

331

332 isImp (PImp p _ _ _ _) = (True, p)

333− isImp arg = (False, priority arg)

333+ isImp arg = (False, priority arg)

334+

335+ typeNotSearchable ty =

336+ lift $ tfail $ FancyMsg $

337+ [TextPart "Attempted to find an element of type",

338+ TermPart ty,

339+ TextPart "using proof search, but proof search only works on datatypes with constructors."] ++

340+ case ty of

341+ (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

342+ _ -> []

334

343

335-- In interactive mode, only search for things if there is some

344-- In interactive mode, only search for things if there is some

336-- index to help pick a relevant constructor

345-- index to help pick a relevant constructor