Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: bobatkey/foveran
base: dde425fb30
...
head fork: bobatkey/foveran
compare: 7ef283b839
Checking mergeability… Don't worry, you can still create the pull request.
  • 6 commits
  • 15 files changed
  • 0 commit comments
  • 1 contributor
Commits on Oct 22, 2011
Robert Atkey New syntax for 'elimEmpty'
- Instead of 'elimEmpty A t', use 'elimEmpty t [for A]'
- the 'for A' part is optional, and only needed if the elimination
  is in a type synthesis context
fed1f28
Robert Atkey Fiddling with the syntax
- new keyword 'then' for use with 'rewriteBy'
- change the precedences of elimEmpty and rewriteBy/elimEq
0058503
Robert Atkey 'absurdBy' as alternative (and preferred) syntax for 'elimEmpty' a611e9c
Robert Atkey Vector reverse example, and transivity ce980e9
Commits on Oct 24, 2011
Robert Atkey Re-do the 'data' declaration handling
- Do not generate constructor functions; this will be handled by
  special constructor syntax
- Now works for non-indexed data
df84606
Robert Atkey Use the Forvie layout module to do Haskell-style semicolon-free layout 7ef283b
View
11 src/Language/Foveran/Parsing.hs
@@ -23,6 +23,7 @@ import Control.StreamProcessor.IO
import Text.ParserCombinators
import Language.Forvie.Lexing.Spec
import Language.Forvie.Lexing.Generator
+import Language.Forvie.Layout
import Language.Foveran.Util.PrettyPrinting
@@ -37,6 +38,7 @@ data InputError
= PE_UTF8DecodeError String
| PE_LexingError (Maybe (Char, Position))
| PE_ParsingError (Maybe (Lexeme Token)) [Maybe Token]
+ | PE_LayoutError Span
instance UTF8DecodeError InputError where
utf8DecodeError = PE_UTF8DecodeError
@@ -48,6 +50,9 @@ instance LexingError InputError where
instance ParsingError Token InputError where
parseError = PE_ParsingError
+instance LayoutError InputError where
+ layoutError = PE_LayoutError
+
--------------------------------------------------------------------------------
ppToken Nothing = "End of file"
ppToken (Just t) = text $ show t
@@ -71,10 +76,11 @@ ppInputError (PE_ParsingError Nothing expecting) =
ppInputError (PE_ParsingError (Just (Lexeme _ p s)) expecting) =
"Parse error" <+> ppSpan p <+> "on input" <+> text (T.unpack s)
$$ ppExpecting expecting
+ppInputError (PE_LayoutError p) = "Layout error at" <+> ppSpan p
--------------------------------------------------------------------------------
-lexer :: SP InputError ByteString (Lexeme (Action Token))
+lexer :: SP InputError ByteString (Lexeme (Action (NewlineOr Token)))
lexer =
toWord8 >>>
decodeUTF8 >>>
@@ -83,7 +89,8 @@ lexer =
parser :: SR InputError ByteString [Declaration]
parser =
lexer >>>
- exceptIgnorable >>|
+ exceptIgnorable >>>
+ layout >>|
parse file
readFoveranFile :: FilePath -> IO (Either InputError [Declaration])
View
136 src/Language/Foveran/Parsing/LexicalSpec.hs
@@ -5,77 +5,83 @@ module Language.Foveran.Parsing.LexicalSpec
where
import Language.Forvie.Lexing.Spec
+import Language.Forvie.Layout
import Language.Foveran.Parsing.Token
-lexicalSpec :: LexicalSpecification (Action Token)
-lexicalSpec =
- [ "assume" :==> Emit Assume
- , "normalise" :==> Emit Normalise
- , ":" :==> Emit Colon
- , ":=" :==> Emit ColonEquals
- , ";" :==> Emit Semicolon
- , "=" :==> Emit Equals
- , "\\" .|. "\x03bb" :==> Emit Lambda
- , "->" .|. "" :==> Emit Arrow
- , "(" :==> Emit LParen
- , ")" :==> Emit RParen
- , "“→”" :==> Emit QuoteArrow
- , "×" :==> Emit Times
- , "“×”" :==> Emit QuoteTimes
- , "+" :==> Emit Plus
- , "“+”" :==> Emit QuotePlus
- , "fst" :==> Emit Fst
- , "snd" :==> Emit Snd
- , "inl" :==> Emit Inl
- , "inr" :==> Emit Inr
- , "“K”" :==> Emit QuoteK
- , "µ" :==> Emit Mu
- , "construct" :==> Emit Construct
- , "induction" :==> Emit Induction
- , "elimD" :==> Emit ElimD
- , "sem" :==> Emit Sem
- , "()" .|. "" :==> Emit UnitValue
- , "«" :==> Emit LDoubleAngle
- , "»" :==> Emit RDoubleAngle
- , "," :==> Emit Comma
- , "case" :==> Emit Case
- , "for" :==> Emit For
- , "." :==> Emit FullStop
- , "with" :==> Emit With
- , "{" :==> Emit LBrace
- , "}" :==> Emit RBrace
- , "Set" :==> Emit Set
- , "Empty" .|. "𝟘" :==> Emit EmptyType
- , "Unit" .|. "𝟙" :==> Emit UnitType
- , "elimEmpty" :==> Emit ElimEmpty
- , "“Id”" :==> Emit QuoteId
- , "Desc" :==> Emit Desc
- , "data" :==> Emit Data
- , "|" :==> Emit Pipe
- , "IDesc" :==> Emit IDesc
- , "“IId”" :==> Emit Quote_IId
- , "“Σ”" :==> Emit Quote_Sg
- , "“Π”" :==> Emit Quote_Pi
- , "elimID" :==> Emit IDesc_Elim
- , "µI" :==> Emit MuI
- , "inductionI" :==> Emit InductionI
- , "" :==> Emit Eq
- , "refl" :==> Emit Refl
- , "rewriteBy" :==> Emit RewriteBy
- , "elimEq" :==> Emit ElimEq
- , "where" :==> Emit Where
- , "_" :==> Emit Underscore
+emit = Emit . Token
+
+lexicalSpec :: LexicalSpecification (Action (NewlineOr Token))
+lexicalSpec =
+ [ "assume" :==> emit Assume
+ , "normalise" :==> emit Normalise
+ , ":" :==> emit Colon
+ , ":=" :==> emit ColonEquals
+ , ";" :==> emit Semicolon
+ , "=" :==> emit Equals
+ , "\\" .|. "\x03bb" :==> emit Lambda
+ , "->" .|. "" :==> emit Arrow
+ , "(" :==> emit LParen
+ , ")" :==> emit RParen
+ , "“→”" :==> emit QuoteArrow
+ , "×" :==> emit Times
+ , "“×”" :==> emit QuoteTimes
+ , "+" :==> emit Plus
+ , "“+”" :==> emit QuotePlus
+ , "fst" :==> emit Fst
+ , "snd" :==> emit Snd
+ , "inl" :==> emit Inl
+ , "inr" :==> emit Inr
+ , "“K”" :==> emit QuoteK
+ , "µ" :==> emit Mu
+ , "construct" :==> emit Construct
+ , "induction" :==> emit Induction
+ , "elimD" :==> emit ElimD
+ , "sem" :==> emit Sem
+ , "()" .|. "" :==> emit UnitValue
+ , "«" :==> emit LDoubleAngle
+ , "»" :==> emit RDoubleAngle
+ , "," :==> emit Comma
+ , "case" :==> emit Case
+ , "for" :==> emit For
+ , "." :==> emit FullStop
+ , "with" :==> emit With
+ , "{" :==> emit LBrace
+ , "}" :==> emit RBrace
+ , "Set" :==> emit Set
+ , "Empty" .|. "𝟘" :==> emit EmptyType
+ , "Unit" .|. "𝟙" :==> emit UnitType
+ , "elimEmpty" :==> emit ElimEmpty
+ , "“Id”" :==> emit QuoteId
+ , "Desc" :==> emit Desc
+ , "data" :==> emit Data
+ , "|" :==> emit Pipe
+ , "IDesc" :==> emit IDesc
+ , "“IId”" :==> emit Quote_IId
+ , "“Σ”" :==> emit Quote_Sg
+ , "“Π”" :==> emit Quote_Pi
+ , "elimID" :==> emit IDesc_Elim
+ , "µI" :==> emit MuI
+ , "inductionI" :==> emit InductionI
+ , "" :==> emit Eq
+ , "refl" :==> emit Refl
+ , "rewriteBy" :==> emit RewriteBy
+ , "elimEq" :==> emit ElimEq
+ , "where" :==> emit Where
+ , "_" :==> emit Underscore
+ , "then" :==> emit Then
+ , "absurdBy" :==> emit AbsurdBy
, tok (nameStartChar .&. complement (singleton '\x03bb')) .>>. zeroOrMore (tok nameChar) :==>
- Emit Ident
+ emit Ident
, oneOrMore (tok digit) :==>
- Emit Number
- , oneOrMore (tok space) :==>
- Ignore Whitespace
+ emit Number
+ , "\n" :==> Emit Newline
+ , oneOrMore (tok " \t") :==>
+ Ignore Whitespace
, ("--" .|. "") .>>. star (tok (complement (singleton '\n'))) :==>
- Ignore Comment
+ Ignore Comment
, "{-"
.>>.
(star (tok anyChar) .&. complement (star (tok anyChar) .>>. "-}" .>>. star (tok anyChar)))
.>>.
- "-}" :==> Ignore Comment
- ]
+ "-}" :==> Ignore Comment
+ ]
View
73 src/Language/Foveran/Parsing/Parser.hs
@@ -56,29 +56,32 @@ patternList =
pure []
file :: Parser Tok.Token [Declaration]
-file = declarations <* eos
+file = token Tok.LBrace *> declarations <* token Tok.RBrace <* eos
+
+declarations :: Parser Tok.Token [Declaration]
+declarations = many (token Tok.Semicolon)
+ *> many (declaration <* some (token Tok.Semicolon))
declaration :: Parser Tok.Token Declaration
declaration =
- (\p nm t p' -> AssumptionDecl (Assume (makeSpan p p') nm t))
+ (\p nm t -> AssumptionDecl (Assume (makeSpan p t) nm t))
<$> token Tok.Assume
<* commit
<*> identifier
<* token Tok.Colon
<*> term
- <*> token Tok.Semicolon
<|>
- (\(nm1,p) t1 (nm2,p2) nms t2 p' ->
- DefinitionDecl $ Definition (makeSpan p p') nm1 t1 nm2 (case nms of [] -> t2; nms -> Annot (makeSpan p2 t2) (Lam nms t2)))
- <$> tokenWithText Tok.Ident <* commit <* token Tok.Colon <*> term <* token Tok.Semicolon
+ (\(nm1,p) t1 (nm2,p2) nms t2 ->
+ DefinitionDecl $ Definition (makeSpan p t2) nm1 t1 nm2 (case nms of [] -> t2; nms -> Annot (makeSpan p2 t2) (Lam nms t2)))
+ <$> tokenWithText Tok.Ident <* commit <* token Tok.Colon <*> term <* some (token Tok.Semicolon)
<*> tokenWithText Tok.Ident
<*> patternList
- <* token Tok.Equals <*> term <*> token Tok.Semicolon
+ <* token Tok.Equals <*> term
<|>
IDataDecl <$> idata
<|>
- (\p nm params constructors p' ->
- DatatypeDecl $ Datatype (makeSpan p p') nm params constructors)
+ (\p nm params constructors ->
+ DatatypeDecl $ Datatype (makeSpan p p) nm params constructors)
<$> token Tok.Data
<*> identifier
<*> ((map (\p -> (paramIdent p,paramType p))) <$> dataParamList)
@@ -86,12 +89,10 @@ declaration =
<* token Tok.Set
<* token Tok.ColonEquals
<*> constructorList
- <*> token Tok.Semicolon
<|>
- (\p tm p' -> Normalise tm)
- <$> token Tok.Normalise
- <*> term
- <*> token Tok.Semicolon
+ (\p tm -> Normalise tm)
+ <$> token Tok.Normalise
+ <*> term
dataParamList :: Parser Tok.Token [DataParameter]
dataParamList =
@@ -123,10 +124,9 @@ idata =
(\pl nm params idxType constrs pr -> IData (makeSpan pl pr) nm params idxType constrs) <$>
token Tok.Data <*> identifier
<*> dataParamList
- <* token Tok.Colon <*> term09 <* token Tok.Arrow <* token Tok.Set
+ <* token Tok.Colon <*> optional (term09 <* token Tok.Arrow) <* token Tok.Set
<* token Tok.Where
<* token Tok.LBrace <*> iconstructors <*> token Tok.RBrace
- <* token Tok.Semicolon
iconstructors :: Parser Tok.Token [IConstructor]
iconstructors =
@@ -152,17 +152,10 @@ iconstructor =
<*> constructorbits
<|>
binary ConsArr <$> term09 <* token Tok.Arrow <*> constructorbits
- <|>
- (\(nm,p) ts -> Annot (makeSpan p ts) (ConsEnd nm ts)) <$> tokenWithText Tok.Ident <*> many term00
+ <|> -- FIXME: better source position here
+ (\(nm,p) ts -> Annot (makeSpan p p) (ConsEnd nm ts)) <$> tokenWithText Tok.Ident <*> many term00
--------------------------------------------------------------------------------
-
-declarations :: Parser Tok.Token [Declaration]
-declarations =
- (:) <$> declaration <*> declarations
- <|>
- pure []
-
term :: Parser Tok.Token TermPos
term = term10
@@ -226,10 +219,28 @@ term01 =
<|>
binaryPrefix IDesc_Pi <$> token Tok.Quote_Pi <*> term00 <*> term00
<|>
+ (\p t1 t2 -> Annot (makeSpan p t2) (ElimEmpty t1 (Just t2)))
+ <$> (token Tok.ElimEmpty <|> token Tok.AbsurdBy)
+ <*> term10
+ <* token Tok.For
+ <*> term10
+ <|>
+ (\p t1 -> Annot (makeSpan p t1) (ElimEmpty t1 Nothing))
+ <$> (token Tok.ElimEmpty <|> token Tok.AbsurdBy)
+ <*> term10
+ <|>
+ (\p t t1 t2 -> Annot (makeSpan p t2)
+ (ElimEq t t1 t2)) <$>
+ (token Tok.ElimEq <|> token Tok.RewriteBy)
+ <*> term10
+ <*> optional ((\a x t -> (a,x,t)) <$ token Tok.For <*> identifier <*> identifier <* token Tok.FullStop <*> term10)
+ <* (token Tok.With <|> token Tok.Then)
+ <*> term10
+ <|>
-- function application
-- left associative
(\t ts -> case ts of [] -> t
- ts -> binary App t ts) <$> term00 <*> many term00
+ ts -> Annot (makeSpan t (last ts)) (App t ts)) <$> term00 <*> many term00
term00 :: Parser Tok.Token TermPos
term00 =
@@ -269,21 +280,11 @@ term00 =
<* token Tok.Inr <*> pattern <* token Tok.FullStop <*> term10)
<*> token Tok.RBrace
<|>
- (\p t t1 t2 -> Annot (makeSpan p t2)
- (ElimEq t t1 t2)) <$>
- (token Tok.ElimEq <|> token Tok.RewriteBy)
- <*> term10
- <*> optional ((\a x t -> (a,x,t)) <$ token Tok.For <*> identifier <*> identifier <* token Tok.FullStop <*> term10)
- <* token Tok.With
- <*> term00
- <|>
(\p x -> case x of Nothing -> Annot p (Set 0)
Just (l,p') -> Annot (makeSpan p p') (Set l)) <$> token Tok.Set <*> optional number
<|>
keyword Empty <$> token Tok.EmptyType
<|>
- keyword ElimEmpty <$> token Tok.ElimEmpty
- <|>
keyword Unit <$> token Tok.UnitType
<|>
keyword Desc_Id <$> token Tok.QuoteId
View
17 src/Language/Foveran/Parsing/PrettyPrinter.hs
@@ -10,6 +10,8 @@ module Language.Foveran.Parsing.PrettyPrinter
where
import Data.String
+import Data.Functor ((<$>))
+import Data.Maybe (fromMaybe)
import Data.Rec (foldAnnot, Rec, foldRec, AnnotRec (..))
import Text.PrettyPrintPrec
import qualified Text.PrettyPrint as PP
@@ -41,7 +43,7 @@ pprint (App t ts) = paren 01 (sep (t:map (nest 2 . down) ts))
pprint (Prod t1 t2) = paren 08 (down t1 <+> "×" <+> t2)
pprint (Sigma nms t1 t2) = paren 10 (hang ("(" <> ppIdents nms <+> ":" <+> t1 <> ")" <+> "×") 0 t2)
-pprint (Proj1 t) = paren 01 ("fst" <+> down t)
+pprint (Proj1 t) = paren 01 ("fst" <+> down t) -- These precs are a hack to make the output look less weird
pprint (Proj2 t) = paren 01 ("snd" <+> down t)
pprint (Pair t1 t2) = "«" <> (sep $ punctuate "," [resetPrec t1, resetPrec t2]) <> "»"
@@ -49,7 +51,7 @@ pprint (Sum t1 t2) = paren 09 (down t1 <+> "+" <+> t2)
pprint (Inl t) = paren 01 ("inl" <+> down t)
pprint (Inr t) = paren 01 ("inr" <+> down t)
pprint (Case t x tP y tL z tR) =
- ("case" <+> t <+> "for" <+> ppIdent x <> "." <+> tP <+> "with")
+ ("case" <+> t <+> "for" <+> ppIdent x <> "." <+> resetPrec tP <+> "with")
$$
nest 2 (("{" <+> hang ("inl" <+> ppPattern y <> ".") 3 (resetPrec tL))
$$
@@ -59,14 +61,15 @@ pprint (Case t x tP y tL z tR) =
pprint Unit = "𝟙"
pprint UnitI = "()"
pprint Empty = "𝟘"
-pprint ElimEmpty = "elimEmpty"
+pprint (ElimEmpty t1 Nothing) = paren 01 ("absurdBy" <+> resetPrec t1)
+pprint (ElimEmpty t1 (Just t2)) = paren 01 ("absurdBy" <+> resetPrec t1 $$ nest 6 "for" <+> resetPrec t2)
pprint (Eq t1 t2) = paren 07 (sep [down t1, nest 2 "", t2])
pprint Refl = "refl"
-pprint (ElimEq t Nothing t2) = paren 00 ("rewriteBy" <+> resetPrec t <+> "with" <+> t2)
-pprint (ElimEq t (Just (a, e, t1)) t2) = paren 00 ("rewriteBy" <+> resetPrec t
+pprint (ElimEq t Nothing t2) = paren 01 ("rewriteBy" <+> resetPrec t <+> "then" $$ resetPrec t2)
+pprint (ElimEq t (Just (a, e, t1)) t2) = paren 01 ("rewriteBy" <+> resetPrec t
$$ nest 3 "for" <+> ppIdent a <+> ppIdent e <> "." <+> resetPrec t1
- $$ nest 2 "with" <+> t2)
+ $$ nest 2 "then" <+> resetPrec t2)
pprint Desc = "Desc"
pprint (Desc_K t) = paren 01 ("“K”" <+> down t)
@@ -103,7 +106,7 @@ ppIDataDecl d = doc `atPrecedenceLevel` 10
doc = ("data" <+>
ppIdent (dataName d) <+>
hsep [ "(" <> ppIdent nm <+> ":" <+> fromDoc (ppAnnotTerm t) <> ")" | DataParameter _ nm t <- dataParameters d ] <+>
- ":" <+> fromDoc (ppAnnotTermLev 9 (dataIndexType d)) <+> "" <+> "Set" <+> "where")
+ ":" <+> fromMaybe "" (fromDoc . ppAnnotTermLev 9 <$> dataIndexType d) <+> "" <+> "Set" <+> "where")
$$ nest 2 (doConstructors (dataConstructors d))
doConstructors [] = "{ };"
View
14 src/Language/Foveran/Parsing/Token.hs
@@ -5,6 +5,7 @@ module Language.Foveran.Parsing.Token
)
where
+import Language.Forvie.Layout
import Language.Forvie.Lexing.Spec
import Language.Haskell.TH.Lift
@@ -70,6 +71,8 @@ data Token
| InductionI
| Underscore
+ | Then
+ | AbsurdBy
deriving (Eq,Ord)
deriveLift ''Token
@@ -133,6 +136,15 @@ instance SyntaxHighlight Token where
lexicalClass RewriteBy = Keyword
lexicalClass Where = Keyword
lexicalClass Underscore = Punctuation
+ lexicalClass Then = Keyword
+ lexicalClass AbsurdBy = Keyword
+
+instance Layout Token where
+ lbrace = LBrace
+ rbrace = RBrace
+ semicolon = Semicolon
+ blockOpener Where = True
+ blockOpener _ = False
instance Show Token where
show Assume = "assume"
@@ -193,3 +205,5 @@ instance Show Token where
show Normalise = "normalise"
show Where = "where"
show Underscore = "_"
+ show Then = "then"
+ show AbsurdBy = "absurdBy"
View
8 src/Language/Foveran/Syntax/Checked.hs
@@ -49,7 +49,7 @@ data TermCon tm
| Unit
| UnitI
| Empty
- | ElimEmpty
+ | ElimEmpty tm tm
| Eq tm tm tm tm
| Refl
@@ -108,7 +108,7 @@ traverseSyn (Case t1 tA tB x t2 y t3 z t4)
traverseSyn Unit = pure Unit
traverseSyn UnitI = pure UnitI
traverseSyn Empty = pure Empty
-traverseSyn ElimEmpty = pure ElimEmpty
+traverseSyn (ElimEmpty t1 t2) = ElimEmpty <$> t1 <*> t2
traverseSyn (Eq tA tB t1 t2) = Eq <$> tA <*> tB <*> t1 <*> t2
traverseSyn Refl = pure Refl
@@ -199,7 +199,7 @@ toDisplay (Case t1 _ _ x t2 y t3 z t4)
toDisplay Unit = pure DS.Unit
toDisplay UnitI = pure DS.UnitI
toDisplay Empty = pure DS.Empty
-toDisplay ElimEmpty = pure DS.ElimEmpty
+toDisplay (ElimEmpty t1 t2) = DS.ElimEmpty <$> t1 <*> (Just <$> t2)
toDisplay (Eq _ _ t1 t2) = DS.Eq <$> t1 <*> t2
toDisplay Refl = pure DS.Refl
@@ -280,7 +280,7 @@ instance Eq Term where
In Unit == In Unit = True
In UnitI == In UnitI = True
In Empty == In Empty = True
- In ElimEmpty == In ElimEmpty = True
+ In (ElimEmpty t1 t2) == In (ElimEmpty t1' t2') = t1 == t1'
In (Eq _ _ ta tb) == In (Eq _ _ ta' tb') = ta == ta' && tb == tb'
In Refl == In Refl = True
View
4 src/Language/Foveran/Syntax/Display.hs
@@ -64,7 +64,7 @@ data IDataDecl =
IData { dataPos :: Span
, dataName :: Ident
, dataParameters :: [DataParameter]
- , dataIndexType :: TermPos
+ , dataIndexType :: Maybe TermPos
, dataConstructors :: [IConstructor]
}
@@ -114,7 +114,7 @@ data TermCon tm
| Unit
| UnitI
| Empty
- | ElimEmpty
+ | ElimEmpty tm (Maybe tm)
| Eq tm tm
| Refl
View
8 src/Language/Foveran/Syntax/LocallyNameless.hs
@@ -11,6 +11,7 @@ module Language.Foveran.Syntax.LocallyNameless
where
import Data.List (elemIndex)
+import Data.Traversable (sequenceA)
import Control.Applicative
import Data.Rec
import Text.Position (Span)
@@ -39,7 +40,7 @@ data TermCon tm
| Unit
| UnitI
| Empty
- | ElimEmpty
+ | ElimEmpty tm (Maybe tm)
| Eq tm tm
| Refl
@@ -118,7 +119,8 @@ toLN (DS.Case t1 x t2 y t3 z t4) bv =
toLN DS.Unit bv = Layer $ Unit
toLN DS.UnitI bv = Layer $ UnitI
toLN DS.Empty bv = Layer $ Empty
-toLN DS.ElimEmpty bv = Layer $ ElimEmpty
+toLN (DS.ElimEmpty t1 Nothing) bv = Layer $ ElimEmpty (return $ t1 bv) Nothing
+toLN (DS.ElimEmpty t1 (Just t2)) bv = Layer $ ElimEmpty (return $ t1 bv) (Just (return $ t2 bv))
toLN (DS.Eq t1 t2) bv = Layer $ Eq (return $ t1 bv) (return $ t2 bv)
toLN DS.Refl bv = Layer $ Refl
@@ -177,7 +179,7 @@ close' fnm (Case t1 x t2 y t3 z t4) = Case <$> t1
close' fnm Unit = pure Unit
close' fnm UnitI = pure UnitI
close' fnm Empty = pure Empty
-close' fnm ElimEmpty = pure ElimEmpty
+close' fnm (ElimEmpty t1 t2) = ElimEmpty <$> t1 <*> sequenceA t2
close' fnm (Eq t1 t2) = Eq <$> t1 <*> t2
close' fnm Refl = pure Refl
View
13 src/Language/Foveran/Typing/Checker.hs
@@ -184,6 +184,11 @@ tyCheck (Annot p (ElimEq t Nothing tp)) ctxt tP =
ty ->
Error p (ExpectingEqualityType ctxt ty)
+tyCheck (Annot p (ElimEmpty t1 Nothing)) ctxt v =
+ do tm1 <- tyCheck t1 ctxt VEmpty
+ let tm2 = reifyType0 v
+ return (In $ CS.ElimEmpty tm1 tm2)
+
tyCheck (Annot p t) ctxt v =
do (v',tm) <- tySynth (Annot p t) ctxt
compareTypes p ctxt v v'
@@ -258,10 +263,16 @@ tySynth (Annot p UnitI) ctxt =
tySynth (Annot p Empty) ctxt =
return (VSet 0, In $ CS.Empty)
-tySynth (Annot p ElimEmpty) ctxt =
+tySynth (Annot p (ElimEmpty t1 (Just t2))) ctxt =
+ do tm1 <- tyCheck t1 ctxt VEmpty
+ (_,tm2) <- setCheck t2 ctxt
+ let vtm2 = evaluate tm2 [] (lookupDef ctxt)
+ return (vtm2, In $ CS.ElimEmpty tm1 tm2)
+{-
-- FIXME: make this have a mandatory argument so we can use an arbitrary level
return ( forall "A" (VSet 10) $ \a -> VEmpty .->. a
, In $ CS.ElimEmpty)
+-}
tySynth (Annot p (ElimEq t (Just (a, e, tP)) tp)) ctxt =
do (ty, tm) <- tySynth t ctxt
View
2  src/Language/Foveran/Typing/Conversion/Evaluation.hs
@@ -53,7 +53,7 @@ eval (Case t tA tB x tP y tL z tR) = vcase <$> t
eval Unit = pure VUnit
eval UnitI = pure VUnitI
eval Empty = pure VEmpty
-eval ElimEmpty = pure $ VLam "A" $ \a -> VLam "x" $ \x -> velimEmpty a x
+eval (ElimEmpty x a) = velimEmpty <$> x <*> a
eval (Eq tA tB ta tb) = VEq <$> tA <*> tB <*> ta <*> tb
eval Refl = pure VRefl
View
4 src/Language/Foveran/Typing/Conversion/Value.hs
@@ -140,9 +140,7 @@ vcase _ _ _ _ _ _ _ _ _ = error "internal: type error when elimi
{------------------------------------------------------------------------------}
velimEmpty :: Value -> Value -> Value
-velimEmpty a (VNeutral n) = reflect a (pure (In ElimEmpty)
- `tmApp` reifyType a
- `tmApp` n)
+velimEmpty (VNeutral n) a = reflect a (In <$> (ElimEmpty <$> n <*> reifyType a))
{------------------------------------------------------------------------------}
velimeq tA ta tb VRefl a e tP tp = tp
View
387 src/Language/Foveran/Typing/IDataDecl.hs
@@ -5,18 +5,19 @@ module Language.Foveran.Typing.IDataDecl
where
import qualified Data.Set as S
-import Control.Monad (unless, guard, when, forM_)
+import Control.Monad (unless, guard, when, forM_, forM)
import Control.Monad.State (StateT, evalStateT, get, put, lift)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust)
import Data.Rec (AnnotRec (Annot))
import Language.Foveran.Typing.DeclCheckMonad
import Language.Foveran.Typing.Errors
-import Language.Foveran.Syntax.Display
+import Language.Foveran.Syntax.Display hiding (Constructor, consPos)
import Language.Foveran.Syntax.Identifier ((<+>))
import qualified Language.Foveran.Syntax.LocallyNameless as LN
import Text.Position (Span (..), makeSpan)
--------------------------------------------------------------------------------
+evalStateTWith :: Monad m => s -> StateT s m a -> m a
evalStateTWith = flip evalStateT
(@|) p t = Annot p t
@@ -30,23 +31,20 @@ processIDataDecl d = do
-- Check the constructors for duplicate names, shadowing and
-- correctness of parameter names. Does not check for any type
-- correctness.
- evalStateTWith S.empty $ do
- forM_ (dataConstructors d) (checkConstructor d)
+ constructors <- evalStateTWith S.empty $ do
+ forM (dataConstructors d) (checkConstructor d)
-- Generate the description of this datatype
let codeName = dataName d <+> ":code"
- codeType = paramsType (dataParameters d) (descType d) []
- code = paramsLambda (dataParameters d) (makeCode d) []
- checkInternalDefinition (dataPos d) codeName codeType (Just code)
+ codeTyp = paramsType (dataParameters d) (codeType d) []
+ code = paramsLambda (dataParameters d) (makeCode d constructors) []
+ checkInternalDefinition (dataPos d) codeName codeTyp (Just code)
-- Generate the type itself
let typ = paramsType (dataParameters d) (makeMuTy d) []
- trm = paramsLambda (dataParameters d) (makeMu d) []
+ trm = paramsLambda (dataParameters d) (makeMu d constructors) []
checkInternalDefinition (dataPos d) (dataName d) typ (Just trm)
- -- Generate the functions for each of the constructors
- makeConstructors d id (dataConstructors d)
-
--------------------------------------------------------------------------------
checkParameterName :: DataParameter ->
StateT (S.Set Ident) DeclCheckM ()
@@ -57,247 +55,228 @@ checkParameterName (DataParameter pos paramName _) = do
put (S.insert paramName usedNames)
--------------------------------------------------------------------------------
-checkConstructor :: IDataDecl ->
- IConstructor ->
- StateT (S.Set Ident) DeclCheckM ()
-checkConstructor d (IConstructor p nm components) = do
+-- Intermediate representation of constructors, after the parameter
+-- lists have been checked, and recursive references have been
+-- discovered.
+
+-- These are still in Display syntax, because we will have to
+-- translate them to multiple binding contexts.
+data ConstructorArg
+ = ConsArg Span (Maybe Ident) TermPos
+ | ConsCall Span (Maybe Ident) [(Maybe Ident, TermPos)] TermPos
+
+data Constructor =
+ Constructor { consPos :: Span
+ , consIdent :: Ident
+ , consArgs :: [ConstructorArg]
+ , consResultIdx :: TermPos
+ }
+
+--------------------------------------------------------------------------------
+checkConstructor :: IDataDecl
+ -> IConstructor
+ -> StateT (S.Set Ident) DeclCheckM Constructor
+checkConstructor d (IConstructor pos nm bits) = do
usedNames <- get
when (nm `S.member` usedNames) $ do
- lift $ reportError p (DuplicateConstructorName nm)
- lift $ checkConstructorBits d components
- put (S.insert nm usedNames)
+ lift $ reportError pos (DuplicateConstructorName nm)
+ (args, idxTm) <- lift $ checkConstructorBits d bits
+ return (Constructor pos nm args idxTm)
-checkConstructorBits :: IDataDecl ->
- IConstructorBitsPos ->
- DeclCheckM ()
+checkConstructorBits :: IDataDecl
+ -> IConstructorBitsPos
+ -> DeclCheckM ([ConstructorArg], TermPos)
checkConstructorBits d (Annot p (ConsPi nm t bits)) = do
when (nm == dataName d) $ reportError p ShadowingDatatypeName
when (nm `elem` (map paramIdent $ dataParameters d)) $ reportError p ShadowingParameterName
- checkConstructorBits d bits
+ (args, idxTm) <- checkConstructorBits d bits
+ return (ConsArg p (Just nm) t : args, idxTm)
checkConstructorBits d (Annot p (ConsArr t bits)) = do
- -- FIXME: extract the recursive call if it exists and check to see
- -- whether it properly uses the parameter names
- checkConstructorBits d bits
-checkConstructorBits d (Annot p (ConsEnd nm ts)) = do
- unless (nm == dataName d) $ reportError p (ConstructorTypesMustEndWithNameOfDatatype nm (dataName d))
- checkParameters p ts (map paramIdent $ dataParameters d)
-
-checkParameters :: Span -> [TermPos] -> [Ident] -> DeclCheckM ()
-checkParameters pos [x] [] = return ()
-checkParameters pos [x] _ = reportError pos NotEnoughArgumentsForDatatype
-checkParameters pos (a:args) (p:ps) =
+ (args, idxTm) <- checkConstructorBits d bits
+ case extractRecursiveCall d t of
+ Nothing ->
+ do return (ConsArg p Nothing t : args, idxTm)
+ Just (bindings, callArgs) ->
+ do callIdxTm <- checkParameters p (isJust (dataIndexType d)) callArgs (map paramIdent $ dataParameters d)
+ return (ConsCall p Nothing bindings callIdxTm : args, idxTm)
+checkConstructorBits d (Annot p (ConsEnd nm tms)) = do
+ when (nm /= dataName d) $ reportError p (ConstructorTypesMustEndWithNameOfDatatype nm (dataName d))
+ idxTm <- checkParameters p (isJust (dataIndexType d)) tms (map paramIdent $ dataParameters d)
+ return ([], idxTm)
+
+checkParameters :: Span -> Bool -> [TermPos] -> [Ident] -> DeclCheckM TermPos
+checkParameters pos False [] [] = return (pos @| UnitI)
+checkParameters pos False [] (p:ps) = reportError pos NotEnoughArgumentsForDatatype
+checkParameters pos True [x] [] = return x
+checkParameters pos True [x] (p:ps) = reportError pos NotEnoughArgumentsForDatatype
+checkParameters pos needIdx _ [] = reportError pos TooManyArgumentsForDatatype
+checkParameters pos needIdx [] _ = reportError pos NotEnoughArgumentsForDatatype
+checkParameters pos needIdx (a:args) (p:ps) =
case a of
- Annot pos' (Var arg) -> do
- when (arg /= p) $ reportError pos' (NonMatchingParameterArgument arg p)
- checkParameters pos args ps
- Annot pos' _ -> do
- reportError pos' (IllFormedArgument p)
-checkParameters pos _ [] = reportError pos TooManyArgumentsForDatatype
-checkParameters pos [] _ = reportError pos NotEnoughArgumentsForDatatype
+ Annot pos' (Var arg) -> do when (arg /= p) $ reportError pos' (NonMatchingParameterArgument arg p)
+ checkParameters pos needIdx args ps
+ Annot pos' _ -> do reportError pos' (IllFormedArgument p)
+
+extractRecursiveCall :: IDataDecl
+ -> TermPos
+ -> Maybe ([(Maybe Ident, TermPos)], [TermPos])
+extractRecursiveCall d t = loop t
+ where
+ loop (Annot p (Pi bindings t)) =
+ do let args = [ (nm, t) | (nms, t) <- bindings
+ , nm <- case nms of [] -> [Nothing]; nms -> map Just nms]
+ (args', tms) <- loop t
+ return (args ++ args', tms)
+ loop (Annot p (App (Annot p' (Var nm)) tms)) =
+ do guard (nm == dataName d)
+ return ([], tms)
+ loop (Annot p (Var nm)) =
+ do guard (nm == dataName d)
+ return ([], [])
+ loop _ = Nothing
--------------------------------------------------------------------------------
-makeMuTy :: IDataDecl ->
- [Maybe Ident] ->
- LN.TermPos
-makeMuTy d bv = pos @| LN.Pi Nothing idxType (pos @| LN.Set 0)
+paramsType :: [DataParameter] ->
+ ([Maybe Ident] -> LN.TermPos) ->
+ [Maybe Ident] ->
+ LN.TermPos
+paramsType [] tm bv = tm bv
+paramsType (param:params) tm bv = pos @| LN.Pi (Just nm) tyDom tyCod
+ where DataParameter pos nm ty = param
+ tyDom = LN.toLocallyNameless ty bv
+ tyCod = paramsType params tm (Just nm:bv)
+
+paramsLambda :: [DataParameter] ->
+ ([Maybe Ident] -> LN.TermPos) ->
+ [Maybe Ident] -> LN.TermPos
+paramsLambda [] tm bv = tm bv
+paramsLambda (param:params) tm bv = pos @| LN.Lam nm tmCod
+ where DataParameter pos nm ty = param
+ tmCod = paramsLambda params tm (Just nm:bv)
+
+--------------------------------------------------------------------------------
+makeMuTy :: IDataDecl
+ -> [Maybe Ident]
+ -> LN.TermPos
+makeMuTy d bv =
+ case dataIndexType d of
+ Nothing -> pos @| LN.Set 0
+ Just idxTy -> pos @| LN.Pi Nothing (LN.toLocallyNameless idxTy bv) (pos @| LN.Set 0)
where pos = dataPos d
- idxType = LN.toLocallyNameless (dataIndexType d) bv
-- FIXME: instead of regenerating the code, generate a reference to it
-makeMu :: IDataDecl ->
- [Maybe Ident] ->
- LN.TermPos
-makeMu d bv = pos @| LN.MuI idxType code
+makeMu :: IDataDecl
+ -> [Constructor]
+ -> [Maybe Ident]
+ -> LN.TermPos
+makeMu d constrs bv =
+ case dataIndexType d of
+ Nothing -> pos @| LN.App (pos @| LN.MuI (pos @| LN.Unit) code) (pos @| LN.UnitI)
+ Just idxTy -> pos @| LN.MuI (LN.toLocallyNameless idxTy bv) code
where pos = dataPos d
- idxType = LN.toLocallyNameless (dataIndexType d) bv
- code = makeCode d bv
+ code = makeCode d constrs bv
--------------------------------------------------------------------------------
-- Generates the type of the code for the datatype, given a binding
-- environment for the parameters
-descType :: IDataDecl -> [Maybe Ident] -> LN.TermPos
-descType d bv = pos @| LN.Pi Nothing idxType1 (pos @| LN.App (pos @| LN.IDesc) idxType2)
+codeType :: IDataDecl -> [Maybe Ident] -> LN.TermPos
+codeType d bv = pos @| LN.Pi Nothing idxType1 (pos @| LN.App (pos @| LN.IDesc) idxType2)
where pos = dataPos d
- idxType1 = LN.toLocallyNameless (dataIndexType d) bv
- idxType2 = LN.toLocallyNameless (dataIndexType d) (Nothing:bv)
+ idxType1 = case dataIndexType d of
+ Nothing -> pos @| LN.Unit
+ Just idxTy -> LN.toLocallyNameless idxTy bv
+ idxType2 = case dataIndexType d of
+ Nothing -> pos @| LN.Unit
+ Just idxTy -> LN.toLocallyNameless idxTy (Nothing:bv)
--------------------------------------------------------------------------------
-- generate the big sum type to name the constructors
-namesSumType :: Span -> [IConstructor] -> LN.TermPos
+namesSumType :: Span -> [a] -> LN.TermPos
namesSumType pos [] = pos @| LN.Empty
namesSumType pos [x] = pos @| LN.Unit
namesSumType pos (x:xs) = pos @| LN.Sum (pos @| LN.Unit) (namesSumType pos xs)
--------------------------------------------------------------------------------
-makeCode :: IDataDecl ->
- [Maybe Ident] ->
- LN.TermPos
-makeCode d bv = pos @| LN.Lam "i" (pos @| LN.IDesc_Sg namesTy body)
+makeCode :: IDataDecl
+ -> [Constructor]
+ -> [Maybe Ident]
+ -> LN.TermPos
+makeCode d constrs bv = pos @| LN.Lam "i" (pos @| LN.IDesc_Sg namesTy body)
where
pos = dataPos d
- namesTy = namesSumType pos (dataConstructors d)
- body = pos @| LN.Lam "d" (codeBody d (Nothing:Nothing:bv) 1 (dataConstructors d))
+ namesTy = namesSumType pos constrs
+ body = pos @| LN.Lam "d" (codeBody d (Nothing:Nothing:bv) 1 constrs)
-- expects that the bound variables include the parameters, the index
-- variable and the discriminator at position 0
-codeBody :: IDataDecl ->
- [Maybe Ident] ->
- Int ->
- [IConstructor] ->
- LN.TermPos
+codeBody :: IDataDecl
+ -> [Maybe Ident]
+ -> Int
+ -> [Constructor]
+ -> LN.TermPos
codeBody d bv idxVar [] =
-- Special case when we have no constructors
- pos @| LN.App (pos @| LN.App (pos @| LN.ElimEmpty) descType)
- (pos @| LN.Bound 0)
+ pos @| LN.ElimEmpty (pos @| LN.Bound 0) Nothing
where
pos = dataPos d
- descType = pos @| LN.App (pos @| LN.IDesc) idxType
- idxType = LN.toLocallyNameless (dataIndexType d) bv
codeBody d bv idxVar [constr] =
- consCode d bits bv idxVar
- where
- IConstructor p nm bits = constr
+ consCode d constr bv idxVar
codeBody d bv idxVar (constr:constrs) =
p @| LN.Case discrimVar "x" resultType "a" thisCase "b" otherCases
where
- IConstructor p nm bits = constr
+ p = dataPos d
discrimVar = p @| LN.Bound 0
- idxType = LN.toLocallyNameless (dataIndexType d) (Nothing:bv)
+ idxType = case dataIndexType d of
+ Nothing -> p @| LN.Unit
+ Just idxTy -> LN.toLocallyNameless idxTy (Nothing:bv)
resultType = p @| LN.App (p @| LN.IDesc) idxType
- thisCase = consCode d bits (Nothing:bv) (idxVar+1)
+ thisCase = consCode d constr (Nothing:bv) (idxVar+1)
otherCases = codeBody d (Nothing:bv) (idxVar+1) constrs
--------------------------------------------------------------------------------
-makeConstructors :: IDataDecl ->
- (LN.TermPos -> LN.TermPos) ->
- [IConstructor] ->
- DeclCheckM ()
-makeConstructors d consNameCode [] = do
- return ()
-makeConstructors d consNameCode [constr] = do
- let nameCode = consNameCode (consPos constr @| LN.UnitI)
- makeConstructor d nameCode constr
-makeConstructors d consNameCode (constr:constrs) = do
- let nameCode = consNameCode (consPos constr @| LN.Inl (consPos constr @| LN.UnitI))
- makeConstructor d nameCode constr
- makeConstructors d (consNameCode . (\x -> consPos constr @| LN.Inr x)) constrs
-
---------------------------------------------------------------------------------
-paramsType :: [DataParameter] ->
- ([Maybe Ident] -> LN.TermPos) ->
- [Maybe Ident] ->
- LN.TermPos
-paramsType [] tm bv = tm bv
-paramsType (param:params) tm bv = pos @| LN.Pi (Just nm) tyDom tyCod
- where DataParameter pos nm ty = param
- tyDom = LN.toLocallyNameless ty bv
- tyCod = paramsType params tm (Just nm:bv)
-
-paramsLambda :: [DataParameter] ->
- ([Maybe Ident] -> LN.TermPos) ->
- [Maybe Ident] -> LN.TermPos
-paramsLambda [] tm bv = tm bv
-paramsLambda (param:params) tm bv = pos @| LN.Lam nm tmCod
- where DataParameter pos nm ty = param
- tmCod = paramsLambda params tm (Just nm:bv)
-
---------------------------------------------------------------------------------
-makeConstructor :: IDataDecl ->
- LN.TermPos ->
- IConstructor ->
- DeclCheckM ()
-makeConstructor d nameCode constr = do
- let IConstructor p nm xs = constr
- typ = paramsType (dataParameters d) (consType xs) []
- trm = paramsLambda (dataParameters d) (const $ consTerm nameCode xs) []
- checkInternalDefinition p nm typ (Just trm)
-
---------------------------------------------------------------------------------
-consTerm :: LN.TermPos
- -> IConstructorBitsPos
- -> LN.TermPos
-consTerm consNameCode constr = lambdas constr 0
- where
- lambdas (Annot p (ConsPi nm t bits)) bv = p @| LN.Lam nm (lambdas bits (bv+1))
- lambdas (Annot p (ConsArr t bits)) bv = p @| LN.Lam "x" (lambdas bits (bv+1))
- lambdas (Annot p (ConsEnd _ _)) bv = p @| LN.Construct (tuple p bv)
-
- tuple p bv = p @| LN.Pair consNameCode (term constr bv)
-
- term (Annot p (ConsPi _ _ bits)) bv = p @| LN.Pair (p @| LN.Bound (bv-1)) (term bits (bv-1))
- term (Annot p (ConsArr _ bits)) bv = p @| LN.Pair (p @| LN.Bound (bv-1)) (term bits (bv-1))
- term (Annot p (ConsEnd _ _)) bv = p @| LN.Refl
-
---------------------------------------------------------------------------------
--- Given a display-level constructor description and a list of binding
--- names, generate the locally-nameless type of the constructor.
-consType :: IConstructorBitsPos
- -> [Maybe Ident]
- -> LN.TermPos
-consType (Annot p (ConsPi nm t bits)) bv = p @| LN.Pi (Just nm) tyDom tyBits
- where tyBits = consType bits (Just nm:bv)
- tyDom = LN.toLocallyNameless t bv
-consType (Annot p (ConsArr t bits)) bv = p @| LN.Pi Nothing tyDom tyBits
- where tyBits = consType bits (Nothing:bv)
- tyDom = LN.toLocallyNameless t bv
-consType (Annot p (ConsEnd nm ts)) bv = foldl doArg hd ts
- where hd = p @| LN.Free nm
- doArg t arg = p @| LN.App t (LN.toLocallyNameless arg bv)
-
---------------------------------------------------------------------------------
--- Given the full datatype declaration, the display-level constructor
--- description, a binding environment, and the de Bruijn index of the
--- index variable, generate the locallynameless term for the
--- description of this constructor.
consCode :: IDataDecl
- -> IConstructorBitsPos
+ -> Constructor
-> [Maybe Ident]
-> Int
-> LN.TermPos
-consCode d (Annot p (ConsPi nm t bits)) bv idxVar = p @| LN.IDesc_Sg t' (p @| LN.Lam nm code)
- where t' = LN.toLocallyNameless t bv
- code = consCode d bits (Just nm:bv) (idxVar+1)
-
-consCode d (Annot p (ConsArr t bits)) bv idxVar = p @| LN.Desc_Prod codeDom code
- where t' = LN.toLocallyNameless t bv
- p' = makeSpan t' t'
- codeDom = (p' @| LN.Desc_K t') `fromMaybe` (extractRecursiveCall d t')
- code = consCode d bits bv idxVar
-
-consCode d (Annot p (ConsEnd nm ts)) bv idxVar = p @| LN.Desc_K (p @| LN.Eq idxVal idx)
- where args = reverse ts
- idx = p @| LN.Bound idxVar
- idxVal = LN.toLocallyNameless (head args) bv -- FIXME: handle types with no index
-
---------------------------------------------------------------------------------
--- Extracts a recursive call to the datatype currently being defined
-extractRecursiveCall :: IDataDecl
- -> LN.TermPos
- -> Maybe LN.TermPos
-extractRecursiveCall d t = loop t
+consCode d constr =
+ foldr (consBitCode d) (consEndCode d (consResultIdx constr)) $ consArgs constr
+
+consEndCode :: IDataDecl
+ -> TermPos
+ -> [Maybe Ident] -> Int -> LN.TermPos
+consEndCode d idxTm bv idxVar =
+ p @| LN.Desc_K (p @| LN.Eq idxTm' idx)
where
- loop (Annot p (LN.Pi nm t t')) =
- do code <- loop t'
- return (p @| LN.IDesc_Pi t (p @| LN.Lam (fromMaybe "x" nm) code))
- loop t =
- do (p, nm, args) <- extractApplication t
- -- we only care about applications with the right name
- -- FIXME: handle mutually inductive types
- guard (nm == dataName d)
- -- FIXME: check the parameters against the names
- let idxVal = head args -- FIXME: handle non-indexed data
- return (p @| LN.IDesc_Id idxVal)
-
--- if the given term is of the form
--- nm @ t1 @ ... @ t2
--- then return the position of nm, nm, and the ti in reverse order
--- otherwise return 'Nothing'
-extractApplication :: LN.TermPos
- -> Maybe (Span, Ident, [LN.TermPos])
-extractApplication t = loop t
+ p = dataPos d -- FIXME: this location ought to be the location of the ConsEnd bit
+ idx = p @| LN.Bound idxVar
+ idxTm' = LN.toLocallyNameless idxTm bv
+
+consBitCode :: IDataDecl
+ -> ConstructorArg
+ -> ([Maybe Ident] -> Int -> LN.TermPos)
+ -> [Maybe Ident] -> Int -> LN.TermPos
+consBitCode d (ConsArg pos maybeNm t) rest bv idxVar =
+ pos @| LN.IDesc_Sg t' (pos @| LN.Lam nm code)
+ where
+ nm = fromMaybe "x" maybeNm
+ t' = LN.toLocallyNameless t bv
+ code = rest (maybeNm:bv) (idxVar+1)
+consBitCode d (ConsCall pos maybeNm hyps idxTm) rest bv idxVar =
+ pos @| LN.Desc_Prod codeCall code
where
- loop (Annot p (LN.Free nm)) = return (p, nm, [])
- loop (Annot p (LN.App t t')) = do (p, nm, l) <- loop t
- return (p, nm, t':l)
- loop _ = Nothing
+ code = rest bv idxVar
+ codeCall = foldr makeHyp makeCall hyps bv
+
+ makeCall bv =
+ let idxTm' = LN.toLocallyNameless idxTm bv
+ -- FIXME: get the position from idxTm'
+ in pos @| LN.IDesc_Id idxTm'
+
+ makeHyp (nm, t) rest bv =
+ let t' = LN.toLocallyNameless t bv
+ nm' = fromMaybe "x" nm
+ code = rest (nm:bv)
+ -- FIXME: get the position from t'
+ in pos @| LN.IDesc_Pi t' (pos @| LN.Lam nm' code)
View
271 tests/idata.fv
@@ -1,93 +1,192 @@
-data Nat : Unit → Set where
- { zero : Nat ()
- ; succ : Nat () → Nat ()
- };
-
-data List (A : Set) : Unit → Set where
- { nil : List A ()
- ; cons : A → List A () → List A ()
- };
-
-data Vector (A : Set) : Nat () → Set where
- { vnil : Vector A zero
- ; vcons : (n : Nat ()) → A → Vector A n → Vector A (succ n)
- };
-
-––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
-semI : (I : Set) → IDesc I → (I → Set 2) → Set 2;
+semI : (I : Set) → IDesc I → (I → Set 2) → Set 2
semI I D X = elimID I (λD. Set 2)
(λi. X i)
(λA. A)
(λD₁ D₂ semD₁ semD₂. semD₁ × semD₂)
(λA D semD. (a : A) × semD a)
(λA D semD. (a : A) → semD a)
- D;
-
-Vector:body : Set → Nat () → Unit + Unit → IDesc (Nat ());
-Vector:body α n b =
- case b for b. IDesc (Nat ()) with
- { inl u. “K” (zero ≡ n)
- ; inr u. “Σ” (Nat ()) (λn'. “K”α “×” “IId” n' “×” “K”(succ n' ≡ n))
- };
-
-h :
- (α : Set) →
- (Φ : (n : Nat ()) → Vector α n → Set 2) →
- Φ zero (vnil α) →
- ((n : Nat ()) → (a : α) → (xs : Vector α n) → Φ n xs → Φ (succ n) (vcons α n a xs)) →
-
- (n : Nat ()) →
- (xs : semI (Nat ()) (Vector:code α n) (λn. Vector α n)) →
- (φ : liftI (Nat ()) (Vector:code α n) (λn. Vector α n) Φ xs) →
- Φ n (construct xs);
-h α Φ φnil φcons =
- λn x.
- case fst x for b. (z : semI (Nat ()) (Vector:body α n b) (λn. Vector α n)) →
- liftI (Nat ()) (Vector:body α n b) (λn. Vector α n) Φ z →
- Φ n (construct «b,z») with
- { inl u. λz φ.
- elimEq z
- for n p. Φ n (construct «inl (), p»)
- with φnil
- ; inr u. λz φ.
- elimEq snd (snd (snd z))
- for n p. Φ n (construct «inr (), fst z, fst (snd z), fst (snd (snd z)), p»)
- with (φcons (fst z) (fst (snd z)) (fst (snd (snd z))) (fst (snd φ)))
- } (snd x);
+ D
+
+––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
+data Nat : Set where
+ zero : Nat
+ succ : Nat → Nat
+
+zero : Nat
+zero = construct «inl (), refl» – :zero
+
+succ : Nat → Nat
+succ n = construct «inr (), n, refl» – :succ n
+
+– Somewhere, we store that 'succ' is a constructor, because it was generated by 'data' decl.
+– The conversion to locally nameless then knows that, and converts the application to a constructor application
+
+– The type checker then realises that the type will be pushed in, so
+– we can determine which constructor is meant. In this way, we can
+– overload constructors.
+
+– Need to make sure that constructor names cannot be shadowed
+
+– and we should add a check that we have got the right type. This will
+– be some kind of hint in the LocallyNameless syntax
+
+Nat:body : Unit + Unit -> IDesc Unit
+Nat:body d = case d for x. IDesc 𝟙 with
+ { inl _. “K” (() ≡ ())
+ ; inr _. “IId” () “×” “K” (() ≡ ())
+ }
+
+elimtype :
+ (I : Set) →
+ (C : Set) →
+ (body : I → C → IDesc I) →
+ (P : (i : I) → µI I (λi. “Σ” C (body i)) i → Set 2) →
+ (i : I) →
+ (c : C) →
+ Set 2
+elimtype I C body P =
+ λi c.
+ (z : semI I (body i c) (λi. µI I (λi. “Σ” C (body i)) i)) →
+ liftI I (body i c) (λi. µI I (λi. “Σ” C (body i)) i) P z →
+ P i (construct «c,z»)
+
+Nat:elim :
+ (P : Nat → Set 2) →
+ (P zero) →
+ ((n : Nat) → P n → P (succ n)) →
+ (n : Nat) →
+ P n
+Nat:elim P pzero psucc =
+ inductionI Unit Nat:code (λ_. P)
+ (λ_ x. case fst x for b. elimtype Unit (Unit + Unit) (λ_. Nat:body) (λ_. P) () b with
+ { inl _. λz _. rewriteBy z then pzero
+ ; inr _. λz p. rewriteBy (snd z) then psucc (fst z) (fst p)
+ } (snd x))
+ ()
+
+{-
+introduce P pzero psucc n.
+eliminate n with
+ introduce _ «constructor, arguments».
+ case constructor for c. (z : semI Unit (Nat:body c) (λ_. Nat ())) →
+ liftI Unit (Nat:body c) (λ_. Nat ()) (λ_. P) z →
+ P (construct «c, arguments») with
+ { inl _. introduce eq _.
+ rewriteBy eq then pzero
+ ; inr _. introduce «n, eq» «p, _».
+ rewriteBy eq then psucc n p
+ } arguments
+
+introduce P pzero psucc n.
+eliminate n with
+ zero. pzero
+ succ n. psucc n (recurse n)
+
+introduce n₁ n₂.
+eliminate[plus] n₁ with
+ zero. n₂
+ succ n. succ (plus n)
+
+introduce n₁.
+eliminate[plus] n₁ with
+ zero. introduce n₂. n₂
+ succ n. introduce n₂. succ (plus n n₂)
+
+These last three look at the form of the datatype, and use it to
+generate the code above. The name of the eliminator tells it how to
+translate the recusive calls into references to the proof objects.
+
+To do: deeper recursion, probably with the generic sub-term relation.
+
+To do: elimination-with-a-motive-style enhancing of the inductive
+premise and removal of cases that are impossible. Could implement this
+with a "ElimEq"-style tactic that attempts to get rid of as many
+equalities from the context as possible.
+
+"introduce" should emit a warning if a function type has a name, but
+we use a different name in the code.
+
+How would "with" work? If you do something like
+ with isZero n
+then you either get back a proof that 'n' is zero, or a new number 'm'
+and a proof that n = succ m. The plan then is to rewrite all the
+hypotheses to include this new information. This could be done with a
+new tactic.
+
+-}
+
+data List (A : Set) : Set where
+ nil : List A
+ cons : A → List A → List A
+
+data Vector (A : Set) : Nat → Set where
+ vnil : Vector A zero
+ vcons : (n : Nat) → A → Vector A n → Vector A (succ n)
+
+vnil : (A : Set) → Vector A zero
+vnil A = construct «inl (), refl»
+
+vcons : (A : Set) → (n : Nat) → A → Vector A n → Vector A (succ n)
+vcons A n a xs = construct «inr (), n, a, xs, refl»
+
+{-
+Maybe:
+
+local
+ assume A : Set
+
+ data List : Set where
+ nil : List
+ cons : A → List → List
+-}
+––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
+Vector:body : Set → Nat → Unit + Unit → IDesc Nat;
+Vector:body A n b =
+ case b for b. IDesc Nat with
+ { inl _. “K” (zero ≡ n)
+ ; inr _. “Σ” Nat (λn'. “Σ” A (λa. “IId” n' “×” “K”(succ n' ≡ n)))
+ }
Vector:elim :
- (α : Set) →
- (Φ : (n : Nat ()) → Vector α n → Set 2) →
- Φ zero (vnil α) →
- ((n : Nat ()) → (a : α) → (xs : Vector α n) → Φ n xs → Φ (succ n) (vcons α n a xs)) →
- (n : Nat ()) →
- (xs : Vector α n) →
- Φ n xs;
-Vector:elim α Φ φnil φcons n xs =
- inductionI (Nat ()) (Vector:code α) Φ
- (h α Φ φnil φcons)
- n
- xs;
-
-–normalise Vector:elim;
+ (A : Set) →
+ (Φ : (n : Nat) → Vector A n → Set 2) →
+ Φ zero (vnil A) →
+ ((n : Nat) → (a : A) → (xs : Vector A n) → Φ n xs → Φ (succ n) (vcons A n a xs)) →
+ (n : Nat) →
+ (xs : Vector A n) →
+ Φ n xs
+Vector:elim A Φ φnil φcons =
+ inductionI Nat (Vector:code A) Φ
+ (λn x.
+ case fst x for b. elimtype Nat (Unit + Unit) (Vector:body A) Φ n b with
+ { inl _. λz _. rewriteBy z then φnil
+ ; inr _. λz φ. rewriteBy snd (snd (snd z)) then φcons (fst z) (fst (snd z)) (fst (snd (snd z))) (fst φ)
+ } (snd x))
+
+ –; inr _. λ«n', a, xs, eq» «φ, _». rewriteBy eq then (φcons n' a xs φ)
+ –; inr «n', a, xs, eq». λ«φ, _». rewriteBy eq then (φcons n' a xs φ)
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
-data regexp : Unit -> Set where
- { eps : regexp ()
- ; emp : regexp ()
- ; alt : regexp () → regexp () → regexp ()
- ; seq : regexp () → regexp () → regexp ()
- ; star : regexp () → regexp ()
- ; tok : (Unit + Unit) → regexp ()
- };
+data Emp : Set where
-– normalise regexp:code;
+––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
+data regexp (A : Set) : Set where
+ eps : regexp A
+ emp : regexp A
+ alt : regexp A → regexp A → regexp A
+ seq : regexp A → regexp A → regexp A
+ star : regexp A → regexp A
+ tok : A → regexp A
+;
{-
-data Fin : Nat () → Set where
- { fz : (n : Nat ()) → Fin (succ n)
- ; fs : (n : Nat ()) → Fin n → Fin (succ n)
+data Fin : Nat → Set where
+ { fz : (n : Nat) → Fin (succ n)
+ ; fs : (n : Nat) → Fin n → Fin (succ n)
};
+-}
+{-
+{-
data Foo : Unit → Set where
{ foo1 : Foo ()
@@ -97,17 +196,37 @@ data Foo : Unit → Set where
};
-}
+{-
assume lt : Nat () → Nat () → Set;
data Acc : Nat () → Set where
{ acc : (n : Nat ()) → ((n' : Nat ()) → lt n' n → Acc n') → Acc n
};
+-}
+{-
data Acc2 (A : Set) (lt : A → A → Set) : A → Set where
{ acc2 : (a : A) → ((a' : A) → lt a' a → Acc2 A lt a') → Acc2 A lt a
};
+assume acc2ty :
+ (A : Set) →
+ (lt : A → A → Set) → – parameters
+
+ (Φ : (a : A) → Acc2 A lt a → Set) → – predicate
+
+ (a : A) →
+ (f : (a' : A) → lt a' a → Acc2 A lt a') → – constructor arguments
+
+ ((a' : A) → (x : lt a' a) → Φ a' (f a' x)) → – induction hypotheses
+
+ Φ a (acc2 A lt a f); – result
+-}
+
+{-
normalise acc2;
data Emp : Nat () → Set where
{ };
+-}
+
View
4 tests/inductors-descript.fv
@@ -968,9 +968,9 @@ equal-to-leibniz =
natInduction (λn₁. (n₂ : Nat) → equalNat n₁ n₂ → nat-equal n₁ n₂)
(caseNat (λn₂. equalNat zero n₂ → nat-equal zero n₂)
(λu. nat-refl zero)
- (λn₂ e. elimEmpty (nat-equal zero (succ n₂)) e))
+ (λn₂ e. elimEmpty e))
(λn₁ ih. caseNat (λn₂. equalNat (succ n₁) n₂ → nat-equal (succ n₁) n₂)
- (λe. elimEmpty (nat-equal (succ n₁) zero) e)
+ (λe. elimEmpty e)
(λn₂ eq. λF f₁. ih n₂ eq (λn. F (succ n)) f₁));
compareView : Nat → Nat → Set;
View
72 tests/vectors2.fv
@@ -95,14 +95,9 @@ vecElim α Φ φnil φcons =
case fst x for b. (z : semI Nat (body α n b) (λn. vec α n)) →
liftI Nat (body α n b) (λn. vec α n) Φ z →
Φ n (construct «b,z») with
- { inl u. λz u.
- elimEq z
- for n' p. Φ n' (construct «inl (), p»)
- with φnil
- ; inr u. λz φ.
- elimEq snd (snd (snd z))
- for n p. Φ n (construct «inr (), fst z, fst (snd z), fst (snd (snd z)), p»)
- with (φcons (fst z) (fst (snd z)) (fst (snd (snd z))) (fst φ))
+ { inl _. λz _. rewriteBy z then φnil
+ ; inr _. λz φ. rewriteBy snd (snd (snd z)) then
+ φcons (fst z) (fst (snd z)) (fst (snd (snd z))) (fst φ)
} (snd x));
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
@@ -122,10 +117,27 @@ vecappend α n₁ n₂ xs ys =
n₁
xs;
--- vecreverse :
--- (α : Set) →
--- (n : Nat) →
--- vec α n →
+singleton : (α : Set) → α → vec α (succ zero);
+singleton α a = vcons α zero a (vnil α);
+
+add_succ :
+ (n : Nat) →
+ add n (succ zero) ≡ succ n;
+add_succ = natInduction (λn. add n (succ zero) ≡ succ n)
+ refl
+ (λn p. rewriteBy p then refl);
+
+vecreverse :
+ (α : Set) →
+ (n : Nat) →
+ vec α n →
+ vec α n;
+vecreverse α =
+ vecElim α (λn xs. vec α n)
+ (vnil α)
+ (λn a xs rev_xs.
+ rewriteBy add_succ n then
+ vecappend α n (succ zero) rev_xs (singleton α a));
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
assume A : Set;
@@ -137,16 +149,16 @@ v = vcons A one a (vcons A zero b (vnil A));
normalise vecappend A two two v v;
+normalise vecreverse A two v;
+
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
not : Set → Set;
not A = A → Empty;
-succ≢zero : (n : Nat) → not (succ n ≡ zero);
-succ≢zero n eq =
+succ_ne_zero : (n : Nat) → not (succ n ≡ zero);
+succ_ne_zero n eq =
elimEq eq for n p. natCase (λn. Set) Empty (λu. Unit) n with ();
-normalise succ≢zero;
-
symm :
(α : Set) →
(a₁ a₂ : α) →
@@ -154,6 +166,12 @@ symm :
a₂ ≡ a₁;
symm α a₁ a₂ eq = rewriteBy eq with refl;
+trans :
+ (α : Set) →
+ (a₁ a₂ a₃ : α) →
+ a₁ ≡ a₂ → a₂ ≡ a₃ → a₁ ≡ a₃;
+trans α a₁ a₂ a₃ eq₁ = rewriteBy eq₁ then λeq₂. eq₂;
+
succ-inj : (n₁ n₂ : Nat) → succ n₁ ≡ succ n₂ → n₁ ≡ n₂;
succ-inj n₁ n₂ eq =
elimEq symm Nat (succ n₁) (succ n₂) eq
@@ -164,7 +182,7 @@ is-vnil : (α : Set) → (xs : vec α zero) → xs ≡ vnil α;
is-vnil α xs =
vecElim α (λn xs. n ≡ zero → xs ≡ vnil α)
(λeq. refl)
- (λn a xs φ eq. elimEmpty (vcons α n a xs ≡ vnil α) (succ≢zero n eq))
+ (λn a xs φ eq. absurdBy succ_ne_zero n eq)
zero
xs
refl;
@@ -178,7 +196,7 @@ elim-veczero :
elim-veczero α Φ φnil xs =
vecElim α (λn xs. n ≡ zero → Φ n xs)
(λeq. φnil)
- (λn a xs φ eq. elimEmpty (Φ (succ n) (vcons α n a xs)) (succ≢zero n eq))
+ (λn a xs φ eq. absurdBy succ_ne_zero n eq)
zero
xs
refl;
@@ -191,8 +209,8 @@ elim-veczero2 :
Φ xs;
elim-veczero2 α Φ φnil xs =
vecElim α (λn xs. n ≡ zero → (xs' : vec α zero) → xs ≡ xs' → Φ xs')
- (λeq₁ xs' eq₂. rewriteBy eq₂ with φnil)
- (λn a xs φ eq₁ xs' eq₂. elimEmpty (Φ xs') (succ≢zero n eq₁))
+ (λeq₁ xs' eq₂. rewriteBy eq₂ then φnil)
+ (λn a xs φ eq₁ xs' eq₂. absurdBy succ_ne_zero n eq₁)
zero
xs
refl
@@ -205,8 +223,8 @@ is-vcons : (α : Set) →
(a : α) × (xs' : vec α n) × xs ≡ vcons α n a xs';
is-vcons α n xs =
vecElim α (λn' xs. succ n ≡ n' → (a : α) × (xs' : vec α n) × xs ≡ vcons α n a xs')
- (λeq. elimEmpty ((a : α) × (xs' : vec α n) × vnil α ≡ vcons α n a xs') (succ≢zero n eq))
- (λn' a xs' φ eq. rewriteBy symm Nat n n' (succ-inj n n' eq) with «a, xs', refl»)
+ (λeq. absurdBy succ_ne_zero n eq)
+ (λn' a xs' φ eq. rewriteBy symm Nat n n' (succ-inj n n' eq) then «a, xs', refl»)
(succ n)
xs
refl;
@@ -219,12 +237,12 @@ elim-vecsucc :
elim-vecsucc α Φ φcons n xs =
vecElim α (λn xs. (n' : Nat) → n ≡ succ n' → (xs' : vec α (succ n')) → xs ≡ xs' → Φ n' xs')
(λn' eq₁ xs' eq₂.
- elimEmpty (Φ n' xs') (succ≢zero n' (rewriteBy eq₁ with refl)))
+ absurdBy succ_ne_zero n' (rewriteBy eq₁ then refl))
(λn a xs φ n' eq₁.
- rewriteBy succ-inj n n' eq₁ with
- (λxs' eq₂.
- rewriteBy eq₂ with
- (φcons n a xs)))
+ rewriteBy succ-inj n n' eq₁ then
+ λxs' eq₂.
+ rewriteBy eq₂ then
+ φcons n a xs)
(succ n)
xs
n

No commit comments for this range

Something went wrong with that request. Please try again.