isa-parser: add parsing for case of; add parsing for ConstTerm IntLit…

…eral (only supports nat for now
au-ts · Jan 17, 2020 · 29d2fdb · 29d2fdb
1 parent 6d8f1b8
commit 29d2fdb
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 4 deletions.
diff --git a/isa-parser/Isabelle/InnerAST.hs b/isa-parser/Isabelle/InnerAST.hs
@@ -43,6 +43,7 @@ data Term = TermIdent      Ident
           | CaseOf         Term       [(Term, Term)]
           | RecordUpd                 [(Term, Term)]
           | RecordDcl                 [(Term, Term)]
+          | IfThenElse     Term       Term    Term
   deriving (Data, Typeable, Eq, Ord, Show)
 
 data Const = TrueC | FalseC
@@ -259,6 +260,7 @@ prettyTerm p t = case t of
   CaseOf e alts         -> parens (string "case" <+> pretty e <+> string "of" <+> sep (punctuate (text "|") (map prettyAlt alts)))
   RecordUpd upds        -> string "\\<lparr>" <+> sep (punctuate (text ",") (map (prettyAssis ":=") upds)) <+> string "\\<rparr>"
   RecordDcl dcls        -> string "\\<lparr>" <+> sep (punctuate (text ",") (map (prettyAssis "=") dcls)) <+> string "\\<rparr>"
+  IfThenElse cond c1 c2 -> string "if" <+> prettyTerm p cond <+> string "then" <+> prettyTerm p c1 <+> string "else" <+> prettyTerm p c2 
 
 prettyAssis :: String -> (Term, Term) -> Doc 
 prettyAssis s (p, e) = pretty p <+> pretty s <+> pretty e

diff --git a/isa-parser/Isabelle/Parser.hs b/isa-parser/Isabelle/Parser.hs
@@ -626,8 +626,18 @@ termL = buildExpressionParser table restL
 
 
     restL =  antiquoteTermL <||> parensTermL <||> constTermL <||> (TermIdent <$> innerIdentL) <||> 
-             caseOfTermL <||> recordUpdTermL <||> recordDclTermL
+             caseOfTermL <||> recordUpdTermL <||> recordDclTermL <||> ifThenElseTermL 
     parensTermL = parensL termL
+
+ifThenElseTermL :: ParserM Term
+ifThenElseTermL = do
+  reserved "if"
+  cond <- termL 
+  reserved "then"
+  case1 <- termL
+  reserved "else"
+  case2 <- termL
+  return $ IfThenElse cond case1 case2
 
 recordDclTermL :: ParserM Term 
 recordDclTermL = do { stringL "\\<lparr>"
@@ -662,9 +672,9 @@ fieldS = letterS <++> manyP fieldLetters
       fieldLetters = ((letterS <||> digitS <||> charString '_') <||> charString '\'' <||> charString '.') <?> "quasi-letter"
 
 caseOfTermL :: ParserM Term
-caseOfTermL = do { stringL "case"
+caseOfTermL = do { reserved "case"
                  ; term <- termL
-                 ; stringL "of"
+                 ; reserved "of"
                  ; alts <- sepBy1 (try altTermL) (stringL "|") 
                  ; return $ CaseOf term alts }
 
@@ -695,10 +705,12 @@ typedTermL = do
   return (TermWithType t ty)
 
 constTermL :: ParserM Term
-constTermL = ConstTerm <$> (trueL <||> falseL)  -- TODO: only support very limited forms of constants / zilinc
+constTermL = ConstTerm <$> (trueL <||> falseL <||> (IntLiteral <$> intL))  -- TODO: only support very limited forms of constants / zilinc
   where
     trueL  = stringL "True" >> return TrueC
     falseL = stringL "False" >> return FalseC
+    intL = read <$> natL
+
 
 antiquoteTypeL :: ParserM Type 
 antiquoteTypeL = AntiType <$> antiquoteL