e530718 · Idris-dev · git.iko.soy

lib/builtins.idr+6

compare with master

unifiedsplit

@@ -79,18 +79,24 @@ class Num a where {

79 (+) : a -> a -> a;

80 (-) : a -> a -> a;

81 (*) : a -> a -> a;

82+

83+ fromInteger : Int -> a;

82}

84}

83

85

84instance Num Int where {

86instance Num Int where {

85 (+) = prim__addInt;

87 (+) = prim__addInt;

86 (-) = prim__subInt;

88 (-) = prim__subInt;

87 (*) = prim__mulInt;

89 (*) = prim__mulInt;

90+

91+ fromInteger = id;

88}

92}

89

93

90instance Num Float where {

94instance Num Float where {

91 (+) = prim__addFloat;

95 (+) = prim__addFloat;

92 (-) = prim__subFloat;

96 (-) = prim__subFloat;

93 (*) = prim__mulFloat;

97 (*) = prim__mulFloat;

98+

99+ fromInteger = prim__intToFloat;

94}

100}

95

101

96class Eq a where {

102class Eq a where {

lib/nat.idr+2

@@ -22,6 +22,8 @@ instance Num Nat where {

22 (+) = plus;

23 (-) = sub;

24 (*) = mult;

25+

26+ fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;

25}

27}

26

28

27instance Eq Nat where {

29instance Eq Nat where {

src/Idris/ElabDecls.hs+7−5

@@ -561,18 +561,20 @@ elab ist info pattern tm

561 elabE ty

562 elabE sc

563 solve

564− elab' (PLet n Placeholder val sc)

564+ elab' (PLet n ty val sc)

565− = do attack; -- (h:_) <- get_holes

565+ = do attack;

566 tyn <- unique_hole (MN 0 "letty")

567− -- start_unify h

568 claim tyn (RSet 0)

567 claim tyn (RSet 0)

569 valn <- unique_hole (MN 0 "letval")

568 valn <- unique_hole (MN 0 "letval")

570 claim valn (Var tyn)

569 claim valn (Var tyn)

571− letbind n (Var tyn) (Var valn)

570+ letbind n (Var tyn) (Var valn)

571+ case ty of

572+ Placeholder -> return ()

573+ _ -> do focus tyn

574+ elabE ty

572 focus valn

575 focus valn

573 elabE val

576 elabE val

574 elabE sc

577 elabE sc

575− -- end_unify

576 solve

578 solve

577 elab' (PApp fc (PRef _ f) args')

579 elab' (PApp fc (PRef _ f) args')

578 = do let args = {- case lookupCtxt f (inblock info) of

580 = do let args = {- case lookupCtxt f (inblock info) of

src/Idris/Parser.hs+12−3

@@ -418,13 +418,20 @@ pSimpleExpr syn =

418 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

419 <|> try (pPair syn)

420 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

421− <|> try (do c <- pConstant; return (PConstant c))

421+ <|> try (do c <- pConstant; fc <- pfc

422+ return (modifyConst syn fc (PConstant c)))

422 <|> do reserved "Set"; return PSet

423 <|> do reserved "Set"; return PSet

423 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

424 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

424 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

425 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

425 <|> do lchar '_'; return Placeholder

426 <|> do lchar '_'; return Placeholder

426 <|> pSimpleExtExpr syn

427 <|> pSimpleExtExpr syn

427

428

429+modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

430+modifyConst syn fc (PConstant (I x))

431+ | not (inPattern syn)

432+ = PApp fc (PRef fc (UN ["fromInteger"])) [pexp (PConstant (I x))]

433+modifyConst syn fc x = x

434+

428pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp

435pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp

429 fc <- pfc

436 fc <- pfc

430 r <- pExpr syn; lchar ')';

437 r <- pExpr syn; lchar ')';

@@ -470,9 +477,11 @@ pLambda syn = do lchar '\\';

470 sc <- pExpr syn

477 sc <- pExpr syn

471 return (bindList PLam xt sc)

478 return (bindList PLam xt sc)

472

479

473−pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn

480+pLet syn = do reserved "let"; n <- pName;

481+ ty <- option Placeholder (do lchar ':'; pExpr' syn)

482+ lchar '='; v <- pExpr syn

474 reserved "in"; sc <- pExpr syn

483 reserved "in"; sc <- pExpr syn

475− return (PLet n Placeholder v sc)

484+ return (PLet n ty v sc)

476

485

477pPi syn =

486pPi syn =

478 try (do lazy <- option False (do lchar '|'; return True)

487 try (do lazy <- option False (do lchar '|'; return True)