@@ -153,40 +153,6 @@ elabDecl' info (PParams ns ps) = do iLOG $ "Params block " ++ show ns
153 info { params = newps,
153 info { params = newps,
154 inblock = newb }
154 inblock = newb }
157−parameterise :: [(Name, Type)] -> (Name -> Name) -> [PDecl] -> Idris [PDecl]
158−parameterise ns hide ds = do
160− let pns = map (\ (n, t) -> (n, delab i t)) ns
161− mapM (paramDecl (concatMap declared ds) hide pns) ds
163−paramDecl :: [Name] -> -- Names defined in this block
164− (Name -> Name) -> -- what to call the lifted functions
165− [(Name, PTerm)] -> -- parameters to add
166− PDecl -> Idris PDecl
167−paramDecl ns newname ps (PTy n ty)
168− = do let ty' = piBind ps ty
169− return (PTy (newname n) (addNs ns newname (map fst ps) ty'))
170−paramDecl ns newname ps (PClauses n cs)
171− = do cs' <- mapM pclause cs
172− return (PClauses n cs')
174− pclause (PClause n lhs rhs [])
175− = return $ PClause n [] (addNs ns newname (map fst ps) lhs)
176− (addNs ns newname (map fst ps) rhs)
177−paramDecl ns newname ps (PData (PDatadecl n ty cons))
178− = do let ty' = piBind ps ty
179− cons' <- mapM con cons
180− return (PData (PDatadecl n ty' cons'))
182− con (n, ty) = do let ty' = piBind ps ty
183− return (n, addNs ns newname (map fst ps) ty')
184−paramDecl ns newname ps d = return d
187−addNs :: [Name] -> (Name -> Name) -> [Name] -> PTerm -> PTerm
190-- Using the elaborator, convert a term in raw syntax to a fully
156-- Using the elaborator, convert a term in raw syntax to a fully
191-- elaborated, typechecked term.
157-- elaborated, typechecked term.