Merge pull request #235 from edwinb/reflect-binders

Make lambda elaborator dependent

libs/base/Language/Reflection.idr

@@ -20,9 +20,9 @@ data Elab : Type -> Type where
      Quote : val -> Elab TTImp
 
      -- Elaborate under a lambda
-     Lambda : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
-     -- Elaborate under a forall
-     ForAll : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
+     Lambda : (0 x : Type) ->
+              {0 ty : x -> Type} ->
+              ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
 
      -- Get the current goal type, if known 
      -- (it might need to be inferred from the solution)
@@ -90,13 +90,11 @@ quote : val -> Elab TTImp
 quote = Quote
 
 export
-lambda : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
+lambda : (0 x : Type) ->
+         {0 ty : x -> Type} ->
+         ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
 lambda = Lambda
 
-export
-forAll : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
-forAll = ForAll
-
 export
 goal : Elab (Maybe TTImp)
 goal = Goal

src/TTImp/Elab/RunElab.idr

@@ -93,7 +93,7 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
              defs <- get Ctxt
              empty <- clearDefs defs
              scriptRet !(unelabUniqueBinders env !(quote empty env tm'))
-    elabCon defs "Lambda" [_, x, scope]
+    elabCon defs "Lambda" [x, _, scope]
         = do empty <- clearDefs defs
              NBind bfc x (Lam c p ty) sc <- evalClosure defs scope
                    | _ => throw (GenericMsg fc "Not a lambda")
@@ -114,27 +114,6 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
          quotePi Implicit = pure Implicit
          quotePi AutoImplicit = pure AutoImplicit
          quotePi (DefImplicit t) = throw (GenericMsg fc "Can't add default lambda")
-    elabCon defs "ForAll" [_, x, scope]
-        = do empty <- clearDefs defs
-             NBind bfc x (Pi c p ty) sc <- evalClosure defs scope
-                   | _ => throw (GenericMsg fc "Not a lambda")
-             n <- genVarName "x"
-             sc' <- sc defs (toClosure withAll env (Ref bfc Bound n))
-             qsc <- quote empty env sc'
-             let lamsc = refToLocal n x qsc
-             qp <- quotePi p
-             qty <- quote empty env ty
-             let env' = Pi c qp qty :: env
-
-             runsc <- elabScript fc (weaken nest) env'
-                                 !(nf defs env' lamsc) Nothing -- (map weaken exp)
-             nf empty env (Bind bfc x (Pi c qp qty) !(quote empty env' runsc))
-       where
-         quotePi : PiInfo (NF vars) -> Core (PiInfo (Term vars))
-         quotePi Explicit = pure Explicit
-         quotePi Implicit = pure Implicit
-         quotePi AutoImplicit = pure AutoImplicit
-         quotePi (DefImplicit t) = throw (GenericMsg fc "Can't add default lambda")
     elabCon defs "Goal" []
         = do let Just gty = exp
                  | Nothing => nfOpts withAll defs env