@@ -869,49 +869,67 @@ bindsymbol opts st syn
869869 = do symbol "->"
870870 return (Exp opts st False)
871871
872+explicitPi opts st syn
873+ = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
874+ binder <- bindsymbol opts st syn
875+ sc <- expr syn
876+ return (bindList (PPi binder) xt sc)
877+
878+autoImplicit opts st syn
879+ = do reserved "auto"
880+ when (st == Static) $ fail "auto type constraints can not be static"
881+ xt <- typeDeclList syn
882+ lchar '}'
883+ symbol "->"
884+ sc <- expr syn
885+ return (bindList (PPi
886+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)
887+
888+defaultImplicit opts st syn = do
889+ reserved "default"
890+ when (st == Static) $ fail "default tactic constraints can not be static"
891+ ist <- get
892+ script' <- simpleExpr syn
893+ let script = debindApp syn . desugar syn ist $ script'
894+ xt <- typeDeclList syn
895+ lchar '}'
896+ symbol "->"
897+ sc <- expr syn
898+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc)
899+
900+normalImplicit opts st syn = do
901+ xt <- typeDeclList syn <* lchar '}'
902+ symbol "->"
903+ cs <- constraintList syn
904+ sc <- expr syn
905+ let (im,cl)
906+ = if implicitAllowed syn
907+ then (Imp opts st False Nothing,
908+ constraint)
909+ else (Imp opts st False (Just (Impl False)),
910+ Imp opts st False (Just (Impl True)))
911+ return (bindList (PPi im) xt
912+ (bindList (PPi cl) cs sc))
913+
914+implicitPi opts st syn =
915+ autoImplicit opts st syn
916+ <|> defaultImplicit opts st syn
917+ <|> normalImplicit opts st syn
918+
919+unboundPi opts st syn = do
920+ x <- opExpr syn
921+ (do binder <- bindsymbol opts st syn
922+ sc <- expr syn
923+ return (PPi binder (sUN "__pi_arg") x sc))
924+ <|> return x
925+
872926pi :: SyntaxInfo -> IdrisParser PTerm
873927pi syn =
874928 do opts <- piOpts syn
875929 st <- static
876− (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
877− binder <- bindsymbol opts st syn
878− sc <- expr syn
879− return (bindList (PPi binder) xt sc)) <|> (do
880− (do try (lchar '{' *> reserved "auto")
881− when (st == Static) $ fail "auto type constraints can not be static"
882− xt <- typeDeclList syn
883− lchar '}'
884− symbol "->"
885− sc <- expr syn
886− return (bindList (PPi
887− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
888− try (lchar '{' *> reserved "default")
889− when (st == Static) $ fail "default tactic constraints can not be static"
890− ist <- get
891− script' <- simpleExpr syn
892− let script = debindApp syn . desugar syn ist $ script'
893− xt <- typeDeclList syn
894− lchar '}'
895− symbol "->"
896− sc <- expr syn
897− return (bindList (PPi (TacImp [] Dynamic script)) xt sc))
898− <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')
899− symbol "->"
900− cs <- constraintList syn
901− sc <- expr syn
902− let (im,cl)
903− = if implicitAllowed syn
904− then (Imp opts st False Nothing,
905− constraint)
906− else (Imp opts st False (Just (Impl False)),
907− Imp opts st False (Just (Impl True)))
908− return (bindList (PPi im) xt
909− (bindList (PPi cl) cs sc))))
910− <|> (do x <- opExpr syn
911− (do binder <- bindsymbol opts st syn
912− sc <- expr syn
913− return (PPi binder (sUN "__pi_arg") x sc))
914− <|> return x)
930+ explicitPi opts st syn
931+ <|> try (do lchar '{'; implicitPi opts st syn)
932+ <|> unboundPi opts st syn
915933 <?> "dependent type signature"
916934
917935{- | Parses Possible Options for Pi Expressions
@@ -944,7 +962,7 @@ constraintList1 syn = try (do lchar '('
944962 lchar ')'
945963 reservedOp "=>"
946964 return tys)
947− <|> try (do t <- expr (disallowImp syn)
965+ <|> try (do t <- opExpr (disallowImp syn)
948966 reservedOp "=>"
949967 return [(defname, t)])
950968 <?> "type constraint list"