Merge pull request #988 from CakeML/pancake_shmem_syntax

Pancake: concrete syntax for shared memory

compiler/bootstrap/translation/from_pancake32ProgScript.sml

@@ -306,6 +306,8 @@ val res = translate destTOK_def;
 
 val res = translate $ PURE_REWRITE_RULE [GSYM mlstringTheory.implode_def] conv_ident_def;
 
+val res = translate $ PURE_REWRITE_RULE [GSYM mlstringTheory.implode_def] conv_ffi_ident_def;
+
 val res = translate isNT_def;
 
 val res = translate conv_int_def;

compiler/bootstrap/translation/from_pancake64ProgScript.sml

@@ -309,6 +309,8 @@ val res = translate destTOK_def;
 
 val res = translate $ PURE_REWRITE_RULE [GSYM mlstringTheory.implode_def] conv_ident_def;
 
+val res = translate $ PURE_REWRITE_RULE [GSYM mlstringTheory.implode_def] conv_ffi_ident_def;
+
 val res = translate isNT_def;
 
 val res = translate conv_int_def;

compiler/bootstrap/translation/pancake_lexProgScript.sml

@@ -103,10 +103,27 @@ QED
 
 val _ = update_precondition next_atom_side;
 
+Theorem get_keyword_side[local]:
+  ∀x. get_keyword_side x
+Proof
+  simp[fetch "-" "get_keyword_side_def"]
+QED
+
+val _ = update_precondition get_keyword_side;
+
+Theorem token_of_atom_side[local]:
+  ∀x. token_of_atom_side x
+Proof
+  simp[fetch "-" "token_of_atom_side_def",get_keyword_side]
+QED
+
+val _ = update_precondition token_of_atom_side;
+
 Theorem next_token_2_side[local]:
   ∀x y. next_token_2_side x y
 Proof
-  simp [Once (fetch "-" "next_token_2_side_def"), next_atom_side]
+  simp [Once (fetch "-" "next_token_2_side_def"),
+    next_atom_side, token_of_atom_side]
 QED
 
 val _ = update_precondition next_token_2_side;

pancake/parser/README.md

@@ -2,6 +2,8 @@ The Pancake parser.
 
 [panConcreteExamplesScript.sml](panConcreteExamplesScript.sml):
 * Pancake concrete syntax examples
+* 9th May 2023: Updated with function declarations
+* March 2024: Updated with shared memory instructions
 
 [panLexerScript.sml](panLexerScript.sml):
 * The beginnings of a lexer for the Pancake language.

pancake/parser/panConcreteExamplesScript.sml

@@ -1,6 +1,7 @@
 (**
  * Pancake concrete syntax examples
  * 9th May 2023: Updated with function declarations
+ * March 2024: Updated with shared memory instructions
  *)
 open HolKernel Parse boolLib bossLib stringLib numLib intLib;
 open preamble panPtreeConversionTheory;
@@ -97,8 +98,8 @@ val ex4 = ‘
       if x >= 5 {
         break;
       } else {
-        strb y, 8; // store byte
-        #foo(x,y,k,z); // ffi function call with pointer args
+        st8 y, 8; // store byte
+        @foo(x,y,k,z); // ffi function call with pointer args
         x = x + 1;
         y = x + 1;
       }
@@ -198,8 +199,8 @@ val ex9 = ‘
    var b = 8;
    var c = @base + 16;
    var d = 1;
-   #out_morefun(a,b,c,d);
-   str @base, ic;
+   @out_morefun(a,b,c,d);
+   stw @base, ic;
    return 0;
  }’;
 
@@ -223,7 +224,7 @@ val argument_call = ‘
 
 val arg_call_tree = check_success $ parse_tree_pancake argument_call;
 
-val arg_call_parse =  parse_pancake $ argument_call;
+val arg_call_parse = check_success $ parse_pancake argument_call;
 
 (** Return call example. It is not currently possible to initialise a variable
     to a value returned from a function as a variable is declared. Instead, the
@@ -241,7 +242,7 @@ val ret_call = ‘
 
 val ret_call_parse_tree = check_success $ parse_tree_pancake ret_call;
 
-val ret_call_parse =  parse_pancake $ ret_call;
+val ret_call_parse = check_success $ parse_pancake ret_call;
 
 (** Shapes and Structs. *)
 val struct_access = ‘
@@ -254,7 +255,7 @@ val struct_access = ‘
 
 val struct_access_parse_tree = check_success $ parse_tree_pancake struct_access;
 
-val struct_access_parse =  parse_pancake $ struct_access;
+val struct_access_parse = check_success $ parse_pancake struct_access;
 
 
 (* Writing ‘n’ for a shape is convenient syntax which is equivalent to ‘{1,1,...,1}’
@@ -299,4 +300,15 @@ val struct_argument_parse_tree =  parse_tree_pancake $ struct_arguments;
 
 val struct_argument_parse =  parse_pancake $ struct_arguments;
 
+val shmem_ex = ‘
+  fun test_shmem() {
+    var v = 12;
+    !st8 v, 1000; // store byte stored in v (12) to shared memory address 1000
+    !stw v, 1004; // store word stored in v (12) to shared memory address 1004
+    !ld8 v, 1000 + 12; // load byte stored in shared memory address 1012 to v
+    !ldw v, 1000 + 12 * 2; // load word stored in shared memory address 1024 to v
+  }’;
+
+val shmem_ex_parse =  check_success $ parse_pancake shmem_ex;
+
 val _ = export_theory();

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 | FunK | TrueK | FalseK
+  | LdsK | LdbK | LdwK | BaseK | InK | FunK | TrueK | FalseK
 End
 
 Datatype:
   token = AndT | OrT | XorT | NotT
   | EqT | NeqT | LessT | GreaterT | GeqT | LeqT
-  | PlusT | MinusT | HashT | DotT | StarT
+  | PlusT | MinusT | DotT | StarT
   | LslT | LsrT | AsrT | RorT
-  | IntT int | IdentT string
+  | IntT int | IdentT string | ForeignIdent string (* @ffi_str except @base *)
   | LParT | RParT | CommaT | SemiT | ColonT | DArrowT | AddrT
   | LBrakT | RBrakT | LCurT | RCurT
   | AssignT
@@ -44,6 +44,9 @@ Definition isAtom_singleton_def:
 End
 
 Definition isAtom_begin_group_def:
+  (* # is for only for RorT,
+  * and should remove it to avoid collision with
+  * C-preprocessor later *)
   isAtom_begin_group c = MEM c "#=><!"
 End
 
@@ -71,7 +74,6 @@ Definition get_token_def:
   if s = "+" then PlusT else
   if s = "-" then MinusT else
   if s = "*" then StarT else
-  if s = "#" then HashT else
   if s = "." then DotT else
   if s = "<<" then LslT else
   if s = ">>>" then LsrT else
@@ -93,8 +95,8 @@ End
 Definition get_keyword_def:
   get_keyword s =
   if s = "skip" then (KeywordT SkipK) else
-  if s = "str" then (KeywordT StoreK) else
-  if s = "strb" then (KeywordT StoreBK) else
+  if s = "stw" then (KeywordT StoreK) else
+  if s = "st8" then (KeywordT StoreBK) else
   if s = "if" then (KeywordT IfK) else
   if s = "else" then (KeywordT ElseK) else
   if s = "while" then (KeywordT WhileK) else
@@ -108,12 +110,14 @@ Definition get_keyword_def:
   if s = "with" then (KeywordT WithK) else
   if s = "handle" then (KeywordT HandleK) else
   if s = "lds" then (KeywordT LdsK) else
-  if s = "ldb" then (KeywordT LdbK) else
+  if s = "ldw" then (KeywordT LdwK) else
+  if s = "ld8" then (KeywordT LdbK) else
   if s = "@base" then (KeywordT BaseK) else
   if s = "true" then (KeywordT TrueK) else
   if s = "false" then (KeywordT FalseK) else
   if s = "fun" then (KeywordT FunK) else
-  if isPREFIX "@" s ∨ s = "" then LexErrorT else
+  if s = "" ∨ s = "@" then LexErrorT else
+  if 2 <= LENGTH s ∧ EL 0 s = #"@" then ForeignIdent (DROP 1 s) else
   IdentT s
 End
 

pancake/parser/panPEGScript.sml

@@ -26,6 +26,8 @@ Datatype:
             | StructNT | LoadNT | LoadByteNT | LabelNT | FLabelNT
             | ShapeNT | ShapeCombNT
             | EqOpsNT | CmpOpsNT | ShiftOpsNT | AddOpsNT | MulOpsNT
+            | SharedLoadNT | SharedLoadByteNT
+            | SharedStoreNT | SharedStoreByteNT
 End
 
 Definition mknt_def:
@@ -70,6 +72,12 @@ Definition keep_ident_def:
                        | _ => F) mkleaf
 End
 
+Definition keep_ffi_ident_def:
+  keep_ffi_ident = tok (λt. case t of
+                       | ForeignIdent _ => T
+                       | _ => F) mkleaf
+End
+
 Definition keep_int_def:
   keep_int = tok (λt. case t of
                        | IntT _ => T
@@ -136,6 +144,10 @@ Definition pancake_peg_def[nocompute]:
                               mknt CallNT;
                               mknt AssignNT; mknt StoreNT;
                               mknt StoreByteNT;
+                              mknt SharedLoadByteNT;
+                              mknt SharedLoadNT;
+                              mknt SharedStoreByteNT;
+                              mknt SharedStoreNT;
                               keep_kw BrK; keep_kw ContK;
                               mknt ExtCallNT;
                               mknt RaiseNT; mknt ReturnNT;
@@ -176,7 +188,7 @@ Definition pancake_peg_def[nocompute]:
                              consume_tok DArrowT; mknt ProgNT;
                              consume_kw HandleK]
                             (mksubtree HandleNT));
-        (INL ExtCallNT, seql [consume_tok HashT; keep_ident;
+        (INL ExtCallNT, seql [keep_ffi_ident;
                               consume_tok LParT; mknt ExpNT;
                               consume_tok CommaT; mknt ExpNT;
                               consume_tok CommaT; mknt ExpNT;
@@ -257,7 +269,20 @@ Definition pancake_peg_def[nocompute]:
         (INL ShiftOpsNT, choicel [keep_tok LslT; keep_tok LsrT;
                                   keep_tok AsrT; keep_tok RorT]);
         (INL AddOpsNT, choicel [keep_tok PlusT; keep_tok MinusT]);
-        (INL MulOpsNT, keep_tok StarT)]
+        (INL MulOpsNT, keep_tok StarT);
+        (INL SharedLoadNT,seql [consume_tok NotT; consume_kw LdwK; keep_ident;
+                                consume_tok CommaT; mknt ExpNT]
+                               (mksubtree SharedLoadNT));
+        (INL SharedLoadByteNT,seql [consume_tok NotT; consume_kw LdbK; keep_ident;
+                                    consume_tok CommaT; mknt ExpNT]
+                                   (mksubtree SharedLoadByteNT));
+        (INL SharedStoreNT,seql [consume_tok NotT; consume_kw StoreK; keep_ident;
+                                 consume_tok CommaT; mknt ExpNT]
+                                (mksubtree SharedStoreNT));
+        (INL SharedStoreByteNT,seql [consume_tok NotT; consume_kw StoreBK; keep_ident;
+                                     consume_tok CommaT; mknt ExpNT]
+                                    (mksubtree SharedStoreByteNT));
+        ]
         |>
 End
 
@@ -367,14 +392,16 @@ val wfpeg_rwts = wfpeg_cases
                                      ‘choicel (h::t)’, ‘keep_tok t’,
                                      ‘consume_tok t’, ‘keep_kw k’,
                                      ‘consume_kw k’, ‘keep_int’,
-                                     ‘keep_nat’, ‘keep_ident’,
+                                     ‘keep_nat’,‘keep_ffi_ident’,
+                                     ‘keep_ident’,
                                      ‘pegf e f’])
                    |> map (CONV_RULE
                            (RAND_CONV (SIMP_CONV (srw_ss())
                                        [choicel_def, seql_def,
                                         keep_tok_def, consume_tok_def,
                                         keep_kw_def, consume_kw_def,
                                         keep_int_def, keep_nat_def,
+                                        keep_ffi_ident_def,
                                         keep_ident_def, pegf_def])))
 
 val wfpeg_mknt = wfpeg_cases
@@ -472,6 +499,12 @@ Proof
   simp[keep_ident_def]
 QED
 
+Theorem peg0_keep_ffi_ident[simp]:
+  peg0 G keep_ffi_ident = F
+Proof
+  simp[keep_ffi_ident_def]
+QED
+
 Theorem peg0_choicel[simp]:
   (peg0 G (choicel []) = F) ∧
   (peg0 G (choicel (h::t)) ⇔
@@ -504,8 +537,11 @@ val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”
                 “RaiseNT”, “ExtCallNT”,
                 “HandleNT”, “RetNT”, “CallNT”,
                 “WhileNT”, “IfNT”, “StoreByteNT”,
-                “StoreNT”, “AssignNT”, “DecNT”,
-                “StmtNT”, “BlockNT”, “ParamListNT”, “FunNT”];
+                “StoreNT”, “AssignNT”,
+                “SharedLoadByteNT”, “SharedLoadNT”,
+                “SharedStoreByteNT”, “SharedStoreNT”, “DecNT”,
+                “StmtNT”, “BlockNT”, “ParamListNT”, “FunNT”
+                ];
 
 (*  “FunNT”, “FunListNT” *)
 
@@ -521,7 +557,7 @@ fun wfnt(t,acc) = let
                     [wfpeg_mknt, FDOM_pancake_peg, try_def,
                      seql_def, keep_tok_def, consume_tok_def,
                      keep_kw_def, consume_kw_def, keep_int_def,
-                     keep_nat_def, keep_ident_def]) THEN
+                     keep_nat_def, keep_ident_def, keep_ffi_ident_def]) THEN
           simp(wfpeg_rwts @ npeg0_rwts @ peg0_rwts @ acc))
 in
   th::acc
@@ -544,7 +580,7 @@ Proof
        subexprs_mknt, peg_start, peg_range, DISJ_IMP_THM,FORALL_AND_THM,
        choicel_def, seql_def, pegf_def, keep_tok_def, consume_tok_def,
        keep_kw_def, consume_kw_def, keep_int_def, keep_nat_def,
-       keep_ident_def, try_def] >>
+       keep_ident_def, keep_ffi_ident_def, try_def] >>
   simp(pancake_wfpeg_thm :: wfpeg_rwts @ peg0_rwts @ npeg0_rwts)
 QED
 

pancake/parser/panPtreeConversionScript.sml

@@ -90,6 +90,13 @@ Definition conv_ident_def:
     | _ => NONE
 End
 
+Definition conv_ffi_ident_def:
+  conv_ffi_ident tree =
+    case destTOK ' (destLf tree) of
+      SOME (ForeignIdent s) => SOME (strlit s)
+    | _ => NONE
+End
+
 Definition conv_var_def:
   conv_var t = lift Var (conv_ident t)
 End
@@ -339,10 +346,26 @@ Definition conv_NonRecStmt_def:
       case args of
         [dst; src] => lift2 StoreByte (conv_Exp dst) (conv_Exp src)
       | _ => NONE
+    else if isNT nodeNT SharedLoadNT then
+      case args of
+        [v; e] => lift2 (ShMem Load) (conv_ident v) (conv_Exp e)
+      | _ => NONE
+    else if isNT nodeNT SharedLoadByteNT then
+      case args of
+        [v; e] => lift2 (ShMem Load8) (conv_ident v) (conv_Exp e)
+      | _ => NONE
+    else if isNT nodeNT SharedStoreNT then
+      case args of
+        [v; e] => lift2 (ShMem Store) (conv_ident v) (conv_Exp e)
+      | _ => NONE
+    else if isNT nodeNT SharedStoreByteNT then
+      case args of
+        [v; e] => lift2 (ShMem Store8) (conv_ident v) (conv_Exp e)
+      | _ => NONE
     else if isNT nodeNT ExtCallNT then
       case args of
         [name; ptr; clen; array; alen] =>
-          do name' <- conv_ident name;
+          do name' <- conv_ffi_ident name;
              ptr' <- conv_Exp ptr;
              clen' <- conv_Exp clen;
              array' <- conv_Exp array;