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

git.iko.soy/Idris-dev

Merge pull request #2718 from david-christiansen/pruviloj

Pruviloj and reflection updates

commit6c4deb24c1c7a8feab4dfd868e54b2897ff2f3cb authorDavid Christiansen <david@davidchristiansen.dk> dateTue 13 Oct 2015, 13:43 (11 years ago) parent16ed52d 1e687f3

12 files changed+89−53

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+21−16 libs/pruviloj/Pruviloj/Core.idr+16 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+9−9 libs/pruviloj/Pruviloj/Injective.idr+4−4 libs/pruviloj/Pruviloj/Internals.idr+6−6 libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+11−11 src/Idris/Core/Binary.hs+3−1 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+2 src/Idris/IBC.hs+1−1 src/Idris/ProofSearch.hs+14−5

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

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

3737||| used for functions.

3838record FunArg where

3939 constructor MkFunArg

40− argName : TTName

41− argTy : Raw

40+ name : TTName

41+ type : Raw

4242 plicity : Plicity

4343 erasure : Erasure

4444

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

5454 TyConIndex FunArg

5555

5656||| A type declaration

57−data TyDecl : Type where

58− ||| A type declaration.

59− |||

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

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

62− ||| argument names.

63− |||

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

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

66− ||| @ ret the final return type

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

57+record TyDecl where

58+ constructor Declare

59+

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

61+ name : TTName

62+

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

64+ arguments : List FunArg

65+

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

67+ returnType : Raw

68+

6869

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

71+-- added at some point.

6972||| A single pattern-matching clause

7073data FunClause : Type where

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

7275

7376||| A reflected function definition.

74−data FunDefn : Type where

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

77+record FunDefn where

78+ constructor DefineFun

79+ name : TTName

80+ clauses : List FunClause

7681

7782

7883data CtorArg = CtorParameter FunArg | CtorField FunArg

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

8287 constructor MkDatatype

8388

8489 ||| The name of the type constructor

85− familyName : TTName

90+ name : TTName

8691

8792 ||| The arguments to the type constructor

8893 tyConArgs : List TyConArg

libs/pruviloj/Pruviloj/Core.idr+16

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

222222 both tm n1 n2

223223 try (unproduct (Var n1))

224224 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 =

8686 focus argH; fill ctorApp; solve

8787 solve

8888elabMethodTy 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)))

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

91− do let n = argName arg

92− let t = argTy arg

91+ do let n = name arg

92+ let t = type arg

9393 attack; forall n t

9494 mkIh info motiveName n t (result info)

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

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

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

154154 case arg of

155155 CtorParameter _ => return ()

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

157− unfocus (argName arg)

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

157+ unfocus (name arg)

158158

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

160160 scrutinee <- newHole "scrutinee" resTy

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

177177 focus scrutinee

178178 apply (mkApp (Var cn) $

179179 map (\x => case x of

180− CtorParameter param => Var (argName param)

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

180+ CtorParameter param => Var (name param)

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

182182 args)

183183 []

184184 solve)

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

195195 case x of

196196 CtorParameter _ => return List.Nil

197197 CtorField arg =>

198− do let n = argName arg

199− let t = argTy arg

198+ do let n = name arg

199+ let t = type arg

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

201201 if headsMatch argRes (result info) --recursive

202202 then return [ NormalArgument n

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

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

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

4444 `(() : Type)

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

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

47− {B=~(argTy a2)}

48− ~(Var (argName a1))

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

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

47+ {B=~(type a2)}

48+ ~(Var (name a1))

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

5050 (zip impls1 impls2))

5151

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

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

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

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

1111tyConArgName : TyConArg -> TTName

12−tyConArgName (TyConParameter a) = argName a

13−tyConArgName (TyConIndex a) = argName a

12+tyConArgName (TyConParameter a) = name a

13+tyConArgName (TyConIndex a) = name a

1414

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

1616setTyConArgName : TyConArg -> TTName -> TyConArg

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

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

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

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

1919

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

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

2222updateTyConArgTy f (TyConParameter a) =

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

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

2424updateTyConArgTy f (TyConIndex a) =

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

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

2626

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

2828unApply tm = unApply' tm []

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

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

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

2424getParams info = mapMaybe param (args info)

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

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

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

2727 param _ = Nothing

2828

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

3030getIndices info = mapMaybe index (args info)

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

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

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

3333 index _ = Nothing

3434

3535||| Rename a bound variable across a telescope

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

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

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

7777 if n == paramN

78− then return (argName a)

78+ then return (name a)

7979 else findParam paramN args tcArgs

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

8181 findParam paramN args tcArgs

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

8989 TyConInfo -> Elab (List CtorArg, Raw)

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

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

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

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

9393 let a' = record {

94− argName = n'

95− , argTy = alphaRaw subst (argTy a)

94+ name = n'

95+ , type = alphaRaw subst (type a)

9696 } a

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

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

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

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

100100 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)

102102 let a' = record {

103− argName = n'

104− , argTy = alphaRaw subst (argTy a)

103+ name = n'

104+ , type = alphaRaw subst (type a)

105105 } a

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

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

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

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

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

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

190190 put e

191191 put (ElabScriptStaging n) = do putWord8 43

192192 put n

193−

193+ put (FancyMsg xs) = do putWord8 44

194+ put xs

194195 get = do i <- getWord8

195196 case i of

196197 0 -> fmap Msg get

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

262263 41 -> fmap NoValidAlts get

263264 42 -> fmap RunningElabScript get

264265 43 -> fmap ElabScriptStaging get

266+ 44 -> fmap FancyMsg get

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

266268----- Generated by 'derive'

267269

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

160161

161162instance NFData ErrorReportPart where

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

src/Idris/Core/TT.hs+1

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

298298 | ElabScriptStuck t

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

300300 | ElabScriptStaging Name

301+ | FancyMsg [ErrorReportPart]

301302 deriving (Eq, Functor, Data, Typeable)

302303

303304type Err = Err' Term

src/Idris/Delaborate.hs+2

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

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

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

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

510+pprintErr' i (FancyMsg parts) =

511+ fillSep (map (showPart i) parts)

510512

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

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

src/Idris/IBC.hs+1−1

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 123

43+ibcVersion = 124

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+14−5

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

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

197197 return True

198198 TType _ -> return True

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

199+ _ -> typeNotSearchable ty

200200

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

202202 conReady as n

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

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

283283 $ checkConstructor ist others

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

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

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

285+ Nothing -> typeNotSearchable t

286+ _ -> typeNotSearchable t

287287

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

289289 -- applying them too

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

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

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

328328 aty <- goal

329− psRec True d locs tys) newhs

329+ psRec True d locs tys) newhs

330330 solve

331331

332332 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+ _ -> []

334343

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

336345-- index to help pick a relevant constructor