Fix parsing of true/false in Pancake

These aren't in the concrete syntax, so map them to 1 and 0 C-style Addresses (the easy part of) issue #939
CakeML · May 25, 2023 · 6291302 · 6291302
1 parent 5e0612a
commit 6291302
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 7 deletions.
diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml
@@ -64,14 +64,14 @@ val ex2 = ‘if b & (a ^ c) & d {
              goo(4, 5, 6);
            }’;
 
-val treeEx2 = parse_pancake ex2;
+val treeEx2 = check_success $ parse_pancake ex2;
 
 (** We also have a selection of boolean operators and
     a ‘return’ statement. *)
 (** FIXME: Add ‘true’ and ‘false’ to EBaseNT *)
 val ex3 = ‘if b & (a ^ c) & d { return true; } else { return false; }’;
 
-val treeEx3 = (* check_success $ *) parse_pancake ex3;
+val treeEx3 = check_success $ parse_pancake ex3;
 
 (** Loops: standard looping construct. *)
 

diff --git a/pancake/parser/panLexerScript.sml b/pancake/parser/panLexerScript.sml
@@ -19,15 +19,15 @@ val _ = new_theory "panLexer";
 Datatype:
   keyword = SkipK | StoreK | StoreBK | IfK | ElseK | WhileK
   | BrK | ContK | RaiseK | RetK | TicK | VarK | WithK | HandleK
-  | LdsK | LdbK | BaseK | InK
+  | LdsK | LdbK | BaseK | InK | TrueK | FalseK
 End
 
 Datatype:
   token = AndT | OrT | XorT | NotT
   | EqT | NeqT | LessT | GreaterT | GeqT | LeqT
   | PlusT | MinusT | HashT | DotT | StarT
   | LslT | LsrT | AsrT | RorT
-  | TrueT | FalseT | IntT int | IdentT string
+  | IntT int | IdentT string
   | LParT | RParT | CommaT | SemiT | ColonT | DArrowT | AddrT
   | LBrakT | RBrakT | LCurT | RCurT
   | AssignT
@@ -110,8 +110,8 @@ Definition get_keyword_def:
   if s = "lds" then (KeywordT LdsK) else
   if s = "ldb" then (KeywordT LdbK) else
   if s = "@base" then (KeywordT BaseK) else
-  if s = "true" then TrueT else
-  if s = "false" then FalseT else
+  if s = "true" then (KeywordT TrueK) else
+  if s = "false" then (KeywordT FalseK) else
   if isPREFIX "@" s ∨ s = "" then LexErrorT else
   IdentT s
 End

diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml
@@ -202,9 +202,11 @@ Definition pancake_peg_def[nocompute]:
         (INL EBaseNT, seql [choicel [seql [consume_tok LParT;
                                            mknt ExpNT;
                                            consume_tok RParT] I;
+                                     keep_kw TrueK; keep_kw FalseK;
                                      keep_int; keep_ident; mknt LabelNT;
                                      mknt StructNT; mknt LoadNT;
-                                     mknt LoadByteNT; keep_kw BaseK];
+                                     mknt LoadByteNT; keep_kw BaseK;
+                                     ];
                             rpt (seql [consume_tok DotT; keep_nat] I)
                                 FLAT]
                            (mksubtree EBaseNT));

diff --git a/pancake/parser/panPtreeConversionScript.sml b/pancake/parser/panPtreeConversionScript.sml
@@ -250,6 +250,8 @@ Definition conv_Exp_def:
       | (e::es) => conv_binaryExps es ' (conv_Exp e)
     else NONE) ∧
   (conv_Exp leaf = if tokcheck leaf (kw BaseK) then SOME BaseAddr
+                   else if tokcheck leaf (kw TrueK) then SOME $ Const 1w
+                   else if tokcheck leaf (kw FalseK) then SOME $ Const 0w
                   else NONE) ∧
   conv_binaryExps [] e = SOME e ∧
   (conv_binaryExps (t1::t2::ts) res =