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

git.iko.soy/Idris-dev

EXPERIMENTAL: Disambiguate names in a block

Syntax: with <names list> expr In the expr, if there are any ambiguous names which are defined in any of the modules in the <names list>, restrict the options to that list. e.g. *disamb> with List [1,2,3,4] [1,2,3,4] : List Integer *disamb> with List [[1,2],[3,4],[5,6]] [[1,2],[3,4],[5,6]] : List (List Integer) *disamb> with Vect [[1,2],[3,4],[5,6]] [[1,2],[3,4],[5,6]] : Vect 3 (Vect 2 Integer) -- Fails since both options work *disamb> with Vect, List [[1,2],[3,4],[5,6]] Can't disambiguate name: Prelude.List.::, Prelude.Vect.:: -- Succeeds since only one option works *disamb> with Vect, Stream [[1,2],[3,4],[5,6]] [[1,2],[3,4],[5,6]] : Vect 3 (Vect 2 Integer) This is really intended for disambiguating more complex or awkward things, e.g. (>>=) can be disambiguated as follows: foo = with Effects do putStrLn "Hello" --- etc

commit1c51b0131f2f44e08b81f81ad002360211695e47 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Jan 2014, 00:19 (13 years ago) parentd82f5fe

4 files changed+116−70

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+93−70 src/Idris/AbsSyntaxTree.hs+8 src/Idris/DSL.hs+1 src/Idris/ParseExpr.hs+14

src/Idris/AbsSyntax.hs+93−70

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

2222

2323import Data.List

2424import Data.Char

25+import qualified Data.Text as T

2526import Data.Either

2627import Data.Maybe

2728import Data.Word (Word)

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

11941195-- and *not* inside a PHidden

11951196

11961197addImpl' :: 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

11981199 where

1199− ai env (PRef fc f)

1200+ ai env ds (PRef fc f)

12001201 | f `elem` infns = PInferRef fc f

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

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

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

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

1205− r' = ai env r in

1206− PEq fc l' r'

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

1208− r' = ai env r

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

1210− PRewrite fc l' r' g'

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

1212− r' = ai env r in

1213− PTyped l' r'

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

1215− r' = ai env r in

1216− PPair fc l' r'

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

1218− t' = ai env t

1219− r' = ai env r in

1220− PDPair fc l' t' r'

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

1222− PAlternative a as'

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

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

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

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

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

1205+ ai env ds (PEq fc l r)

1206+ = let l' = ai env ds l

1207+ r' = ai env ds r in

1208+ PEq fc l' r'

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

1210+ = let l' = ai env ds l

1211+ r' = ai env ds r

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

1213+ PRewrite fc l' r' g'

1214+ ai env ds (PTyped l r)

1215+ = let l' = ai env ds l

1216+ r' = ai env ds r in

1217+ PTyped l' r'

1218+ ai env ds (PPair fc l r)

1219+ = let l' = ai env ds l

1220+ r' = ai env ds r in

1221+ PPair fc l' r'

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

1223+ = let l' = ai env ds l

1224+ t' = ai env ds t

1225+ r' = ai env ds r in

1226+ PDPair fc l' t' r'

1227+ ai env ds (PAlternative a as)

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

1229+ PAlternative a as'

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

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

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

12251233 PApp fc (PInferRef fc f) as'

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

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

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

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

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

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

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

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

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

1233− arity = getPArity ty in

1234− mkPApp fc arity ftm as'

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

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

1237− mkPApp fc 1 f' as'

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

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

1240− PCase fc c' os'

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

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

1243− PLam n ty' sc'

1244− ai env (PLet n ty val sc)

1245− = let ty' = ai env ty

1246− val' = ai env val

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

1248− PLet n ty' val' sc'

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

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

1251− PPi p n ty' sc'

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

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

1254− PGoal fc r' n sc'

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

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

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

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

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

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

1261− ai env tm = tm

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

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

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

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

1241+ arity = getPArity ty in

1242+ mkPApp fc arity ftm as'

1243+ ai env ds (PApp fc f as)

1244+ = let f' = ai env ds f

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

1246+ mkPApp fc 1 f' as'

1247+ ai env ds (PCase fc c os)

1248+ = let c' = ai env ds c

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

1250+ PCase fc c' os'

1251+ ai env ds (PLam n ty sc)

1252+ = let ty' = ai env ds ty

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

1254+ PLam n ty' sc'

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

1256+ = let ty' = ai env ds ty

1257+ val' = ai env ds val

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

1259+ PLet n ty' val' sc'

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

1261+ = let ty' = ai env ds ty

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

1263+ PPi p n ty' sc'

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

1265+ = let r' = ai env ds r

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

1267+ PGoal fc r' n sc'

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

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

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

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

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

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

1274+ ai env ds tm = tm

12621275

12631276 handleErr (Left err) = PElabError err

12641277 handleErr (Right x) = x

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

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

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

12681281

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

1270−aiFn inpat True ist fc f []

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

1283+aiFn inpat True ist fc f ds []

12711284 = case lookupDef f (tt_ctxt ist) of

12721285 [] -> Right $ PPatvar fc f

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

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

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

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

12771290-- 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

12791292 else Right $ PPatvar fc f

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

12811294 imp _ = True

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

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

12901303 vname _ = False

12911304

1292−aiFn inpat expat ist fc f as

1305+aiFn inpat expat ist fc f ds as

12931306 | 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

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

12961309 = 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

12981314 case ns' of

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

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

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

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

13031319 alts -> Right $

1304− PAlternative True $

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

1306− (insertImpl ns as)) alts

1320+ PAlternative True $

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

1322+ (insertImpl ns as)) alts

13071323 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+

13081331 notHidden n = case getAccessibility n of

13091332 Hidden -> False

13101333 _ -> True

src/Idris/AbsSyntaxTree.hs+8

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

2424

2525import Data.List

2626import Data.Char

27+import qualified Data.Text as T

2728import Data.Either

2829import Data.Word (Word)

2930

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

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

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

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

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

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

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

613615 deriving Eq

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

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

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

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

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

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

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

643646 mpt x = x

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

12881291 se p bnd (PElabError s) = show s

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

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

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

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

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

12931297

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

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

13691373 size (PHidden hidden) = size hidden

13701374 size (PUnifyLog tm) = size tm

1375+ size (PDisamb _ tm) = size tm

13711376 size (PNoImplicits tm) = size tm

13721377 size PType = 1

13731378 size (PConstant const) = 1 + size const

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

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

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

14081413 ni env (PUnifyLog tm) = ni env tm

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

14091415 ni env (PNoImplicits tm) = ni env tm

14101416 ni env _ = []

14111417

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

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

14341440 ni env (PHidden tm) = ni env tm

14351441 ni env (PUnifyLog tm) = ni env tm

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

14361443 ni env (PNoImplicits tm) = ni env tm

14371444 ni env _ = []

14381445

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

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

14611468 ni env (PHidden tm) = ni env tm

14621469 ni env (PUnifyLog tm) = ni env tm

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

14631471 ni env (PNoImplicits tm) = ni env tm

14641472 ni env _ = []

14651473

src/Idris/DSL.hs+1

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

4444expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

4545expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

4646expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)

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

4748expandDo dsl (PReturn fc) = dsl_return dsl

4849expandDo dsl (PRewrite fc r t ty)

4950 = PRewrite fc r (expandDo dsl t) ty

src/Idris/ParseExpr.hs+14

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

190190 try (app syn)

191191 <|> try (matchApp syn)

192192 <|> try (unifyLog syn)

193+ <|> try (disamb syn)

193194 <|> try (noImplicits syn)

194195 <|> recordType syn

195196 <|> lambda syn

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

483484 return (PUnifyLog tm)

484485 <?> "unification log expression"

485486

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)]

486500{- | Parses a no implicits expression

487501@

488502NoImplicits ::=