0c27247 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow class names to be infix

Use case: class (:<:) (f : Type -> Type) (g : Type -> Type) where isSubFun : SubFunctor f g

commit0c27247d9b9c4d5d771eecf490cd41f9e4d58e61 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 30 Jan 2014, 16:21 (13 years ago) parent60abf37

1 file changed+2−2

compare with master

unifiedsplit

src/Idris/Parser.hs+2−2

src/Idris/Parser.hs+2−2

@@ -561,7 +561,7 @@ class_ syn = do (doc, acc) <- try (do

561561 doc <- option "" (docComment '|')

562562 acc <- optional accessibility

563563 return (doc, acc))

564− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name

564+ reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

565565 let n = expandNS syn n_in

566566 cs <- many carg

567567 ds <- option [] (classBlock syn)

@@ -591,7 +591,7 @@ instance_ :: SyntaxInfo -> IdrisParser [PDecl]

591591instance_ syn = do reserved "instance"; fc <- getFC

592592 en <- optional instanceName

593593 cs <- constraintList syn

594− cn <- name

594+ cn <- fnName

595595 args <- many (simpleExpr syn)

596596 let sc = PApp fc (PRef fc cn) (map pexp args)

597597 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc