idris 0.9.14 → 0.9.14.1
raw patch · 50 files changed
+3830/−2805 lines, 50 files
Files
- idris.cabal +23/−1
- libs/base/Data/SortedMap.idr +1/−1
- libs/base/Data/Vect/Quantifiers.idr +4/−1
- libs/base/Language/Reflection.idr +358/−87
- libs/base/Language/Reflection/Errors.idr +0/−7
- libs/base/Language/Reflection/Utils.idr +55/−34
- libs/effects/Effect/File.idr +9/−5
- libs/effects/Makefile +11/−4
- libs/prelude/Builtins.idr +8/−4
- libs/prelude/Prelude/Applicative.idr +4/−0
- libs/prelude/Prelude/Functor.idr +5/−0
- libs/prelude/Prelude/Monad.idr +4/−0
- libs/prelude/Prelude/Traversable.idr +6/−0
- src/Idris/AbsSyntaxTree.hs +22/−7
- src/Idris/CaseSplit.hs +4/−2
- src/Idris/Core/TT.hs +6/−0
- src/Idris/DeepSeq.hs +8/−0
- src/Idris/Elab/Class.hs +226/−0
- src/Idris/Elab/Clause.hs +877/−0
- src/Idris/Elab/Data.hs +489/−0
- src/Idris/Elab/Instance.hs +260/−0
- src/Idris/Elab/Provider.hs +117/−0
- src/Idris/Elab/Record.hs +242/−0
- src/Idris/Elab/Type.hs +200/−0
- src/Idris/Elab/Utils.hs +151/−0
- src/Idris/Elab/Value.hs +88/−0
- src/Idris/ElabDecls.hs +260/−2495
- src/Idris/ElabTerm.hs +91/−39
- src/Idris/Interactive.hs +4/−2
- src/Idris/ParseExpr.hs +6/−2
- src/Idris/Prover.hs +5/−2
- src/Idris/REPL.hs +19/−14
- src/Idris/REPLParser.hs +94/−94
- src/Idris/TypeSearch.hs +2/−2
- test/quasiquote004/Quasiquote004.idr +51/−0
- test/quasiquote004/expected +2/−0
- test/quasiquote004/run +3/−0
- test/reg048/expected +0/−0
- test/reg048/reg048.idr +24/−0
- test/reg048/run +4/−0
- test/reg049/expected +2/−0
- test/reg049/reg049.idr +5/−0
- test/reg049/run +3/−0
- test/reg050/badbangop.idr +15/−0
- test/reg050/baddoublebang.idr +7/−0
- test/reg050/expected +27/−0
- test/reg050/run +5/−0
- test/reg050/working.idr +21/−0
- test/totality003/totality003.idr +1/−1
- test/totality003/totality003a.idr +1/−1
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.14+Version: 0.9.14.1 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -241,6 +241,15 @@ test/reg047/run test/reg047/*.idr test/reg047/expected+ test/reg048/run+ test/reg048/*.idr+ test/reg048/expected+ test/reg049/run+ test/reg049/*.idr+ test/reg049/expected+ test/reg050/run+ test/reg050/*.idr+ test/reg050/expected test/basic001/run test/basic001/*.idr@@ -425,6 +434,9 @@ test/quasiquote003/run test/quasiquote003/*.idr test/quasiquote003/expected+ test/quasiquote004/run+ test/quasiquote004/*.idr+ test/quasiquote004/expected test/records001/run@@ -543,6 +555,16 @@ , Idris.Core.TT , Idris.Core.Typecheck , Idris.Core.Unify++ , Idris.Elab.Utils+ , Idris.Elab.Type+ , Idris.Elab.Clause+ , Idris.Elab.Data+ , Idris.Elab.Record+ , Idris.Elab.Class+ , Idris.Elab.Instance+ , Idris.Elab.Provider+ , Idris.Elab.Value , Idris.AbsSyntax , Idris.AbsSyntaxTree
libs/base/Data/SortedMap.idr view
@@ -114,7 +114,7 @@ else case treeInsert' k v t3 of Left t3' => Left (Branch3 t1 k1 t2 k2 t3')- Right (a, b, c) => Right (Branch2 t1 k2 t2, k2, Branch2 a b c)+ Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c) treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v) treeInsert k v t =
libs/base/Data/Vect/Quantifiers.idr view
@@ -5,8 +5,11 @@ There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs) anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_-anyNilAbsurd (Here _) impossible +anyNilAbsurd (Here _) impossible anyNilAbsurd (There _) impossible++instance Uninhabited (Any p Nil) where+ uninhabited = anyNilAbsurd anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b anyElim _ f (Here p) = f p
libs/base/Language/Reflection.idr view
@@ -2,32 +2,44 @@ %access public -data TTName = UN String- -- ^ User-provided name- | NS TTName (List String)- -- ^ Root, namespaces- | MN Int String- -- ^ Machine chosen names- | NErased- -- ^ Name of somethng which is never used in scope+data TTName =+ ||| A user-provided name+ UN String |+ ||| A name in some namespace.+ |||+ ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])` represents the name `A.B.foo`+ NS TTName (List String) |+ ||| Machine-chosen names+ MN Int String |+ ||| Name of something which is never used in scope+ NErased %name TTName n, n' implicit userSuppliedName : String -> TTName userSuppliedName = UN -data TTUExp = UVar Int- -- ^ universe variable- | UVal Int- -- ^ explicit universe variable+data TTUExp =+ ||| Universe variable+ UVar Int |+ ||| Explicit universe level+ UVal Int %name TTUExp uexp +data NativeTy = IT8 | IT16 | IT32 | IT64++data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar+ | ITVec NativeTy Int++data ArithTy = ATInt Language.Reflection.IntTy | ATFloat+ ||| Primitive constants data Const = I Int | BI Integer | Fl Float | Ch Char | Str String- | IType | BIType | FlType | ChType | StrType | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64- | B8Type | B16Type | B32Type | B64Type- | PtrType | VoidType | Forgot+ | B8V Bits8x16 | B16V Bits16x8+ | B32V Bits32x4 | B64V Bits64x2+ | AType ArithTy | StrType+ | PtrType | ManagedPtrType | BufferType | VoidType | Forgot %name Const c, c' @@ -125,81 +137,340 @@ ||| Reflection of the well typed core language-data TT = P NameType TTName TT- -- ^ named binders- | V Int- -- ^ variables- | Bind TTName (Binder TT) TT- -- ^ type annotated named bindings- | App TT TT- -- ^ (named) application of a function to a value- | TConst Const- -- ^ constants- | Proj TT Int- -- ^ argument projection; runtime only- | Erased- -- ^ erased terms- | Impossible- -- ^ impossible terms- | TType TTUExp- -- ^ types-+data TT =+ ||| A reference to some name (P for Parameter)+ P NameType TTName TT |+ ||| de Bruijn variables+ V Int |+ ||| Bind a variable+ Bind TTName (Binder TT) TT |+ ||| Apply one term to another+ App TT TT |+ ||| Embed a constant+ TConst Const |+ ||| Argument projection; runtime only+ Proj TT Int |+ ||| Erased terms+ Erased |+ ||| Impossible terms+ Impossible |+ ||| The type of types along (with universe constraints)+ TType TTUExp %name TT tm, tm' ||| Raw terms without types-data Raw = Var TTName- | RBind TTName (Binder Raw) Raw- | RApp Raw Raw- | RType- | RForce Raw- | RConstant Const-+data Raw =+ ||| Variables, global or local+ Var TTName |+ ||| Bind a variable+ RBind TTName (Binder Raw) Raw |+ ||| Application+ RApp Raw Raw |+ ||| The type of types+ RType |+ RForce Raw |+ ||| Embed a constant+ RConstant Const %name Raw tm, tm' -data Tactic = Try Tactic Tactic- -- ^ try the first tactic and resort to the second one on failure- | GoalType String Tactic- -- ^ only run if the goal has the right type- | Refine TTName- -- ^ resolve function name, find matching arguments in the- -- context and compute the proof target- | Seq Tactic Tactic- -- ^ apply both tactics in sequence- | Trivial- -- ^ intelligently construct the proof target from the context- | Search Int- -- ^ build a proof by applying contructors up to a maximum depth - | Instance- -- ^ resolve a type class - | Solve- -- ^ infer the proof target from the context- | Intros- -- ^ introduce all variables into the context- | Intro TTName- -- ^ introduce a named variable into the context, use the- -- first one if the given name is not found- | ApplyTactic TT- -- ^ invoke the reflected rep. of another tactic- | Reflect TT- -- ^ turn a value into its reflected representation- | ByReflection TT- -- ^ use a %reflection function- | Fill Raw- -- ^ turn a raw value back into a term- | Exact TT- -- ^ use the given value to conclude the proof- | Focus TTName- -- ^ focus a named hole- | Rewrite TT- -- ^ rewrite using the reflected rep. of a equality proof- | Induction TT- -- ^ do induction on the particular expression- | Case TT- -- ^ do case analysis on particular expression- | LetTac TTName TT- -- ^ name a reflected term- | LetTacTy TTName TT TT- -- ^ name a reflected term and type it- | Compute- -- ^ normalise the context+||| Error reports are a list of report parts+data ErrorReportPart =+ ||| A human-readable string+ TextPart String |+ ||| An Idris name (to be semantically coloured)+ NamePart TTName |+ ||| An Idris term, to be pretty printed+ TermPart TT |+ ||| An indented sub-report, to provide more details+ SubReport (List ErrorReportPart)+%name ErrorReportPart part, p++||| A representation of Idris's tactics that can be returned from custom+||| tactic implementations. Generate these using `applyTactic`.+data Tactic =+ ||| Try the first tactic and resort to the second one on failure+ Try Tactic Tactic |+ ||| Only run if the goal has the right type+ GoalType String Tactic |+ ||| Resolve function name, find matching arguments in the+ ||| context and compute the proof target+ Refine TTName |+ ||| Apply both tactics in sequence+ Seq Tactic Tactic |+ ||| Intelligently construct the proof target from the context+ Trivial |+ ||| Build a proof by applying contructors up to a maximum depth+ Search Int |+ ||| Resolve a type class+ Instance |+ ||| Infer the proof target from the context+ Solve |+ ||| introduce all variables into the context+ Intros |+ ||| Introduce a named variable into the context, use the+ ||| first one if the given name is not found+ Intro TTName |+ ||| Invoke the reflected rep. of another tactic+ ApplyTactic TT |+ ||| Turn a value into its reflected representation+ Reflect TT |+ ||| Use a `%reflection` function+ ByReflection TT |+ ||| Turn a raw value back into a term+ Fill Raw |+ ||| Use the given value to conclude the proof+ Exact TT |+ ||| Focus on a particular hole+ Focus TTName |+ ||| Rewrite with an equality+ Rewrite TT |+ ||| Perform induction on a particular expression+ Induction TT |+ ||| Perform case analysis on a particular expression+ Case TT |+ ||| Name a reflected term+ LetTac TTName TT |+ ||| Name a reflected term and type it+ LetTacTy TTName TT TT |+ ||| Normalise the goal+ Compute |+ ||| Do nothing+ Skip |+ ||| Fail with an error message+ Fail (List ErrorReportPart) %name Tactic tac, tac'+++||| Things with a canonical representation in the TT datatype.+|||+||| This type class is intended to be used during proof automation and the+||| construction of custom tactics.+|||+||| @ a the type to be quoted+class Quotable a where+ ||| A representation of the type `a`.+ |||+ ||| This is to enable quoting polymorphic datatypes+ quotedTy : TT++ ||| Quote a particular element of `a`.+ |||+ ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```+ quote : a -> TT++instance Quotable Nat where+ quotedTy = `(Nat)++ quote Z = `(Z)+ quote (S k) = `(S ~(quote k))++instance Quotable Int where+ quotedTy = `(Int)+ quote x = TConst (I x)++instance Quotable Float where+ quotedTy = `(Float)+ quote x = TConst (Fl x)++instance Quotable Char where+ quotedTy = `(Char)+ quote x = TConst (Ch x)++instance Quotable Bits8 where+ quotedTy = `(Bits8)+ quote x = TConst (B8 x)++instance Quotable Bits16 where+ quotedTy = `(Bits16)+ quote x = TConst (B16 x)++instance Quotable Bits32 where+ quotedTy = `(Bits32)+ quote x = TConst (B32 x)++instance Quotable Bits64 where+ quotedTy = `(Bits64)+ quote x = TConst (B64 x)++instance Quotable Integer where+ quotedTy = `(Integer)+ quote x = TConst (BI x)++instance Quotable Bits8x16 where+ quotedTy = `(Bits8x16)+ quote x = TConst (B8V x)++instance Quotable Bits16x8 where+ quotedTy = `(Bits16x8)+ quote x = TConst (B16V x)++instance Quotable Bits32x4 where+ quotedTy = `(Bits32x4)+ quote x = TConst (B32V x)++instance Quotable Bits64x2 where+ quotedTy = `(Bits64x2)+ quote x = TConst (B64V x)++instance Quotable String where+ quotedTy = `(String)+ quote x = TConst (Str x)++instance Quotable NameType where+ quotedTy = `(NameType)+ quote Bound = `(Bound)+ quote Ref = `(Ref)+ quote (DCon x y) = `(DCon ~(quote x) ~(quote y))+ quote (TCon x y) = `(TCon ~(quote x) ~(quote y))++instance Quotable a => Quotable (List a) where+ quotedTy = `(List ~(quotedTy {a=a}))+ quote [] = `(List.Nil {a=~quotedTy})+ quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))++instance Quotable TTName where+ quotedTy = `(TTName)+ quote (UN x) = `(UN ~(quote x))+ quote (NS n xs) = `(NS ~(quote n) ~(quote xs))+ quote (MN x y) = `(MN ~(quote x) ~(quote y))+ quote NErased = `(NErased)++instance Quotable NativeTy where+ quotedTy = `(NativeTy)+ quote IT8 = `(Reflection.IT8)+ quote IT16 = `(Reflection.IT16)+ quote IT32 = `(Reflection.IT32)+ quote IT64 = `(Reflection.IT64)++instance Quotable Reflection.IntTy where+ quotedTy = `(Reflection.IntTy)+ quote (ITFixed x) = `(ITFixed ~(quote x))+ quote ITNative = `(Reflection.ITNative)+ quote ITBig = `(ITBig)+ quote ITChar = `(Reflection.ITChar)+ quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))++instance Quotable ArithTy where+ quotedTy = `(ArithTy)+ quote (ATInt x) = `(ATInt ~(quote x))+ quote ATFloat = `(ATFloat)++instance Quotable Const where+ quotedTy = `(Const)+ quote (I x) = `(I ~(quote x))+ quote (BI x) = `(BI ~(quote x))+ quote (Fl x) = `(Fl ~(quote x))+ quote (Ch x) = `(Ch ~(quote x))+ quote (Str x) = `(Str ~(quote x))+ quote (B8 x) = `(B8 ~(quote x))+ quote (B16 x) = `(B16 ~(quote x))+ quote (B32 x) = `(B32 ~(quote x))+ quote (B64 x) = `(B64 ~(quote x))+ quote (B8V xs) = `(B8V ~(quote xs))+ quote (B16V xs) = `(B16V ~(quote xs))+ quote (B32V xs) = `(B32V ~(quote xs))+ quote (B64V xs) = `(B64V ~(quote xs))+ quote (AType x) = `(AType ~(quote x))+ quote StrType = `(StrType)+ quote PtrType = `(PtrType)+ quote ManagedPtrType = `(ManagedPtrType)+ quote BufferType = `(BufferType)+ quote VoidType = `(VoidType)+ quote Forgot = `(Forgot)+++instance Quotable TTUExp where+ quotedTy = `(TTUExp)+ quote (UVar x) = `(UVar ~(quote x))+ quote (UVal x) = `(UVal ~(quote x))++mutual+ instance Quotable TT where+ quotedTy = `(TT)+ quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))+ quote (V x) = `(V ~(quote x))+ quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))+ quote (App f x) = `(App ~(quote f) ~(quote x))+ quote (TConst c) = `(TConst ~(quote c))+ quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))+ quote Erased = `(Erased)+ quote Impossible = `(Impossible)+ quote (TType uexp) = `(TType ~(quote uexp))++ instance Quotable (Binder TT) where+ quotedTy = `(Binder TT)+ quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))+ quote (Pi x) = `(Pi {a=TT} ~(assert_total (quote x)))+ quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))+ ~(assert_total (quote y)))+ quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))+ ~(assert_total (quote y)))+ quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))+ quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))+ quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))+ ~(assert_total (quote y)))+ quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))+ quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))+++instance Quotable ErrorReportPart where+ quotedTy = `(ErrorReportPart)+ quote (TextPart x) = `(TextPart ~(quote x))+ quote (NamePart n) = `(NamePart ~(quote n))+ quote (TermPart tm) = `(TermPart ~(quote tm))+ quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))++mutual+ quoteRaw : Raw -> TT+ quoteRaw (Var n) = `(Var ~(quote n))+ quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))+ quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))+ quoteRaw RType = `(RType)+ quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))+ quoteRaw (RConstant c) = `(RConstant ~(quote c))++ quoteRawBinder : Binder Raw -> TT+ quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))+ quoteRawBinder (Pi x) = `(Pi {a=Raw} ~(quoteRaw x))+ quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))+ quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))+ quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))+ quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))+ quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))+ quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))+ quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))++instance Quotable Raw where+ quotedTy = `(Raw)+ quote = quoteRaw++instance Quotable (Binder Raw) where+ quotedTy = `(Binder Raw)+ quote = quoteRawBinder++instance Quotable Tactic where+ quotedTy = `(Tactic)+ quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))+ quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))+ quote (Refine n) = `(Refine ~(quote n))+ quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))+ quote Trivial = `(Trivial)+ quote (Search x) = `(Search ~(quote x))+ quote Instance = `(Instance)+ quote Solve = `(Solve)+ quote Intros = `(Intros)+ quote (Intro n) = `(Intro ~(quote n))+ quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))+ quote (Reflect tm) = `(Reflect ~(quote tm))+ quote (ByReflection tm) = `(ByReflection ~(quote tm))+ quote (Fill tm) = `(Fill ~(quote tm))+ quote (Exact tm) = `(Exact ~(quote tm))+ quote (Focus n) = `(Focus ~(quote n))+ quote (Rewrite tm) = `(Rewrite ~(quote tm))+ quote (Induction tm) = `(Induction ~(quote tm))+ quote (Case tm) = `(Case ~(quote tm))+ quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))+ quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))+ quote Compute = `(Compute)+ quote Skip = `(Skip)+ quote (Fail xs) = `(Fail ~(quote xs))
libs/base/Language/Reflection/Errors.idr view
@@ -40,13 +40,6 @@ %name Err err, e -||| Error reports are a list of report parts-data ErrorReportPart = TextPart String- | NamePart TTName- | TermPart TT- | SubReport (List ErrorReportPart)-%name ErrorReportPart part, p- -- Error reports become functions in List (String, TT) -> Err -> ErrorReport ErrorHandler : Type ErrorHandler = Err -> Maybe (List ErrorReportPart)
libs/base/Language/Reflection/Utils.idr view
@@ -3,6 +3,8 @@ import Language.Reflection import Language.Reflection.Errors +%default total+ -------------------------------------------------------- -- Tactic construction conveniences --------------------------------------------------------@@ -83,46 +85,65 @@ show (Fl f) = "(Fl " ++ show f ++ ")" show (Ch c) = "(Ch " ++ show c ++ ")" show (Str str) = "(Str " ++ show str ++ ")"- show IType = "IType"- show BIType = "BIType"- show FlType = "FlType"- show ChType = "ChType"- show StrType = "StrType" show (B8 b) = "(B8 ...)" show (B16 b) = "(B16 ...)" show (B32 b) = "(B32 ...)" show (B64 b) = "(B64 ...)"- show B8Type = "B8Type"- show B16Type = "B16Type"- show B32Type = "B32Type"- show B64Type = "B64Type"- show PtrType = "PtrType"- show VoidType = "VoidType"- show Forgot = "Forgot"+ show (B8V xs) = "(B8V ...)"+ show (B16V xs) = "(B16V ...)"+ show (B32V xs) = "(B32V ...)"+ show (B64V xs) = "(B64V ...)"+ show (AType x) = "(AType ...)"+ show StrType = "StrType"+ show PtrType = "PtrType"+ show ManagedPtrType = "ManagedPtrType"+ show BufferType = "BufferType"+ show VoidType = "VoidType"+ show Forgot = "Forgot" +instance Eq NativeTy where+ IT8 == IT8 = True+ IT16 == IT16 = True+ IT32 == IT32 = True+ IT64 == IT64 = True+ _ == _ = False++instance Eq Reflection.IntTy where+ (ITFixed x) == (ITFixed y) = x == y+ ITNative == ITNative = True+ ITBig == ITBig = True+ ITChar == ITChar = True+ (ITVec x i) == (ITVec y j) = x == y && i == j+ _ == _ = False++instance Eq ArithTy where+ (ATInt x) == (ATInt y) = x == y+ ATFloat == ATFloat = True+ _ == _ = False+ instance Eq Const where- (I i) == (I i') = i == i'- (BI n) == (BI n') = n == n'- (Fl f) == (Fl f') = f == f'- (Ch c) == (Ch c') = c == c'- (Str str) == (Str str') = str == str'- IType == IType = True- BIType == BIType = True- FlType == FlType = True- ChType == ChType = True- StrType == StrType = True- (B8 b) == (B8 b') = False -- FIXME: b == b'- (B16 b) == (B16 b') = False -- FIXME: b == b'- (B32 b) == (B32 b') = False -- FIXME: b == b'- (B64 b) == (B64 b') = False -- FIXME: b == b'- B8Type == B8Type = True- B16Type == B16Type = True- B32Type == B32Type = True- B64Type == B64Type = True- PtrType == PtrType = True- VoidType == VoidType = True- Forgot == Forgot = True- x == y = False+ (I x) == (I y) = x == y+ (BI x) == (BI y) = x == y+ (Fl x) == (Fl y) = x == y+ (Ch x) == (Ch y) = x == y+ (Str x) == (Str y) = x == y+ (B8 x) == (B8 y) = x == y+ (B16 x) == (B16 y) = x == y+ (B32 x) == (B32 y) = x == y+ (B64 x) == (B64 y) = x == y+ (B8V xs) == (B8V ys) = False -- TODO+ (B16V xs) == (B16V ys) = False -- TODO+ (B32V xs) == (B32V ys) = False -- TODO+ (B64V xs) == (B64V ys) = False -- TODO+ (AType x) == (AType y) = x == y+ StrType == StrType = True+ PtrType == PtrType = True+ ManagedPtrType == ManagedPtrType = True+ BufferType == BufferType = True+ VoidType == VoidType = True+ Forgot == Forgot = True+ _ == _ = False+ instance Show NameType where show Bound = "Bound"
libs/effects/Effect/File.idr view
@@ -60,10 +60,10 @@ ||| Only files that are open for reading can be read. ReadLine : {OpenFile Read} FileIO String - ||| Write a line to a file.+ ||| Write a string to a file. ||| ||| Only file that are open for writing can be written to.- WriteLine : String -> {OpenFile Write} FileIO ()+ WriteString : String -> {OpenFile Write} FileIO () ||| End of file? ||| @@ -82,8 +82,8 @@ k () () handle (FH h) ReadLine k = do str <- fread h k str (FH h)- handle (FH h) (WriteLine str) k = do fwrite h str- k () (FH h)+ handle (FH h) (WriteString str) k = do fwrite h str+ k () (FH h) handle (FH h) EOF k = do e <- feof h k e (FH h) @@ -117,9 +117,13 @@ readLine : { [FILE_IO (OpenFile Read)] } Eff String readLine = call $ ReadLine +||| Write a string to a file.+writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()+writeString str = call $ WriteString str+ ||| Write a line to a file. writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()-writeLine str = call $ WriteLine str+writeLine str = call $ WriteString (str ++ "\n") ||| End of file? eof : { [FILE_IO (OpenFile Read)] } Eff Bool
libs/effects/Makefile view
@@ -1,14 +1,21 @@ IDRIS := idris+PKG := effects build:- $(IDRIS) --build effects.ipkg+ $(IDRIS) --build ${PKG}.ipkg clean:- $(IDRIS) --clean effects.ipkg+ $(IDRIS) --clean ${PKG}.ipkg install:- $(IDRIS) --install effects.ipkg+ $(IDRIS) --install ${PKG}.ipkg rebuild: clean build -.PHONY: build clean install rebuild+doc:+ $(IDRIS) --mkdoc ${PKG}.ipkg++doc_clean:+ rm -rf ${PKG}_doc++.PHONY: build clean install rebuild doc doc_clean
libs/prelude/Builtins.idr view
@@ -15,12 +15,16 @@ ||| For 'symbol syntax. 'foo becomes Symbol_ "foo" data Symbol_ : String -> Type where --- Eq_ : a -> a -> Type--- Eq_ x y = (=) _ _ x y- + infix 5 ~=~ -(~=~) : a -> b -> Type+||| Explicit heterogeneous ("John Major") equality. Use this when Idris+||| incorrectly chooses homogeneous equality for `(=)`.+||| @ a the type of the left side+||| @ b the type of the right side+||| @ x the left side+||| @ y the right side+(~=~) : (x : a) -> (y : b) -> Type (~=~) x y = (=) _ _ x y -- ------------------------------------------------------ [ For rewrite tactic ]
libs/prelude/Prelude/Applicative.idr view
@@ -13,6 +13,10 @@ pure : a -> f a (<$>) : f (a -> b) -> f a -> f b +instance Applicative id where+ pure a = a+ f <$> a = f a+ infixl 2 <$ (<$) : Applicative f => f a -> f b -> f a a <$ b = map const a <$> b
libs/prelude/Prelude/Functor.idr view
@@ -1,5 +1,7 @@ module Prelude.Functor +import Prelude.Basics+ ||| Functors ||| @ f the action of the functor on objects class Functor (f : Type -> Type) where@@ -7,3 +9,6 @@ ||| @ f the functor ||| @ m the morphism map : (m : a -> b) -> f a -> f b++instance Functor id where+ map f a = f a
libs/prelude/Prelude/Monad.idr view
@@ -5,6 +5,7 @@ import Builtins import Prelude.List import Prelude.Applicative+import Prelude.Basics %access public @@ -12,6 +13,9 @@ class Applicative m => Monad (m : Type -> Type) where (>>=) : m a -> (a -> m b) -> m b++instance Monad id where+ a >>= f = f a ||| Also called `join` or mu flatten : Monad m => m (m a) -> m a
libs/prelude/Prelude/Traversable.idr view
@@ -9,8 +9,14 @@ sequence_ : (Foldable t, Applicative f) => t (f a) -> f () sequence_ = foldr ($>) (pure ()) +for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()+for_ = flip traverse_+ class (Functor t, Foldable t) => Traversable (t : Type -> Type) where traverse : Applicative f => (a -> f b) -> t a -> f (t b) sequence : (Traversable t, Applicative f) => t (f a) -> f (t a) sequence = traverse id++for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)+for = flip traverse
src/Idris/AbsSyntaxTree.hs view
@@ -35,15 +35,24 @@ import Text.PrettyPrint.Annotated.Leijen +data ElabWhat = ETypes | EDefns | EAll+ deriving (Show, Eq)+ -- Data to pass to recursively called elaborators; e.g. for where blocks, -- paramaterised declarations, etc. +-- rec_elabDecl is used to pass the top level elaborator into other elaborators,+-- so that we can have mutually recursive elaborators in separate modules without+-- having to much about with cyclic modules. data ElabInfo = EInfo { params :: [(Name, PTerm)], inblock :: Ctxt [Name], -- names in the block, and their params liftname :: Name -> Name,- namespace :: Maybe [String] }+ namespace :: Maybe [String], + rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> + Idris () } -toplevel = EInfo [] emptyContext id Nothing+toplevel :: ElabInfo+toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented") eInfoNames :: ElabInfo -> [Name] eInfoNames info = map fst (params info) ++ M.keys (inblock info)@@ -194,6 +203,10 @@ idris_callswho :: Maybe (M.Map Name [Name]) } +-- Required for parsers library, and therefore trifecta+instance Show IState where+ show = const "{internal state}"+ data SizeChange = Smaller | Same | Bigger | Unknown deriving (Show, Eq) {-!@@ -763,6 +776,8 @@ | TEval t | TDocStr (Either Name Const) | TSearch t+ | Skip+ | TFail [ErrorReportPart] | Qed | Abandon deriving (Show, Eq, Functor) {-!@@ -792,6 +807,8 @@ size (Fill t) = 1 + size t size Qed = 1 size Abandon = 1+ size Skip = 1+ size (TFail ts) = 1 + size ts type PTactic = PTactic' PTerm @@ -1070,13 +1087,11 @@ "To use such a proof, pattern-match on it, and the two equal things will " ++ "then need to be the _same_ pattern." ++ "\n\n" ++- "**Note**: Idris's equality type is _heterogeneous_, which means that it " +++ "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++ "is possible to state equalities between values of potentially different " ++- "types. This is sometimes referred to in the literature as \"John Major\" " ++- "equality." +++ "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++ "\n\n" ++- "Thus, if Idris can't infer the type of one side of the equality, then " ++- "you may need to annotate it. See the function `the`."+ "You may need to use `(~=~)` to explicitly request heterogeneous equality." eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)] (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
src/Idris/CaseSplit.hs view
@@ -16,6 +16,8 @@ import Idris.Error import Idris.Output +import Idris.Elab.Value+ import Idris.Core.TT import Idris.Core.Typecheck import Idris.Core.Evaluate@@ -55,7 +57,7 @@ = do ist <- getIState -- Make sure all the names in the term are accessible mapM_ (\n -> setAccessibility n Public) (allNamesIn t')- (tm, ty, pats) <- elabValBind toplevel ELHS True (addImplPat ist t')+ (tm, ty, pats) <- elabValBind recinfo ELHS True (addImplPat ist t') -- ASSUMPTION: tm is in normal form after elabValBind, so we don't -- need to do anything special to find out what family each argument -- is in@@ -201,7 +203,7 @@ -- tidyVar t = t elabNewPat :: PTerm -> Idris (Maybe PTerm)-elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel ELHS t+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t i <- getIState return (Just (delab i tm))) (\e -> do i <- getIState
src/Idris/Core/TT.hs view
@@ -158,6 +158,12 @@ deriving instance NFData Err !-} +instance Sized ErrorReportPart where+ size (TextPart msg) = 1 + length msg+ size (TermPart t) = 1 + size t+ size (NamePart n) = 1 + size n+ size (SubReport rs) = 1 + size rs+ instance Sized Err where size (Msg msg) = length msg size (InternalMsg msg) = length msg
src/Idris/DeepSeq.hs view
@@ -260,6 +260,14 @@ rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf Qed = () rnf Abandon = ()+ rnf Skip = ()+ rnf (TFail x1) = rnf x1 `seq` ()++instance NFData ErrorReportPart where+ rnf (TermPart x1) = rnf x1 `seq` ()+ rnf (TextPart x1) = rnf x1 `seq` ()+ rnf (NamePart x1) = rnf x1 `seq` ()+ rnf (SubReport x1) = rnf x1 `seq` () instance (NFData t) => NFData (PDo' t) where rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
+ src/Idris/Elab/Class.hs view
@@ -0,0 +1,226 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Class(elabClass) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Data+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++data MArgTy = IA | EA | CA deriving Show++elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->+ FC -> [PTerm] ->+ Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()+elabClass info syn_in doc fc constraints tn ps pDocs ds+ = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)+ let tty = pibind ps PType+ let constraint = PApp fc (PRef fc tn)+ (map (pexp . PRef fc) (map fst ps))++ let syn = syn_in { using = addToUsing (using syn_in) ps }++ -- build data declaration+ let mdecls = filter tydecl ds -- method declarations+ let idecls = filter instdecl ds -- default superclass instance declarations+ mapM_ checkDefaultSuperclassInstance idecls+ let mnames = map getMName mdecls+ logLvl 2 $ "Building methods " ++ show mnames+ ims <- mapM (tdecl mnames) mdecls+ defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)+ (filter clause ds)+ let (methods, imethods)+ = unzip (map (\ ( x,y,z) -> (x, y)) ims)+ let defaults = map (\ (x, (y, z)) -> (x,y)) defs+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])+ -- build instance constructor type+ -- decorate names of functions to ensure they can't be referred+ -- to elsewhere in the class declaration+ let cty = impbind ps $ conbind constraints+ $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)+ constraint+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]+ let ddecl = PDatadecl tn tty cons+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl+ -- for each constraint, build a top level function to chase it+ logLvl 5 $ "Building functions"+-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps+-- ++ using syn }+ fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints+ mapM_ (rec_elabDecl info EAll info) (concat fns)+ -- for each method, build a top level function+ fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods+ mapM_ (rec_elabDecl info EAll info) (concat fns)+ -- add the default definitions+ mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))+ addIBC (IBCClass tn)+ where+ nodoc (n, (_, o, t)) = (n, (o, t))+ pibind [] x = x+ pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)++ mdec (UN n) = SN (MethodN (UN n))+ mdec (NS x n) = NS (mdec x) n+ mdec x = x++ -- TODO: probably should normalise+ checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)+ = do when (not $ null cs) . tclift+ $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))+ i <- getIState+ let t = PApp fc (PRef fc n) (map pexp ps)+ let isConstrained = any (== t) constraints+ when (not isConstrained) . tclift+ $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))+ return ()++ impbind [] x = x+ impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)+ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)+ conbind [] x = x++ getMName (PTy _ _ _ _ _ n _) = nsroot n+ tdecl allmeths (PTy doc _ syn _ o n t)+ = do t' <- implicit' info syn allmeths n t+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'+ return ( (n, (toExp (map fst ps) Exp t')),+ (n, (doc, o, (toExp (map fst ps) Imp t'))),+ (n, (syn, o, t) ) )+ tdecl _ _ = ifail "Not allowed in a class declaration"++ -- Create default definitions+ defdecl mtys c d@(PClauses fc opts n cs) =+ case lookup n mtys of+ Just (syn, o, ty) -> do let ty' = insertConstraint c ty+ let ds = map (decorateid defaultdec)+ [PTy emptyDocstring [] syn fc [] n ty',+ PClauses fc (o ++ opts) n cs]+ iLOG (show ds)+ return (n, ((defaultdec n, ds!!1), ds))+ _ -> ifail $ show n ++ " is not a method"+ defdecl _ _ _ = ifail "Can't happen (defdecl)"++ defaultdec (UN n) = sUN ("default#" ++ str n)+ defaultdec (NS n ns) = NS (defaultdec n) ns++ tydecl (PTy _ _ _ _ _ _ _) = True+ tydecl _ = False+ instdecl (PInstance _ _ _ _ _ _ _ _) = True+ instdecl _ = False+ clause (PClauses _ _ _ _) = True+ clause _ = False++ -- Generate a function for chasing a dictionary constraint+ cfun cn c syn all con+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)+ -- SN (ParentN cn (show con))+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)+ let lhs = PApp fc (PRef fc cfn) [pconst capp]+ let rhs = PResolveTC (fileFC "HACK")+ let ty = PPi constraint (sMN 0 "pc") c con+ iLOG (showTmImpls ty)+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)+ i <- getIState+ let conn = case con of+ PRef _ n -> n+ PApp _ (PRef _ n) _ -> n+ let conn' = case lookupCtxtName conn (idris_classes i) of+ [(n, _)] -> n+ _ -> conn+ addInstance False conn' cfn+ addIBC (IBCInstance False conn' cfn)+-- iputStrLn ("Added " ++ show (conn, cfn, ty))+ return [PTy emptyDocstring [] syn fc [] cfn ty,+ PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]++ -- Generate a top level function which looks up a method in a given+ -- dictionary (this is inlinable, always)+ tfun cn c syn all (m, (doc, o, ty))+ = do let ty' = insertConstraint c ty+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)+ let margs = getMArgs ty+ let anames = map (\x -> sMN x "arg") [0..]+ let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)+ let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)+ iLOG (showTmImpls ty)+ iLOG (show (m, ty', capp, margs))+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)+ return [PTy doc [] syn fc o m ty',+ PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]++ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc+ getMArgs _ = []++ getMeth (m:ms) (a:as) x | x == a = PRef fc m+ | otherwise = getMeth ms as x++ lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns+ lhsArgs (IA : xs) ns = lhsArgs xs ns+ lhsArgs (CA : xs) ns = lhsArgs xs ns+ lhsArgs [] _ = []++ rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns+ rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns+ rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns+ rhsArgs [] _ = []++ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)+ = PPi p n ty (insertConstraint c sc)+ insertConstraint c sc = PPi constraint (sMN 0 "class") c sc++ -- make arguments explicit and don't bind class parameters+ toExp ns e (PPi (Imp l s p) n ty sc)+ | n `elem` ns = toExp ns e sc+ | otherwise = PPi (e l s p) n ty (toExp ns e sc)+ toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)+ toExp ns e sc = sc++
+ src/Idris/Elab/Clause.hs view
@@ -0,0 +1,877 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Clause where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++-- | Elaborate a collection of left-hand and right-hand pairs - that is, a+-- top-level definition.+elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()+elabClauses info fc opts n_in cs = let n = liftname info n_in in+ do ctxt <- getContext+ ist <- getIState+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)++ -- Check n actually exists, with no definition yet+ let tys = lookupTy n ctxt+ let reflect = Reflection `elem` opts+ checkUndefined n ctxt+ unless (length tys > 1) $ do+ fty <- case tys of+ [] -> -- TODO: turn into a CAF if there's no arguments+ -- question: CAFs in where blocks?+ tclift $ tfail $ At fc (NoTypeDecl n)+ [ty] -> return ty+ let atys = map snd (getArgTys fty)+ cs_elab <- mapM (elabClause info opts)+ (zip [0..] cs)+ let (pats_in, cs_full) = unzip cs_elab++ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in++ solveDeferred n++ -- just ensure that the structure exists+ fmodifyState (ist_optimisation n) id+ addIBC (IBCOpt n)++ ist <- getIState+ let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in++ -- logLvl 3 (showSep "\n" (map (\ (l,r) ->+ -- show l ++ " = " +++ -- show r) pats))+ let tcase = opt_typecase (idris_options ist)++ -- Summary of what's about to happen: Definitions go:+ --+ -- pats_in -> pats -> pdef -> pdef'++ -- addCaseDef builds case trees from <pdef> and <pdef'>++ -- pdef is the compile-time pattern definition.+ -- This will get further optimised for run-time, and, separately,+ -- further inlined to help with totality checking.+ let pdef = map debind pats++ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats+ logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef++ -- Look for 'static' names and generate new specialised+ -- definitions for them++ mapM_ (\ e -> case e of+ Left _ -> return ()+ Right (l, r) -> elabPE info fc n r) pats++ -- NOTE: Need to store original definition so that proofs which+ -- rely on its structure aren't affected by any changes to the+ -- inliner. Just use the inlined version to generate pdef' and to+ -- help with later inlinings.++ ist <- getIState+ let pdef_inl = inlineDef ist pdef++ numArgs <- tclift $ sameLength pdef++ case specNames opts of+ Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats+ _ -> return ()++ erInfo <- getErasureInfo <$> getIState+ tree@(CaseDef scargs sc _) <- tclift $+ simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo+ cov <- coverage+ pmissing <-+ if cov && not (hasDefault cs)+ then do missing <- genClauses fc n (map getLHS pdef) cs_full+ -- missing <- genMissing n scargs sc+ missing' <- filterM (checkPossible info fc True n) missing+ let clhs = map getLHS pdef+ logLvl 2 $ "Must be unreachable:\n" +++ showSep "\n" (map showTmImpls missing') +++ "\nAgainst: " +++ showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))+ -- filter out anything in missing' which is+ -- matched by any of clhs. This might happen since+ -- unification may force a variable to take a+ -- particular form, rather than force a case+ -- to be impossible.+ return (filter (noMatch ist clhs) missing')+ else return []+ let pcover = null pmissing++ -- pdef' is the version that gets compiled for run-time+ pdef_in' <- applyOpts pdef+ let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'++ logLvl 5 $ "After data structure transformations:\n" ++ show pdef'++ ist <- getIState+ -- let wf = wellFounded ist n sc+ let tot = if pcover || AssertTotal `elem` opts+ then Unchecked -- finish checking later+ else Partial NotCovering -- already know it's not total++ -- case lookupCtxt (namespace info) n (idris_flags ist) of+ -- [fs] -> if TotalFn `elem` fs+ -- then case tot of+ -- Total _ -> return ()+ -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))+ -- else return ()+ -- _ -> return ()+ case tree of+ CaseDef _ _ [] -> return ()+ CaseDef _ _ xs -> mapM_ (\x ->+ iputStrLn $ show fc +++ ":warning - Unreachable case: " +++ show (delab ist x)) xs+ let knowncovering = (pcover && cov) || AssertTotal `elem` opts++ tree' <- tclift $ simpleCase tcase knowncovering reflect+ RunTime fc inacc atys pdef' erInfo+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree+ logLvl 3 $ "Optimised: " ++ show tree'+ ctxt <- getContext+ ist <- getIState+ let opt = idris_optimisation ist+ putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)+ (idris_patdefs ist) })+ let caseInfo = CaseInfo (inlinable opts) (dictionary opts)+ case lookupTy n ctxt of+ [ty] -> do updateContext (addCasedef n erInfo caseInfo+ tcase knowncovering+ reflect+ (AssertTotal `elem` opts)+ atys+ inacc+ pats+ pdef pdef pdef_inl pdef' ty)+ addIBC (IBCDef n)+ setTotality n tot+ when (not reflect) $ do totcheck (fc, n)+ defer_totcheck (fc, n)+ when (tot /= Unchecked) $ addIBC (IBCTotal n tot)+ i <- getIState+ case lookupDef n (tt_ctxt i) of+ (CaseOp _ _ _ _ _ cd : _) ->+ let (scargs, sc) = cases_compiletime cd+ (scargs', sc') = cases_runtime cd in+ do let calls = findCalls sc' scargs'+ let used = findUsedArgs sc' scargs'+ -- let scg = buildSCG i sc scargs+ -- add SCG later, when checking totality+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore+ logLvl 2 $ "Called names: " ++ show cg+ addToCG n cg+ addToCalledG n (nub (map fst calls)) -- plus names in type!+ addIBC (IBCCG n)+ _ -> return ()+ return ()+ -- addIBC (IBCTotal n tot)+ [] -> return ()+ -- Check it's covering, if 'covering' option is used. Chase+ -- all called functions, and fail if any of them are also+ -- 'Partial NotCovering'+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n+ where+ noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of+ Right _ -> False+ Left miss -> True) cs++ checkUndefined n ctxt = case lookupDef n ctxt of+ [] -> return ()+ [TyDecl _ _] -> return ()+ _ -> tclift $ tfail (At fc (AlreadyDefined n))++ debind (Right (x, y)) = let (vs, x') = depat [] x+ (_, y') = depat [] y in+ (vs, x', y')+ debind (Left x) = let (vs, x') = depat [] x in+ (vs, x', Impossible)++ depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)+ depat acc x = (acc, x)++ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args+ hasDefault _ = False++ getLHS (_, l, _) = l++ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, + force (normalisePats ctxt [] y))+ simple_lhs ctxt t = t++ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p + (rt_simplify ctxt [] y)))++ -- this is so pattern types are in the right form for erasure+ normalisePats ctxt env (Bind n (PVar t) sc) + = let t' = normalise ctxt env t in+ Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)+ normalisePats ctxt env (Bind n (PVTy t) sc) + = let t' = normalise ctxt env t in+ Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)+ normalisePats ctxt env t = t++ specNames [] = Nothing+ specNames (Specialise ns : _) = Just ns+ specNames (_ : xs) = specNames xs++ sameLength ((_, x, _) : xs)+ = do l <- sameLength xs+ let (f, as) = unApply x+ if (null xs || l == length as) then return (length as)+ else tfail (At fc (Msg "Clauses have differing numbers of arguments "))+ sameLength [] = return 0++ -- apply all transformations (just specialisation for now, add+ -- user defined transformation rules later)+ doTransforms ist pats =+ case specNames opts of+ Nothing -> pats+ Just ns -> partial_eval (tt_ctxt ist) ns pats++-- | Find 'static' applications in a term and partially evaluate them+elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()+elabPE info fc caller r =+ do ist <- getIState+ let sa = getSpecApps ist [] r+ mapM_ (mkSpecialised ist) sa+ where + -- TODO: Add a PTerm level transformation rule, which is basically the + -- new definition in reverse (before specialising it). + -- RHS => LHS where implicit arguments are left blank in the + -- transformation.++ -- Apply that transformation after every PClauses elaboration++ mkSpecialised ist specapp_in = do+ let (specTy, specapp) = getSpecTy ist specapp_in+ let (n, newnm, pats) = getSpecClause ist specapp+ let undef = case lookupDef newnm (tt_ctxt ist) of+ [] -> True+ _ -> False+ logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))+ idrisCatch+ (when (undef && all (concreteArg ist) (snd specapp)) $ do+ cgns <- getAllNames n+ let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++ + mapMaybe specName (snd specapp))]+ logLvl 3 $ "Specialising application: " ++ show specapp+ logLvl 2 $ "New name: " ++ show newnm+ iLOG $ "PE definition type : " ++ (show specTy)+ ++ "\n" ++ show opts+ logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" +++ showSep "\n" + (map (\ (lhs, rhs) ->+ (showTmImpls lhs ++ " = " ++ + showTmImpls rhs)) pats)+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy+ let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats+ elabClauses info fc opts newnm def+ logLvl 2 $ "Specialised " ++ show newnm)+ -- if it doesn't work, just don't specialise. Could happen for lots+ -- of valid reasons (e.g. local variables in scope which can't be+ -- lifted out).+ (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e)) ++ specName (ImplicitS, tm) + | (P Ref n _, _) <- unApply tm = Just (n, Just 1)+ specName (ExplicitS, tm)+ | (P Ref n _, _) <- unApply tm = Just (n, Just 1)+ specName _ = Nothing++ concreteArg ist (ImplicitS, tm) = concreteTm ist tm+ concreteArg ist (ExplicitS, tm) = concreteTm ist tm+ concreteArg ist _ = True++ concreteTm ist tm | (P _ n _, _) <- unApply tm =+ case lookupTy n (tt_ctxt ist) of+ [] -> False+ _ -> True+ concreteTm ist (Constant _) = True+ concreteTm ist _ = False++ -- get the type of a specialised application+ getSpecTy ist (n, args)+ = case lookupTy n (tt_ctxt ist) of+ [ty] -> let (specty_in, args') = specType args (explicitNames ty)+ specty = normalise (tt_ctxt ist) [] (finalise specty_in)+ t = mkPE_TyDecl ist args' (explicitNames specty) in+ (t, (n, args'))+-- (normalise (tt_ctxt ist) [] (specType args ty))+ _ -> error "Can't happen (getSpecTy)"++ -- get the clause of a specialised application+ getSpecClause ist (n, args)+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++ + showSep "_" (map showArg args)) in + -- UN (show n ++ show (map snd args)) in+ (n, newnm, mkPE_TermDecl ist newnm n args)+ where showArg (ExplicitS, n) = show n+ showArg (ImplicitS, n) = show n+ showArg _ = ""++-- checks if the clause is a possible left hand side. Returns the term if+-- possible, otherwise Nothing.++checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool+checkPossible info fc tcgen fname lhs_in+ = do ctxt <- getContext+ i <- getIState+ let lhs = addImplPat i lhs_in+ -- if the LHS type checks, it is possible+ case elaborate ctxt (sMN 0 "patLHS") infP []+ (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of+ OK ((lhs', _, _), _) ->+ do let lhs_tm = orderPats (getInferTerm lhs')+ case recheck ctxt [] (forget lhs_tm) lhs_tm of+ OK _ -> return True+ err -> return False+ -- if it's a recoverable error, the case may become possible+ Error err -> if tcgen then return (recoverable ctxt err)+ else return (validCase ctxt err ||+ recoverable ctxt err)+ where validCase ctxt (CantUnify _ topx topy e _ _)+ = let topx' = normalise ctxt [] topx+ topy' = normalise ctxt [] topy in+ not (sameFam topx' topy' || not (validCase ctxt e))+ validCase ctxt (CantConvert _ _ _) = False+ validCase ctxt (At _ e) = validCase ctxt e+ validCase ctxt (Elaborating _ _ e) = validCase ctxt e+ validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e+ validCase ctxt _ = True+ + recoverable ctxt (CantUnify r topx topy e _ _) + = let topx' = normalise ctxt [] topx+ topy' = normalise ctxt [] topy in+ checkRec topx' topy'+ recoverable ctxt (At _ e) = recoverable ctxt e+ recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e+ recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e+ recoverable _ _ = False++ sameFam topx topy + = case (unApply topx, unApply topy) of+ ((P _ x _, _), (P _ y _, _)) -> x == y+ _ -> False++ -- different notion of recoverable than in unification, since we+ -- have no metavars -- just looking to see if a constructor is failing+ -- to unify with a function that may be reduced later++ checkRec (App f a) p@(P _ _ _) = checkRec f p+ checkRec p@(P _ _ _) (App f a) = checkRec p f+ checkRec fa@(App _ _) fa'@(App _ _) + | (f, as) <- unApply fa,+ (f', as') <- unApply fa'+ = if (length as /= length as') + then checkRec f f' + else checkRec f f' && and (zipWith checkRec as as')+ checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt+ checkRec _ _ = False++ ntRec x y | Ref <- x = True+ | Ref <- y = True+ | otherwise = False -- name is different, unrecoverable++getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)+ = nub $ getFixedInType i env [] t +++ getFixedInType i (n : env) is (instantiate (P Bound n t) sc)+getFixedInType i env (_ : is) (Bind n (Pi t) sc)+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)+getFixedInType i env is tm@(App f a)+ | (P _ tn _, args) <- unApply tm+ = case lookupCtxt tn (idris_datatypes i) of+ [t] -> nub $ paramNames args env (param_pos t) +++ getFixedInType i env is f +++ getFixedInType i env is a+ [] -> nub $ getFixedInType i env is f +++ getFixedInType i env is a+ | otherwise = nub $ getFixedInType i env is f +++ getFixedInType i env is a+getFixedInType i _ _ _ = []++getFlexInType i env ps (Bind n (Pi t) sc)+ = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) +++ getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)+getFlexInType i env ps tm@(App f a)+ | (P _ tn _, args) <- unApply tm+ = case lookupCtxt tn (idris_datatypes i) of+ [t] -> nub $ paramNames args env [x | x <- [0..length args],+ not (x `elem` param_pos t)] + ++ getFlexInType i env ps f +++ getFlexInType i env ps a+ [] -> nub $ getFlexInType i env ps f +++ getFlexInType i env ps a+ | otherwise = nub $ getFlexInType i env ps f +++ getFlexInType i env ps a+getFlexInType i _ _ _ = []++-- Treat a name as a parameter if it appears in parameter positions in+-- types, and never in a non-parameter position in a (non-param) argument type.++getParamsInType i env ps t = let fix = getFixedInType i env ps t+ flex = getFlexInType i env fix t in+ [x | x <- fix, not (x `elem` flex)]++paramNames args env [] = []+paramNames args env (p : ps)+ | length args > p = case args!!p of+ P _ n _ -> if n `elem` env+ then n : paramNames args env ps+ else paramNames args env ps+ _ -> paramNames args env ps+ | otherwise = paramNames args env ps++propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm+propagateParams i ps t tm@(PApp _ (PRef fc n) args)+ = PApp fc (PRef fc n) (addP t args)+ where addP (Bind n _ sc) (t : ts)+ | Placeholder <- getTm t,+ n `elem` ps,+ not (n `elem` allNamesIn tm)+ = t { getTm = PRef fc n } : addP sc ts+ addP (Bind n _ sc) (t : ts) = t : addP sc ts+ addP _ ts = ts+propagateParams i ps t (PRef fc n)+ = case lookupCtxt n (idris_implicits i) of+ [is] -> let ps' = filter (isImplicit is) ps in+ PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')+ _ -> PRef fc n+ where isImplicit [] n = False+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True+ isImplicit (_ : is) n = isImplicit is n+propagateParams i ps t x = x++-- Return the elaborated LHS/RHS, and the original LHS with implicits added+elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->+ Idris (Either Term (Term, Term), PTerm)+elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])+ = do let tcgen = Dictionary `elem` opts+ i <- get+ let lhs = addImpl i lhs_in+ b <- checkPossible info fc tcgen fname lhs_in+ case b of+ True -> tclift $ tfail (At fc + (Msg $ show lhs_in ++ " is a valid case"))+ False -> do ptm <- mkPatTm lhs_in+ return (Left ptm, lhs)+elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)+ = do let tcgen = Dictionary `elem` opts+ ctxt <- getContext++ -- Build the LHS as an "Infer", and pull out its type and+ -- pattern bindings+ i <- getIState+ inf <- isTyInferred fname+ -- get the parameters first, to pass through to any where block+ let fn_ty = case lookupTy fname (tt_ctxt i) of+ [t] -> t+ _ -> error "Can't happen (elabClause function type)"+ let fn_is = case lookupCtxt fname (idris_implicits i) of+ [t] -> t+ _ -> []+ let params = getParamsInType i [] fn_is fn_ty+ let lhs = mkLHSapp $ stripUnmatchable i $+ propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)+ logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in +++ "\n" ++ show (fn_ty, fn_is))++ (((lhs', dlhs, []), probs, inj), _) <-+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []+ (do res <- errAt "left hand side of " fname+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))+ probs <- get_probs+ inj <- get_inj+ return (res, probs, inj))++ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)++ let lhs_tm = orderPats (getInferTerm lhs')+ let lhs_ty = getInferType lhs'+ logLvl 3 ("Elaborated: " ++ show lhs_tm)+ logLvl 3 ("Elaborated type: " ++ show lhs_ty)+ logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)++ -- If we're inferring metavariables in the type, don't recheck,+ -- because we're only doing this to try to work out those metavariables+ (clhs_c, clhsty) <- if not inf+ then recheckC fc [] lhs_tm+ else return (lhs_tm, lhs_ty)+ let clhs = normalise ctxt [] clhs_c+ + logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))++ rep <- useREPL+ when rep $ do+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))++ logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)+ -- Elaborate where block+ ist <- getIState+ windex <- getName+ let decls = nub (concatMap declared whereblock)+ let defs = nub (decls ++ concatMap defined whereblock)+ let newargs = pvars ist lhs_tm+ let winfo = pinfo info newargs defs windex+ let wb = map (expandParamsD False ist decorate newargs defs) whereblock++ -- Split the where block into declarations with a type, and those+ -- without+ -- Elaborate those with a type *before* RHS, those without *after*+ let (wbefore, wafter) = sepBlocks wb++ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter+ mapM_ (rec_elabDecl info EAll winfo) wbefore+ -- Now build the RHS, using the type of the LHS as the goal.+ i <- getIState -- new implicits from where block+ logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))+ let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)+ (expandParams decorate newargs defs (defs \\ decls) rhs_in)+ logLvl 2 $ "RHS: " ++ showTmImpls rhs+ ctxt <- getContext -- new context with where block added+ logLvl 5 "STARTING CHECK"+ ((rhs', defer, is, probs), _) <-+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []+ (do pbinds ist lhs_tm+ mapM_ setinj (nub (params ++ inj))+ setNextName + (_, _, is) <- errAt "right hand side of " fname+ (erun fc (build i winfo ERHS opts fname rhs))+ errAt "right hand side of " fname+ (erun fc $ psolve lhs_tm)+ hs <- get_holes+ aux <- getAux+ mapM_ (elabCaseHole aux) hs+ tt <- get_term+ let (tm, ds) = runState (collectDeferred (Just fname) tt) []+ probs <- get_probs+ return (tm, ds, is, probs))++ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)++ logLvl 5 "DONE CHECK"+ logLvl 2 $ "---> " ++ show rhs'+ when (not (null defer)) $ iLOG $ "DEFERRED " ++ + show (map (\ (n, (_,_,t)) -> (n, t)) defer)+ def' <- checkDef fc defer+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'+ addDeferred def''+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''++ when (not (null def')) $ do+ mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')++ -- Now the remaining deferred (i.e. no type declarations) clauses+ -- from the where block++ mapM_ (rec_elabDecl info EAll winfo) wafter+ mapM_ (elabCaseBlock winfo opts) is++ ctxt <- getContext+ logLvl 5 $ "Rechecking"+ logLvl 6 $ " ==> " ++ show (forget rhs')+ (crhs, crhsty) <- if not inf + then recheckC fc [] rhs'+ else return (rhs', clhsty)+ logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty+ case converts ctxt [] clhsty crhsty of+ OK _ -> return ()+ Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))+ i <- getIState+ checkInferred fc (delab' i crhs True True) rhs+ -- if the function is declared '%error_reverse', or its type,+ -- then we'll try running it in reverse to improve error messages+ let (ret_fam, _) = unApply (getRetTy crhsty)+ rev <- case ret_fam of+ P _ rfamn _ -> + case lookupCtxt rfamn (idris_datatypes i) of+ [TI _ _ dopts _ _] -> + return (DataErrRev `elem` dopts)+ _ -> return False+ _ -> return False++ when (rev || ErrorReverse `elem` opts) $ do+ addIBC (IBCErrRev (crhs, clhs))+ addErrRev (crhs, clhs) + return $ (Right (clhs, crhs), lhs)+ where+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo+ pinfo info ns ds i+ = let newps = params info ++ ns+ dsParams = map (\n -> (n, map fst newps)) ds+ newb = addAlist dsParams (inblock info)+ l = liftname info in+ info { params = newps,+ inblock = newb,+ liftname = id -- (\n -> case lookupCtxt n newb of+ -- Nothing -> n+ -- _ -> MN i (show n)) . l+ }++ mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []+ mkLHSapp t = t++ decorate (NS x ns)+ = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])+-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])+ decorate x+ = SN (WhereN cnum fname x)+-- = NS (SN (WhereN cnum fname x)) [show cnum]+-- = NS (UN ('#':show x)) [show cnum, show fname]++ sepBlocks bs = sepBlocks' [] bs where+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)+ = let (bf, af) = sepBlocks' (n : ns) bs in+ (d : bf, af)+ sepBlocks' ns (d@(PClauses _ _ n _) : bs)+ | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in+ (bf, d : af)+ sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in+ (b : bf, af)+ sepBlocks' ns [] = ([], [])+++ -- if a hole is just an argument/result of a case block, treat it as+ -- the unit type. Hack to help elaborate case in do blocks.+ elabCaseHole aux h = do+ focus h+ g <- goal+ case g of+ TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve+ _ -> return ()++ -- Is the name a pattern argument in the declaration+ isArg :: Name -> PDecl -> Bool+ isArg n (PClauses _ _ _ cs) = any isArg' cs+ where+ isArg' (PClause _ _ (PApp _ _ args) _ _ _) + = any (\x -> case x of+ PRef _ n' -> n == n'+ _ -> False) (map getTm args)+ isArg' _ = False+ isArg _ _ = False++elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)+ = do let tcgen = Dictionary `elem` opts+ ctxt <- getContext+ -- Build the LHS as an "Infer", and pull out its type and+ -- pattern bindings+ i <- getIState+ -- get the parameters first, to pass through to any where block+ let fn_ty = case lookupTy fname (tt_ctxt i) of+ [t] -> t+ _ -> error "Can't happen (elabClause function type)"+ let fn_is = case lookupCtxt fname (idris_implicits i) of+ [t] -> t+ _ -> []+ let params = getParamsInType i [] fn_is fn_ty+ let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))+ logLvl 2 ("LHS: " ++ show lhs)+ ((lhs', dlhs, []), _) <-+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []+ (errAt "left hand side of with in " fname+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )+ let lhs_tm = orderPats (getInferTerm lhs')+ let lhs_ty = getInferType lhs'+ let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))+ logLvl 3 (show lhs_tm)+ (clhs, clhsty) <- recheckC fc [] lhs_tm+ logLvl 5 ("Checked " ++ show clhs)+ let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))+ let wval = addImplBound i (map fst bargs) wval_in+ logLvl 5 ("Checking " ++ showTmImpls wval)+ -- Elaborate wval in this context+ ((wval', defer, is), _) <-+ tclift $ elaborate ctxt (sMN 0 "withRHS")+ (bindTyArgs PVTy bargs infP) []+ (do pbinds i lhs_tm+ setNextName+ -- TODO: may want where here - see winfo abpve+ (_', d, is) <- errAt "with value in " fname+ (erun fc (build i info ERHS opts fname (infTerm wval)))+ erun fc $ psolve lhs_tm+ tt <- get_term+ return (tt, d, is))+ def' <- checkDef fc defer+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'+ addDeferred def''+ mapM_ (elabCaseBlock info opts) is+ logLvl 5 ("Checked wval " ++ show wval')+ (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')+ let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)+ let cwvalN = explicitNames (normalise ctxt [] cwval)+ logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)+ let pvars = map fst (getPBtys cwvalty)+ -- we need the unelaborated term to get the names it depends on+ -- rather than a de Bruijn index.+ let pdeps = usedNamesIn pvars i (delab i cwvalty)+ let (bargs_pre, bargs_post) = split pdeps bargs []+ logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) +++ " depends on " ++ show pdeps ++ " from " ++ show pvars)+ logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)+ windex <- getName+ -- build a type declaration for the new function:+ -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty+ let wargval = getRetTy cwvalN+ let wargtype = getRetTy cwvaltyN+ logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)+ let wtype = bindTyArgs Pi (bargs_pre +++ (sMN 0 "warg", wargtype) :+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)+ logLvl 5 ("New function type " ++ show wtype)+ let wname = sMN windex (show fname)++ let imps = getImps wtype -- add to implicits context+ putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })+ addIBC (IBCDef wname)+ def' <- checkDef fc [(wname, (-1, Nothing, wtype))]+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'+ addDeferred def''++ -- in the subdecls, lhs becomes:+ -- fname pats | wpat [rest]+ -- ==> fname' ps wpat [rest], match pats against toplevel for ps+ wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))+ withblock+ logLvl 3 ("with block " ++ show wb)+ -- propagate totality assertion to the new definitions+ when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]+ mapM_ (rec_elabDecl info EAll info) wb++ -- rhs becomes: fname' ps wval+ let rhs = PApp fc (PRef fc wname)+ (map (pexp . (PRef fc) . fst) bargs_pre +++ pexp wval :+ (map (pexp . (PRef fc) . fst) bargs_post))+ logLvl 5 ("New RHS " ++ showTmImpls rhs)+ ctxt <- getContext -- New context with block added+ i <- getIState+ ((rhs', defer, is), _) <-+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []+ (do pbinds i lhs_tm+ setNextName+ (_, d, is) <- erun fc (build i info ERHS opts fname rhs)+ psolve lhs_tm+ tt <- get_term+ return (tt, d, is))+ def' <- checkDef fc defer+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'+ addDeferred def''+ mapM_ (elabCaseBlock info opts) is+ logLvl 5 ("Checked RHS " ++ show rhs')+ (crhs, crhsty) <- recheckC fc [] rhs'+ return $ (Right (clhs, crhs), lhs)+ where+ getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t+ getImps _ = []++ mkAuxC wname lhs ns ns' (PClauses fc o n cs)+ | True = do cs' <- mapM (mkAux wname lhs ns ns') cs+ return $ PClauses fc o wname cs'+ | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n+ mkAuxC wname lhs ns ns' d = return $ d++ mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)+ = do i <- getIState+ let tm = addImplPat i tm_in+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " +++ showTmImpls toplhs)+ case matchClause i toplhs tm of+ Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"+ Right mvars ->+ do logLvl 3 ("Match vars : " ++ show mvars)+ lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w+ return $ PClause fc wname lhs ws rhs wheres+ mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)+ = do i <- getIState+ let tm = addImplPat i tm_in+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " +++ showTmImpls toplhs)+ withs' <- mapM (mkAuxC wname toplhs ns ns') withs+ case matchClause i toplhs tm of+ Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")+ Right mvars ->+ do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w+ return $ PWith fc wname lhs ws wval withs'+ mkAux wname toplhs ns ns' c+ = ifail $ show fc ++ ":badly formed with clause"++ addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])+ addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]++ updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w+ = let ns = map (keepMvar (map fst mvars) fc') ns_in+ ns' = map (keepMvar (map fst mvars) fc') ns_in' in+ return $ substMatches mvars $+ PApp fc (PRef fc' wname)+ (map pexp ns ++ pexp w : (map pexp ns'))+ updateLHS n wname mvars ns_in ns_in' tm w+ = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w++ keepMvar mvs fc v | v `elem` mvs = PRef fc v+ | otherwise = Placeholder++ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))+ fullApp x = x++ split [] rest pre = (reverse pre, rest)+ split deps ((n, ty) : rest) pre+ | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)+ | otherwise = split deps rest ((n, ty) : pre)+ split deps [] pre = (reverse pre, [])++ abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)++
+ src/Idris/Elab/Data.hs view
@@ -0,0 +1,489 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Data(elabData) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)+ = do let codata = Codata `elem` opts+ iLOG (show (fc, doc))+ checkUndefined fc n+ (cty, t, inacc) <- buildType info syn fc [] n t_in++ addIBC (IBCDef n)+ updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons++elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)+ = do let codata = Codata `elem` opts+ iLOG (show fc)+ undef <- isUndefined fc n+ (cty, t, inacc) <- buildType info syn fc [] n t_in+ -- if n is defined already, make sure it is just a type declaration+ -- with the same type we've just elaborated+ i <- getIState+ checkDefinedAs fc n cty (tt_ctxt i)+ -- temporary, to check cons+ when undef $ updateContext (addTyDecl n (TCon 0 0) cty)+ let cnameinfo = cinfo info (map cname dcons)+ cons <- mapM (elabCon cnameinfo syn n codata) dcons+ ttag <- getName+ i <- getIState+ let as = map (const Nothing) (getArgTys cty)+ let params = findParams (map snd cons)+ logLvl 2 $ "Parameters : " ++ show params+ -- TI contains information about mutually declared types - this will+ -- be updated when the mutual block is complete+ putIState (i { idris_datatypes =+ addDef n (TI (map fst cons) codata opts params [n])+ (idris_datatypes i) })+ addIBC (IBCDef n)+ addIBC (IBCData n)+ checkDocs fc argDocs t+ addDocStr n doc argDocs+ addIBC (IBCDoc n)+ let metainf = DataMI params+ addIBC (IBCMetaInformation n metainf)+ -- TMP HACK! Make this a data option+ updateContext (addDatatype (Data n ttag cty cons))+ updateContext (setMetaInformation n metainf)+ mapM_ totcheck (zip (repeat fc) (map fst cons))+-- mapM_ (checkPositive n) cons++ -- if there's exactly one constructor,+ -- mark both the type and the constructor as detaggable+ case cons of+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)+ _ -> return ()++ -- create an eliminator+ when (DefaultEliminator `elem` opts) $+ evalStateT (elabCaseFun True params n t dcons info) Map.empty+ -- create a case function+ when (DefaultCaseFun `elem` opts) $+ evalStateT (elabCaseFun False params n t dcons info) Map.empty+ where+ setDetaggable :: Name -> Idris ()+ setDetaggable n = do+ ist <- getIState+ let opt = idris_optimisation ist+ case lookupCtxt n opt of+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }++ checkDefinedAs fc n t ctxt + = case lookupDef n ctxt of+ [] -> return ()+ [TyDecl _ ty] ->+ case converts ctxt [] t ty of+ OK () -> return ()+ _ -> tclift $ tfail (At fc (AlreadyDefined n))+ _ -> tclift $ tfail (At fc (AlreadyDefined n))+ -- parameters are names which are unchanged across the structure,+ -- which appear exactly once in the return type of a constructor++ -- First, find all applications of the constructor, then check over+ -- them for repeated arguments++ findParams :: [Type] -> [Int]+ findParams ts = let allapps = concatMap getDataApp ts in+ paramPos allapps++ paramPos [] = []+ paramPos (args : rest)+ = dropNothing $ keepSame (zip [0..] args) rest++ dropNothing [] = []+ dropNothing ((x, Nothing) : ts) = dropNothing ts+ dropNothing ((x, _) : ts) = x : dropNothing ts++ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->+ [(Int, Maybe Name)]+ keepSame as [] = as+ keepSame as (args : rest) = keepSame (update as args) rest+ where+ update [] _ = []+ update _ [] = []+ update ((n, Just x) : as) (Just x' : args)+ | x == x' = (n, Just x) : update as args+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args++ getDataApp :: Type -> [[Maybe Name]]+ getDataApp f@(App _ _)+ | (P _ d _, args) <- unApply f+ = if (d == n) then [mParam args args] else []+ getDataApp (Bind n (Pi t) sc)+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)+ getDataApp _ = []++ -- keep the arguments which are single names, which don't appear+ -- elsewhere++ mParam args [] = []+ mParam args (P Bound n _ : rest)+ | count n args == 1+ = Just n : mParam args rest+ where count n [] = 0+ count n (t : ts)+ | n `elem` freeNames t = 1 + count n ts+ | otherwise = count n ts+ mParam args (_ : rest) = Nothing : mParam args rest++ cname (_, _, n, _, _, _) = n++ -- Abuse of ElabInfo.+ -- TODO Contemplate whether the ElabInfo type needs modification.+ cinfo :: ElabInfo -> [Name] -> ElabInfo+ cinfo info ds+ = let newps = params info+ dsParams = map (\n -> (n, [])) ds+ newb = addAlist dsParams (inblock info)+ l = liftname info in+ info { params = newps,+ inblock = newb,+ liftname = id -- Is this appropriate?+ }++-- FIXME: 'forcenames' is an almighty hack! Need a better way of+-- erasing non-forceable things+-- ^^^+-- TODO: the above is a comment from the past;+-- forcenames is probably no longer needed+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)+ = do checkUndefined fc n+ (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)+ ctxt <- getContext+ let cty' = normalise ctxt [] cty++ -- Check that the constructor type is, in fact, a part of the family being defined+ tyIs n cty'++ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t+ logLvl 5 $ "Inaccessible args: " ++ show inacc+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'++ addIBC (IBCDef n)+ checkDocs fc argDocs t+ addDocStr n doc argDocs+ addIBC (IBCDoc n)+ fputState (opt_inaccessible . ist_optimisation n) inacc+ addIBC (IBCOpt n)+ return (n, cty')+ where+ tyIs con (Bind n b sc) = tyIs con sc+ tyIs con t | (P _ n' _, _) <- unApply t+ = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show n' ++ " is not " ++ show tn))))+ else return ()+ tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))++ mkLazy (PPi pl n ty sc) + = let ty' = if getTyName ty+ then PApp fc (PRef fc (sUN "Lazy'"))+ [pexp (PRef fc (sUN "LazyCodata")),+ pexp ty]+ else ty in+ PPi pl n ty' (mkLazy sc)+ mkLazy t = t++ getTyName (PApp _ (PRef _ n) _) = n == nsroot tn+ getTyName (PRef _ n) = n == nsroot tn+ getTyName _ = False+++ getNamePos :: Int -> PTerm -> Name -> Maybe Int+ getNamePos i (PPi _ n _ sc) x | n == x = Just i+ | otherwise = getNamePos (i + 1) sc x+ getNamePos _ _ _ = Nothing++type EliminatorState = StateT (Map.Map String Int) Idris++-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)+-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function+-- rename to caseFun to match updated intend+elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->+ ElabInfo -> EliminatorState ()+elabCaseFun ind paramPos n ty cons info = do+ elimLog $ "Elaborating case function"+ put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))+ let (cnstrs, _) = splitPi ty+ let (splittedTy@(pms, idxs)) = splitPms cnstrs+ generalParams <- namePis False pms+ motiveIdxs <- namePis False idxs+ let motive = mkMotive n paramPos generalParams motiveIdxs+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do+ let casefunt = if ind then "elim_" else "case_"+ name <- freshName $ casefunt ++ simpleName cnm+ consTerm <- extractConsTerm c generalParams+ return (name, expl, consTerm)) cons+ scrutineeIdxs <- namePis False idxs+ let motiveConstr = [(motiveName, expl, motive)]+ let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy+ let clauseConsElimArgs = map getPiName consTerms+ let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'+ let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy+ elimLog elimSig+ eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)+ let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses+ elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef+ State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl) (\err -> return ())+ -- Do not elaborate clauses if there aren't any+ case eliminatorClauses of+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type+ _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef) (\err -> return ())+ where elimLog :: String -> EliminatorState ()+ elimLog s = State.lift (logLvl 2 s)++ elimFC :: FC+ elimFC = fileFC "(casefun)"++ elimDeclName :: Name+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n++ applyNS :: Name -> [String] -> Name+ applyNS n [] = n+ applyNS n ns = sNS n ns++ splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)+ splitPi = splitPi' []+ where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)+ splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr+ splitPi' acc t = (reverse acc, t)++ splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])+ splitPms cnstrs = (map fst pms, map fst idxs)+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])++ isMachineGenerated :: Name -> Bool+ isMachineGenerated (MN _ _) = True+ isMachineGenerated _ = False++ namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]+ namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms+ let oldNames = map fst names+ let params = map snd names+ return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params++ mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))+ mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))+ mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg+ return (oldName, (name, pl, piarg))+ where keyOf :: PTerm -> String+ keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"+ keyOf (PApp _ tyf _) = keyOf tyf+ keyOf PType = "ty__"+ keyOf _ = "carg__"+ nameStart :: Name -> Char+ nameStart n = nameStart' (simpleName n)+ where nameStart' :: String -> Char+ nameStart' "" = ' '+ nameStart' ns = head ns++ simpleName :: Name -> String+ simpleName (NS n _) = simpleName n+ simpleName (MN i n) = str n ++ show i+ simpleName n = show n++ nameSpaces :: Name -> [String]+ nameSpaces (NS _ ns) = map str ns+ nameSpaces _ = []++ freshName :: String -> EliminatorState Name+ freshName key = do+ nameMap <- get+ let i = fromMaybe 0 (Map.lookup key nameMap)+ let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)+ put $ Map.insert key (i+1) nameMap+ return name++ scrutineeName :: Name+ scrutineeName = sUN "scrutinee"++ scrutineeArgName :: Name+ scrutineeArgName = sUN "scrutineeArg"++ motiveName :: Name+ motiveName = sUN "prop"++ mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm+ mkMotive n paramPos params indicies =+ let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))+ in piConstr (indicies ++ [scrutineeTy]) PType++ piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm+ piConstr [] ty = ty+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)++ interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]+ interlievePos idxs [] l2 i = l2+ interlievePos idxs l1 [] i = l1+ interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))+ interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))++ replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm+ replaceParams paramPos params cns =+ let (_, cnsResTy) = splitPi cns+ in case cnsResTy of+ PApp _ _ args ->+ let oldParams = paramNamesOf 0 paramPos args+ in removeParamPis oldParams params cns+ _ -> cns++ removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm+ removeParamPis oldParams params (PPi pl n tyb tyr) =+ case findIndex (== n) oldParams of+ Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))+ Just i -> (removeParamPis oldParams params tyr)+ removeParamPis oldParams params (PRef _ n) = + case findIndex (== n) oldParams of+ Nothing -> (PRef elimFC n)+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))+ removeParamPis oldParams params (PApp _ cns args) =+ PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args+ where replaceParamArgs :: [PArg] -> [PArg]+ replaceParamArgs [] = []+ replaceParamArgs (arg:args) =+ case extractName (getTm arg) of+ [] -> arg:replaceParamArgs args+ [n] ->+ case findIndex (== n) oldParams of+ Nothing -> arg:replaceParamArgs args+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args+ removeParamPis oldParams params t = t++ paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]+ paramNamesOf i paramPos [] = []+ paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args++ extractName :: PTerm -> [Name]+ extractName (PRef _ n) = [n]+ extractName _ = []++ splitArgPms :: PTerm -> ([PTerm], [PTerm])+ splitArgPms (PApp _ f args) = splitArgPms' args+ where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])+ splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])+ splitArgPms _ = ([],[])+++ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do+ i <- State.lift getIState+ implargs' <- case lookupCtxt cnm (idris_implicits i) of+ [] -> do fail $ "Error while showing implicits for " ++ show cnm+ [args] -> do return args+ _ -> do fail $ "Ambigous name for " ++ show cnm+ let implargs = mapMaybe convertImplPi implargs'+ let (_, cnsResTy) = splitPi ty+ case cnsResTy of+ PApp _ _ args ->+ let oldParams = paramNamesOf 0 paramPos args+ in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs+ _ -> return implargs++ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do+ let cons' = replaceParams paramPos generalParameters ty+ let (args, resTy) = splitPi cons'+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)+ consArgs <- namePis False args+ let recArgs = findRecArgs consArgs+ let recMotives = if ind then map applyRecMotive recArgs else []+ let (_, consIdxs) = splitArgPms resTy+ return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))+ where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)+ applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))+ where (_, idxs) = splitArgPms ty++ findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]+ findRecArgs [] = []+ findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs+ findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs+ findRecArgs (ty:rs) = findRecArgs rs++ applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)++ convertArg :: (Name, Plicity, PTerm) -> PArg+ convertArg (n, _, _) = pexp (PRef elimFC n)++ applyMotive :: [PTerm] -> PTerm -> PTerm+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])++ getPiName :: (Name, Plicity, PTerm) -> Name+ getPiName (name,_,_) = name++ convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)+ convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)+ convertImplPi _ = Nothing++ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do+ let cons' = replaceParams paramPos generalParameters ty+ let (args, resTy) = splitPi cons'+ i <- State.lift getIState+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)+ let (_, generalIdxs') = splitArgPms resTy+ let generalIdxs = map pexp generalIdxs'+ consArgs <- namePis False args+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])+ let recArgs = findRecArgs consArgs+ let recElims = if ind then map applyRecElim recArgs else []+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)+ return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []+ where applyRecElim :: (Name, Plicity, PTerm) -> PArg+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])+ where (_, idxs) = splitArgPms recTy+
+ src/Idris/Elab/Instance.hs view
@@ -0,0 +1,260 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Instance(elabInstance) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Data+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++elabInstance :: ElabInfo -> SyntaxInfo ->+ ElabWhat -> -- phase+ FC -> [PTerm] -> -- constraints+ Name -> -- the class+ [PTerm] -> -- class parameters (i.e. instance)+ PTerm -> -- full instance type+ Maybe Name -> -- explicit name+ [PDecl] -> Idris ()+elabInstance info syn what fc cs n ps t expn ds = do+ i <- getIState+ (n, ci) <- case lookupCtxtName n (idris_classes i) of+ [c] -> return c+ [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"+ cs -> tclift $ tfail $ At fc + (CantResolveAlts (map fst cs))+ let constraint = PApp fc (PRef fc n) (map pexp ps)+ let iname = mkiname n ps expn+ let emptyclass = null (class_methods ci)+ when (what /= EDefns || (null ds && not emptyclass)) $ do+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t+ -- if the instance type matches any of the instances we have already,+ -- and it's not a named instance, then it's overlapping, so report an error+ case expn of+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))+ (class_instances ci)+ addInstance intInst n iname+ Just _ -> addInstance intInst n iname+ when (what /= ETypes && (not (null ds && not emptyclass))) $ do + let ips = zip (class_params ci) ps+ let ns = case n of+ NS n ns' -> ns'+ _ -> []+ -- get the implicit parameters that need passing through to the+ -- where block+ wparams <- mapM (\p -> case p of+ PApp _ _ args -> getWParams (map getTm args)+ _ -> return []) ps+ let pnames = map pname (concat (nub wparams))+ let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances+ mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances+ let all_meths = map (nsroot . fst) (class_methods ci)+ let mtys = map (\ (n, (op, t)) ->+ let t_in = substMatchesShadow ips pnames t + mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))+ all_meths+ t' = substMatchesShadow mnamemap pnames t_in in+ (decorate ns iname n,+ op, coninsert cs t', t'))+ (class_methods ci)+ logLvl 3 (show (mtys, ips))+ let ds' = insertDefaults i iname (class_defaults ci) ns ds+ iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)+ mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))+ mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')+ let wbTys = map mkTyDecl mtys+ let wbVals = map (decorateid (decorate ns iname)) ds'+ let wb = wbTys ++ wbVals+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)+ logLvl 3 $ "Instance is " ++ show ps ++ " implicits " +++ show (concat (nub wparams))++ -- Bring variables in instance head into scope+ ist <- getIState+ let headVars = nub $ mapMaybe (\p -> case p of+ PRef _ n -> + case lookupTy n (tt_ctxt ist) of+ [] -> Just n+ _ -> Nothing+ _ -> Nothing) ps+-- let lhs = PRef fc iname+ let lhs = PApp fc (PRef fc iname)+ (map (\n -> pimp n (PRef fc n) True) headVars)+ let rhs = PApp fc (PRef fc (instanceName ci))+ (map (pexp . mkMethApp) mtys)++ logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars+ logLvl 5 $ "Instance RHS " ++ show rhs++ let idecls = [PClauses fc [Dictionary] iname+ [PClause fc iname lhs [] rhs wb]]+ iLOG (show idecls)+ mapM_ (rec_elabDecl info EAll info) idecls+ addIBC (IBCInstance intInst n iname)++ where+ intInst = case ps of+ [PConstant (AType (ATInt ITNative))] -> True+ _ -> False++ mkiname n' ps' expn' =+ case expn' of+ Nothing -> SN (sInstanceN n' (map show ps'))+ Just nm -> nm++ substInstance ips pnames (PInstance syn _ cs n ps t expn ds)+ = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds++ isOverlapping i (PInstance syn _ _ n ps t expn _)+ = case lookupCtxtName n (idris_classes i) of+ [(n, ci)] -> let iname = (mkiname n ps expn) in+ case lookupTy iname (tt_ctxt i) of+ [] -> elabFindOverlapping i ci iname syn t+ (_:_) -> return True+ _ -> return False -- couldn't find class, just let elabInstance fail later++ -- TODO: largely based upon elabType' - should try to abstract+ elabFindOverlapping i ci iname syn t+ = do ty' <- addUsingConstraints syn fc t+ -- TODO think: something more in info?+ ty' <- implicit info syn iname ty'+ let ty = addImpl i ty'+ ctxt <- getContext+ ((tyT, _, _), _) <-+ tclift $ elaborate ctxt iname (TType (UVal 0)) []+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))+ ctxt <- getContext+ (cty, _) <- recheckC fc [] tyT+ let nty = normalise ctxt [] cty+ return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)++ findOverlapping i t n+ | take 2 (show n) == "@@" = Nothing+ | otherwise+ = case lookupTy n (tt_ctxt i) of+ [t'] -> let tret = getRetType t+ tret' = getRetType (delab i t') in+ case matchClause i tret' tret of+ Right ms -> Just tret'+ Left _ -> case matchClause i tret tret' of+ Right ms -> Just tret'+ Left _ -> Nothing+ _ -> Nothing+ overlapping t' = tclift $ tfail (At fc (Msg $+ "Overlapping instance: " ++ show t' ++ " already defined"))+ getRetType (PPi _ _ _ sc) = getRetType sc+ getRetType t = t++ mkMethApp (n, _, _, ty)+ = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))+ lamBind i (PPi (Constraint _ _) _ _ sc) sc'+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')+ lamBind i (PPi _ n ty sc) sc'+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')+ lamBind i _ sc = sc+ methArgs i (PPi (Imp _ _ _) n ty sc)+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc+ methArgs i (PPi (Exp _ _ _) n ty sc)+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc+ methArgs i (PPi (Constraint _ _) n ty sc)+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc+ methArgs i _ = []++ papp fc f [] = f+ papp fc f as = PApp fc f as++ getWParams [] = return []+ getWParams (p : ps)+ | PRef _ n <- p+ = do ps' <- getWParams ps+ ctxt <- getContext+ case lookupP n ctxt of+ [] -> return (pimp n (PRef fc n) True : ps')+ _ -> return ps'+ getWParams (_ : ps) = getWParams ps++ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns+ decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns++ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t++ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)+ conbind [] x = x++ coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)+ coninsert cs sc = conbind cs sc++ insertDefaults :: IState -> Name ->+ [(Name, (Name, PDecl))] -> [T.Text] ->+ [PDecl] -> [PDecl]+ insertDefaults i iname [] ns ds = ds+ insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds+ = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)++ insertDef i meth def clauses ns iname decls+ | null $ filter (clauseFor meth iname ns) decls+ = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in+ -- trace (show newd) $+ decls ++ [newd]+ | otherwise = decls++ warnMissing decls ns iname meth+ | null $ filter (clauseFor meth iname ns) decls+ = iWarn fc . text $ "method " ++ show meth ++ " not defined"+ | otherwise = return ()++ checkInClass ns meth+ | not (null (filter (eqRoot meth) ns)) = return ()+ | otherwise = tclift $ tfail (At fc (Msg $+ show meth ++ " not a method of class " ++ show n))++ eqRoot x y = nsroot x == nsroot y++ clauseFor m iname ns (PClauses _ _ m' _)+ = decorate ns iname m == decorate ns iname m'+ clauseFor m iname ns _ = False++
+ src/Idris/Elab/Provider.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Provider(elabProvider) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Clause+import Idris.Elab.Value+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++-- | Elaborate a type provider+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()+elabProvider info syn fc what n+ = do i <- getIState+ -- Ensure that the experimental extension is enabled+ unless (TypeProviders `elem` idris_language_extensions i) $+ ifail $ "Failed to define type provider \"" ++ show n +++ "\".\nYou must turn on the TypeProviders extension."++ ctxt <- getContext++ -- First elaborate the expected type (and check that it's a type)+ -- The goal type for a postulate is always Type.+ (ty', typ) <- case what of+ ProvTerm ty p -> elabVal info ERHS ty+ ProvPostulate _ -> elabVal info ERHS PType+ unless (isTType typ) $+ ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)++ -- Elaborate the provider term to TT and check that the type matches+ (e, et) <- case what of+ ProvTerm _ tm -> elabVal info ERHS tm+ ProvPostulate tm -> elabVal info ERHS tm+ unless (isProviderOf (normalise ctxt [] ty') et) $+ ifail $ "Expected provider type IO (Provider (" +++ show ty' ++ "))" ++ ", got " ++ show et ++ " instead."++ -- Execute the type provider and normalise the result+ -- use 'run__provider' to convert to a primitive IO action++ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)+ [Erased, e])+ let rhs' = normalise ctxt [] rhs+ logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs++ -- Extract the provided term or postulate from the type provider+ provided <- getProvided fc rhs'++ case provided of+ Provide tm+ | ProvTerm ty _ <- what ->+ do -- Finally add a top-level definition of the provided term+ elabType info syn emptyDocstring [] fc [] n ty+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]+ logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm+ | ProvPostulate _ <- what ->+ do -- Add the postulate+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)+ logLvl 3 $ "Elaborated provided postulate " ++ show n+ | otherwise ->+ ierror . Msg $ "Attempted to provide a postulate where a term was expected."++ where isTType :: TT Name -> Bool+ isTType (TType _) = True+ isTType _ = False++ isProviderOf :: TT Name -> TT Name -> Bool+ isProviderOf tp prov+ | (P _ (UN io) _, [prov']) <- unApply prov+ , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'+ , tp == tp', io == txt "IO"+ , prov == txt "Provider" && provs == txt "Providers" = True+ isProviderOf _ _ = False+
+ src/Idris/Elab/Record.hs view
@@ -0,0 +1,242 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Record(elabRecord) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Type+import Idris.Elab.Data+import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])+ -- TODO think: something more in info?+ cty' <- implicit info syn cn cty_in+ i <- getIState++ -- get bound implicits and propagate to setters (in case they+ -- provide useful information for inference)+ let extraImpls = getBoundImpls cty'++ cty <- case lookupTy cn (tt_ctxt i) of+ [t] -> return (delab i t)+ _ -> ifail "Something went inexplicably wrong"+ cimp <- case lookupCtxt cn (idris_implicits i) of+ [imps] -> return imps+ ppos <- case lookupCtxt tyn (idris_datatypes i) of+ [ti] -> return $ param_pos ti+ let cty_imp = renameBs cimp cty+ let ptys = getProjs [] cty_imp+ let ptys_u = getProjs [] cty+ let recty = getRecTy cty_imp+ let recty_u = getRecTy cty++ let paramNames = getPNames recty ppos++ -- rename indices when we generate the getter/setter types, so+ -- that they don't clash with the names of the projections+ -- we're generating+ let index_names_in = getRecNameMap "_in" ppos recty+ let recty_in = substMatches index_names_in recty++ logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)+ -- Substitute indices with projection functions, and parameters with+ -- the updated parameter name+ let substs = map (\ (n, _) -> + if n `elem` paramNames+ then (n, PRef fc (mkp n))+ else (n, PApp fc (PRef fc n)+ [pexp (PRef fc rec)])) + ptys ++ -- Generate projection functions+ proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])+ logLvl 3 $ show proj_decls+ let nonImp = mapMaybe isNonImp (zip cimp ptys_u)+ let implBinds = getImplB id cty'++ -- Generate update functions+ update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls+ (getFieldNames cty')+ implBinds (length nonImp)) (zip nonImp [0..])+ mapM_ (rec_elabDecl info EAll info) (concat proj_decls)+ logLvl 3 $ show update_decls+ mapM_ (tryElabDecl info) (update_decls)+ where+-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }++ isNonImp (PExp _ _ _ _, a) = Just a+ isNonImp _ = Nothing++ getPNames (PApp _ _ as) ppos = getpn as ppos+ where+ getpn as [] = []+ getpn as (i:is) | length as > i,+ PRef _ n <- getTm (as!!i) = n : getpn as is+ | otherwise = getpn as is+ getPNames _ _ = []+ + tryElabDecl info (fn, ty, val)+ = do i <- getIState+ idrisCatch (do rec_elabDecl info EAll info ty+ rec_elabDecl info EAll info val)+ (\v -> do iputStrLn $ show fc +++ ":Warning - can't generate setter for " +++ show fn ++ " (" ++ show ty ++ ")"+-- ++ "\n" ++ pshow i v+ putIState i)++ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc+ getBoundImpls _ = []++ getImplB k (PPi (Imp l s _) n Placeholder sc)+ = getImplB k sc+ getImplB k (PPi (Imp l s p) n ty sc)+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc+ getImplB k (PPi _ n ty sc)+ = getImplB k sc+ getImplB k _ = k++ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)+ = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))+ renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)+ renameBs _ t = t++ getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s+ getProjs acc r = reverse acc++ getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s + getFieldNames (PPi _ _ _ s) = getFieldNames s+ getFieldNames _ = []++ getRecTy (PPi _ n ty s) = getRecTy s+ getRecTy t = t++ -- make sure we pick a consistent name for parameters; any name will do+ -- otherwise+ getRecNameMap x ppos (PApp fc t args) + = mapMaybe toMN (zip [0..] (map getTm args))+ where+ toMN (i, PRef fc n) + | i `elem` ppos = Just (n, PRef fc (mkp n))+ | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))+ toMN _ = Nothing+ getRecNameMap x _ _ = []++ rec = sMN 0 "rec"++ -- only UNs propagate properly as parameters (bit of a hack then...)+ mkp (UN n) = sUN ("_p_" ++ str n)+ mkp (MN i n) = sMN i ("p_" ++ str n)+ mkp (NS n s) = NS (mkp n) s++ mkImp (UN n) = sUN ("implicit_" ++ str n)+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)+ mkImp (NS n s) = NS (mkImp n) s++ mkType (UN n) = sUN ("set_" ++ str n)+ mkType (MN i n) = sMN i ("set_" ++ str n)+ mkType (NS n s) = NS (mkType n) s++ mkProj recty substs cimp ((pn_in, pty), pos)+ = do let pn = expandNS syn pn_in -- projection name+ -- use pn_in in the indices, consistently, to avoid clash+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn+ (PPi expl rec recty+ (substMatches substs pty))+ let pls = repeat Placeholder+ let before = pos+ let after = length substs - (pos + 1)+ let args = take before pls ++ PRef fc (mkp pn_in) : take after pls+ let iargs = map implicitise (zip cimp args)+ let lhs = PApp fc (PRef fc pn)+ [pexp (PApp fc (PRef fc cn) iargs)]+ let rhs = PRef fc (mkp pn_in)+ let pclause = PClause fc pn lhs [] rhs []+ return [pfnTy, PClauses fc [] pn [pclause]]++ implicitise (pa, t) = pa { getTm = t }++ -- If the 'pty' we're updating includes anything in 'substs', we're+ -- updating the type as well, so use recty', otherwise just use+ -- recty+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)+ = do let setname = expandNS syn $ mkType pn+ let valname = sMN 0 "updateval"+ let pn_out = sMN 0 (show pn ++ "_out")+ let pn_in = sMN 0 (show pn ++ "_in")+ let recty_in = substMatches [(pn, PRef fc pn_in)] recty+ let recty_out = substMatches [(pn, PRef fc pn_out)] recty+ let pt = substMatches inames $ + k (implBindUp extras inames (PPi expl pn_out pty+ (PPi expl rec recty_in recty_out)))+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt+-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]+ let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames+ let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames+ let lhsArgs = pls+ let rhsArgs = take pos pls ++ (PRef fc valname) :+ drop (pos + 1) pls+ let before = pos+ let pclause = PClause fc setname (PApp fc (PRef fc setname)+ [pexp (PRef fc valname),+ pexp (PApp fc (PRef fc cn)+ (map pexp lhsArgs))])+ []+ (PApp fc (PRef fc cn)+ (map pexp rhsArgs)) []+ return (pn, pfnTy, PClauses fc [] setname [pclause])++ implBindUp [] is t = t+ implBindUp ((n, ty):ns) is t + = let n' = case lookup n is of+ Just (PRef _ x) -> x+ _ -> n in+ if n `elem` allNamesIn t + then PPi impl n' ty (implBindUp ns is t)+ else implBindUp ns is t+
+ src/Idris/Elab/Type.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Type(buildType, elabType, elabType', elabPostulate) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> + Idris (Type, PTerm, [(Int, Name)])+buildType info syn fc opts n ty' = do+ ctxt <- getContext+ i <- getIState++ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'+ ty' <- addUsingConstraints syn fc ty'+ ty' <- addUsingImpls syn n fc ty'+ let ty = addImpl i ty'++ logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'+ logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty++ ((tyT', defer, is), log) <-+ tclift $ elaborate ctxt n (TType (UVal 0)) []+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))++ let tyT = patToImp tyT'++ logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'++ ds <- checkAddDef True False fc defer+ -- if the type is not complete, note that we'll need to infer+ -- things later (for solving metavariables)+ when (not (null ds)) $ addTyInferred n++ mapM_ (elabCaseBlock info opts) is+ ctxt <- getContext+ logLvl 5 $ "Rechecking"+ logLvl 6 $ show tyT+ logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT+ (cty, _) <- recheckC fc [] tyT++ -- record the implicit and inaccessible arguments+ i <- getIState+ let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty+ let inacc = inaccessibleImps 0 cty inaccData+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc++ putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }+ logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)+ addIBC (IBCImp n)++ return (cty, ty, inacc)+ where+ patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)+ patToImp (Bind n b sc) = Bind n b (patToImp sc)+ patToImp t = t+++-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->+ FC -> FnOpts -> Name -> PTerm -> Idris Type+elabType = elabType' False++elabType' :: Bool -> -- normalise it+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->+ FC -> FnOpts -> Name -> PTerm -> Idris Type+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in+ n = liftname info n_in in -}+ do checkUndefined fc n+ (cty, ty, inacc) <- buildType info syn fc opts n ty'++ addStatics n cty ty+ let nty = cty -- normalise ctxt [] cty+ -- if the return type is something coinductive, freeze the definition+ ctxt <- getContext+ let nty' = normalise ctxt [] nty+ logLvl 2 $ "Rechecked to " ++ show nty'++ -- Add normalised type to internals+ i <- getIState+ rep <- useREPL+ when rep $ do+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))++ let (t, _) = unApply (getRetTy nty')+ let corec = case t of+ P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of+ [TI _ True _ _ _] -> True+ _ -> False+ _ -> False+ -- Productivity checking now via checking for guarded 'Delay' + let opts' = opts -- if corec then (Coinductive : opts) else opts+ let usety = if norm then nty' else nty+ ds <- checkDef fc [(n, (-1, Nothing, usety))]+ addIBC (IBCDef n)+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds+ addDeferred ds'+ setFlags n opts'+ checkDocs fc argDocs ty+ addDocStr n doc argDocs+ addIBC (IBCDoc n)+ addIBC (IBCFlags n opts')+ fputState (opt_inaccessible . ist_optimisation n) inacc+ addIBC (IBCOpt n)+ when (Implicit `elem` opts') $ do addCoercion n+ addIBC (IBCCoercion n)++ -- If the function is declared as an error handler and the language+ -- extension is enabled, then add it to the list of error handlers.+ errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState+ when (ErrorHandler `elem` opts) $ do+ if errorReflection+ then+ -- TODO: Check that the declared type is the correct type for an error handler:+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt+ if tyIsHandler nty'+ then do i <- getIState+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }+ addIBC (IBCErrorHandler n)+ else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"+ else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."+ return usety+ where+ -- for making an internalapp, we only want the explicit ones, and don't+ -- want the parameters, so just take the arguments which correspond to the+ -- user declared explicit ones+ mergeTy (PPi e n ty sc) (PPi e' n' _ sc')+ | e == e' = PPi e n ty (mergeTy sc sc')+ | otherwise = mergeTy sc sc'+ mergeTy _ sc = sc++ err = txt "Err"+ maybe = txt "Maybe"+ lst = txt "List"+ errrep = txt "ErrorReportPart"++ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))+ (App (P _ (NS (UN m) ns2) _)+ (App (P _ (NS (UN l) ns3) _)+ (P _ (NS (UN r) ns4) _))))+ | e == err && m == maybe && l == lst && r == errrep+ , ns1 == map txt ["Errors","Reflection","Language"]+ , ns2 == map txt ["Maybe", "Prelude"]+ , ns3 == map txt ["List", "Prelude"]+ , ns4 == map txt ["Reflection","Language"] = True+ tyIsHandler _ = False++elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->+ FC -> FnOpts -> Name -> PTerm -> Idris ()+elabPostulate info syn doc fc opts n ty = do+ elabType info syn doc [] fc opts n ty+ putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState+ addIBC (IBCPostulate n)++ -- remove it from the deferred definitions list+ solveDeferred n
+ src/Idris/Elab/Utils.hs view
@@ -0,0 +1,151 @@+module Idris.Elab.Utils where++import Idris.AbsSyntax+import Idris.Error+import Idris.DeepSeq+import Idris.Delaborate+import Idris.Docstrings++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Typecheck++import Control.Applicative hiding (Const)+import Control.Monad+import Data.List++import Debug.Trace++import qualified Data.Map as Map++recheckC fc env t+ = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)+ ctxt <- getContext+ (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of+ Error e -> tfail (At fc e)+ OK x -> return x+ addConstraints fc cs+ return (tm, ty)+++checkDef fc ns = checkAddDef False True fc ns++checkAddDef add toplvl fc [] = return []+checkAddDef add toplvl fc ((n, (i, top, t)) : ns) + = do ctxt <- getContext+ (t', _) <- recheckC fc [] t+ when add $ do addDeferred [(n, (i, top, t, toplvl))]+ addIBC (IBCDef n)+ ns' <- checkAddDef add toplvl fc ns+ return ((n, (i, top, t')) : ns')++-- Get the list of (index, name) of inaccessible arguments from an elaborated+-- type+inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]+inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)+ | inacc = (i, n) : inaccessibleImps (i + 1) sc ins+ | otherwise = inaccessibleImps (i + 1) sc ins+inaccessibleImps _ _ _ = []++-- Get the list of (index, name) of inaccessible arguments from the type.+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]+inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit+inaccessibleArgs i (PPi plicity n ty t)+ | InaccessibleArg `elem` pargopts plicity+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}+ | otherwise+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}+inaccessibleArgs _ _ = []++elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()+elabCaseBlock info opts d@(PClauses f o n ps)+ = do addIBC (IBCDef n)+ logLvl 5 $ "CASE BLOCK: " ++ show (n, d)+ let opts' = nub (o ++ opts)+ -- propagate totality assertion to the new definitions+ when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]+ rec_elabDecl info EAll info (PClauses f opts' n ps )++-- Check that the result of type checking matches what the programmer wrote+-- (i.e. - if we inferred any arguments that the user provided, make sure+-- they are the same!)++checkInferred :: FC -> PTerm -> PTerm -> Idris ()+checkInferred fc inf user =+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" +++ showTmImpls user+ logLvl 10 $ "Checking match"+ i <- getIState+ tclift $ case matchClause' True i user inf of+ _ -> return ()+-- Left (x, y) -> tfail $ At fc+-- (Msg $ "The type-checked term and given term do not match: "+-- ++ show x ++ " and " ++ show y)+ logLvl 10 $ "Checked match"+-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)++-- Return whether inferred term is different from given term+-- (as above, but return a Bool)++inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool+inferredDiff fc inf user =+ do i <- getIState+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" +++ showTmImpls user+ tclift $ case matchClause' True i user inf of+ Right vs -> return False+ Left (x, y) -> return True++-- | Check a PTerm against documentation and ensure that every documented+-- argument actually exists. This must be run _after_ implicits have been+-- found, or it will give spurious errors.+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()+checkDocs fc args tm = cd (Map.fromList args) tm+ where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc+ cd as _ | Map.null as = return ()+ | otherwise = ierror . At fc . Msg $+ "There is documentation for argument(s) "+ ++ (concat . intersperse ", " . map show . Map.keys) as+ ++ " but they were not found."++decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t+decorateid decorate (PClauses f o n cs)+ = PClauses f o (decorate n) (map dc cs)+ where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds+ dc (PWith fc n t as w ds)+ = PWith fc (decorate n) (dappname t) as w+ (map (decorateid decorate) ds)+ dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as+ dappname t = t+++-- if 't' is a type class application, assume its arguments are injective+pbinds :: IState -> Term -> ElabD ()+pbinds i (Bind n (PVar t) sc) + = do attack; patbind n+ case unApply t of+ (P _ c _, args) -> case lookupCtxt c (idris_classes i) of+ [] -> return ()+ _ -> -- type class, set as injective+ mapM_ setinjArg args+ _ -> return ()+ pbinds i sc+ where setinjArg (P _ n _) = setinj n+ setinjArg _ = return ()+pbinds i tm = return ()++pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)+pbty _ tm = tm++getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc+getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc+getPBtys _ = []++psolve (Bind n (PVar t) sc) = do solve; psolve sc+psolve tm = return ()++pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc+pvars ist _ = []+
+ src/Idris/Elab/Value.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE PatternGuards #-}+module Idris.Elab.Value(elabVal, elabValBind) where++import Idris.AbsSyntax+import Idris.ASTUtils+import Idris.DSL+import Idris.Error+import Idris.Delaborate+import Idris.Imports+import Idris.ElabTerm+import Idris.Coverage+import Idris.DataOpts+import Idris.Providers+import Idris.Primitives+import Idris.Inliner+import Idris.PartialEval+import Idris.DeepSeq+import Idris.Output (iputStrLn, pshow, iWarn)+import IRTS.Lang++import Idris.Elab.Utils++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)++-- Elaborate a value, returning any new bindings created (this will only+-- happen if elaborating as a pattern clause)+elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])+elabValBind info aspat norm tm_in+ = do ctxt <- getContext+ i <- getIState+ let tm = addImpl i tm_in+ logLvl 10 (showTmImpls tm)+ -- try:+ -- * ordinary elaboration+ -- * elaboration as a Type+ -- * elaboration as a function a -> b++ ((tm', defer, is), _) <-+ tclift (elaborate ctxt (sMN 0 "val") infP []+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))+ let vtm = orderPats (getInferTerm tm')++ def' <- checkDef (fileFC "(input)") defer+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'+ addDeferred def''+ mapM_ (elabCaseBlock info []) is++ logLvl 3 ("Value: " ++ show vtm)+ (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm++ let vtm = if norm then normalise (tt_ctxt i) [] vtm_in+ else vtm_in+ let bargs = getPBtys vtm++ return (vtm, vty, bargs)++elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)+elabVal info aspat tm_in+ = do (tm, ty, _) <- elabValBind info aspat False tm_in+ return (tm, ty)++
src/Idris/ElabDecls.hs view
@@ -20,2498 +20,263 @@ import Idris.Output (iputStrLn, pshow, iWarn) import IRTS.Lang -import Idris.Core.TT-import Idris.Core.Elaborate hiding (Tactic(..))-import Idris.Core.Evaluate-import Idris.Core.Execute-import Idris.Core.Typecheck-import Idris.Core.CaseTree--import Idris.Docstrings--import Prelude hiding (id, (.))-import Control.Category--import Control.Applicative hiding (Const)-import Control.DeepSeq-import Control.Monad-import Control.Monad.State.Strict as State-import Data.List-import Data.Maybe-import Debug.Trace--import qualified Data.Map as Map-import qualified Data.Set as S-import qualified Data.Text as T-import Data.Char(isLetter, toLower)-import Data.List.Split (splitOn)--import Util.Pretty(pretty, text)--recheckC fc env t- = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)- ctxt <- getContext- (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of- Error e -> tfail (At fc e)- OK x -> return x- addConstraints fc cs- return (tm, ty)---checkDef fc ns = checkAddDef False True fc ns--checkAddDef add toplvl fc [] = return []-checkAddDef add toplvl fc ((n, (i, top, t)) : ns) - = do ctxt <- getContext- (t', _) <- recheckC fc [] t- when add $ do addDeferred [(n, (i, top, t, toplvl))]- addIBC (IBCDef n)- ns' <- checkAddDef add toplvl fc ns- return ((n, (i, top, t')) : ns')--- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t--- return (n, (i, top, t'))) ns--buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> - Idris (Type, PTerm, [(Int, Name)])-buildType info syn fc opts n ty' = do- ctxt <- getContext- i <- getIState-- logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'- ty' <- addUsingConstraints syn fc ty'- ty' <- addUsingImpls syn n fc ty'- let ty = addImpl i ty'-- logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'- logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty-- ((tyT', defer, is), log) <-- tclift $ elaborate ctxt n (TType (UVal 0)) []- (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))-- let tyT = patToImp tyT'-- logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'-- ds <- checkAddDef True False fc defer- -- if the type is not complete, note that we'll need to infer- -- things later (for solving metavariables)- when (not (null ds)) $ addTyInferred n-- mapM_ (elabCaseBlock info opts) is- ctxt <- getContext- logLvl 5 $ "Rechecking"- logLvl 6 $ show tyT- logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT- (cty, _) <- recheckC fc [] tyT-- -- record the implicit and inaccessible arguments- i <- getIState- let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty- let inacc = inaccessibleImps 0 cty inaccData- logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc-- putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }- logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)- addIBC (IBCImp n)-- return (cty, ty, inacc)- where- patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)- patToImp (Bind n b sc) = Bind n b (patToImp sc)- patToImp t = t----- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".-elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->- FC -> FnOpts -> Name -> PTerm -> Idris Type-elabType = elabType' False--elabType' :: Bool -> -- normalise it- ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->- FC -> FnOpts -> Name -> PTerm -> Idris Type-elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in- n = liftname info n_in in -}- do checkUndefined fc n- (cty, ty, inacc) <- buildType info syn fc opts n ty'-- addStatics n cty ty- let nty = cty -- normalise ctxt [] cty- -- if the return type is something coinductive, freeze the definition- ctxt <- getContext- let nty' = normalise ctxt [] nty- logLvl 2 $ "Rechecked to " ++ show nty'-- -- Add normalised type to internals- i <- getIState- rep <- useREPL- when rep $ do- addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?- addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))-- let (t, _) = unApply (getRetTy nty')- let corec = case t of- P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of- [TI _ True _ _ _] -> True- _ -> False- _ -> False- -- Productivity checking now via checking for guarded 'Delay' - let opts' = opts -- if corec then (Coinductive : opts) else opts- let usety = if norm then nty' else nty- ds <- checkDef fc [(n, (-1, Nothing, usety))]- addIBC (IBCDef n)- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds- addDeferred ds'- setFlags n opts'- checkDocs fc argDocs ty- addDocStr n doc argDocs- addIBC (IBCDoc n)- addIBC (IBCFlags n opts')- fputState (opt_inaccessible . ist_optimisation n) inacc- addIBC (IBCOpt n)- when (Implicit `elem` opts') $ do addCoercion n- addIBC (IBCCoercion n)-- -- If the function is declared as an error handler and the language- -- extension is enabled, then add it to the list of error handlers.- errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState- when (ErrorHandler `elem` opts) $ do- if errorReflection- then- -- TODO: Check that the declared type is the correct type for an error handler:- -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt- if tyIsHandler nty'- then do i <- getIState- putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }- addIBC (IBCErrorHandler n)- else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"- else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."- return usety- where- -- for making an internalapp, we only want the explicit ones, and don't- -- want the parameters, so just take the arguments which correspond to the- -- user declared explicit ones- mergeTy (PPi e n ty sc) (PPi e' n' _ sc')- | e == e' = PPi e n ty (mergeTy sc sc')- | otherwise = mergeTy sc sc'- mergeTy _ sc = sc-- err = txt "Err"- maybe = txt "Maybe"- lst = txt "List"- errrep = txt "ErrorReportPart"-- tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))- (App (P _ (NS (UN m) ns2) _)- (App (P _ (NS (UN l) ns3) _)- (P _ (NS (UN r) ns4) _))))- | e == err && m == maybe && l == lst && r == errrep- , ns1 == map txt ["Errors","Reflection","Language"]- , ns2 == map txt ["Maybe", "Prelude"]- , ns3 == map txt ["List", "Prelude"]- , ns4 == map txt ["Errors","Reflection","Language"] = True- tyIsHandler _ = False---- Get the list of (index, name) of inaccessible arguments from an elaborated--- type-inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]-inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)- | inacc = (i, n) : inaccessibleImps (i + 1) sc ins- | otherwise = inaccessibleImps (i + 1) sc ins-inaccessibleImps _ _ _ = []---- Get the list of (index, name) of inaccessible arguments from the type.-inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]-inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)- = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit-inaccessibleArgs i (PPi plicity n ty t)- | InaccessibleArg `elem` pargopts plicity- = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}- | otherwise- = inaccessibleArgs (i+1) t -- a {regular : Implicit}-inaccessibleArgs _ _ = []--elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->- FC -> FnOpts -> Name -> PTerm -> Idris ()-elabPostulate info syn doc fc opts n ty = do- elabType info syn doc [] fc opts n ty- putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState- addIBC (IBCPostulate n)-- -- remove it from the deferred definitions list- solveDeferred n--elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()-elabData info syn doc argDocs fc opts (PLaterdecl n t_in)- = do let codata = Codata `elem` opts- iLOG (show (fc, doc))- checkUndefined fc n- (cty, t, inacc) <- buildType info syn fc [] n t_in-- addIBC (IBCDef n)- updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons--elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)- = do let codata = Codata `elem` opts- iLOG (show fc)- undef <- isUndefined fc n- (cty, t, inacc) <- buildType info syn fc [] n t_in- -- if n is defined already, make sure it is just a type declaration- -- with the same type we've just elaborated- i <- getIState- checkDefinedAs fc n cty (tt_ctxt i)- -- temporary, to check cons- when undef $ updateContext (addTyDecl n (TCon 0 0) cty)- let cnameinfo = cinfo info (map cname dcons)- cons <- mapM (elabCon cnameinfo syn n codata) dcons- ttag <- getName- i <- getIState- let as = map (const Nothing) (getArgTys cty)- let params = findParams (map snd cons)- logLvl 2 $ "Parameters : " ++ show params- -- TI contains information about mutually declared types - this will- -- be updated when the mutual block is complete- putIState (i { idris_datatypes =- addDef n (TI (map fst cons) codata opts params [n])- (idris_datatypes i) })- addIBC (IBCDef n)- addIBC (IBCData n)- checkDocs fc argDocs t- addDocStr n doc argDocs- addIBC (IBCDoc n)- let metainf = DataMI params- addIBC (IBCMetaInformation n metainf)- -- TMP HACK! Make this a data option- updateContext (addDatatype (Data n ttag cty cons))- updateContext (setMetaInformation n metainf)- mapM_ totcheck (zip (repeat fc) (map fst cons))--- mapM_ (checkPositive n) cons-- -- if there's exactly one constructor,- -- mark both the type and the constructor as detaggable- case cons of- [(cn,ct)] -> setDetaggable cn >> setDetaggable n- >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)- _ -> return ()-- -- create an eliminator- when (DefaultEliminator `elem` opts) $- evalStateT (elabCaseFun True params n t dcons info) Map.empty- -- create a case function- when (DefaultCaseFun `elem` opts) $- evalStateT (elabCaseFun False params n t dcons info) Map.empty- where- setDetaggable :: Name -> Idris ()- setDetaggable n = do- ist <- getIState- let opt = idris_optimisation ist- case lookupCtxt n opt of- [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }- _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }-- checkDefinedAs fc n t ctxt - = case lookupDef n ctxt of- [] -> return ()- [TyDecl _ ty] ->- case converts ctxt [] t ty of- OK () -> return ()- _ -> tclift $ tfail (At fc (AlreadyDefined n))- _ -> tclift $ tfail (At fc (AlreadyDefined n))- -- parameters are names which are unchanged across the structure,- -- which appear exactly once in the return type of a constructor-- -- First, find all applications of the constructor, then check over- -- them for repeated arguments-- findParams :: [Type] -> [Int]- findParams ts = let allapps = concatMap getDataApp ts in- paramPos allapps-- paramPos [] = []- paramPos (args : rest)- = dropNothing $ keepSame (zip [0..] args) rest-- dropNothing [] = []- dropNothing ((x, Nothing) : ts) = dropNothing ts- dropNothing ((x, _) : ts) = x : dropNothing ts-- keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->- [(Int, Maybe Name)]- keepSame as [] = as- keepSame as (args : rest) = keepSame (update as args) rest- where- update [] _ = []- update _ [] = []- update ((n, Just x) : as) (Just x' : args)- | x == x' = (n, Just x) : update as args- update ((n, _) : as) (_ : args) = (n, Nothing) : update as args-- getDataApp :: Type -> [[Maybe Name]]- getDataApp f@(App _ _)- | (P _ d _, args) <- unApply f- = if (d == n) then [mParam args args] else []- getDataApp (Bind n (Pi t) sc)- = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)- getDataApp _ = []-- -- keep the arguments which are single names, which don't appear- -- elsewhere-- mParam args [] = []- mParam args (P Bound n _ : rest)- | count n args == 1- = Just n : mParam args rest- where count n [] = 0- count n (t : ts)- | n `elem` freeNames t = 1 + count n ts- | otherwise = count n ts- mParam args (_ : rest) = Nothing : mParam args rest-- cname (_, _, n, _, _, _) = n-- -- Abuse of ElabInfo.- -- TODO Contemplate whether the ElabInfo type needs modification.- cinfo :: ElabInfo -> [Name] -> ElabInfo- cinfo info ds- = let newps = params info- dsParams = map (\n -> (n, [])) ds- newb = addAlist dsParams (inblock info)- l = liftname info in- info { params = newps,- inblock = newb,- liftname = id -- Is this appropriate?- }---- FIXME: 'forcenames' is an almighty hack! Need a better way of--- erasing non-forceable things--- ^^^--- TODO: the above is a comment from the past;--- forcenames is probably no longer needed-elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->- (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)-elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)- = do checkUndefined fc n- (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)- ctxt <- getContext- let cty' = normalise ctxt [] cty-- logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t- logLvl 5 $ "Inaccessible args: " ++ show inacc- logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'-- addIBC (IBCDef n)- checkDocs fc argDocs t- addDocStr n doc argDocs- addIBC (IBCDoc n)- fputState (opt_inaccessible . ist_optimisation n) inacc- addIBC (IBCOpt n)- return (n, cty')- where- tyIs (Bind n b sc) = tyIs sc- tyIs t | (P _ n' _, _) <- unApply t- = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))- else return ()- tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))-- mkLazy (PPi pl n ty sc) - = let ty' = if getTyName ty- then PApp fc (PRef fc (sUN "Lazy'"))- [pexp (PRef fc (sUN "LazyCodata")),- pexp ty]- else ty in- PPi pl n ty' (mkLazy sc)- mkLazy t = t-- getTyName (PApp _ (PRef _ n) _) = n == nsroot tn- getTyName (PRef _ n) = n == nsroot tn- getTyName _ = False--- getNamePos :: Int -> PTerm -> Name -> Maybe Int- getNamePos i (PPi _ n _ sc) x | n == x = Just i- | otherwise = getNamePos (i + 1) sc x- getNamePos _ _ _ = Nothing--type EliminatorState = StateT (Map.Map String Int) Idris---- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)--- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function--- rename to caseFun to match updated intend-elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->- [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->- ElabInfo -> EliminatorState ()-elabCaseFun ind paramPos n ty cons info = do- elimLog $ "Elaborating case function"- put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))- let (cnstrs, _) = splitPi ty- let (splittedTy@(pms, idxs)) = splitPms cnstrs- generalParams <- namePis False pms- motiveIdxs <- namePis False idxs- let motive = mkMotive n paramPos generalParams motiveIdxs- consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do- let casefunt = if ind then "elim_" else "case_"- name <- freshName $ casefunt ++ simpleName cnm- consTerm <- extractConsTerm c generalParams- return (name, expl, consTerm)) cons- scrutineeIdxs <- namePis False idxs- let motiveConstr = [(motiveName, expl, motive)]- let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))- let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))- let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy- let clauseConsElimArgs = map getPiName consTerms- let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs- let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'- let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy- elimLog elimSig- eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)- let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses- elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef- State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())- -- Do not elaborate clauses if there aren't any- case eliminatorClauses of- [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type- _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())- where elimLog :: String -> EliminatorState ()- elimLog s = State.lift (logLvl 2 s)-- elimFC :: FC- elimFC = fileFC "(casefun)"-- elimDeclName :: Name- elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n-- applyNS :: Name -> [String] -> Name- applyNS n [] = n- applyNS n ns = sNS n ns-- splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)- splitPi = splitPi' []- where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)- splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr- splitPi' acc t = (reverse acc, t)-- splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])- splitPms cnstrs = (map fst pms, map fst idxs)- where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])-- isMachineGenerated :: Name -> Bool- isMachineGenerated (MN _ _) = True- isMachineGenerated _ = False-- namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]- namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms- let oldNames = map fst names- let params = map snd names- return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params-- mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))- mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))- mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg- return (oldName, (name, pl, piarg))- where keyOf :: PTerm -> String- keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"- keyOf (PApp _ tyf _) = keyOf tyf- keyOf PType = "ty__"- keyOf _ = "carg__"- nameStart :: Name -> Char- nameStart n = nameStart' (simpleName n)- where nameStart' :: String -> Char- nameStart' "" = ' '- nameStart' ns = head ns-- simpleName :: Name -> String- simpleName (NS n _) = simpleName n- simpleName (MN i n) = str n ++ show i- simpleName n = show n-- nameSpaces :: Name -> [String]- nameSpaces (NS _ ns) = map str ns- nameSpaces _ = []-- freshName :: String -> EliminatorState Name- freshName key = do- nameMap <- get- let i = fromMaybe 0 (Map.lookup key nameMap)- let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)- put $ Map.insert key (i+1) nameMap- return name-- scrutineeName :: Name- scrutineeName = sUN "scrutinee"-- scrutineeArgName :: Name- scrutineeArgName = sUN "scrutineeArg"-- motiveName :: Name- motiveName = sUN "prop"-- mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm- mkMotive n paramPos params indicies =- let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))- in piConstr (indicies ++ [scrutineeTy]) PType-- piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm- piConstr [] ty = ty- piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)-- interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]- interlievePos idxs [] l2 i = l2- interlievePos idxs l1 [] i = l1- interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))- interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))-- replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm- replaceParams paramPos params cns =- let (_, cnsResTy) = splitPi cns- in case cnsResTy of- PApp _ _ args ->- let oldParams = paramNamesOf 0 paramPos args- in removeParamPis oldParams params cns- _ -> cns-- removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm- removeParamPis oldParams params (PPi pl n tyb tyr) =- case findIndex (== n) oldParams of- Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))- Just i -> (removeParamPis oldParams params tyr)- removeParamPis oldParams params (PRef _ n) = - case findIndex (== n) oldParams of- Nothing -> (PRef elimFC n)- Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))- removeParamPis oldParams params (PApp _ cns args) =- PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args- where replaceParamArgs :: [PArg] -> [PArg]- replaceParamArgs [] = []- replaceParamArgs (arg:args) =- case extractName (getTm arg) of- [] -> arg:replaceParamArgs args- [n] ->- case findIndex (== n) oldParams of- Nothing -> arg:replaceParamArgs args- Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args- removeParamPis oldParams params t = t-- paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]- paramNamesOf i paramPos [] = []- paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args-- extractName :: PTerm -> [Name]- extractName (PRef _ n) = [n]- extractName _ = []-- splitArgPms :: PTerm -> ([PTerm], [PTerm])- splitArgPms (PApp _ f args) = splitArgPms' args- where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])- splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)- where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])- splitArgPms _ = ([],[])--- implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]- implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do- i <- State.lift getIState- implargs' <- case lookupCtxt cnm (idris_implicits i) of- [] -> do fail $ "Error while showing implicits for " ++ show cnm- [args] -> do return args- _ -> do fail $ "Ambigous name for " ++ show cnm- let implargs = mapMaybe convertImplPi implargs'- let (_, cnsResTy) = splitPi ty- case cnsResTy of- PApp _ _ args ->- let oldParams = paramNamesOf 0 paramPos args- in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs- _ -> return implargs-- extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm- extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do- let cons' = replaceParams paramPos generalParameters ty- let (args, resTy) = splitPi cons'- implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)- consArgs <- namePis False args- let recArgs = findRecArgs consArgs- let recMotives = if ind then map applyRecMotive recArgs else []- let (_, consIdxs) = splitArgPms resTy- return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))- where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)- applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))- where (_, idxs) = splitArgPms ty-- findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]- findRecArgs [] = []- findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs- findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs- findRecArgs (ty:rs) = findRecArgs rs-- applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm- applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)-- convertArg :: (Name, Plicity, PTerm) -> PArg- convertArg (n, _, _) = pexp (PRef elimFC n)-- applyMotive :: [PTerm] -> PTerm -> PTerm- applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])-- getPiName :: (Name, Plicity, PTerm) -> Name- getPiName (name,_,_) = name-- convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)- convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)- convertImplPi _ = Nothing-- generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause- generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do- let cons' = replaceParams paramPos generalParameters ty- let (args, resTy) = splitPi cons'- i <- State.lift getIState- implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)- let (_, generalIdxs') = splitArgPms resTy- let generalIdxs = map pexp generalIdxs'- consArgs <- namePis False args- let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])- let recArgs = findRecArgs consArgs- let recElims = if ind then map applyRecElim recArgs else []- let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)- return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []- where applyRecElim :: (Name, Plicity, PTerm) -> PArg- applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])- where (_, idxs) = splitArgPms recTy---- | Elaborate primitives--elabPrims :: Idris ()-elabPrims = do mapM_ (elabDecl EAll toplevel)- (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)- (zip4- [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]- [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]- [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]- [[], [], [], pairParamDoc, eqParamDoc]))- addNameHint eqTy (sUN "prf")- elabDecl EAll toplevel elimDecl- mapM_ elabPrim primitives- -- Special case prim__believe_me because it doesn't work on just constants- elabBelieveMe- -- Finally, syntactic equality- elabSynEq- where elabPrim :: Prim -> Idris ()- elabPrim (Prim n ty i def sc tot)- = do updateContext (addOperator n ty i (valuePrim def))- setTotality n tot- i <- getIState- putIState i { idris_scprims = (n, sc) : idris_scprims i }-- valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value- valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)-- getConst (VConstant c) = Just c- getConst _ = Nothing--- p_believeMe [_,_,x] = Just x- p_believeMe _ = Nothing- believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))- (Bind (sUN "b") (Pi (TType (UVar (-2))))- (Bind (sUN "x") (Pi (V 1)) (V 1)))- elabBelieveMe- = do let prim__believe_me = sUN "prim__believe_me"- updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)- setTotality prim__believe_me (Partial NotCovering)- i <- getIState- putIState i {- idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i- }-- p_synEq [t,_,x,y]- | x == y = Just (VApp (VApp vnJust VErased)- (VApp (VApp vnRefl t) x))- | otherwise = Just (VApp vnNothing VErased)- p_synEq args = Nothing-- nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased- vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased- vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased- vnRefl = VP (DCon 0 2) eqCon VErased-- synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))- (Bind (sUN "b") (Pi (TType (UVar (-3))))- (Bind (sUN "x") (Pi (V 1))- (Bind (sUN "y") (Pi (V 1))- (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)- [V 3, V 2, V 1, V 0]]))))- elabSynEq- = do let synEq = sUN "prim__syntactic_eq"-- updateContext (addOperator synEq synEqTy 4 p_synEq)- setTotality synEq (Total [])- i <- getIState- putIState i {- idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i- }----- | Elaborate a type provider-elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()-elabProvider info syn fc what n- = do i <- getIState- -- Ensure that the experimental extension is enabled- unless (TypeProviders `elem` idris_language_extensions i) $- ifail $ "Failed to define type provider \"" ++ show n ++- "\".\nYou must turn on the TypeProviders extension."-- ctxt <- getContext-- -- First elaborate the expected type (and check that it's a type)- -- The goal type for a postulate is always Type.- (ty', typ) <- case what of- ProvTerm ty p -> elabVal toplevel ERHS ty- ProvPostulate _ -> elabVal toplevel ERHS PType- unless (isTType typ) $- ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)-- -- Elaborate the provider term to TT and check that the type matches- (e, et) <- case what of- ProvTerm _ tm -> elabVal toplevel ERHS tm- ProvPostulate tm -> elabVal toplevel ERHS tm- unless (isProviderOf (normalise ctxt [] ty') et) $- ifail $ "Expected provider type IO (Provider (" ++- show ty' ++ "))" ++ ", got " ++ show et ++ " instead."-- -- Execute the type provider and normalise the result- -- use 'run__provider' to convert to a primitive IO action-- rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)- [Erased, e])- let rhs' = normalise ctxt [] rhs- logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs-- -- Extract the provided term or postulate from the type provider- provided <- getProvided fc rhs'-- case provided of- Provide tm- | ProvTerm ty _ <- what ->- do -- Finally add a top-level definition of the provided term- elabType info syn emptyDocstring [] fc [] n ty- elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]- logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm- | ProvPostulate _ <- what ->- do -- Add the postulate- elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)- logLvl 3 $ "Elaborated provided postulate " ++ show n- | otherwise ->- ierror . Msg $ "Attempted to provide a postulate where a term was expected."-- where isTType :: TT Name -> Bool- isTType (TType _) = True- isTType _ = False-- isProviderOf :: TT Name -> TT Name -> Bool- isProviderOf tp prov- | (P _ (UN io) _, [prov']) <- unApply prov- , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'- , tp == tp', io == txt "IO"- , prov == txt "Provider" && provs == txt "Providers" = True- isProviderOf _ _ = False--elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()-elabTransform info fc safe lhs_in rhs_in- = do ctxt <- getContext- i <- getIState- let lhs = addImplPat i lhs_in- ((lhs', dlhs, []), _) <-- tclift $ elaborate ctxt (sMN 0 "transLHS") infP []- (erun fc (buildTC i info ELHS [] (sUN "transform")- (infTerm lhs)))- let lhs_tm = orderPats (getInferTerm lhs')- let lhs_ty = getInferType lhs'- let newargs = pvars i lhs_tm-- (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm- logLvl 3 ("Transform LHS " ++ show clhs_tm)- let rhs = addImplBound i (map fst newargs) rhs_in- ((rhs', defer), _) <-- tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []- (do pbinds i lhs_tm- setNextName- erun fc (build i info ERHS [] (sUN "transform") rhs)- erun fc $ psolve lhs_tm- tt <- get_term- return (runState (collectDeferred Nothing tt) []))- (crhs_tm, crhs_ty) <- recheckC fc [] rhs'- logLvl 3 ("Transform RHS " ++ show crhs_tm)- when safe $ case converts ctxt [] clhs_tm crhs_tm of- OK _ -> return ()- Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))- addTrans (clhs_tm, crhs_tm)- addIBC (IBCTrans (clhs_tm, crhs_tm))---elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->- PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()-elabRecord info syn doc fc tyn ty opts cdoc cn cty_in- = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])- -- TODO think: something more in info?- cty' <- implicit info syn cn cty_in- i <- getIState-- -- get bound implicits and propagate to setters (in case they- -- provide useful information for inference)- let extraImpls = getBoundImpls cty'-- cty <- case lookupTy cn (tt_ctxt i) of- [t] -> return (delab i t)- _ -> ifail "Something went inexplicably wrong"- cimp <- case lookupCtxt cn (idris_implicits i) of- [imps] -> return imps- ppos <- case lookupCtxt tyn (idris_datatypes i) of- [ti] -> return $ param_pos ti- let cty_imp = renameBs cimp cty- let ptys = getProjs [] cty_imp- let ptys_u = getProjs [] cty- let recty = getRecTy cty_imp- let recty_u = getRecTy cty-- let paramNames = getPNames recty ppos-- -- rename indices when we generate the getter/setter types, so- -- that they don't clash with the names of the projections- -- we're generating- let index_names_in = getRecNameMap "_in" ppos recty- let recty_in = substMatches index_names_in recty-- logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)- -- Substitute indices with projection functions, and parameters with- -- the updated parameter name- let substs = map (\ (n, _) -> - if n `elem` paramNames- then (n, PRef fc (mkp n))- else (n, PApp fc (PRef fc n)- [pexp (PRef fc rec)])) - ptys -- -- Generate projection functions- proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])- logLvl 3 $ show proj_decls- let nonImp = mapMaybe isNonImp (zip cimp ptys_u)- let implBinds = getImplB id cty'-- -- Generate update functions- update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls- (getFieldNames cty')- implBinds (length nonImp)) (zip nonImp [0..])- mapM_ (elabDecl EAll info) (concat proj_decls)- logLvl 3 $ show update_decls- mapM_ (tryElabDecl info) (update_decls)- where--- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }-- isNonImp (PExp _ _ _ _, a) = Just a- isNonImp _ = Nothing-- getPNames (PApp _ _ as) ppos = getpn as ppos- where- getpn as [] = []- getpn as (i:is) | length as > i,- PRef _ n <- getTm (as!!i) = n : getpn as is- | otherwise = getpn as is- getPNames _ _ = []- - tryElabDecl info (fn, ty, val)- = do i <- getIState- idrisCatch (do elabDecl' EAll info ty- elabDecl' EAll info val)- (\v -> do iputStrLn $ show fc ++- ":Warning - can't generate setter for " ++- show fn ++ " (" ++ show ty ++ ")"--- ++ "\n" ++ pshow i v- putIState i)-- getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc- getBoundImpls _ = []-- getImplB k (PPi (Imp l s _) n Placeholder sc)- = getImplB k sc- getImplB k (PPi (Imp l s p) n ty sc)- = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc- getImplB k (PPi _ n ty sc)- = getImplB k sc- getImplB k _ = k-- renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)- = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))- renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)- renameBs _ t = t-- getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s- getProjs acc r = reverse acc-- getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s - getFieldNames (PPi _ _ _ s) = getFieldNames s- getFieldNames _ = []-- getRecTy (PPi _ n ty s) = getRecTy s- getRecTy t = t-- -- make sure we pick a consistent name for parameters; any name will do- -- otherwise- getRecNameMap x ppos (PApp fc t args) - = mapMaybe toMN (zip [0..] (map getTm args))- where- toMN (i, PRef fc n) - | i `elem` ppos = Just (n, PRef fc (mkp n))- | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))- toMN _ = Nothing- getRecNameMap x _ _ = []-- rec = sMN 0 "rec"-- -- only UNs propagate properly as parameters (bit of a hack then...)- mkp (UN n) = sUN ("_p_" ++ str n)- mkp (MN i n) = sMN i ("p_" ++ str n)- mkp (NS n s) = NS (mkp n) s-- mkImp (UN n) = sUN ("implicit_" ++ str n)- mkImp (MN i n) = sMN i ("implicit_" ++ str n)- mkImp (NS n s) = NS (mkImp n) s-- mkType (UN n) = sUN ("set_" ++ str n)- mkType (MN i n) = sMN i ("set_" ++ str n)- mkType (NS n s) = NS (mkType n) s-- mkProj recty substs cimp ((pn_in, pty), pos)- = do let pn = expandNS syn pn_in -- projection name- -- use pn_in in the indices, consistently, to avoid clash- let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn- (PPi expl rec recty- (substMatches substs pty))- let pls = repeat Placeholder- let before = pos- let after = length substs - (pos + 1)- let args = take before pls ++ PRef fc (mkp pn_in) : take after pls- let iargs = map implicitise (zip cimp args)- let lhs = PApp fc (PRef fc pn)- [pexp (PApp fc (PRef fc cn) iargs)]- let rhs = PRef fc (mkp pn_in)- let pclause = PClause fc pn lhs [] rhs []- return [pfnTy, PClauses fc [] pn [pclause]]-- implicitise (pa, t) = pa { getTm = t }-- -- If the 'pty' we're updating includes anything in 'substs', we're- -- updating the type as well, so use recty', otherwise just use- -- recty- mkUpdate recty inames extras fnames k num ((pn, pty), pos)- = do let setname = expandNS syn $ mkType pn- let valname = sMN 0 "updateval"- let pn_out = sMN 0 (show pn ++ "_out")- let pn_in = sMN 0 (show pn ++ "_in")- let recty_in = substMatches [(pn, PRef fc pn_in)] recty- let recty_out = substMatches [(pn, PRef fc pn_out)] recty- let pt = substMatches inames $ - k (implBindUp extras inames (PPi expl pn_out pty- (PPi expl rec recty_in recty_out)))- let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt--- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]- let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames- let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames- let lhsArgs = pls- let rhsArgs = take pos pls ++ (PRef fc valname) :- drop (pos + 1) pls- let before = pos- let pclause = PClause fc setname (PApp fc (PRef fc setname)- [pexp (PRef fc valname),- pexp (PApp fc (PRef fc cn)- (map pexp lhsArgs))])- []- (PApp fc (PRef fc cn)- (map pexp rhsArgs)) []- return (pn, pfnTy, PClauses fc [] setname [pclause])-- implBindUp [] is t = t- implBindUp ((n, ty):ns) is t - = let n' = case lookup n is of- Just (PRef _ x) -> x- _ -> n in- if n `elem` allNamesIn t - then PPi impl n' ty (implBindUp ns is t)- else implBindUp ns is t---- | Elaborate a collection of left-hand and right-hand pairs - that is, a--- top-level definition.-elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()-elabClauses info fc opts n_in cs = let n = liftname info n_in in- do ctxt <- getContext- ist <- getIState- inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)-- -- Check n actually exists, with no definition yet- let tys = lookupTy n ctxt- let reflect = Reflection `elem` opts- checkUndefined n ctxt- unless (length tys > 1) $ do- fty <- case tys of- [] -> -- TODO: turn into a CAF if there's no arguments- -- question: CAFs in where blocks?- tclift $ tfail $ At fc (NoTypeDecl n)- [ty] -> return ty- let atys = map snd (getArgTys fty)- cs_elab <- mapM (elabClause info opts)- (zip [0..] cs)- let (pats_in, cs_full) = unzip cs_elab-- logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in-- solveDeferred n-- -- just ensure that the structure exists- fmodifyState (ist_optimisation n) id- addIBC (IBCOpt n)-- ist <- getIState- let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in-- -- logLvl 3 (showSep "\n" (map (\ (l,r) ->- -- show l ++ " = " ++- -- show r) pats))- let tcase = opt_typecase (idris_options ist)-- -- Summary of what's about to happen: Definitions go:- --- -- pats_in -> pats -> pdef -> pdef'-- -- addCaseDef builds case trees from <pdef> and <pdef'>-- -- pdef is the compile-time pattern definition.- -- This will get further optimised for run-time, and, separately,- -- further inlined to help with totality checking.- let pdef = map debind pats-- logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats- logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef-- -- Look for 'static' names and generate new specialised- -- definitions for them-- mapM_ (\ e -> case e of- Left _ -> return ()- Right (l, r) -> elabPE info fc n r) pats-- -- NOTE: Need to store original definition so that proofs which- -- rely on its structure aren't affected by any changes to the- -- inliner. Just use the inlined version to generate pdef' and to- -- help with later inlinings.-- ist <- getIState- let pdef_inl = inlineDef ist pdef-- numArgs <- tclift $ sameLength pdef-- case specNames opts of- Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats- _ -> return ()-- erInfo <- getErasureInfo <$> getIState- tree@(CaseDef scargs sc _) <- tclift $- simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo- cov <- coverage- pmissing <-- if cov && not (hasDefault cs)- then do missing <- genClauses fc n (map getLHS pdef) cs_full- -- missing <- genMissing n scargs sc- missing' <- filterM (checkPossible info fc True n) missing- let clhs = map getLHS pdef- logLvl 2 $ "Must be unreachable:\n" ++- showSep "\n" (map showTmImpls missing') ++- "\nAgainst: " ++- showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))- -- filter out anything in missing' which is- -- matched by any of clhs. This might happen since- -- unification may force a variable to take a- -- particular form, rather than force a case- -- to be impossible.- return (filter (noMatch ist clhs) missing')- else return []- let pcover = null pmissing-- -- pdef' is the version that gets compiled for run-time- pdef_in' <- applyOpts pdef- let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'-- logLvl 5 $ "After data structure transformations:\n" ++ show pdef'-- ist <- getIState- -- let wf = wellFounded ist n sc- let tot = if pcover || AssertTotal `elem` opts- then Unchecked -- finish checking later- else Partial NotCovering -- already know it's not total-- -- case lookupCtxt (namespace info) n (idris_flags ist) of- -- [fs] -> if TotalFn `elem` fs- -- then case tot of- -- Total _ -> return ()- -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))- -- else return ()- -- _ -> return ()- case tree of- CaseDef _ _ [] -> return ()- CaseDef _ _ xs -> mapM_ (\x ->- iputStrLn $ show fc ++- ":warning - Unreachable case: " ++- show (delab ist x)) xs- let knowncovering = (pcover && cov) || AssertTotal `elem` opts-- tree' <- tclift $ simpleCase tcase knowncovering reflect- RunTime fc inacc atys pdef' erInfo- logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree- logLvl 3 $ "Optimised: " ++ show tree'- ctxt <- getContext- ist <- getIState- let opt = idris_optimisation ist- putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)- (idris_patdefs ist) })- let caseInfo = CaseInfo (inlinable opts) (dictionary opts)- case lookupTy n ctxt of- [ty] -> do updateContext (addCasedef n erInfo caseInfo- tcase knowncovering- reflect- (AssertTotal `elem` opts)- atys- inacc- pats- pdef pdef pdef_inl pdef' ty)- addIBC (IBCDef n)- setTotality n tot- when (not reflect) $ do totcheck (fc, n)- defer_totcheck (fc, n)- when (tot /= Unchecked) $ addIBC (IBCTotal n tot)- i <- getIState- case lookupDef n (tt_ctxt i) of- (CaseOp _ _ _ _ _ cd : _) ->- let (scargs, sc) = cases_compiletime cd- (scargs', sc') = cases_runtime cd in- do let calls = findCalls sc' scargs'- let used = findUsedArgs sc' scargs'- -- let scg = buildSCG i sc scargs- -- add SCG later, when checking totality- let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore- logLvl 2 $ "Called names: " ++ show cg- addToCG n cg- addToCalledG n (nub (map fst calls)) -- plus names in type!- addIBC (IBCCG n)- _ -> return ()- return ()- -- addIBC (IBCTotal n tot)- [] -> return ()- -- Check it's covering, if 'covering' option is used. Chase- -- all called functions, and fail if any of them are also- -- 'Partial NotCovering'- when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n- where- noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of- Right _ -> False- Left miss -> True) cs-- checkUndefined n ctxt = case lookupDef n ctxt of- [] -> return ()- [TyDecl _ _] -> return ()- _ -> tclift $ tfail (At fc (AlreadyDefined n))-- debind (Right (x, y)) = let (vs, x') = depat [] x- (_, y') = depat [] y in- (vs, x', y')- debind (Left x) = let (vs, x') = depat [] x in- (vs, x', Impossible)-- depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)- depat acc x = (acc, x)-- hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs- , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args- hasDefault _ = False-- getLHS (_, l, _) = l-- simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, - force (normalisePats ctxt [] y))- simple_lhs ctxt t = t-- simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p - (rt_simplify ctxt [] y)))-- -- this is so pattern types are in the right form for erasure- normalisePats ctxt env (Bind n (PVar t) sc) - = let t' = normalise ctxt env t in- Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)- normalisePats ctxt env (Bind n (PVTy t) sc) - = let t' = normalise ctxt env t in- Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)- normalisePats ctxt env t = t-- specNames [] = Nothing- specNames (Specialise ns : _) = Just ns- specNames (_ : xs) = specNames xs-- sameLength ((_, x, _) : xs)- = do l <- sameLength xs- let (f, as) = unApply x- if (null xs || l == length as) then return (length as)- else tfail (At fc (Msg "Clauses have differing numbers of arguments "))- sameLength [] = return 0-- -- apply all transformations (just specialisation for now, add- -- user defined transformation rules later)- doTransforms ist pats =- case specNames opts of- Nothing -> pats- Just ns -> partial_eval (tt_ctxt ist) ns pats---- | Find 'static' applications in a term and partially evaluate them-elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()-elabPE info fc caller r =- do ist <- getIState- let sa = getSpecApps ist [] r- mapM_ (mkSpecialised ist) sa- where - -- TODO: Add a PTerm level transformation rule, which is basically the - -- new definition in reverse (before specialising it). - -- RHS => LHS where implicit arguments are left blank in the - -- transformation.-- -- Apply that transformation after every PClauses elaboration-- mkSpecialised ist specapp_in = do- let (specTy, specapp) = getSpecTy ist specapp_in- let (n, newnm, pats) = getSpecClause ist specapp- let undef = case lookupDef newnm (tt_ctxt ist) of- [] -> True- _ -> False- logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))- idrisCatch- (when (undef && all (concreteArg ist) (snd specapp)) $ do- cgns <- getAllNames n- let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++ - mapMaybe specName (snd specapp))]- logLvl 3 $ "Specialising application: " ++ show specapp- logLvl 2 $ "New name: " ++ show newnm- iLOG $ "PE definition type : " ++ (show specTy)- ++ "\n" ++ show opts- logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++- showSep "\n" - (map (\ (lhs, rhs) ->- (showTmImpls lhs ++ " = " ++ - showTmImpls rhs)) pats)- elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy- let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats- elabClauses info fc opts newnm def- logLvl 2 $ "Specialised " ++ show newnm)- -- if it doesn't work, just don't specialise. Could happen for lots- -- of valid reasons (e.g. local variables in scope which can't be- -- lifted out).- (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e)) -- specName (ImplicitS, tm) - | (P Ref n _, _) <- unApply tm = Just (n, Just 1)- specName (ExplicitS, tm)- | (P Ref n _, _) <- unApply tm = Just (n, Just 1)- specName _ = Nothing-- concreteArg ist (ImplicitS, tm) = concreteTm ist tm- concreteArg ist (ExplicitS, tm) = concreteTm ist tm- concreteArg ist _ = True-- concreteTm ist tm | (P _ n _, _) <- unApply tm =- case lookupTy n (tt_ctxt ist) of- [] -> False- _ -> True- concreteTm ist (Constant _) = True- concreteTm ist _ = False-- -- get the type of a specialised application- getSpecTy ist (n, args)- = case lookupTy n (tt_ctxt ist) of- [ty] -> let (specty_in, args') = specType args (explicitNames ty)- specty = normalise (tt_ctxt ist) [] (finalise specty_in)- t = mkPE_TyDecl ist args' (explicitNames specty) in- (t, (n, args'))--- (normalise (tt_ctxt ist) [] (specType args ty))- _ -> error "Can't happen (getSpecTy)"-- -- get the clause of a specialised application- getSpecClause ist (n, args)- = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++ - showSep "_" (map showArg args)) in - -- UN (show n ++ show (map snd args)) in- (n, newnm, mkPE_TermDecl ist newnm n args)- where showArg (ExplicitS, n) = show n- showArg (ImplicitS, n) = show n- showArg _ = ""----- Elaborate a value, returning any new bindings created (this will only--- happen if elaborating as a pattern clause)-elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])-elabValBind info aspat norm tm_in- = do ctxt <- getContext- i <- getIState- let tm = addImpl i tm_in- logLvl 10 (showTmImpls tm)- -- try:- -- * ordinary elaboration- -- * elaboration as a Type- -- * elaboration as a function a -> b-- ((tm', defer, is), _) <---- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []--- (build i info aspat (MN 0 "val") tm))- tclift (elaborate ctxt (sMN 0 "val") infP []- (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))- let vtm = orderPats (getInferTerm tm')-- def' <- checkDef (fileFC "(input)") defer- let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'- addDeferred def''- mapM_ (elabCaseBlock info []) is-- logLvl 3 ("Value: " ++ show vtm)--- recheckC (fileFC "(input)") [] tm'--- logLvl 2 (show vtm)- (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm-- let vtm = if norm then normalise (tt_ctxt i) [] vtm_in- else vtm_in- let bargs = getPBtys vtm-- return (vtm, vty, bargs)--elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)-elabVal info aspat tm_in- = do (tm, ty, _) <- elabValBind info aspat False tm_in- return (tm, ty)---- checks if the clause is a possible left hand side. Returns the term if--- possible, otherwise Nothing.--checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool-checkPossible info fc tcgen fname lhs_in- = do ctxt <- getContext- i <- getIState- let lhs = addImplPat i lhs_in- -- if the LHS type checks, it is possible- case elaborate ctxt (sMN 0 "patLHS") infP []- (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of- OK ((lhs', _, _), _) ->- do let lhs_tm = orderPats (getInferTerm lhs')- case recheck ctxt [] (forget lhs_tm) lhs_tm of- OK _ -> return True- err -> return False- -- if it's a recoverable error, the case may become possible- Error err -> if tcgen then return (recoverable ctxt err)- else return (validCase ctxt err ||- recoverable ctxt err)- where validCase ctxt (CantUnify _ topx topy e _ _)- = let topx' = normalise ctxt [] topx- topy' = normalise ctxt [] topy in- not (sameFam topx' topy' || not (validCase ctxt e))- validCase ctxt (CantConvert _ _ _) = False- validCase ctxt (At _ e) = validCase ctxt e- validCase ctxt (Elaborating _ _ e) = validCase ctxt e- validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e- validCase ctxt _ = True- - recoverable ctxt (CantUnify r topx topy e _ _) - = let topx' = normalise ctxt [] topx- topy' = normalise ctxt [] topy in- checkRec topx' topy'- recoverable ctxt (At _ e) = recoverable ctxt e- recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e- recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e- recoverable _ _ = False-- sameFam topx topy - = case (unApply topx, unApply topy) of- ((P _ x _, _), (P _ y _, _)) -> x == y- _ -> False-- -- different notion of recoverable than in unification, since we- -- have no metavars -- just looking to see if a constructor is failing- -- to unify with a function that may be reduced later-- checkRec (App f a) p@(P _ _ _) = checkRec f p- checkRec p@(P _ _ _) (App f a) = checkRec p f- checkRec fa@(App _ _) fa'@(App _ _) - | (f, as) <- unApply fa,- (f', as') <- unApply fa'- = if (length as /= length as') - then checkRec f f' - else checkRec f f' && and (zipWith checkRec as as')- checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt- checkRec _ _ = False-- ntRec x y | Ref <- x = True- | Ref <- y = True- | otherwise = False -- name is different, unrecoverable--getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)- = nub $ getFixedInType i env [] t ++- getFixedInType i (n : env) is (instantiate (P Bound n t) sc)-getFixedInType i env (_ : is) (Bind n (Pi t) sc)- = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)-getFixedInType i env is tm@(App f a)- | (P _ tn _, args) <- unApply tm- = case lookupCtxt tn (idris_datatypes i) of- [t] -> nub $ paramNames args env (param_pos t) ++- getFixedInType i env is f ++- getFixedInType i env is a- [] -> nub $ getFixedInType i env is f ++- getFixedInType i env is a- | otherwise = nub $ getFixedInType i env is f ++- getFixedInType i env is a-getFixedInType i _ _ _ = []--getFlexInType i env ps (Bind n (Pi t) sc)- = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++- getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)-getFlexInType i env ps tm@(App f a)- | (P _ tn _, args) <- unApply tm- = case lookupCtxt tn (idris_datatypes i) of- [t] -> nub $ paramNames args env [x | x <- [0..length args],- not (x `elem` param_pos t)] - ++ getFlexInType i env ps f ++- getFlexInType i env ps a- [] -> nub $ getFlexInType i env ps f ++- getFlexInType i env ps a- | otherwise = nub $ getFlexInType i env ps f ++- getFlexInType i env ps a-getFlexInType i _ _ _ = []---- Treat a name as a parameter if it appears in parameter positions in--- types, and never in a non-parameter position in a (non-param) argument type.--getParamsInType i env ps t = let fix = getFixedInType i env ps t- flex = getFlexInType i env fix t in- [x | x <- fix, not (x `elem` flex)]--paramNames args env [] = []-paramNames args env (p : ps)- | length args > p = case args!!p of- P _ n _ -> if n `elem` env- then n : paramNames args env ps- else paramNames args env ps- _ -> paramNames args env ps- | otherwise = paramNames args env ps--propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm-propagateParams i ps t tm@(PApp _ (PRef fc n) args)- = PApp fc (PRef fc n) (addP t args)- where addP (Bind n _ sc) (t : ts)- | Placeholder <- getTm t,- n `elem` ps,- not (n `elem` allNamesIn tm)- = t { getTm = PRef fc n } : addP sc ts- addP (Bind n _ sc) (t : ts) = t : addP sc ts- addP _ ts = ts-propagateParams i ps t (PRef fc n)- = case lookupCtxt n (idris_implicits i) of- [is] -> let ps' = filter (isImplicit is) ps in- PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')- _ -> PRef fc n- where isImplicit [] n = False- isImplicit (PImp _ _ _ x _ : is) n | x == n = True- isImplicit (_ : is) n = isImplicit is n-propagateParams i ps t x = x---- Return the elaborated LHS/RHS, and the original LHS with implicits added-elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->- Idris (Either Term (Term, Term), PTerm)-elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])- = do let tcgen = Dictionary `elem` opts- i <- get- let lhs = addImpl i lhs_in- b <- checkPossible info fc tcgen fname lhs_in- case b of- True -> tclift $ tfail (At fc - (Msg $ show lhs_in ++ " is a valid case"))- False -> do ptm <- mkPatTm lhs_in- return (Left ptm, lhs)-elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)- = do let tcgen = Dictionary `elem` opts- ctxt <- getContext-- -- Build the LHS as an "Infer", and pull out its type and- -- pattern bindings- i <- getIState- inf <- isTyInferred fname- -- get the parameters first, to pass through to any where block- let fn_ty = case lookupTy fname (tt_ctxt i) of- [t] -> t- _ -> error "Can't happen (elabClause function type)"- let fn_is = case lookupCtxt fname (idris_implicits i) of- [t] -> t- _ -> []- let params = getParamsInType i [] fn_is fn_ty- let lhs = mkLHSapp $ stripUnmatchable i $- propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))- logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)- logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++- "\n" ++ show (fn_ty, fn_is))-- (((lhs', dlhs, []), probs, inj), _) <-- tclift $ elaborate ctxt (sMN 0 "patLHS") infP []- (do res <- errAt "left hand side of " fname- (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))- probs <- get_probs- inj <- get_inj- return (res, probs, inj))-- when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)-- let lhs_tm = orderPats (getInferTerm lhs')- let lhs_ty = getInferType lhs'- logLvl 3 ("Elaborated: " ++ show lhs_tm)- logLvl 3 ("Elaborated type: " ++ show lhs_ty)- logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)-- -- If we're inferring metavariables in the type, don't recheck,- -- because we're only doing this to try to work out those metavariables- (clhs_c, clhsty) <- if not inf- then recheckC fc [] lhs_tm- else return (lhs_tm, lhs_ty)- let clhs = normalise ctxt [] clhs_c- - logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))-- rep <- useREPL- when rep $ do- addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?- addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))-- logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)- -- Elaborate where block- ist <- getIState- windex <- getName- let decls = nub (concatMap declared whereblock)- let defs = nub (decls ++ concatMap defined whereblock)- let newargs = pvars ist lhs_tm- let winfo = pinfo info newargs defs windex- let wb = map (expandParamsD False ist decorate newargs defs) whereblock-- -- Split the where block into declarations with a type, and those- -- without- -- Elaborate those with a type *before* RHS, those without *after*- let (wbefore, wafter) = sepBlocks wb-- logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter- mapM_ (elabDecl' EAll winfo) wbefore- -- Now build the RHS, using the type of the LHS as the goal.- i <- getIState -- new implicits from where block- logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))- let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)- (expandParams decorate newargs defs (defs \\ decls) rhs_in)- logLvl 2 $ "RHS: " ++ showTmImpls rhs- ctxt <- getContext -- new context with where block added- logLvl 5 "STARTING CHECK"- ((rhs', defer, is, probs), _) <-- tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []- (do pbinds ist lhs_tm- mapM_ setinj (nub (params ++ inj))- setNextName - (_, _, is) <- errAt "right hand side of " fname- (erun fc (build i winfo ERHS opts fname rhs))- errAt "right hand side of " fname- (erun fc $ psolve lhs_tm)- hs <- get_holes- aux <- getAux- mapM_ (elabCaseHole aux) hs- tt <- get_term- let (tm, ds) = runState (collectDeferred (Just fname) tt) []- probs <- get_probs- return (tm, ds, is, probs))-- when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)-- logLvl 5 "DONE CHECK"- logLvl 2 $ "---> " ++ show rhs'- when (not (null defer)) $ iLOG $ "DEFERRED " ++ - show (map (\ (n, (_,_,t)) -> (n, t)) defer)- def' <- checkDef fc defer- let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'- addDeferred def''- mapM_ (\(n, _) -> addIBC (IBCDef n)) def''-- when (not (null def')) $ do- mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')-- -- Now the remaining deferred (i.e. no type declarations) clauses- -- from the where block-- mapM_ (elabDecl' EAll winfo) wafter- mapM_ (elabCaseBlock winfo opts) is-- ctxt <- getContext- logLvl 5 $ "Rechecking"- logLvl 6 $ " ==> " ++ show (forget rhs')- (crhs, crhsty) <- if not inf - then recheckC fc [] rhs'- else return (rhs', clhsty)- logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty- case converts ctxt [] clhsty crhsty of- OK _ -> return ()- Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))- i <- getIState- checkInferred fc (delab' i crhs True True) rhs- -- if the function is declared '%error_reverse', or its type,- -- then we'll try running it in reverse to improve error messages- let (ret_fam, _) = unApply (getRetTy crhsty)- rev <- case ret_fam of- P _ rfamn _ -> - case lookupCtxt rfamn (idris_datatypes i) of- [TI _ _ dopts _ _] -> - return (DataErrRev `elem` dopts)- _ -> return False- _ -> return False-- when (rev || ErrorReverse `elem` opts) $ do- addIBC (IBCErrRev (crhs, clhs))- addErrRev (crhs, clhs) - return $ (Right (clhs, crhs), lhs)- where- pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo- pinfo info ns ds i- = let newps = params info ++ ns- dsParams = map (\n -> (n, map fst newps)) ds- newb = addAlist dsParams (inblock info)- l = liftname info in- info { params = newps,- inblock = newb,- liftname = id -- (\n -> case lookupCtxt n newb of- -- Nothing -> n- -- _ -> MN i (show n)) . l- }-- mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []- mkLHSapp t = t-- decorate (NS x ns)- = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])--- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])- decorate x- = SN (WhereN cnum fname x)--- = NS (SN (WhereN cnum fname x)) [show cnum]--- = NS (UN ('#':show x)) [show cnum, show fname]-- sepBlocks bs = sepBlocks' [] bs where- sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)- = let (bf, af) = sepBlocks' (n : ns) bs in- (d : bf, af)- sepBlocks' ns (d@(PClauses _ _ n _) : bs)- | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in- (bf, d : af)- sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in- (b : bf, af)- sepBlocks' ns [] = ([], [])--- -- if a hole is just an argument/result of a case block, treat it as- -- the unit type. Hack to help elaborate case in do blocks.- elabCaseHole aux h = do- focus h- g <- goal- case g of- TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve- _ -> return ()-- -- Is the name a pattern argument in the declaration- isArg :: Name -> PDecl -> Bool- isArg n (PClauses _ _ _ cs) = any isArg' cs- where- isArg' (PClause _ _ (PApp _ _ args) _ _ _) - = any (\x -> case x of- PRef _ n' -> n == n'- _ -> False) (map getTm args)- isArg' _ = False- isArg _ _ = False--elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)- = do let tcgen = Dictionary `elem` opts- ctxt <- getContext- -- Build the LHS as an "Infer", and pull out its type and- -- pattern bindings- i <- getIState- -- get the parameters first, to pass through to any where block- let fn_ty = case lookupTy fname (tt_ctxt i) of- [t] -> t- _ -> error "Can't happen (elabClause function type)"- let fn_is = case lookupCtxt fname (idris_implicits i) of- [t] -> t- _ -> []- let params = getParamsInType i [] fn_is fn_ty- let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))- logLvl 2 ("LHS: " ++ show lhs)- ((lhs', dlhs, []), _) <-- tclift $ elaborate ctxt (sMN 0 "patLHS") infP []- (errAt "left hand side of with in " fname- (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )- let lhs_tm = orderPats (getInferTerm lhs')- let lhs_ty = getInferType lhs'- let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))- logLvl 3 (show lhs_tm)- (clhs, clhsty) <- recheckC fc [] lhs_tm- logLvl 5 ("Checked " ++ show clhs)- let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))- let wval = addImplBound i (map fst bargs) wval_in- logLvl 5 ("Checking " ++ showTmImpls wval)- -- Elaborate wval in this context- ((wval', defer, is), _) <-- tclift $ elaborate ctxt (sMN 0 "withRHS")- (bindTyArgs PVTy bargs infP) []- (do pbinds i lhs_tm- setNextName- -- TODO: may want where here - see winfo abpve- (_', d, is) <- errAt "with value in " fname- (erun fc (build i info ERHS opts fname (infTerm wval)))- erun fc $ psolve lhs_tm- tt <- get_term- return (tt, d, is))- def' <- checkDef fc defer- let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'- addDeferred def''- mapM_ (elabCaseBlock info opts) is- logLvl 5 ("Checked wval " ++ show wval')- (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')- let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)- let cwvalN = explicitNames (normalise ctxt [] cwval)- logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)- let pvars = map fst (getPBtys cwvalty)- -- we need the unelaborated term to get the names it depends on- -- rather than a de Bruijn index.- let pdeps = usedNamesIn pvars i (delab i cwvalty)- let (bargs_pre, bargs_post) = split pdeps bargs []- logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++- " depends on " ++ show pdeps ++ " from " ++ show pvars)- logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)- windex <- getName- -- build a type declaration for the new function:- -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty- let wargval = getRetTy cwvalN- let wargtype = getRetTy cwvaltyN- logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)- let wtype = bindTyArgs Pi (bargs_pre ++- (sMN 0 "warg", wargtype) :- map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)- (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)- logLvl 5 ("New function type " ++ show wtype)- let wname = sMN windex (show fname)-- let imps = getImps wtype -- add to implicits context- putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })- addIBC (IBCDef wname)- def' <- checkDef fc [(wname, (-1, Nothing, wtype))]- let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'- addDeferred def''-- -- in the subdecls, lhs becomes:- -- fname pats | wpat [rest]- -- ==> fname' ps wpat [rest], match pats against toplevel for ps- wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))- withblock- logLvl 3 ("with block " ++ show wb)- -- propagate totality assertion to the new definitions- when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]- mapM_ (elabDecl EAll info) wb-- -- rhs becomes: fname' ps wval- let rhs = PApp fc (PRef fc wname)- (map (pexp . (PRef fc) . fst) bargs_pre ++- pexp wval :- (map (pexp . (PRef fc) . fst) bargs_post))- logLvl 5 ("New RHS " ++ showTmImpls rhs)- ctxt <- getContext -- New context with block added- i <- getIState- ((rhs', defer, is), _) <-- tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []- (do pbinds i lhs_tm- setNextName- (_, d, is) <- erun fc (build i info ERHS opts fname rhs)- psolve lhs_tm- tt <- get_term- return (tt, d, is))- def' <- checkDef fc defer- let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'- addDeferred def''- mapM_ (elabCaseBlock info opts) is- logLvl 5 ("Checked RHS " ++ show rhs')- (crhs, crhsty) <- recheckC fc [] rhs'- return $ (Right (clhs, crhs), lhs)- where- getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t- getImps _ = []-- mkAuxC wname lhs ns ns' (PClauses fc o n cs)- | True = do cs' <- mapM (mkAux wname lhs ns ns') cs- return $ PClauses fc o wname cs'- | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n- mkAuxC wname lhs ns ns' d = return $ d-- mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)- = do i <- getIState- let tm = addImplPat i tm_in- logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++- showTmImpls toplhs)- case matchClause i toplhs tm of- Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"- Right mvars ->- do logLvl 3 ("Match vars : " ++ show mvars)- lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w- return $ PClause fc wname lhs ws rhs wheres- mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)- = do i <- getIState- let tm = addImplPat i tm_in- logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++- showTmImpls toplhs)- withs' <- mapM (mkAuxC wname toplhs ns ns') withs- case matchClause i toplhs tm of- Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")- Right mvars ->- do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w- return $ PWith fc wname lhs ws wval withs'- mkAux wname toplhs ns ns' c- = ifail $ show fc ++ ":badly formed with clause"-- addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])- addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]-- updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w- = let ns = map (keepMvar (map fst mvars) fc') ns_in- ns' = map (keepMvar (map fst mvars) fc') ns_in' in- return $ substMatches mvars $- PApp fc (PRef fc' wname)- (map pexp ns ++ pexp w : (map pexp ns'))- updateLHS n wname mvars ns_in ns_in' tm w- = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w-- keepMvar mvs fc v | v `elem` mvs = PRef fc v- | otherwise = Placeholder-- fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))- fullApp x = x-- split [] rest pre = (reverse pre, rest)- split deps ((n, ty) : rest) pre- | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)- | otherwise = split deps rest ((n, ty) : pre)- split deps [] pre = (reverse pre, [])-- abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)--data MArgTy = IA | EA | CA deriving Show--elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->- FC -> [PTerm] ->- Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()-elabClass info syn_in doc fc constraints tn ps pDocs ds- = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)- let tty = pibind ps PType- let constraint = PApp fc (PRef fc tn)- (map (pexp . PRef fc) (map fst ps))-- let syn = syn_in { using = addToUsing (using syn_in) ps }-- -- build data declaration- let mdecls = filter tydecl ds -- method declarations- let idecls = filter instdecl ds -- default superclass instance declarations- mapM_ checkDefaultSuperclassInstance idecls- let mnames = map getMName mdecls- logLvl 2 $ "Building methods " ++ show mnames- ims <- mapM (tdecl mnames) mdecls- defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)- (filter clause ds)- let (methods, imethods)- = unzip (map (\ ( x,y,z) -> (x, y)) ims)- let defaults = map (\ (x, (y, z)) -> (x,y)) defs- addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])- -- build instance constructor type- -- decorate names of functions to ensure they can't be referred- -- to elsewhere in the class declaration- let cty = impbind ps $ conbind constraints- $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)- constraint- let cons = [(emptyDocstring, [], cn, cty, fc, [])]- let ddecl = PDatadecl tn tty cons- logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)- elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl- -- for each constraint, build a top level function to chase it- logLvl 5 $ "Building functions"--- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps--- ++ using syn }- fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints- mapM_ (elabDecl EAll info) (concat fns)- -- for each method, build a top level function- fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods- mapM_ (elabDecl EAll info) (concat fns)- -- add the default definitions- mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))- addIBC (IBCClass tn)- where- nodoc (n, (_, o, t)) = (n, (o, t))- pibind [] x = x- pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)-- mdec (UN n) = SN (MethodN (UN n))- mdec (NS x n) = NS (mdec x) n- mdec x = x-- -- TODO: probably should normalise- checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)- = do when (not $ null cs) . tclift- $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))- i <- getIState- let t = PApp fc (PRef fc n) (map pexp ps)- let isConstrained = any (== t) constraints- when (not isConstrained) . tclift- $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))- return ()-- impbind [] x = x- impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)- conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)- conbind [] x = x-- getMName (PTy _ _ _ _ _ n _) = nsroot n- tdecl allmeths (PTy doc _ syn _ o n t)- = do t' <- implicit' info syn allmeths n t- logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'- return ( (n, (toExp (map fst ps) Exp t')),- (n, (doc, o, (toExp (map fst ps) Imp t'))),- (n, (syn, o, t) ) )- tdecl _ _ = ifail "Not allowed in a class declaration"-- -- Create default definitions- defdecl mtys c d@(PClauses fc opts n cs) =- case lookup n mtys of- Just (syn, o, ty) -> do let ty' = insertConstraint c ty- let ds = map (decorateid defaultdec)- [PTy emptyDocstring [] syn fc [] n ty',- PClauses fc (o ++ opts) n cs]- iLOG (show ds)- return (n, ((defaultdec n, ds!!1), ds))- _ -> ifail $ show n ++ " is not a method"- defdecl _ _ _ = ifail "Can't happen (defdecl)"-- defaultdec (UN n) = sUN ("default#" ++ str n)- defaultdec (NS n ns) = NS (defaultdec n) ns-- tydecl (PTy _ _ _ _ _ _ _) = True- tydecl _ = False- instdecl (PInstance _ _ _ _ _ _ _ _) = True- instdecl _ = False- clause (PClauses _ _ _ _) = True- clause _ = False-- -- Generate a function for chasing a dictionary constraint- cfun cn c syn all con- = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)- -- SN (ParentN cn (show con))- let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]- let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)- let lhs = PApp fc (PRef fc cfn) [pconst capp]- let rhs = PResolveTC (fileFC "HACK")- let ty = PPi constraint (sMN 0 "pc") c con- iLOG (showTmImpls ty)- iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)- i <- getIState- let conn = case con of- PRef _ n -> n- PApp _ (PRef _ n) _ -> n- let conn' = case lookupCtxtName conn (idris_classes i) of- [(n, _)] -> n- _ -> conn- addInstance False conn' cfn- addIBC (IBCInstance False conn' cfn)--- iputStrLn ("Added " ++ show (conn, cfn, ty))- return [PTy emptyDocstring [] syn fc [] cfn ty,- PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]-- -- Generate a top level function which looks up a method in a given- -- dictionary (this is inlinable, always)- tfun cn c syn all (m, (doc, o, ty))- = do let ty' = insertConstraint c ty- let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]- let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)- let margs = getMArgs ty- let anames = map (\x -> sMN x "arg") [0..]- let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)- let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)- iLOG (showTmImpls ty)- iLOG (show (m, ty', capp, margs))- iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)- return [PTy doc [] syn fc o m ty',- PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]-- getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc- getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc- getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc- getMArgs _ = []-- getMeth (m:ms) (a:as) x | x == a = PRef fc m- | otherwise = getMeth ms as x-- lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns- lhsArgs (IA : xs) ns = lhsArgs xs ns- lhsArgs (CA : xs) ns = lhsArgs xs ns- lhsArgs [] _ = []-- rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns- rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns- rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns- rhsArgs [] _ = []-- insertConstraint c (PPi p@(Imp _ _ _) n ty sc)- = PPi p n ty (insertConstraint c sc)- insertConstraint c sc = PPi constraint (sMN 0 "class") c sc-- -- make arguments explicit and don't bind class parameters- toExp ns e (PPi (Imp l s p) n ty sc)- | n `elem` ns = toExp ns e sc- | otherwise = PPi (e l s p) n ty (toExp ns e sc)- toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)- toExp ns e sc = sc--elabInstance :: ElabInfo -> SyntaxInfo ->- ElabWhat -> -- phase- FC -> [PTerm] -> -- constraints- Name -> -- the class- [PTerm] -> -- class parameters (i.e. instance)- PTerm -> -- full instance type- Maybe Name -> -- explicit name- [PDecl] -> Idris ()-elabInstance info syn what fc cs n ps t expn ds = do- i <- getIState- (n, ci) <- case lookupCtxtName n (idris_classes i) of- [c] -> return c- [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"- cs -> tclift $ tfail $ At fc - (CantResolveAlts (map fst cs))- let constraint = PApp fc (PRef fc n) (map pexp ps)- let iname = mkiname n ps expn- let emptyclass = null (class_methods ci)- when (what /= EDefns || (null ds && not emptyclass)) $ do- nty <- elabType' True info syn emptyDocstring [] fc [] iname t- -- if the instance type matches any of the instances we have already,- -- and it's not a named instance, then it's overlapping, so report an error- case expn of- Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))- (class_instances ci)- addInstance intInst n iname- Just _ -> addInstance intInst n iname- when (what /= ETypes && (not (null ds && not emptyclass))) $ do - let ips = zip (class_params ci) ps- let ns = case n of- NS n ns' -> ns'- _ -> []- -- get the implicit parameters that need passing through to the- -- where block- wparams <- mapM (\p -> case p of- PApp _ _ args -> getWParams (map getTm args)- _ -> return []) ps- let pnames = map pname (concat (nub wparams))- let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)- undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances- mapM_ (elabDecl EAll info) undefinedSuperclassInstances- let all_meths = map (nsroot . fst) (class_methods ci)- let mtys = map (\ (n, (op, t)) ->- let t_in = substMatchesShadow ips pnames t - mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))- all_meths- t' = substMatchesShadow mnamemap pnames t_in in- (decorate ns iname n,- op, coninsert cs t', t'))- (class_methods ci)- logLvl 3 (show (mtys, ips))- let ds' = insertDefaults i iname (class_defaults ci) ns ds- iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)- mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))- mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')- let wbTys = map mkTyDecl mtys- let wbVals = map (decorateid (decorate ns iname)) ds'- let wb = wbTys ++ wbVals- logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)- logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++- show (concat (nub wparams))-- -- Bring variables in instance head into scope- ist <- getIState- let headVars = nub $ mapMaybe (\p -> case p of- PRef _ n -> - case lookupTy n (tt_ctxt ist) of- [] -> Just n- _ -> Nothing- _ -> Nothing) ps--- let lhs = PRef fc iname- let lhs = PApp fc (PRef fc iname)- (map (\n -> pimp n (PRef fc n) True) headVars)- let rhs = PApp fc (PRef fc (instanceName ci))- (map (pexp . mkMethApp) mtys)-- logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars- logLvl 5 $ "Instance RHS " ++ show rhs-- let idecls = [PClauses fc [Dictionary] iname- [PClause fc iname lhs [] rhs wb]]- iLOG (show idecls)- mapM_ (elabDecl EAll info) idecls- addIBC (IBCInstance intInst n iname)-- where- intInst = case ps of- [PConstant (AType (ATInt ITNative))] -> True- _ -> False-- mkiname n' ps' expn' =- case expn' of- Nothing -> SN (sInstanceN n' (map show ps'))- Just nm -> nm-- substInstance ips pnames (PInstance syn _ cs n ps t expn ds)- = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds-- isOverlapping i (PInstance syn _ _ n ps t expn _)- = case lookupCtxtName n (idris_classes i) of- [(n, ci)] -> let iname = (mkiname n ps expn) in- case lookupTy iname (tt_ctxt i) of- [] -> elabFindOverlapping i ci iname syn t- (_:_) -> return True- _ -> return False -- couldn't find class, just let elabInstance fail later-- -- TODO: largely based upon elabType' - should try to abstract- elabFindOverlapping i ci iname syn t- = do ty' <- addUsingConstraints syn fc t- -- TODO think: something more in info?- ty' <- implicit info syn iname ty'- let ty = addImpl i ty'- ctxt <- getContext- ((tyT, _, _), _) <-- tclift $ elaborate ctxt iname (TType (UVal 0)) []- (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))- ctxt <- getContext- (cty, _) <- recheckC fc [] tyT- let nty = normalise ctxt [] cty- return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)-- findOverlapping i t n- | take 2 (show n) == "@@" = Nothing- | otherwise- = case lookupTy n (tt_ctxt i) of- [t'] -> let tret = getRetType t- tret' = getRetType (delab i t') in- case matchClause i tret' tret of- Right ms -> Just tret'- Left _ -> case matchClause i tret tret' of- Right ms -> Just tret'- Left _ -> Nothing- _ -> Nothing- overlapping t' = tclift $ tfail (At fc (Msg $- "Overlapping instance: " ++ show t' ++ " already defined"))- getRetType (PPi _ _ _ sc) = getRetType sc- getRetType t = t-- mkMethApp (n, _, _, ty)- = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))- lamBind i (PPi (Constraint _ _) _ _ sc) sc'- = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')- lamBind i (PPi _ n ty sc) sc'- = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')- lamBind i _ sc = sc- methArgs i (PPi (Imp _ _ _) n ty sc)- = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc- methArgs i (PPi (Exp _ _ _) n ty sc)- = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc- methArgs i (PPi (Constraint _ _) n ty sc)- = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc- methArgs i _ = []-- papp fc f [] = f- papp fc f as = PApp fc f as-- getWParams [] = return []- getWParams (p : ps)- | PRef _ n <- p- = do ps' <- getWParams ps- ctxt <- getContext- case lookupP n ctxt of- [] -> return (pimp n (PRef fc n) True : ps')- _ -> return ps'- getWParams (_ : ps) = getWParams ps-- decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns- decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns-- mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t-- conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)- conbind [] x = x-- coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)- coninsert cs sc = conbind cs sc-- insertDefaults :: IState -> Name ->- [(Name, (Name, PDecl))] -> [T.Text] ->- [PDecl] -> [PDecl]- insertDefaults i iname [] ns ds = ds- insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds- = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)-- insertDef i meth def clauses ns iname decls- | null $ filter (clauseFor meth iname ns) decls- = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in- -- trace (show newd) $- decls ++ [newd]- | otherwise = decls-- warnMissing decls ns iname meth- | null $ filter (clauseFor meth iname ns) decls- = iWarn fc . text $ "method " ++ show meth ++ " not defined"- | otherwise = return ()-- checkInClass ns meth- | not (null (filter (eqRoot meth) ns)) = return ()- | otherwise = tclift $ tfail (At fc (Msg $- show meth ++ " not a method of class " ++ show n))-- eqRoot x y = nsroot x == nsroot y-- clauseFor m iname ns (PClauses _ _ m' _)- = decorate ns iname m == decorate ns iname m'- clauseFor m iname ns _ = False--{- This won't work yet. Can it ever, in this form?-- cfun cn c syn all con- = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)- let mnames = take (length all) $ map (\x -> MN x "meth") [0..]- let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)- let lhs = PApp fc (PRef fc cfn) [pconst capp]- let rhs = PResolveTC (FC "HACK" 0)- let ty = PPi constraint (MN 0 "pc") c con- iLOG (showImp True ty)- iLOG (showImp True lhs ++ " = " ++ showImp True rhs)- i <- getIState- let conn = case con of- PRef _ n -> n- PApp _ (PRef _ n) _ -> n- let conn' = case lookupCtxtName Nothing conn (idris_classes i) of- [(n, _)] -> n- _ -> conn- addInstance False conn' cfn- addIBC (IBCInstance False conn' cfn)- iputStrLn ("Added " ++ show (conn, cfn, ty) ++ "\n" ++ show (lhs, rhs))- return [PTy "" syn fc [] cfn ty,- PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]--}--decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t-decorateid decorate (PClauses f o n cs)- = PClauses f o (decorate n) (map dc cs)- where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds- dc (PWith fc n t as w ds)- = PWith fc (decorate n) (dappname t) as w- (map (decorateid decorate) ds)- dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as- dappname t = t----- if 't' is a type class application, assume its arguments are injective-pbinds :: IState -> Term -> ElabD ()-pbinds i (Bind n (PVar t) sc) - = do attack; patbind n- case unApply t of- (P _ c _, args) -> case lookupCtxt c (idris_classes i) of- [] -> return ()- _ -> -- type class, set as injective- mapM_ setinjArg args- _ -> return ()- pbinds i sc- where setinjArg (P _ n _) = setinj n- setinjArg _ = return ()-pbinds i tm = return ()--pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)-pbty _ tm = tm--getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc-getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc-getPBtys _ = []--psolve (Bind n (PVar t) sc) = do solve; psolve sc-psolve tm = return ()--pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc-pvars ist _ = []--data ElabWhat = ETypes | EDefns | EAll- deriving (Show, Eq)--elabDecls :: ElabInfo -> [PDecl] -> Idris ()-elabDecls info ds = do mapM_ (elabDecl EAll info) ds--- mapM_ (elabDecl EDefns info) ds--elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()-elabDecl what info d- = idrisCatch (withErrorReflection $ elabDecl' what info d) (setAndReport)--elabDecl' _ info (PFix _ _ _)- = return () -- nothing to elaborate-elabDecl' _ info (PSyntax _ p)- = return () -- nothing to elaborate-elabDecl' what info (PTy doc argdocs s f o n ty)- | what /= EDefns- = do iLOG $ "Elaborating type decl " ++ show n ++ show o- elabType info s doc argdocs f o n ty- return ()-elabDecl' what info (PPostulate doc s f o n ty)- | what /= EDefns- = do iLOG $ "Elaborating postulate " ++ show n ++ show o- elabPostulate info s doc f o n ty-elabDecl' what info (PData doc argDocs s f co d)- | what /= ETypes- = do iLOG $ "Elaborating " ++ show (d_name d)- elabData info s doc argDocs f co d- | otherwise- = do iLOG $ "Elaborating [type of] " ++ show (d_name d)- elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))-elabDecl' what info d@(PClauses f o n ps)- | what /= ETypes- = do iLOG $ "Elaborating clause " ++ show n- i <- getIState -- get the type options too- let o' = case lookupCtxt n (idris_flags i) of- [fs] -> fs- [] -> []- elabClauses info f (o ++ o') n ps-elabDecl' what info (PMutual f ps)- = do case ps of- [p] -> elabDecl what info p- _ -> do mapM_ (elabDecl ETypes info) ps- mapM_ (elabDecl EDefns info) ps- -- record mutually defined data definitions- let datans = concatMap declared (filter isDataDecl ps)- mapM_ (setMutData datans) datans- iLOG $ "Rechecking for positivity " ++ show datans- mapM_ (\x -> do setTotality x Unchecked) datans- -- Do totality checking after entire mutual block- i <- get- mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n- updateContext (simplifyCasedef n $ getErasureInfo i))- (map snd (idris_totcheck i))- mapM_ buildSCG (idris_totcheck i)- mapM_ checkDeclTotality (idris_totcheck i)- clear_totcheck- where isDataDecl (PData _ _ _ _ _ _) = True- isDataDecl _ = False-- setMutData ns n - = do i <- getIState- case lookupCtxt n (idris_datatypes i) of- [x] -> do let x' = x { mutual_types = ns }- putIState $ i { idris_datatypes - = addDef n x' (idris_datatypes i) }- _ -> return ()--elabDecl' what info (PParams f ns ps)- = do i <- getIState- iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++- show (concatMap tldeclared ps)- let nblock = pblock i- mapM_ (elabDecl' what info) nblock- where- pinfo = let ds = concatMap tldeclared ps- newps = params info ++ ns- dsParams = map (\n -> (n, map fst newps)) ds- newb = addAlist dsParams (inblock info) in- info { params = newps,- inblock = newb }- pblock i = map (expandParamsD False i id ns- (concatMap tldeclared ps)) ps--elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps- where- ninfo = case namespace info of- Nothing -> info { namespace = Just [n] }- Just ns -> info { namespace = Just (n:ns) }-elabDecl' what info (PClass doc s f cs n ps pdocs ds)- | what /= EDefns- = do iLOG $ "Elaborating class " ++ show n- elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds-elabDecl' what info (PInstance s f cs n ps t expn ds)- = do iLOG $ "Elaborating instance " ++ show n- elabInstance info s what f cs n ps t expn ds-elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)- | what /= ETypes- = do iLOG $ "Elaborating record " ++ show tyn- elabRecord info s doc f tyn ty opts cdoc cn cty- | otherwise- = do iLOG $ "Elaborating [type of] " ++ show tyn- elabData info s doc [] f [] (PLaterdecl tyn ty)-elabDecl' _ info (PDSL n dsl)- = do i <- getIState- putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })- addIBC (IBCDSL n)-elabDecl' what info (PDirective i)- | what /= EDefns = i-elabDecl' what info (PProvider syn fc provWhat n)- | what /= EDefns- = do iLOG $ "Elaborating type provider " ++ show n- elabProvider info syn fc provWhat n-elabDecl' what info (PTransform fc safety old new)- = elabTransform info fc safety old new-elabDecl' _ _ _ = return () -- skipped this time--elabCaseBlock info opts d@(PClauses f o n ps)- = do addIBC (IBCDef n)- logLvl 5 $ "CASE BLOCK: " ++ show (n, d)- let opts' = nub (o ++ opts)- -- propagate totality assertion to the new definitions- when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]- elabDecl' EAll info (PClauses f opts' n ps )---- elabDecl' info (PImport i) = loadModule i---- Check that the result of type checking matches what the programmer wrote--- (i.e. - if we inferred any arguments that the user provided, make sure--- they are the same!)--checkInferred :: FC -> PTerm -> PTerm -> Idris ()-checkInferred fc inf user =- do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++- showTmImpls user- logLvl 10 $ "Checking match"- i <- getIState- tclift $ case matchClause' True i user inf of- _ -> return ()--- Left (x, y) -> tfail $ At fc--- (Msg $ "The type-checked term and given term do not match: "--- ++ show x ++ " and " ++ show y)- logLvl 10 $ "Checked match"--- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)---- Return whether inferred term is different from given term--- (as above, but return a Bool)--inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool-inferredDiff fc inf user =- do i <- getIState- logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++- showTmImpls user- tclift $ case matchClause' True i user inf of- Right vs -> return False- Left (x, y) -> return True---- | Check a PTerm against documentation and ensure that every documented--- argument actually exists. This must be run _after_ implicits have been--- found, or it will give spurious errors.-checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()-checkDocs fc args tm = cd (Map.fromList args) tm- where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc- cd as _ | Map.null as = return ()- | otherwise = ierror . At fc . Msg $- "There is documentation for argument(s) "- ++ (concat . intersperse ", " . map show . Map.keys) as- ++ " but they were not found."+import Idris.Elab.Utils+import Idris.Elab.Type+import Idris.Elab.Clause+import Idris.Elab.Data+import Idris.Elab.Record+import Idris.Elab.Class+import Idris.Elab.Instance+import Idris.Elab.Provider+import Idris.Elab.Value++import Idris.Core.TT+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.Typecheck+import Idris.Core.CaseTree++import Idris.Docstrings++import Prelude hiding (id, (.))+import Control.Category++import Control.Applicative hiding (Const)+import Control.DeepSeq+import Control.Monad+import Control.Monad.State.Strict as State+import Data.List+import Data.Maybe+import Debug.Trace++import qualified Data.Map as Map+import qualified Data.Set as S+import qualified Data.Text as T+import Data.Char(isLetter, toLower)+import Data.List.Split (splitOn)++import Util.Pretty(pretty, text)+++-- Top level elaborator info, supporting recursive elaboration+recinfo :: ElabInfo+recinfo = EInfo [] emptyContext id Nothing elabDecl'++-- | Elaborate primitives+elabPrims :: Idris ()+elabPrims = do mapM_ (elabDecl' EAll recinfo)+ (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)+ (zip4+ [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]+ [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]+ [[], [], [], pairParamDoc, eqParamDoc]))+ addNameHint eqTy (sUN "prf")+ elabDecl' EAll recinfo elimDecl+ mapM_ elabPrim primitives+ -- Special case prim__believe_me because it doesn't work on just constants+ elabBelieveMe+ -- Finally, syntactic equality+ elabSynEq+ where elabPrim :: Prim -> Idris ()+ elabPrim (Prim n ty i def sc tot)+ = do updateContext (addOperator n ty i (valuePrim def))+ setTotality n tot+ i <- getIState+ putIState i { idris_scprims = (n, sc) : idris_scprims i }++ valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value+ valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)++ getConst (VConstant c) = Just c+ getConst _ = Nothing+++ p_believeMe [_,_,x] = Just x+ p_believeMe _ = Nothing+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))+ (Bind (sUN "b") (Pi (TType (UVar (-2))))+ (Bind (sUN "x") (Pi (V 1)) (V 1)))+ elabBelieveMe+ = do let prim__believe_me = sUN "prim__believe_me"+ updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)+ setTotality prim__believe_me (Partial NotCovering)+ i <- getIState+ putIState i {+ idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i+ }++ p_synEq [t,_,x,y]+ | x == y = Just (VApp (VApp vnJust VErased)+ (VApp (VApp vnRefl t) x))+ | otherwise = Just (VApp vnNothing VErased)+ p_synEq args = Nothing++ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased+ vnRefl = VP (DCon 0 2) eqCon VErased++ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))+ (Bind (sUN "b") (Pi (TType (UVar (-3))))+ (Bind (sUN "x") (Pi (V 1))+ (Bind (sUN "y") (Pi (V 1))+ (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)+ [V 3, V 2, V 1, V 0]]))))+ elabSynEq+ = do let synEq = sUN "prim__syntactic_eq"++ updateContext (addOperator synEq synEqTy 4 p_synEq)+ setTotality synEq (Total [])+ i <- getIState+ putIState i {+ idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i+ }++elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()+elabTransform info fc safe lhs_in rhs_in+ = do ctxt <- getContext+ i <- getIState+ let lhs = addImplPat i lhs_in+ ((lhs', dlhs, []), _) <-+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []+ (erun fc (buildTC i info ELHS [] (sUN "transform")+ (infTerm lhs)))+ let lhs_tm = orderPats (getInferTerm lhs')+ let lhs_ty = getInferType lhs'+ let newargs = pvars i lhs_tm++ (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm+ logLvl 3 ("Transform LHS " ++ show clhs_tm)+ let rhs = addImplBound i (map fst newargs) rhs_in+ ((rhs', defer), _) <-+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []+ (do pbinds i lhs_tm+ setNextName+ erun fc (build i info ERHS [] (sUN "transform") rhs)+ erun fc $ psolve lhs_tm+ tt <- get_term+ return (runState (collectDeferred Nothing tt) []))+ (crhs_tm, crhs_ty) <- recheckC fc [] rhs'+ logLvl 3 ("Transform RHS " ++ show crhs_tm)+ when safe $ case converts ctxt [] clhs_tm crhs_tm of+ OK _ -> return ()+ Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))+ addTrans (clhs_tm, crhs_tm)+ addIBC (IBCTrans (clhs_tm, crhs_tm))++elabDecls :: ElabInfo -> [PDecl] -> Idris ()+elabDecls info ds = do mapM_ (elabDecl EAll info) ds++elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()+elabDecl what info d+ = let info' = info { rec_elabDecl = elabDecl' } in+ idrisCatch (withErrorReflection $ elabDecl' what info' d) (setAndReport)++elabDecl' _ info (PFix _ _ _)+ = return () -- nothing to elaborate+elabDecl' _ info (PSyntax _ p)+ = return () -- nothing to elaborate+elabDecl' what info (PTy doc argdocs s f o n ty)+ | what /= EDefns+ = do iLOG $ "Elaborating type decl " ++ show n ++ show o+ elabType info s doc argdocs f o n ty+ return ()+elabDecl' what info (PPostulate doc s f o n ty)+ | what /= EDefns+ = do iLOG $ "Elaborating postulate " ++ show n ++ show o+ elabPostulate info s doc f o n ty+elabDecl' what info (PData doc argDocs s f co d)+ | what /= ETypes+ = do iLOG $ "Elaborating " ++ show (d_name d)+ elabData info s doc argDocs f co d+ | otherwise+ = do iLOG $ "Elaborating [type of] " ++ show (d_name d)+ elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))+elabDecl' what info d@(PClauses f o n ps)+ | what /= ETypes+ = do iLOG $ "Elaborating clause " ++ show n+ i <- getIState -- get the type options too+ let o' = case lookupCtxt n (idris_flags i) of+ [fs] -> fs+ [] -> []+ elabClauses info f (o ++ o') n ps+elabDecl' what info (PMutual f ps)+ = do case ps of+ [p] -> elabDecl what info p+ _ -> do mapM_ (elabDecl ETypes info) ps+ mapM_ (elabDecl EDefns info) ps+ -- record mutually defined data definitions+ let datans = concatMap declared (filter isDataDecl ps)+ mapM_ (setMutData datans) datans+ iLOG $ "Rechecking for positivity " ++ show datans+ mapM_ (\x -> do setTotality x Unchecked) datans+ -- Do totality checking after entire mutual block+ i <- get+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n+ updateContext (simplifyCasedef n $ getErasureInfo i))+ (map snd (idris_totcheck i))+ mapM_ buildSCG (idris_totcheck i)+ mapM_ checkDeclTotality (idris_totcheck i)+ clear_totcheck+ where isDataDecl (PData _ _ _ _ _ _) = True+ isDataDecl _ = False++ setMutData ns n + = do i <- getIState+ case lookupCtxt n (idris_datatypes i) of+ [x] -> do let x' = x { mutual_types = ns }+ putIState $ i { idris_datatypes + = addDef n x' (idris_datatypes i) }+ _ -> return ()++elabDecl' what info (PParams f ns ps)+ = do i <- getIState+ iLOG $ "Expanding params block with " ++ show ns ++ " decls " +++ show (concatMap tldeclared ps)+ let nblock = pblock i+ mapM_ (elabDecl' what info) nblock+ where+ pinfo = let ds = concatMap tldeclared ps+ newps = params info ++ ns+ dsParams = map (\n -> (n, map fst newps)) ds+ newb = addAlist dsParams (inblock info) in+ info { params = newps,+ inblock = newb }+ pblock i = map (expandParamsD False i id ns+ (concatMap tldeclared ps)) ps++elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps+ where+ ninfo = case namespace info of+ Nothing -> info { namespace = Just [n] }+ Just ns -> info { namespace = Just (n:ns) }+elabDecl' what info (PClass doc s f cs n ps pdocs ds)+ | what /= EDefns+ = do iLOG $ "Elaborating class " ++ show n+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds+elabDecl' what info (PInstance s f cs n ps t expn ds)+ = do iLOG $ "Elaborating instance " ++ show n+ elabInstance info s what f cs n ps t expn ds+elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)+ | what /= ETypes+ = do iLOG $ "Elaborating record " ++ show tyn+ elabRecord info s doc f tyn ty opts cdoc cn cty+ | otherwise+ = do iLOG $ "Elaborating [type of] " ++ show tyn+ elabData info s doc [] f [] (PLaterdecl tyn ty)+elabDecl' _ info (PDSL n dsl)+ = do i <- getIState+ putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })+ addIBC (IBCDSL n)+elabDecl' what info (PDirective i)+ | what /= EDefns = i+elabDecl' what info (PProvider syn fc provWhat n)+ | what /= EDefns+ = do iLOG $ "Elaborating type provider " ++ show n+ elabProvider info syn fc provWhat n+elabDecl' what info (PTransform fc safety old new)+ = elabTransform info fc safety old new+elabDecl' _ _ _ = return () -- skipped this time+
src/Idris/ElabTerm.hs view
@@ -26,6 +26,8 @@ import Data.Maybe (mapMaybe, fromMaybe) import qualified Data.Set as S import qualified Data.Text as T+import Data.Vector.Unboxed (Vector)+import qualified Data.Vector.Unboxed as V import Debug.Trace @@ -57,7 +59,7 @@ mapM_ (\n -> when (n `elem` hs) $ do focus n g <- goal- try (resolveTC 7 g fn ist)+ try (resolveTC True 7 g fn ist) (movelast n)) ivs ivs <- get_instances hs <- get_holes@@ -65,7 +67,7 @@ mapM_ (\n -> when (n `elem` hs) $ do focus n g <- goal- resolveTC 7 g fn ist) ivs+ resolveTC True 7 g fn ist) ivs tm <- get_term ctxt <- get_context probs <- get_probs@@ -243,7 +245,7 @@ (elab' ina (PRef fc unitTy)) elab' ina (PFalse fc) = elab' ina (PRef fc falseTy) elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes- = do g <- goal; resolveTC 5 g fn ist+ = do g <- goal; resolveTC False 5 g fn ist elab' ina (PResolveTC fc) = do c <- getNameFrom (sMN 0 "class") instanceArg c@@ -405,18 +407,18 @@ focus valn elabE (True, a, True, qq) val ivs' <- get_instances+ env <- get_env+ elabE (True, a, inty, qq) sc when (not pattern) $ mapM_ (\n -> do focus n g <- goal hs <- get_holes if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g) -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))- then try (resolveTC 7 g fn ist)+ then try (resolveTC True 7 g fn ist) (movelast n) else movelast n) (ivs' \\ ivs)- env <- get_env- elabE (True, a, inty, qq) sc -- HACK: If the name leaks into its type, it may leak out of -- scope outside, so substitute in the outer scope. expandLet n (case lookup n env of@@ -543,7 +545,7 @@ hs <- get_holes if all (\n -> not (n `elem` hs)) (freeNames g) -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))- then try (resolveTC 7 g fn ist)+ then try (resolveTC False 7 g fn ist) (movelast n) else movelast n) (ivs' \\ ivs)@@ -1004,12 +1006,12 @@ proofSearch rec prv depth (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist -resolveTC :: Int -> Term -> Name -> IState -> ElabD ()+resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD () resolveTC = resTC' [] -resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"-resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True-resTC' tcs depth topg fn ist+resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"+resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True+resTC' tcs defaultOn depth topg fn ist = do hnf_compute g <- goal ptm <- get_term@@ -1040,7 +1042,7 @@ numclass = sNS (sUN "Num") ["Classes","Prelude"] - needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn = do focus a fill (RConstant (AType (ATInt ITBig))) -- default Integer solve@@ -1085,7 +1087,7 @@ let got = fst (unApply t) let depth' = if tc' `elem` tcs then depth - 1 else depth - resTC' (got : tcs) depth' topg fn ist)+ resTC' (got : tcs) defaultOn depth' topg fn ist) (filter (\ (x, y) -> not x) (zip (map fst imps) args)) -- if there's any arguments left, we've failed to resolve hs <- get_holes@@ -1359,6 +1361,8 @@ _ -> fail "Wrong goal type" runT ProofState = do g <- goal return ()+ runT Skip = return ()+ runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "") runT x = fail $ "Not implemented " ++ show x runReflected t = do t' <- reify ist t@@ -1376,6 +1380,7 @@ reify _ (P _ n _) | n == reflm "Instance" = return TCInstance reify _ (P _ n _) | n == reflm "Solve" = return Solve reify _ (P _ n _) | n == reflm "Compute" = return Compute+reify _ (P _ n _) | n == reflm "Skip" = return Skip reify ist t@(App _ _) | (P _ f _, args) <- unApply t = reifyApp ist f args reify _ t = fail ("Unknown tactic " ++ show t)@@ -1416,6 +1421,15 @@ tt'' <- reifyTT tt' t'' <- reifyTT t' return $ LetTacTy n' (delab ist tt'') (delab ist t'')+reifyApp ist t [errs]+ | t == reflm "Fail" = case unList errs of+ Nothing -> fail "Failed to reify errors"+ Just errs' ->+ let parts = mapM reifyReportPart errs' in+ case parts of+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err+ Right errs'' ->+ return $ TFail errs'' reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen -- | Reify terms from their reflected representation@@ -1547,15 +1561,7 @@ reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args)) reifyTTConst :: Term -> ElabD Const-reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))-reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))-reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)-reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar)) reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType-reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))-reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))-reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32)))-reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64))) reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot@@ -1564,6 +1570,8 @@ reifyTTConst t = fail ("Unknown reflection constant: " ++ show t) reifyTTConstApp :: Name -> Term -> ElabD Const+reifyTTConstApp f aty+ | f == reflm "AType" = fmap AType (reifyArithTy aty) reifyTTConstApp f (Constant c@(I _)) | f == reflm "I" = return $ c reifyTTConstApp f (Constant c@(BI _))@@ -1584,6 +1592,26 @@ | f == reflm "B64" = return $ c reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg)) +reifyArithTy :: Term -> ElabD ArithTy+reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)+reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat+reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)++reifyNativeTy :: Term -> ElabD NativeTy+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8+reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x++reifyIntTy :: Term -> ElabD IntTy+reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)+reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative+reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig+reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar+reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)+ (reifyNativeTy nt)+ reifyTTUExp :: Term -> ElabD UExp reifyTTUExp t@(App _ _) = case unApply t of@@ -1778,8 +1806,9 @@ reflectName (NErased) = Var (reflm "NErased") reflectName n = Var (reflm "NErased") -- special name, not yet implemented --- | Elaborate a name to a pattern. This means that NS and UN will be intact,--- while all others become _+-- | Elaborate a name to a pattern. This means that NS and UN will be intact.+-- MNs corresponding to will care about the string but not the number. All+-- others become _. reflectNameQuotePattern :: Name -> ElabD () reflectNameQuotePattern n@(UN s) = do fill $ reflectName n@@ -1787,6 +1816,12 @@ reflectNameQuotePattern n@(NS _ _) = do fill $ reflectName n solve+reflectNameQuotePattern (MN _ n)+ = do i <- getNameFrom (sMN 0 "mnCounter")+ claim i (RConstant (AType (ATInt ITNative)))+ movelast i+ fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]+ solve reflectNameQuotePattern _ -- for all other names, match any = do nameHole <- getNameFrom (sMN 0 "name") claim nameHole (Var (reflm "TTName"))@@ -1817,29 +1852,46 @@ reflectBinderQuote unq (PVTy t) = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t] +mkList :: Raw -> [Raw] -> Raw+mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty+mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)+ x)+ (mkList ty xs)+ reflectConstant :: Const -> Raw reflectConstant c@(I _) = reflCall "I" [RConstant c] reflectConstant c@(BI _) = reflCall "BI" [RConstant c] reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c] reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c] reflectConstant c@(Str _) = reflCall "Str" [RConstant c]-reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")-reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")-reflectConstant (AType ATFloat) = Var (reflm "FlType")-reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")-reflectConstant (StrType) = Var (reflm "StrType") reflectConstant c@(B8 _) = reflCall "B8" [RConstant c] reflectConstant c@(B16 _) = reflCall "B16" [RConstant c] reflectConstant c@(B32 _) = reflCall "B32" [RConstant c] reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]-reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")-reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")-reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")-reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")-reflectConstant (PtrType) = Var (reflm "PtrType")-reflectConstant (VoidType) = Var (reflm "VoidType")-reflectConstant (Forgot) = Var (reflm "Forgot")+reflectConstant (B8V ws) = reflCall "B8V" [mkList (Var (sUN "Bits8")) . map (RConstant . B8) . V.toList $ ws]+reflectConstant (B16V ws) = reflCall "B8V" [mkList (Var (sUN "Bits16")) . map (RConstant . B16) . V.toList $ ws]+reflectConstant (B32V ws) = reflCall "B8V" [mkList (Var (sUN "Bits32")) . map (RConstant . B32) . V.toList $ ws]+reflectConstant (B64V ws) = reflCall "B8V" [mkList (Var (sUN "Bits64")) . map (RConstant . B64) . V.toList $ ws]+reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]+reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]+reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]+reflectConstant StrType = Var (reflm "StrType")+reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]+reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]+reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]+reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]+reflectConstant (AType (ATInt (ITVec IT8 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT8"), RConstant (I c)]]]+reflectConstant (AType (ATInt (ITVec IT16 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT16"), RConstant (I c)]]]+reflectConstant (AType (ATInt (ITVec IT32 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT32"), RConstant (I c)]]]+reflectConstant (AType (ATInt (ITVec IT64 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT64"), RConstant (I c)]]]+reflectConstant PtrType = Var (reflm "PtrType")+reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")+reflectConstant BufferType = Var (reflm "BufferType")+reflectConstant VoidType = Var (reflm "VoidType")+reflectConstant Forgot = Var (reflm "Forgot") + reflectUExp :: UExp -> Raw reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)] reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]@@ -2042,10 +2094,10 @@ -- representation. Not in Idris or ElabD monads because it should be usable -- from either. reifyReportPart :: Term -> Either Err ErrorReportPart-reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =+reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" = Right (TextPart msg) reifyReportPart (App (P (DCon _ _) n _) ttn)- | n == reflErrName "NamePart" =+ | n == reflm "NamePart" = case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of Error e -> Left . InternalMsg $ "could not reify name term " ++@@ -2053,7 +2105,7 @@ " when reflecting an error:" ++ show e OK (n', _)-> Right $ NamePart n' reifyReportPart (App (P (DCon _ _) n _) tm)- | n == reflErrName "TermPart" =+ | n == reflm "TermPart" = case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of Error e -> Left . InternalMsg $ "could not reify reflected term " ++@@ -2061,7 +2113,7 @@ " when reflecting an error:" ++ show e OK (tm', _) -> Right $ TermPart tm' reifyReportPart (App (P (DCon _ _) n _) tm)- | n == reflErrName "SubReport" =+ | n == reflm "SubReport" = case unList tm of Just xs -> do subParts <- mapM reifyReportPart xs Right (SubReport subParts)
src/Idris/Interactive.hs view
@@ -18,6 +18,8 @@ import Idris.Output import Idris.IdeSlave hiding (IdeSlaveCommand(..)) +import Idris.Elab.Value+ import Util.Pretty import Util.System @@ -174,8 +176,8 @@ (ProofSearch rec False depth t hints)] let def = PClause fc mn (PRef fc mn) [] (body top) [] newmv <- idrisCatch- (do elabDecl' EAll toplevel (PClauses fc [] mn [def])- (tm, ty) <- elabVal toplevel ERHS (PRef fc mn)+ (do elabDecl' EAll recinfo (PClauses fc [] mn [def])+ (tm, ty) <- elabVal recinfo ERHS (PRef fc mn) ctxt <- getContext i <- getIState return . flip displayS "" . renderPretty 1.0 80 $
src/Idris/ParseExpr.hs view
@@ -320,7 +320,7 @@ <|> idiom syn <|> listExpr syn <|> alt syn- <|> do lchar '!'+ <|> do reservedOp "!" s <- simpleExpr syn fc <- getFC return (PAppBind fc s [])@@ -522,7 +522,7 @@ return (dslify i ap) <|> do f <- simpleExpr syn- (do try $ symbol "<=="+ (do try $ reservedOp "<==" fc <- getFC ff <- fnName return (PLet (sMN 0 "match")@@ -1278,6 +1278,10 @@ <|> do reserved "undo"; return Undo <|> do reserved "qed"; return Qed <|> do reserved "abandon"; return Abandon+ <|> do reserved "skip"; return Skip+ <|> do reserved "fail"+ msg <- stringLiteral+ return $ TFail [Idris.Core.TT.TextPart msg] <|> do lchar ':'; ( (do reserved "q"; return Abandon) <|> (do (reserved "e" <|> reserved "eval");
src/Idris/Prover.hs view
@@ -6,6 +6,9 @@ import Idris.Core.CaseTree import Idris.Core.Typecheck +import Idris.Elab.Utils+import Idris.Elab.Value+ import Idris.AbsSyntax import Idris.AbsSyntaxTree import Idris.Delaborate@@ -272,7 +275,7 @@ let OK env = envAtFocus (proof e) ctxt' = envCtxt env ctxt putIState ist { tt_ctxt = ctxt' }- (tm, ty) <- elabVal toplevel ERHS t+ (tm, ty) <- elabVal recinfo ERHS t let ppo = ppOptionIst ist ty' = normaliseC ctxt [] ty h = idris_outh ist@@ -296,7 +299,7 @@ ist' = ist { tt_ctxt = ctxt' } bnd = map (\x -> (fst x, False)) env putIState ist'- (tm, ty) <- elabVal toplevel ERHS t+ (tm, ty) <- elabVal recinfo ERHS t let tm' = force (normaliseAll ctxt' env tm) ty' = force (normaliseAll ctxt' env ty) ppo = ppOption (idris_options ist')
src/Idris/REPL.hs view
@@ -34,6 +34,11 @@ import Idris.WhoCalls import Idris.TypeSearch (searchByType) +import Idris.Elab.Type+import Idris.Elab.Clause+import Idris.Elab.Data+import Idris.Elab.Value+ import Version_idris (gitHash) import Util.System import Util.DynamicLinker@@ -653,7 +658,7 @@ return () process h fn (Eval t) = withErrorReflection $ do logLvl 5 $ show t- (tm, ty) <- elabVal toplevel ERHS t+ (tm, ty) <- elabVal recinfo ERHS t ctxt <- getContext let tm' = force (normaliseAll ctxt [] tm) let ty' = force (normaliseAll ctxt [] ty)@@ -679,17 +684,17 @@ getClauseName (PWith fc name whole with rhs whereBlock) = name defineName :: [PDecl] -> Idris () defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do - elabDecl EAll toplevel tyDecl- elabClauses toplevel fc opts name (concatMap getClauses decls)+ elabDecl EAll recinfo tyDecl+ elabClauses recinfo fc opts name (concatMap getClauses decls) defineName [PClauses fc opts _ [clause]] = do let pterm = getRHS clause- (tm,ty) <- elabVal toplevel ERHS pterm+ (tm,ty) <- elabVal recinfo ERHS pterm ctxt <- getContext let tm' = force (normaliseAll ctxt [] tm) let ty' = force (normaliseAll ctxt [] ty) updateContext (addCtxtDef (getClauseName clause) (Function ty' tm')) defineName [PData doc argdocs syn fc opts decl] = do- elabData toplevel syn doc argdocs fc opts decl+ elabData recinfo syn doc argdocs fc opts decl getClauses (PClauses fc opts name clauses) = clauses getClauses _ = [] getRHS :: PClause -> PTerm@@ -701,7 +706,7 @@ process h fn (ExecVal t) = do ctxt <- getContext ist <- getIState- (tm, ty) <- elabVal toplevel ERHS t+ (tm, ty) <- elabVal recinfo ERHS t -- let tm' = normaliseAll ctxt [] tm let ty' = normaliseAll ctxt [] ty res <- execute tm@@ -745,7 +750,7 @@ process h fn (Check t)- = do (tm, ty) <- elabVal toplevel ERHS t+ = do (tm, ty) <- elabVal recinfo ERHS t ctxt <- getContext ist <- getIState let ppo = ppOptionIst ist@@ -840,7 +845,7 @@ process h fn (DoProofSearch updatefile rec l n hints) = doProofSearch h fn updatefile rec l n hints Nothing process h fn (Spec t)- = do (tm, ty) <- elabVal toplevel ERHS t+ = do (tm, ty) <- elabVal recinfo ERHS t ctxt <- getContext ist <- getIState let tm' = simplify ctxt [] {- (idris_statics ist) -} tm@@ -919,13 +924,13 @@ warnTotality process h fn (HNF t)- = do (tm, ty) <- elabVal toplevel ERHS t+ = do (tm, ty) <- elabVal recinfo ERHS t ctxt <- getContext ist <- getIState let tm' = hnf ctxt [] tm iPrintResult (show (delab ist tm')) process h fn (TestInline t)- = do (tm, ty) <- elabVal toplevel ERHS t+ = do (tm, ty) <- elabVal recinfo ERHS t ctxt <- getContext ist <- getIState let tm' = inlineTerm ist tm@@ -934,7 +939,7 @@ process h fn Execute = idrisCatch (do ist <- getIState- (m, _) <- elabVal toplevel ERHS+ (m, _) <- elabVal recinfo ERHS (PApp fc (PRef fc (sUN "run__IO")) [pexp $ PRef fc (sNS (sUN "main") ["Main"])])@@ -950,7 +955,7 @@ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e) where fc = fileFC "main" process h fn (Compile codegen f)- = do (m, _) <- elabVal toplevel ERHS+ = do (m, _) <- elabVal recinfo ERHS (PApp fc (PRef fc (sUN "run__IO")) [pexp $ PRef fc (sNS (sUN "main") ["Main"])]) compile codegen f m@@ -958,7 +963,7 @@ process h fn (LogLvl i) = setLogLevel i -- Elaborate as if LHS of a pattern (debug command) process h fn (Pattelab t)- = do (tm, ty) <- elabVal toplevel ELHS t+ = do (tm, ty) <- elabVal recinfo ELHS t iPrintResult $ show tm ++ "\n\n : " ++ show ty process h fn (Missing n)@@ -1376,7 +1381,7 @@ Failure err -> do iputStrLn $ show (fixColour c err) runIO $ exitWith (ExitFailure 1) Success term -> do ctxt <- getContext- (tm, _) <- elabVal toplevel ERHS term+ (tm, _) <- elabVal recinfo ERHS term res <- execute tm runIO $ exitWith ExitSuccess
src/Idris/REPLParser.hs view
@@ -27,104 +27,104 @@ parseCmd i inputname = P.runparser pCmd i inputname cmd :: [String] -> P.IdrisParser ()-cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)+cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)) where docmd [] = fail "No such command"- docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs+ docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs pCmd :: P.IdrisParser Command-pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)- <|> try (do cmd ["h", "?", "help"]; eof; return Help)- <|> try (do cmd ["w", "warranty"]; eof; return Warranty)- <|> try (do cmd ["r", "reload"]; eof; return Reload)- <|> try (do cmd ["module"]; f <- P.identifier; eof;- return (ModImport (toPath f)))- <|> try (do cmd ["e", "edit"]; eof; return Edit)- <|> try (do cmd ["exec", "execute"]; eof; return Execute)- <|> try (do cmd ["c", "compile"]- i <- get- c <- option (opt_codegen $ idris_options i) codegenOption- f <- P.identifier- eof- return (Compile c f))- <|> try (do cmd ["proofs"]; eof; return Proofs)- <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))- <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))- <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))- <|> try (do cmd ["let"]- defn <- concat <$> many (P.decl defaultSyntax)- return (NewDefn defn))- <|> try (do cmd ["lto", "loadto"];- toline <- P.natural- f <- many anyChar;- return (Load f (Just (fromInteger toline))))- <|> try (do cmd ["l", "load"]; f <- many anyChar;- return (Load f Nothing))- <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))- <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))- <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))- <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))- <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))- <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))- <|> try (do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n))- <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))- <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))- <|> try (do cmd ["u", "universes"]; eof; return Universes)- <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))- <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit+ <|> do cmd ["h", "?", "help"]; eof; return Help+ <|> do cmd ["w", "warranty"]; eof; return Warranty+ <|> do cmd ["r", "reload"]; eof; return Reload+ <|> do cmd ["module"]; f <- P.identifier; eof;+ return (ModImport (toPath f))+ <|> do cmd ["e", "edit"]; eof; return Edit+ <|> do cmd ["exec", "execute"]; eof; return Execute+ <|> do cmd ["c", "compile"]+ i <- get+ c <- option (opt_codegen $ idris_options i) codegenOption+ f <- P.identifier+ eof+ return (Compile c f)+ <|> do cmd ["proofs"]; eof; return Proofs+ <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)+ <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)+ <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))+ <|> do cmd ["let"]+ defn <- concat <$> many (P.decl defaultSyntax)+ return (NewDefn defn)+ <|> do cmd ["lto", "loadto"];+ toline <- P.natural+ f <- many anyChar;+ return (Load f (Just (fromInteger toline)))+ <|> do cmd ["l", "load"]; f <- many anyChar;+ return (Load f Nothing)+ <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)+ <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)+ <|> do cmd ["u", "universes"]; eof; return Universes+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n) <|> try (do cmd ["dynamic"]; eof; return ListDynamic)- <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))- <|> try (do cmd ["color", "colour"]; pSetColourCmd)- <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))- <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))- <|> try (do cmd ["s", "search"]; P.whiteSpace;- t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))- <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (CaseSplitAt upd (fromInteger l) n))- <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (AddProofClauseFrom upd (fromInteger l) n))- <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (AddClauseFrom upd (fromInteger l) n))- <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (AddMissing upd (fromInteger l) n))- <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (MakeWith upd (fromInteger l) n))- <|> try (do cmd ["ml", "makelemma"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- return (MakeLemma upd (fromInteger l) n))- <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- hints <- many P.fnName- return (DoProofSearch upd True (fromInteger l) n hints))- <|> try (do cmd ["ref", "refine"]; P.whiteSpace;- upd <- option False (do P.lchar '!'; return True)- l <- P.natural; n <- P.name;- hint <- P.fnName- return (DoProofSearch upd False (fromInteger l) n [hint]))- <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))- <|> try (do cmd ["m", "metavars"]; eof; return Metavars)- <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;- return (Just x))- eof; return (AddProof n))- <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))- <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))- <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)- <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))- <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))- <|> try (do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n))- <|> try (do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n))- <|> try (do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str))+ <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)+ <|> do cmd ["color", "colour"]; pSetColourCmd+ <|> do cmd ["set"]; o <- pOption; return (SetOpt o)+ <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)+ <|> do cmd ["s", "search"]; P.whiteSpace;+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)+ <|> do cmd ["cs", "casesplit"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (CaseSplitAt upd (fromInteger l) n)+ <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (AddProofClauseFrom upd (fromInteger l) n)+ <|> do cmd ["ac", "addclause"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (AddClauseFrom upd (fromInteger l) n)+ <|> do cmd ["am", "addmissing"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (AddMissing upd (fromInteger l) n)+ <|> do cmd ["mw", "makewith"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (MakeWith upd (fromInteger l) n)+ <|> do cmd ["ml", "makelemma"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ return (MakeLemma upd (fromInteger l) n)+ <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ hints <- many P.fnName+ return (DoProofSearch upd True (fromInteger l) n hints)+ <|> do cmd ["ref", "refine"]; P.whiteSpace;+ upd <- option False (do P.lchar '!'; return True)+ l <- P.natural; n <- P.name;+ hint <- P.fnName+ return (DoProofSearch upd False (fromInteger l) n [hint])+ <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)+ <|> do cmd ["m", "metavars"]; eof; return Metavars+ <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;+ return (Just x))+ eof; return (AddProof n)+ <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)+ <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)+ <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str) <|> do P.whiteSpace; do eof; return NOP <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
src/Idris/TypeSearch.hs view
@@ -28,7 +28,7 @@ import Idris.Core.Unify (match_unify) import Idris.Delaborate (delabTy) import Idris.Docstrings (noDocs, overview)-import Idris.ElabDecls (elabType')+import Idris.Elab.Type (elabType) import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult) import System.IO (Handle)@@ -41,7 +41,7 @@ pterm'' <- implicit toplevel syn n pterm' i <- getIState let pterm''' = addImpl i pterm''- ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'+ ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm' putIState i -- don't actually make any changes let names = searchUsing searchPred i ty let names' = take numLimit $ names
+ test/quasiquote004/Quasiquote004.idr view
@@ -0,0 +1,51 @@+module Quasiquote004++import Language.Reflection++%default total++normPlus : List (TTName, Binder TT) -> TT -> Tactic+normPlus ctxt `((=) {Nat} {Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y+normPlus ctxt `(S ~n) = normPlus ctxt n+normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))+ (normPlus ctxt m)+normPlus _ _ = Skip+++zero : List (TTName, Binder TT) -> TT -> Tactic+zero ctxt `(Nat) = Exact `(Z)+zero _ _ = Fail [TextPart "Not a Nat goal"]++-- A number is fizzy if it is evenly divisible by 3+data Fizzy : Nat -> Type where+ ZeroFizzy : Fizzy Z+ Fizz : Fizzy n -> Fizzy (3 + n)++-- Fizzy is a correct specification of divisibility by 3 - that is, if n is+-- fizzy then there exists some k such that n = 3*k.+fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)+fizzyCorrect Z ZeroFizzy = (Z ** refl)+fizzyCorrect (S (S (S k))) (Fizz x) =+ let (k' ** ih) = fizzyCorrect k x+ in (S k' ** ?fizzyIsAOK)++someNat : Nat+someNat = ?getMeNat++notNat : String+notNat = ?getMeNat'++---------- Proofs ----------+Quasiquote004.getMeNat = proof+ applyTactic zero++Quasiquote004.fizzyIsAOK = proof+ compute+ intros+ applyTactic normPlus+ applyTactic normPlus+ rewrite ih+ trivial++Quasiquote004.getMeNat' = proof+ applyTactic zero
+ test/quasiquote004/expected view
@@ -0,0 +1,2 @@+Quasiquote004.idr:50:25:When elaborating right hand side of Quasiquote004.getMeNat':+Not a Nat goal
+ test/quasiquote004/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris $@ --check --nocolour Quasiquote004.idr+rm -f *.ibc
+ test/reg048/expected view
+ test/reg048/reg048.idr view
@@ -0,0 +1,24 @@+module Main+import Data.SortedMap++test : List Int -> IO ()+test xs = do let lst = Data.SortedMap.toList mp+ if length lst /= n + then putStrLn $ "wrong length for " ++ show xs+ else do let res = map (\x => lookup x mp) xs+ let found = mapMaybe id res+ if length found /= n + then putStrLn $ "some lost in " ++ show xs ++ ": res=" ++ show res + ++ " toList=" ++ show lst+ else return ()++ where + mp : SortedMap Int ()+ mp = foldr (\x => \m => insert x () m) empty xs+ n : Nat+ n = length xs++main : IO ()+main = do test [1,2,3]+ test [4,3,2,1]+ test [1,2,3,4]
+ test/reg048/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+idris $@ reg048.idr -o reg048+./reg048+rm -f reg048 *.ibc
+ test/reg049/expected view
@@ -0,0 +1,2 @@+reg049.idr:2:9:When elaborating constructor Main.Bogus:+{__False0} is not Main.Foo
+ test/reg049/reg049.idr view
@@ -0,0 +1,5 @@+data Foo : Type where+ Bogus : _|_++uhOh : _|_+uhOh = Bogus
+ test/reg049/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --nocolour --check $@ reg049.idr+rm -f *.ibc
+ test/reg050/badbangop.idr view
@@ -0,0 +1,15 @@+module badbangop++-- Check that using "!" by itself as an operator does not work++infixl 2 !++(!) : List a -> Nat -> Maybe a+xs ! n = index' n xs++aList : List Integer+aList = [1,2,3,4,5]++opUse : Maybe Integer+opUse = aList ! 2+
+ test/reg050/baddoublebang.idr view
@@ -0,0 +1,7 @@+module baddoublebang++-- Check that two bang bindings running together don't work++doubleBang : Maybe (Maybe Nat) -> Maybe Nat+doubleBang mmn = do pure !!mmn+
+ test/reg050/expected view
@@ -0,0 +1,27 @@+badbangop.idr:16:1:When elaborating right hand side of opUse:+When elaborating an application of function Prelude.Monad.>>=:+ Can't unify+ List Integer+ with+ argTy -> retTy+ + Specifically:+ Can't unify+ List+ with+ \{uv0} => argTy -> uv+./baddoublebang.idr:6:26: error: not+ a terminator, expected: "$",+ "$>", "&&", "*", "+", "++", "-",+ "->", ".", "/", "/=", "::", ";",+ "<", "<$", "<$>", "<*>", "<+>",+ "<->", "<<", "<=", "<|>", "=",+ "==", ">", ">=", ">>", ">>=",+ "\\\\", "`", "in", "||", "~=~",+ ambiguous use of a left-associative operator,+ ambiguous use of a non-associative operator,+ ambiguous use of a right-associative operator,+ end of input, function argument,+ matching application expression+doubleBang mmn = do pure !!mmn + ^
+ test/reg050/run view
@@ -0,0 +1,5 @@+#!/usr/bin/env bash+idris --nocolour --check $@ working.idr+idris --nocolour --check $@ badbangop.idr+idris --nocolour --check $@ baddoublebang.idr+rm -f *.ibc
+ test/reg050/working.idr view
@@ -0,0 +1,21 @@+module working++-- Check that using an operator beginning with "!" works++infixl 2 !!++(!!) : List a -> Nat -> Maybe a+xs !! n = index' n xs++aList : List Integer+aList = [1,2,3,4,5]++opUse : Maybe Integer+opUse = aList !! 2++opUseWithBang : Maybe Nat -> Maybe Integer+opUseWithBang mn = do aList !! !mn++doubleBang : Maybe (Maybe Nat) -> Maybe Nat+doubleBang mmn = do pure ! !mmn+
test/totality003/totality003.idr view
@@ -3,5 +3,5 @@ total qsort : Ord a => List a -> List a qsort [] = []-qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++ +qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++ (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
test/totality003/totality003a.idr view
@@ -3,5 +3,5 @@ total qsort : Ord a => List a -> List a qsort [] = []-qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++ +qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++ (x :: qsort (filter (>= x) xs))