Make spec compile again
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 6ce1f83..fa8f6ea 100644 --- a/spectec/doc/example/output/NanoWasm.pdf +++ b/spectec/doc/example/output/NanoWasm.pdf Binary files differ
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index 5906910..102c667 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml
@@ -1823,7 +1823,7 @@ | (Il.VariantT tcs1, dots1), (Il.VariantT tcs2, dots2) -> let* () = - (* Shallow recursive breadth subtyping on variants *) + (* Recursive subtyping on variants *) match iter_attempt (fun (mixop, (tC1, _, _), _) -> let* _, (tC2, _, _), _ = attempt (find_case tcs2 mixop t1.at) t2 in @@ -2457,46 +2457,6 @@ d | _ -> d -let infer_fundef env (d : def) = - match d.it with - | DecD (x, ps, t, _hints) -> - let env' = local_env env in - let ps' = elab_params env' ps in - let t' = elab_typ env' t in - if env'.pm then error d.at "misplaced +- or -+ operator in declaration"; - let dims = Dim.check Map.empty ps' [] [t'] [] [] [] in - let t' = Dim.annot_typ dims t' in - infer_no_quants env dims Det.empty ps' [] [t'] [] [] [] d.at; - env.defs <- bind "definition" env.defs x (ps', t', []); - | _ -> () - -let infer_reldef env (d : def) = - match d.it with - | RelD (x, ps, t, _hints) -> - let env' = local_env env in - let ps' = elab_params env' ps in - let mixop, xts' = elab_typ_notation' env' x t in - let ts' = List.map snd xts' in - if env'.pm then error d.at "misplaced +- or -+ operator in relation"; - let dims = Dim.check Map.empty [] [] ts' [] [] [] in - let ts' = List.map (Dim.annot_typ dims) ts' in - infer_no_quants env' dims Det.empty [] [] ts' [] [] [] d.at; - let not = Mixop.apply mixop (List.map (fun t' -> "_" $ d.at, t') ts') in - let t' = tup_typ' ts' t.at in - env.rels <- bind "relation" env.rels x (ps', t', [], mixop, not); - | _ -> () - -let infer_gramdef env (d : def) = - match d.it with - | GramD (x1, _x2, ps, t, _gram, _hints) -> - if not (bound env.grams x1) then ( - let env' = local_env env in - let ps' = elab_params env' ps in - let t' = elab_typ env' t in - env.grams <- bind "grammar" env.grams x1 (ps', t', [], None); - ) - | _ -> () - let elab_hintdef _env (hd : hintdef) : Il.def list = match hd.it with | TypH (id1, _id2, hints) -> @@ -2514,9 +2474,9 @@ [] -let rec elab_def env (d : def) : Il.def list = - Debug.(log_in "el.elab_def" line); - Debug.(log_in_at "el.elab_def" d.at (fun _ -> el_def d)); +let rec elab_def_pass1 env (d : def) : Il.def list = + Debug.(log_in "el.elab_def_pass1" line); + Debug.(log_in_at "el.elab_def_pass1" d.at (fun _ -> el_def d)); let env' = local_env env in env'.pm <- false; match d.it with @@ -2561,7 +2521,71 @@ env.typs <- rebind "syntax type" env.typs x1 (ps', k'); (if not last then [] else [Il.TypD (x1, ps', [inst']) $ d.at]) @ elab_hintdef env (TypH (x1, x2, hints) $ d.at) @ - (if not env'.pm then [] else elab_def env Subst.(subst_def pm_snd (Iter.clone_def d))) + (if not env'.pm then [] else elab_def_pass1 env Subst.(subst_def pm_snd (Iter.clone_def d))) + + | GramD (x1, _x2, ps, t, _gram, _hints) -> + if not (bound env.grams x1) then ( + let env' = local_env env in + let ps' = elab_params env' ps in + let t' = elab_typ env' t in + env.grams <- bind "grammar" env.grams x1 (ps', t', [], None); + ); + [] + + | RelD (x, ps, t, hints) -> + let ps' = elab_params env' ps in + let mixop, xts' = elab_typ_notation' env' x t in + let ts' = List.map snd xts' in + if env'.pm then error d.at "misplaced +- or -+ operator in relation"; + let dims = Dim.check Map.empty [] [] ts' [] [] [] in + let ts' = List.map (Dim.annot_typ dims) ts' in + infer_no_quants env' dims Det.empty [] [] ts' [] [] [] d.at; + let not = Mixop.apply mixop (List.map (fun t' -> "_" $ d.at, t') ts') in + let t' = tup_typ' ts' t.at in + env.rels <- bind "relation" env.rels x (ps', t', [], mixop, not); + [Il.RelD (x, ps', mixop, t', []) $ d.at] + @ elab_hintdef env (RelH (x, hints) $ d.at) + + | RuleD _ -> [] + + | VarD (x, t, _hints) -> + let t' = elab_typ env' t in + if env'.pm then + error d.at "misplaced +- or -+ operator in variable declaration"; + let dims = Dim.check Map.empty [] [] [t'] [] [] [] in + let t' = Dim.annot_typ dims t' in + infer_no_quants env' dims Det.empty [] [] [t'] [] [] [] d.at; + env.gvars <- rebind "variable" env.gvars x t'; + [] + + | DecD (x, ps, t, hints) -> + let ps' = elab_params env' ps in + let t' = elab_typ env' t in + if env'.pm then error d.at "misplaced +- or -+ operator in declaration"; + let d' = Il.DecD (x, ps', t', []) $ d.at in + let dims = Dim.check Map.empty ps' [] [t'] [] [] [] in + let t' = Dim.annot_typ dims t' in + infer_no_quants env dims Det.empty ps' [] [t'] [] [] [] d.at; + env.defs <- bind "definition" env.defs x (ps', t', []); + [d'] @ elab_hintdef env (DecH (x, hints) $ d.at) + + | DefD _ -> [] + + | SepD -> [] + + | HintD hd -> + elab_hintdef env' hd + + +let rec elab_def_pass2 env (d : def) : Il.def list = + Debug.(log_in "el.elab_def_pass2" line); + Debug.(log_in_at "el.elab_def_pass2" d.at (fun _ -> el_def d)); + let env' = local_env env in + env'.pm <- false; + match d.it with + | FamD _ -> [] + + | TypD _ -> [] | GramD (x1, x2, ps, t, gram, hints) -> let ps' = elab_params env' ps in @@ -2598,19 +2622,7 @@ (if dots2 = Dots then [] else [Il.GramD (x1, ps', t', []) $ d.at]) @ elab_hintdef env (GramH (x1, x2, hints) $ d.at) - | RelD (x, ps, t, hints) -> - let ps' = elab_params env' ps in - let mixop, xts' = elab_typ_notation' env' x t in - let ts' = List.map snd xts' in - if env'.pm then error d.at "misplaced +- or -+ operator in relation"; - let dims = Dim.check Map.empty [] [] ts' [] [] [] in - let ts' = List.map (Dim.annot_typ dims) ts' in - infer_no_quants env' dims Det.empty [] [] ts' [] [] [] d.at; - let not = Mixop.apply mixop (List.map (fun t' -> "_" $ d.at, t') ts') in - let t' = tup_typ' ts' t.at in - env.rels <- rebind "relation" env.rels x (ps', t', [], mixop, not); - [Il.RelD (x, ps', mixop, t', []) $ d.at] - @ elab_hintdef env (RelH (x, hints) $ d.at) + | RelD _ -> [] | RuleD (x1, ps, x2, e, prems) -> let ps', t', rules', mixop, not' = find "relation" env.rels x1 in @@ -2630,28 +2642,11 @@ let qs = infer_quants env env' dims det [] [] [] es' [] prems' d.at in let rule' = Il.RuleD (x2, qs, mixop, e', prems') $ d.at in env.rels <- rebind "relation" env.rels x1 (ps', t', rules' @ [x2, rule'], mixop, not'); - if not env'.pm then [] else elab_def env Subst.(subst_def pm_snd (Iter.clone_def d)) + if not env'.pm then [] else elab_def_pass2 env Subst.(subst_def pm_snd (Iter.clone_def d)) - | VarD (x, t, _hints) -> - let t' = elab_typ env' t in - if env'.pm then - error d.at "misplaced +- or -+ operator in variable declaration"; - let dims = Dim.check Map.empty [] [] [t'] [] [] [] in - let t' = Dim.annot_typ dims t' in - infer_no_quants env' dims Det.empty [] [] [t'] [] [] [] d.at; - env.gvars <- rebind "variable" env.gvars x t'; - [] + | VarD _ -> [] - | DecD (x, ps, t, hints) -> - let ps' = elab_params env' ps in - let t' = elab_typ env' t in - if env'.pm then error d.at "misplaced +- or -+ operator in declaration"; - let d' = Il.DecD (x, ps', t', []) $ d.at in - let dims = Dim.check Map.empty ps' [] [t'] [] [] [] in - let t' = Dim.annot_typ dims t' in - infer_no_quants env dims Det.empty ps' [] [t'] [] [] [] d.at; - env.defs <- rebind "definition" env.defs x (ps', t', []); - [d'] @ elab_hintdef env (DecH (x, hints) $ d.at) + | DecD _ -> [] | DefD (x, as_, e, prems) -> let ps', t', clauses' = find "definition" env.defs x in @@ -2667,13 +2662,11 @@ let qs = infer_quants env env' dims det [] as' [] [e'] [] prems' d.at in let clause' = Il.DefD (qs, as', e', prems') $ d.at in env.defs <- rebind "definition" env.defs x (ps', t', clauses' @ [(d, clause')]); - if not env'.pm then [] else elab_def env Subst.(subst_def pm_snd (Iter.clone_def d)) + if not env'.pm then [] else elab_def_pass2 env Subst.(subst_def pm_snd (Iter.clone_def d)) - | SepD -> - [] + | SepD -> [] - | HintD hd -> - elab_hintdef env' hd + | HintD _ -> [] let check_dots env = @@ -2795,12 +2788,10 @@ let env = new_env () in let ds = List.map (infer_typdef env) ds in let ds = Map.fold implicit_typdef env.atoms ds in - List.iter (infer_fundef env) ds; - List.iter (infer_reldef env) ds; - List.iter (infer_gramdef env) ds; - let ds' = List.concat_map (elab_def env) ds in + let ds1' = List.concat_map (elab_def_pass1 env) ds in + let ds2' = List.concat_map (elab_def_pass2 env) ds in check_dots env; - let ds' = List.map (populate_def env) ds' in + let ds' = List.map (populate_def env) (ds1' @ ds2') in recursify_defs ds', env let elab_exp env (e : exp) (t : typ) : Il.exp =
diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly index e343b1b..8106e2d 100644 --- a/spectec/src/frontend/parser.mly +++ b/spectec/src/frontend/parser.mly
@@ -404,6 +404,7 @@ | DOTDOT { Atom.Dot2 } | DOTDOTDOT { Atom.Dot3 } | SEMICOLON { Atom.Semicolon } + | BACKSLASH { Atom.Backslash } | ARROW { Atom.Arrow } | ARROW2 { Atom.Arrow2 } | ARROWSUB { Atom.ArrowSub }
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 59328a5..2c294e7 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md
@@ -7326,6 +7326,384 @@ -- Expand: `%~~%`(s.FUNCS_store[funcaddr].TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (Val_ok: `%|-%:%`(s, val, t_1))*{t_1 <- `t_1*`, val <- `val*`} +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax castop = (null?, null?) + +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax memidxop = (memidx, memarg) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax startopt = start* + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax code = (local*, expr) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax nopt = u32* + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +def $ieee_(N : N, rat : rat) : fNmag(N) + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax idctxt = +{ + TYPES name?*, + TAGS name?*, + GLOBALS name?*, + MEMS name?*, + TABLES name?*, + FUNCS name?*, + DATAS name?*, + ELEMS name?*, + LOCALS name?*, + LABELS name?*, + FIELDS name?**, + TYPEDEFS deftype?* +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax I = idctxt + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +rec { + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 +def $concat_idctxt(idctxt*) : idctxt + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 + def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 + def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +relation Idctxt_ok: `|-%:OK`(idctxt) + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec + rule _{I : I, `field**` : char**}: + `|-%:OK`(I) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) + -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} + -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $dots : () + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +syntax decl = + | TYPE(rectype : rectype) + | IMPORT(name : name, name : name, externtype : externtype) + | TAG(tagtype : tagtype) + | GLOBAL(globaltype : globaltype, expr : expr) + | MEMORY(memtype : memtype) + | TABLE(tabletype : tabletype, expr : expr) + | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) + | DATA(`byte*` : byte*, datamode : datamode) + | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) + | START(funcidx : funcidx) + | EXPORT(name : name, externidx : externidx) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 +def $typesd(decl*) : type* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 + def $typesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 + def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 + def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 +def $importsd(decl*) : import* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 + def $importsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 + def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 + def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 +def $tagsd(decl*) : tag* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 + def $tagsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 + def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 + def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 +def $globalsd(decl*) : global* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 + def $globalsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 + def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 + def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 +def $memsd(decl*) : mem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 + def $memsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 + def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 + def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 +def $tablesd(decl*) : table* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 + def $tablesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 + def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 + def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 +def $funcsd(decl*) : func* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 + def $funcsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 + def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 + def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 +def $datasd(decl*) : data* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 + def $datasd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 + def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 + def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 +def $elemsd(decl*) : elem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 + def $elemsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 + def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 + def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 +def $startsd(decl*) : start* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 + def $startsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 + def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 + def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 +def $exportsd(decl*) : export* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 + def $exportsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 + def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 + def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $ordered(decl*) : bool + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true + -- if ($importsd(decl*{decl <- `decl*`}) = []) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax A = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax B = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax sym = + | _FIRST(A_1 : A) + | _DOTS + | _LAST(A_n : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax symsplit = + | _FIRST(A_1 : A) + | _LAST(A_2 : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax recorddots = () + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax record = +{ + FIELD_1 A, + FIELD_2 A, + `...` recorddots +} + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax pth = + | PTHSYNTAX + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +syntax T = nat + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremise: `%`(nat) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremisedots: `...` + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingScheme: `%`(nat) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec + rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: + `%`(conclusion) + -- NotationTypingPremise: `%`(premise_1) + -- NotationTypingPremise: `%`(premise_2) + -- NotationTypingPremisedots: `...` + -- NotationTypingPremise: `%`(premise_n) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +rec { + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 +relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 + rule `i32.add`{C : context}: + `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 + rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: + `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) + -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 + rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: + `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) +} + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +relation NotationReduct: `~>%`(instr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 4{q_6 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_6)]) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $instrdots : instr* + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax label = + | `LABEL_%{%}`(n : n, `instr*` : instr*) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax callframe = + | `FRAME_%{%}`(n : n, frame : frame) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +rec { + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 +def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 + def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 + def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) + -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) + -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) +} + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +syntax symdots = + | `%`(i : nat) + -- if (i = 0) + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +def $var(syntax X) : nat + ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec + def $var{syntax X}(syntax X) = 0 + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax abbreviated = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax expanded = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax syntax = () + ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec grammar Bbyte : byte ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec @@ -7649,9 +8027,6 @@ prod{jt : tagtype} {{0x04} {jt:Btagtype}} => TAG_externtype(jt) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax castop = (null?, null?) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bcastop : castop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod 0x00 => (?(), ?()) @@ -7684,9 +8059,6 @@ prod{l : labelidx} {{0x03} {l:Blabelidx}} => CATCH_ALL_REF_catch(l) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax memidxop = (memidx, memarg) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bmemarg : memidxop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod{n : n, m : m} {{`%`_u32(n):Bu32} {`%`_u64(m):Bu64}} => (`%`_memidx(0), {ALIGN `%`_u32(n), OFFSET `%`_u64(m)}) @@ -8800,9 +9172,6 @@ prod{x : idx} x:Bfuncidx => [START_start(x)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax startopt = start* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bstartsec : start? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt) @@ -8837,9 +9206,6 @@ prod{`elem*` : elem*} elem*{elem <- `elem*`}:Bsection_(9, syntax elem, grammar Blist(syntax elem, grammar Belem)) => elem*{elem <- `elem*`} ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax code = (local*, expr) - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Blocals : local* ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{t : valtype, n : n} {{`%`_u32(n):Bu32} {t:Bvaltype}} => LOCAL_local(t)^n{} @@ -8881,9 +9247,6 @@ prod{n : n} `%`_u32(n):Bu32 => [`%`_u32(n)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax nopt = u32* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bdatacntsec : u32? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{nopt : nopt} nopt:Bsection_(12, syntax u32, grammar Bdatacnt) => $opt_(syntax u32, nopt) @@ -9302,9 +9665,6 @@ prod{p : nat, q : rat} {{p:Thexnum} {"."} {q:Thexfrac}} => ((p + (q : rat <:> nat)) : nat <:> rat) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -def $ieee_(N : N, rat : rat) : fNmag(N) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tfloat : rat ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{p : rat, s : int, ee : nat} {{p:Tmant} ({"E"} | {"e"}) {s:Tsign} {ee:Tnum}} => (p * ((10 ^ ((s * (ee : nat <:> int)) : int <:> nat)) : nat <:> rat)) @@ -9389,55 +9749,6 @@ -- if (|el*{el <- `el*`}| < (2 ^ 32)) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax idctxt = -{ - TYPES name?*, - TAGS name?*, - GLOBALS name?*, - MEMS name?*, - TABLES name?*, - FUNCS name?*, - DATAS name?*, - ELEMS name?*, - LOCALS name?*, - LABELS name?*, - FIELDS name?**, - TYPEDEFS deftype?* -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax I = idctxt - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -rec { - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 -def $concat_idctxt(idctxt*) : idctxt - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 - def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 - def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -relation Idctxt_ok: `|-%:OK`(idctxt) - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec - rule _{I : I, `field**` : char**}: - `|-%:OK`(I) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) - -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} - -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tidx_(ids : name?*) : idx ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{x : idx} x:Tu32 => x @@ -10908,9 +11219,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{"("} {"import"} {Tname} {Tname} {")"}} => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $dots : () - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Texporttagdots_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{Texportdots*{}} {Ttagtype_(I)}} => (`<implicit-prod-result>`, ()).1 @@ -10971,182 +11279,6 @@ grammar Telemtable_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -syntax decl = - | TYPE(rectype : rectype) - | IMPORT(name : name, name : name, externtype : externtype) - | TAG(tagtype : tagtype) - | GLOBAL(globaltype : globaltype, expr : expr) - | MEMORY(memtype : memtype) - | TABLE(tabletype : tabletype, expr : expr) - | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | DATA(`byte*` : byte*, datamode : datamode) - | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) - | START(funcidx : funcidx) - | EXPORT(name : name, externidx : externidx) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 -def $typesd(decl*) : type* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 - def $typesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 - def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 - def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 -def $importsd(decl*) : import* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 - def $importsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 - def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 - def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 -def $tagsd(decl*) : tag* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 - def $tagsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 - def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 - def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 -def $globalsd(decl*) : global* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 - def $globalsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 - def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 - def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 -def $memsd(decl*) : mem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 - def $memsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 - def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 - def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 -def $tablesd(decl*) : table* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 - def $tablesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 - def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 - def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 -def $funcsd(decl*) : func* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 - def $funcsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 - def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 - def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 -def $datasd(decl*) : data* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 - def $datasd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 - def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 - def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 -def $elemsd(decl*) : elem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 - def $elemsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 - def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 - def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 -def $startsd(decl*) : start* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 - def $startsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 - def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 - def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 -def $exportsd(decl*) : export* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 - def $exportsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 - def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 - def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $ordered(decl*) : bool - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true - -- if ($importsd(decl*{decl <- `decl*`}) = []) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Tdecl_(I : I) : (decl, idctxt) ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (type, idctxt)} `<implicit-prod-result>`:Ttype_(I) => (`<implicit-prod-result>` : (type, idctxt) <: (decl, idctxt)) @@ -11195,129 +11327,6 @@ ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (decl, idctxt)} [`<implicit-prod-result>`]:Tdecl_(I)*{} => [`<implicit-prod-result>`] -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax A = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax B = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax sym = - | _FIRST(A_1 : A) - | _DOTS - | _LAST(A_n : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax symsplit = - | _FIRST(A_1 : A) - | _LAST(A_2 : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax recorddots = () - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax record = -{ - FIELD_1 A, - FIELD_2 A, - `...` recorddots -} - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax pth = - | PTHSYNTAX - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -syntax T = nat - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremise: `%`(nat) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremisedots: `...` - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingScheme: `%`(nat) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec - rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: - `%`(conclusion) - -- NotationTypingPremise: `%`(premise_1) - -- NotationTypingPremise: `%`(premise_2) - -- NotationTypingPremisedots: `...` - -- NotationTypingPremise: `%`(premise_n) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -rec { - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 -relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 - rule `i32.add`{C : context}: - `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 - rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: - `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) - -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 - rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -} - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -relation NotationReduct: `~>%`(instr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 4{q_6 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_6)]) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $instrdots : instr* - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax label = - | `LABEL_%{%}`(n : n, `instr*` : instr*) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax callframe = - | `FRAME_%{%}`(n : n, frame : frame) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -rec { - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 -def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 - def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 - def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) - -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) - -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) -} - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -syntax symdots = - | `%`(i : nat) - -- if (i = 0) - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -def $var(syntax X) : nat - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec - def $var{syntax X}(syntax X) = 0 - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec grammar Bvar(syntax X) : () ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec @@ -11357,15 +11366,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:Tvar(syntax B) => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax abbreviated = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax expanded = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax syntax = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec grammar Tabbrev : () == IL Validation...
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index cddc014..3f4e66e 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md
@@ -7316,6 +7316,384 @@ -- Expand: `%~~%`(s.FUNCS_store[funcaddr].TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (Val_ok: `%|-%:%`(s, val, t_1))*{t_1 <- `t_1*`, val <- `val*`} +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax castop = (null?, null?) + +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax memidxop = (memidx, memarg) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax startopt = start* + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax code = (local*, expr) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax nopt = u32* + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +def $ieee_(N : N, rat : rat) : fNmag(N) + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax idctxt = +{ + TYPES name?*, + TAGS name?*, + GLOBALS name?*, + MEMS name?*, + TABLES name?*, + FUNCS name?*, + DATAS name?*, + ELEMS name?*, + LOCALS name?*, + LABELS name?*, + FIELDS name?**, + TYPEDEFS deftype?* +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax I = idctxt + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +rec { + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 +def $concat_idctxt(idctxt*) : idctxt + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 + def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 + def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +relation Idctxt_ok: `|-%:OK`(idctxt) + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec + rule _{I : I, `field**` : char**}: + `|-%:OK`(I) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) + -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} + -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $dots : () + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +syntax decl = + | TYPE(rectype : rectype) + | IMPORT(name : name, name : name, externtype : externtype) + | TAG(tagtype : tagtype) + | GLOBAL(globaltype : globaltype, expr : expr) + | MEMORY(memtype : memtype) + | TABLE(tabletype : tabletype, expr : expr) + | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) + | DATA(`byte*` : byte*, datamode : datamode) + | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) + | START(funcidx : funcidx) + | EXPORT(name : name, externidx : externidx) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 +def $typesd(decl*) : type* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 + def $typesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 + def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 + def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 +def $importsd(decl*) : import* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 + def $importsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 + def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 + def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 +def $tagsd(decl*) : tag* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 + def $tagsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 + def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 + def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 +def $globalsd(decl*) : global* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 + def $globalsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 + def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 + def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 +def $memsd(decl*) : mem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 + def $memsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 + def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 + def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 +def $tablesd(decl*) : table* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 + def $tablesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 + def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 + def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 +def $funcsd(decl*) : func* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 + def $funcsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 + def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 + def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 +def $datasd(decl*) : data* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 + def $datasd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 + def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 + def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 +def $elemsd(decl*) : elem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 + def $elemsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 + def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 + def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 +def $startsd(decl*) : start* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 + def $startsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 + def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 + def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 +def $exportsd(decl*) : export* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 + def $exportsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 + def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 + def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $ordered(decl*) : bool + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true + -- if ($importsd(decl*{decl <- `decl*`}) = []) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax A = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax B = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax sym = + | _FIRST(A_1 : A) + | _DOTS + | _LAST(A_n : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax symsplit = + | _FIRST(A_1 : A) + | _LAST(A_2 : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax recorddots = () + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax record = +{ + FIELD_1 A, + FIELD_2 A, + `...` recorddots +} + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax pth = + | PTHSYNTAX + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +syntax T = nat + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremise: `%`(nat) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremisedots: `...` + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingScheme: `%`(nat) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec + rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: + `%`(conclusion) + -- NotationTypingPremise: `%`(premise_1) + -- NotationTypingPremise: `%`(premise_2) + -- NotationTypingPremisedots: `...` + -- NotationTypingPremise: `%`(premise_n) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +rec { + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 +relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 + rule `i32.add`{C : context}: + `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 + rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: + `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) + -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 + rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: + `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) +} + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +relation NotationReduct: `~>%`(instr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 4{q_6 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_6)]) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $instrdots : instr* + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax label = + | `LABEL_%{%}`(n : n, `instr*` : instr*) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax callframe = + | `FRAME_%{%}`(n : n, frame : frame) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +rec { + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 +def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 + def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 + def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) + -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) + -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) +} + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +syntax symdots = + | `%`(i : nat) + -- if (i = 0) + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +def $var(syntax X) : nat + ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec + def $var{syntax X}(syntax X) = 0 + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax abbreviated = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax expanded = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax syntax = () + ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec grammar Bbyte : byte ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec @@ -7639,9 +8017,6 @@ prod{jt : tagtype} {{0x04} {jt:Btagtype}} => TAG_externtype(jt) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax castop = (null?, null?) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bcastop : castop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod 0x00 => (?(), ?()) @@ -7674,9 +8049,6 @@ prod{l : labelidx} {{0x03} {l:Blabelidx}} => CATCH_ALL_REF_catch(l) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax memidxop = (memidx, memarg) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bmemarg : memidxop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod{n : n, m : m} {{`%`_u32(n):Bu32} {`%`_u64(m):Bu64}} => (`%`_memidx(0), {ALIGN `%`_u32(n), OFFSET `%`_u64(m)}) @@ -8790,9 +9162,6 @@ prod{x : idx} x:Bfuncidx => [START_start(x)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax startopt = start* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bstartsec : start? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt) @@ -8827,9 +9196,6 @@ prod{`elem*` : elem*} elem*{elem <- `elem*`}:Bsection_(9, syntax elem, grammar Blist(syntax elem, grammar Belem)) => elem*{elem <- `elem*`} ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax code = (local*, expr) - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Blocals : local* ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{t : valtype, n : n} {{`%`_u32(n):Bu32} {t:Bvaltype}} => LOCAL_local(t)^n{} @@ -8871,9 +9237,6 @@ prod{n : n} `%`_u32(n):Bu32 => [`%`_u32(n)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax nopt = u32* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bdatacntsec : u32? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{nopt : nopt} nopt:Bsection_(12, syntax u32, grammar Bdatacnt) => $opt_(syntax u32, nopt) @@ -9292,9 +9655,6 @@ prod{p : nat, q : rat} {{p:Thexnum} {"."} {q:Thexfrac}} => ((p + (q : rat <:> nat)) : nat <:> rat) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -def $ieee_(N : N, rat : rat) : fNmag(N) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tfloat : rat ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{p : rat, s : int, ee : nat} {{p:Tmant} ({"E"} | {"e"}) {s:Tsign} {ee:Tnum}} => (p * ((10 ^ ((s * (ee : nat <:> int)) : int <:> nat)) : nat <:> rat)) @@ -9379,55 +9739,6 @@ -- if (|el*{el <- `el*`}| < (2 ^ 32)) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax idctxt = -{ - TYPES name?*, - TAGS name?*, - GLOBALS name?*, - MEMS name?*, - TABLES name?*, - FUNCS name?*, - DATAS name?*, - ELEMS name?*, - LOCALS name?*, - LABELS name?*, - FIELDS name?**, - TYPEDEFS deftype?* -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax I = idctxt - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -rec { - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 -def $concat_idctxt(idctxt*) : idctxt - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 - def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 - def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -relation Idctxt_ok: `|-%:OK`(idctxt) - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec - rule _{I : I, `field**` : char**}: - `|-%:OK`(I) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) - -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} - -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tidx_(ids : name?*) : idx ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{x : idx} x:Tu32 => x @@ -10898,9 +11209,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{"("} {"import"} {Tname} {Tname} {")"}} => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $dots : () - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Texporttagdots_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{Texportdots*{}} {Ttagtype_(I)}} => (`<implicit-prod-result>`, ()).1 @@ -10961,182 +11269,6 @@ grammar Telemtable_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -syntax decl = - | TYPE(rectype : rectype) - | IMPORT(name : name, name : name, externtype : externtype) - | TAG(tagtype : tagtype) - | GLOBAL(globaltype : globaltype, expr : expr) - | MEMORY(memtype : memtype) - | TABLE(tabletype : tabletype, expr : expr) - | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | DATA(`byte*` : byte*, datamode : datamode) - | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) - | START(funcidx : funcidx) - | EXPORT(name : name, externidx : externidx) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 -def $typesd(decl*) : type* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 - def $typesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 - def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 - def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 -def $importsd(decl*) : import* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 - def $importsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 - def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 - def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 -def $tagsd(decl*) : tag* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 - def $tagsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 - def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 - def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 -def $globalsd(decl*) : global* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 - def $globalsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 - def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 - def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 -def $memsd(decl*) : mem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 - def $memsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 - def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 - def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 -def $tablesd(decl*) : table* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 - def $tablesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 - def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 - def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 -def $funcsd(decl*) : func* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 - def $funcsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 - def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 - def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 -def $datasd(decl*) : data* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 - def $datasd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 - def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 - def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 -def $elemsd(decl*) : elem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 - def $elemsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 - def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 - def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 -def $startsd(decl*) : start* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 - def $startsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 - def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 - def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 -def $exportsd(decl*) : export* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 - def $exportsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 - def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 - def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $ordered(decl*) : bool - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true - -- if ($importsd(decl*{decl <- `decl*`}) = []) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Tdecl_(I : I) : (decl, idctxt) ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (type, idctxt)} `<implicit-prod-result>`:Ttype_(I) => (`<implicit-prod-result>` : (type, idctxt) <: (decl, idctxt)) @@ -11185,129 +11317,6 @@ ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (decl, idctxt)} [`<implicit-prod-result>`]:Tdecl_(I)*{} => [`<implicit-prod-result>`] -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax A = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax B = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax sym = - | _FIRST(A_1 : A) - | _DOTS - | _LAST(A_n : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax symsplit = - | _FIRST(A_1 : A) - | _LAST(A_2 : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax recorddots = () - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax record = -{ - FIELD_1 A, - FIELD_2 A, - `...` recorddots -} - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax pth = - | PTHSYNTAX - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -syntax T = nat - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremise: `%`(nat) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremisedots: `...` - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingScheme: `%`(nat) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec - rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: - `%`(conclusion) - -- NotationTypingPremise: `%`(premise_1) - -- NotationTypingPremise: `%`(premise_2) - -- NotationTypingPremisedots: `...` - -- NotationTypingPremise: `%`(premise_n) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -rec { - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 -relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 - rule `i32.add`{C : context}: - `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 - rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: - `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) - -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 - rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -} - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -relation NotationReduct: `~>%`(instr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 4{q_6 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_6)]) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $instrdots : instr* - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax label = - | `LABEL_%{%}`(n : n, `instr*` : instr*) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax callframe = - | `FRAME_%{%}`(n : n, frame : frame) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -rec { - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 -def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 - def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 - def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) - -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) - -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) -} - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -syntax symdots = - | `%`(i : nat) - -- if (i = 0) - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -def $var(syntax X) : nat - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec - def $var{syntax X}(syntax X) = 0 - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec grammar Bvar(syntax X) : () ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec @@ -11347,15 +11356,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:Tvar(syntax B) => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax abbreviated = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax expanded = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax syntax = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec grammar Tabbrev : () == IL Validation... @@ -18681,6 +18681,384 @@ -- Expand: `%~~%`(s.FUNCS_store[funcaddr].TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (Val_ok: `%|-%:%`(s, val, t_1))*{t_1 <- `t_1*`, val <- `val*`} +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax castop = (null?, null?) + +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax memidxop = (memidx, memarg) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax startopt = start* + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax code = (local*, expr) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax nopt = u32* + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +def $ieee_(N : N, rat : rat) : fNmag(N) + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax idctxt = +{ + TYPES name?*, + TAGS name?*, + GLOBALS name?*, + MEMS name?*, + TABLES name?*, + FUNCS name?*, + DATAS name?*, + ELEMS name?*, + LOCALS name?*, + LABELS name?*, + FIELDS name?**, + TYPEDEFS deftype?* +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax I = idctxt + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +rec { + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 +def $concat_idctxt(idctxt*) : idctxt + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 + def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 + def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +relation Idctxt_ok: `|-%:OK`(idctxt) + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec + rule _{I : I, `field**` : char**}: + `|-%:OK`(I) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) + -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} + -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $dots : () + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +syntax decl = + | TYPE(rectype : rectype) + | IMPORT(name : name, name : name, externtype : externtype) + | TAG(tagtype : tagtype) + | GLOBAL(globaltype : globaltype, expr : expr) + | MEMORY(memtype : memtype) + | TABLE(tabletype : tabletype, expr : expr) + | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) + | DATA(`byte*` : byte*, datamode : datamode) + | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) + | START(funcidx : funcidx) + | EXPORT(name : name, externidx : externidx) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 +def $typesd(decl*) : type* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 + def $typesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 + def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 + def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 +def $importsd(decl*) : import* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 + def $importsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 + def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 + def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 +def $tagsd(decl*) : tag* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 + def $tagsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 + def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 + def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 +def $globalsd(decl*) : global* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 + def $globalsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 + def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 + def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 +def $memsd(decl*) : mem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 + def $memsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 + def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 + def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 +def $tablesd(decl*) : table* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 + def $tablesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 + def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 + def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 +def $funcsd(decl*) : func* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 + def $funcsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 + def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 + def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 +def $datasd(decl*) : data* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 + def $datasd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 + def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 + def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 +def $elemsd(decl*) : elem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 + def $elemsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 + def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 + def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 +def $startsd(decl*) : start* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 + def $startsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 + def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 + def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 +def $exportsd(decl*) : export* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 + def $exportsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 + def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 + def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $ordered(decl*) : bool + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true + -- if ($importsd(decl*{decl <- `decl*`}) = []) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax A = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax B = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax sym = + | _FIRST(A_1 : A) + | _DOTS + | _LAST(A_n : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax symsplit = + | _FIRST(A_1 : A) + | _LAST(A_2 : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax recorddots = () + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax record = +{ + FIELD_1 A, + FIELD_2 A, + `...` recorddots +} + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax pth = + | PTHSYNTAX + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +syntax T = nat + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremise: `%`(nat) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremisedots: `...` + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingScheme: `%`(nat) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec + rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: + `%`(conclusion) + -- NotationTypingPremise: `%`(premise_1) + -- NotationTypingPremise: `%`(premise_2) + -- NotationTypingPremisedots: `...` + -- NotationTypingPremise: `%`(premise_n) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +rec { + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 +relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 + rule `i32.add`{C : context}: + `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 + rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: + `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) + -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 + rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: + `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) +} + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +relation NotationReduct: `~>%`(instr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 4{q_6 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_6)]) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $instrdots : instr* + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax label = + | `LABEL_%{%}`(n : n, `instr*` : instr*) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax callframe = + | `FRAME_%{%}`(n : n, frame : frame) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +rec { + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 +def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 + def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 + def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) + -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) + -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) +} + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +syntax symdots = + | `%`(i : nat) + -- if (i = 0) + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +def $var(syntax X) : nat + ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec + def $var{syntax X}(syntax X) = 0 + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax abbreviated = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax expanded = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax syntax = () + ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec grammar Bbyte : byte ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec @@ -19004,9 +19382,6 @@ prod{jt : tagtype} {{0x04} {jt:Btagtype}} => TAG_externtype(jt) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax castop = (null?, null?) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bcastop : castop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod 0x00 => (?(), ?()) @@ -19039,9 +19414,6 @@ prod{l : labelidx} {{0x03} {l:Blabelidx}} => CATCH_ALL_REF_catch(l) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax memidxop = (memidx, memarg) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bmemarg : memidxop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod{n : n, m : m} {{`%`_u32(n):Bu32} {`%`_u64(m):Bu64}} => (`%`_memidx(0), {ALIGN `%`_u32(n), OFFSET `%`_u64(m)}) @@ -20155,9 +20527,6 @@ prod{x : idx} x:Bfuncidx => [START_start(x)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax startopt = start* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bstartsec : start? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt) @@ -20192,9 +20561,6 @@ prod{`elem*` : elem*} elem*{elem <- `elem*`}:Bsection_(9, syntax elem, grammar Blist(syntax elem, grammar Belem)) => elem*{elem <- `elem*`} ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax code = (local*, expr) - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Blocals : local* ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{t : valtype, n : n} {{`%`_u32(n):Bu32} {t:Bvaltype}} => LOCAL_local(t)^n{} @@ -20236,9 +20602,6 @@ prod{n : n} `%`_u32(n):Bu32 => [`%`_u32(n)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax nopt = u32* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bdatacntsec : u32? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{nopt : nopt} nopt:Bsection_(12, syntax u32, grammar Bdatacnt) => $opt_(syntax u32, nopt) @@ -20657,9 +21020,6 @@ prod{p : nat, q : rat} {{p:Thexnum} {"."} {q:Thexfrac}} => ((p + (q : rat <:> nat)) : nat <:> rat) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -def $ieee_(N : N, rat : rat) : fNmag(N) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tfloat : rat ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{p : rat, s : int, ee : nat} {{p:Tmant} ({"E"} | {"e"}) {s:Tsign} {ee:Tnum}} => (p * ((10 ^ ((s * (ee : nat <:> int)) : int <:> nat)) : nat <:> rat)) @@ -20744,55 +21104,6 @@ -- if (|el*{el <- `el*`}| < (2 ^ 32)) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax idctxt = -{ - TYPES name?*, - TAGS name?*, - GLOBALS name?*, - MEMS name?*, - TABLES name?*, - FUNCS name?*, - DATAS name?*, - ELEMS name?*, - LOCALS name?*, - LABELS name?*, - FIELDS name?**, - TYPEDEFS deftype?* -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax I = idctxt - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -rec { - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 -def $concat_idctxt(idctxt*) : idctxt - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 - def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 - def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -relation Idctxt_ok: `|-%:OK`(idctxt) - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec - rule _{I : I, `field**` : char**}: - `|-%:OK`(I) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) - -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} - -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tidx_(ids : name?*) : idx ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{x : idx} x:Tu32 => x @@ -22263,9 +22574,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{"("} {"import"} {Tname} {Tname} {")"}} => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $dots : () - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Texporttagdots_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{Texportdots*{}} {Ttagtype_(I)}} => (`<implicit-prod-result>`, ()).1 @@ -22326,182 +22634,6 @@ grammar Telemtable_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -syntax decl = - | TYPE(rectype : rectype) - | IMPORT(name : name, name : name, externtype : externtype) - | TAG(tagtype : tagtype) - | GLOBAL(globaltype : globaltype, expr : expr) - | MEMORY(memtype : memtype) - | TABLE(tabletype : tabletype, expr : expr) - | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | DATA(`byte*` : byte*, datamode : datamode) - | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) - | START(funcidx : funcidx) - | EXPORT(name : name, externidx : externidx) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 -def $typesd(decl*) : type* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 - def $typesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 - def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 - def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 -def $importsd(decl*) : import* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 - def $importsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 - def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 - def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 -def $tagsd(decl*) : tag* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 - def $tagsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 - def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 - def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 -def $globalsd(decl*) : global* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 - def $globalsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 - def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 - def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 -def $memsd(decl*) : mem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 - def $memsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 - def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 - def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 -def $tablesd(decl*) : table* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 - def $tablesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 - def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 - def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 -def $funcsd(decl*) : func* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 - def $funcsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 - def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 - def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 -def $datasd(decl*) : data* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 - def $datasd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 - def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 - def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 -def $elemsd(decl*) : elem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 - def $elemsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 - def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 - def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 -def $startsd(decl*) : start* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 - def $startsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 - def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 - def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 -def $exportsd(decl*) : export* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 - def $exportsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 - def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 - def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $ordered(decl*) : bool - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true - -- if ($importsd(decl*{decl <- `decl*`}) = []) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Tdecl_(I : I) : (decl, idctxt) ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (type, idctxt)} `<implicit-prod-result>`:Ttype_(I) => (`<implicit-prod-result>` : (type, idctxt) <: (decl, idctxt)) @@ -22550,129 +22682,6 @@ ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (decl, idctxt)} [`<implicit-prod-result>`]:Tdecl_(I)*{} => [`<implicit-prod-result>`] -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax A = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax B = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax sym = - | _FIRST(A_1 : A) - | _DOTS - | _LAST(A_n : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax symsplit = - | _FIRST(A_1 : A) - | _LAST(A_2 : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax recorddots = () - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax record = -{ - FIELD_1 A, - FIELD_2 A, - `...` recorddots -} - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax pth = - | PTHSYNTAX - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -syntax T = nat - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremise: `%`(nat) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremisedots: `...` - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingScheme: `%`(nat) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec - rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: - `%`(conclusion) - -- NotationTypingPremise: `%`(premise_1) - -- NotationTypingPremise: `%`(premise_2) - -- NotationTypingPremisedots: `...` - -- NotationTypingPremise: `%`(premise_n) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -rec { - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 -relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 - rule `i32.add`{C : context}: - `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 - rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: - `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) - -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 - rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -} - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -relation NotationReduct: `~>%`(instr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 4{q_6 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_6)]) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $instrdots : instr* - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax label = - | `LABEL_%{%}`(n : n, `instr*` : instr*) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax callframe = - | `FRAME_%{%}`(n : n, frame : frame) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -rec { - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 -def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 - def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 - def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) - -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) - -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) -} - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -syntax symdots = - | `%`(i : nat) - -- if (i = 0) - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -def $var(syntax X) : nat - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec - def $var{syntax X}(syntax X) = 0 - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec grammar Bvar(syntax X) : () ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec @@ -22712,15 +22721,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:Tvar(syntax B) => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax abbreviated = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax expanded = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax syntax = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec grammar Tabbrev : () == IL Validation after pass totalize... @@ -30225,6 +30225,385 @@ -- Expand: `%~~%`(s.FUNCS_store[funcaddr].TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (Val_ok: `%|-%:%`(s, val, t_1))*{t_1 <- `t_1*`, val <- `val*`} +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax castop = (null?, null?) + +;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec +syntax memidxop = (memidx, memarg) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax startopt = start* + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax code = (local*, expr) + +;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec +syntax nopt = u32* + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +def $ieee_(N : N, rat : rat) : fNmag(N) + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax idctxt = +{ + TYPES name?*, + TAGS name?*, + GLOBALS name?*, + MEMS name?*, + TABLES name?*, + FUNCS name?*, + DATAS name?*, + ELEMS name?*, + LOCALS name?*, + LABELS name?*, + FIELDS name?**, + TYPEDEFS deftype?* +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +syntax I = idctxt + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +rec { + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 +def $concat_idctxt(idctxt*) : idctxt + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 + def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 + def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) +} + +;; ../../../../specification/wasm-latest/6.1-text.values.spectec +relation Idctxt_ok: `|-%:OK`(idctxt) + ;; ../../../../specification/wasm-latest/6.1-text.values.spectec + rule _{I : I, `field**` : char**}: + `|-%:OK`(I) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) + -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) + -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} + -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $dots : () + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +syntax decl = + | TYPE(rectype : rectype) + | IMPORT(name : name, name : name, externtype : externtype) + | TAG(tagtype : tagtype) + | GLOBAL(globaltype : globaltype, expr : expr) + | MEMORY(memtype : memtype) + | TABLE(tabletype : tabletype, expr : expr) + | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) + | DATA(`byte*` : byte*, datamode : datamode) + | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) + | START(funcidx : funcidx) + | EXPORT(name : name, externidx : externidx) + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 +def $typesd(decl*) : type* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 + def $typesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 + def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 + def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 +def $importsd(decl*) : import* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 + def $importsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 + def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 + def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 +def $tagsd(decl*) : tag* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 + def $tagsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 + def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 + def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 +def $globalsd(decl*) : global* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 + def $globalsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 + def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 + def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 +def $memsd(decl*) : mem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 + def $memsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 + def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 + def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 +def $tablesd(decl*) : table* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 + def $tablesd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 + def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 + def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 +def $funcsd(decl*) : func* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 + def $funcsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 + def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 + def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 +def $datasd(decl*) : data* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 + def $datasd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 + def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 + def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 +def $elemsd(decl*) : elem* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 + def $elemsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 + def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 + def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 +def $startsd(decl*) : start* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 + def $startsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 + def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 + def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 +def $exportsd(decl*) : export* + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 + def $exportsd([]) = [] + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 + def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 + def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) + -- otherwise +} + +;; ../../../../specification/wasm-latest/6.4-text.modules.spectec +def $ordered(decl*) : bool + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true + -- if ($importsd(decl*{decl <- `decl*`}) = []) + ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec + def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax A = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax B = nat + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax sym = + | _FIRST(A_1 : A) + | _DOTS + | _LAST(A_n : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax symsplit = + | _FIRST(A_1 : A) + | _LAST(A_2 : A) + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax recorddots = () + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax record = +{ + FIELD_1 A, + FIELD_2 A, + `...` recorddots +} + +;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec +syntax pth = + | PTHSYNTAX + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +syntax T = nat + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremise: `%`(nat) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingPremisedots: `...` + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +relation NotationTypingScheme: `%`(nat) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec + rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: + `%`(conclusion) + -- NotationTypingPremise: `%`(premise_1) + -- NotationTypingPremise: `%`(premise_2) + -- NotationTypingPremisedots: `...` + -- NotationTypingPremise: `%`(premise_n) + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec +rec { + +;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 +relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 + rule `i32.add`{C : context}: + `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 + rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: + `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) + -- if (x!`%`_idx.0 < |C.GLOBALS_context|) + -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) + + ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 + rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: + `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) +} + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +relation NotationReduct: `~>%`(instr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) + + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec + rule 4{q_6 : num_(F64_numtype)}: + `~>%`([CONST_instr(F64_numtype, q_6)]) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $instrdots : instr* + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax label = + | `LABEL_%{%}`(n : n, `instr*` : instr*) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +syntax callframe = + | `FRAME_%{%}`(n : n, frame : frame) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec +rec { + +;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 +def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 + def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) + ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 + def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) + -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) + -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) +} + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +syntax symdots = + | `%`(i : nat) + -- if (i = 0) + +;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec +def $var(syntax X) : nat + ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec + def $var{syntax X}(syntax X) = 0 + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax abbreviated = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax expanded = () + +;; ../../../../specification/wasm-latest/X.5-notation.text.spectec +syntax syntax = () + ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec grammar Bbyte : byte ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec @@ -30548,9 +30927,6 @@ prod{jt : tagtype} {{0x04} {jt:Btagtype}} => TAG_externtype(jt) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax castop = (null?, null?) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bcastop : castop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod 0x00 => (?(), ?()) @@ -30583,9 +30959,6 @@ prod{l : labelidx} {{0x03} {l:Blabelidx}} => CATCH_ALL_REF_catch(l) ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec -syntax memidxop = (memidx, memarg) - -;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec grammar Bmemarg : memidxop ;; ../../../../specification/wasm-latest/5.3-binary.instructions.spectec prod{n : n, m : m} {{`%`_u32(n):Bu32} {`%`_u64(m):Bu64}} => (`%`_memidx(0), {ALIGN `%`_u32(n), OFFSET `%`_u64(m)}) @@ -31699,9 +32072,6 @@ prod{x : idx} x:Bfuncidx => [START_start(x)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax startopt = start* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bstartsec : start? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt) @@ -31736,9 +32106,6 @@ prod{`elem*` : elem*} elem*{elem <- `elem*`}:Bsection_(9, syntax elem, grammar Blist(syntax elem, grammar Belem)) => elem*{elem <- `elem*`} ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax code = (local*, expr) - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Blocals : local* ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{t : valtype, n : n} {{`%`_u32(n):Bu32} {t:Bvaltype}} => LOCAL_local(t)^n{} @@ -31780,9 +32147,6 @@ prod{n : n} `%`_u32(n):Bu32 => [`%`_u32(n)] ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec -syntax nopt = u32* - -;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec grammar Bdatacntsec : u32? ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec prod{nopt : nopt} nopt:Bsection_(12, syntax u32, grammar Bdatacnt) => $opt_(syntax u32, nopt) @@ -32201,9 +32565,6 @@ prod{p : nat, q : rat} {{p:Thexnum} {"."} {q:Thexfrac}} => ((p + (q : rat <:> nat)) : nat <:> rat) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -def $ieee_(N : N, rat : rat) : fNmag(N) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tfloat : rat ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{p : rat, s : int, ee : nat} {{p:Tmant} ({"E"} | {"e"}) {s:Tsign} {ee:Tnum}} => (p * ((10 ^ ((s * (ee : nat <:> int)) : int <:> nat)) : nat <:> rat)) @@ -32288,55 +32649,6 @@ -- if (|el*{el <- `el*`}| < (2 ^ 32)) ;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax idctxt = -{ - TYPES name?*, - TAGS name?*, - GLOBALS name?*, - MEMS name?*, - TABLES name?*, - FUNCS name?*, - DATAS name?*, - ELEMS name?*, - LOCALS name?*, - LABELS name?*, - FIELDS name?**, - TYPEDEFS deftype?* -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -syntax I = idctxt - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -rec { - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec:154.1-154.56 -def $concat_idctxt(idctxt*) : idctxt - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:155.1-155.29 - def $concat_idctxt([]) = {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []} - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec:156.1-156.53 - def $concat_idctxt{I : I, `I'*` : I*}([I] ++ I'*{I' <- `I'*`}) = I +++ $concat_idctxt(I'*{I' <- `I'*`}) -} - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec -relation Idctxt_ok: `|-%:OK`(idctxt) - ;; ../../../../specification/wasm-latest/6.1-text.values.spectec - rule _{I : I, `field**` : char**}: - `|-%:OK`(I) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TYPES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TAGS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.GLOBALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.MEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.TABLES_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.FUNCS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.DATAS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.ELEMS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LOCALS_I)) - -- if $disjoint_(syntax name, $concatopt_(syntax name, I.LABELS_I)) - -- (if $disjoint_(syntax name, $concatopt_(syntax name, [?(`%`_name(field*{field <- `field*`}))])))*{`field*` <- `field**`} - -- if ([?(`%`_name(field*{field <- `field*`}))*{`field*` <- `field**`}] = I.FIELDS_I) - -;; ../../../../specification/wasm-latest/6.1-text.values.spectec grammar Tidx_(ids : name?*) : idx ;; ../../../../specification/wasm-latest/6.1-text.values.spectec prod{x : idx} x:Tu32 => x @@ -33807,9 +34119,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{"("} {"import"} {Tname} {Tname} {")"}} => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $dots : () - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Texporttagdots_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:{{Texportdots*{}} {Ttagtype_(I)}} => (`<implicit-prod-result>`, ()).1 @@ -33870,182 +34179,6 @@ grammar Telemtable_(I : I) : () ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -syntax decl = - | TYPE(rectype : rectype) - | IMPORT(name : name, name : name, externtype : externtype) - | TAG(tagtype : tagtype) - | GLOBAL(globaltype : globaltype, expr : expr) - | MEMORY(memtype : memtype) - | TABLE(tabletype : tabletype, expr : expr) - | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | DATA(`byte*` : byte*, datamode : datamode) - | ELEM(reftype : reftype, `expr*` : expr*, elemmode : elemmode) - | START(funcidx : funcidx) - | EXPORT(name : name, externidx : externidx) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:258.1-258.76 -def $typesd(decl*) : type* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:270.1-270.23 - def $typesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:271.1-271.48 - def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:272.1-272.57 - def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:259.1-259.78 -def $importsd(decl*) : import* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:274.1-274.25 - def $importsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:275.1-275.56 - def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:276.1-276.61 - def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:260.1-260.75 -def $tagsd(decl*) : tag* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:278.1-278.22 - def $tagsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:279.1-279.44 - def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:280.1-280.55 - def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:261.1-261.78 -def $globalsd(decl*) : global* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:282.1-282.25 - def $globalsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:283.1-283.56 - def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:284.1-284.61 - def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:262.1-262.75 -def $memsd(decl*) : mem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:286.1-286.22 - def $memsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:287.1-287.44 - def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:288.1-288.55 - def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:263.1-263.77 -def $tablesd(decl*) : table* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:290.1-290.24 - def $tablesd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:291.1-291.52 - def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:292.1-292.59 - def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:264.1-264.76 -def $funcsd(decl*) : func* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:294.1-294.23 - def $funcsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:295.1-295.48 - def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:296.1-296.57 - def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:265.1-265.76 -def $datasd(decl*) : data* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:298.1-298.23 - def $datasd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:299.1-299.48 - def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:300.1-300.57 - def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:266.1-266.76 -def $elemsd(decl*) : elem* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:302.1-302.23 - def $elemsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:303.1-303.48 - def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:304.1-304.57 - def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:267.1-267.77 -def $startsd(decl*) : start* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24 - def $startsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52 - def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59 - def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -rec { - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.78 -def $exportsd(decl*) : export* - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:310.1-310.25 - def $exportsd([]) = [] - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:311.1-311.56 - def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`}) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:312.1-312.61 - def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`}) - -- otherwise -} - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec -def $ordered(decl*) : bool - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl*` : decl*}(decl*{decl <- `decl*`}) = true - -- if ($importsd(decl*{decl <- `decl*`}) = []) - ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec - def $ordered{`decl_1*` : decl*, import : import, `decl_2*` : decl*}(decl_1*{decl_1 <- `decl_1*`} ++ [(import : import <: decl)] ++ decl_2*{decl_2 <- `decl_2*`}) = (((((($importsd(decl_1*{decl_1 <- `decl_1*`}) = []) /\ ($tagsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($globalsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($memsd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($tablesd(decl_1*{decl_1 <- `decl_1*`}) = [])) /\ ($funcsd(decl_1*{decl_1 <- `decl_1*`}) = [])) - -;; ../../../../specification/wasm-latest/6.4-text.modules.spectec grammar Tdecl_(I : I) : (decl, idctxt) ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (type, idctxt)} `<implicit-prod-result>`:Ttype_(I) => (`<implicit-prod-result>` : (type, idctxt) <: (decl, idctxt)) @@ -34094,130 +34227,6 @@ ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec prod{`<implicit-prod-result>` : (decl, idctxt)} [`<implicit-prod-result>`]:Tdecl_(I)*{} => [`<implicit-prod-result>`] -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax A = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax B = nat - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax sym = - | _FIRST(A_1 : A) - | _DOTS - | _LAST(A_n : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax symsplit = - | _FIRST(A_1 : A) - | _LAST(A_2 : A) - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax recorddots = () - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax record = -{ - FIELD_1 A, - FIELD_2 A, - `...` recorddots -} - -;; ../../../../specification/wasm-latest/X.1-notation.syntax.spectec -syntax pth = - | PTHSYNTAX - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -syntax T = nat - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremise: `%`(nat) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingPremisedots: `...` - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -relation NotationTypingScheme: `%`(nat) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec - rule _{conclusion : nat, premise_1 : nat, premise_2 : nat, premise_n : nat}: - `%`(conclusion) - -- NotationTypingPremise: `%`(premise_1) - -- NotationTypingPremise: `%`(premise_2) - -- NotationTypingPremisedots: `...` - -- NotationTypingPremise: `%`(premise_n) - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec -rec { - -;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:20.1-20.83 -relation NotationTypingInstrScheme: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:22.1-23.38 - rule `i32.add`{C : context}: - `%|-%:%`(C, [BINOP_instr(I32_numtype, ADD_binop_)], `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([I32_valtype]))) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:25.1-27.29 - rule `global.get`{C : context, x : idx, t : valtype, mut : mut}: - `%|-%:%`(C, [`GLOBAL.GET`_instr(x)], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) - -- if (x!`%`_idx.0 < |C.GLOBALS_context|) - -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(mut), t)) - - ;; ../../../../specification/wasm-latest/X.2-notation.typing.spectec:29.1-32.78 - rule block{C : context, blocktype : blocktype, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:%`(C, [BLOCK_instr(blocktype, instr*{instr <- `instr*`})], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- Blocktype_ok: `%|-%:%`(C, blocktype, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- NotationTypingInstrScheme: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -} - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -relation NotationReduct: `~>%`(instr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 2{q_1 : num_(F64_numtype), q_4 : num_(F64_numtype), q_3 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_4) CONST_instr(F64_numtype, q_3) BINOP_instr(F64_numtype, ADD_binop_) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 3{q_1 : num_(F64_numtype), q_5 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_1) CONST_instr(F64_numtype, q_5) BINOP_instr(F64_numtype, MUL_binop_)]) - - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec - rule 4{q_6 : num_(F64_numtype)}: - `~>%`([CONST_instr(F64_numtype, q_6)]) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $instrdots : instr* - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax label = - | `LABEL_%{%}`(n : n, `instr*` : instr*) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -syntax callframe = - | `FRAME_%{%}`(n : n, frame : frame) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -def $allocX(syntax X, syntax Y, store : store, X : X, Y : Y) : (store, addr) - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec -rec { - -;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:32.1-32.117 -def $allocXs(syntax X, syntax Y, store : store, X*, Y*) : (store, addr*) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:33.1-33.57 - def $allocXs{syntax X, syntax Y, s : store}(syntax X, syntax Y, s, [], []) = (s, []) - ;; ../../../../specification/wasm-latest/X.3-notation.execution.spectec:34.1-36.65 - def $allocXs{syntax X, syntax Y, s : store, X : X, `X'*` : X*, Y : Y, `Y'*` : Y*, s_2 : store, a : addr, `a'*` : addr*, s_1 : store}(syntax X, syntax Y, s, [X] ++ X'*{X' <- `X'*`}, [Y] ++ Y'*{Y' <- `Y'*`}) = (s_2, [a] ++ a'*{a' <- `a'*`}) - -- if ((s_1, a) = $allocX(syntax X, syntax Y, s, X, Y)) - -- if ((s_2, a'*{a' <- `a'*`}) = $allocXs(syntax X, syntax Y, s_1, X'*{X' <- `X'*`}, Y'*{Y' <- `Y'*`})) -} - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -syntax symdots = - | `%`(i : nat) - -- if (i = 0) - -;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec -def $var(syntax X) : nat - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec - def $var{syntax X}(syntax X) = 0 - ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec grammar Bvar(syntax X) : () ;; ../../../../specification/wasm-latest/X.4-notation.binary.spectec @@ -34257,15 +34266,6 @@ prod{`<implicit-prod-result>` : ()} `<implicit-prod-result>`:Tvar(syntax B) => (`<implicit-prod-result>`, ()).1 ;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax abbreviated = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax expanded = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec -syntax syntax = () - -;; ../../../../specification/wasm-latest/X.5-notation.text.spectec grammar Tabbrev : () == IL Validation after pass sideconditions...