cleanup

Author: andrevidela

src/Core/Reflect.idr

@@ -890,50 +890,6 @@ Reflect a => Reflect (WithFC a) where
            val' <- reflect fc defs lhs env value.val
            appCon fc defs (reflectiontt "MkFCVal") [Erased fc Placeholder, loc', val']
 
--- -- Records are reflected into Data.List.Quantifier.All
--- export
--- (refs : All (Reflect . LabelledValue) fields) => Reflect (Record fields) where
---   reflect fc defs lhs env [] = appCon fc defs (listAll "Nil") [Erased fc Placeholder]
---   reflect fc defs lhs env (x :: xs) {refs = r :: rs}
---       = do x' <- reflect @{r} fc defs lhs env x
---            xs' <- reflect fc defs lhs env xs
---            appCon fc defs (listAll "::") [Erased fc Placeholder, x', xs']
---
--- -- Records are reified from Data.List.Quantifier.All the labels are inferred from the type
--- export
--- {fields : _} -> (rei : All (Reify . LabelledValue) fields) => Reify (Record fields) where
---   reify defs val@(NDCon _ n _ _ args) {fields = []}
---     = case (dropAllNS !(full (gamma defs) n)) of
---            (UN (Basic "Nil")) => pure []
---            _ => cantReify val "expected empty fields"
---   reify defs val@(NDCon _ n _ _ args) {fields = f :: fs} {rei = r :: rs}
---     = case (dropAllNS !(full (gamma defs) n), map snd args) of
---            (UN (Basic "::"), [_, x, xs]) => do
---              x' <- reify defs !(evalClosure defs x)
---              xs' <- reify defs !(evalClosure defs xs)
---              pure (x' :: xs')
---            (_, args) => cantReify val "fields : \{show (map label (f :: fs))}, args: \{show (length args)}"
---   reify defs val {fields} = cantReify val "fields : \{show (map label fields)}"
-
--- export
--- All (Reflect . LabelledValue) fields => Reflect a => Reflect (WithData fields a) where
---   reflect fc defs lhs env (MkWithData metadata val)
---     = do m' <- reflect fc defs lhs env metadata
---          val' <- reflect fc defs lhs env val
---          appCon fc defs (reflectiontt "MkWithData") [m', val']
---
--- export
--- {fields : _} -> All (Reify . LabelledValue) fields => Reify a => Reify (WithData fields a) where
---   reify defs val@(NDCon _ n _ _ args) {fields}
---     = case (dropAllNS !(full (gamma defs) n), map snd args) of
---            (UN (Basic "MkWithData"), [_, m, val]) => do
---              m' <- reify defs !(evalClosure defs m)
---              v' <- reify defs !(evalClosure defs val)
---              pure (MkWithData m' v')
---            (_, args) => cantReify val "WithData : \{show (map label fields)}, args : \{show (length args)}"
---   reify defs val {fields} = cantReify val "WithData : \{show (map label fields)}"
-
-
 export
 Reflect BindingModifier where
   reflect fc defs lhs env NotBinding = getCon fc defs (reflectiontt "NotBinding")

src/Core/WithData.idr

@@ -199,14 +199,12 @@ public export
 TyName' : KeyVal
 TyName' = "name" :-: FCBind Name
 
-namespace TypeName
-  ||| Extract the "tyname" value from the metadata record
-  export
-  (.tyName) : {n : Nat} ->
-            (inRange : NameInRange "name" fields === Just (n, FCBind Name)) =>
-            WithData fields a -> FCBind Name
-  (.tyName) = WithData.get "name" @{inRange}
-
+||| Extract the "tyname" value from the metadata record
+export
+(.tyName) : {n : Nat} ->
+          (inRange : NameInRange "name" fields === Just (n, FCBind Name)) =>
+          WithData fields a -> FCBind Name
+(.tyName) = WithData.get "name" @{inRange}
 
 ||| Attach documentation, binding and location information to a type
 public export