git.iko.soy/Idris-dev
on master help sign in
Add fromInteger to Nat class; allow type labels on let
commite5307182bc2536bb581bad6b796168e964033a0a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 22:41 (15 years ago) parent8784b67
4 files changed+27−8
compare with master
unifiedsplit
lib/builtins.idr+6 lib/nat.idr+2 src/Idris/ElabDecls.hs+7−5 src/Idris/Parser.hs+12−3
lib/builtins.idr+6
@@ -79,18 +79,24 @@ class Num a where {
7979 (+) : a -> a -> a;
8080 (-) : a -> a -> a;
8181 (*) : a -> a -> a;
82+
83+ fromInteger : Int -> a;
8284}
8385
8486instance Num Int where {
8587 (+) = prim__addInt;
8688 (-) = prim__subInt;
8789 (*) = prim__mulInt;
90+
91+ fromInteger = id;
8892}
8993
9094instance Num Float where {
9195 (+) = prim__addFloat;
9296 (-) = prim__subFloat;
9397 (*) = prim__mulFloat;
98+
99+ fromInteger = prim__intToFloat;
94100}
95101
96102class Eq a where {
lib/nat.idr+2
@@ -22,6 +22,8 @@ instance Num Nat where {
2222 (+) = plus;
2323 (-) = sub;
2424 (*) = mult;
25+
26+ fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;
2527}
2628
2729instance Eq Nat where {
src/Idris/ElabDecls.hs+7−5
@@ -561,18 +561,20 @@ elab ist info pattern tm
561561 elabE ty
562562 elabE sc
563563 solve
564− elab' (PLet n Placeholder val sc)
565− = do attack; -- (h:_) <- get_holes
564+ elab' (PLet n ty val sc)
565+ = do attack;
566566 tyn <- unique_hole (MN 0 "letty")
567− -- start_unify h
568567 claim tyn (RSet 0)
569568 valn <- unique_hole (MN 0 "letval")
570569 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
572575 focus valn
573576 elabE val
574577 elabE sc
575− -- end_unify
576578 solve
577579 elab' (PApp fc (PRef _ f) args')
578580 = do let args = {- case lookupCtxt f (inblock info) of
src/Idris/Parser.hs+12−3
@@ -418,13 +418,20 @@ pSimpleExpr syn =
418418 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
419419 <|> try (pPair syn)
420420 <|> 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)))
422423 <|> do reserved "Set"; return PSet
423424 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
424425 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
425426 <|> do lchar '_'; return Placeholder
426427 <|> pSimpleExtExpr syn
427428
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+
428435pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp
429436 fc <- pfc
430437 r <- pExpr syn; lchar ')';
@@ -470,9 +477,11 @@ pLambda syn = do lchar '\\';
470477 sc <- pExpr syn
471478 return (bindList PLam xt sc)
472479
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
474483 reserved "in"; sc <- pExpr syn
475− return (PLet n Placeholder v sc)
484+ return (PLet n ty v sc)
476485
477486pPi syn =
478487 try (do lazy <- option False (do lchar '|'; return True)