2e02cf6 · Idris-dev · git.iko.soy

samples/interp.idr+1−2

compare with master

unifiedsplit

@@ -27,7 +27,6 @@ using (G : Vect Ty n) {

27 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

28 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

29

30−

31 interp : Env G -> [static] Expr G t -> interpTy t;

30 interp : Env G -> [static] Expr G t -> interpTy t;

32 interp env (Var i) = envLookup i env;

31 interp env (Var i) = envLookup i env;

33 interp env (Val x) = x;

32 interp env (Val x) = x;

@@ -40,7 +39,7 @@ using (G : Vect Ty n) {

40

39

41 eId : Expr G (TyFun TyInt TyInt);

40 eId : Expr G (TyFun TyInt TyInt);

42 eId = Lam (Var fO);

41 eId = Lam (Var fO);

43−

42+

44 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

43 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

45 eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

44 eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

46

45

src/Idris/Parser.hs+8−6

@@ -675,12 +675,14 @@ pWhereblock n syn

675 return (concat ds, map (\x -> (x, decoration syn x)) dns)

676

677pDirective :: IParser [PDecl]

678−pDirective = do lchar '%'; reserved "lib"; lib <- strlit;

678+pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

679− return [PDirective (addLib lib)]

679+ return [PDirective (addLib lib)])

680− <|> do lchar '%'; reserved "link"; obj <- strlit;

680+ <|> try (do lchar '%'; reserved "link"; obj <- strlit;

681− return [PDirective (do datadir <- lift $ getDataDir

681+ return [PDirective (do datadir <- lift $ getDataDir

682− o <- lift $ findInPath [".", datadir] obj

682+ o <- lift $ findInPath [".", datadir] obj

683− addObjectFile o)]

683+ addObjectFile o)])

684+ <|> do lchar '%'; reserved "logging"; i <- natural;

685+ return [PDirective (setLogLevel (fromInteger i))]

684

686

685pTactic :: SyntaxInfo -> IParser PTactic

687pTactic :: SyntaxInfo -> IParser PTactic

686pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

688pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/REPL.hs+1−1

@@ -52,7 +52,7 @@ processInput cmd orig inputs

52 case parseCmd i cmd of

53 Left err -> do lift $ print err

54 return (Just inputs)

55− Right Reload -> do put orig

55+ Right Reload -> do put (orig { idris_options = idris_options i })

56 clearErr

57 mods <- mapM loadModule inputs

58 return (Just inputs)