Skip to content

Commit

Permalink
Merge pull request #1049 from halogentlepersuasion/pan_loadprec
Browse files Browse the repository at this point in the history
  • Loading branch information
@myreen
myreen committed Aug 29, 2024
2 parents f3c3408 + 2752848 commit aae58d5
Show file tree
Hide file tree
Showing 6 changed files with 47 additions and 33 deletions.
4 changes: 2 additions & 2 deletions compiler/bootstrap/translation/from_pancake32ProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -497,12 +497,12 @@ Definition conv_Exp_alt_def:
case args of
[t] => OPTION_MAP (λe. Cmp Equal (Const 0w) e) (conv_Exp_alt t)
| _ => NONE
else if isNT nodeNT LoadByteNT then
else if isNT nodeNT ELoadByteNT then
case args of
[] => NONE
| [t] => OPTION_MAP LoadByte (conv_Exp_alt t)
| t::v6::v7 => NONE
else if isNT nodeNT LoadNT then
else if isNT nodeNT ELoadNT then
case args of
[] => NONE
| [t1] => NONE
Expand Down
4 changes: 2 additions & 2 deletions compiler/bootstrap/translation/from_pancake64ProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -502,12 +502,12 @@ Definition conv_Exp_alt_def:
case args of
[t] => OPTION_MAP (λe. Cmp Equal (Const 0w) e) (conv_Exp_alt t)
| _ => NONE
else if isNT nodeNT LoadByteNT then
else if isNT nodeNT ELoadByteNT then
case args of
[] => NONE
| [t] => OPTION_MAP LoadByte (conv_Exp_alt t)
| t::v6::v7 => NONE
else if isNT nodeNT LoadNT then
else if isNT nodeNT ELoadNT then
case args of
[] => NONE
| [t1] => NONE
Expand Down
13 changes: 12 additions & 1 deletion pancake/parser/panConcreteExamplesScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ val ex9 = ‘
var c = @base + 16;
var d = 1;
@out_morefun(a,b,c,d);
stw @base, ic;
st @base, ic;
return 0;
}’;

Expand Down Expand Up @@ -339,6 +339,17 @@ val struct_argument_parse_tree = parse_tree_pancake $ struct_arguments;

val struct_argument_parse = parse_pancake $ struct_arguments;

val locmem_ex = ‘
fun test_locmem() {
var v = 12;
st 1000, 1 + 1; // store 1 + 1 (ie 2) at local memory address 1000
st8 1000 + 4, v; // store byte from variable v (12) to local memory address 1004
v = lds 1 1000 + 8; // load word from local address 1008 and assign to variable v
v = ld8 1000 + 4 * 3; // load byte from local address 1012 and assign to variable v
}’;

val locmem_ex_parse = check_success $ parse_pancake locmem_ex;

val shmem_ex = ‘
fun test_shmem() {
var v = 12;
Expand Down
13 changes: 7 additions & 6 deletions pancake/parser/panLexerScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ open mlstringTheory;
val _ = new_theory "panLexer";

Datatype:
keyword = SkipK | StoreK | StoreBK | Store32K | IfK | ElseK | WhileK
keyword = SkipK | StK | StwK | St8K | St32K | IfK | ElseK | WhileK
| BrK | ContK | RaiseK | RetK | TicK | VarK | WithK | HandleK | BiwK
| LdsK | LdbK | LdwK | Ld32K | BaseK | InK | FunK | ExportK | TrueK | FalseK
| LdsK | Ld8K | LdwK | Ld32K | BaseK | InK | FunK | ExportK | TrueK | FalseK
End

Datatype:
Expand Down Expand Up @@ -114,9 +114,10 @@ End
Definition get_keyword_def:
get_keyword s =
if s = "skip" then (KeywordT SkipK) else
if s = "stw" then (KeywordT StoreK) else
if s = "st8" then (KeywordT StoreBK) else
if s = "st32" then (KeywordT Store32K) else
if s = "st" then (KeywordT StK) else
if s = "stw" then (KeywordT StwK) else
if s = "st8" then (KeywordT St8K) else
if s = "st32" then (KeywordT St32K) else
if s = "if" then (KeywordT IfK) else
if s = "else" then (KeywordT ElseK) else
if s = "while" then (KeywordT WhileK) else
Expand All @@ -131,7 +132,7 @@ Definition get_keyword_def:
if s = "handle" then (KeywordT HandleK) else
if s = "lds" then (KeywordT LdsK) else
if s = "ldw" then (KeywordT LdwK) else
if s = "ld8" then (KeywordT LdbK) else
if s = "ld8" then (KeywordT Ld8K) else
if s = "ld32" then (KeywordT Ld32K) else
if s = "@base" then (KeywordT BaseK) else
if s = "@biw" then (KeywordT BiwK) else
Expand Down
42 changes: 22 additions & 20 deletions pancake/parser/panPEGScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,12 @@ Datatype:
| DecCallNT | RetCallNT
| ArgListNT | NotNT
| ParamListNT
| EXorNT | EOrNT | EAndNT | EEqNT | ECmpNT
| EBoolAndNT | EEqNT | ECmpNT
| ELoadNT | ELoadByteNT
| EXorNT | EOrNT | EAndNT
| EShiftNT | EAddNT | EMulNT
| EBaseNT | EBoolAndNT
| StructNT | LoadNT | LoadByteNT | LabelNT | FLabelNT
| EBaseNT
| StructNT | LabelNT | FLabelNT
| ShapeNT | ShapeCombNT
| EqOpsNT | CmpOpsNT | ShiftOpsNT | AddOpsNT | MulOpsNT
| SharedLoadNT | SharedLoadByteNT | SharedLoad32NT
Expand Down Expand Up @@ -182,10 +184,10 @@ Definition pancake_peg_def[nocompute]:
(mksubtree DecNT));
(INL AssignNT, seql [keep_ident; consume_tok AssignT;
mknt ExpNT] (mksubtree AssignNT));
(INL StoreNT, seql [consume_kw StoreK; mknt ExpNT;
(INL StoreNT, seql [consume_kw StK; mknt ExpNT;
consume_tok CommaT; mknt ExpNT]
(mksubtree StoreNT));
(INL StoreByteNT, seql [consume_kw StoreBK; mknt ExpNT;
(INL StoreByteNT, seql [consume_kw St8K; mknt ExpNT;
consume_tok CommaT; mknt ExpNT]
(mksubtree StoreByteNT));
(INL IfNT, seql [consume_kw IfK; mknt ExpNT; consume_tok LCurT;
Expand Down Expand Up @@ -243,9 +245,15 @@ Definition pancake_peg_def[nocompute]:
(INL EEqNT, seql [mknt ECmpNT;
try (seql [mknt EqOpsNT; mknt ECmpNT] I)]
(mksubtree EEqNT));
(INL ECmpNT, seql [mknt EOrNT;
try (seql [mknt CmpOpsNT; mknt EOrNT] I)]
(INL ECmpNT, seql [mknt ELoadNT;
try (seql [mknt CmpOpsNT; mknt ELoadNT] I)]
(mksubtree ECmpNT));
(INL ELoadNT, choicel [seql [consume_kw LdsK; mknt ShapeNT; mknt ELoadByteNT]
(mksubtree ELoadNT);
mknt ELoadByteNT]);
(INL ELoadByteNT, choicel [seql [consume_kw Ld8K; mknt EOrNT]
(mksubtree ELoadByteNT);
mknt EOrNT]);
(INL EOrNT, seql [mknt EXorNT;
rpt (seql [keep_tok OrT; mknt EXorNT] I)
FLAT]
Expand Down Expand Up @@ -275,8 +283,7 @@ Definition pancake_peg_def[nocompute]:
mknt NotNT;
keep_kw TrueK; keep_kw FalseK;
keep_int; keep_ident; mknt LabelNT;
mknt StructNT; mknt LoadNT;
mknt LoadByteNT; keep_kw BaseK; keep_kw BiwK;
mknt StructNT; keep_kw BaseK; keep_kw BiwK;
];
rpt (seql [consume_tok DotT; keep_nat] I)
FLAT]
Expand All @@ -290,10 +297,6 @@ Definition pancake_peg_def[nocompute]:
(INL StructNT, seql [consume_tok LessT; mknt ArgListNT;
consume_tok GreaterT]
(mksubtree StructNT));
(INL LoadNT, seql [consume_kw LdsK; mknt ShapeNT; mknt ExpNT]
(mksubtree LoadNT));
(INL LoadByteNT, seql [consume_kw LdbK; mknt ExpNT]
(mksubtree LoadByteNT));
(INL ShapeNT, choicel [keep_int;
seql [consume_tok LCurT;
mknt ShapeCombNT;
Expand All @@ -313,19 +316,19 @@ Definition pancake_peg_def[nocompute]:
(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;
(INL SharedLoadByteNT,seql [consume_tok NotT; consume_kw Ld8K; keep_ident;
consume_tok CommaT; mknt ExpNT]
(mksubtree SharedLoadByteNT));
(INL SharedLoad32NT,seql [consume_tok NotT; consume_kw Ld32K; keep_ident;
consume_tok CommaT; mknt ExpNT]
(mksubtree SharedLoad32NT));
(INL SharedStoreNT,seql [consume_tok NotT; consume_kw StoreK; mknt ExpNT;
(INL SharedStoreNT,seql [consume_tok NotT; consume_kw StwK; mknt ExpNT;
consume_tok CommaT; mknt ExpNT]
(mksubtree SharedStoreNT));
(INL SharedStoreByteNT,seql [consume_tok NotT; consume_kw StoreBK; mknt ExpNT;
(INL SharedStoreByteNT,seql [consume_tok NotT; consume_kw St8K; mknt ExpNT;
consume_tok CommaT; mknt ExpNT]
(mksubtree SharedStoreByteNT));
(INL SharedStore32NT,seql [consume_tok NotT; consume_kw Store32K; mknt ExpNT;
(INL SharedStore32NT,seql [consume_tok NotT; consume_kw St32K; mknt ExpNT;
consume_tok CommaT; mknt ExpNT]
(mksubtree SharedStore32NT));
]
Expand Down Expand Up @@ -637,10 +640,9 @@ end

val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”,
“EqOpsNT”, “ShapeNT”,
“ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “LoadByteNT”,
“LoadNT”, “StructNT”,
“ShapeCombNT”, “NotNT”, “LabelNT”, “FLabelNT”, “StructNT”,
“EBaseNT”, “EMulNT”, “EAddNT”, “EShiftNT”, “EAndNT”, “EXorNT”, “EOrNT”,
“ECmpNT”, “EEqNT”, “EBoolAndNT”,
“ELoadByteNT”, “ELoadNT”, “ECmpNT”, “EEqNT”, “EBoolAndNT”,
“ExpNT”, “ArgListNT”, “ReturnNT”,
“RaiseNT”, “ExtCallNT”,
“HandleNT”, “RetNT”, “RetCallNT”, “CallNT”,
Expand Down
4 changes: 2 additions & 2 deletions pancake/parser/panPtreeConversionScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -274,11 +274,11 @@ Definition conv_Exp_def:
case args of
[t] => lift (Cmp Equal (Const 0w)) (conv_Exp t)
| _ => NONE
else if isNT nodeNT LoadByteNT then
else if isNT nodeNT ELoadByteNT then
case args of
[t] => lift LoadByte (conv_Exp t)
| _ => NONE
else if isNT nodeNT LoadNT then
else if isNT nodeNT ELoadNT then
case args of
[t1; t2] => do s <- conv_Shape t1;
e <- conv_Exp t2;
Expand Down

0 comments on commit aae58d5

Please sign in to comment.