9abbc3f · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+3−3

compare with master

unifiedsplit

@@ -198,7 +198,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

198 where

199 (args, sc) = cases_runtime cd

200

201−mkLDecl n (TyDecl (DCon tag arity) _) =

201+mkLDecl n (TyDecl (DCon tag arity _) _) =

202 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)

203

204mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

@@ -286,7 +286,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

286 ])

287

288 -- data constructor

289− (P (DCon t arity) n _, args) -> do

289+ (P (DCon t arity _) n _, args) -> do

290 detag <- fgetState (opt_detaggable . ist_optimisation n)

291 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

292

@@ -391,7 +391,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

391

392 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of

393 Just (CaseOp ci ty tys def tot cdefs) -> length tys

394− Just (TyDecl (DCon tag ar) _) -> ar

394+ Just (TyDecl (DCon tag ar _) _) -> ar

395 Just (TyDecl Ref ty) -> length $ getArgTys ty

396 Just (Operator ty ar op) -> ar

397 Just def -> error $ "unknown arity: " ++ show (n, def)

src/Idris/AbsSyntax.hs+3−3

@@ -228,7 +228,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

228 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

229 (P (TCon _ _) n _, Constant _) -> errWhen True

230 (Constant _, P (TCon _ _) n' _) -> errWhen True

231− (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)

231+ (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

232 _ -> return ()

233

234 where errWhen True

@@ -1026,7 +1026,7 @@ getPriority i tm = 1 -- pri tm

1026 where

1027 pri (PRef _ n) =

1028 case lookupP n (tt_ctxt i) of

1029− ((P (DCon _ _) _ _):_) -> 1

1029+ ((P (DCon _ _ _) _ _):_) -> 1

1030 ((P (TCon _ _) _ _):_) -> 1

1031 ((P Ref _ _):_) -> 1

1032 [] -> 0 -- must be locally bound, if it's not an error...

@@ -1474,7 +1474,7 @@ aiFn inpat True qq ist fc f ds []

1474 imp _ = True

1475-- allImp [] = False

1476 allImp xs = all imp xs

1477− constructor (TyDecl (DCon _ _) _) = True

1477+ constructor (TyDecl (DCon _ _ _) _) = True

1478 constructor _ = False

1479

1480 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

src/Idris/Apropos.hs+1−1

@@ -61,7 +61,7 @@ instance Apropos (Binder (TT Name)) where

61instance Apropos (TT Name) where

62 isApropos str (P Ref n ty) = isApropos str n || isApropos str ty

63 isApropos str (P (TCon _ _) n ty) = isApropos str n || isApropos str ty

64− isApropos str (P (DCon _ _) n ty) = isApropos str n || isApropos str ty

64+ isApropos str (P (DCon _ _ _) n ty) = isApropos str n || isApropos str ty

65 isApropos str (P Bound _ ty) = isApropos str ty

66 isApropos str (Bind n b tm) = isApropos str b || isApropos str tm

67 isApropos str (App t1 t2) = isApropos str t1 || isApropos str t2

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

@@ -290,8 +290,9 @@ instance Binary NameType where

290 = case x of

291 Bound -> putWord8 0

292 Ref -> putWord8 1

293− DCon x1 x2 -> do putWord8 2

293+ DCon x1 x2 x3 -> do putWord8 2

294− put (x1 * 65536 + x2)

294+ put (x1 * 65536 + x2)

295+ put x3

295 TCon x1 x2 -> do putWord8 3

296 TCon x1 x2 -> do putWord8 3

296 put (x1 * 65536 + x2)

297 put (x1 * 65536 + x2)

297 get

298 get

@@ -300,7 +301,8 @@ instance Binary NameType where

300 0 -> return Bound

301 0 -> return Bound

301 1 -> return Ref

302 1 -> return Ref

302 2 -> do x1x2 <- get

303 2 -> do x1x2 <- get

304+ x3 <- get

303− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

305+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)

304 3 -> do x1x2 <- get

306 3 -> do x1x2 <- get

305 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

307 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

306 _ -> error "Corrupted binary data for NameType"

308 _ -> error "Corrupted binary data for NameType"

src/Idris/Core/CaseTree.hs+2−2

@@ -344,11 +344,11 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

344toPat :: Bool -> Bool -> [Term] -> [Pat]

345toPat reflect tc = map $ toPat' []

346 where

347− toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)

347+ toPat' [_,_,arg](P (DCon t a _) nm@(UN n) _)

348 | n == txt "Delay"

349 = PCon nm t [PAny, PAny, toPat' [] arg]

350

351− toPat' args (P (DCon t a) n _)

351+ toPat' args (P (DCon t a _) n _)

352 = PCon n t $ map (toPat' []) args

353

354 -- n + 1

src/Idris/Core/DeepSeq.hs+1−1

@@ -85,7 +85,7 @@ instance NFData UExp where

85instance NFData NameType where

86 rnf Bound = ()

87 rnf Ref = ()

88− rnf (DCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

88+ rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

89 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

90

91instance (NFData n) => NFData (TT n) where

src/Idris/Core/Evaluate.hs+6−6

@@ -292,7 +292,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

292 t' <- ev ntimes stk top env t

293-- tfull' <- reapply ntimes stk top env t' []

294 return (doProj t' (getValArgs t'))

295− where doProj t' (VP (DCon _ _) _ _, args)

295+ where doProj t' (VP (DCon _ _ _) _ _, args)

296 | i >= 0 && i < length args = args!!i

297 doProj t' _ = VProj t' i

298

@@ -412,7 +412,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

412 _ -> return Nothing

413

414 conHeaded tm@(App _ _)

415− | (P (DCon _ _) _ _, args) <- unApply tm = True

415+ | (P (DCon _ _ _) _ _, args) <- unApply tm = True

416 conHeaded t = False

417

418 chooseAlt' ntimes stk env _ (f, args) alts amap

@@ -423,7 +423,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

423 chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->

424 [(Name, Value)] ->

425 Eval (Maybe ([(Name, Value)], SC))

426− chooseAlt env _ (VP (DCon i a) _ _, args) alts amap

426+ chooseAlt env _ (VP (DCon i a _) _ _, args) alts amap

427 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)

428 | Just v <- findDefault alts = return $ Just (amap, v)

429 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap

@@ -792,7 +792,7 @@ addTyDecl n nt ty uctxt

792 uctxt { definitions = ctxt' }

793

794addDatatype :: Datatype Name -> Context -> Context

795−addDatatype (Data n tag ty cons) uctxt

795+addDatatype (Data n tag ty unique cons) uctxt

796 = let ctxt = definitions uctxt

797 ty' = normalise uctxt [] ty

798 ctxt' = addCons 0 cons (addDef n

@@ -803,7 +803,7 @@ addDatatype (Data n tag ty cons) uctxt

803 addCons tag ((n, ty) : cons) ctxt

804 = let ty' = normalise uctxt [] ty in

805 addCons (tag+1) cons (addDef n

806− (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt)

806+ (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

807

808-- FIXME: Too many arguments! Refactor all these Bools.

809addCasedef :: Name -> ErasureInfo -> CaseInfo ->

@@ -928,7 +928,7 @@ isDConName :: Name -> Context -> Bool

928isDConName n ctxt

929 = or $ do def <- lookupCtxt n (definitions ctxt)

930 case tfst def of

931− (TyDecl (DCon _ _) _) -> return True

931+ (TyDecl (DCon _ _ _) _) -> return True

932 _ -> return False

933

934isFnName :: Name -> Context -> Bool

src/Idris/Core/Execute.hs+3−3

@@ -144,7 +144,7 @@ execute tm = do est <- initState

144 Right tm' -> return tm'

145

146ioWrap :: ExecVal -> ExecVal

147−ioWrap tm = mkEApp (EP (DCon 0 2) (sUN "prim__IO") EErased) [EErased, tm]

147+ioWrap tm = mkEApp (EP (DCon 0 2 False) (sUN "prim__IO") EErased) [EErased, tm]

148

149ioUnit :: ExecVal

150ioUnit = ioWrap (EP Ref unitCon EErased)

@@ -168,7 +168,7 @@ doExec env ctxt p@(P Bound n ty) =

168 case lookup n env of

169 Nothing -> execFail . Msg $ "not found"

170 Just tm -> return tm

171−doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

171+doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)

172doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

173doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

174 | otherwise = execFail . Msg $ "env too small"

@@ -340,7 +340,7 @@ execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

340 Just r -> return (mkEApp r xs')

341 Nothing -> return (mkEApp f args)

342

343−execApp env ctxt c@(EP (DCon _ arity) n _) args =

343+execApp env ctxt c@(EP (DCon _ arity _) n _) args =

344 do let args' = take arity args

345 let restArgs = drop arity args

346 execApp env ctxt (mkEApp c args') restArgs

src/Idris/Core/TT.hs+4−3

@@ -726,7 +726,7 @@ type UCs = (Int, [UConstraint])

726

727data NameType = Bound

728 | Ref

729− | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor

729+ | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

730 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

731 deriving (Show, Ord)

732{-!

@@ -743,7 +743,7 @@ instance Pretty NameType OutputAnnotation where

743instance Eq NameType where

744 Bound == Bound = True

745 Ref == Ref = True

746− DCon _ a == DCon _ b = (a == b) -- ignore tag

746+ DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag

747 TCon _ a == TCon _ b = (a == b) -- ignore tag

748 _ == _ = False

749

@@ -812,6 +812,7 @@ type EnvTT n = [(n, Binder (TT n))]

812data Datatype n = Data { d_typename :: n,

813 d_typetag :: Int,

814 d_type :: (TT n),

815+ d_unique :: Bool,

815 d_cons :: [(n, TT n)] }

816 d_cons :: [(n, TT n)] }

816 deriving (Show, Functor, Eq)

817 deriving (Show, Functor, Eq)

817

818

@@ -833,7 +834,7 @@ instance Eq n => Eq (TT n) where

833-- constant, the type Type, pi-binding, or an application of an injective

834-- constant, the type Type, pi-binding, or an application of an injective

834-- term.

835-- term.

835isInjective :: TT n -> Bool

836isInjective :: TT n -> Bool

836−isInjective (P (DCon _ _) _ _) = True

837+isInjective (P (DCon _ _ _) _ _) = True

837isInjective (P (TCon _ _) _ _) = True

838isInjective (P (TCon _ _) _ _) = True

838isInjective (Constant _) = True

839isInjective (Constant _) = True

839isInjective (TType x) = True

840isInjective (TType x) = True

src/Idris/Core/Typecheck.hs+1−13

@@ -81,23 +81,11 @@ check' holes ctxt env top = chk env top where

81 _ -> normalise ctxt env fty

82 case fty' of

83 Bind x (Pi s) t ->

84−-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

85−-- " from " ++ show fv ++ " : " ++ show fty) $

86 do convertsC ctxt env aty s

84 do convertsC ctxt env aty s

87− -- let apty = normalise initContext env

88− -- (Bind x (Let aty av) t)

89 let apty = simplify initContext env

85 let apty = simplify initContext env

90 (Bind x (Let aty av) t)

86 (Bind x (Let aty av) t)

91 return (App fv av, apty)

87 return (App fv av, apty)

92− t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"

88+ t -> lift $ tfail $ NonFunctionType fv fty

93− -- This rather unpleasant hack is needed because during incomplete

94− -- proofs, variables are locally bound with an explicit name. If we just

95− -- make sure bound names in function types are locally unique, machine

96− -- generated names, we'll be fine.

97− -- NOTE: now replaced with 'uniqueBinders' above

98− where renameBinders i (Bind x (Pi s) t) = Bind (sMN i "binder") (Pi s)

99− (renameBinders (i+1) t)

100− renameBinders i sc = sc

101 chk env RType

89 chk env RType

102 | holes = return (TType (UVal 0), TType (UVal 0))

90 | holes = return (TType (UVal 0), TType (UVal 0))

103 | otherwise = do (v, cs) <- get

91 | otherwise = do (v, cs) <- get

src/Idris/Core/Unify.hs+18−18

@@ -85,12 +85,12 @@ match_unify ctxt env topx topy inj holes from =

85 -- answer, merely a valid one, so perhaps we're okay.

86 -- In other words: it may vanish without warning some day :)

87 un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

88− | (P (DCon _ _) _ _, _) <- unApply x,

88+ | (P (DCon _ _ _) _ _, _) <- unApply x,

89 holeIn env f || f `elem` holes

90 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

91 checkCycle names (f, Bind n' (Lam t) x)

92 un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

93− | (P (DCon _ _) _ _, _) <- unApply x,

93+ | (P (DCon _ _ _) _ _, _) <- unApply x,

94 holeIn env f || f `elem` holes

95 = let n' = uniqueName fn (map fst env) in

96 checkCycle names (f, Bind n' (Lam t) x)

@@ -265,11 +265,11 @@ unify ctxt env topx topy inj holes usersupp from =

265-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

266 Error e -> tfail e

267 where

268− headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

268+ headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

269 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

270 headDiff _ _ = False

271

272− injective (P (DCon _ _) _ _) = True

272+ injective (P (DCon _ _ _) _ _) = True

273 injective (P (TCon _ _) _ _) = True

274-- injective (App f (P _ _ _)) = injective f

275-- injective (App f (Constant _)) = injective f

@@ -315,13 +315,13 @@ unify ctxt env topx topy inj holes usersupp from =

315 StateT UInfo

316 TC [(Name, TT Name)]

317 un' fn names x y | x == y = return [] -- shortcut

318− un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)

318+ un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)

319 | x /= y = unifyFail topx topy

320 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)

321 | x /= y = unifyFail topx topy

322− un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)

322+ un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)

323 = unifyFail topx topy

324− un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

324+ un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)

325 = unifyFail topx topy

326 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

327 = unifyFail topx topy

@@ -461,13 +461,13 @@ unify ctxt env topx topy inj holes usersupp from =

461 | otherwise = unifyTmpFail appx appy

462 where hnormalise [] _ _ t = t

463 hnormalise ns ctxt env t = normalise ctxt env t

464− checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

464+ checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)

465 | x /= y = unifyFail appx appy

466 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

467 | x /= y = unifyFail appx appy

468− checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)

468+ checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)

469 = unifyFail appx appy

470− checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)

470+ checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)

471 = unifyFail appx appy

472 checkHeads _ _ = return []

473

@@ -493,7 +493,7 @@ unify ctxt env topx topy inj holes usersupp from =

493 all (\x -> pat x || metavar x) (f : args)

494 && nub args == args

495

496− rigid (P (DCon _ _) _ _) = True

496+ rigid (P (DCon _ _ _) _ _) = True

497 rigid (P (TCon _ _) _ _) = True

498 rigid t@(P Ref _ _) = inenv t || globmetavar t

499 rigid (Constant _) = True

@@ -633,15 +633,15 @@ recoverable t@(App _ _) _

633 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

634recoverable _ t@(App _ _)

635 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

636−recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

636+recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

637recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

638−recoverable (Constant _) (P (DCon _ _) y _) = False

638+recoverable (Constant _) (P (DCon _ _ _) y _) = False

639recoverable (Constant x) (Constant y) = x == y

640−recoverable (P (DCon _ _) x _) (Constant _) = False

640+recoverable (P (DCon _ _ _) x _) (Constant _) = False

641recoverable (Constant _) (P (TCon _ _) y _) = False

642recoverable (P (TCon _ _) x _) (Constant _) = False

643−recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

643+recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

644−recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

644+recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

645recoverable p@(Constant _) (App f a) = recoverable p f

646recoverable (App f a) p@(Constant _) = recoverable f p

647recoverable p@(P _ n _) (App f a) = recoverable p f

@@ -651,10 +651,10 @@ recoverable (App f a) (App f' a')

651recoverable (App f a) (App f' a')

652 = recoverable f f' -- && recoverable a a'

653recoverable f (Bind _ (Pi _) sc)

654− | (P (DCon _ _) _ _, _) <- unApply f = False

654+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

655 | (P (TCon _ _) _ _, _) <- unApply f = False

656recoverable (Bind _ (Pi _) sc) f

657− | (P (DCon _ _) _ _, _) <- unApply f = False

657+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

658 | (P (TCon _ _) _ _, _) <- unApply f = False

659recoverable (Bind _ (Lam _) sc) f = recoverable sc f

660recoverable f (Bind _ (Lam _) sc) = recoverable f sc

src/Idris/Coverage.hs+5−5

@@ -206,7 +206,7 @@ genAll i args

206 otherPats arg = return Placeholder

207

208 ops fc n xs o

209− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

209+ | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)

210 = do xs' <- mapM otherPats (map getExpTm xs)

211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212 let tyn = getTy n (tt_ctxt i)

@@ -341,7 +341,7 @@ calcProd i fc topn pats

341 return (and ok)

342 _ -> return True -- defined elsewhere, can't call topn

343

344− cotype (DCon _ _) n ty

344+ cotype (DCon _ _ _) n ty

345 | (P _ t _, _) <- unApply (getRetTy ty)

346 = case lookupCtxt t (idris_datatypes i) of

347 [TI _ True _ _ _] -> True

@@ -391,7 +391,7 @@ checkTotality path fc n

391 setTotality n t'

392 addIBC (IBCTotal n t')

393 return t'

394− [TyDecl (DCon _ _) ty] ->

394+ [TyDecl (DCon _ _ _) ty] ->

395 case unApply (getRetTy ty) of

396 (P _ tyn _, _) -> do

397 let ms = case lookupCtxt tyn (idris_datatypes i) of

@@ -558,7 +558,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

558 | a == t = isInductive (fst (unApply (getRetTy tyn)))

559 (fst (unApply (getRetTy tyt)))

560 smaller ty a (ap@(App f s), _)

561− | (P (DCon _ _) n _, args) <- unApply ap

561+ | (P (DCon _ _ _) n _, args) <- unApply ap

562 = let tyn = getType n in

563 any (smaller (ty `mplus` Just tyn) a)

564 (zip args (map toJust (getArgTys tyn)))

@@ -652,7 +652,7 @@ checkMP ist i mp = if i > 0

652-- = Partial BelieveMe

653 -- if we get to a constructor, it's fine as long as it's strictly positive

654 tryPath desc path ((f, _) : es) arg

655− | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

655+ | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)

656 = case lookupTotal f (tt_ctxt ist) of

657 [Total _] -> Unchecked -- okay so far

658 [Partial _] -> Partial (Other [f])

src/Idris/DataOpts.hs+8−7

@@ -72,19 +72,19 @@ instance Optimisable (TT Name) where

72 applyOpts (P _ (NS (UN fn) mod) _)

73 | fn == txt "toIntegerNat" && mod == prel

74 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

75− applyOpts c@(P (DCon t arity) n _)

75+ applyOpts c@(P (DCon t arity uniq) n _)

76− = return $ applyDataOptRT n t arity []

76+ = return $ applyDataOptRT n t arity uniq []

77 applyOpts t@(App f a)

78− | (c@(P (DCon t arity) n _), args) <- unApply t

78+ | (c@(P (DCon t arity uniq) n _), args) <- unApply t

79− = applyDataOptRT n t arity <$> mapM applyOpts args

79+ = applyDataOptRT n t arity uniq <$> mapM applyOpts args

80 | otherwise = App <$> applyOpts f <*> applyOpts a

81 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

82 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

83 applyOpts t = return t

84

85-- Need to saturate arguments first to ensure that optimisation happens uniformly

86−applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term

86+applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term

87−applyDataOptRT n tag arity args

87+applyDataOptRT n tag arity uniq args

88 | length args == arity = doOpts n args

89 | otherwise = let extra = satArgs (arity - length args)

90 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

@@ -104,4 +104,5 @@ applyDataOptRT n tag arity args

104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106

107− doOpts n args = mkApp (P (DCon tag arity) n Erased) args

107+ doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

108+

src/Idris/Elab/Data.hs+5−2

@@ -71,6 +71,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

71 -- temporary, to check cons

72 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

73 let cnameinfo = cinfo info (map cname dcons)

74+ let unique = case getRetTy cty of

75+ UType UniqueType -> True

76+ _ -> False

74 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

77 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

75 ttag <- getName

78 ttag <- getName

76 i <- getIState

79 i <- getIState

@@ -90,7 +93,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

90 let metainf = DataMI params

93 let metainf = DataMI params

91 addIBC (IBCMetaInformation n metainf)

94 addIBC (IBCMetaInformation n metainf)

92 -- TMP HACK! Make this a data option

95 -- TMP HACK! Make this a data option

93− updateContext (addDatatype (Data n ttag cty cons))

96+ updateContext (addDatatype (Data n ttag cty unique cons))

94 updateContext (setMetaInformation n metainf)

97 updateContext (setMetaInformation n metainf)

95 mapM_ totcheck (zip (repeat fc) (map fst cons))

98 mapM_ totcheck (zip (repeat fc) (map fst cons))

96-- mapM_ (checkPositive n) cons

99-- mapM_ (checkPositive n) cons

@@ -258,7 +261,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

258 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()

261 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()

259 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()

262 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()

260 checkUniqueKind (UType UniqueType) (TType _)

263 checkUniqueKind (UType UniqueType) (TType _)

261− = tclift $ tfail (UniqueKindError n)

264+ = tclift $ tfail (At fc (UniqueKindError n))

262 checkUniqueKind (UType AllTypes) _ = return ()

265 checkUniqueKind (UType AllTypes) _ = return ()

263 checkUniqueKind (TType _) _ = return ()

266 checkUniqueKind (TType _) _ = return ()

264

267

src/Idris/ElabDecls.hs+3−3

@@ -122,9 +122,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

122 p_synEq args = Nothing

123

124 nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased

125− vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

125+ vnJust = VP (DCon 1 2 False) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

126− vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

126+ vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

127− vnRefl = VP (DCon 0 2) eqCon VErased

127+ vnRefl = VP (DCon 0 2 False) eqCon VErased

128

129 synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

130 (Bind (sUN "b") (Pi (TType (UVar (-3))))

src/Idris/ElabTerm.hs+8−8

@@ -1608,7 +1608,7 @@ reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

1608reifyTTNameType t@(App _ _)

1609 = case unApply t of

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

1611− | f == reflm "DCon" -> return $ DCon tag num

1611+ | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

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

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

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

@@ -1866,8 +1866,8 @@ reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

1866reflectNameType :: NameType -> Raw

1867reflectNameType (Bound) = Var (reflm "Bound")

1868reflectNameType (Ref) = Var (reflm "Ref")

1869−reflectNameType (DCon x y)

1869+reflectNameType (DCon x y _)

1870− = reflCall "DCon" [RConstant (I x), RConstant (I y)]

1870+ = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

1871reflectNameType (TCon x y)

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

1873

@@ -2165,7 +2165,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2165 parts -> ReflectionError errorparts e

2166

2167fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2168−fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

2168+fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

2169 | just == txt "Just" = Just tm

2170fromTTMaybe x = Nothing

2171

@@ -2176,9 +2176,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2176-- representation. Not in Idris or ElabD monads because it should be usable

2177-- from either.

2178reifyReportPart :: Term -> Either Err ErrorReportPart

2179−reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2179+reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2180 Right (TextPart msg)

2181−reifyReportPart (App (P (DCon _ _) n _) ttn)

2181+reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2182 | n == reflm "NamePart" =

2183 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2184 Error e -> Left . InternalMsg $

@@ -2186,7 +2186,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

2186 show ttn ++

2187 " when reflecting an error:" ++ show e

2188 OK (n', _)-> Right $ NamePart n'

2189−reifyReportPart (App (P (DCon _ _) n _) tm)

2189+reifyReportPart (App (P (DCon _ _ _) n _) tm)

2190 | n == reflm "TermPart" =

2191 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2192 Error e -> Left . InternalMsg $

@@ -2194,7 +2194,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

2194 show tm ++

2195 " when reflecting an error:" ++ show e

2196 OK (tm', _) -> Right $ TermPart tm'

2197−reifyReportPart (App (P (DCon _ _) n _) tm)

2197+reifyReportPart (App (P (DCon _ _ _) n _) tm)

2198 | n == reflm "SubReport" =

2199 case unList tm of

2200 Just xs -> do subParts <- mapM reifyReportPart xs

src/Idris/Erasure.hs+4−4

@@ -370,13 +370,13 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

370 getDepsTerm vs bs cd app@(App _ _)

371 | (fun, args) <- unApply app = case fun of

372 -- instance constructors -> create metamethod deps

373− P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _

373+ P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

374 -> conditionalDeps ctorName args -- regular data ctor stuff

375 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

376

377 -- ordinary constructors

378 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

379− P (DCon _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

379+ P (DCon _ _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

380

381 -- mkForeign* calls must be special-cased because they are variadic

382 -- All arguments must be marked as used, except for the first one,

@@ -469,7 +469,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

469 -- Get the number of arguments that might be considered for erasure.

470 getArity :: Name -> Int

471 getArity (SN (WhereN i' ctorName (MN i field)))

472− | Just (TyDecl (DCon _ _) ty) <- lookupDefExact ctorName ctx

472+ | Just (TyDecl (DCon _ _ _) ty) <- lookupDefExact ctorName ctx

473 = let argTys = map snd $ getArgTys ty

474 in if i <= length argTys

475 then length $ getArgTys (argTys !! i)

@@ -479,7 +479,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

479

480 getArity n = case lookupDefExact n ctx of

481 Just (CaseOp ci ty tys def tot cdefs) -> length tys

482− Just (TyDecl (DCon tag arity) _) -> arity

482+ Just (TyDecl (DCon tag arity _) _) -> arity

483 Just (TyDecl (Ref) ty) -> length $ getArgTys ty

484 Just (Operator ty arity op) -> arity

485 Just df -> error $ "Erasure/getArity: unrecognised entity '"

src/Idris/IBC.hs+1−1

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

32

33ibcVersion :: Word8

34−ibcVersion = 78

34+ibcVersion = 79

35

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,