@@ -18,10 +18,10 @@ import Debug.Trace
19import Control.Monad.State.Strict
19import Control.Monad.State.Strict
21−-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
21+-- | Generate a pattern from an 'impossible' LHS.
23+-- We need this to eliminate the pattern clauses which have been
22−-- pattern clauses which have been provided explicitly from new clause
24+-- provided explicitly from new clause generation.
25mkPatTm :: PTerm -> Idris Term
25mkPatTm :: PTerm -> Idris Term
26mkPatTm t = do i <- getIState
26mkPatTm t = do i <- getIState
27 let timp = addImpl' True [] [] i t
27 let timp = addImpl' True [] [] i t
@@ -44,13 +44,12 @@ mkPatTm t = do i <- getIState
44 deNS (PRef f (NS n _)) = PRef f n
44 deNS (PRef f (NS n _)) = PRef f n
45 deNS t = t
45 deNS t = t
47−-- Given a list of LHSs, generate a extra clauses which cover the remaining
47+-- | Given a list of LHSs, generate a extra clauses which cover the remaining
48−-- cases. The ones which haven't been provided are marked 'absurd' so that the
48+-- cases. The ones which haven't been provided are marked 'absurd' so
49−-- checker will make sure they can't happen.
49+-- that the checker will make sure they can't happen.
51-- This will only work after the given clauses have been typechecked and the
51-- This will only work after the given clauses have been typechecked and the
52-- names are fully explicit!
52-- names are fully explicit!
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
53genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
55genClauses fc n xs given
54genClauses fc n xs given
56 = do i <- getIState
55 = do i <- getIState