a3b40c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix generation of operator definitions

a3b40c2Edwin Brady10 years ago

src/Idris/CaseSplit.hs+20−5

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ import Idris.AbsSyntaxTree (Idris, IState, PTerm)

12import Idris.ElabDecls

13import Idris.Delaborate

14import Idris.Parser

15+import Idris.Parser.Helpers

15import Idris.Error

16import Idris.Error

16import Idris.Output

17import Idris.Output

@@ -368,6 +369,20 @@ nameRoot acc nm =

368 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

369 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

369 _ -> showSep "_" (acc ++ [nm])

370 _ -> showSep "_" (acc ++ [nm])

370

371

372+-- Show a name for use in pattern definitions on the lhs

373+showLHSName :: Name -> String

374+showLHSName n = let fn = show n in

375+ if any (flip elem opChars) fn

376+ then "(" ++ fn ++ ")"

377+ else fn

378+

379+-- Show a name for the purpose of generating a metavariable name on the rhs

380+showRHSName :: Name -> String

381+showRHSName n = let fn = show n in

382+ if any (flip elem opChars) fn

383+ then "op"

384+ else fn

385+

371getClause :: Int -- ^ line number that the type is declared on

386getClause :: Int -- ^ line number that the type is declared on

372 -> Name -- ^ Function name

387 -> Name -- ^ Function name

373 -> Name -- ^ User given name

388 -> Name -- ^ User given name

@@ -383,8 +398,8 @@ getClause l fn un fp

383 x -> x

398 x -> x

384 ist <- get

399 ist <- get

385 let ap = mkApp ist ty []

400 let ap = mkApp ist ty []

386− return (show un ++ " " ++ ap ++ "= ?"

401+ return (showLHSName un ++ " " ++ ap ++ "= ?"

387− ++ show un ++ "_rhs")

402+ ++ showRHSName un ++ "_rhs")

388 where mkApp :: IState -> PTerm -> [Name] -> String

403 where mkApp :: IState -> PTerm -> [Name] -> String

389 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

404 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

390 = let n = getNameFrom i used ty in

405 = let n = getNameFrom i used ty in

@@ -417,7 +432,7 @@ getClause l fn un fp

417 def (show (nsroot n)) ++ " "

432 def (show (nsroot n)) ++ " "

418 ++ mkApp i ty []

433 ++ mkApp i ty []

419 ++ "= ?"

434 ++ "= ?"

420− ++ show un ++ "_rhs_" ++ show m) ns [1..])

435+ ++ showRHSName un ++ "_rhs_" ++ show m) ns [1..])

421

436

422 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"

437 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"

423 def n = n

438 def n = n

@@ -431,7 +446,7 @@ getProofClause l fn fp

431 let ty = case ty_in of

446 let ty = case ty_in of

432 PTyped n t -> t

447 PTyped n t -> t

433 x -> x

448 x -> x

434− return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

449+ return (mkApp ty ++ " = ?" ++ showRHSName fn ++ "_rhs")

435 where mkApp (PPi _ _ _ _ sc) = mkApp sc

450 where mkApp (PPi _ _ _ _ sc) = mkApp sc

436 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

451 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

437

452

@@ -451,7 +466,7 @@ mkWith str n = let str' = replaceRHS str "with (_)"

451 newpat ('>':patstr) = '>':newpat patstr

466 newpat ('>':patstr) = '>':newpat patstr

452 newpat patstr =

467 newpat patstr =

453 " " ++

468 " " ++

454− replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"

469+ replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"

455

470

456-- Replace _ with names in missing clauses

471-- Replace _ with names in missing clauses

457

472