@@ -12,6 +12,7 @@ import Idris.AbsSyntaxTree (Idris, IState, PTerm)
1212import Idris.ElabDecls
1313import Idris.Delaborate
1414import Idris.Parser
15+import Idris.Parser.Helpers
1516import Idris.Error
1617import Idris.Output
1718
@@ -368,6 +369,20 @@ nameRoot acc nm =
368369 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
369370 _ -> showSep "_" (acc ++ [nm])
370371
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+
371386getClause :: Int -- ^ line number that the type is declared on
372387 -> Name -- ^ Function name
373388 -> Name -- ^ User given name
@@ -383,8 +398,8 @@ getClause l fn un fp
383398 x -> x
384399 ist <- get
385400 let ap = mkApp ist ty []
386− return (show un ++ " " ++ ap ++ "= ?"
387− ++ show un ++ "_rhs")
401+ return (showLHSName un ++ " " ++ ap ++ "= ?"
402+ ++ showRHSName un ++ "_rhs")
388403 where mkApp :: IState -> PTerm -> [Name] -> String
389404 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
390405 = let n = getNameFrom i used ty in
@@ -417,7 +432,7 @@ getClause l fn un fp
417432 def (show (nsroot n)) ++ " "
418433 ++ mkApp i ty []
419434 ++ "= ?"
420− ++ show un ++ "_rhs_" ++ show m) ns [1..])
435+ ++ showRHSName un ++ "_rhs_" ++ show m) ns [1..])
421436
422437 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
423438 def n = n
@@ -431,7 +446,7 @@ getProofClause l fn fp
431446 let ty = case ty_in of
432447 PTyped n t -> t
433448 x -> x
434− return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
449+ return (mkApp ty ++ " = ?" ++ showRHSName fn ++ "_rhs")
435450 where mkApp (PPi _ _ _ _ sc) = mkApp sc
436451 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
437452
@@ -451,7 +466,7 @@ mkWith str n = let str' = replaceRHS str "with (_)"
451466 newpat ('>':patstr) = '>':newpat patstr
452467 newpat patstr =
453468 " " ++
454− replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
469+ replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"
455470
456471-- Replace _ with names in missing clauses
457472