2378a62 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Convert holes to patterns when evaluating at the prompt, for display

2378a62Edwin Brady15 years ago

interp.mi+6−3

@@ -69,11 +69,14 @@ eDouble' : {G : Vect Ty n} ->

69 Expr G (TyFun TyNat TyNat);

70eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));

72+-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

73+

72−eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat TyNat);

74+eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat (TyFun TyNat TyNat));

75+eProg = Lam (Lam

73−eProg = Lam (Bind (App eDouble (Var fO))

76+ (Bind (App eDouble (Var (fS fO)))

74 (\x => Bind (App eDouble (Var fO))

77 (\x => Bind (App eDouble (Var fO))

75 (\y => Bind (App eDouble (Val x))

78 (\y => Bind (App eDouble (Val x))

76− (\z => App (App eAdd (Val y)) (Val z)))));

79+ (\z => App (App eAdd (Val y)) (Val z))))));

78test : Nat;

81test : Nat;

79test = interp Empty eAdd (S (S O)) (S (S O));

82test = interp Empty eAdd (S (S O)) (S (S O));

src/Idris/ElabDecls.hs+1−1

@@ -62,7 +62,7 @@ elabVal :: PTerm -> Idris (Term, Type)

62elabVal tm

63 = do ctxt <- getContext

64 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

65− (build False (infTerm tm))

65+ (build True (infTerm tm))

66 let vtm = getInferTerm tm'

67 iLOG (show vtm)

68 tclift $ recheck ctxt [] vtm