1c51b01 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

EXPERIMENTAL: Disambiguate names in a block

1c51b01Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+93−70

compare with master

unifiedsplit

@@ -22,6 +22,7 @@ import Control.Monad.State

23import Data.List

24import Data.Char

25+import qualified Data.Text as T

25import Data.Either

26import Data.Either

26import Data.Maybe

27import Data.Maybe

27import Data.Word (Word)

28import Data.Word (Word)

@@ -1194,71 +1195,83 @@ addImpl = addImpl' False [] []

1194-- and *not* inside a PHidden

1195-- and *not* inside a PHidden

1195

1196

1196addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1197addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1197−addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

1198+addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) [] ptm

1198 where

1199 where

1199− ai env (PRef fc f)

1200+ ai env ds (PRef fc f)

1200 | f `elem` infns = PInferRef fc f

1201 | f `elem` infns = PInferRef fc f

1201− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []

1202+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []

1202− ai env (PHidden (PRef fc f))

1203+ ai env ds (PHidden (PRef fc f))

1203− | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []

1204+ | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []

1204− ai env (PEq fc l r) = let l' = ai env l

1205+ ai env ds (PEq fc l r)

1206+ = let l' = ai env ds l

1205− r' = ai env r in

1207+ r' = ai env ds r in

1206− PEq fc l' r'

1208+ PEq fc l' r'

1207− ai env (PRewrite fc l r g) = let l' = ai env l

1209+ ai env ds (PRewrite fc l r g)

1210+ = let l' = ai env ds l

1208− r' = ai env r

1211+ r' = ai env ds r

1209− g' = fmap (ai env) g in

1212+ g' = fmap (ai env ds) g in

1210− PRewrite fc l' r' g'

1213+ PRewrite fc l' r' g'

1211− ai env (PTyped l r) = let l' = ai env l

1214+ ai env ds (PTyped l r)

1215+ = let l' = ai env ds l

1212− r' = ai env r in

1216+ r' = ai env ds r in

1213− PTyped l' r'

1217+ PTyped l' r'

1214− ai env (PPair fc l r) = let l' = ai env l

1218+ ai env ds (PPair fc l r)

1219+ = let l' = ai env ds l

1215− r' = ai env r in

1220+ r' = ai env ds r in

1216− PPair fc l' r'

1221+ PPair fc l' r'

1217− ai env (PDPair fc l t r) = let l' = ai env l

1222+ ai env ds (PDPair fc l t r)

1223+ = let l' = ai env ds l

1218− t' = ai env t

1224+ t' = ai env ds t

1219− r' = ai env r in

1225+ r' = ai env ds r in

1220− PDPair fc l' t' r'

1226+ PDPair fc l' t' r'

1221− ai env (PAlternative a as) = let as' = map (ai env) as in

1227+ ai env ds (PAlternative a as)

1228+ = let as' = map (ai env ds) as in

1222− PAlternative a as'

1229+ PAlternative a as'

1230+ ai env _ (PDisamb ds' as) = ai env ds' as

1223− ai env (PApp fc (PInferRef _ f) as)

1231+ ai env ds (PApp fc (PInferRef _ f) as)

1224− = let as' = map (fmap (ai env)) as in

1232+ = let as' = map (fmap (ai env ds)) as in

1225 PApp fc (PInferRef fc f) as'

1233 PApp fc (PInferRef fc f) as'

1226− ai env (PApp fc ftm@(PRef _ f) as)

1234+ ai env ds (PApp fc ftm@(PRef _ f) as)

1227− | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)

1235+ | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)

1228 | not (f `elem` map fst env)

1236 | not (f `elem` map fst env)

1229− = let as' = map (fmap (ai env)) as in

1237+ = let as' = map (fmap (ai env ds)) as in

1230− handleErr $ aiFn inpat False ist fc f as'

1238+ handleErr $ aiFn inpat False ist fc f ds as'

1231− | Just (Just ty) <- lookup f env

1239+ | Just (Just ty) <- lookup f env =

1232− = let as' = map (fmap (ai env)) as

1240+ let as' = map (fmap (ai env ds)) as

1233− arity = getPArity ty in

1241+ arity = getPArity ty in

1234− mkPApp fc arity ftm as'

1242+ mkPApp fc arity ftm as'

1235− ai env (PApp fc f as) = let f' = ai env f

1243+ ai env ds (PApp fc f as)

1244+ = let f' = ai env ds f

1236− as' = map (fmap (ai env)) as in

1245+ as' = map (fmap (ai env ds)) as in

1237− mkPApp fc 1 f' as'

1246+ mkPApp fc 1 f' as'

1238− ai env (PCase fc c os) = let c' = ai env c

1247+ ai env ds (PCase fc c os)

1248+ = let c' = ai env ds c

1239− os' = map (pmap (ai env)) os in

1249+ os' = map (pmap (ai env ds)) os in

1240− PCase fc c' os'

1250+ PCase fc c' os'

1241− ai env (PLam n ty sc) = let ty' = ai env ty

1251+ ai env ds (PLam n ty sc)

1252+ = let ty' = ai env ds ty

1242− sc' = ai ((n, Just ty):env) sc in

1253+ sc' = ai ((n, Just ty):env) ds sc in

1243− PLam n ty' sc'

1254+ PLam n ty' sc'

1244− ai env (PLet n ty val sc)

1255+ ai env ds (PLet n ty val sc)

1245− = let ty' = ai env ty

1256+ = let ty' = ai env ds ty

1246− val' = ai env val

1257+ val' = ai env ds val

1247− sc' = ai ((n, Just ty):env) sc in

1258+ sc' = ai ((n, Just ty):env) ds sc in

1248− PLet n ty' val' sc'

1259+ PLet n ty' val' sc'

1249− ai env (PPi p n ty sc) = let ty' = ai env ty

1260+ ai env ds (PPi p n ty sc)

1261+ = let ty' = ai env ds ty

1250− sc' = ai ((n, Just ty):env) sc in

1262+ sc' = ai ((n, Just ty):env) ds sc in

1251− PPi p n ty' sc'

1263+ PPi p n ty' sc'

1252− ai env (PGoal fc r n sc) = let r' = ai env r

1264+ ai env ds (PGoal fc r n sc)

1265+ = let r' = ai env ds r

1253− sc' = ai ((n, Nothing):env) sc in

1266+ sc' = ai ((n, Nothing):env) ds sc in

1254− PGoal fc r' n sc'

1267+ PGoal fc r' n sc'

1255− ai env (PHidden tm) = PHidden (ai env tm)

1268+ ai env ds (PHidden tm) = PHidden (ai env ds tm)

1256− ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

1269+ ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)

1257− ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1270+ ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)

1258− ai env (PRefl fc tm) = PRefl fc (ai env tm)

1271+ ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)

1259− ai env (PUnifyLog tm) = PUnifyLog (ai env tm)

1272+ ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)

1260− ai env (PNoImplicits tm) = PNoImplicits (ai env tm)

1273+ ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)

1261− ai env tm = tm

1274+ ai env ds tm = tm

1262

1275

1263 handleErr (Left err) = PElabError err

1276 handleErr (Left err) = PElabError err

1264 handleErr (Right x) = x

1277 handleErr (Right x) = x

@@ -1266,8 +1279,8 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

1266-- if in a pattern, and there are no arguments, and there's no possible

1279-- if in a pattern, and there are no arguments, and there's no possible

1267-- names with zero explicit arguments, don't add implicits.

1280-- names with zero explicit arguments, don't add implicits.

1268

1281

1269−aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

1282+aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1270−aiFn inpat True ist fc f []

1283+aiFn inpat True ist fc f ds []

1271 = case lookupDef f (tt_ctxt ist) of

1284 = case lookupDef f (tt_ctxt ist) of

1272 [] -> Right $ PPatvar fc f

1285 [] -> Right $ PPatvar fc f

1273 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1286 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1275,7 +1288,7 @@ aiFn inpat True ist fc f []

1275 if (not (vname f) || tcname f

1288 if (not (vname f) || tcname f

1276 || any (conCaf (tt_ctxt ist)) ialts)

1289 || any (conCaf (tt_ctxt ist)) ialts)

1277-- any constructor alts || any allImp ialts))

1290-- any constructor alts || any allImp ialts))

1278− then aiFn inpat False ist fc f [] -- use it as a constructor

1291+ then aiFn inpat False ist fc f ds [] -- use it as a constructor

1279 else Right $ PPatvar fc f

1292 else Right $ PPatvar fc f

1280 where imp (PExp _ _ _ _) = False

1293 where imp (PExp _ _ _ _) = False

1281 imp _ = True

1294 imp _ = True

@@ -1289,22 +1302,32 @@ aiFn inpat True ist fc f []

1289 vname (UN n) = True -- non qualified

1302 vname (UN n) = True -- non qualified

1290 vname _ = False

1303 vname _ = False

1291

1304

1292−aiFn inpat expat ist fc f as

1305+aiFn inpat expat ist fc f ds as

1293 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1306 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1294−aiFn inpat expat ist fc f as

1307+aiFn inpat expat ist fc f ds as

1295 -- This is where namespaces get resolved by adding PAlternative

1308 -- This is where namespaces get resolved by adding PAlternative

1296 = do let ns = lookupCtxtName f (idris_implicits ist)

1309 = do let ns = lookupCtxtName f (idris_implicits ist)

1297− let ns' = filter (\(n, _) -> notHidden n) ns

1310+ let nh = filter (\(n, _) -> notHidden n) ns

1311+ let ns' = case trimAlts ds nh of

1312+ [] -> nh

1313+ x -> x

1298 case ns' of

1314 case ns' of

1299 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1315 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1300 [] -> if f `elem` (map fst (idris_metavars ist))

1316 [] -> if f `elem` (map fst (idris_metavars ist))

1301 then Right $ PApp fc (PRef fc f) as

1317 then Right $ PApp fc (PRef fc f) as

1302 else Right $ mkPApp fc (length as) (PRef fc f) as

1318 else Right $ mkPApp fc (length as) (PRef fc f) as

1303 alts -> Right $

1319 alts -> Right $

1304− PAlternative True $

1320+ PAlternative True $

1305− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1321+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1306− (insertImpl ns as)) alts

1322+ (insertImpl ns as)) alts

1307 where

1323 where

1324+ trimAlts [] alts = alts

1325+ trimAlts ns alts

1326+ = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

1327+

1328+ nspace (NS _ s) = s

1329+ nspace _ = []

1330+

1308 notHidden n = case getAccessibility n of

1331 notHidden n = case getAccessibility n of

1309 Hidden -> False

1332 Hidden -> False

1310 _ -> True

1333 _ -> True

src/Idris/AbsSyntaxTree.hs+8

@@ -24,6 +24,7 @@ import Control.Monad.Trans.Error

25import Data.List

26import Data.Char

27+import qualified Data.Text as T

27import Data.Either

28import Data.Either

28import Data.Word (Word)

29import Data.Word (Word)

@@ -608,6 +609,7 @@ data PTerm = PQuote Raw

608 | PElabError Err -- ^ Error to report on elaboration

609 | PElabError Err -- ^ Error to report on elaboration

609 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

610 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

610 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

611 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

612+ | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces

611 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

613 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

612 | PNoImplicits PTerm -- ^ never run implicit converions on the term

614 | PNoImplicits PTerm -- ^ never run implicit converions on the term

613 deriving Eq

615 deriving Eq

@@ -638,6 +640,7 @@ mapPT f t = f (mpt t) where

638 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

640 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

639 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

641 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

640 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

642 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

643+ mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)

641 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)

644 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)

642 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

645 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)

643 mpt x = x

646 mpt x = x

@@ -1288,6 +1291,7 @@ showImp ist impl colour tm = se 10 [] tm where

1288 se p bnd (PElabError s) = show s

1291 se p bnd (PElabError s) = show s

1289 se p bnd (PCoerced t) = se p bnd t

1292 se p bnd (PCoerced t) = se p bnd t

1290 se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1293 se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1294+ se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t

1291 se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t

1295 se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t

1292-- se p bnd x = "Not implemented"

1296-- se p bnd x = "Not implemented"

1293

1297

@@ -1368,6 +1372,7 @@ instance Sized PTerm where

1368 size (PAlternative a alts) = 1 + size alts

1372 size (PAlternative a alts) = 1 + size alts

1369 size (PHidden hidden) = size hidden

1373 size (PHidden hidden) = size hidden

1370 size (PUnifyLog tm) = size tm

1374 size (PUnifyLog tm) = size tm

1375+ size (PDisamb _ tm) = size tm

1371 size (PNoImplicits tm) = size tm

1376 size (PNoImplicits tm) = size tm

1372 size PType = 1

1377 size PType = 1

1373 size (PConstant const) = 1 + size const

1378 size (PConstant const) = 1 + size const

@@ -1406,6 +1411,7 @@ allNamesIn tm = nub $ ni [] tm

1406 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1411 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1407 ni env (PAlternative a ls) = concatMap (ni env) ls

1412 ni env (PAlternative a ls) = concatMap (ni env) ls

1408 ni env (PUnifyLog tm) = ni env tm

1413 ni env (PUnifyLog tm) = ni env tm

1414+ ni env (PDisamb _ tm) = ni env tm

1409 ni env (PNoImplicits tm) = ni env tm

1415 ni env (PNoImplicits tm) = ni env tm

1410 ni env _ = []

1416 ni env _ = []

1411

1417

@@ -1433,6 +1439,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1433 ni env (PAlternative a as) = concatMap (ni env) as

1439 ni env (PAlternative a as) = concatMap (ni env) as

1434 ni env (PHidden tm) = ni env tm

1440 ni env (PHidden tm) = ni env tm

1435 ni env (PUnifyLog tm) = ni env tm

1441 ni env (PUnifyLog tm) = ni env tm

1442+ ni env (PDisamb _ tm) = ni env tm

1436 ni env (PNoImplicits tm) = ni env tm

1443 ni env (PNoImplicits tm) = ni env tm

1437 ni env _ = []

1444 ni env _ = []

1438

1445

@@ -1460,6 +1467,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1460 ni env (PAlternative a as) = concatMap (ni env) as

1467 ni env (PAlternative a as) = concatMap (ni env) as

1461 ni env (PHidden tm) = ni env tm

1468 ni env (PHidden tm) = ni env tm

1462 ni env (PUnifyLog tm) = ni env tm

1469 ni env (PUnifyLog tm) = ni env tm

1470+ ni env (PDisamb _ tm) = ni env tm

1463 ni env (PNoImplicits tm) = ni env tm

1471 ni env (PNoImplicits tm) = ni env tm

1464 ni env _ = []

1472 ni env _ = []

1465

1473

src/Idris/DSL.hs+1

@@ -44,6 +44,7 @@ expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

44expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

45expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

46expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)

47+expandDo dsl (PDisamb ns t) = PDisamb ns (expandDo dsl t)

47expandDo dsl (PReturn fc) = dsl_return dsl

48expandDo dsl (PReturn fc) = dsl_return dsl

48expandDo dsl (PRewrite fc r t ty)

49expandDo dsl (PRewrite fc r t ty)

49 = PRewrite fc r (expandDo dsl t) ty

50 = PRewrite fc r (expandDo dsl t) ty

src/Idris/ParseExpr.hs+14

@@ -190,6 +190,7 @@ internalExpr syn =

190 try (app syn)

191 <|> try (matchApp syn)

192 <|> try (unifyLog syn)

193+ <|> try (disamb syn)

193 <|> try (noImplicits syn)

194 <|> try (noImplicits syn)

194 <|> recordType syn

195 <|> recordType syn

195 <|> lambda syn

196 <|> lambda syn

@@ -483,6 +484,19 @@ unifyLog syn = do lchar '%'; reserved "unifyLog";

483 return (PUnifyLog tm)

484 return (PUnifyLog tm)

484 <?> "unification log expression"

485 <?> "unification log expression"

485

486

487+{- | Parses a disambiguation expression

488+Disamb ::=

489+ '%' 'disamb' NameList Expr

490+ ;

491+-}

492+disamb :: SyntaxInfo -> IdrisParser PTerm

493+disamb syn = do reserved "with";

494+ ns <- sepBy1 name (lchar ',')

495+ tm <- expr' syn

496+ return (PDisamb (map tons ns) tm)

497+ <?> "unification log expression"

498+ where tons (NS n s) = txt (show n) : s

499+ tons n = [txt (show n)]

486{- | Parses a no implicits expression

500{- | Parses a no implicits expression

487@

501@

488NoImplicits ::=

502NoImplicits ::=