diff --git a/compiler/bootstrap/translation/from_pancake32ProgScript.sml b/compiler/bootstrap/translation/from_pancake32ProgScript.sml index e67719c80c..7fa0a8ffd3 100644 --- a/compiler/bootstrap/translation/from_pancake32ProgScript.sml +++ b/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; diff --git a/compiler/bootstrap/translation/from_pancake64ProgScript.sml b/compiler/bootstrap/translation/from_pancake64ProgScript.sml index c6e537f222..cc1193aaa6 100644 --- a/compiler/bootstrap/translation/from_pancake64ProgScript.sml +++ b/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; diff --git a/compiler/bootstrap/translation/pancake_lexProgScript.sml b/compiler/bootstrap/translation/pancake_lexProgScript.sml index 7c4d04e57f..162e072528 100644 --- a/compiler/bootstrap/translation/pancake_lexProgScript.sml +++ b/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; diff --git a/pancake/parser/README.md b/pancake/parser/README.md index 3275ef4e74..b7ce44aae1 100644 --- a/pancake/parser/README.md +++ b/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. diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml index 8a4d5d3b0c..8f4e47317b 100644 --- a/pancake/parser/panConcreteExamplesScript.sml +++ b/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(); diff --git a/pancake/parser/panLexerScript.sml b/pancake/parser/panLexerScript.sml index e65869189b..46ae519132 100644 --- 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 | 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 "#=>>>" 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 diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index dc10fdcc3b..375d52c244 100644 --- a/pancake/parser/panPEGScript.sml +++ b/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,7 +392,8 @@ 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()) @@ -375,6 +401,7 @@ val wfpeg_rwts = wfpeg_cases 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 diff --git a/pancake/parser/panPtreeConversionScript.sml b/pancake/parser/panPtreeConversionScript.sml index a537789a26..3cfd19a40e 100644 --- a/pancake/parser/panPtreeConversionScript.sml +++ b/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;