Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Add new right-associative infix "a * b" syntax for saw-core pair types.
Browse files Browse the repository at this point in the history
The old syntax "#(a | b)" is still supported, for now.
  • Loading branch information
Brian Huffman committed Dec 5, 2018
1 parent 3ecc615 commit 4f76c53
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 10 deletions.
4 changes: 2 additions & 2 deletions prelude/Prelude.sawcore
Original file line number Diff line number Diff line change
Expand Up @@ -63,10 +63,10 @@ Pair_snd : (a b : sort 0) -> PairType a b -> b;
Pair_snd a b = Pair__rec a b (\ (p:PairType a b) -> b)
(\ (x:a) -> \ (y:b) -> y);

fst : (a b : sort 0) -> #(a | b) -> a;
fst : (a b : sort 0) -> a * b -> a;
fst a b tup = tup.(1);

snd : (a b : sort 0) -> #(a | b) -> b;
snd : (a b : sort 0) -> a * b -> b;
snd a b tup = tup.(2);

uncurry (a b c : sort 0) (f : a -> b -> c) : (#(a, b) -> c)
Expand Down
11 changes: 9 additions & 2 deletions src/Verifier/SAW/Grammar.y
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ import Verifier.SAW.Lexer
'{' { PosPair _ (TKey "{") }
'}' { PosPair _ (TKey "}") }
'|' { PosPair _ (TKey "|") }
'*' { PosPair _ (TKey "*") }
'data' { PosPair _ (TKey "data") }
'hiding' { PosPair _ (TKey "hiding") }
'import' { PosPair _ (TKey "import") }
Expand Down Expand Up @@ -146,12 +147,18 @@ Term : LTerm { $1 }

-- Term with uses of pi and lambda, but no type ascriptions
LTerm :: { Term }
LTerm : AppTerm { $1 }
LTerm : ProdTerm { $1 }
| PiArg '->' LTerm { Pi (pos $2) $1 $3 }
| '\\' VarCtx '->' LTerm { Lambda (pos $1) $2 $4 }

PiArg :: { [(TermVar, Term)] }
PiArg : AppTerm { mkPiArg $1 }
PiArg : ProdTerm { mkPiArg $1 }

-- Term formed from infix product type operator (right-associative)
ProdTerm :: { Term }
ProdTerm
: AppTerm { $1 }
| AppTerm '*' ProdTerm { PairType (pos $1) $1 $3 }

-- Term formed from applications of atomic expressions
AppTerm :: { Term }
Expand Down
2 changes: 1 addition & 1 deletion src/Verifier/SAW/Lexer.x
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ $cntrl = [$large \@\[\\\]\^\_]
$idchar = [a-z A-Z 0-9 \' \_]
@ident = [a-z A-Z \_] $idchar*

@punct = "#" | "," | "->" | "." | ";" | ":" | "="
@punct = "#" | "," | "->" | "." | ";" | ":" | "=" | "*"
| "\" | "(" | ")" | "[" | "]" | "{" | "}" | "|"
@keywords = "data" | "hiding" | "import" | "module"
| "sort" | "Prop" | "where" | "primitive" | "axiom"
Expand Down
12 changes: 7 additions & 5 deletions src/Verifier/SAW/Term/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ depthAllowed _ _ = True
data Prec
= PrecNone -- ^ Nonterminal 'Term'
| PrecLambda -- ^ Nonterminal 'LTerm'
| PrecProd -- ^ Nonterminal 'ProductTerm'
| PrecApp -- ^ Nonterminal 'AppTerm'
| PrecArg -- ^ Nonterminal 'AtomTerm'

Expand All @@ -88,6 +89,8 @@ precContains _ PrecArg = True
precContains PrecArg _ = False
precContains _ PrecApp = True
precContains PrecApp _ = False
precContains _ PrecProd = True
precContains PrecProd _ = False
precContains _ PrecLambda = True
precContains PrecLambda _ = False
precContains PrecNone PrecNone = True
Expand Down Expand Up @@ -308,10 +311,9 @@ ppLetBlock defs body =
ppPair :: Doc -> Doc -> Doc
ppPair x y = parens (x <+> char '|' <+> y)

-- | Pretty-print pair types as "#(x | y)"
ppPairType :: Doc -> Doc -> Doc
ppPairType x y =
char '#' <> parens (x <+> char '|' <+> y)
-- | Pretty-print pair types as "x * y"
ppPairType :: Prec -> Doc -> Doc -> Doc
ppPairType prec x y = ppParensPrec prec PrecProd (x <+> char '*' <+> y)

-- | Pretty-print records (if the flag is 'False') or record types (if the flag
-- is 'True'), where the latter are preceded by the string @#@, either as:
Expand Down Expand Up @@ -387,7 +389,7 @@ ppFlatTermF prec tf =
UnitValue -> return $ text "(-empty-)"
UnitType -> return $ text "#(-empty-)"
PairValue x y -> ppPair <$> ppTerm' PrecNone x <*> ppTerm' PrecNone y
PairType x y -> ppPairType <$> ppTerm' PrecNone x <*> ppTerm' PrecNone y
PairType x y -> ppPairType prec <$> ppTerm' PrecApp x <*> ppTerm' PrecProd y
PairLeft t -> ppProj "1" <$> ppTerm' PrecArg t
PairRight t -> ppProj "2" <$> ppTerm' PrecArg t

Expand Down

0 comments on commit 4f76c53

Please sign in to comment.