diff --git a/TODO.md b/TODO.md index 7190b72..18bf960 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,7 @@ ## TODO -- [ ] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this. +- [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this. - [ ] Remove context lambdas when printing solutions (show names from context) - build list of names and strip λ, then call pprint with names - [ ] Check for shadowing when declaring dcon diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index b8f7612..7c5a2c1 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -225,7 +225,8 @@ varname = (ident <|> uident <|> keyword "_" *> pure "_") ebind : Parser (List (FC, String, Icit, Raw)) ebind = do -- don't commit until we see the ":" - names <- try (sym "(" *> some (withPos varname) <* sym ":") + sym "(" + names <- try (some (withPos varname) <* sym ":") ty <- typeExpr sym ")" pure $ map (\(pos, name) => (pos, name, Explicit, ty)) names @@ -234,18 +235,18 @@ ibind : Parser (List (FC, String, Icit, Raw)) ibind = do sym "{" -- REVIEW - I have name required and type optional, which I think is the opposite of what I expect - names <- some $ withPos varname - ty <- optional (sym ":" >> typeExpr) + names <- try (some (withPos varname) <* sym ":") + ty <- typeExpr sym "}" - pure $ map (\(pos,name) => (pos, name, Implicit, fromMaybe (RImplicit pos) ty)) names + pure $ map (\(pos,name) => (pos, name, Implicit, ty)) names abind : Parser (List (FC, String, Icit, Raw)) abind = do sym "{{" - names <- some $ withPos varname - ty <- optional (sym ":" >> typeExpr) + names <- try (some (withPos varname) <* sym ":") + ty <- typeExpr sym "}}" - pure $ map (\(pos,name) => (pos, name, Auto, fromMaybe (RImplicit pos) ty)) names + pure $ map (\(pos,name) => (pos, name, Auto, ty)) names arrow : Parser Unit arrow = sym "->" <|> sym "→" diff --git a/tests/black/Zoo4eg.newt b/tests/black/Zoo4eg.newt index a778d25..0ad46c7 100644 --- a/tests/black/Zoo4eg.newt +++ b/tests/black/Zoo4eg.newt @@ -4,14 +4,14 @@ id : {A : U} -> A -> A id = \x => x -- elaborated to \{A} x. x -- implicit arg types can be omitted -const : {A B} -> A -> B -> A +const : {A B : U} -> A -> B -> A const = \x y => x -- function arguments can be grouped: group1 : {A B : U}(x y z : A) -> B -> B group1 = \x y z b => b -group2 : {A B}(x y z : A) -> B -> B +group2 : {A B : U}(x y z : A) -> B -> B group2 = \x y z b => b -- explicit id function used for annotation as in Idris @@ -43,20 +43,20 @@ false = \B t f => f List : U -> U List = \A => (L : _) -> (A -> L -> L) -> L -> L -nil : {A} -> List A +nil : {A : U} -> List A nil = \L cons nil => nil -cons : {A} -> A -> List A -> List A +cons : {A : U} -> A -> List A -> List A cons = \ x xs L cons nil => cons x (xs L cons nil) -map : {A B} -> (A -> B) -> List A -> List B +map : {A B : U} -> (A -> B) -> List A -> List B map = \{A} {B} f xs L c n => xs L (\a => c (f a)) n list1 : List Bool list1 = cons true (cons false (cons true nil)) -- dependent function composition -comp : {A} {B : A -> U} {C : {a : A} -> B a -> U} +comp : {A : U} {B : A -> U} {C : {a : A} -> B a -> U} (f : {a : A} (b : B a) -> C b) (g : (a : A) -> B a) (a : A) @@ -80,13 +80,13 @@ hundred : _ hundred = mul ten ten -- Leibniz equality -Eq : {A} -> A -> A -> U +Eq : {A: U} -> A -> A -> U Eq = \{A} x y => (P : A -> U) -> P x -> P y -refl : {A} {x : A} -> Eq x x +refl : {A : U} {x : A} -> Eq x x refl = \_ px => px -sym : {A x y} -> Eq {A} x y -> Eq y x +sym : {A x y : _} -> Eq {A} x y -> Eq y x sym = \p => p (\y => Eq y x) refl eqtest : Eq (mul ten ten) hundred