From 4f76c5309bff32fcdec552c33045db571117033e Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 5 Dec 2018 09:51:44 -0800
Subject: [PATCH] Add new right-associative infix "a * b" syntax for saw-core
 pair types.

The old syntax "#(a | b)" is still supported, for now.
---
 prelude/Prelude.sawcore         |  4 ++--
 src/Verifier/SAW/Grammar.y      | 11 +++++++++--
 src/Verifier/SAW/Lexer.x        |  2 +-
 src/Verifier/SAW/Term/Pretty.hs | 12 +++++++-----
 4 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
index 6f0231ff..1d9088a0 100644
--- a/prelude/Prelude.sawcore
+++ b/prelude/Prelude.sawcore
@@ -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)
diff --git a/src/Verifier/SAW/Grammar.y b/src/Verifier/SAW/Grammar.y
index 394a8ee7..2ca0e517 100644
--- a/src/Verifier/SAW/Grammar.y
+++ b/src/Verifier/SAW/Grammar.y
@@ -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") }
@@ -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 }
diff --git a/src/Verifier/SAW/Lexer.x b/src/Verifier/SAW/Lexer.x
index a267e8ad..914c0762 100644
--- a/src/Verifier/SAW/Lexer.x
+++ b/src/Verifier/SAW/Lexer.x
@@ -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"
diff --git a/src/Verifier/SAW/Term/Pretty.hs b/src/Verifier/SAW/Term/Pretty.hs
index e1bbd0f3..f3ee228c 100644
--- a/src/Verifier/SAW/Term/Pretty.hs
+++ b/src/Verifier/SAW/Term/Pretty.hs
@@ -74,6 +74,7 @@ depthAllowed _ _ = True
 data Prec
   = PrecNone   -- ^ Nonterminal 'Term'
   | PrecLambda -- ^ Nonterminal 'LTerm'
+  | PrecProd   -- ^ Nonterminal 'ProductTerm'
   | PrecApp    -- ^ Nonterminal 'AppTerm'
   | PrecArg    -- ^ Nonterminal 'AtomTerm'
 
@@ -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
@@ -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:
@@ -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