@@ -63,24 +63,27 @@ elabInstance :: ElabInfo -> SyntaxInfo ->
63 Maybe Name -> -- explicit name
63 Maybe Name -> -- explicit name
64 [PDecl] -> Idris ()
64 [PDecl] -> Idris ()
65elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do
65elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do
66− i <- getIState
66+ ist <- getIState
67− (n, ci) <- case lookupCtxtName n (idris_classes i) of
67+ (n, ci) <- case lookupCtxtName n (idris_classes ist) of
68 [c] -> return c
68 [c] -> return c
69 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
69 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
70 cs -> tclift $ tfail $ At fc
70 cs -> tclift $ tfail $ At fc
71 (CantResolveAlts (map fst cs))
71 (CantResolveAlts (map fst cs))
72 let constraint = PApp fc (PRef fc [] n) (map pexp ps)
72 let constraint = PApp fc (PRef fc [] n) (map pexp ps)
73 let iname = mkiname n (namespace info) ps expn
73 let iname = mkiname n (namespace info) ps expn
74− putIState (i { hide_list = addDef iname acc (hide_list i) })
74+ putIState (ist { hide_list = addDef iname acc (hide_list ist) })
75− i <- getIState
75+ ist <- getIState
77+ let totopts = if default_total ist then [TotalFn, Dictionary]
77 let emptyclass = null (class_methods ci)
80 let emptyclass = null (class_methods ci)
78 when (what /= EDefns) $ do
81 when (what /= EDefns) $ do
79− nty <- elabType' True info syn doc argDocs fc [] iname NoFC t
82+ nty <- elabType' True info syn doc argDocs fc totopts iname NoFC t
80 -- if the instance type matches any of the instances we have already,
83 -- if the instance type matches any of the instances we have already,
81 -- and it's not a named instance, then it's overlapping, so report an error
84 -- and it's not a named instance, then it's overlapping, so report an error
82 case expn of
85 case expn of
83− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))
86+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (class_determiners ci) (delab ist nty))
84 (map fst $ class_instances ci)
87 (map fst $ class_instances ci)
85 addInstance intInst True n iname
88 addInstance intInst True n iname
86 Just _ -> addInstance intInst False n iname
89 Just _ -> addInstance intInst False n iname
@@ -99,7 +102,7 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do
99 let pnames = nub $ map pname (concat (nub wparams)) ++
102 let pnames = nub $ map pname (concat (nub wparams)) ++
100 concatMap (namesIn [] ist) ps
103 concatMap (namesIn [] ist) ps
101 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
104 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
102− undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
105+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances
103 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
106 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
104 let all_meths = map (nsroot . fst) (class_methods ci)
107 let all_meths = map (nsroot . fst) (class_methods ci)
105 let mtys = map (\ (n, (op, t)) ->
108 let mtys = map (\ (n, (op, t)) ->
@@ -112,7 +115,7 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do
112 (class_methods ci)
115 (class_methods ci)
113 logElab 3 (show (mtys, ips))
116 logElab 3 (show (mtys, ips))
114 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))
117 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))
115− let ds_defs = insertDefaults i iname (class_defaults ci) ns ds
118+ let ds_defs = insertDefaults ist iname (class_defaults ci) ns ds
116 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
119 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
117 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs
120 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs
118 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
121 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
@@ -138,10 +141,10 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do
138 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))
141 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))
139 (map (pexp . mkMethApp) mtys)
142 (map (pexp . mkMethApp) mtys)
141− logElab 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
144+ logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ show lhs ++ " " ++ show headVars
142 logElab 5 $ "Instance RHS " ++ show rhs
145 logElab 5 $ "Instance RHS " ++ show rhs
144− let idecls = [PClauses fc [Dictionary] iname
147+ let idecls = [PClauses fc totopts iname
145 [PClause fc iname lhs [] rhs wb]]
148 [PClause fc iname lhs [] rhs wb]]
146 logElab 1 (show idecls)
149 logElab 1 (show idecls)
147 push_estack iname True
150 push_estack iname True