@@ -15,7 +15,7 @@ import Data.Maybe
1515import Data.List
1616import Control.Monad
1717
18−elabRecord :: ElabInfo ->
18+elabRecord :: ElabInfo ->
1919 (Docstring (Either Err PTerm)) ->
2020 SyntaxInfo ->
2121 FC ->
@@ -23,13 +23,12 @@ elabRecord :: ElabInfo ->
2323 Name -> -- ^ Record Type Name
2424 [(Name, Plicity, PTerm)] -> -- ^ Parameters
2525 [(Name, Docstring (Either Err PTerm))] -> -- ^ Parameter Docs
26− [(Name, Plicity, PTerm)] -> -- ^ Fields
27− [(Name, Docstring (Either Err PTerm))] -> -- ^ Field Docs
26+ [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> -- ^ Fields
2827 Maybe Name -> -- ^ Constructor Name
2928 (Docstring (Either Err PTerm)) -> -- ^ Constructor Doc
3029 SyntaxInfo -> -- ^ Constructor SyntaxInfo
3130 Idris ()
32−elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdoc csyn
31+elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
3332 = do logLvl 1 $ "Building data declaration for " ++ show tyn
3433 -- Type constructor
3534 let tycon = generateTyConType params
@@ -37,16 +36,105 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
3736
3837 -- Data constructor
3938 dconName <- generateDConName cname
40− let dconTy = generateDConType params fields
39+ let dconTy = generateDConType params fieldsWithNameAndDoc
4140 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
42−
41+
4342 -- Build data declaration for elaboration
44− let datadecl = PDatadecl tyn tycon [(cdoc, [], dconName, dconTy, fc, [])]
45− elabData info rsyn doc [] fc opts datadecl
43+ let datadecl = PDatadecl tyn tycon [(cdoc, dconsArgDocs, dconName, dconTy, fc, [])]
44+ elabData info rsyn doc paramDocs fc opts datadecl
45+
46+ iLOG $ "fieldsWithName " ++ show fieldsWithName
47+ iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
48+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
49+ where
50+ -- | Generates a type constructor.
51+ generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
52+ generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
53+ generateTyConType [] = PType
4654
47− i <- getIState
55+ -- | Generates a name for the data constructor if none was specified.
56+ generateDConName :: Maybe Name -> Idris Name
57+ generateDConName (Just n) = return $ expandNS csyn n
58+ generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
59+ where
60+ uniqueName :: Name -> Idris Name
61+ uniqueName n = do i <- getIState
62+ case lookupTyNameExact n (tt_ctxt i) of
63+ Just _ -> uniqueName (nextName n)
64+ Nothing -> return n
65+
66+ -- | Generates the data constructor type.
67+ generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm
68+ generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
69+ generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) t (generateDConType [] as)
70+ generateDConType [] [] = target
71+
72+ -- | The target for the constructor and projection functions. Also the source of the update functions.
73+ target :: PTerm
74+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, _) <- params]
75+
76+ paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
77+ paramsAndDoc = pad params paramDocs
78+ where
79+ pad :: [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
80+ pad ((n, p, t) : rest) docs
81+ = let d = case lookup n docs of
82+ Just d' -> d
83+ Nothing -> emptyDocstring
84+ in (n, p, t, d) : (pad rest docs)
85+ pad _ _ = []
86+
87+ dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
88+ dconsArgDocs = paramDocs ++ (dcad fieldsWithName)
89+ where
90+ dcad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]
91+ dcad ((n, _, _, (Just d)) : rest) = (n, d) : (dcad rest)
92+ dcad (_ : rest) = dcad rest
93+ dcad [] = []
94+
95+ fieldsWithName :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
96+ fieldsWithName = fwn [] fields
97+ where
98+ fwn :: [Name] -> [(Maybe Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
99+ fwn ns ((n, p, t, d) : rest)
100+ = let nn = case n of
101+ Just n' -> n'
102+ Nothing -> newName ns baseName
103+ in (expandNS rsyn $ nn, p, t, d) : (fwn (nn : ns) rest)
104+ fwn _ _ = []
105+
106+ baseName = sUN "__pi_arg"
107+
108+ newName :: [Name] -> Name -> Name
109+ newName ns n
110+ | n `elem` ns = newName ns (nextName n)
111+ | otherwise = n
112+
113+ fieldsWithNameAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
114+ fieldsWithNameAndDoc = fwnad fieldsWithName
115+ where
116+ fwnad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
117+ fwnad ((n, p, t, d) : rest)
118+ = let doc = fromMaybe emptyDocstring d
119+ in (n, p, t, doc) : (fwnad rest)
120+ fwnad [] = []
48121
122+elabRecordFunctions :: ElabInfo ->
123+ SyntaxInfo ->
124+ FC ->
125+ Name -> -- ^ Record Type Name
126+ [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -> -- ^ Parameters
127+ [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]-> -- ^ Fields
128+ Name -> -- ^ Constructor Name
129+ PTerm -> -- ^ Target Type
130+ Idris ()
131+elabRecordFunctions info rsyn fc tyn params fields dconName target
132+ = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn
133+
134+ iLOG $ "Fields: " ++ show fieldNames
135+ iLOG $ "Params: " ++ show paramNames
49136 -- The elaborated constructor type for the data declaration
137+ i <- getIState
50138 ttConsTy <-
51139 case lookupTyExact dconName (tt_ctxt i) of
52140 Just as -> return as
@@ -54,15 +142,17 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
54142
55143 -- The arguments to the constructor
56144 let constructorArgs = getArgTys ttConsTy
145+ iLOG $ "Cons args: " ++ show constructorArgs
146+ iLOG $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
57147 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
58148 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
59149
60150 -- The parameters for elaboration with their documentation
61151 -- Parameter functions are all prefixed with "param_".
62− let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, t, d) <- zipParams i params paramDocs]
152+ let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, t, d) <- params] -- zipParams i params paramDocs]
63153
64154 -- The fields (written by the user) with their documentation.
65− let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
155+ let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, p, t, d) <- fields]
66156
67157 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
68158 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
@@ -78,46 +168,16 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
78168 -- Build and elaborate update functions
79169 elabUp dconName updaters
80170 where
81− -- | Generates a type constructor.
82− generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
83− generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
84− generateTyConType [] = PType
85−
86− -- | Generates a name for the data constructor if none was specified.
87− generateDConName :: Maybe Name -> Idris Name
88− generateDConName (Just n) = return $ expandNS csyn n
89− generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
90− where
91− uniqueName :: Name -> Idris Name
92− uniqueName n = do i <- getIState
93− case lookupTyNameExact n (tt_ctxt i) of
94− Just _ -> uniqueName (nextName n)
95− Nothing -> return n
96−
97− -- | Generates the data constructor type.
98− generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
99− generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
100− generateDConType [] ((n, p, t) : as) = PPi p (nsroot n) t (generateDConType [] as)
101− generateDConType [] [] = target
102−
103− -- | Creates an PArg from a plicity and a name where the term is a PRef.
104− asPRefArg :: Plicity -> Name -> PArg
105− asPRefArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)
106−
107− -- | The target for the constructor and projection functions. Also the source of the update functions.
108− target :: PTerm
109− target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, t) <- params]
110−
111171 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
112172 placeholderArg :: Plicity -> Name -> PArg
113173 placeholderArg p n = asArg p (nsroot n) Placeholder
114174
115175 -- | Root names of all fields in the current record declarations
116176 fieldNames :: [Name]
117− fieldNames = [nsroot n | (n, _, _) <- fields]
177+ fieldNames = [nsroot n | (n, _, _, _) <- fields]
118178
119179 paramNames :: [Name]
120− paramNames = [nsroot n | (n, _, _) <- params]
180+ paramNames = [nsroot n | (n, _, _, _) <- params]
121181
122182 isFieldOrParam :: Name -> Bool
123183 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
@@ -132,7 +192,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
132192 isField' (n, _, _, _, _, _) = isField n
133193
134194 fieldTerms :: [PTerm]
135− fieldTerms = [t | (_, _, t) <- fields]
195+ fieldTerms = [t | (_, _, t, _) <- fields]
136196
137197 -- Delabs the TT to PTerm
138198 -- This is not good.
@@ -186,7 +246,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
186246
187247 -- | A map from a field name to the other fields it depends on.
188248 fieldDependencies :: [(Name, [Name])]
189− fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]
249+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]
190250 where
191251 fieldDep :: Name -> PTerm -> (Name, [Name])
192252 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
@@ -363,3 +423,7 @@ projectInType xs = mapPT st
363423 st (PRef fc n)
364424 | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
365425 st t = t
426+
427+-- | Creates an PArg from a plicity and a name where the term is a PRef.
428+asPRefArg :: Plicity -> Name -> PArg
429+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)