From 6291302640b2b6026f216317ab97062da58efa7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20=C3=85man=20Pohjola?= Date: Fri, 17 Mar 2023 11:01:37 +1100 Subject: [PATCH] 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 --- pancake/parser/panConcreteExamplesScript.sml | 4 ++-- pancake/parser/panLexerScript.sml | 8 ++++---- pancake/parser/panPEGScript.sml | 4 +++- pancake/parser/panPtreeConversionScript.sml | 2 ++ 4 files changed, 11 insertions(+), 7 deletions(-) diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml index fb68dbe34a..bbeb55395d 100644 --- 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 index 6bbf229093..745f7fd769 100644 --- a/pancake/parser/panLexerScript.sml +++ b/pancake/parser/panLexerScript.sml @@ -19,7 +19,7 @@ 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: @@ -27,7 +27,7 @@ Datatype: | 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 index e532279547..e5ca34e629 100644 --- 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 index 098986b9c7..0d7aebe29f 100644 --- 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 =