@@ -33,19 +33,17 @@ import Data.List
3333import Control.Monad
3434
3535-- | Elaborate a record declaration
36−elabRecord :: ElabInfo ->
37− (Docstring (Either Err PTerm)) -> -- ^ The documentation for the whole declaration
38− SyntaxInfo ->
39− FC ->
40− DataOpts ->
41− Name -> -- ^ Record Type Name
42− [(Name, Plicity, PTerm)] -> -- ^ Parameters
43− [(Name, Docstring (Either Err PTerm))] -> -- ^ Parameter Docs
44− [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> -- ^ Fields
45− Maybe Name -> -- ^ Constructor Name
46− (Docstring (Either Err PTerm)) -> -- ^ Constructor Doc
47− SyntaxInfo -> -- ^ Constructor SyntaxInfo
48− Idris ()
36+elabRecord :: ElabInfo
37+ -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
38+ -> SyntaxInfo -> FC -> DataOpts
39+ -> Name -- ^ The name of the type being defined
40+ -> [(Name, Plicity, PTerm)] -- ^ Parameters
41+ -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs
42+ -> [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields
43+ -> Maybe Name -- ^ Constructor Name
44+ -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
45+ -> SyntaxInfo -- ^ Constructor SyntaxInfo
46+ -> Idris ()
4947elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
5048 = do logLvl 1 $ "Building data declaration for " ++ show tyn
5149 -- Type constructor
@@ -138,15 +136,13 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
138136 in (n, p, t, doc) : (fwnad rest)
139137 fwnad [] = []
140138
141−elabRecordFunctions :: ElabInfo ->
142− SyntaxInfo ->
143− FC ->
144− Name -> -- ^ Record Type Name
145− [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -> -- ^ Parameters
146− [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]-> -- ^ Fields
147− Name -> -- ^ Constructor Name
148− PTerm -> -- ^ Target Type
149− Idris ()
139+elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC
140+ -> Name -- ^ Record type name
141+ -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters
142+ -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields
143+ -> Name -- ^ Constructor Name
144+ -> PTerm -- ^ Target type
145+ -> Idris ()
150146elabRecordFunctions info rsyn fc tyn params fields dconName target
151147 = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn
152148
@@ -286,20 +282,19 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
286282 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
287283
288284-- | Creates and elaborates a projection function.
289−elabProjection :: ElabInfo ->
290− Name -> -- ^ Name of the argument in the constructor
291− Name -> -- ^ Projection Name
292− Plicity -> -- ^ Projection Plicity
293− PTerm -> -- ^ Projection Type
294− (Docstring (Either Err PTerm)) -> -- ^ Projection Documentation
295− SyntaxInfo -> -- ^ Projection SyntaxInfo
296− FC ->
297− PTerm -> -- ^ Projection Target Type
298− Name -> -- ^ Data Constructor Name
299− [PArg] -> -- ^ Placeholder Arguments to constructor
300− [Name] -> -- ^ All Field Names
301− Int -> -- ^ Argument Index
302− Idris ()
285+elabProjection :: ElabInfo
286+ -> Name -- ^ Name of the argument in the constructor
287+ -> Name -- ^ Projection Name
288+ -> Plicity -- ^ Projection Plicity
289+ -> PTerm -- ^ Projection Type
290+ -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation
291+ -> SyntaxInfo -- ^ Projection SyntaxInfo
292+ -> FC -> PTerm -- ^ Projection target type
293+ -> Name -- ^ Data constructor tame
294+ -> [PArg] -- ^ Placeholder Arguments to constructor
295+ -> [Name] -- ^ All Field Names
296+ -> Int -- ^ Argument Index
297+ -> Idris ()
303298elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
304299 = do logLvl 1 $ "Generating Projection for " ++ show pname
305300
@@ -343,21 +338,20 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f
343338
344339-- | Creates and elaborates an update function.
345340-- If 'optional' is true, we will not fail if we can't elaborate the update function.
346−elabUpdate :: ElabInfo ->
347− Name -> -- ^ Name of the argument in the constructor
348− Name -> -- ^ Field Name
349− Plicity -> -- ^ Field Plicity
350− PTerm -> -- ^ Field Type
351− (Docstring (Either Err PTerm)) -> -- ^ Field Documentation
352− SyntaxInfo -> -- ^ Field SyntaxInfo
353− FC ->
354− PTerm -> -- ^ Projection Source Type
355− Name -> -- ^ Data Constructor Name
356− [PArg] -> -- ^ Arguments to constructor
357− [Name] -> -- ^ All fields
358− Int -> -- ^ Argument Index
359− Bool -> -- ^ Optional
360− Idris ()
341+elabUpdate :: ElabInfo
342+ -> Name -- ^ Name of the argument in the constructor
343+ -> Name -- ^ Field Name
344+ -> Plicity -- ^ Field Plicity
345+ -> PTerm -- ^ Field Type
346+ -> (Docstring (Either Err PTerm)) -- ^ Field Documentation
347+ -> SyntaxInfo -- ^ Field SyntaxInfo
348+ -> FC -> PTerm -- ^ Projection Source Type
349+ -> Name -- ^ Data Constructor Name
350+ -> [PArg] -- ^ Arguments to constructor
351+ -> [Name] -- ^ All fields
352+ -> Int -- ^ Argument Index
353+ -> Bool -- ^ Optional
354+ -> Idris ()
361355elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional
362356 = do logLvl 1 $ "Generating Update for " ++ show pname
363357