Skip to content

Commit

Permalink
update comment documentation strings
Browse files Browse the repository at this point in the history
  • Loading branch information
andrevidela committed Dec 15, 2023
1 parent dbe4803 commit 1230a76
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 15 deletions.
14 changes: 7 additions & 7 deletions src/Core/TT.idr
Original file line number Diff line number Diff line change
Expand Up @@ -173,25 +173,25 @@ Eq FixityInfo where
-- Left-hand-side information for operators, carries autobind information
-- an operator can either be
-- - not autobind, a regular operator
-- - binding types, such that (nm : ty ** fn nm) desugars into (ty ** \(nm : ty) => fn nm)
-- - binding types, such that `(nm : ty) =@ fn nm` desugars into `(=@) ty (\(nm : ty) => fn nm)`
-- - binding expressing with an inferred type such that
-- (nm := exp ** fn nm) desugars into (exp ** \(nm : ?) => fn nm)
-- `(nm := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)`
-- - binding both types and expression such that
-- (nm : ty := exp ** fn nm) desugars into (exp ** \(nm : ty) => fn nm)
-- `(nm : ty := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)`
public export
data OperatorLHSInfo : tm -> Type where
-- Traditional operator wihtout binding, carries the lhs
NoBinder : (lhs : tm) -> OperatorLHSInfo tm
-- (nm : ty) ** fn x
-- (nm : ty) =@ fn x
BindType : (name : WithBounds Name) -> (ty : tm) -> OperatorLHSInfo tm
-- (nm := exp) ** fn nm
-- (nm := exp) =@ fn nm
BindExpr : (name : WithBounds Name) -> (expr : tm) -> OperatorLHSInfo tm
-- (nm : ty := exp) ** fn nm
-- (nm : ty := exp) =@ fn nm
BindExplicitType : (name : WithBounds Name) -> (type, expr : tm) -> OperatorLHSInfo tm

export
Show (OperatorLHSInfo tm) where
show (NoBinder lhs) = "regular"
show (NoBinder lhs) = "regular"
show (BindType name ty) = "type-binding (typebind)"
show (BindExpr name expr) = "automatically-binding (autobind)"
show (BindExplicitType name type expr) = "automatically-binding (autobind)"
Expand Down
6 changes: 3 additions & 3 deletions src/Idris/Desugar.idr
Original file line number Diff line number Diff line change
Expand Up @@ -780,19 +780,19 @@ mutual
= do l' <- desugarTree side ps l
r' <- desugarTree side ps r
pure (IApp loc (IApp loc (IVar opFC op) l') r')
-- (x : ty ** f x) ==>> (**) exp (\x : ty => f x)
-- (x : ty) =@ f x ==>> (=@) exp (\x : ty => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindType name lhs)) _ r)
= do desugaredLHS <- desugarB side ps lhs
desugaredRHS <- desugarTree side ps r
pure $ IApp loc (IApp loc (IVar opFC op) desugaredLHS)
(ILam loc top Explicit (Just name.val) desugaredLHS desugaredRHS)
-- (x := exp ** f x) ==>> (**) exp (\x : ? => f x)
-- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindExpr name lhs)) _ r)
= do desugaredLHS <- desugarB side ps lhs
desugaredRHS <- desugarTree side ps r
pure $ IApp loc (IApp loc (IVar opFC op) desugaredLHS)
(ILam loc top Explicit (Just name.val) (Implicit opFC False) desugaredRHS)
-- (x : ty := exp ** f x) ==>> (**) exp (\x : ty => f x)
-- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType name ty expr)) _ r)
= do desugaredLHS <- desugarB side ps expr
desugaredType <- desugarB side ps ty
Expand Down
10 changes: 5 additions & 5 deletions src/Idris/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -1882,16 +1882,16 @@ definition fname indents
= do nd <- bounds (clause 0 Nothing fname indents)
pure (PDef (boundToFC fname nd) [nd.val])

operatorBindingKeyword : EmptyRule BindingModifier
operatorBindingKeyword
= (keyword "autobind" >> pure Autobind)
<|> (keyword "typebind" >> pure Typebind)
operatorBindingKeyword : OriginDesc -> EmptyRule BindingModifier
operatorBindingKeyword fname
= (decoratedKeyword fname "autobind" >> pure Autobind)
<|> (decoratedKeyword fname "typebind" >> pure Typebind)
<|> pure NotBinding

fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
fixDecl fname indents
= do vis <- exportVisibility fname
binding <- operatorBindingKeyword
binding <- operatorBindingKeyword fname
b <- bounds (do fixity <- decorate fname Keyword $ fix
commit
prec <- decorate fname Keyword $ intLit
Expand Down

0 comments on commit 1230a76

Please sign in to comment.