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

src/IRTS/Compiler.hs+3−3

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

198198 where

199199 (args, sc) = cases_runtime cd

200200

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

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

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

203203

204204mkLDecl 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

286286 ])

287287

288288 -- data constructor

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

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

290290 detag <- fgetState (opt_detaggable . ist_optimisation n)

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

292292

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

391391

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

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

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

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

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

396396 Just (Operator ty ar op) -> ar

397397 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

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

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

230230 (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)

232232 _ -> return ()

233233

234234 where errWhen True

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

10261026 where

10271027 pri (PRef _ n) =

10281028 case lookupP n (tt_ctxt i) of

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

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

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

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

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

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

14741474 imp _ = True

14751475-- allImp [] = False

14761476 allImp xs = all imp xs

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

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

14781478 constructor _ = False

14791479

14801480 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

6161instance Apropos (TT Name) where

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

6363 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

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

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

6767 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

290290 = case x of

291291 Bound -> putWord8 0

292292 Ref -> putWord8 1

293− DCon x1 x2 -> do putWord8 2

294− put (x1 * 65536 + x2)

293+ DCon x1 x2 x3 -> do putWord8 2

294+ put (x1 * 65536 + x2)

295+ put x3

295296 TCon x1 x2 -> do putWord8 3

296297 put (x1 * 65536 + x2)

297298 get

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

300301 0 -> return Bound

301302 1 -> return Ref

302303 2 -> do x1x2 <- get

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

304+ x3 <- get

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

304306 3 -> do x1x2 <- get

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

306308 _ -> 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

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

345345toPat reflect tc = map $ toPat' []

346346 where

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

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

348348 | n == txt "Delay"

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

350350

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

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

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

353353

354354 -- n + 1

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

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

8585instance NFData NameType where

8686 rnf Bound = ()

8787 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` ()

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

9090

9191instance (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

292292 t' <- ev ntimes stk top env t

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

294294 return (doProj t' (getValArgs t'))

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

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

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

297297 doProj t' _ = VProj t' i

298298

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

412412 _ -> return Nothing

413413

414414 conHeaded tm@(App _ _)

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

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

416416 conHeaded t = False

417417

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

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

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

424424 [(Name, Value)] ->

425425 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

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

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

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

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

792792 uctxt { definitions = ctxt' }

793793

794794addDatatype :: Datatype Name -> Context -> Context

795−addDatatype (Data n tag ty cons) uctxt

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

796796 = let ctxt = definitions uctxt

797797 ty' = normalise uctxt [] ty

798798 ctxt' = addCons 0 cons (addDef n

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

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

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

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

807807

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

809809addCasedef :: Name -> ErasureInfo -> CaseInfo ->

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

928928isDConName n ctxt

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

930930 case tfst def of

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

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

932932 _ -> return False

933933

934934isFnName :: Name -> Context -> Bool

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

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

144144 Right tm' -> return tm'

145145

146146ioWrap :: 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]

148148

149149ioUnit :: ExecVal

150150ioUnit = ioWrap (EP Ref unitCon EErased)

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

168168 case lookup n env of

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

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

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

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

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

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

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

341341 Nothing -> return (mkEApp f args)

342342

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

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

344344 do let args' = take arity args

345345 let restArgs = drop arity args

346346 execApp env ctxt (mkEApp c args') restArgs

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

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

726726

727727data NameType = Bound

728728 | Ref

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

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

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

731731 deriving (Show, Ord)

732732{-!

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

743743instance Eq NameType where

744744 Bound == Bound = True

745745 Ref == Ref = True

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

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

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

748748 _ == _ = False

749749

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

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

813813 d_typetag :: Int,

814814 d_type :: (TT n),

815+ d_unique :: Bool,

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

816817 deriving (Show, Functor, Eq)

817818

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

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

834835-- term.

835836isInjective :: TT n -> Bool

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

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

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

838839isInjective (Constant _) = True

839840isInjective (TType x) = True

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

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

8181 _ -> normalise ctxt env fty

8282 case fty' of

8383 Bind x (Pi s) t ->

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

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

8684 do convertsC ctxt env aty s

87− -- let apty = normalise initContext env

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

8985 let apty = simplify initContext env

9086 (Bind x (Let aty av) t)

9187 return (App fv av, apty)

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

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

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

10189 chk env RType

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

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

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

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

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

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

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

8989 holeIn env f || f `elem` holes

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

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

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

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

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

9494 holeIn env f || f `elem` holes

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

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

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

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

266266 Error e -> tfail e

267267 where

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

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

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

270270 headDiff _ _ = False

271271

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

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

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

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

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

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

315315 StateT UInfo

316316 TC [(Name, TT Name)]

317317 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 _)

319319 | x /= y = unifyFail topx topy

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

321321 | 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 _)

323323 = 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 _)

325325 = unifyFail topx topy

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

327327 = unifyFail topx topy

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

461461 | otherwise = unifyTmpFail appx appy

462462 where hnormalise [] _ _ t = t

463463 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 _)

465465 | x /= y = unifyFail appx appy

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

467467 | x /= y = unifyFail appx appy

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

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

469469 = unifyFail appx appy

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

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

471471 = unifyFail appx appy

472472 checkHeads _ _ = return []

473473

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

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

494494 && nub args == args

495495

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

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

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

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

499499 rigid (Constant _) = True

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

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

634634recoverable _ t@(App _ _)

635635 | (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

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

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

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

639639recoverable (Constant x) (Constant y) = x == y

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

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

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

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

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

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

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

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

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

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

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

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

651651recoverable (App f a) (App f' a')

652652 = recoverable f f' -- && recoverable a a'

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

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

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

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

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

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

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

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

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

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

src/Idris/Coverage.hs+5−5

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

206206 otherPats arg = return Placeholder

207207

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

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

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

212212 let tyn = getTy n (tt_ctxt i)

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

341341 return (and ok)

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

343343

344− cotype (DCon _ _) n ty

344+ cotype (DCon _ _ _) n ty

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

346346 = case lookupCtxt t (idris_datatypes i) of

347347 [TI _ True _ _ _] -> True

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

391391 setTotality n t'

392392 addIBC (IBCTotal n t')

393393 return t'

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

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

395395 case unApply (getRetTy ty) of

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

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

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

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

559559 (fst (unApply (getRetTy tyt)))

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

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

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

562562 = let tyn = getType n in

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

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

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

652652-- = Partial BelieveMe

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

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

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

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

656656 = case lookupTotal f (tt_ctxt ist) of

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

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

src/Idris/DataOpts.hs+8−7

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

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

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

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

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

76− = return $ applyDataOptRT n t arity []

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

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

7777 applyOpts t@(App f a)

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

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

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

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

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

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

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

8383 applyOpts t = return t

8484

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

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

87−applyDataOptRT n tag arity args

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

87+applyDataOptRT n tag arity uniq args

8888 | length args == arity = doOpts n args

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

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

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

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

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

106106

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)

7171 -- temporary, to check cons

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

7373 let cnameinfo = cinfo info (map cname dcons)

74+ let unique = case getRetTy cty of

75+ UType UniqueType -> True

76+ _ -> False

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

7578 ttag <- getName

7679 i <- getIState

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

9093 let metainf = DataMI params

9194 addIBC (IBCMetaInformation n metainf)

9295 -- TMP HACK! Make this a data option

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

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

9497 updateContext (setMetaInformation n metainf)

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

9699-- mapM_ (checkPositive n) cons

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

258261 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()

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

260263 checkUniqueKind (UType UniqueType) (TType _)

261− = tclift $ tfail (UniqueKindError n)

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

262265 checkUniqueKind (UType AllTypes) _ = return ()

263266 checkUniqueKind (TType _) _ = return ()

264267

src/Idris/ElabDecls.hs+3−3

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

122122 p_synEq args = Nothing

123123

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

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

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

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

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

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

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

128128

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

130130 (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

16081608reifyTTNameType t@(App _ _)

16091609 = case unApply t of

16101610 (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!

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

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

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

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

18661866reflectNameType :: NameType -> Raw

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

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

1869−reflectNameType (DCon x y)

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

1869+reflectNameType (DCon x y _)

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

18711871reflectNameType (TCon x y)

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

18731873

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

21652165 parts -> ReflectionError errorparts e

21662166

21672167fromTTMaybe :: 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)

21692169 | just == txt "Just" = Just tm

21702170fromTTMaybe x = Nothing

21712171

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

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

21772177-- from either.

21782178reifyReportPart :: 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" =

21802180 Right (TextPart msg)

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

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

21822182 | n == reflm "NamePart" =

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

21842184 Error e -> Left . InternalMsg $

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

21862186 show ttn ++

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

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

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

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

21902190 | n == reflm "TermPart" =

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

21922192 Error e -> Left . InternalMsg $

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

21942194 show tm ++

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

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

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

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

21982198 | n == reflm "SubReport" =

21992199 case unList tm of

22002200 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]

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

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

372372 -- instance constructors -> create metamethod deps

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

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

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

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

376376

377377 -- ordinary constructors

378378 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

380380

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

382382 -- 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]

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

470470 getArity :: Name -> Int

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

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

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

473473 = let argTys = map snd $ getArgTys ty

474474 in if i <= length argTys

475475 then length $ getArgTys (argTys !! i)

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

479479

480480 getArity n = case lookupDefExact n ctx of

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

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

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

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

484484 Just (Operator ty arity op) -> arity

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

src/Idris/IBC.hs+1−1

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

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 78

34+ibcVersion = 79

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,