diff --git a/spectec/.gitignore b/spectec/.gitignore index 96abbd1af7..a2f79715c8 100644 --- a/spectec/.gitignore +++ b/spectec/.gitignore @@ -1 +1,2 @@ watsup +*/_log diff --git a/spectec/spec/wasm-1.0/A-binary.watsup b/spectec/spec/wasm-1.0/A-binary.watsup index ebcf41ce9c..0dc190e792 100644 --- a/spectec/spec/wasm-1.0/A-binary.watsup +++ b/spectec/spec/wasm-1.0/A-binary.watsup @@ -5,7 +5,7 @@ ;; Vectors grammar Bvec(grammar BX : el) : el* = - | n:Bu32 (el:BX)^n => el^n + | n:Bu32 el*:BX^n => el* @@ -139,10 +139,10 @@ grammar Bblocktype : blocktype = grammar Binstr/control : instr = | 0x00 => UNREACHABLE | 0x01 => NOP - | 0x02 bt:Bblocktype (in:Binstr)* 0x0B => BLOCK bt in* - | 0x03 bt:Bblocktype (in:Binstr)* 0x0B => LOOP bt in* - | 0x04 bt:Bblocktype (in:Binstr)* 0x0B => IF bt in* ELSE eps - | 0x04 bt:Bblocktype (in_1:Binstr)* 0x05 (in_2:Binstr)* 0x0B => IF bt in_1* ELSE in_2* + | 0x02 bt:Bblocktype in*:Binstr* 0x0B => BLOCK bt in* + | 0x03 bt:Bblocktype in*:Binstr* 0x0B => LOOP bt in* + | 0x04 bt:Bblocktype in*:Binstr* 0x0B => IF bt in* ELSE eps + | 0x04 bt:Bblocktype in_1*:Binstr* 0x05 in_2*:Binstr* 0x0B => IF bt in_1* ELSE in_2* | 0x0C l:Blabelidx => BR l | 0x0D l:Blabelidx => BR_IF l | 0x0E l*:Bvec(Blabelidx) l_N:Blabelidx => BR_TABLE l* l_N @@ -386,7 +386,7 @@ grammar Binstr/numeric-cvt : instr = ... ;; Expressions grammar Bexpr : expr = - | (in:Binstr)* 0x0B => in* + | in*:Binstr* 0x0B => in* diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup index 4030a89523..7b81cc6304 100644 --- a/spectec/spec/wasm-2.0/A-binary.watsup +++ b/spectec/spec/wasm-2.0/A-binary.watsup @@ -5,7 +5,7 @@ ;; Vectors grammar Bvec(grammar BX : el) : el* = - | n:Bu32 (el:BX)^n => el^n + | n:Bu32 el*:BX^n => el* @@ -155,10 +155,10 @@ grammar Bblocktype : blocktype = grammar Binstr/control : instr = | 0x00 => UNREACHABLE | 0x01 => NOP - | 0x02 bt:Bblocktype (in:Binstr)* 0x0B => BLOCK bt in* - | 0x03 bt:Bblocktype (in:Binstr)* 0x0B => LOOP bt in* - | 0x04 bt:Bblocktype (in:Binstr)* 0x0B => IF bt in* ELSE eps - | 0x04 bt:Bblocktype (in_1:Binstr)* 0x05 (in_2:Binstr)* 0x0B => IF bt in_1* ELSE in_2* + | 0x02 bt:Bblocktype in*:Binstr* 0x0B => BLOCK bt in* + | 0x03 bt:Bblocktype in*:Binstr* 0x0B => LOOP bt in* + | 0x04 bt:Bblocktype in*:Binstr* 0x0B => IF bt in* ELSE eps + | 0x04 bt:Bblocktype in_1*:Binstr* 0x05 in_2*:Binstr* 0x0B => IF bt in_1* ELSE in_2* | 0x0C l:Blabelidx => BR l | 0x0D l:Blabelidx => BR_IF l | 0x0E l*:Bvec(Blabelidx) l_N:Blabelidx => BR_TABLE l* l_N @@ -478,11 +478,11 @@ grammar Binstr/vector-memory : instr = ... | ... grammar Binstr/vector-const : instr = ... - | 0xFD 12:Bu32 (b:Bbyte)^16 => VCONST V128 b' -- if $ibytes_(128, b') = b + | 0xFD 12:Bu32 b*:Bbyte^16 => VCONST V128 b' -- if $ibytes_(128, b') = b | ... grammar Binstr/vector-shuffle : instr = ... - | 0xFD 13:Bu32 (l:Blaneidx)^16 => VSHUFFLE (I8 X 16) l + | 0xFD 13:Bu32 l*:Blaneidx^16 => VSHUFFLE (I8 X 16) l* | ... grammar Binstr/vector-lanes : instr = ... @@ -751,7 +751,7 @@ grammar Binstr/vector-cvt : instr = ... ;; Expressions grammar Bexpr : expr = - | (in:Binstr)* 0x0B => in* + | in*:Binstr* 0x0B => in* diff --git a/spectec/spec/wasm-3.0/0-aux.watsup b/spectec/spec/wasm-3.0/0-aux.watsup index 2d1148258b..b72dad7716 100644 --- a/spectec/spec/wasm-3.0/0-aux.watsup +++ b/spectec/spec/wasm-3.0/0-aux.watsup @@ -50,6 +50,7 @@ def $concat_(syntax X, (X*)*) : X* hint(show (++) %2) def $concat_(syntax X, eps) = eps def $concat_(syntax X, (w*) (w'*)*) = w* ++ $concat_(X, (w'*)*) +;; TODO(3, rossberg): remove def $concatn_(syntax X, (X*)*, nat) : X* hint(show (++) %2) def $concatn_(syntax X, eps, n) = eps def $concatn_(syntax X, (w^n) (w'^n)*, n) = w^n $concatn_(X, (w'^n)*, n) diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup index 96ecca0308..bf84d012b6 100644 --- a/spectec/spec/wasm-3.0/A-binary.watsup +++ b/spectec/spec/wasm-3.0/A-binary.watsup @@ -5,7 +5,7 @@ ;; Lists grammar Blist(grammar BX : el) : el* = - | n:Bu32 (el:BX)^n => el^n + | n:Bu32 el*:BX^n => el* @@ -46,26 +46,47 @@ grammar Bf64 : f64 = p:BfN(64) => p var ch : char +;; def $utf8(char*) : byte* +def $utf8c(char) : byte* hint(show $utf8(%)) + def $cont(byte) : nat hint(macro none) def $cont(b) = $(b - 0x80) -- if (0x80 < b < 0xC0) -;; def $utf8(char*) : byte* -def $utf8(ch*) = $concat_(byte, $utf8(ch)*) -def $utf8(ch) = b +def $utf8(ch*) = $concat_(byte, $utf8c(ch)*) + +def $utf8c(ch) = b -- if ch < U+0080 -- if ch = b -def $utf8(ch) = b_1 b_2 +def $utf8c(ch) = b_1 b_2 -- if U+0080 <= ch < U+0800 -- if ch = $(2^6*(b_1 - 0xC0) + $cont(b_2)) -def $utf8(ch) = b_1 b_2 b_3 +def $utf8c(ch) = b_1 b_2 b_3 -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000 -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3)) -def $utf8(ch) = b_1 b_2 b_3 b_4 +def $utf8c(ch) = b_1 b_2 b_3 b_4 -- if U+10000 <= ch < U+11000 -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4)) + +def $code(nat, nat) : char +def $code(min, n) = n + -- if min <= n < 0x11000 /\ ~(0xD800 <= n < 0xE000) + +def $invutf8(byte*) : name hint(show $utf8^(-1)#((%))) + +def $invutf8(eps) = eps +def $invutf8(b_1 b*) = $code(0x0, b_1) $invutf8(b*) + -- if b_1 < 0x80 +def $invutf8(b_1 b_2 b*) = $code(0x80, $(2^6*(b_1 - 0xC0) + $cont(b_2))) $invutf8(b*) + -- if 0xC0 <= b_1 < 0xE0 +def $invutf8(b_1 b_2 b_3 b*) = $code(0x800, $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3))) $invutf8(b*) + -- if 0xE0 <= b_1 < 0xF0 +def $invutf8(b_1 b_2 b_3 b_4 b*) = $code(0x10000, $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4))) $invutf8(b*) + -- if 0xF0 <= b_1 < 0xF8 + + grammar Bname : name = - | b*:Blist(Bbyte) => name -- if $utf8(name) = b* + | b*:Blist(Bbyte) => $invutf8(b*) ;; Indices @@ -205,14 +226,14 @@ grammar Bblocktype : blocktype = grammar Binstr/control : instr = | 0x00 => UNREACHABLE | 0x01 => NOP - | 0x02 bt:Bblocktype (in:Binstr)* 0x0B => BLOCK bt in* - | 0x03 bt:Bblocktype (in:Binstr)* 0x0B => LOOP bt in* - | 0x04 bt:Bblocktype (in:Binstr)* 0x0B => IF bt in* ELSE eps - | 0x04 bt:Bblocktype (in_1:Binstr)* + | 0x02 bt:Bblocktype in*:Binstr* 0x0B => BLOCK bt in* + | 0x03 bt:Bblocktype in*:Binstr* 0x0B => LOOP bt in* + | 0x04 bt:Bblocktype in*:Binstr* 0x0B => IF bt in* ELSE eps + | 0x04 bt:Bblocktype in_1*:Binstr* ;; TODO(2, rossberg): do not require 2 empty lines - 0x05 (in_2:Binstr)* 0x0B => IF bt in_1* ELSE in_2* + 0x05 in_2*:Binstr* 0x0B => IF bt in_1* ELSE in_2* | 0x0C l:Blabelidx => BR l | 0x0D l:Blabelidx => BR_IF l | 0x0E l*:Blist(Blabelidx) l_n:Blabelidx => BR_TABLE l* l_n @@ -610,11 +631,11 @@ grammar Binstr/vec-memory : instr = ... | ... grammar Binstr/vec-const : instr = ... - | 0xFD 12:Bu32 (b:Bbyte)^16 => VCONST V128 $invibytes_(`128, (b)^16) + | 0xFD 12:Bu32 b*:Bbyte^16 => VCONST V128 $invibytes_(`128, (b)*) | ... grammar Binstr/vec-shuffle : instr = ... - | 0xFD 13:Bu32 (l:Blaneidx)^16 => VSHUFFLE (I8 X `16) l + | 0xFD 13:Bu32 l*:Blaneidx^16 => VSHUFFLE (I8 X `16) l* | 0xFD 14:Bu32 => VSWIZZLE (I8 X `16) | ... @@ -976,7 +997,7 @@ grammar Binstr/vec-cvt : instr = ... ;; Expressions grammar Bexpr : expr = - | (in:Binstr)* 0x0B => in* + | in*:Binstr* 0x0B => in* @@ -988,14 +1009,17 @@ grammar Bexpr : expr = var len : nat -grammar Bsection_(N, grammar BX : en*) : en* hint(desc "section") = - | N:Bbyte len:Bu32 en*:BX => en* -- if len = ||BX|| +grammar Bsection_(N, grammar BX : sec) : sec hint(desc "section") = + | N:Bbyte len:Bu32 sec:BX => sec -- if len = ||BX|| + +grammar Boptlist(grammar BX : en*) : en* hint(show %?) = | eps => eps + | en*:BX => en* ;; Custom sections -grammar Bcustom : ()* hint(desc "custom data") = +grammar Bcustom : () hint(desc "custom data") = | Bname Bbyte* => () grammar Bcustomsec : () hint(desc "custom section") = @@ -1065,13 +1089,11 @@ grammar Bexportsec : export* hint(desc "export section") = ;; Start section -grammar Bstart : start* = +grammar Bstart : start = | x:Bfuncidx => (START x) -syntax startopt hint(show start?) = start* ;; HACK - -grammar Bstartsec : start? hint(desc "start section") = - | startopt:Bsection_(8, Bstart) => $opt_(start, startopt) +grammar Bstartsec : start hint(desc "start section") = + | start:Bsection_(8, Bstart) => start ;; Element section @@ -1132,13 +1154,11 @@ grammar Bdatasec : data* hint(desc "data section") = ;; Data count section -grammar Bdatacnt : u32* hint(desc "data count") = +grammar Bdatacnt : u32 hint(desc "data count") = | n:Bu32 => n -syntax nopt hint(show n?) = u32* ;; HACK - -grammar Bdatacntsec : u32? hint(desc "data count section") = - | nopt:Bsection_(12, Bdatacnt) => $opt_(u32, nopt) +grammar Bdatacntsec : u32 hint(desc "data count section") = + | n:Bsection_(12, Bdatacnt) => n ;; Modules @@ -1152,56 +1172,61 @@ grammar Bmodule : module = Bcustomsec* - type*:Btypesec + type*:Boptlist(Btypesec) Bcustomsec* - import*:Bimportsec + import*:Boptlist(Bimportsec) Bcustomsec* - typeidx*:Bfuncsec + typeidx*:Boptlist(Bfuncsec) Bcustomsec* - table*:Btablesec + table*:Boptlist(Btablesec) Bcustomsec* - mem*:Bmemsec + mem*:Boptlist(Bmemsec) Bcustomsec* - global*:Bglobalsec + global*:Boptlist(Bglobalsec) Bcustomsec* - export*:Bexportsec + export*:Boptlist(Bexportsec) Bcustomsec* - start?:Bstartsec + start?:Bstartsec? Bcustomsec* - elem*:Belemsec + elem*:Boptlist(Belemsec) Bcustomsec* - n?:Bdatacntsec + n?:Bdatacntsec? Bcustomsec* - (local*, expr)*:Bcodesec + (local*, expr)*:Boptlist(Bcodesec) Bcustomsec* - data*:Bdatasec + data*:Boptlist(Bdatasec) Bcustomsec* => - MODULE type* import* func* global* table* mem* elem* data* start? export* +;; TODO(2, rossberg): enable binding for func +;; MODULE type* import* func* global* table* mem* elem* data* start? export* +;; ---- +;; -- (if n = |data*|)? +;; -- if n? =/= eps \/ $dataidx_funcs(func*) = eps +;; -- (if func = FUNC typeidx local* expr)* + MODULE type* import* (FUNC typeidx local* expr)* global* table* mem* elem* data* start? export* ---- -- (if n = |data*|)? - -- if n? =/= eps \/ $dataidx_funcs(func*) = eps - -- (if func = FUNC typeidx local* expr)* + -- if n? =/= eps \/ $dataidx_funcs((FUNC typeidx local* expr)*) = eps diff --git a/spectec/src/el/free.mli b/spectec/src/el/free.mli index 650d4fe1d6..f6431394bd 100644 --- a/spectec/src/el/free.mli +++ b/spectec/src/el/free.mli @@ -25,6 +25,7 @@ val free_typcase : typcase -> sets val free_typcon : typcon -> sets val free_exp : exp -> sets val free_path : path -> sets +val free_sym : sym -> sets val free_arg : arg -> sets val free_args : arg list -> sets val free_prem : prem -> sets diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml index 68fb2fc07c..80c7acd5b0 100644 --- a/spectec/src/exe-watsup/main.ml +++ b/spectec/src/exe-watsup/main.ml @@ -8,6 +8,7 @@ let version = "0.4" type target = | Check + | Parse of [`File | `String] * string | Latex | Prose of bool | Splice of Backend_splice.Config.t @@ -31,6 +32,7 @@ let all_passes = [ Totalize; Wild; Sideconditions ] type file_kind = | Spec + | Input | Patch | Output @@ -43,6 +45,7 @@ let warn_prose = ref false (* warn about unused or reused prose splices *) let file_kind = ref Spec let srcs = ref [] (* spec src file arguments *) +let inps = ref [] (* input src for parsing *) let pdsts = ref [] (* patch file arguments *) let odsts = ref [] (* output file arguments *) @@ -100,6 +103,7 @@ let add_arg source = let args = match !file_kind with | Spec -> srcs + | Input -> inps | Patch -> pdsts | Output -> odsts in args := !args @ [source] @@ -114,8 +118,6 @@ let argspec = Arg.align "-i", Arg.Set in_place, " Splice patch files in-place"; "-d", Arg.Set dry, " Dry run (when -p) "; "-o", Arg.Unit (fun () -> file_kind := Output), " Output files"; - "-l", Arg.Set logging, " Log execution steps"; - "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution"; "-w", Arg.Unit (fun () -> warn_math := true; warn_prose := true), " Warn about unused or multiply used splices"; "--warn-math", Arg.Set warn_math, @@ -124,6 +126,8 @@ let argspec = Arg.align " Warn about unused or multiply used prose splices"; "--check", Arg.Unit (fun () -> target := Check), " Check only (default)"; + "--parse", Arg.String (fun id -> target := Parse (`File, id); file_kind := Input), " Parse with grammar"; + "--parse-string", Arg.String (fun id -> target := Parse (`String, id); file_kind := Input), " Parse with grammar"; "--latex", Arg.Unit (fun () -> target := Latex), " Generate Latex"; "--splice-latex", Arg.Unit (fun () -> target := Splice Backend_splice.Config.latex), " Splice Sphinx"; @@ -136,6 +140,12 @@ let argspec = Arg.align "--latex-macros", Arg.Set latex_macros, " Splice Latex with macro invocations"; + "-l", Arg.Set logging, " Log execution steps"; + "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution"; + "--trace-parse", Arg.Set Il.Parse.trace, " Trace parsing execution"; + "--debug", Arg.String (fun s -> Util.Debug_log.active := s :: !Util.Debug_log.active), + " Turn on debugging log for named function"; + "--print-el", Arg.Set print_el, " Print EL"; "--print-il", Arg.Set print_elab_il, " Print IL (after elaboration)"; "--print-final-il", Arg.Set print_final_il, " Print final IL"; @@ -153,6 +163,35 @@ let argspec = Arg.align ] +let unescape s = + let b = Buffer.create (String.length s) in + let i = ref 0 in + while !i < String.length s do + let c = if s.[!i] <> '\\' then s.[!i] else + match (incr i; s.[!i]) with + | 'n' -> '\n' + | 'r' -> '\r' + | 't' -> '\t' + | '\\' -> '\\' + | '\'' -> '\'' + | '\"' -> '\"' + | 'u' -> + let j = !i + 2 in + i := String.index_from s j '}'; + let n = int_of_string ("0x" ^ String.sub s j (!i - j)) in + let bs = Util.Utf8.encode [n] in + Buffer.add_substring b bs 0 (String.length bs - 1); + bs.[String.length bs - 1] + | '0'..'9' | 'A'..'F' | 'a'..'f' as h -> + incr i; + Char.chr (int_of_string ("0x" ^ String.make 1 h ^ String.make 1 s.[!i])) + | c -> c (* TODO: error *) + in Buffer.add_char b c; + incr i + done; + Buffer.contents b + + (* Main *) let log s = if !logging then Printf.printf "== %s\n%!" s @@ -172,13 +211,12 @@ let () = log "IL Validation..."; Il.Valid.valid il; - (match !target with - | Prose _ | Splice _ | Interpreter _ -> - enable_pass Sideconditions; - | _ when !print_al || !print_al_o <> "" -> - enable_pass Sideconditions; - | _ -> () - ); + let need_al = + match !target with + | Prose _ | Splice _ | Interpreter _ -> true + | _ -> !print_al || !print_al_o <> "" + in + if need_al then enable_pass Sideconditions; let il = List.fold_left (fun il pass -> @@ -199,8 +237,8 @@ let () = if !print_final_il && not !print_all_il then print_il il; let al = - if not (!print_al || !print_al_o <> "") && (!target = Check || !target = Latex) then [] - else ( + if not need_al then [] else + ( log "Translating to AL..."; (Il2al.Translate.translate il @ Il2al.Manual.manual_algos) ) @@ -230,6 +268,20 @@ let () = (match !target with | Check -> () + | Parse (mode, id) -> + log "Parser Execution..."; + List.iter (fun s -> + let src = + match mode with + | `String -> unescape s + | `File -> In_channel.with_open_bin s In_channel.input_all + in + match Il.Parse.parse il id src with + | Ok e -> print_endline (Il.Print.string_of_exp e) + | Error (i, msg) -> prerr_endline (string_of_int i ^ ": " ^ msg) + | exception Il.Parse.Grammar_unknown -> prerr_endline ("unknown grammar `" ^ id ^ "`") + ) !inps + | Latex -> log "Latex Generation..."; let config = diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml index d35efd9a78..638e315506 100644 --- a/spectec/src/frontend/dim.ml +++ b/spectec/src/frontend/dim.ml @@ -428,6 +428,8 @@ and annot_exp env e : Il.Ast.exp * occur = | CaseE (atom, e1) -> let e1', occur1 = annot_exp env e1 in CaseE (atom, e1'), occur1 + | SizeE id -> + SizeE id, Env.empty | SubE (e1, t1, t2) -> let e1', occur1 = annot_exp env e1 in SubE (e1', t1, t2), occur1 @@ -482,7 +484,7 @@ and annot_sym env g : Il.Ast.sym * occur = | VarG (id, as1) -> let as1', occurs = List.split (List.map (annot_arg env) as1) in VarG (id, as1'), List.fold_left union Env.empty occurs - | NatG _ | TextG _ | EpsG -> + | NatG _ | TextG _ | EpsG | RangeG _ -> g.it, Env.empty | SeqG gs -> let gs', occurs = List.split (List.map (annot_sym env) gs) in @@ -490,10 +492,6 @@ and annot_sym env g : Il.Ast.sym * occur = | AltG gs -> let gs', occurs = List.split (List.map (annot_sym env) gs) in AltG gs', List.fold_left union Env.empty occurs - | RangeG (g1, g2) -> - let g1', occur1 = annot_sym env g1 in - let g2', occur2 = annot_sym env g2 in - RangeG (g1', g2'), union occur1 occur2 | IterG (g1, iter) -> let g1', occur1 = annot_sym env g1 in let iter', occur' = annot_iterexp env occur1 iter g.at in diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index c53e9ef462..4d5980525e 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -995,8 +995,10 @@ and infer_exp' env e : Il.exp' * typ = let _t11 = as_list_typ "expression" env Infer t1 e1.at in Il.LenE e1', NumT NatT $ e.at | SizeE id -> - let _ = find "grammar" env.grams id in - Il.NatE Z.zero, NumT NatT $ e.at + let ps, _, _, _ = find "grammar" env.grams id in + if ps <> [] then + error e.at "parameterized grammar in size expression"; + Il.SizeE id, NumT NatT $ e.at | ParenE (e1, _) | ArithE e1 -> infer_exp' env e1 | TupE es -> @@ -1585,77 +1587,75 @@ and elab_iterexp env iter : Il.iterexp = (elab_iter env iter, []) -(* Premises *) - -and elab_prem env prem : Il.prem list = - match prem.it with - | VarPr (id, t) -> - env.vars <- bind "variable" env.vars id t; - [] - | RulePr (id, e) -> - let t, _ = find "relation" env.rels id in - let mixop, _, _ = elab_typ_notation env id t in - let es', _s = elab_exp_notation' env id e t in - [Il.RulePr (id, mixop, tup_exp' es' e.at) $ prem.at] - | IfPr e -> - let e' = elab_exp env e (BoolT $ e.at) in - [Il.IfPr e' $ prem.at] - | ElsePr -> - [Il.ElsePr $ prem.at] - | IterPr ({it = VarPr _; at; _}, _iter) -> - error at "misplaced variable premise" - | IterPr (prem1, iter) -> - let prem1' = List.hd (elab_prem env prem1) in - let iter' = elab_iterexp env iter in - [Il.IterPr (prem1', iter') $ prem.at] - - (* Grammars *) and elab_sym env g : Il.sym * typ * env = + let g', t, env' = elab_sym' env g in + g' $$ g.at % elab_typ env' t, t, env' + +and elab_sym' env g : Il.sym' * typ * env = match g.it with | VarG (id, as_) -> let ps, t, _gram, _prods' = find "grammar" env.grams id in let as', s = elab_args `Rhs env as_ ps g.at in - Il.VarG (id, as') $ g.at, Subst.subst_typ s t, env + Il.VarG (id, as'), Subst.subst_typ s t, env | NatG (CharOp, n) -> let s = try Utf8.encode [Z.to_int n] with Z.Overflow | Utf8.Utf8 -> error g.at "character value out of range" in - Il.TextG s $ g.at, TextT $ g.at, env + Il.TextG s, TextT $ g.at, env | NatG (_, n) -> if n < Z.of_int 0x00 || n > Z.of_int 0xff then error g.at "byte value out of range"; - Il.NatG (Z.to_int n) $ g.at, NumT NatT $ g.at, env - | TextG s -> Il.TextG s $ g.at, TextT $ g.at, env - | EpsG -> Il.EpsG $ g.at, TupT [] $ g.at, env + Il.NatG (Char.chr (Z.to_int n)), NumT NatT $ g.at, env + | TextG s -> + Il.TextG s, TextT $ g.at, env + | EpsG -> + Il.EpsG, TupT [] $ g.at, env | SeqG gs -> let gs', _ts, env' = elab_sym_list env (filter_nl gs) in - Il.SeqG gs' $ g.at, TupT [] $ g.at, env' + Il.SeqG gs', TupT [] $ g.at, env' | AltG gs -> let gs', _ts, _env' = elab_sym_list env (filter_nl gs) in - Il.AltG gs' $ g.at, TupT [] $ g.at, env + if Free.(free_nl_list free_sym gs).varid <> Free.Set.empty then + error g.at "variable occurrences in alternative grammar"; + Il.AltG gs', TupT [] $ g.at, env | RangeG (g1, g2) -> - let g1', t1, env1 = elab_sym env g1 in - let g2', t2, env2 = elab_sym env g2 in - if env1 != env then - error g1.at "invalid symbol in range"; - if env2 != env then - error g2.at "invalid symbol in range"; - if not (equiv_typ env t1 t2) then - error_typ2 env g2.at "range item" t2 t1 " of other range item"; - Il.RangeG (g1', g2') $ g.at, TupT [] $ g.at, env - | ParenG g1 -> elab_sym env g1 + (match g1.it, g2.it with + | AttrG (e1, g11), AttrG (e2, g21) -> + (* allow inner attributes as long as they are consistent *) + if not (Eq.eq_exp e1 e2) then + error g.at "inconsistent attribute patterns in range"; + elab_sym' env (AttrG (e1, RangeG (g11, g21) $ g.at) $ g.at) + | NatG (_, n1), NatG (_, n2) -> + let _g1', _t1, _env1 = elab_sym env g1 in + let _g2', _t2, _env2 = elab_sym env g2 in + if n1 > n2 then + error g.at "inconsistent range bounds"; + Il.RangeG (Char.chr (Z.to_int n1), Char.chr (Z.to_int n2)), + NumT NatT $ g.at, env + | _, _ -> error g.at "malformed range" + ) + | ParenG g1 -> elab_sym' env g1 | TupG _ -> error g.at "malformed grammar" - | ArithG e -> elab_sym env (sym_of_exp e) + | ArithG e -> elab_sym' env (sym_of_exp e) | IterG (g1, iter) -> - let g1', t1, env1 = elab_sym env g1 in - let iterexp' = elab_iterexp env iter in - Il.IterG (g1', iterexp') $ g.at, - IterT (t1, match iter with Opt -> Opt | _ -> List) $ g.at, env1 + (match g1.it with + | AttrG (e11, g11) | ParenG {it = AttrG (e11, g11); _} -> + (* allow inner attributes as long as they are immediate *) + elab_sym' env (AttrG (IterE (e11, Iter.clone_iter iter) $ g.at, + IterG (g11, iter) $ g.at) $ g.at) + | _ -> + let g1', t1, env1 = elab_sym env g1 in + let iterexp' = elab_iterexp env iter in + let iter' = match iter with Opt -> Opt | _ -> List in + if (Free.free_sym g1).varid <> Free.Set.empty then + error g.at "variable occurrences in iteration grammar"; + Il.IterG (g1', iterexp'), IterT (t1, iter') $ g.at, env1 + ) | AttrG (e, g1) -> let g1', t1, env1 = elab_sym env g1 in let e' = elab_exp env1 e t1 in - Il.AttrG (e', g1') $ g.at, t1, env + Il.AttrG (e', g1'), t1, env | FuseG _ -> error g.at "misplaced token concatenation" | UnparenG _ -> error g.at "misplaced token unparenthesize" @@ -1666,7 +1666,7 @@ and elab_sym_list env = function let gs', ts, env'' = elab_sym_list env' gs in g'::gs', t::ts, env'' -and elab_prod env prod t : Il.prod = +and elab_prod env prod as' t : Il.prod = let (g, e, prems) = prod.it in let env' = local_env env in let dims = Dim.check_prod prod in @@ -1686,11 +1686,36 @@ and elab_prod env prod t : Il.prod = Acc.sym g; Acc.exp e; Acc.prems prems; - Il.ProdD (!acc_bs', g', e', prems') $ prod.at + Il.ProdD (!acc_bs', as', g', e', prems') $ prod.at -and elab_gram env gram t : Il.prod list = +and elab_gram env gram as' t : Il.prod list = let (_dots1, prods, _dots2) = gram.it in - map_filter_nl_list (fun prod -> elab_prod env prod t) prods + map_filter_nl_list (fun prod -> elab_prod env prod as' t) prods + + +(* Premises *) + +and elab_prem env prem : Il.prem list = + match prem.it with + | VarPr (id, t) -> + env.vars <- bind "variable" env.vars id t; + [] + | RulePr (id, e) -> + let t, _ = find "relation" env.rels id in + let mixop, _, _ = elab_typ_notation env id t in + let es', _s = elab_exp_notation' env id e t in + [Il.RulePr (id, mixop, tup_exp' es' e.at) $ prem.at] + | IfPr e -> + let e' = elab_exp env e (BoolT $ e.at) in + [Il.IfPr e' $ prem.at] + | ElsePr -> + [Il.ElsePr $ prem.at] + | IterPr ({it = VarPr _; at; _}, _iter) -> + error at "misplaced variable premise" + | IterPr (prem1, iter) -> + let prem1' = List.hd (elab_prem env prem1) in + let iter' = elab_iterexp env iter in + [Il.IterPr (prem1', iter') $ prem.at] (* Definitions *) @@ -1753,7 +1778,7 @@ and make_binds_iter_arg env free dims : Il.bind list ref * (module Iter.Arg) = if Free.Set.mem id.it !left.defid then ( let ps, t, _ = find "definition" env.defs id in let env' = local_env env in - let ps' = elab_params env' ps in + let ps', _as' = elab_params env' ps in let t' = elab_typ env' t in let free' = Free.(union (free_params ps) (diff (free_typ t) (bound_params ps))) in let fwd = Free.(inter free' !left) in @@ -1790,8 +1815,10 @@ and elab_arg in_lhs env a p s : Il.arg list * Subst.subst = | TypA t, TypP id -> let t' = elab_typ env t in [Il.TypA t' $ a.at], Subst.add_typid s id t +(* | GramA g, GramP _ when in_lhs = `Lhs -> error g.at "misplaced grammar symbol" +*) | GramA g, GramP (id', t) -> let g', t', _ = elab_sym env g in let s' = subst_implicit env s t t' in @@ -1845,7 +1872,7 @@ and subst_implicit env s t t' : Subst.subst = | _ -> s in inst s t t' -and elab_param env p : Il.param list = +and elab_param env p : Il.param list * Il.arg list = match p.it with | ExpP (id, t) -> let t' = elab_typ env t in @@ -1864,38 +1891,39 @@ and elab_param env p : Il.param list = ) else env.vars <- bind "variable" env.vars id t; - [Il.ExpP (id, t') $ p.at] + [Il.ExpP (id, t') $ p.at], [Il.ExpA (Il.VarE id $$ p.at % t') $ p.at] | TypP id -> env.typs <- bind "syntax type" env.typs id ([], Opaque); env.gvars <- bind "variable" env.gvars (strip_var_sub id) (VarT (id, []) $ id.at); - [Il.TypP id $ p.at] + [Il.TypP id $ p.at], [Il.TypA (Il.VarT (id, []) $ p.at) $ p.at] | GramP (id, t) -> (* Treat unbound type identifiers in t as implicitly bound. *) let free = Free.free_typ t in env.grams <- bind "grammar" env.grams id ([], t, None, []); - let ps' = - Free.Set.fold (fun id' ps' -> - if Map.mem id' env.typs then ps' else ( + let ps', as' = + Free.Set.fold (fun id' (ps', as') -> + if Map.mem id' env.typs then ps', as' else ( let id = id' $ t.at in if id.it <> (strip_var_suffix id).it then error_id id "invalid identifer suffix in binding position"; env.typs <- bind "syntax type" env.typs id ([], Opaque); env.gvars <- bind "variable" env.gvars (strip_var_sub id) (VarT (id, []) $ id.at); - (Il.TypP id $ id.at) :: ps' + (Il.TypP id $ id.at) :: ps', (Il.TypA (Il.VarT (id, []) $ id.at) $ id.at) :: as' ) - ) free.typid [] + ) free.typid ([], []) in let t' = elab_typ env t in - ps' @ [Il.GramP (id, t') $ p.at] + ps' @ [Il.GramP (id, t') $ p.at], as' @ [Il.GramA (Il.VarG (id, []) $$ p.at % t') $ p.at] | DefP (id, ps, t) -> let env' = local_env env in - let ps' = elab_params env' ps in + let ps', _as' = elab_params env' ps in let t' = elab_typ env' t in env.defs <- bind "definition" env.defs id (ps, t, []); - [Il.DefP (id, ps', t') $ p.at] + [Il.DefP (id, ps', t') $ p.at], [Il.DefA id $ p.at] -and elab_params env ps : Il.param list = - List.concat_map (elab_param env) ps +and elab_params env ps : Il.param list * Il.arg list = + let pss', ass' = List.split (List.map (elab_param env) ps) in + List.concat pss', List.concat ass' let infer_typ_definition _env t : kind = @@ -1992,7 +2020,7 @@ let elab_def env d : Il.def list = Debug.(log_in_at "el.elab_def" d.at (fun _ -> el_def d)); match d.it with | FamD (id, ps, hints) -> - let ps' = elab_params (local_env env) ps in + let ps', _as' = elab_params (local_env env) ps in let dims = Dim.check_def d in infer_no_binds env dims d; env.typs <- rebind "syntax type" env.typs id (ps, Family []); @@ -2038,14 +2066,14 @@ let elab_def env d : Il.def list = env.typs <- rebind "syntax type" env.typs id1 (ps1, k1'); (if not closed then [] else let ps = List.map Convert.param_of_arg as_ in - let ps' = elab_params (local_env env) ps in + let ps', _as' = elab_params (local_env env) ps in [Il.TypD (id1, ps', [inst']) $ d.at] ) @ elab_hintdef env (TypH (id1, id2, hints) $ d.at) | GramD (id1, id2, ps, t, gram, hints) -> let env' = local_env env in - let ps' = elab_params env' ps in + let ps', as' = elab_params env' ps in let t' = elab_typ env' t in - let prods' = elab_gram env' gram t in + let prods' = elab_gram env' gram as' t in let dims = Dim.check_def d in infer_no_binds env' dims d; let ps1, t1, gram1_opt, prods1' = find "grammar" env.grams id1 in @@ -2098,7 +2126,7 @@ let elab_def env d : Il.def list = [] | DecD (id, ps, t, hints) -> let env' = local_env env in - let ps' = elab_params env' ps in + let ps', _as' = elab_params env' ps in let t' = elab_typ env' t in let dims = Dim.check_def d in infer_no_binds env dims d; diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml index aa32c6c576..ac77fcc79d 100644 --- a/spectec/src/frontend/eval.ml +++ b/spectec/src/frontend/eval.ml @@ -57,9 +57,17 @@ let disj_list disj_x env xs1 xs2 = List.length xs1 <> List.length xs2 || List.exists2 (disj_x env) xs1 xs2 +(* Iteration *) + +let rec reduce_iter env iter : iter = + match iter with + | Opt | List | List1 -> iter + | ListN (e, ido) -> ListN (reduce_exp env e, ido) + + (* Type Reduction (weak-head) *) -let rec reduce_typ env t : typ = +and reduce_typ env t : typ = Debug.(log_if "el.reduce_typ" (t.it <> NumT NatT) (fun _ -> fmt "%s" (el_typ t)) (fun r -> fmt "%s" (el_typ r)) @@ -327,7 +335,8 @@ and reduce_exp env e : exp = ) | IterE (e1, iter) -> let e1' = reduce_exp env e1 in - IterE (e1', iter) $ e.at (* TODO(2, rossberg): simplify? *) + let iter' = reduce_iter env iter in + IterE (e1', iter') $ e.at (* TODO(2, rossberg): simplify? *) | HoleE _ | FuseE _ | UnparenE _ | LatexE _ -> assert false and reduce_expfield env (atom, e) : expfield = (atom, reduce_exp env e) @@ -809,6 +818,11 @@ and snd3 (_, x, _) = x (* Type Disjointness *) +and disj_iter env iter1 iter2 = + match iter1, iter2 with + | ListN (e1, _), ListN (e2, _) -> disj_exp env e1 e2 + | _, _ -> not (Eq.eq_iter iter1 iter2) + and disj_typ env t1 t2 = Debug.(log "el.disj_typ" (fun _ -> fmt "%s ## %s" (el_typ t1) (el_typ t2)) Bool.to_string @@ -832,7 +846,7 @@ and disj_typ env t1 t2 = | _, ParenT t21 -> disj_typ env t1 t21 | TupT ts1, TupT ts2 | SeqT ts1, SeqT ts2 -> disj_list disj_typ env ts1 ts2 | IterT (t11, iter1), IterT (t21, iter2) -> - disj_typ env t11 t21 || not (Eq.eq_iter iter1 iter2) + disj_typ env t11 t21 || disj_iter env iter1 iter2 | AtomT atom1, AtomT atom2 -> atom1.it <> atom2.it | InfixT (t11, atom1, t12), InfixT (t21, atom2, t22) -> disj_typ env t11 t21 || atom1.it <> atom2.it || disj_typ env t12 t22 diff --git a/spectec/src/frontend/eval.mli b/spectec/src/frontend/eval.mli index da866387cd..7e97574abb 100644 --- a/spectec/src/frontend/eval.mli +++ b/spectec/src/frontend/eval.mli @@ -10,6 +10,7 @@ type subst = El.Subst.t val (let*) : subst option -> (subst -> subst option) -> subst option +val reduce_iter : env -> iter -> iter val reduce_exp : env -> exp -> exp val reduce_typ : env -> typ -> typ val reduce_arg : env -> arg -> arg diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index 22b7ffb0ff..953878f8f0 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -103,6 +103,7 @@ and exp' = | ExtE of exp * path * exp (* exp[path =.. exp] *) | CallE of id * arg list (* defid( arg* ) *) | IterE of exp * iterexp (* exp iter *) + | SizeE of id (* ||gramid|| *) | SubE of exp * typ * typ (* exp : typ1 <: typ2 *) and expfield = atom * exp (* atom exp *) @@ -119,15 +120,15 @@ and iterexp = iter * (id * exp) list (* Grammars *) -and sym = sym' phrase +and sym = (sym', typ) note_phrase and sym' = | VarG of id * arg list (* gramid (`(` arg,* `)`)? *) - | NatG of int (* nat *) + | NatG of char (* nat *) | TextG of string (* `"`text`"` *) | EpsG (* `eps` *) | SeqG of sym list (* sym sym *) | AltG of sym list (* sym `|` sym *) - | RangeG of sym * sym (* sym `|` `...` `|` sym *) + | RangeG of char * char (* nat `|` `...` `|` nat *) | IterG of sym * iterexp (* sym iter *) | AttrG of exp * sym (* exp `:` sym *) @@ -178,7 +179,7 @@ and clause' = and prod = prod' phrase and prod' = - | ProdD of bind list * sym * exp * prem list (* grammar production *) + | ProdD of bind list * arg list * sym * exp * prem list (* grammar production *) and prem = prem' phrase and prem' = diff --git a/spectec/src/il/debug.ml b/spectec/src/il/debug.ml index dcba627d98..09ebdb215a 100644 --- a/spectec/src/il/debug.ml +++ b/spectec/src/il/debug.ml @@ -3,7 +3,8 @@ include Util.Debug_log open Print let il_side = function `Lhs -> "L" | `Rhs -> "" -let il_id = Util.Source.it +let il_text = string_of_text +let il_id = string_of_id let il_atom = string_of_atom let il_mixop = string_of_mixop let il_iter = string_of_iter @@ -19,6 +20,7 @@ let il_args = list il_arg let il_binds = string_of_binds let il_params = list il_param let il_def = string_of_def + let il_free s = String.concat " " Free.[ set s.typid; @@ -26,6 +28,7 @@ let il_free s = String.concat " " set s.gramid; set s.defid; ] + let il_subst s = String.concat " " Subst.[ mapping il_typ s.typid; diff --git a/spectec/src/il/dune b/spectec/src/il/dune index 6abfab98a0..1a8c849dec 100644 --- a/spectec/src/il/dune +++ b/spectec/src/il/dune @@ -1,5 +1,5 @@ (library (name il) (libraries util zarith el) - (modules mixop ast eq free subst iter env eval print debug valid) + (modules mixop ast eq free subst iter env eval print debug valid parse) ) diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml index 665eefd52e..28d24ddf12 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml @@ -94,6 +94,7 @@ and eq_exp e1 e2 = | ProjE (e1, i1), ProjE (e2, i2) -> eq_exp e1 e2 && i1 = i2 | TheE e1, TheE e2 -> eq_exp e1 e2 | CaseE (op1, e1), CaseE (op2, e2) -> eq_mixop op1 op2 && eq_exp e1 e2 + | SizeE id1, SizeE id2 -> eq_id id1 id2 | SubE (e1, t11, t12), SubE (e2, t21, t22) -> eq_exp e1 e2 && eq_typ t11 t21 && eq_typ t12 t22 | _, _ -> e1.it = e2.it @@ -122,7 +123,6 @@ and eq_sym g1 g2 = eq_id id1 id2 && eq_list eq_arg args1 args2 | SeqG gs1, SeqG gs2 | AltG gs1, AltG gs2 -> eq_list eq_sym gs1 gs2 - | RangeG (g11, g12), RangeG (g21, g22) -> eq_sym g11 g21 && eq_sym g12 g22 | IterG (g11, iter1), IterG (g21, iter2) -> eq_sym g11 g21 && eq_iterexp iter1 iter2 | AttrG (e1, g11), AttrG (e2, g21) -> eq_exp e1 e2 && eq_sym g11 g21 diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index fdd650fc6f..ccceb3899d 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -30,6 +30,11 @@ let snd3 (_, x, _) = x let unordered s1 s2 = not Set.(subset s1 s2 || subset s2 s1) +let as_iter_typ t = + match t.it with + | IterT (t1, _) -> t1 + | _ -> failwith "as_iter_typ" + let as_opt_exp e = match e.it with | OptE eo -> eo @@ -89,7 +94,7 @@ and reduce_typdef env t : deftyp = and reduce_typ_app env id args at : deftyp option = Debug.(log "il.reduce_typ_app" - (fun _ -> fmt "%s(%s)" id.it (il_args args)) + (fun _ -> fmt "%s(%s)" (il_id id) (il_args args)) (fun r -> fmt "%s" (opt il_deftyp r)) ) @@ fun _ -> reduce_typ_app' env id (List.map (reduce_arg env) args) at (Env.find_opt_typ env id) @@ -102,7 +107,7 @@ and reduce_typ_app' env id args at = function ("undefined instance of partial type `" ^ id.it ^ "`") | Some (ps, {it = InstD (_binds, args', dt); _}::insts') -> Debug.(log "il.reduce_typ_app'" - (fun _ -> fmt "%s(%s) =: %s(%s)" id.it (il_args args) id.it (il_args args')) + (fun _ -> fmt "%s(%s) =: %s(%s)" (il_id id) (il_args args) (il_id id) (il_args args')) (fun r -> fmt "%s" (opt (Fun.const "!") r)) ) @@ fun _ -> match match_list match_arg env Subst.empty args args' with @@ -312,7 +317,7 @@ and reduce_exp env e : exp = else if List.for_all Option.is_some eos' then let es1' = List.map Option.get eos' in let s = List.fold_left2 Subst.add_varid Subst.empty ids es1' in - reduce_exp env (Subst.subst_exp s e1') + OptE (Some (reduce_exp env (Subst.subst_exp s e1'))) $> e else IterE (e1', iterexp') $> e | List | List1 -> @@ -327,7 +332,7 @@ and reduce_exp env e : exp = let ns = List.map List.length ess' in let n = Z.to_int n' in if List.for_all ((=) n) ns then - (TupE (List.init n (fun i -> + (ListE (List.init n (fun i -> let esI' = List.map (fun es -> List.nth es i) ess' in let s = List.fold_left2 Subst.add_varid Subst.empty ids esI' in let s' = @@ -372,6 +377,7 @@ and reduce_exp env e : exp = | _ -> CatE (e1', e2') ) $> e | CaseE (op, e1) -> CaseE (op, reduce_exp env e1) $> e + | SizeE _ -> e | SubE (e1, t1, t2) when equiv_typ env t1 t2 -> reduce_exp env e1 | SubE (e1, t1, t2) -> @@ -472,7 +478,7 @@ and reduce_exp_call env id args at = function ("undefined call to partial function `$" ^ id.it ^ "`") | {it = DefD (_binds, args', e, prems); _}::clauses' -> Debug.(log "il.reduce_exp_call" - (fun _ -> fmt "$%s(%s) =: $%s(%s)" id.it (il_args args) id.it (il_args args')) + (fun _ -> fmt "$%s(%s) =: $%s(%s)" (il_id id) (il_args args) (il_id id) (il_args args')) (function None -> "-" | Some e' -> fmt "%s" (il_exp e')) ) @@ fun _ -> assert (List.for_all (fun a -> Eq.eq_arg a (reduce_arg env a)) args); @@ -495,6 +501,10 @@ and reduce_prems env = function | other -> other and reduce_prem env prem : bool option = + Debug.(log "il.reduce_prem" + (fun _ -> fmt "%s" (il_prem prem)) + (fun r -> fmt "%s" (match r with None -> "-" | Some b -> string_of_bool b)) + ) @@ fun _ -> match prem.it with | RulePr _ -> None | IfPr e -> @@ -509,7 +519,49 @@ and reduce_prem env prem : bool option = | None -> None | exception Irred -> None ) - | IterPr (_prem, _iter) -> None (* TODO(3, rossberg): reduce? *) + | IterPr (prem1, iterexp) -> + let iter', xes' = reduce_iterexp env iterexp in + let ids, es' = List.split xes' in + match iter' with + | Opt -> + let eos' = List.map as_opt_exp es' in + if List.for_all Option.is_none eos' then + Some true + else if List.for_all Option.is_some eos' then + let es1' = List.map Option.get eos' in + let s = List.fold_left2 Subst.add_varid Subst.empty ids es1' in + reduce_prem env (Subst.subst_prem s prem1) + else + None + | List | List1 -> + let n = List.length (as_list_exp (List.hd es')) in + if iter' = List || n >= 1 then + let en = NatE (Z.of_int n) $$ prem.at % (NumT NatT $ prem.at) in + reduce_prem env (IterPr (prem1, (ListN (en, None), xes')) $ prem.at) + else + None + | ListN ({it = NatE n'; _}, ido) -> + let ess' = List.map as_list_exp es' in + let ns = List.map List.length ess' in + let n = Z.to_int n' in + if List.for_all ((=) n) ns then + List.fold_left (fun b_opt i -> + match b_opt with + | None | Some false -> b_opt + | Some true -> + let esI' = List.map (fun es -> List.nth es i) ess' in + let s = List.fold_left2 Subst.add_varid Subst.empty ids esI' in + let s' = + Option.fold ido ~none:s ~some:(fun id -> + let en = NatE (Z.of_int i) $$ id.at % (NumT NatT $ id.at) in + Subst.add_varid s id en + ) + in reduce_prem env (Subst.subst_prem s' prem1) + ) (Some true) (List.init n Fun.id) + else + None + | ListN _ -> + None (* Matching *) @@ -695,7 +747,8 @@ and match_exp' env s e1 e2 : subst option = let xs, exs = List.split xes in let* s''' = match_list (fun env s xI exI -> - let eI = ListE (List.map (fun sJ -> Subst.subst_exp sJ (VarE xI $> exI)) ss) $> e2 in + let varI = VarE xI $$ xI.at % as_iter_typ exI.note in + let eI = ListE (List.map (fun sJ -> Subst.subst_exp sJ varI) ss) $> e2 in match_exp' env s eI exI ) env s' xs exs in Some (Subst.union s''' s) (* re-add possibly locally shadowed bindings *) @@ -790,7 +843,10 @@ and match_sym env s g1 g2 : subst option = (* Parameters *) and match_arg env s a1 a2 : subst option = - Debug.(log_in "il.match_arg" (fun _ -> fmt "%s =: %s" (il_arg a1) (il_arg a2))); + Debug.(log "il.match_arg" + (fun _ -> fmt "%s =: %s" (il_arg a1) (il_arg a2)) + (fun r -> fmt "%s" (opt il_subst r)) + ) @@ fun _ -> match a1.it, a2.it with | ExpA e1, ExpA e2 -> match_exp env s e1 e2 | TypA t1, TypA t2 -> match_typ env s t1 t2 @@ -896,7 +952,7 @@ and equiv_params env ps1 ps2 = Some (Subst.add_defid s id2 id1) | GramP (id1, t1), GramP (id2, t2) -> if not (equiv_typ env t1 t2) then None else - Some (Subst.add_gramid s id2 (VarG (id1, []) $ p1.at)) + Some (Subst.add_gramid s id2 (VarG (id1, []) $$ p1.at % t1)) | _, _ -> assert false ) (Some Subst.empty) ps1 ps2 diff --git a/spectec/src/il/eval.mli b/spectec/src/il/eval.mli index e8c9b691fc..461b32bf88 100644 --- a/spectec/src/il/eval.mli +++ b/spectec/src/il/eval.mli @@ -3,12 +3,16 @@ open Ast type env = Env.t type subst = Subst.t +val is_normal_exp : exp -> bool +val is_head_normal_exp : exp -> bool + val (let*) : subst option -> (subst -> subst option) -> subst option val reduce_exp : env -> exp -> exp val reduce_typ : env -> typ -> typ val reduce_typdef : env -> typ -> deftyp val reduce_arg : env -> arg -> arg +val reduce_prems : env -> prem list -> bool option val equiv_functyp : env -> param list * typ -> param list * typ -> bool val equiv_typ : env -> typ -> typ -> bool diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index cf95dee877..51ad31d835 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -136,6 +136,7 @@ and free_exp e = | CaseE (_, e1) | UncaseE (e1, _) -> free_exp e1 | CallE (id, as1) -> free_defid id + free_args as1 | IterE (e1, iter) -> (free_exp e1 - bound_iterexp iter) + free_iterexp iter + | SizeE id -> free_gramid id | SubE (e1, t1, t2) -> free_exp e1 + free_typ t1 + free_typ t2 and free_expfield (_, e) = free_exp e @@ -159,9 +160,8 @@ and bound_iterexp (iter, xes) = and free_sym g = match g.it with | VarG (id, as_) -> free_gramid id + free_args as_ - | NatG _ | TextG _ | EpsG -> empty + | NatG _ | TextG _ | EpsG | RangeG _ -> empty | SeqG gs | AltG gs -> free_list free_sym gs - | RangeG (g1, g2) -> free_sym g1 + free_sym g2 | IterG (g1, iter) -> (free_sym g1 - bound_iterexp iter) + free_iterexp iter | AttrG (e, g1) -> free_exp e + free_sym g1 @@ -240,8 +240,8 @@ let free_clause clause = let free_prod prod = match prod.it with - | ProdD (bs, g, e, prems) -> - free_binds bs + (free_sym g + free_exp e + free_prems prems - bound_binds bs) + | ProdD (bs, as_, g, e, prems) -> + free_binds bs + (free_args as_ + free_sym g + free_exp e + free_prems prems - bound_binds bs) let free_hintdef hd = match hd.it with diff --git a/spectec/src/il/free.mli b/spectec/src/il/free.mli index 8bfb6597e1..1f7a051965 100644 --- a/spectec/src/il/free.mli +++ b/spectec/src/il/free.mli @@ -20,6 +20,7 @@ val free_iter : iter -> sets val free_typ : typ -> sets val free_exp : exp -> sets val free_path : path -> sets +val free_sym : sym -> sets val free_prem : prem -> sets val free_arg : arg -> sets val free_def : def -> sets diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml index 649f540073..518fb73f58 100644 --- a/spectec/src/il/iter.ml +++ b/spectec/src/il/iter.ml @@ -136,6 +136,7 @@ and exp e = | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> exp e1; path p; exp e2 | CallE (x, as_) -> defid x; args as_ | IterE (e1, it) -> exp e1; iterexp it + | SizeE id -> gramid id | SubE (e1, t1, t2) -> exp e1; typ t1; typ t2 and expfield (at, e) = atom at; exp e @@ -161,7 +162,7 @@ and sym g = | TextG s -> text s | EpsG -> () | SeqG gs | AltG gs -> list sym gs - | RangeG (g1, g2) -> sym g1; sym g2 + | RangeG (n1, n2) -> nat n1; nat n2 | IterG (g1, it) -> sym g1; iterexp it | AttrG (e, g1) -> exp e; sym g1 @@ -228,7 +229,7 @@ let clause c = let prod p = match p.it with - | ProdD (bs, g, e, prs) -> binds bs; sym g; exp e; prems prs + | ProdD (bs, as_, g, e, prs) -> binds bs; args as_; sym g; exp e; prems prs let rec def d = visit_def d; diff --git a/spectec/src/il/parse.ml b/spectec/src/il/parse.ml new file mode 100644 index 0000000000..99a6543f14 --- /dev/null +++ b/spectec/src/il/parse.ml @@ -0,0 +1,381 @@ +open Ast +open Util.Source + + +(* Flags *) + +let trace = ref false +let check_ambiguity = ref false + + +(* Source stream *) + +type stream = {src : string; pos : int} + +let stream src = {src; pos = 0} + +let pos str = str.pos +let rem str = String.length str.src - str.pos +let eof str = (rem str = 0) +let get str = str.src.[str.pos] +let text str n = String.sub str.src str.pos n +let rest str = String.sub str.src str.pos (String.length str.src - str.pos) +let adv str n = {str with pos = str.pos + n} + +let at str n = + let left = {no_pos with column = str.pos} in + let right = {no_pos with column = str.pos + n} in + {left; right} + + +(* Tracing *) + +type trace_entry = {id : id; args : arg list; prod : sym option} (* for logging *) +type 'a trace = {entries : trace_entry list; print : 'a -> string} + +let empty_trace = {entries = []; print = fun _ -> assert false} + +let enter tr id args print = + {print; entries = {id; args; prod = None}::tr.entries} + +let alt tr prod = + {tr with entries = {(List.hd tr.entries) with prod}::(List.tl tr.entries)} + +let prod tr = (List.hd tr.entries).prod + +let string_of_exps es = + "[" ^ Print.(string_of_list string_of_exp " " es) ^ "]" + +let rec string_of_sym g = + match g.it with + | VarG (id, as_) -> id.it ^ string_of_args as_ + | SeqG gs -> Print.string_of_list string_of_sym_paren " " gs + | AltG gs -> Print.string_of_list string_of_sym_paren "|" gs + | RangeG (b1, b2) -> Print.string_of_byte b1 ^ "|...|" ^ Print.string_of_byte b2 + | IterG (g1, (iter, _)) -> string_of_sym_paren g1 ^ Print.string_of_iter iter + | AttrG (_e, g1) -> string_of_sym g1 + | _ -> Print.string_of_sym ~short:true g + +and string_of_sym_paren g = + match g.it with + | SeqG _ | AltG _ | RangeG _ -> "(" ^ string_of_sym g ^ ")" + | _ -> string_of_sym g + +and string_of_args as_ = + if as_ = [] then "" else + "(" ^ String.concat "," (List.filter_map string_of_arg as_) ^ ")" + +and string_of_arg a = + match a.it with + | ExpA e -> Some (Print.string_of_exp e) + | TypA _ -> None + | DefA id -> Some ("$" ^ id.it) + | GramA g -> Some (string_of_sym g) + +let string_of_trace_entry entry = + string_of_sym + (VarG (entry.id, entry.args) $$ no_region % (TupT [] $ no_region)) + +let string_of_trace tr = + String.concat "/" (List.map string_of_trace_entry (List.rev tr.entries)) + +let trace_log tr str value = + if !trace then + ( + let pre = string_of_trace tr in + let src = rest str in + let src' = + if String.length src <= 20 + then Print.string_of_string src + else Print.string_of_string (String.sub src 0 16) ^ "..." + in + let value' = + if value = "" then "" + else if String.length value <= 30 then " => " ^ value + else " => " ^ String.sub value 0 26 ^ "..." + in + match prod tr with + | None -> + Printf.printf "%s%s @ %s\n%!" pre value' src' + | Some g -> + Printf.printf "%s ::= %s%s @ %s\n%!" pre (string_of_sym g) value' src' + ) + + +(* Results *) + +type 'a results = + | Success of 'a trace * stream * Subst.t * 'a * 'a results Lazy.t + | Failure of string trace * stream * string + +let string_of_results = function + | Success (tr, _str, _s, v, _tl) -> tr.print v + | Failure (_tr, _str, msg) -> "fail: " ^ msg + +let il_results = function + | Success (tr, str, _, v, _) -> + Debug.(fmt "success[%s] @ %s" (tr.print v) (il_text (rest str))) + | Failure (_, _, msg) -> "failure[" ^ msg ^ "]" + +let failure tr str msg = + Failure ({tr with print = Fun.id}, str, msg) +let unexpected tr str = + failure tr str ("unexpected " ^ (if eof str then "end of " else "") ^ "input") +let success tr str n s e = + Success (tr, adv str n, s, e, lazy (unexpected tr str)) +let success_final tr str n s e = + Success (tr, adv str n, s, e, lazy (failure tr str "")) + +let trace_result = function + | Failure (tr, str, msg) as r -> if msg <> "" then trace_log tr str (string_of_results r) + | Success (tr, str, _, _, _) as r -> trace_log tr str (string_of_results r) + +let rec map_results f r = + match r with + | Failure _ -> f r + | Success (tr, str, s, e, tl) -> + f (Success (tr, str, s, e, lazy (map_results f (Lazy.force tl)))) + +let rec append_results r1 lr2 = + match r1 with + | Failure (_, str1, msg1) -> + (match Lazy.force lr2 with + | Failure (_, str2, msg2) when msg2 = "" || msg1 <> "" && pos str1 > pos str2 -> r1 + | r2 -> r2 + ) + | Success (tr, str, s, e, tl) -> + Success (tr, str, s, e, lazy (append_results (Lazy.force tl) lr2)) + +(* Using this for bind would implement breadth-first search +let rec interleave_results r1 lr2 = + match r1 with + | Failure _ -> Lazy.force lr2 + | Success (str, s, e, tl) -> + Success (str, s, e, lazy (interleave_results (Lazy.force lr2) tl)) +*) + +let rec bind_results r f = + match r with + | Failure (tr, str, msg) -> Failure (tr, str, msg) (* need to copy for polymorphism *) + | Success (_tr, str, s, e, tl) -> + append_results (f (str, s, e)) (lazy (bind_results (Lazy.force tl) f)) + +let (let*) = bind_results +let (|||) = append_results + + +(* Tracing *) + +let trace_parse tr str f = + trace_log tr str ""; + match f tr with + | r -> + map_results (function + | Failure (_tr', str', msg) -> + let r' = failure tr str' msg in + trace_result r'; r' + | Success (_tr', str', s, e, tl) -> + let r' = Success (tr, str', s, e, tl) in + trace_result r'; r' + ) r + | exception exn -> + let bt = Printexc.get_raw_backtrace () in + trace_log tr str ("raise " ^ Printexc.to_string exn); + Printexc.raise_with_backtrace exn bt + +let trace_alt tr str g f = + trace_parse (alt tr (Some g)) str f + + +(* Parsing *) + +let rec parse_sym env (tr : exp trace) str s g : exp results = + Debug.(log "il.parse_sym" + (fun _ -> fmt "%s: %s" (il_sym g) (il_text (rest str))) il_results + ) @@ fun _ -> + match g.it with + | VarG (x, as_) -> + let* str', _s', e = parse_gram env tr str x as_ in + let s' = Subst.add_sizeid s x (pos str' - pos str) in + success tr str' 0 s' e + | NatG _ when eof str -> + unexpected tr str + | NatG b -> + if get str = b then + success_final tr str 1 s (NatE (Z.of_int (Char.code b)) $$ at str 1 % g.note) + else + failure tr str (Printf.sprintf "byte %s expected" (Print.string_of_byte b)) + | TextG t when t <> "" && eof str -> + unexpected tr str + | TextG t -> + let n = String.length t in + if rem str >= n && text str n = t then + success_final tr str n s (TextE t $$ at str n % g.note) + else + failure tr str (Printf.sprintf "text %s expected" (Print.string_of_string t)) + | EpsG -> + success_final tr str 0 s (TupE [] $$ at str 0 % g.note) + | SeqG [] -> + success_final tr str 0 s (TupE [] $$ at str 0 % g.note) + | SeqG (g1::gs) -> + let* str', s', _e = parse_sym env tr str s g1 in + parse_sym env tr str' s' {g with it = SeqG gs} + | AltG gs -> + let id = "(_|...|_)" $ no_region in + trace_parse (enter tr id [] Print.string_of_exp) str @@ fun tr' -> + parse_sym_alts env tr' str s 0 gs + | RangeG _ when eof str -> + unexpected tr str + | RangeG (b1, b2) when b1 <= get str && get str <= b2-> + parse_sym env tr str s (NatG (get str) $$ g.at % g.note) + | RangeG (b1, b2) -> + failure tr str (Printf.sprintf "byte %s..%s expected" + (Print.string_of_byte b1) (Print.string_of_byte b2)) + | IterG (g1, (Opt, _xes)) -> + let tr' = enter tr (string_of_sym g $ no_region) [] string_of_exps in + let* str', s', es = parse_sym_list env tr' str s 0 1 g1 in + let eo = match es with [] -> None | e::_ -> Some e in + success tr str' 0 s' (OptE eo $$ g.at % g.note) + | IterG (g1, (List, _xes)) -> + let tr' = enter tr (string_of_sym g $ no_region) [] string_of_exps in + let* str', s', es = parse_sym_list env tr' str s 0 max_int g1 in + success tr str' 0 s' (ListE es $$ g.at % g.note) + | IterG (g1, (List1, _xes)) -> + let tr' = enter tr (string_of_sym g $ no_region) [] string_of_exps in + let* str', s', es = parse_sym_list env tr' str s 1 max_int g1 in + if es = [] then + failure tr str "non-empty sequence expected" + else + success tr str' 0 s' (ListE es $$ g.at % g.note) + | IterG (g1, (ListN (en, _ido), _xes)) -> + (match (Eval.reduce_exp env (Subst.subst_exp s en)).it with + | NatE n -> + let tr' = enter tr (string_of_sym g $ no_region) [] string_of_exps in + let* str', s', es = parse_sym_list env tr' str s (Z.to_int n) (Z.to_int n) g1 in + success tr str' 0 s' (ListE es $$ g.at % g.note) + | _ -> + failure tr str "cannot determine expected length of sequence" + ) + | AttrG (e, g1) -> + let* str', s', e' = parse_sym env tr str s g1 in + match Eval.match_exp env s' e' e with + | Some s'' -> success_final tr str' 0 s'' e' + | None -> failure tr str "result does not match attribute pattern" + +(* +and parse_sym_opt env (tr : exp option trace) str s g1 : exp option results = + ( trace_alt tr str (EpsG $$ g1.at % g1.note) @@ fun _tr' -> + success_final tr str 0 s None + ) ||| + lazy ( + trace_alt tr str g1 @@ fun tr' -> + let tr'' = {tr' with print = Print.string_of_exp} in + let* str', s', e = parse_sym env tr'' str s g1 in + success tr str' 0 s' (Some e) + ) +*) + +and parse_sym_list env (tr : exp list trace) str s m n g1 : exp list results = + let r1 () = + ( trace_alt tr str (EpsG $$ g1.at % g1.note) @@ fun _tr' -> + success_final tr str 0 s [] + ) + in + let r2 = + lazy ( + let g' = IterG (g1, (List, [])) $$ g1.at % g1.note in + trace_alt tr str (SeqG [g1; g'] $$ g1.at % g1.note) @@ fun tr' -> + let tr1 = {tr' with print = Print.string_of_exp} in + let* str', s', e = parse_sym env tr1 str s g1 in + let tr2 = enter tr' (string_of_sym g' $ no_region) [] string_of_exps in + let* str'', s'', es = + parse_sym_list env tr2 str' s' (max 0 (m - 1)) (n - 1) g1 in + success tr str'' 0 s'' (e::es) + ) + in + if n = 0 then r1 () else + if m > 0 then Lazy.force r2 else + r1 () ||| r2 + +and parse_sym_alts env tr str s i = function + | [] -> unexpected tr str + | g1::[] when i = 0 -> + trace_alt tr str g1 @@ fun tr' -> + parse_sym env tr' str s g1 (* preserve error message *) + | g1::gs' -> + ( trace_alt tr str g1 @@ fun tr' -> + parse_sym env tr' str s g1 + ) ||| + lazy (parse_sym_alts env tr str s (i + 1) gs') + +and parse_prod env tr str as_ prod = + let ProdD (_bs, as', g, e, prems) = prod.it in + Debug.(log "il.parse_prod" + (fun _ -> fmt "%s -> %s @ %s" (il_sym g) (il_exp e) (il_text (rest str))) + il_results + ) @@ fun _ -> + match Eval.match_list Eval.match_arg env Subst.empty as_ as' with + | exception Eval.Irred -> failure tr str "irreducible grammar arguments" + | None -> failure tr str "grammar undefined for arguments" + | Some s -> + let g', e', prems' = + Subst.(subst_sym s g, subst_exp s e, subst_prems s prems) in + trace_alt tr str g' @@ fun tr' -> + Debug.(log_in "il.parse_prod" (fun _ -> "arg subst: " ^ mapping il_exp s.varid)); + let* str', s', _e' = parse_sym env tr' str Subst.empty g' in + Debug.(log_in "il.parse_prod" (fun _ -> "prem subst: " ^ mapping il_exp s'.varid)); + match Eval.reduce_prems env (Subst.subst_prems s' prems') with + | None -> failure tr' str "cannot verify side condition" + | Some false -> failure tr' str "violating side condition" + | Some true -> + success_final tr' str' 0 Subst.empty (Eval.reduce_exp env (Subst.subst_exp s' e')) + +and parse_prods env tr str id as_ i = function + | [] -> unexpected tr str + | prod::[] when i = 0 -> + parse_prod env tr str as_ prod (* preserve error message *) + | prod::prods' -> + parse_prod env tr str as_ prod ||| lazy (parse_prods env tr str id as_ (i + 1) prods') + +and parse_gram env tr str id as_ = + Debug.(log "il.parse_gram" + (fun _ -> fmt "%s(%s) @ %s" (il_id id) (il_args as_) (il_text (rest str))) + il_results + ) @@ fun _ -> + (* TODO(4, rossberg): rethink evaluation to enforce this better *) + let as' = List.map (Eval.reduce_arg env) as_ in + if + List.exists (fun a -> + match a.it with + | ExpA e -> not (Eval.is_normal_exp e) + | _ -> false + ) as' + then + failure tr str "indeterminate argument values" + else + let _ps, _t, prods = Env.find_gram env id in + trace_parse (enter tr id as' Print.string_of_exp) str @@ fun tr' -> + parse_prods env tr' str id as' 0 prods + + +let rec parse_all = function + | Failure _ as r -> r + | Success (_, str, _, _, _) as r when eof str -> r + | Success (tr, str, _, _, tl) -> + let r = failure (alt tr None) str "end of input expected" in + trace_result r; + parse_all (Lazy.force tl) ||| lazy r + +exception Grammar_unknown + +let parse script name src = + let env = Env.env_of_script script in + let id = name $ no_region in + if not (Env.mem_gram env id) then raise Grammar_unknown else + match parse_all (parse_gram env empty_trace (stream src) id []) with + | Failure (_, str, msg) -> Error (pos str, msg) + | Success (_, _, _, e, _) when not !check_ambiguity -> Ok e + | Success (_, _, _, e, tl) -> + match Lazy.force tl with + | Failure _ -> Ok e + | Success _ -> Error (0, "ambiguous parse") diff --git a/spectec/src/il/parse.mli b/spectec/src/il/parse.mli new file mode 100644 index 0000000000..fdb05b1086 --- /dev/null +++ b/spectec/src/il/parse.mli @@ -0,0 +1,7 @@ +val trace : bool ref +val check_ambiguity : bool ref + +exception Grammar_unknown + +val parse : Ast.script -> string -> string -> (Ast.exp, int * string) result + (* raises Grammar_unknown *) diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index 483ca1ada3..76173a95de 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -5,22 +5,43 @@ open Ast (* Helpers *) -let concat = String.concat let prefix s f x = s ^ f x let space f x = " " ^ f x ^ " " +let string_of_list f sep xs = String.concat sep (List.map f xs) +let string_of_opt f = function None -> "-" | Some x -> f x -(* Identifiers *) -let is_alphanum = function - | '0'..'9' - | 'A'..'Z' - | 'a'..'z' - | '_' | '.' | '\'' -> true - | _ -> false +(* Strings *) + +let add_hex buf c = Printf.bprintf buf "\\%02X" (Char.code c) +let add_char buf = function + | '\n' -> Buffer.add_string buf "\\n" + | '\t' -> Buffer.add_string buf "\\t" + | '\"' -> Buffer.add_string buf "\\\"" + | '\\' -> Buffer.add_string buf "\\\\" + | c when '\x20' <= c && c < '\x7f' -> Buffer.add_char buf c + | c -> add_hex buf c + +let string_with add_char s = + let buf = Buffer.create 256 in + String.iter (add_char buf) s; + Buffer.contents buf + +let string_of_binary s = "\"" ^ string_with add_hex s ^ "\"" +let string_of_text s = "\"" ^ string_with add_char s ^ "\"" + +let string_of_string s = + if String.for_all (fun c -> '\x20' <= c && c < '\x7f') s then + string_of_text s + else + string_of_binary s + + +(* Identifiers *) let string_of_id id = - if String.for_all is_alphanum id.it + if String.for_all Lib.Char.is_alphanum_ascii id.it then id.it else "`" ^ id.it ^ "`" @@ -78,11 +99,11 @@ and string_of_numtyp t = and string_of_typ t = match t.it with - | VarT (id, as1) -> string_of_id id ^ string_of_args as1 + | VarT (id, as1) -> string_of_id id ^ string_of_args ~short:true as1 | BoolT -> "bool" | NumT t -> string_of_numtyp t | TextT -> "text" - | TupT ets -> "(" ^ concat ", " (List.map string_of_typbind ets) ^ ")" + | TupT ets -> "(" ^ string_of_list string_of_typbind ", " ets ^ ")" | IterT (t1, iter) -> string_of_typ t1 ^ string_of_iter iter and string_of_typ_name t = @@ -105,21 +126,21 @@ and string_of_deftyp layout dt = match dt.it with | AliasT t -> string_of_typ t | StructT tfs when layout = `H -> - "{" ^ concat ", " (List.map string_of_typfield tfs) ^ "}" + "{" ^ string_of_list string_of_typfield ", " tfs ^ "}" | StructT tfs -> - "\n{\n " ^ concat ",\n " (List.map string_of_typfield tfs) ^ "\n}" + "\n{\n " ^ string_of_list string_of_typfield ",\n " tfs ^ "\n}" | VariantT tcs when layout = `H -> - "| " ^ concat " | " (List.map string_of_typcase tcs) + "| " ^ string_of_list string_of_typcase " | " tcs | VariantT tcs -> - "\n | " ^ concat "\n | " (List.map string_of_typcase tcs) + "\n | " ^ string_of_list string_of_typcase "\n | " tcs and string_of_typfield (atom, (bs, t, prems), _hints) = string_of_mixop [[atom]] ^ string_of_binds bs ^ " " ^ string_of_typ t ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + string_of_list (prefix "\n -- " string_of_prem) "" prems and string_of_typcase (op, (bs, t, prems), _hints) = string_of_mixop op ^ string_of_binds bs ^ string_of_typ_args t ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + string_of_list (prefix "\n -- " string_of_prem) "" prems (* Expressions *) @@ -129,7 +150,7 @@ and string_of_exp e = | VarE id -> string_of_id id | BoolE b -> string_of_bool b | NatE n -> Z.to_string n - | TextE t -> "\"" ^ String.escaped t ^ "\"" + | TextE t -> string_of_string t | UnE (op, e2) -> string_of_unop op ^ " " ^ string_of_exp e2 | BinE (op, e1, e2) -> "(" ^ string_of_exp e1 ^ space string_of_binop op ^ string_of_exp e2 ^ ")" @@ -145,24 +166,28 @@ and string_of_exp e = | ExtE (e1, p, e2) -> string_of_exp e1 ^ "[" ^ string_of_path p ^ " =++ " ^ string_of_exp e2 ^ "]" - | StrE efs -> "{" ^ concat ", " (List.map string_of_expfield efs) ^ "}" + | StrE efs -> "{" ^ string_of_list string_of_expfield ", " efs ^ "}" | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_mixop [[atom]] ^ "_" ^ string_of_typ_name e1.note | CompE (e1, e2) -> string_of_exp e1 ^ " +++ " ^ string_of_exp e2 | MemE (e1, e2) -> string_of_exp e1 ^ " <- " ^ string_of_exp e2 | LenE e1 -> "|" ^ string_of_exp e1 ^ "|" - | TupE es -> "(" ^ string_of_exps ", " es ^ ")" - | CallE (id, as1) -> "$" ^ string_of_id id ^ string_of_args as1 + | TupE es -> "(" ^ string_of_list string_of_exp ", " es ^ ")" + | CallE (id, as1) -> "$" ^ string_of_id id ^ string_of_args ~short:true as1 | IterE (e1, iter) -> string_of_exp e1 ^ string_of_iterexp iter | ProjE (e1, i) -> string_of_exp e1 ^ "." ^ string_of_int i + | UncaseE (e1, [[]; []]) -> + string_of_exp e1 ^ "!" ^ string_of_typ_name e1.note | UncaseE (e1, op) -> string_of_exp e1 ^ "!" ^ string_of_mixop op ^ "_" ^ string_of_typ_name e1.note - | OptE eo -> "?(" ^ string_of_exps "" (Option.to_list eo) ^ ")" + | OptE eo -> "?(" ^ string_of_list string_of_exp "" (Option.to_list eo) ^ ")" | TheE e1 -> "!(" ^ string_of_exp e1 ^ ")" - | ListE es -> "[" ^ string_of_exps " " es ^ "]" + | ListE es -> "[" ^ string_of_list string_of_exp " " es ^ "]" | CatE (e1, e2) -> string_of_exp e1 ^ " ++ " ^ string_of_exp e2 + | CaseE ([[]; []], e1) -> string_of_typ_name e.note ^ string_of_exp_args e1 | CaseE (op, e1) -> string_of_mixop op ^ "_" ^ string_of_typ_name e.note ^ string_of_exp_args e1 + | SizeE id -> "||" ^ string_of_id id ^ "||" | SubE (e1, t1, t2) -> "(" ^ string_of_exp e1 ^ " : " ^ string_of_typ t1 ^ " <: " ^ string_of_typ t2 ^ ")" @@ -172,9 +197,6 @@ and string_of_exp_args e = | TupE _ | SubE _ | BinE _ | CmpE _ -> string_of_exp e | _ -> "(" ^ string_of_exp e ^ ")" -and string_of_exps sep es = - concat sep (List.map string_of_exp es) - and string_of_expfield (atom, e) = string_of_mixop [[atom]] ^ " " ^ string_of_exp e @@ -191,23 +213,30 @@ and string_of_path p = string_of_path p1 ^ "." ^ string_of_mixop [[atom]] ^ "_" ^ string_of_typ_name p1.note and string_of_iterexp (iter, xes) = - string_of_iter iter ^ "{" ^ String.concat ", " - (List.map (fun (id, e) -> string_of_id id ^ " <- " ^ string_of_exp e) xes) ^ "}" + string_of_iter iter ^ "{" ^ + string_of_list (fun (id, e) -> string_of_id id ^ "<-" ^ string_of_exp e) ", " xes + ^ "}" (* Grammars *) -and string_of_sym g = +and string_of_byte b = + Printf.sprintf "0x%02X" (Char.code b) + +and string_of_sym ?(short=false) g = match g.it with - | VarG (id, args) -> string_of_id id ^ string_of_args args - | NatG n -> Printf.sprintf "0x%02X" n - | TextG t -> "\"" ^ String.escaped t ^ "\"" + | VarG (id, args) -> string_of_id id ^ string_of_args ~short:true args + | NatG b -> string_of_byte b + | TextG t -> string_of_string t | EpsG -> "eps" - | SeqG gs -> "{" ^ concat " " (List.map string_of_sym gs) ^ "}" - | AltG gs -> "(" ^ concat " | " (List.map string_of_sym gs) ^ ")" - | RangeG (g1, g2) -> string_of_sym g1 ^ " | ... | " ^ string_of_sym g2 - | IterG (g1, iter) -> string_of_sym g1 ^ string_of_iterexp iter - | AttrG (e, g1) -> string_of_exp e ^ ":" ^ string_of_sym g1 + | SeqG gs -> "{" ^ string_of_list (string_of_sym ~short) " " gs ^ "}" + | AltG gs -> "(" ^ string_of_list (string_of_sym ~short) " | " gs ^ ")" + | RangeG (b1, b2) -> "(" ^ string_of_byte b1 ^ " | ... | " ^ string_of_byte b2 ^ ")" + | IterG (g1, (iter, _ as iterexp)) -> + string_of_sym ~short g1 ^ + (if short then string_of_iter iter else string_of_iterexp iterexp) + | AttrG (e, g1) -> + (if short then "" else string_of_exp e ^ ":") ^ string_of_sym ~short g1 (* Premises *) @@ -227,16 +256,16 @@ and string_of_prem prem = (* Definitions *) -and string_of_arg a = +and string_of_arg ?(short=false) a = match a.it with | ExpA e -> string_of_exp e - | TypA t -> "syntax " ^ string_of_typ t - | DefA id -> "def $" ^ string_of_id id - | GramA g -> "grammar " ^ string_of_sym g + | TypA t -> (if short then "" else "syntax ") ^ string_of_typ t + | DefA id -> (if short then "$" else "def $") ^ string_of_id id + | GramA g -> (if short then "" else "grammar ") ^ string_of_sym ~short g -and string_of_args = function +and string_of_args ?(short=false) = function | [] -> "" - | as_ -> "(" ^ concat ", " (List.map string_of_arg as_) ^ ")" + | as_ -> "(" ^ string_of_list (string_of_arg ~short) ", " as_ ^ ")" and string_of_bind bind = match bind.it with @@ -249,7 +278,7 @@ and string_of_bind bind = and string_of_binds = function | [] -> "" - | bs -> "{" ^ concat ", " (List.map string_of_bind bs) ^ "}" + | bs -> "{" ^ string_of_list string_of_bind ", " bs ^ "}" and string_of_param p = match p.it with @@ -264,7 +293,7 @@ and string_of_param p = and string_of_params = function | [] -> "" - | ps -> "(" ^ concat ", " (List.map string_of_param ps) ^ ")" + | ps -> "(" ^ string_of_list string_of_param ", " ps ^ ")" let region_comment ?(suppress_pos = false) indent at = if at = no_region then "" else @@ -285,7 +314,7 @@ let string_of_rule ?(suppress_pos = false) rule = "\n" ^ region_comment ~suppress_pos " " rule.at ^ " rule " ^ id' ^ string_of_binds bs ^ ":\n " ^ string_of_mixop mixop ^ string_of_exp_args e ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + string_of_list (prefix "\n -- " string_of_prem) "" prems let string_of_clause ?(suppress_pos = false) id clause = match clause.it with @@ -293,15 +322,15 @@ let string_of_clause ?(suppress_pos = false) id clause = "\n" ^ region_comment ~suppress_pos " " clause.at ^ " def $" ^ string_of_id id ^ string_of_binds bs ^ string_of_args as_ ^ " = " ^ string_of_exp e ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + string_of_list (prefix "\n -- " string_of_prem) "" prems let string_of_prod ?(suppress_pos = false) prod = match prod.it with - | ProdD (bs, g, e, prems) -> + | ProdD (bs, as_, g, e, prems) -> "\n" ^ region_comment ~suppress_pos " " prod.at ^ - " prod" ^ string_of_binds bs ^ " " ^ string_of_sym g ^ " => " ^ - string_of_exp e ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + " prod" ^ string_of_binds bs ^ string_of_args as_ ^ " " ^ + string_of_sym g ^ " => " ^ string_of_exp e ^ + string_of_list (prefix "\n -- " string_of_prem) "" prems let rec string_of_def ?(suppress_pos = false) d = let pre = "\n" ^ region_comment ~suppress_pos "" d.at in @@ -311,19 +340,19 @@ let rec string_of_def ?(suppress_pos = false) d = string_of_deftyp `V dt ^ "\n" | TypD (id, ps, insts) -> pre ^ "syntax " ^ string_of_id id ^ string_of_params ps ^ - concat "\n" (List.map (string_of_inst ~suppress_pos id) insts) ^ "\n" + string_of_list (string_of_inst ~suppress_pos id) "\n" insts ^ "\n" | RelD (id, mixop, t, rules) -> pre ^ "relation " ^ string_of_id id ^ ": " ^ string_of_mixop mixop ^ string_of_typ_args t ^ - concat "\n" (List.map (string_of_rule ~suppress_pos) rules) ^ "\n" + string_of_list (string_of_rule ~suppress_pos) "\n" rules ^ "\n" | DecD (id, ps, t, clauses) -> pre ^ "def $" ^ string_of_id id ^ string_of_params ps ^ " : " ^ string_of_typ t ^ - concat "" (List.map (string_of_clause ~suppress_pos id) clauses) ^ "\n" + string_of_list (string_of_clause ~suppress_pos id) "" clauses ^ "\n" | GramD (id, ps, t, prods) -> pre ^ "grammar " ^ string_of_id id ^ string_of_params ps ^ " : " ^ string_of_typ t ^ - concat "" (List.map (string_of_prod ~suppress_pos) prods) ^ "\n" + string_of_list (string_of_prod ~suppress_pos) "" prods ^ "\n" | RecD ds -> - pre ^ "rec {\n" ^ concat "" (List.map string_of_def ds) ^ "}" ^ "\n" + pre ^ "rec {\n" ^ string_of_list string_of_def "" ds ^ "}" ^ "\n" | HintD _ -> "" @@ -331,4 +360,4 @@ let rec string_of_def ?(suppress_pos = false) d = (* Scripts *) let string_of_script ?(suppress_pos = false) ds = - concat "" (List.map (string_of_def ~suppress_pos) ds) + string_of_list (string_of_def ~suppress_pos) "" ds diff --git a/spectec/src/il/print.mli b/spectec/src/il/print.mli index 08c9bf6e0e..e1026728bc 100644 --- a/spectec/src/il/print.mli +++ b/spectec/src/il/print.mli @@ -1,5 +1,12 @@ open Ast +val string_of_list : ('a -> string) -> string -> 'a list -> string +val string_of_opt : ('a -> string) -> 'a option -> string +val string_of_byte : char -> string +val string_of_text : string -> string +val string_of_binary : string -> string +val string_of_string : string -> string +val string_of_id : id -> string val string_of_atom : atom -> string val string_of_unop : unop -> string val string_of_binop : binop -> string @@ -9,9 +16,9 @@ val string_of_iter : iter -> string val string_of_typ : typ -> string val string_of_exp : exp -> string val string_of_path : path -> string -val string_of_sym : sym -> string +val string_of_sym : ?short:bool -> sym -> string val string_of_prem : prem -> string -val string_of_arg : arg -> string +val string_of_arg : ?short:bool -> arg -> string val string_of_bind : bind -> string val string_of_binds : bind list -> string val string_of_param : param -> string diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml index a39530a171..3761ef64b9 100644 --- a/spectec/src/il/subst.ml +++ b/spectec/src/il/subst.ml @@ -7,7 +7,13 @@ open Ast module Map = Map.Make(String) type subst = - {varid : exp Map.t; typid : typ Map.t; defid : id Map.t; gramid : sym Map.t} + { varid : exp Map.t; + typid : typ Map.t; + defid : id Map.t; + gramid : sym Map.t; + sizeid : int Map.t; + } + type t = subst let empty = @@ -15,33 +21,39 @@ let empty = typid = Map.empty; defid = Map.empty; gramid = Map.empty; + sizeid = Map.empty; } let mem_varid s id = Map.mem id.it s.varid let mem_typid s id = Map.mem id.it s.typid let mem_defid s id = Map.mem id.it s.defid let mem_gramid s id = Map.mem id.it s.gramid +let mem_sizeid s id = Map.mem id.it s.sizeid let find_varid s id = Map.find id.it s.varid let find_typid s id = Map.find id.it s.typid let find_defid s id = Map.find id.it s.defid let find_gramid s id = Map.find id.it s.gramid +let find_sizeid s id = Map.find id.it s.sizeid let add_varid s id e = if id.it = "_" then s else {s with varid = Map.add id.it e s.varid} let add_typid s id t = if id.it = "_" then s else {s with typid = Map.add id.it t s.typid} let add_defid s id x = if id.it = "_" then s else {s with defid = Map.add id.it x s.defid} let add_gramid s id g = if id.it = "_" then s else {s with gramid = Map.add id.it g s.gramid} +let add_sizeid s id g = if id.it = "_" then s else {s with sizeid = Map.add id.it g s.sizeid} let remove_varid s id = if id.it = "_" then s else {s with varid = Map.remove id.it s.varid} let remove_typid s id = if id.it = "_" then s else {s with typid = Map.remove id.it s.typid} let remove_defid s id = if id.it = "_" then s else {s with defid = Map.remove id.it s.defid} let remove_gramid s id = if id.it = "_" then s else {s with gramid = Map.remove id.it s.gramid} +let remove_sizeid s id = if id.it = "_" then s else {s with sizeid = Map.remove id.it s.sizeid} let union s1 s2 = { varid = Map.union (fun _ _e1 e2 -> Some e2) s1.varid s2.varid; typid = Map.union (fun _ _t1 t2 -> Some t2) s1.typid s2.typid; defid = Map.union (fun _ _x1 x2 -> Some x2) s1.defid s2.defid; gramid = Map.union (fun _ _x1 x2 -> Some x2) s1.gramid s2.gramid; + sizeid = Map.union (fun _ _x1 x2 -> Some x2) s1.sizeid s2.sizeid; } let remove_varid' s id' = {s with varid = Map.remove id' s.varid} @@ -68,7 +80,7 @@ let subst_varid s id = match Map.find_opt id.it s.varid with | None -> id | Some {it = VarE id'; _} -> id' - | Some _ -> raise (Invalid_argument "subst_varid") + | Some _ -> assert false let subst_defid s id = match Map.find_opt id.it s.defid with @@ -79,7 +91,11 @@ let subst_gramid s id = match Map.find_opt id.it s.gramid with | None -> id | Some {it = VarG (id', []); _} -> id' - | Some _ -> raise (Invalid_argument "subst_varid") + | Some g -> +Printf.printf "[subst] %s=%s\n%!" (Print.string_of_id id) (Print.string_of_sym g); assert false +(* + | Some _ -> assert false +*) (* Iterations *) @@ -120,11 +136,11 @@ and subst_deftyp s dt = and subst_typfield s (atom, (bs, t, prems), hints) = let bs', s' = subst_binds s bs in - (atom, (bs', subst_typ s' t, subst_list subst_prem s' prems), hints) + (atom, (bs', subst_typ s' t, subst_prems s' prems), hints) and subst_typcase s (op, (bs, t, prems), hints) = let bs', s' = subst_binds s bs in - (op, (bs', subst_typ s' t, subst_list subst_prem s' prems), hints) + (op, (bs', subst_typ s' t, subst_prems s' prems), hints) (* Expressions *) @@ -133,9 +149,9 @@ and subst_exp s e = (match e.it with | VarE id -> (match Map.find_opt id.it s.varid with - | None -> VarE id - | Some e' -> e'.it - ) + | None -> e + | Some e' -> e' + ).it | BoolE _ | NatE _ | TextE _ -> e.it | UnE (op, e1) -> UnE (op, subst_exp s e1) | BinE (op, e1, e2) -> BinE (op, subst_exp s e1, subst_exp s e2) @@ -161,6 +177,15 @@ and subst_exp s e = | ListE es -> ListE (subst_list subst_exp s es) | CatE (e1, e2) -> CatE (subst_exp s e1, subst_exp s e2) | CaseE (op, e1) -> CaseE (op, subst_exp s e1) + | SizeE id -> + (match Map.find_opt id.it s.sizeid with + | Some n -> NatE (Z.of_int n) + | None -> + match Map.find_opt id.it s.gramid with + | None -> SizeE id + | Some {it = VarG (id', _); _} -> SizeE id' + | Some _ -> assert false + ) | SubE (e1, t1, t2) -> SubE (subst_exp s e1, subst_typ s t1, subst_typ s t2) ) $$ e.at % subst_typ s e.note @@ -186,22 +211,36 @@ and subst_iterexp s (iter, xes) = and subst_sym s g = (match g.it with + | VarG (id, []) -> + (match Map.find_opt id.it s.gramid with + | Some g' -> g' + | None -> g + ).it | VarG (id, args) -> VarG (subst_gramid s id, List.map (subst_arg s) args) - | NatG _ | TextG _ -> g.it - | EpsG -> EpsG + | NatG _ | TextG _ | EpsG | RangeG _ -> g.it | SeqG gs -> SeqG (subst_list subst_sym s gs) | AltG gs -> AltG (subst_list subst_sym s gs) - | RangeG (g1, g2) -> RangeG (subst_sym s g1, subst_sym s g2) | IterG (g1, iterexp) -> let it', s' = subst_iterexp s iterexp in IterG (subst_sym s' g1, it') | AttrG (e, g1) -> AttrG (subst_exp s e, subst_sym s g1) - ) $ g.at + ) $$ g.at % subst_typ s g.note + +and subst_prod s prod = + (match prod.it with + | ProdD (bs, as_, g, e, prems) -> + let bs', s' = subst_binds s bs in + ProdD ( + bs', subst_args s' as_, + subst_sym s' g, subst_exp s' e, subst_prems s' prems + ) + ) $ prod.at (* Premises *) and subst_prem s prem = + Util.Debug_log.(log "il.subst_prem" (fun _ -> Print.string_of_prem prem) Print.string_of_prem) @@ fun _ -> (match prem.it with | RulePr (id, op, e) -> RulePr (id, op, subst_exp s e) | IfPr e -> IfPr (subst_exp s e) @@ -212,6 +251,8 @@ and subst_prem s prem = | LetPr (e1, e2, ids) -> LetPr (subst_exp s e1, subst_exp s e2, ids) ) $ prem.at +and subst_prems s prems = subst_list subst_prem s prems + (* Definitions *) @@ -256,4 +297,5 @@ let subst_typ s t = if s = empty then t else subst_typ s t let subst_deftyp s dt = if s = empty then dt else subst_deftyp s dt let subst_exp s e = if s = empty then e else subst_exp s e let subst_sym s g = if s = empty then g else subst_sym s g +let subst_prod s pr = if s = empty then pr else subst_prod s pr let subst_prem s pr = if s = empty then pr else subst_prem s pr diff --git a/spectec/src/il/subst.mli b/spectec/src/il/subst.mli index 37c98645be..3aba1a5124 100644 --- a/spectec/src/il/subst.mli +++ b/spectec/src/il/subst.mli @@ -2,7 +2,14 @@ open Ast module Map : Map.S with type key = string with type 'a t = 'a Map.Make(String).t -type subst = {varid : exp Map.t; typid : typ Map.t; defid : id Map.t; gramid : sym Map.t} +type subst = + { varid : exp Map.t; + typid : typ Map.t; + defid : id Map.t; + gramid : sym Map.t; + sizeid : int Map.t; + } + type t = subst val empty : subst @@ -12,26 +19,31 @@ val add_varid : subst -> id -> exp -> subst val add_typid : subst -> id -> typ -> subst val add_defid : subst -> id -> id -> subst val add_gramid : subst -> id -> sym -> subst +val add_sizeid : subst -> id -> int -> subst val remove_varid : subst -> id -> subst val remove_typid : subst -> id -> subst val remove_defid : subst -> id -> subst val remove_gramid : subst -> id -> subst +val remove_sizeid : subst -> id -> subst val find_varid : subst -> id -> exp val find_typid : subst -> id -> typ val find_defid : subst -> id -> id val find_gramid : subst -> id -> sym +val find_sizeid : subst -> id -> int val mem_varid : subst -> id -> bool val mem_typid : subst -> id -> bool val mem_defid : subst -> id -> bool val mem_gramid : subst -> id -> bool +val mem_sizeid : subst -> id -> bool val subst_typ : subst -> typ -> typ val subst_exp : subst -> exp -> exp val subst_path : subst -> path -> path val subst_sym : subst -> sym -> sym +val subst_prod : subst -> prod -> prod val subst_prem : subst -> prem -> prem val subst_arg : subst -> arg -> arg val subst_param : subst -> param -> param @@ -43,5 +55,6 @@ val subst_typbind : subst -> exp * typ -> exp * typ val subst_args : subst -> arg list -> arg list val subst_binds : subst -> bind list -> bind list * subst val subst_params : subst -> param list -> param list * subst +val subst_prems : subst -> prem list -> prem list val subst_list : (subst -> 'a -> 'a) -> subst -> 'a list -> 'a list diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml index e844e06a74..2f0f9aaf54 100644 --- a/spectec/src/il/valid.ml +++ b/spectec/src/il/valid.ml @@ -237,7 +237,7 @@ and infer_exp (env : Env.t) e : typ = match e.it with | VarE id -> Env.find_var env id | BoolE _ -> BoolT $ e.at - | NatE _ | LenE _ -> NumT NatT $ e.at + | NatE _ | LenE _ | SizeE _ -> NumT NatT $ e.at | TextE _ -> TextT $ e.at | UnE (op, _) -> let _t1, t' = infer_unop op in t' $ e.at | BinE (op, _, _) -> let _t1, _t2, t' = infer_binop op in t' $ e.at @@ -428,6 +428,10 @@ try let cases = as_variant_typ "case" env Check t e.at in let _binds, t1, _prems = find_case cases op e1.at in valid_exp ~side env e1 t1 + | SizeE id -> + let ps, _t', _prods = Env.find_gram env id in + if ps <> [] then + error e.at "parameterized grammar in size expression" | SubE (e1, t1, t2) -> valid_typ env t1; valid_typ env t2; @@ -511,10 +515,7 @@ and valid_sym env g : typ = let ps, t, _ = Env.find_gram env id in let s = valid_args env as_ ps Subst.empty g.at in Subst.subst_typ s t - | NatG n -> - if n < 0x00 || n > 0xff then - error g.at "byte value out of range"; - NumT NatT $ g.at + | NatG _ -> NumT NatT $ g.at | TextG _ -> TextT $ g.at | EpsG -> TupT [] $ g.at | SeqG gs -> @@ -522,16 +523,18 @@ and valid_sym env g : typ = TupT [] $ g.at | AltG gs -> let _ts = List.map (valid_sym env) gs in + if Free.(free_list free_sym gs).varid <> Free.Set.empty then + error g.at "variable occurrences in alternative grammar"; TupT [] $ g.at - | RangeG (g1, g2) -> - let t1 = valid_sym env g1 in - let t2 = valid_sym env g2 in - equiv_typ env t1 (NumT NatT $ g1.at) g.at; - equiv_typ env t2 (NumT NatT $ g2.at) g.at; - TupT [] $ g.at + | RangeG (b1, b2) -> + if b1 > b2 then + error g.at "inconsistent range bounds"; + NumT NatT $ g.at | IterG (g1, iterexp) -> let iter, env' = valid_iterexp ~side:`Lhs env iterexp g.at in let t1 = valid_sym env' g1 in + if (Free.free_sym g1).varid <> Free.Set.empty then + error g.at "variable occurrences in iteration grammar"; IterT (t1, iter) $ g.at | AttrG (e, g1) -> let t1 = valid_sym env g1 in @@ -681,11 +684,12 @@ let valid_prod envr ps t prod = (fun _ -> fmt ": (%s) -> %s" (il_params ps) (il_typ t)) ); match prod.it with - | ProdD (bs, g, e, prems) -> + | ProdD (bs, as_, g, e, prems) -> let envr' = local_env envr in List.iter (valid_bind envr') bs; + let s = valid_args !envr' as_ ps Subst.empty prod.at in let _t' = valid_sym !envr' g in - valid_exp !envr' e t; + valid_exp !envr' e (Subst.subst_typ s t); List.iter (valid_prem !envr') prems let infer_def envr d = diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml index 3954f7211d..ea458d68a8 100644 --- a/spectec/src/il2al/free.ml +++ b/spectec/src/il2al/free.ml @@ -19,7 +19,7 @@ let rec free_exp ignore_listN e = let fa = free_arg ignore_listN in match e.it with | VarE id -> free_varid id - | BoolE _ | NatE _ | TextE _ -> empty + | BoolE _ | NatE _ | TextE _ | SizeE _ -> empty | UnE (_, e1) | LenE e1 | TheE e1 | SubE (e1, _, _) | DotE (e1, _) | CaseE (_, e1) | ProjE (e1, _) | UncaseE (e1, _) -> f e1 diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml index 44ba777a42..f86a56212c 100644 --- a/spectec/src/il2al/il2il.ml +++ b/spectec/src/il2al/il2il.ml @@ -50,6 +50,7 @@ let rec transform_expr f e = | CatE (e1, e2) -> CatE (new_ e1, new_ e2) | MemE (e1, e2) -> MemE (new_ e1, new_ e2) | CaseE (mixop, e1) -> CaseE (mixop, new_ e1) + | SizeE g -> SizeE g | SubE (e1, _t1, t2) -> SubE (new_ e1, _t1, t2) in { e with it } diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml index a8100a1a2d..d065d7bef2 100644 --- a/spectec/src/middlend/sideconditions.ml +++ b/spectec/src/middlend/sideconditions.ml @@ -68,7 +68,7 @@ let rec t_exp env e : prem list = end @ (* And now descend *) match e.it with - | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None + | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None | SizeE _ -> [] | UnE (_, exp) | DotE (exp, _) diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index 5082971fbe..44a235968d 100644 --- a/spectec/src/middlend/sub.ml +++ b/spectec/src/middlend/sub.ml @@ -63,7 +63,7 @@ let arg_of_param param = | ExpP (id, t) -> ExpA (VarE id $$ param.at % t) $ param.at | TypP id -> TypA (VarT (id, []) $ param.at) $ param.at | DefP (id, _ps, _t) -> DefA id $ param.at - | GramP (id, _t) -> GramA (VarG (id, []) $ param.at) $ param.at + | GramP (id, t) -> GramA (VarG (id, []) $$ param.at % t) $ param.at let register_variant (env : env) (id : id) params (cases : typcase list) = if M.mem id.it env.typ then @@ -140,7 +140,7 @@ and t_typcase env (atom, (binds, t, prems), hints) = and t_exp2 env x = { x with it = t_exp' env x.it; note = t_typ env x.note } and t_exp' env = function - | (VarE _ | BoolE _ | NatE _ | TextE _) as e -> e + | (VarE _ | BoolE _ | NatE _ | TextE _ | SizeE _) as e -> e | UnE (unop, exp) -> UnE (unop, t_exp env exp) | BinE (binop, exp1, exp2) -> BinE (binop, t_exp env exp1, t_exp env exp2) | CmpE (cmpop, exp1, exp2) -> CmpE (cmpop, t_exp env exp1, t_exp env exp2) @@ -183,14 +183,13 @@ and t_path env x = { x with it = t_path' env x.it; note = t_typ env x.note } and t_sym' env = function | VarG (id, args) -> VarG (id, t_args env args) - | (NatG _ | TextG _ | EpsG) as g -> g + | (NatG _ | TextG _ | EpsG | RangeG _) as g -> g | SeqG syms -> SeqG (List.map (t_sym env) syms) | AltG syms -> AltG (List.map (t_sym env) syms) - | RangeG (sym1, sym2) -> RangeG (t_sym env sym1, t_sym env sym2) | IterG (sym, iter) -> IterG (t_sym env sym, t_iterexp env iter) | AttrG (e, sym) -> AttrG (t_exp env e, t_sym env sym) -and t_sym env x = { x with it = t_sym' env x.it } +and t_sym env x = { x with it = t_sym' env x.it; note = t_typ env x.note } and t_arg' env = function | ExpA exp -> ExpA (t_exp env exp) @@ -248,8 +247,8 @@ let t_inst env (inst : inst) = { inst with it = t_inst' env inst.it } let t_insts env = List.map (t_inst env) let t_prod' env = function - | ProdD (binds, lhs, rhs, prems) -> - ProdD (t_binds env binds, t_sym env lhs, t_exp env rhs, t_prems env prems) + | ProdD (binds, args, lhs, rhs, prems) -> + ProdD (t_binds env binds, t_args env args, t_sym env lhs, t_exp env rhs, t_prems env prems) let t_prod env (prod : prod) = { prod with it = t_prod' env prod.it } @@ -315,8 +314,9 @@ let rec rename_params s = function rename_params (Il.Subst.add_defid s id id') params | { it = GramP (id, t); at; _ } :: params -> let id' = (id.it ^ "_2") $ id.at in + let t' = Il.Subst.subst_typ s t in (GramP (id', t) $ at) :: - rename_params (Il.Subst.add_gramid s id (VarG (id', []) $ id.at)) params + rename_params (Il.Subst.add_gramid s id (VarG (id', []) $$ id.at % t')) params let insert_injections env (def : def) : def list = add_type_info env def; diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml index 8e8d62d543..d5fe2654cd 100644 --- a/spectec/src/middlend/totalize.ml +++ b/spectec/src/middlend/totalize.ml @@ -78,7 +78,7 @@ and t_typcase env (atom, (binds, t, prems), hints) = and t_exp2 env x = { x with it = t_exp' env x.it; note = t_typ env x.note } and t_exp' env = function - | (VarE _ | BoolE _ | NatE _ | TextE _) as e -> e + | (VarE _ | BoolE _ | NatE _ | TextE _ | SizeE _) as e -> e | UnE (unop, exp) -> UnE (unop, t_exp env exp) | BinE (binop, exp1, exp2) -> BinE (binop, t_exp env exp1, t_exp env exp2) | CmpE (cmpop, exp1, exp2) -> CmpE (cmpop, t_exp env exp1, t_exp env exp2) @@ -121,14 +121,13 @@ and t_path env x = { x with it = t_path' env x.it; note = t_typ env x.note } and t_sym' env = function | VarG (id, args) -> VarG (id, t_args env args) - | (NatG _ | TextG _ | EpsG) as g -> g + | (NatG _ | TextG _ | EpsG | RangeG _) as g -> g | SeqG syms -> SeqG (List.map (t_sym env) syms) | AltG syms -> AltG (List.map (t_sym env) syms) - | RangeG (sym1, sym2) -> RangeG (t_sym env sym1, t_sym env sym2) | IterG (sym, iter) -> IterG (t_sym env sym, t_iterexp env iter) | AttrG (e, sym) -> AttrG (t_exp env e, t_sym env sym) -and t_sym env x = { x with it = t_sym' env x.it } +and t_sym env x = { x with it = t_sym' env x.it; note = t_typ env x.note } and t_arg' env = function | ExpA exp -> ExpA (t_exp env exp) @@ -184,8 +183,8 @@ let t_inst env (inst : inst) = { inst with it = t_inst' env inst.it } let t_insts env = List.map (t_inst env) let t_prod' env = function - | ProdD (binds, lhs, rhs, prems) -> - ProdD (t_binds env binds, t_sym env lhs, t_exp env rhs, t_prems env prems) + | ProdD (binds, args, lhs, rhs, prems) -> + ProdD (t_binds env binds, t_args env args, t_sym env lhs, t_exp env rhs, t_prems env prems) let t_prod env (prod : prod) = { prod with it = t_prod' env prod.it } @@ -214,7 +213,7 @@ let rec t_def' env = function [ExpB (x, typI) $ x.at], ExpA (VarE x $$ no_region % typI) $ no_region | TypP id -> [], TypA (VarT (id, []) $ no_region) $ no_region | DefP (id, _, _) -> [], DefA id $ no_region - | GramP (id, _) -> [], GramA (VarG (id, []) $ no_region) $ no_region + | GramP (id, typI) -> [], GramA (VarG (id, []) $$ no_region % typI) $ no_region ) params' |> List.split in let catch_all = DefD (List.concat binds, args, OptE None $$ no_region % typ'', []) $ no_region in diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml index 900420f94b..bc533040c4 100644 --- a/spectec/src/middlend/unthe.ml +++ b/spectec/src/middlend/unthe.ml @@ -122,7 +122,7 @@ and t_epe n x k = ternary t_exp t_path t_exp n x k and t_exp' n e : eqns * exp' = match e with - | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None -> [], e + | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None | SizeE _ -> [], e | UnE (uo, exp) -> t_e n exp (fun exp' -> UnE (uo, exp')) | DotE (exp, a) -> t_e n exp (fun exp' -> DotE (exp', a)) diff --git a/spectec/src/middlend/wild.ml b/spectec/src/middlend/wild.ml index 6b26e900b9..c2472a5a90 100644 --- a/spectec/src/middlend/wild.ml +++ b/spectec/src/middlend/wild.ml @@ -139,7 +139,7 @@ and t_epe env x k = ternary t_exp t_path t_exp env x k and t_exp' env e : bind list * exp' = match e with - | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None -> [], e + | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None | SizeE _ -> [], e | UnE (uo, exp) -> t_e env exp (fun exp' -> UnE (uo, exp')) | DotE (exp, a) -> t_e env exp (fun exp' -> DotE (exp', a)) diff --git a/spectec/src/util/debug_log.ml b/spectec/src/util/debug_log.ml index b9e908733b..9d30cd3f78 100644 --- a/spectec/src/util/debug_log.ml +++ b/spectec/src/util/debug_log.ml @@ -1,15 +1,15 @@ (* List of actively logged functions' labels *) -let active : string list = [] +let active : string list ref = ref [] let fmt = Printf.sprintf let loc = Source.string_of_region let log_exn _exn = - if active <> [] then + if !active <> [] then Printf.eprintf "\n%s\n%!" (Printexc.get_backtrace ()) let log_at (type a) label at (arg_f : unit -> string) (res_f : a -> string) (f : unit -> a) : a = - if not (List.mem label active) then f () else + if not (List.mem label !active) then f () else let ats = if at = Source.no_region then "" else " " ^ Source.string_of_region at in let arg = arg_f () in Printf.eprintf "[%s%s] %s\n%!" label ats arg; @@ -32,11 +32,12 @@ let log_if label = log_if_at label Source.no_region module MySet = Set.Make(String) module MyMap = Map.Make(String) +let name s = if String.for_all Lib.Char.is_alphanum_ascii s then s else "`" ^ s ^ "`" let opt f xo = match xo with None -> "-" | Some x -> f x let seq f xs = String.concat " " (List.map f xs) let list f xs = String.concat ", " (List.map f xs) -let set s = seq Fun.id (MySet.elements s) -let mapping f m = seq (fun (x, y) -> x ^ "=" ^ f y) (MyMap.bindings m) +let set s = seq name (MySet.elements s) +let mapping f m = seq (fun (x, y) -> name x ^ "=" ^ f y) (MyMap.bindings m) let qline _ = "--------------------" let hline _ = "----------------------------------------" diff --git a/spectec/src/util/lib.ml b/spectec/src/util/lib.ml index c1199bb35d..367ac56cfd 100644 --- a/spectec/src/util/lib.ml +++ b/spectec/src/util/lib.ml @@ -56,6 +56,7 @@ struct let is_uppercase_ascii c = 'A' <= c && c <= 'Z' let is_lowercase_ascii c = 'a' <= c && c <= 'z' let is_letter_ascii c = is_uppercase_ascii c || is_lowercase_ascii c + let is_alphanum_ascii c = is_letter_ascii c || is_digit_ascii c || c = '_' end module String = diff --git a/spectec/src/util/lib.mli b/spectec/src/util/lib.mli index 0e781b34ac..bb081e00c2 100644 --- a/spectec/src/util/lib.mli +++ b/spectec/src/util/lib.mli @@ -21,6 +21,7 @@ sig val is_uppercase_ascii : char -> bool val is_lowercase_ascii : char -> bool val is_letter_ascii : char -> bool + val is_alphanum_ascii : char -> bool end module String : diff --git a/spectec/test-frontend/.gitignore b/spectec/test-frontend/.gitignore deleted file mode 100644 index a333a8b0a0..0000000000 --- a/spectec/test-frontend/.gitignore +++ /dev/null @@ -1 +0,0 @@ -_log diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index b3033e5a30..c6f0c3d415 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -6417,10 +6417,10 @@ rec { ;; A-binary.watsup:20.1-22.82 grammar BuN(N : N) : uN(N) ;; A-binary.watsup:21.5-21.83 - prod{n : n} `%`_byte(n):Bbyte => `%`_uN(n) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_uN(n) -- if ((n < (2 ^ 7)) /\ (n < (2 ^ N))) ;; A-binary.watsup:22.5-22.82 - prod{n : n, m : m} {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) + prod{n : n, m : m}(N) {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) -- if ((n >= (2 ^ 7)) /\ (N > 7)) } @@ -6432,29 +6432,29 @@ grammar Bu32 : u32 ;; A-binary.watsup grammar Blist(syntax el, grammar BX : el) : el* ;; A-binary.watsup - prod{n : n, el^n : el^n} {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} + prod{n : n, el^n : el^n}(syntax el, grammar BX) {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} ;; A-binary.watsup grammar BsN(N : N) : sN(N) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) -- if ((n < (2 ^ 6)) /\ (n < (2 ^ (N - 1)))) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) -- if ((((2 ^ 6) <= n) /\ (n < (2 ^ 7))) /\ (n >= ((2 ^ 7) - (2 ^ (N - 1))))) ;; A-binary.watsup - prod{n : n, i : nat} {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) + prod{n : n, i : nat}(N) {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) -- if ((n >= (2 ^ 7)) /\ (N > 7)) ;; A-binary.watsup grammar BiN(N : N) : iN(N) ;; A-binary.watsup - prod{i : nat} `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) + prod{i : nat}(N) `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) ;; A-binary.watsup grammar BfN(N : N) : fN(N) ;; A-binary.watsup - prod{b* : byte*} b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) + prod{b* : byte*}(N) b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) ;; A-binary.watsup grammar Bu64 : u64 @@ -7694,10 +7694,10 @@ grammar Bexpr : expr ;; A-binary.watsup grammar Bsection_(N : N, syntax en, grammar BX : en*) : en* ;; A-binary.watsup - prod{len : nat, en* : en*} {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} + prod{len : nat, en* : en*}(N, syntax en, grammar BX) {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} -- if (len = 0) ;; A-binary.watsup - prod eps => [] + prod(N, syntax en, grammar BX) eps => [] ;; A-binary.watsup grammar Bcustom : ()* @@ -8021,7 +8021,7 @@ def $var(syntax X) : nat ;; C-conventions.watsup grammar Bvar(syntax X) : () ;; C-conventions.watsup - prod 0x00 => () + prod(syntax X) 0x00 => () ;; C-conventions.watsup grammar Bsym : A diff --git a/spectec/test-interpreter/.gitignore b/spectec/test-interpreter/.gitignore deleted file mode 100644 index a333a8b0a0..0000000000 --- a/spectec/test-interpreter/.gitignore +++ /dev/null @@ -1 +0,0 @@ -_log diff --git a/spectec/test-middlend/.gitignore b/spectec/test-middlend/.gitignore deleted file mode 100644 index a333a8b0a0..0000000000 --- a/spectec/test-middlend/.gitignore +++ /dev/null @@ -1 +0,0 @@ -_log diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 061ca30504..502a9a8b8a 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -6407,10 +6407,10 @@ rec { ;; A-binary.watsup:20.1-22.82 grammar BuN(N : N) : uN(N) ;; A-binary.watsup:21.5-21.83 - prod{n : n} `%`_byte(n):Bbyte => `%`_uN(n) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_uN(n) -- if ((n < (2 ^ 7)) /\ (n < (2 ^ N))) ;; A-binary.watsup:22.5-22.82 - prod{n : n, m : m} {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) + prod{n : n, m : m}(N) {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) -- if ((n >= (2 ^ 7)) /\ (N > 7)) } @@ -6422,29 +6422,29 @@ grammar Bu32 : u32 ;; A-binary.watsup grammar Blist(syntax el, grammar BX : el) : el* ;; A-binary.watsup - prod{n : n, el^n : el^n} {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} + prod{n : n, el^n : el^n}(syntax el, grammar BX) {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} ;; A-binary.watsup grammar BsN(N : N) : sN(N) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) -- if ((n < (2 ^ 6)) /\ (n < (2 ^ (N - 1)))) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) -- if ((((2 ^ 6) <= n) /\ (n < (2 ^ 7))) /\ (n >= ((2 ^ 7) - (2 ^ (N - 1))))) ;; A-binary.watsup - prod{n : n, i : nat} {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) + prod{n : n, i : nat}(N) {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) -- if ((n >= (2 ^ 7)) /\ (N > 7)) ;; A-binary.watsup grammar BiN(N : N) : iN(N) ;; A-binary.watsup - prod{i : nat} `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) + prod{i : nat}(N) `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) ;; A-binary.watsup grammar BfN(N : N) : fN(N) ;; A-binary.watsup - prod{b* : byte*} b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) + prod{b* : byte*}(N) b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) ;; A-binary.watsup grammar Bu64 : u64 @@ -7684,10 +7684,10 @@ grammar Bexpr : expr ;; A-binary.watsup grammar Bsection_(N : N, syntax en, grammar BX : en*) : en* ;; A-binary.watsup - prod{len : nat, en* : en*} {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} + prod{len : nat, en* : en*}(N, syntax en, grammar BX) {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} -- if (len = 0) ;; A-binary.watsup - prod eps => [] + prod(N, syntax en, grammar BX) eps => [] ;; A-binary.watsup grammar Bcustom : ()* @@ -8011,7 +8011,7 @@ def $var(syntax X) : nat ;; C-conventions.watsup grammar Bvar(syntax X) : () ;; C-conventions.watsup - prod 0x00 => () + prod(syntax X) 0x00 => () ;; C-conventions.watsup grammar Bsym : A @@ -14430,10 +14430,10 @@ rec { ;; A-binary.watsup:20.1-22.82 grammar BuN(N : N) : uN(N) ;; A-binary.watsup:21.5-21.83 - prod{n : n} `%`_byte(n):Bbyte => `%`_uN(n) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_uN(n) -- if ((n < (2 ^ 7)) /\ (n < (2 ^ N))) ;; A-binary.watsup:22.5-22.82 - prod{n : n, m : m} {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) + prod{n : n, m : m}(N) {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) -- if ((n >= (2 ^ 7)) /\ (N > 7)) } @@ -14445,29 +14445,29 @@ grammar Bu32 : u32 ;; A-binary.watsup grammar Blist(syntax el, grammar BX : el) : el* ;; A-binary.watsup - prod{n : n, el^n : el^n} {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} + prod{n : n, el^n : el^n}(syntax el, grammar BX) {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} ;; A-binary.watsup grammar BsN(N : N) : sN(N) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) -- if ((n < (2 ^ 6)) /\ (n < (2 ^ (N - 1)))) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) -- if ((((2 ^ 6) <= n) /\ (n < (2 ^ 7))) /\ (n >= ((2 ^ 7) - (2 ^ (N - 1))))) ;; A-binary.watsup - prod{n : n, i : nat} {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) + prod{n : n, i : nat}(N) {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) -- if ((n >= (2 ^ 7)) /\ (N > 7)) ;; A-binary.watsup grammar BiN(N : N) : iN(N) ;; A-binary.watsup - prod{i : nat} `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) + prod{i : nat}(N) `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) ;; A-binary.watsup grammar BfN(N : N) : fN(N) ;; A-binary.watsup - prod{b* : byte*} b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) + prod{b* : byte*}(N) b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) ;; A-binary.watsup grammar Bu64 : u64 @@ -15707,10 +15707,10 @@ grammar Bexpr : expr ;; A-binary.watsup grammar Bsection_(N : N, syntax en, grammar BX : en*) : en* ;; A-binary.watsup - prod{len : nat, en* : en*} {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} + prod{len : nat, en* : en*}(N, syntax en, grammar BX) {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} -- if (len = 0) ;; A-binary.watsup - prod eps => [] + prod(N, syntax en, grammar BX) eps => [] ;; A-binary.watsup grammar Bcustom : ()* @@ -16034,7 +16034,7 @@ def $var(syntax X) : nat ;; C-conventions.watsup grammar Bvar(syntax X) : () ;; C-conventions.watsup - prod 0x00 => () + prod(syntax X) 0x00 => () ;; C-conventions.watsup grammar Bsym : A @@ -22453,10 +22453,10 @@ rec { ;; A-binary.watsup:20.1-22.82 grammar BuN(N : N) : uN(N) ;; A-binary.watsup:21.5-21.83 - prod{n : n} `%`_byte(n):Bbyte => `%`_uN(n) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_uN(n) -- if ((n < (2 ^ 7)) /\ (n < (2 ^ N))) ;; A-binary.watsup:22.5-22.82 - prod{n : n, m : m} {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) + prod{n : n, m : m}(N) {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) -- if ((n >= (2 ^ 7)) /\ (N > 7)) } @@ -22468,29 +22468,29 @@ grammar Bu32 : u32 ;; A-binary.watsup grammar Blist(syntax el, grammar BX : el) : el* ;; A-binary.watsup - prod{n : n, el^n : el^n} {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} + prod{n : n, el^n : el^n}(syntax el, grammar BX) {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} ;; A-binary.watsup grammar BsN(N : N) : sN(N) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) -- if ((n < (2 ^ 6)) /\ (n < (2 ^ (N - 1)))) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) -- if ((((2 ^ 6) <= n) /\ (n < (2 ^ 7))) /\ (n >= ((2 ^ 7) - (2 ^ (N - 1))))) ;; A-binary.watsup - prod{n : n, i : nat} {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) + prod{n : n, i : nat}(N) {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) -- if ((n >= (2 ^ 7)) /\ (N > 7)) ;; A-binary.watsup grammar BiN(N : N) : iN(N) ;; A-binary.watsup - prod{i : nat} `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) + prod{i : nat}(N) `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) ;; A-binary.watsup grammar BfN(N : N) : fN(N) ;; A-binary.watsup - prod{b* : byte*} b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) + prod{b* : byte*}(N) b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) ;; A-binary.watsup grammar Bu64 : u64 @@ -23730,10 +23730,10 @@ grammar Bexpr : expr ;; A-binary.watsup grammar Bsection_(N : N, syntax en, grammar BX : en*) : en* ;; A-binary.watsup - prod{len : nat, en* : en*} {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} + prod{len : nat, en* : en*}(N, syntax en, grammar BX) {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} -- if (len = 0) ;; A-binary.watsup - prod eps => [] + prod(N, syntax en, grammar BX) eps => [] ;; A-binary.watsup grammar Bcustom : ()* @@ -24057,7 +24057,7 @@ def $var(syntax X) : nat ;; C-conventions.watsup grammar Bvar(syntax X) : () ;; C-conventions.watsup - prod 0x00 => () + prod(syntax X) 0x00 => () ;; C-conventions.watsup grammar Bsym : A @@ -30653,10 +30653,10 @@ rec { ;; A-binary.watsup:20.1-22.82 grammar BuN(N : N) : uN(N) ;; A-binary.watsup:21.5-21.83 - prod{n : n} `%`_byte(n):Bbyte => `%`_uN(n) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_uN(n) -- if ((n < (2 ^ 7)) /\ (n < (2 ^ N))) ;; A-binary.watsup:22.5-22.82 - prod{n : n, m : m} {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) + prod{n : n, m : m}(N) {`%`_byte(n):Bbyte `%`_uN(m):BuN((N - 7))} => `%`_uN((((2 ^ 7) * m) + (n - (2 ^ 7)))) -- if ((n >= (2 ^ 7)) /\ (N > 7)) } @@ -30668,29 +30668,29 @@ grammar Bu32 : u32 ;; A-binary.watsup grammar Blist(syntax el, grammar BX : el) : el* ;; A-binary.watsup - prod{n : n, el^n : el^n} {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} + prod{n : n, el^n : el^n}(syntax el, grammar BX) {`%`_u32(n):Bu32 el:BX^n{el : el}} => el^n{el : el} ;; A-binary.watsup grammar BsN(N : N) : sN(N) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN((n : n <: int)) -- if ((n < (2 ^ 6)) /\ (n < (2 ^ (N - 1)))) ;; A-binary.watsup - prod{n : n} `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) + prod{n : n}(N) `%`_byte(n):Bbyte => `%`_sN(((n - (2 ^ 7)) : nat <: int)) -- if ((((2 ^ 6) <= n) /\ (n < (2 ^ 7))) /\ (n >= ((2 ^ 7) - (2 ^ (N - 1))))) ;; A-binary.watsup - prod{n : n, i : nat} {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) + prod{n : n, i : nat}(N) {`%`_byte(n):Bbyte `%`_uN(i):BuN((N - 7))} => `%`_sN(((((2 ^ 7) * i) + (n - (2 ^ 7))) : nat <: int)) -- if ((n >= (2 ^ 7)) /\ (N > 7)) ;; A-binary.watsup grammar BiN(N : N) : iN(N) ;; A-binary.watsup - prod{i : nat} `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) + prod{i : nat}(N) `%`_sN((i : nat <: int)):BsN(N) => `%`_iN($invsigned_(N, (i : nat <: int))) ;; A-binary.watsup grammar BfN(N : N) : fN(N) ;; A-binary.watsup - prod{b* : byte*} b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) + prod{b* : byte*}(N) b*{b : byte}:Bbyte^(N / 8){} => $invfbytes_(N, b*{b : byte}) ;; A-binary.watsup grammar Bu64 : u64 @@ -31930,10 +31930,10 @@ grammar Bexpr : expr ;; A-binary.watsup grammar Bsection_(N : N, syntax en, grammar BX : en*) : en* ;; A-binary.watsup - prod{len : nat, en* : en*} {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} + prod{len : nat, en* : en*}(N, syntax en, grammar BX) {`%`_byte(N):Bbyte `%`_u32(len):Bu32 en*{en : en}:BX} => en*{en : en} -- if (len = 0) ;; A-binary.watsup - prod eps => [] + prod(N, syntax en, grammar BX) eps => [] ;; A-binary.watsup grammar Bcustom : ()* @@ -32258,7 +32258,7 @@ def $var(syntax X) : nat ;; C-conventions.watsup grammar Bvar(syntax X) : () ;; C-conventions.watsup - prod 0x00 => () + prod(syntax X) 0x00 => () ;; C-conventions.watsup grammar Bsym : A diff --git a/spectec/test-parser/Makefile b/spectec/test-parser/Makefile new file mode 100644 index 0000000000..89cd7e43e8 --- /dev/null +++ b/spectec/test-parser/Makefile @@ -0,0 +1,51 @@ +# Configuration + +NAME = watsup +EXE = $(PWD)/../$(NAME) +EXT = $(NAME) +LOG = _log + +OWNDIR = $(PWD) +SPECDIR = ../spec +SPECFILES = $(shell cd $(SPECDIR) && ls -d wasm-*) +TESTFILES = $(shell ls *.$(EXT)) +SPECS = $(SPECFILES:%=test-%) +TESTS = $(TESTFILES:%.$(EXT)=test-%) + + +# Main targets + +.PHONY: all + +all: test + + +# Test + +.PHONY: test $(SPECS) $(TESTS) + +test: $(TESTS) + +$(SPECS): test-%: $(EXE) + (cd $(SPECDIR)/$* && $(EXE) -l *.$(EXT)) + +$(TESTS): test-%: %.$(EXT) $(EXE) + ($(EXE) -l $<) + + +# Executable + +$(EXE): exe + +exe: + @(cd ..; make exe) + + +# Cleanup + +.PHONY: clean distclean + +clean: + rm -f $(LOG) + +distclean: clean diff --git a/spectec/test-parser/TEST.md b/spectec/test-parser/TEST.md new file mode 100644 index 0000000000..007b0556ba --- /dev/null +++ b/spectec/test-parser/TEST.md @@ -0,0 +1,1767 @@ +# Parser constructs + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Teps "" +Teps @ "" +Teps ::= eps @ "" +Teps ::= eps => 42 @ "" +Teps => 42 @ "" +42 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Teps "\00" +Teps @ "\00" +Teps ::= eps @ "\00" +Teps ::= eps => 42 @ "\00" +Teps => 42 @ "\00" +Teps => fail: end of input expected @ "\00" +0: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tbyte "\3A" +Tbyte @ ":" +Tbyte ::= 0x3A @ ":" +Tbyte ::= 0x3A => 58 @ "" +Tbyte => 58 @ "" +58 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tbyte "\33" +Tbyte @ "3" +Tbyte ::= 0x3A @ "3" +Tbyte ::= 0x3A => fail: byte 0x3A expected @ "3" +Tbyte => fail: byte 0x3A expected @ "3" +0: byte 0x3A expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tbyte "" +Tbyte @ "" +Tbyte ::= 0x3A @ "" +Tbyte ::= 0x3A => fail: unexpected end of input @ "" +Tbyte => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tbyte "\3A\00" +Tbyte @ "\3A\00" +Tbyte ::= 0x3A @ "\3A\00" +Tbyte ::= 0x3A => 58 @ "\00" +Tbyte => 58 @ "\00" +Tbyte => fail: end of input expected @ "\00" +1: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "AÄÜ" +Ttext @ "\41\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" @ "\41\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" => () @ "" +Ttext => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "AÄ\c3\9c" +Ttext @ "\41\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" @ "\41\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" => () @ "" +Ttext => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "BÄ\c3\9c" +Ttext @ "\42\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" @ "\42\C3\84\C3\9C" +Ttext ::= "\41\C3\84\C3\9C" => fail: text "\41\C3\84\C3\9... @ "\42\C3\84\C3\9C" +Ttext => fail: text "\41\C3\84\C3\9... @ "\42\C3\84\C3\9C" +0: text "\41\C3\84\C3\9C" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "AÄ\c3\9d" +Ttext @ "\41\C3\84\C3\9D" +Ttext ::= "\41\C3\84\C3\9C" @ "\41\C3\84\C3\9D" +Ttext ::= "\41\C3\84\C3\9C" => fail: text "\41\C3\84\C3\9... @ "\41\C3\84\C3\9D" +Ttext => fail: text "\41\C3\84\C3\9... @ "\41\C3\84\C3\9D" +0: text "\41\C3\84\C3\9C" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "" +Ttext @ "" +Ttext ::= "\41\C3\84\C3\9C" @ "" +Ttext ::= "\41\C3\84\C3\9C" => fail: unexpected end of input @ "" +Ttext => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Ttext "AÄ\c3" +Ttext @ "\41\C3\84\C3" +Ttext ::= "\41\C3\84\C3\9C" @ "\41\C3\84\C3" +Ttext ::= "\41\C3\84\C3\9C" => fail: text "\41\C3\84\C3\9... @ "\41\C3\84\C3" +Ttext => fail: text "\41\C3\84\C3\9... @ "\41\C3\84\C3" +0: text "\41\C3\84\C3\9C" expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bseq "\03\04\02" +Bseq @ "\03\04\02" +Bseq ::= 0x03 0x04 eps 0x02 @ "\03\04\02" +Bseq ::= 0x03 0x04 eps 0x02 => 11 @ "" +Bseq => 11 @ "" +11 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bseq "\02\04\02" +Bseq @ "\02\04\02" +Bseq ::= 0x03 0x04 eps 0x02 @ "\02\04\02" +Bseq ::= 0x03 0x04 eps 0x02 => fail: byte 0x03 expected @ "\02\04\02" +Bseq => fail: byte 0x03 expected @ "\02\04\02" +0: byte 0x03 expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bseq "\03\02\02" +Bseq @ "\03\02\02" +Bseq ::= 0x03 0x04 eps 0x02 @ "\03\02\02" +Bseq ::= 0x03 0x04 eps 0x02 => fail: byte 0x04 expected @ "\02\02" +Bseq => fail: byte 0x04 expected @ "\02\02" +1: byte 0x04 expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bseq "\03\04" +Bseq @ "\03\04" +Bseq ::= 0x03 0x04 eps 0x02 @ "\03\04" +Bseq ::= 0x03 0x04 eps 0x02 => fail: unexpected end of input @ "" +Bseq => fail: unexpected end of input @ "" +2: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bseq "\03\04\02\00" +Bseq @ "\03\04\02\00" +Bseq ::= 0x03 0x04 eps 0x02 @ "\03\04\02\00" +Bseq ::= 0x03 0x04 eps 0x02 => 11 @ "\00" +Bseq => 11 @ "\00" +Bseq => fail: end of input expected @ "\00" +3: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "ABCD" +Tseq @ "ABCD" +Tseq ::= eps "A" eps "BC" "D" @ "ABCD" +Tseq ::= eps "A" eps "BC" "D" => () @ "" +Tseq => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "BCDA" +Tseq @ "BCDA" +Tseq ::= eps "A" eps "BC" "D" @ "BCDA" +Tseq ::= eps "A" eps "BC" "D" => fail: text "A" expected @ "BCDA" +Tseq => fail: text "A" expected @ "BCDA" +0: text "A" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "ABCE" +Tseq @ "ABCE" +Tseq ::= eps "A" eps "BC" "D" @ "ABCE" +Tseq ::= eps "A" eps "BC" "D" => fail: text "D" expected @ "E" +Tseq => fail: text "D" expected @ "E" +3: text "D" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "ACCD" +Tseq @ "ACCD" +Tseq ::= eps "A" eps "BC" "D" @ "ACCD" +Tseq ::= eps "A" eps "BC" "D" => fail: text "BC" expected @ "CCD" +Tseq => fail: text "BC" expected @ "CCD" +1: text "BC" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "ABC" +Tseq @ "ABC" +Tseq ::= eps "A" eps "BC" "D" @ "ABC" +Tseq ::= eps "A" eps "BC" "D" => fail: unexpected end of input @ "" +Tseq => fail: unexpected end of input @ "" +3: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tseq "ABCDE" +Tseq @ "ABCDE" +Tseq ::= eps "A" eps "BC" "D" @ "ABCDE" +Tseq ::= eps "A" eps "BC" "D" => () @ "E" +Tseq => () @ "E" +Tseq => fail: end of input expected @ "E" +4: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "A" +Talt @ "A" +Talt ::= "A"|"BC"|"D" @ "A" +Talt/(_|...|_) @ "A" +Talt/(_|...|_) ::= "A" @ "A" +Talt/(_|...|_) ::= "A" => "A" @ "" +Talt/(_|...|_) => "A" @ "" +Talt ::= "A"|"BC"|"D" => () @ "" +Talt => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "BC" +Talt @ "BC" +Talt ::= "A"|"BC"|"D" @ "BC" +Talt/(_|...|_) @ "BC" +Talt/(_|...|_) ::= "A" @ "BC" +Talt/(_|...|_) ::= "A" => fail: text "A" expected @ "BC" +Talt/(_|...|_) ::= "BC" @ "BC" +Talt/(_|...|_) ::= "BC" => "BC" @ "" +Talt/(_|...|_) => "BC" @ "" +Talt ::= "A"|"BC"|"D" => () @ "" +Talt => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "D" +Talt @ "D" +Talt ::= "A"|"BC"|"D" @ "D" +Talt/(_|...|_) @ "D" +Talt/(_|...|_) ::= "A" @ "D" +Talt/(_|...|_) ::= "A" => fail: text "A" expected @ "D" +Talt/(_|...|_) ::= "BC" @ "D" +Talt/(_|...|_) ::= "BC" => fail: text "BC" expected @ "D" +Talt/(_|...|_) ::= "D" @ "D" +Talt/(_|...|_) ::= "D" => "D" @ "" +Talt/(_|...|_) => "D" @ "" +Talt ::= "A"|"BC"|"D" => () @ "" +Talt => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "ABC" +Talt @ "ABC" +Talt ::= "A"|"BC"|"D" @ "ABC" +Talt/(_|...|_) @ "ABC" +Talt/(_|...|_) ::= "A" @ "ABC" +Talt/(_|...|_) ::= "A" => "A" @ "BC" +Talt/(_|...|_) => "A" @ "BC" +Talt ::= "A"|"BC"|"D" => () @ "BC" +Talt => () @ "BC" +Talt => fail: end of input expected @ "BC" +Talt/(_|...|_) ::= "BC" @ "ABC" +Talt/(_|...|_) ::= "BC" => fail: text "BC" expected @ "ABC" +Talt/(_|...|_) ::= "D" @ "ABC" +Talt/(_|...|_) ::= "D" => fail: text "D" expected @ "ABC" +Talt/(_|...|_) => fail: unexpected input @ "ABC" +Talt ::= "A"|"BC"|"D" => fail: unexpected input @ "ABC" +Talt => fail: unexpected input @ "ABC" +1: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "" +Talt @ "" +Talt ::= "A"|"BC"|"D" @ "" +Talt/(_|...|_) @ "" +Talt/(_|...|_) ::= "A" @ "" +Talt/(_|...|_) ::= "A" => fail: unexpected end of input @ "" +Talt/(_|...|_) ::= "BC" @ "" +Talt/(_|...|_) ::= "BC" => fail: unexpected end of input @ "" +Talt/(_|...|_) ::= "D" @ "" +Talt/(_|...|_) ::= "D" => fail: unexpected end of input @ "" +Talt/(_|...|_) => fail: unexpected end of input @ "" +Talt ::= "A"|"BC"|"D" => fail: unexpected end of input @ "" +Talt => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "C" +Talt @ "C" +Talt ::= "A"|"BC"|"D" @ "C" +Talt/(_|...|_) @ "C" +Talt/(_|...|_) ::= "A" @ "C" +Talt/(_|...|_) ::= "A" => fail: text "A" expected @ "C" +Talt/(_|...|_) ::= "BC" @ "C" +Talt/(_|...|_) ::= "BC" => fail: text "BC" expected @ "C" +Talt/(_|...|_) ::= "D" @ "C" +Talt/(_|...|_) ::= "D" => fail: text "D" expected @ "C" +Talt/(_|...|_) => fail: unexpected input @ "C" +Talt ::= "A"|"BC"|"D" => fail: unexpected input @ "C" +Talt => fail: unexpected input @ "C" +0: unexpected input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt "B" +Talt @ "B" +Talt ::= "A"|"BC"|"D" @ "B" +Talt/(_|...|_) @ "B" +Talt/(_|...|_) ::= "A" @ "B" +Talt/(_|...|_) ::= "A" => fail: text "A" expected @ "B" +Talt/(_|...|_) ::= "BC" @ "B" +Talt/(_|...|_) ::= "BC" => fail: text "BC" expected @ "B" +Talt/(_|...|_) ::= "D" @ "B" +Talt/(_|...|_) ::= "D" => fail: text "D" expected @ "B" +Talt/(_|...|_) => fail: unexpected input @ "B" +Talt ::= "A"|"BC"|"D" => fail: unexpected input @ "B" +Talt => fail: unexpected input @ "B" +0: unexpected input +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt2 "" +Talt2 @ "" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" @ "" +Talt2/(_|...|_) @ "" +Talt2/(_|...|_) ::= "A" @ "" +Talt2/(_|...|_) ::= "A" => fail: unexpected end of input @ "" +Talt2/(_|...|_) ::= "B" @ "" +Talt2/(_|...|_) ::= "B" => fail: unexpected end of input @ "" +Talt2/(_|...|_) ::= "BC" @ "" +Talt2/(_|...|_) ::= "BC" => fail: unexpected end of input @ "" +Talt2/(_|...|_) ::= "A" @ "" +Talt2/(_|...|_) ::= "A" => fail: unexpected end of input @ "" +Talt2/(_|...|_) ::= "DE" @ "" +Talt2/(_|...|_) ::= "DE" => fail: unexpected end of input @ "" +Talt2/(_|...|_) ::= "" @ "" +Talt2/(_|...|_) ::= "" => "" @ "" +Talt2/(_|...|_) => "" @ "" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "" +Talt2 => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt2 "BC" +Talt2 @ "BC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" @ "BC" +Talt2/(_|...|_) @ "BC" +Talt2/(_|...|_) ::= "A" @ "BC" +Talt2/(_|...|_) ::= "A" => fail: text "A" expected @ "BC" +Talt2/(_|...|_) ::= "B" @ "BC" +Talt2/(_|...|_) ::= "B" => "B" @ "C" +Talt2/(_|...|_) => "B" @ "C" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "C" +Talt2 => () @ "C" +Talt2 => fail: end of input expected @ "C" +Talt2/(_|...|_) ::= "BC" @ "BC" +Talt2/(_|...|_) ::= "BC" => "BC" @ "" +Talt2/(_|...|_) => "BC" @ "" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "" +Talt2 => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt2 "D" +Talt2 @ "D" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" @ "D" +Talt2/(_|...|_) @ "D" +Talt2/(_|...|_) ::= "A" @ "D" +Talt2/(_|...|_) ::= "A" => fail: text "A" expected @ "D" +Talt2/(_|...|_) ::= "B" @ "D" +Talt2/(_|...|_) ::= "B" => fail: text "B" expected @ "D" +Talt2/(_|...|_) ::= "BC" @ "D" +Talt2/(_|...|_) ::= "BC" => fail: text "BC" expected @ "D" +Talt2/(_|...|_) ::= "A" @ "D" +Talt2/(_|...|_) ::= "A" => fail: text "A" expected @ "D" +Talt2/(_|...|_) ::= "DE" @ "D" +Talt2/(_|...|_) ::= "DE" => fail: text "DE" expected @ "D" +Talt2/(_|...|_) ::= "" @ "D" +Talt2/(_|...|_) ::= "" => "" @ "D" +Talt2/(_|...|_) => "" @ "D" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "D" +Talt2 => () @ "D" +Talt2 => fail: end of input expected @ "D" +Talt2/(_|...|_) => fail: unexpected input @ "D" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => fail: unexpected input @ "D" +Talt2 => fail: unexpected input @ "D" +0: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Talt2 "ABC" +Talt2 @ "ABC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" @ "ABC" +Talt2/(_|...|_) @ "ABC" +Talt2/(_|...|_) ::= "A" @ "ABC" +Talt2/(_|...|_) ::= "A" => "A" @ "BC" +Talt2/(_|...|_) => "A" @ "BC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "BC" +Talt2 => () @ "BC" +Talt2 => fail: end of input expected @ "BC" +Talt2/(_|...|_) ::= "B" @ "ABC" +Talt2/(_|...|_) ::= "B" => fail: text "B" expected @ "ABC" +Talt2/(_|...|_) ::= "BC" @ "ABC" +Talt2/(_|...|_) ::= "BC" => fail: text "BC" expected @ "ABC" +Talt2/(_|...|_) ::= "A" @ "ABC" +Talt2/(_|...|_) ::= "A" => "A" @ "BC" +Talt2/(_|...|_) => "A" @ "BC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "BC" +Talt2 => () @ "BC" +Talt2 => fail: end of input expected @ "BC" +Talt2/(_|...|_) ::= "DE" @ "ABC" +Talt2/(_|...|_) ::= "DE" => fail: text "DE" expected @ "ABC" +Talt2/(_|...|_) ::= "" @ "ABC" +Talt2/(_|...|_) ::= "" => "" @ "ABC" +Talt2/(_|...|_) => "" @ "ABC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => () @ "ABC" +Talt2 => () @ "ABC" +Talt2 => fail: end of input expected @ "ABC" +Talt2/(_|...|_) => fail: unexpected input @ "ABC" +Talt2 ::= "A"|"B"|"BC"|"A"|"DE"|"" => fail: unexpected input @ "ABC" +Talt2 => fail: unexpected input @ "ABC" +1: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tprod "A" +Tprod @ "A" +Tprod ::= "A" @ "A" +Tprod ::= "A" => 1 @ "" +Tprod => 1 @ "" +1 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tprod "BC" +Tprod @ "BC" +Tprod ::= "A" @ "BC" +Tprod ::= "A" => fail: text "A" expected @ "BC" +Tprod ::= "BC" @ "BC" +Tprod ::= "BC" => 2 @ "" +Tprod => 2 @ "" +2 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tprod "D" +Tprod @ "D" +Tprod ::= "A" @ "D" +Tprod ::= "A" => fail: text "A" expected @ "D" +Tprod ::= "BC" @ "D" +Tprod ::= "BC" => fail: text "BC" expected @ "D" +Tprod ::= "D" @ "D" +Tprod ::= "D" => 3 @ "" +Tprod => 3 @ "" +3 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tprod "ABC" +Tprod @ "ABC" +Tprod ::= "A" @ "ABC" +Tprod ::= "A" => 1 @ "BC" +Tprod => 1 @ "BC" +Tprod => fail: end of input expected @ "BC" +Tprod ::= "BC" @ "ABC" +Tprod ::= "BC" => fail: text "BC" expected @ "ABC" +Tprod ::= "D" @ "ABC" +Tprod ::= "D" => fail: text "D" expected @ "ABC" +Tprod ::= "" @ "ABC" +Tprod ::= "" => 0 @ "ABC" +Tprod => 0 @ "ABC" +Tprod => fail: end of input expected @ "ABC" +Tprod => fail: unexpected input @ "ABC" +1: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tprod "" +Tprod @ "" +Tprod ::= "A" @ "" +Tprod ::= "A" => fail: unexpected end of input @ "" +Tprod ::= "BC" @ "" +Tprod ::= "BC" => fail: unexpected end of input @ "" +Tprod ::= "D" @ "" +Tprod ::= "D" => fail: unexpected end of input @ "" +Tprod ::= "" @ "" +Tprod ::= "" => 0 @ "" +Tprod => 0 @ "" +0 +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "\10" +Brng @ "\10" +Brng ::= 0x10|...|0x20 @ "\10" +Brng ::= 0x10|...|0x20 => 16 @ "" +Brng => 16 @ "" +16 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "\18" +Brng @ "\18" +Brng ::= 0x10|...|0x20 @ "\18" +Brng ::= 0x10|...|0x20 => 24 @ "" +Brng => 24 @ "" +24 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "\20" +Brng @ " " +Brng ::= 0x10|...|0x20 @ " " +Brng ::= 0x10|...|0x20 => 32 @ "" +Brng => 32 @ "" +32 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "\0F" +Brng @ "\0F" +Brng ::= 0x10|...|0x20 @ "\0F" +Brng ::= 0x10|...|0x20 => fail: byte 0x10..0x20 expected @ "\0F" +Brng => fail: byte 0x10..0x20 expected @ "\0F" +0: byte 0x10..0x20 expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "\21" +Brng @ "!" +Brng ::= 0x10|...|0x20 @ "!" +Brng ::= 0x10|...|0x20 => fail: byte 0x10..0x20 expected @ "!" +Brng => fail: byte 0x10..0x20 expected @ "!" +0: byte 0x10..0x20 expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brng "" +Brng @ "" +Brng ::= 0x10|...|0x20 @ "" +Brng ::= 0x10|...|0x20 => fail: unexpected end of input @ "" +Brng => fail: unexpected end of input @ "" +0: unexpected end of input +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar "" +Bstar @ "" +Bstar ::= 0x01* @ "" +Bstar/0x01* ::= eps @ "" +Bstar/0x01* ::= eps => [] @ "" +Bstar ::= 0x01* => [] @ "" +Bstar => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar "\01" +Bstar @ "\01" +Bstar ::= 0x01* @ "\01" +Bstar/0x01* ::= eps @ "\01" +Bstar/0x01* ::= eps => [] @ "\01" +Bstar ::= 0x01* => [] @ "\01" +Bstar => [] @ "\01" +Bstar => fail: end of input expected @ "\01" +Bstar/0x01* ::= 0x01 0x01* @ "\01" +Bstar/0x01*/0x01* ::= eps @ "" +Bstar/0x01*/0x01* ::= eps => [] @ "" +Bstar/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar ::= 0x01* => [1] @ "" +Bstar => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar "\01\01\01" +Bstar @ "\01\01\01" +Bstar ::= 0x01* @ "\01\01\01" +Bstar/0x01* ::= eps @ "\01\01\01" +Bstar/0x01* ::= eps => [] @ "\01\01\01" +Bstar ::= 0x01* => [] @ "\01\01\01" +Bstar => [] @ "\01\01\01" +Bstar => fail: end of input expected @ "\01\01\01" +Bstar/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bstar/0x01*/0x01* ::= eps @ "\01\01" +Bstar/0x01*/0x01* ::= eps => [] @ "\01\01" +Bstar/0x01* ::= 0x01 0x01* => [1] @ "\01\01" +Bstar ::= 0x01* => [1] @ "\01\01" +Bstar => [1] @ "\01\01" +Bstar => fail: end of input expected @ "\01\01" +Bstar/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bstar/0x01*/0x01*/0x01* ::= eps @ "\01" +Bstar/0x01*/0x01*/0x01* ::= eps => [] @ "\01" +Bstar/0x01*/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bstar/0x01* ::= 0x01 0x01* => [1 1] @ "\01" +Bstar ::= 0x01* => [1 1] @ "\01" +Bstar => [1 1] @ "\01" +Bstar => fail: end of input expected @ "\01" +Bstar/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bstar/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bstar/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bstar/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bstar/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bstar ::= 0x01* => [1 1 1] @ "" +Bstar => [1 1 1] @ "" +[1 1 1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar "\00\00" +Bstar @ "\00\00" +Bstar ::= 0x01* @ "\00\00" +Bstar/0x01* ::= eps @ "\00\00" +Bstar/0x01* ::= eps => [] @ "\00\00" +Bstar ::= 0x01* => [] @ "\00\00" +Bstar => [] @ "\00\00" +Bstar => fail: end of input expected @ "\00\00" +Bstar/0x01* ::= 0x01 0x01* @ "\00\00" +Bstar/0x01* ::= 0x01 0x01* => fail: byte 0x01 expected @ "\00\00" +Bstar ::= 0x01* => fail: byte 0x01 expected @ "\00\00" +Bstar => fail: byte 0x01 expected @ "\00\00" +0: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar "\01\00" +Bstar @ "\01\00" +Bstar ::= 0x01* @ "\01\00" +Bstar/0x01* ::= eps @ "\01\00" +Bstar/0x01* ::= eps => [] @ "\01\00" +Bstar ::= 0x01* => [] @ "\01\00" +Bstar => [] @ "\01\00" +Bstar => fail: end of input expected @ "\01\00" +Bstar/0x01* ::= 0x01 0x01* @ "\01\00" +Bstar/0x01*/0x01* ::= eps @ "\00" +Bstar/0x01*/0x01* ::= eps => [] @ "\00" +Bstar/0x01* ::= 0x01 0x01* => [1] @ "\00" +Bstar ::= 0x01* => [1] @ "\00" +Bstar => [1] @ "\00" +Bstar => fail: end of input expected @ "\00" +Bstar/0x01*/0x01* ::= 0x01 0x01* @ "\00" +Bstar/0x01*/0x01* ::= 0x01 0x01* => fail: byte 0x01 expected @ "\00" +Bstar/0x01* ::= 0x01 0x01* => fail: byte 0x01 expected @ "\00" +Bstar ::= 0x01* => fail: byte 0x01 expected @ "\00" +Bstar => fail: byte 0x01 expected @ "\00" +1: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar2 "" +Bstar2 @ "" +Bstar2 ::= 0x01* @ "" +Bstar2/0x01* ::= eps @ "" +Bstar2/0x01* ::= eps => [] @ "" +Bstar2 ::= 0x01* => [] @ "" +Bstar2 => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar2 "\01" +Bstar2 @ "\01" +Bstar2 ::= 0x01* @ "\01" +Bstar2/0x01* ::= eps @ "\01" +Bstar2/0x01* ::= eps => [] @ "\01" +Bstar2 ::= 0x01* => [] @ "\01" +Bstar2 => [] @ "\01" +Bstar2 => fail: end of input expected @ "\01" +Bstar2/0x01* ::= 0x01 0x01* @ "\01" +Bstar2/0x01*/0x01* ::= eps @ "" +Bstar2/0x01*/0x01* ::= eps => [] @ "" +Bstar2/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar2 ::= 0x01* => [1] @ "" +Bstar2 => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar2 "\01\01\01" +Bstar2 @ "\01\01\01" +Bstar2 ::= 0x01* @ "\01\01\01" +Bstar2/0x01* ::= eps @ "\01\01\01" +Bstar2/0x01* ::= eps => [] @ "\01\01\01" +Bstar2 ::= 0x01* => [] @ "\01\01\01" +Bstar2 => [] @ "\01\01\01" +Bstar2 => fail: end of input expected @ "\01\01\01" +Bstar2/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bstar2/0x01*/0x01* ::= eps @ "\01\01" +Bstar2/0x01*/0x01* ::= eps => [] @ "\01\01" +Bstar2/0x01* ::= 0x01 0x01* => [1] @ "\01\01" +Bstar2 ::= 0x01* => [1] @ "\01\01" +Bstar2 => [1] @ "\01\01" +Bstar2 => fail: end of input expected @ "\01\01" +Bstar2/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bstar2/0x01*/0x01*/0x01* ::= eps @ "\01" +Bstar2/0x01*/0x01*/0x01* ::= eps => [] @ "\01" +Bstar2/0x01*/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bstar2/0x01* ::= 0x01 0x01* => [1 1] @ "\01" +Bstar2 ::= 0x01* => [1 1] @ "\01" +Bstar2 => [1 1] @ "\01" +Bstar2 => fail: end of input expected @ "\01" +Bstar2/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bstar2/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bstar2/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bstar2/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar2/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bstar2/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bstar2 ::= 0x01* => [1 1 1] @ "" +Bstar2 => [1 1 1] @ "" +[1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar3 "" +Bstar3 @ "" +Bstar3 ::= 0x01* @ "" +Bstar3/0x01* ::= eps @ "" +Bstar3/0x01* ::= eps => [] @ "" +Bstar3 ::= 0x01* => [] @ "" +Bstar3 => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar3 "\01" +Bstar3 @ "\01" +Bstar3 ::= 0x01* @ "\01" +Bstar3/0x01* ::= eps @ "\01" +Bstar3/0x01* ::= eps => [] @ "\01" +Bstar3 ::= 0x01* => [] @ "\01" +Bstar3 => [] @ "\01" +Bstar3 => fail: end of input expected @ "\01" +Bstar3/0x01* ::= 0x01 0x01* @ "\01" +Bstar3/0x01*/0x01* ::= eps @ "" +Bstar3/0x01*/0x01* ::= eps => [] @ "" +Bstar3/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar3 ::= 0x01* => [1] @ "" +Bstar3 => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bstar3 "\01\01\01" +Bstar3 @ "\01\01\01" +Bstar3 ::= 0x01* @ "\01\01\01" +Bstar3/0x01* ::= eps @ "\01\01\01" +Bstar3/0x01* ::= eps => [] @ "\01\01\01" +Bstar3 ::= 0x01* => [] @ "\01\01\01" +Bstar3 => [] @ "\01\01\01" +Bstar3 => fail: end of input expected @ "\01\01\01" +Bstar3/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bstar3/0x01*/0x01* ::= eps @ "\01\01" +Bstar3/0x01*/0x01* ::= eps => [] @ "\01\01" +Bstar3/0x01* ::= 0x01 0x01* => [1] @ "\01\01" +Bstar3 ::= 0x01* => [1] @ "\01\01" +Bstar3 => [1] @ "\01\01" +Bstar3 => fail: end of input expected @ "\01\01" +Bstar3/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bstar3/0x01*/0x01*/0x01* ::= eps @ "\01" +Bstar3/0x01*/0x01*/0x01* ::= eps => [] @ "\01" +Bstar3/0x01*/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bstar3/0x01* ::= 0x01 0x01* => [1 1] @ "\01" +Bstar3 ::= 0x01* => [1 1] @ "\01" +Bstar3 => [1 1] @ "\01" +Bstar3 => fail: end of input expected @ "\01" +Bstar3/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bstar3/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bstar3/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bstar3/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bstar3/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bstar3/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bstar3 ::= 0x01* => [1 1 1] @ "" +Bstar3 => [1 1 1] @ "" +[1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "" +Tstar @ "" +Tstar ::= "AB"* @ "" +Tstar/"AB"* ::= eps @ "" +Tstar/"AB"* ::= eps => [] @ "" +Tstar ::= "AB"* => () @ "" +Tstar => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "AB" +Tstar @ "AB" +Tstar ::= "AB"* @ "AB" +Tstar/"AB"* ::= eps @ "AB" +Tstar/"AB"* ::= eps => [] @ "AB" +Tstar ::= "AB"* => () @ "AB" +Tstar => () @ "AB" +Tstar => fail: end of input expected @ "AB" +Tstar/"AB"* ::= "AB" "AB"* @ "AB" +Tstar/"AB"*/"AB"* ::= eps @ "" +Tstar/"AB"*/"AB"* ::= eps => [] @ "" +Tstar/"AB"* ::= "AB" "AB"* => ["AB"] @ "" +Tstar ::= "AB"* => () @ "" +Tstar => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "ABABAB" +Tstar @ "ABABAB" +Tstar ::= "AB"* @ "ABABAB" +Tstar/"AB"* ::= eps @ "ABABAB" +Tstar/"AB"* ::= eps => [] @ "ABABAB" +Tstar ::= "AB"* => () @ "ABABAB" +Tstar => () @ "ABABAB" +Tstar => fail: end of input expected @ "ABABAB" +Tstar/"AB"* ::= "AB" "AB"* @ "ABABAB" +Tstar/"AB"*/"AB"* ::= eps @ "ABAB" +Tstar/"AB"*/"AB"* ::= eps => [] @ "ABAB" +Tstar/"AB"* ::= "AB" "AB"* => ["AB"] @ "ABAB" +Tstar ::= "AB"* => () @ "ABAB" +Tstar => () @ "ABAB" +Tstar => fail: end of input expected @ "ABAB" +Tstar/"AB"*/"AB"* ::= "AB" "AB"* @ "ABAB" +Tstar/"AB"*/"AB"*/"AB"* ::= eps @ "AB" +Tstar/"AB"*/"AB"*/"AB"* ::= eps => [] @ "AB" +Tstar/"AB"*/"AB"* ::= "AB" "AB"* => ["AB"] @ "AB" +Tstar/"AB"* ::= "AB" "AB"* => ["AB" "AB"] @ "AB" +Tstar ::= "AB"* => () @ "AB" +Tstar => () @ "AB" +Tstar => fail: end of input expected @ "AB" +Tstar/"AB"*/"AB"*/"AB"* ::= "AB" "AB"* @ "AB" +Tstar/"AB"*/"AB"*/"AB"*/"AB"* ::= eps @ "" +Tstar/"AB"*/"AB"*/"AB"*/"AB"* ::= eps => [] @ "" +Tstar/"AB"*/"AB"*/"AB"* ::= "AB" "AB"* => ["AB"] @ "" +Tstar/"AB"*/"AB"* ::= "AB" "AB"* => ["AB" "AB"] @ "" +Tstar/"AB"* ::= "AB" "AB"* => ["AB" "AB" "AB"] @ "" +Tstar ::= "AB"* => () @ "" +Tstar => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "A" +Tstar @ "A" +Tstar ::= "AB"* @ "A" +Tstar/"AB"* ::= eps @ "A" +Tstar/"AB"* ::= eps => [] @ "A" +Tstar ::= "AB"* => () @ "A" +Tstar => () @ "A" +Tstar => fail: end of input expected @ "A" +Tstar/"AB"* ::= "AB" "AB"* @ "A" +Tstar/"AB"* ::= "AB" "AB"* => fail: text "AB" expected @ "A" +Tstar ::= "AB"* => fail: text "AB" expected @ "A" +Tstar => fail: text "AB" expected @ "A" +0: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "ABA" +Tstar @ "ABA" +Tstar ::= "AB"* @ "ABA" +Tstar/"AB"* ::= eps @ "ABA" +Tstar/"AB"* ::= eps => [] @ "ABA" +Tstar ::= "AB"* => () @ "ABA" +Tstar => () @ "ABA" +Tstar => fail: end of input expected @ "ABA" +Tstar/"AB"* ::= "AB" "AB"* @ "ABA" +Tstar/"AB"*/"AB"* ::= eps @ "A" +Tstar/"AB"*/"AB"* ::= eps => [] @ "A" +Tstar/"AB"* ::= "AB" "AB"* => ["AB"] @ "A" +Tstar ::= "AB"* => () @ "A" +Tstar => () @ "A" +Tstar => fail: end of input expected @ "A" +Tstar/"AB"*/"AB"* ::= "AB" "AB"* @ "A" +Tstar/"AB"*/"AB"* ::= "AB" "AB"* => fail: text "AB" expected @ "A" +Tstar/"AB"* ::= "AB" "AB"* => fail: text "AB" expected @ "A" +Tstar ::= "AB"* => fail: text "AB" expected @ "A" +Tstar => fail: text "AB" expected @ "A" +2: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tstar "B" +Tstar @ "B" +Tstar ::= "AB"* @ "B" +Tstar/"AB"* ::= eps @ "B" +Tstar/"AB"* ::= eps => [] @ "B" +Tstar ::= "AB"* => () @ "B" +Tstar => () @ "B" +Tstar => fail: end of input expected @ "B" +Tstar/"AB"* ::= "AB" "AB"* @ "B" +Tstar/"AB"* ::= "AB" "AB"* => fail: text "AB" expected @ "B" +Tstar ::= "AB"* => fail: text "AB" expected @ "B" +Tstar => fail: text "AB" expected @ "B" +0: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus "" +Bplus @ "" +Bplus ::= 0x01+ @ "" +Bplus/0x01+ ::= 0x01 0x01* @ "" +Bplus/0x01+ ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bplus ::= 0x01+ => fail: unexpected end of input @ "" +Bplus => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus "\01" +Bplus @ "\01" +Bplus ::= 0x01+ @ "\01" +Bplus/0x01+ ::= 0x01 0x01* @ "\01" +Bplus/0x01+/0x01* ::= eps @ "" +Bplus/0x01+/0x01* ::= eps => [] @ "" +Bplus/0x01+ ::= 0x01 0x01* => [1] @ "" +Bplus ::= 0x01+ => [1] @ "" +Bplus => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus "\01\01\01" +Bplus @ "\01\01\01" +Bplus ::= 0x01+ @ "\01\01\01" +Bplus/0x01+ ::= 0x01 0x01* @ "\01\01\01" +Bplus/0x01+/0x01* ::= eps @ "\01\01" +Bplus/0x01+/0x01* ::= eps => [] @ "\01\01" +Bplus/0x01+ ::= 0x01 0x01* => [1] @ "\01\01" +Bplus ::= 0x01+ => [1] @ "\01\01" +Bplus => [1] @ "\01\01" +Bplus => fail: end of input expected @ "\01\01" +Bplus/0x01+/0x01* ::= 0x01 0x01* @ "\01\01" +Bplus/0x01+/0x01*/0x01* ::= eps @ "\01" +Bplus/0x01+/0x01*/0x01* ::= eps => [] @ "\01" +Bplus/0x01+/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bplus/0x01+ ::= 0x01 0x01* => [1 1] @ "\01" +Bplus ::= 0x01+ => [1 1] @ "\01" +Bplus => [1 1] @ "\01" +Bplus => fail: end of input expected @ "\01" +Bplus/0x01+/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bplus/0x01+/0x01*/0x01*/0x01* ::= eps @ "" +Bplus/0x01+/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bplus/0x01+/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bplus/0x01+/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bplus/0x01+ ::= 0x01 0x01* => [1 1 1] @ "" +Bplus ::= 0x01+ => [1 1 1] @ "" +Bplus => [1 1 1] @ "" +[1 1 1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus "\00" +Bplus @ "\00" +Bplus ::= 0x01+ @ "\00" +Bplus/0x01+ ::= 0x01 0x01* @ "\00" +Bplus/0x01+ ::= 0x01 0x01* => fail: byte 0x01 expected @ "\00" +Bplus ::= 0x01+ => fail: byte 0x01 expected @ "\00" +Bplus => fail: byte 0x01 expected @ "\00" +0: byte 0x01 expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus2 "" +Bplus2 @ "" +Bplus2 ::= 0x01+ @ "" +Bplus2/0x01+ ::= 0x01 0x01* @ "" +Bplus2/0x01+ ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bplus2 ::= 0x01+ => fail: unexpected end of input @ "" +Bplus2 => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus2 "\01" +Bplus2 @ "\01" +Bplus2 ::= 0x01+ @ "\01" +Bplus2/0x01+ ::= 0x01 0x01* @ "\01" +Bplus2/0x01+/0x01* ::= eps @ "" +Bplus2/0x01+/0x01* ::= eps => [] @ "" +Bplus2/0x01+ ::= 0x01 0x01* => [1] @ "" +Bplus2 ::= 0x01+ => [1] @ "" +Bplus2 => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus2 "\01\01\01" +Bplus2 @ "\01\01\01" +Bplus2 ::= 0x01+ @ "\01\01\01" +Bplus2/0x01+ ::= 0x01 0x01* @ "\01\01\01" +Bplus2/0x01+/0x01* ::= eps @ "\01\01" +Bplus2/0x01+/0x01* ::= eps => [] @ "\01\01" +Bplus2/0x01+ ::= 0x01 0x01* => [1] @ "\01\01" +Bplus2 ::= 0x01+ => [1] @ "\01\01" +Bplus2 => [1] @ "\01\01" +Bplus2 => fail: end of input expected @ "\01\01" +Bplus2/0x01+/0x01* ::= 0x01 0x01* @ "\01\01" +Bplus2/0x01+/0x01*/0x01* ::= eps @ "\01" +Bplus2/0x01+/0x01*/0x01* ::= eps => [] @ "\01" +Bplus2/0x01+/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bplus2/0x01+ ::= 0x01 0x01* => [1 1] @ "\01" +Bplus2 ::= 0x01+ => [1 1] @ "\01" +Bplus2 => [1 1] @ "\01" +Bplus2 => fail: end of input expected @ "\01" +Bplus2/0x01+/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bplus2/0x01+/0x01*/0x01*/0x01* ::= eps @ "" +Bplus2/0x01+/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bplus2/0x01+/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bplus2/0x01+/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bplus2/0x01+ ::= 0x01 0x01* => [1 1 1] @ "" +Bplus2 ::= 0x01+ => [1 1 1] @ "" +Bplus2 => [1 1 1] @ "" +[1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus3 "" +Bplus3 @ "" +Bplus3 ::= 0x01+ @ "" +Bplus3/0x01+ ::= 0x01 0x01* @ "" +Bplus3/0x01+ ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bplus3 ::= 0x01+ => fail: unexpected end of input @ "" +Bplus3 => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus3 "\01" +Bplus3 @ "\01" +Bplus3 ::= 0x01+ @ "\01" +Bplus3/0x01+ ::= 0x01 0x01* @ "\01" +Bplus3/0x01+/0x01* ::= eps @ "" +Bplus3/0x01+/0x01* ::= eps => [] @ "" +Bplus3/0x01+ ::= 0x01 0x01* => [1] @ "" +Bplus3 ::= 0x01+ => [1] @ "" +Bplus3 => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bplus3 "\01\01\01" +Bplus3 @ "\01\01\01" +Bplus3 ::= 0x01+ @ "\01\01\01" +Bplus3/0x01+ ::= 0x01 0x01* @ "\01\01\01" +Bplus3/0x01+/0x01* ::= eps @ "\01\01" +Bplus3/0x01+/0x01* ::= eps => [] @ "\01\01" +Bplus3/0x01+ ::= 0x01 0x01* => [1] @ "\01\01" +Bplus3 ::= 0x01+ => [1] @ "\01\01" +Bplus3 => [1] @ "\01\01" +Bplus3 => fail: end of input expected @ "\01\01" +Bplus3/0x01+/0x01* ::= 0x01 0x01* @ "\01\01" +Bplus3/0x01+/0x01*/0x01* ::= eps @ "\01" +Bplus3/0x01+/0x01*/0x01* ::= eps => [] @ "\01" +Bplus3/0x01+/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bplus3/0x01+ ::= 0x01 0x01* => [1 1] @ "\01" +Bplus3 ::= 0x01+ => [1 1] @ "\01" +Bplus3 => [1 1] @ "\01" +Bplus3 => fail: end of input expected @ "\01" +Bplus3/0x01+/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bplus3/0x01+/0x01*/0x01*/0x01* ::= eps @ "" +Bplus3/0x01+/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bplus3/0x01+/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bplus3/0x01+/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bplus3/0x01+ ::= 0x01 0x01* => [1 1 1] @ "" +Bplus3 ::= 0x01+ => [1 1 1] @ "" +Bplus3 => [1 1 1] @ "" +[1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "" +Tplus @ "" +Tplus ::= "ABC"+ @ "" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "" +Tplus/"ABC"+ ::= "ABC" "ABC"* => fail: unexpected end of input @ "" +Tplus ::= "ABC"+ => fail: unexpected end of input @ "" +Tplus => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "ABC" +Tplus @ "ABC" +Tplus ::= "ABC"+ @ "ABC" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "ABC" +Tplus/"ABC"+/"ABC"* ::= eps @ "" +Tplus/"ABC"+/"ABC"* ::= eps => [] @ "" +Tplus/"ABC"+ ::= "ABC" "ABC"* => ["ABC"] @ "" +Tplus ::= "ABC"+ => () @ "" +Tplus => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "ABCABCABC" +Tplus @ "ABCABCABC" +Tplus ::= "ABC"+ @ "ABCABCABC" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "ABCABCABC" +Tplus/"ABC"+/"ABC"* ::= eps @ "ABCABC" +Tplus/"ABC"+/"ABC"* ::= eps => [] @ "ABCABC" +Tplus/"ABC"+ ::= "ABC" "ABC"* => ["ABC"] @ "ABCABC" +Tplus ::= "ABC"+ => () @ "ABCABC" +Tplus => () @ "ABCABC" +Tplus => fail: end of input expected @ "ABCABC" +Tplus/"ABC"+/"ABC"* ::= "ABC" "ABC"* @ "ABCABC" +Tplus/"ABC"+/"ABC"*/"ABC"* ::= eps @ "ABC" +Tplus/"ABC"+/"ABC"*/"ABC"* ::= eps => [] @ "ABC" +Tplus/"ABC"+/"ABC"* ::= "ABC" "ABC"* => ["ABC"] @ "ABC" +Tplus/"ABC"+ ::= "ABC" "ABC"* => ["ABC" "ABC"] @ "ABC" +Tplus ::= "ABC"+ => () @ "ABC" +Tplus => () @ "ABC" +Tplus => fail: end of input expected @ "ABC" +Tplus/"ABC"+/"ABC"*/"ABC"* ::= "ABC" "ABC"* @ "ABC" +Tplus/"ABC"+/"ABC"*/"ABC"*/"ABC"* ::= eps @ "" +Tplus/"ABC"+/"ABC"*/"ABC"*/"ABC"* ::= eps => [] @ "" +Tplus/"ABC"+/"ABC"*/"ABC"* ::= "ABC" "ABC"* => ["ABC"] @ "" +Tplus/"ABC"+/"ABC"* ::= "ABC" "ABC"* => ["ABC" "ABC"] @ "" +Tplus/"ABC"+ ::= "ABC" "ABC"* => ["ABC" "ABC" "ABC"] @ "" +Tplus ::= "ABC"+ => () @ "" +Tplus => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "BAC" +Tplus @ "BAC" +Tplus ::= "ABC"+ @ "BAC" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "BAC" +Tplus/"ABC"+ ::= "ABC" "ABC"* => fail: text "ABC" expected @ "BAC" +Tplus ::= "ABC"+ => fail: text "ABC" expected @ "BAC" +Tplus => fail: text "ABC" expected @ "BAC" +0: text "ABC" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "A" +Tplus @ "A" +Tplus ::= "ABC"+ @ "A" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "A" +Tplus/"ABC"+ ::= "ABC" "ABC"* => fail: text "ABC" expected @ "A" +Tplus ::= "ABC"+ => fail: text "ABC" expected @ "A" +Tplus => fail: text "ABC" expected @ "A" +0: text "ABC" expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tplus "AB" +Tplus @ "AB" +Tplus ::= "ABC"+ @ "AB" +Tplus/"ABC"+ ::= "ABC" "ABC"* @ "AB" +Tplus/"ABC"+ ::= "ABC" "ABC"* => fail: text "ABC" expected @ "AB" +Tplus ::= "ABC"+ => fail: text "ABC" expected @ "AB" +Tplus => fail: text "ABC" expected @ "AB" +0: text "ABC" expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest "" +Bquest @ "" +Bquest ::= 0x01? @ "" +Bquest/0x01? ::= eps @ "" +Bquest/0x01? ::= eps => [] @ "" +Bquest ::= 0x01? => ?() @ "" +Bquest => ?() @ "" +?() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest "\01" +Bquest @ "\01" +Bquest ::= 0x01? @ "\01" +Bquest/0x01? ::= eps @ "\01" +Bquest/0x01? ::= eps => [] @ "\01" +Bquest ::= 0x01? => ?() @ "\01" +Bquest => ?() @ "\01" +Bquest => fail: end of input expected @ "\01" +Bquest/0x01? ::= 0x01 0x01* @ "\01" +Bquest/0x01?/0x01* ::= eps @ "" +Bquest/0x01?/0x01* ::= eps => [] @ "" +Bquest/0x01? ::= 0x01 0x01* => [1] @ "" +Bquest ::= 0x01? => ?(1) @ "" +Bquest => ?(1) @ "" +?(1) +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest "\01\01" +Bquest @ "\01\01" +Bquest ::= 0x01? @ "\01\01" +Bquest/0x01? ::= eps @ "\01\01" +Bquest/0x01? ::= eps => [] @ "\01\01" +Bquest ::= 0x01? => ?() @ "\01\01" +Bquest => ?() @ "\01\01" +Bquest => fail: end of input expected @ "\01\01" +Bquest/0x01? ::= 0x01 0x01* @ "\01\01" +Bquest/0x01?/0x01* ::= eps @ "\01" +Bquest/0x01?/0x01* ::= eps => [] @ "\01" +Bquest/0x01? ::= 0x01 0x01* => [1] @ "\01" +Bquest ::= 0x01? => ?(1) @ "\01" +Bquest => ?(1) @ "\01" +Bquest => fail: end of input expected @ "\01" +Bquest/0x01? ::= 0x01 0x01* => fail: unexpected input @ "\01" +Bquest ::= 0x01? => fail: unexpected input @ "\01" +Bquest => fail: unexpected input @ "\01" +1: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest "\00" +Bquest @ "\00" +Bquest ::= 0x01? @ "\00" +Bquest/0x01? ::= eps @ "\00" +Bquest/0x01? ::= eps => [] @ "\00" +Bquest ::= 0x01? => ?() @ "\00" +Bquest => ?() @ "\00" +Bquest => fail: end of input expected @ "\00" +Bquest/0x01? ::= 0x01 0x01* @ "\00" +Bquest/0x01? ::= 0x01 0x01* => fail: byte 0x01 expected @ "\00" +Bquest ::= 0x01? => fail: byte 0x01 expected @ "\00" +Bquest => fail: byte 0x01 expected @ "\00" +0: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest2 "" +Bquest2 @ "" +Bquest2 ::= 0x01? @ "" +Bquest2/0x01? ::= eps @ "" +Bquest2/0x01? ::= eps => [] @ "" +Bquest2 ::= 0x01? => ?() @ "" +Bquest2 => ?() @ "" +?() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest2 "\01" +Bquest2 @ "\01" +Bquest2 ::= 0x01? @ "\01" +Bquest2/0x01? ::= eps @ "\01" +Bquest2/0x01? ::= eps => [] @ "\01" +Bquest2 ::= 0x01? => ?() @ "\01" +Bquest2 => ?() @ "\01" +Bquest2 => fail: end of input expected @ "\01" +Bquest2/0x01? ::= 0x01 0x01* @ "\01" +Bquest2/0x01?/0x01* ::= eps @ "" +Bquest2/0x01?/0x01* ::= eps => [] @ "" +Bquest2/0x01? ::= 0x01 0x01* => [1] @ "" +Bquest2 ::= 0x01? => ?(1) @ "" +Bquest2 => ?(1) @ "" +?(1) +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest3 "" +Bquest3 @ "" +Bquest3 ::= 0x01? @ "" +Bquest3/0x01? ::= eps @ "" +Bquest3/0x01? ::= eps => [] @ "" +Bquest3 ::= 0x01? => ?() @ "" +Bquest3 => ?() @ "" +?() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bquest3 "\01" +Bquest3 @ "\01" +Bquest3 ::= 0x01? @ "\01" +Bquest3/0x01? ::= eps @ "\01" +Bquest3/0x01? ::= eps => [] @ "\01" +Bquest3 ::= 0x01? => ?() @ "\01" +Bquest3 => ?() @ "\01" +Bquest3 => fail: end of input expected @ "\01" +Bquest3/0x01? ::= 0x01 0x01* @ "\01" +Bquest3/0x01?/0x01* ::= eps @ "" +Bquest3/0x01?/0x01* ::= eps => [] @ "" +Bquest3/0x01? ::= 0x01 0x01* => [1] @ "" +Bquest3 ::= 0x01? => ?(1) @ "" +Bquest3 => ?(1) @ "" +?(1) +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tquest "" +Tquest @ "" +Tquest ::= "ABCD"? @ "" +Tquest/"ABCD"? ::= eps @ "" +Tquest/"ABCD"? ::= eps => [] @ "" +Tquest ::= "ABCD"? => () @ "" +Tquest => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tquest "ABCD" +Tquest @ "ABCD" +Tquest ::= "ABCD"? @ "ABCD" +Tquest/"ABCD"? ::= eps @ "ABCD" +Tquest/"ABCD"? ::= eps => [] @ "ABCD" +Tquest ::= "ABCD"? => () @ "ABCD" +Tquest => () @ "ABCD" +Tquest => fail: end of input expected @ "ABCD" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* @ "ABCD" +Tquest/"ABCD"?/"ABCD"* ::= eps @ "" +Tquest/"ABCD"?/"ABCD"* ::= eps => [] @ "" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* => ["ABCD"] @ "" +Tquest ::= "ABCD"? => () @ "" +Tquest => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tquest "ABCDABCD" +Tquest @ "ABCDABCD" +Tquest ::= "ABCD"? @ "ABCDABCD" +Tquest/"ABCD"? ::= eps @ "ABCDABCD" +Tquest/"ABCD"? ::= eps => [] @ "ABCDABCD" +Tquest ::= "ABCD"? => () @ "ABCDABCD" +Tquest => () @ "ABCDABCD" +Tquest => fail: end of input expected @ "ABCDABCD" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* @ "ABCDABCD" +Tquest/"ABCD"?/"ABCD"* ::= eps @ "ABCD" +Tquest/"ABCD"?/"ABCD"* ::= eps => [] @ "ABCD" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* => ["ABCD"] @ "ABCD" +Tquest ::= "ABCD"? => () @ "ABCD" +Tquest => () @ "ABCD" +Tquest => fail: end of input expected @ "ABCD" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* => fail: unexpected input @ "ABCD" +Tquest ::= "ABCD"? => fail: unexpected input @ "ABCD" +Tquest => fail: unexpected input @ "ABCD" +4: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tquest "A" +Tquest @ "A" +Tquest ::= "ABCD"? @ "A" +Tquest/"ABCD"? ::= eps @ "A" +Tquest/"ABCD"? ::= eps => [] @ "A" +Tquest ::= "ABCD"? => () @ "A" +Tquest => () @ "A" +Tquest => fail: end of input expected @ "A" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* @ "A" +Tquest/"ABCD"? ::= "ABCD" "ABCD"* => fail: text "ABCD" expected @ "A" +Tquest ::= "ABCD"? => fail: text "ABCD" expected @ "A" +Tquest => fail: text "ABCD" expected @ "A" +0: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth "\01\01\01\01" +Bnth @ "\01\01\01\01" +Bnth ::= 0x01^(2 * 2) @ "\01\01\01\01" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* @ "\01\01\01\01" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bnth/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bnth/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* => [1 1 1 1] @ "" +Bnth ::= 0x01^(2 * 2) => [1 1 1 1] @ "" +Bnth => [1 1 1 1] @ "" +[1 1 1 1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth "" +Bnth @ "" +Bnth ::= 0x01^(2 * 2) @ "" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* @ "" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bnth ::= 0x01^(2 * 2) => fail: unexpected end of input @ "" +Bnth => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth "\01" +Bnth @ "\01" +Bnth ::= 0x01^(2 * 2) @ "\01" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* @ "\01" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* @ "" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* => fail: unexpected end of input @ "" +Bnth ::= 0x01^(2 * 2) => fail: unexpected end of input @ "" +Bnth => fail: unexpected end of input @ "" +1: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth "\01\01\01\01\01" +Bnth @ "\01\01\01\01\01" +Bnth ::= 0x01^(2 * 2) @ "\01\01\01\01\01" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* @ "\01\01\01\01\01" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* @ "\01\01\01\01" +Bnth/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "\01" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => [1 1 1] @ "\01" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* => [1 1 1 1] @ "\01" +Bnth ::= 0x01^(2 * 2) => [1 1 1 1] @ "\01" +Bnth => [1 1 1 1] @ "\01" +Bnth => fail: end of input expected @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* => fail: unexpected input @ "\01" +Bnth/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* => fail: unexpected input @ "\01" +Bnth/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => fail: unexpected input @ "\01" +Bnth/0x01^(2 * 2) ::= 0x01 0x01* => fail: unexpected input @ "\01" +Bnth ::= 0x01^(2 * 2) => fail: unexpected input @ "\01" +Bnth => fail: unexpected input @ "\01" +4: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth2 "\01\01\01\01" +Bnth2 @ "\01\01\01\01" +Bnth2 ::= 0x01^(2 * 2) @ "\01\01\01\01" +Bnth2/0x01^(2 * 2) ::= 0x01 0x01* @ "\01\01\01\01" +Bnth2/0x01^(2 * 2)/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bnth2/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bnth2/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bnth2/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bnth2/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bnth2/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bnth2/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bnth2/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bnth2/0x01^(2 * 2) ::= 0x01 0x01* => [1 1 1 1] @ "" +Bnth2 ::= 0x01^(2 * 2) => [1 1 1 1] @ "" +Bnth2 => [1 1 1 1] @ "" +[1 1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bnth3 "\01\01\01\01" +Bnth3 @ "\01\01\01\01" +Bnth3 ::= 0x01^(2 * 2) @ "\01\01\01\01" +Bnth3/0x01^(2 * 2) ::= 0x01 0x01* @ "\01\01\01\01" +Bnth3/0x01^(2 * 2)/0x01* ::= 0x01 0x01* @ "\01\01\01" +Bnth3/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* @ "\01\01" +Bnth3/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* @ "\01" +Bnth3/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps @ "" +Bnth3/0x01^(2 * 2)/0x01*/0x01*/0x01*/0x01* ::= eps => [] @ "" +Bnth3/0x01^(2 * 2)/0x01*/0x01*/0x01* ::= 0x01 0x01* => [1] @ "" +Bnth3/0x01^(2 * 2)/0x01*/0x01* ::= 0x01 0x01* => [1 1] @ "" +Bnth3/0x01^(2 * 2)/0x01* ::= 0x01 0x01* => [1 1 1] @ "" +Bnth3/0x01^(2 * 2) ::= 0x01 0x01* => [1 1 1 1] @ "" +Bnth3 ::= 0x01^(2 * 2) => [1 1 1 1] @ "" +Bnth3 => [1 1 1 1] @ "" +[1 1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tnth "ABCABCABC" +Tnth @ "ABCABCABC" +Tnth ::= "ABC"^(7 - 4) @ "ABCABCABC" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* @ "ABCABCABC" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* @ "ABCABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps @ "" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps => [] @ "" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* => ["ABC"] @ "" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => ["ABC" "ABC"] @ "" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => ["ABC" "ABC" "ABC"] @ "" +Tnth ::= "ABC"^(7 - 4) => () @ "" +Tnth => () @ "" +() +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tnth "" +Tnth @ "" +Tnth ::= "ABC"^(7 - 4) @ "" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* @ "" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => fail: unexpected end of input @ "" +Tnth ::= "ABC"^(7 - 4) => fail: unexpected end of input @ "" +Tnth => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tnth "ABC" +Tnth @ "ABC" +Tnth ::= "ABC"^(7 - 4) @ "ABC" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* @ "" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => fail: unexpected end of input @ "" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => fail: unexpected end of input @ "" +Tnth ::= "ABC"^(7 - 4) => fail: unexpected end of input @ "" +Tnth => fail: unexpected end of input @ "" +3: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tnth "ABCABCABCA" +Tnth @ "ABCABCABCA" +Tnth ::= "ABC"^(7 - 4) @ "ABCABCABCA" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* @ "ABCABCABCA" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* @ "ABCABCA" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* @ "ABCA" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps @ "A" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps => [] @ "A" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* => ["ABC"] @ "A" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => ["ABC" "ABC"] @ "A" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => ["ABC" "ABC" "ABC"] @ "A" +Tnth ::= "ABC"^(7 - 4) => () @ "A" +Tnth => () @ "A" +Tnth => fail: end of input expected @ "A" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* => fail: unexpected input @ "A" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => fail: unexpected input @ "A" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => fail: unexpected input @ "A" +Tnth ::= "ABC"^(7 - 4) => fail: unexpected input @ "A" +Tnth => fail: unexpected input @ "A" +9: end of input expected +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Tnth "ABCABCABCABC" +Tnth @ "ABCABCABCABC" +Tnth ::= "ABC"^(7 - 4) @ "ABCABCABCABC" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* @ "ABCABCABCABC" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* @ "ABCABCABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* @ "ABCABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"*/"ABC"* ::= eps => [] @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* => ["ABC"] @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => ["ABC" "ABC"] @ "ABC" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => ["ABC" "ABC" "ABC"] @ "ABC" +Tnth ::= "ABC"^(7 - 4) => () @ "ABC" +Tnth => () @ "ABC" +Tnth => fail: end of input expected @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"*/"ABC"* ::= "ABC" "ABC"* => fail: unexpected input @ "ABC" +Tnth/"ABC"^(7 - 4)/"ABC"* ::= "ABC" "ABC"* => fail: unexpected input @ "ABC" +Tnth/"ABC"^(7 - 4) ::= "ABC" "ABC"* => fail: unexpected input @ "ABC" +Tnth ::= "ABC"^(7 - 4) => fail: unexpected input @ "ABC" +Tnth => fail: unexpected input @ "ABC" +9: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bvar "\01\03\04\10" +Bvar @ "\01\03\04\10" +Bvar ::= 0x01 Bdef 0x10 @ "\01\03\04\10" +Bvar/Bdef @ "\03\04\10" +Bvar/Bdef ::= 0x03 0x04 @ "\03\04\10" +Bvar/Bdef ::= 0x03 0x04 => 7 @ "\10" +Bvar/Bdef => 7 @ "\10" +Bvar ::= 0x01 Bdef 0x10 => 23 @ "" +Bvar => 23 @ "" +23 +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bvar "\01" +Bvar @ "\01" +Bvar ::= 0x01 Bdef 0x10 @ "\01" +Bvar/Bdef @ "" +Bvar/Bdef ::= 0x03 0x04 @ "" +Bvar/Bdef ::= 0x03 0x04 => fail: unexpected end of input @ "" +Bvar/Bdef => fail: unexpected end of input @ "" +Bvar ::= 0x01 Bdef 0x10 => fail: unexpected end of input @ "" +Bvar => fail: unexpected end of input @ "" +1: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Bvar "\01\03\04\10\00" +Bvar @ "\01\03\04\10\00" +Bvar ::= 0x01 Bdef 0x10 @ "\01\03\04\10\00" +Bvar/Bdef @ "\03\04\10\00" +Bvar/Bdef ::= 0x03 0x04 @ "\03\04\10\00" +Bvar/Bdef ::= 0x03 0x04 => 7 @ "\10\00" +Bvar/Bdef => 7 @ "\10\00" +Bvar ::= 0x01 Bdef 0x10 => 23 @ "\00" +Bvar => 23 @ "\00" +Bvar => fail: end of input expected @ "\00" +Bvar ::= 0x01 Bdef 0x10 => fail: unexpected input @ "\10\00" +Bvar => fail: unexpected input @ "\10\00" +4: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec "" +Brec @ "" +Brec ::= eps @ "" +Brec ::= eps => [] @ "" +Brec => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec "\01" +Brec @ "\01" +Brec ::= eps @ "\01" +Brec ::= eps => [] @ "\01" +Brec => [] @ "\01" +Brec => fail: end of input expected @ "\01" +Brec ::= 0x01 Brec @ "\01" +Brec/Brec @ "" +Brec/Brec ::= eps @ "" +Brec/Brec ::= eps => [] @ "" +Brec/Brec => [] @ "" +Brec ::= 0x01 Brec => [1] @ "" +Brec => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec "\01\01\01" +Brec @ "\01\01\01" +Brec ::= eps @ "\01\01\01" +Brec ::= eps => [] @ "\01\01\01" +Brec => [] @ "\01\01\01" +Brec => fail: end of input expected @ "\01\01\01" +Brec ::= 0x01 Brec @ "\01\01\01" +Brec/Brec @ "\01\01" +Brec/Brec ::= eps @ "\01\01" +Brec/Brec ::= eps => [] @ "\01\01" +Brec/Brec => [] @ "\01\01" +Brec ::= 0x01 Brec => [1] @ "\01\01" +Brec => [1] @ "\01\01" +Brec => fail: end of input expected @ "\01\01" +Brec/Brec ::= 0x01 Brec @ "\01\01" +Brec/Brec/Brec @ "\01" +Brec/Brec/Brec ::= eps @ "\01" +Brec/Brec/Brec ::= eps => [] @ "\01" +Brec/Brec/Brec => [] @ "\01" +Brec/Brec ::= 0x01 Brec => [1] @ "\01" +Brec/Brec => [1] @ "\01" +Brec ::= 0x01 Brec => [1 1] @ "\01" +Brec => [1 1] @ "\01" +Brec => fail: end of input expected @ "\01" +Brec/Brec/Brec ::= 0x01 Brec @ "\01" +Brec/Brec/Brec/Brec @ "" +Brec/Brec/Brec/Brec ::= eps @ "" +Brec/Brec/Brec/Brec ::= eps => [] @ "" +Brec/Brec/Brec/Brec => [] @ "" +Brec/Brec/Brec ::= 0x01 Brec => [1] @ "" +Brec/Brec/Brec => [1] @ "" +Brec/Brec ::= 0x01 Brec => [1 1] @ "" +Brec/Brec => [1 1] @ "" +Brec ::= 0x01 Brec => [1 1 1] @ "" +Brec => [1 1 1] @ "" +[1 1 1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec "\01\00" +Brec @ "\01\00" +Brec ::= eps @ "\01\00" +Brec ::= eps => [] @ "\01\00" +Brec => [] @ "\01\00" +Brec => fail: end of input expected @ "\01\00" +Brec ::= 0x01 Brec @ "\01\00" +Brec/Brec @ "\00" +Brec/Brec ::= eps @ "\00" +Brec/Brec ::= eps => [] @ "\00" +Brec/Brec => [] @ "\00" +Brec ::= 0x01 Brec => [1] @ "\00" +Brec => [1] @ "\00" +Brec => fail: end of input expected @ "\00" +Brec/Brec ::= 0x01 Brec @ "\00" +Brec/Brec ::= 0x01 Brec => fail: byte 0x01 expected @ "\00" +Brec/Brec => fail: unexpected input @ "\00" +Brec ::= 0x01 Brec => fail: unexpected input @ "\00" +Brec => fail: unexpected input @ "\00" +1: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec2 "" +Brec2 @ "" +Brec2 ::= eps @ "" +Brec2 ::= eps => [] @ "" +Brec2 => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec2 "\01" +Brec2 @ "\01" +Brec2 ::= eps @ "\01" +Brec2 ::= eps => [] @ "\01" +Brec2 => [] @ "\01" +Brec2 => fail: end of input expected @ "\01" +Brec2 ::= 0x01 Brec2 @ "\01" +Brec2/Brec2 @ "" +Brec2/Brec2 ::= eps @ "" +Brec2/Brec2 ::= eps => [] @ "" +Brec2/Brec2 => [] @ "" +Brec2 ::= 0x01 Brec2 => [1] @ "" +Brec2 => [1] @ "" +[1] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Brec2 "\01\01\01" +Brec2 @ "\01\01\01" +Brec2 ::= eps @ "\01\01\01" +Brec2 ::= eps => [] @ "\01\01\01" +Brec2 => [] @ "\01\01\01" +Brec2 => fail: end of input expected @ "\01\01\01" +Brec2 ::= 0x01 Brec2 @ "\01\01\01" +Brec2/Brec2 @ "\01\01" +Brec2/Brec2 ::= eps @ "\01\01" +Brec2/Brec2 ::= eps => [] @ "\01\01" +Brec2/Brec2 => [] @ "\01\01" +Brec2 ::= 0x01 Brec2 => [1] @ "\01\01" +Brec2 => [1] @ "\01\01" +Brec2 => fail: end of input expected @ "\01\01" +Brec2/Brec2 ::= 0x01 Brec2 @ "\01\01" +Brec2/Brec2/Brec2 @ "\01" +Brec2/Brec2/Brec2 ::= eps @ "\01" +Brec2/Brec2/Brec2 ::= eps => [] @ "\01" +Brec2/Brec2/Brec2 => [] @ "\01" +Brec2/Brec2 ::= 0x01 Brec2 => [1] @ "\01" +Brec2/Brec2 => [1] @ "\01" +Brec2 ::= 0x01 Brec2 => [1 1] @ "\01" +Brec2 => [1 1] @ "\01" +Brec2 => fail: end of input expected @ "\01" +Brec2/Brec2/Brec2 ::= 0x01 Brec2 @ "\01" +Brec2/Brec2/Brec2/Brec2 @ "" +Brec2/Brec2/Brec2/Brec2 ::= eps @ "" +Brec2/Brec2/Brec2/Brec2 ::= eps => [] @ "" +Brec2/Brec2/Brec2/Brec2 => [] @ "" +Brec2/Brec2/Brec2 ::= 0x01 Brec2 => [1] @ "" +Brec2/Brec2/Brec2 => [1] @ "" +Brec2/Brec2 ::= 0x01 Brec2 => [1 1] @ "" +Brec2/Brec2 => [1 1] @ "" +Brec2 ::= 0x01 Brec2 => [1 1 1] @ "" +Brec2 => [1 1 1] @ "" +[1 1 1] +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest1 "\01\02" +Btest1 @ "\01\02" +Btest1 ::= 0x01 Brng* 0x02 @ "\01\02" +Btest1/Brng* ::= eps @ "\02" +Btest1/Brng* ::= eps => [] @ "\02" +Btest1 ::= 0x01 Brng* 0x02 => [] @ "" +Btest1 => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest1 "\01\10\12\10\02" +Btest1 @ "\01\10\12\10\02" +Btest1 ::= 0x01 Brng* 0x02 @ "\01\10\12\10\02" +Btest1/Brng* ::= eps @ "\10\12\10\02" +Btest1/Brng* ::= eps => [] @ "\10\12\10\02" +Btest1/Brng* ::= Brng Brng* @ "\10\12\10\02" +Btest1/Brng*/Brng @ "\10\12\10\02" +Btest1/Brng*/Brng ::= 0x10|...|0x20 @ "\10\12\10\02" +Btest1/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "\12\10\02" +Btest1/Brng*/Brng => 16 @ "\12\10\02" +Btest1/Brng*/Brng* ::= eps @ "\12\10\02" +Btest1/Brng*/Brng* ::= eps => [] @ "\12\10\02" +Btest1/Brng* ::= Brng Brng* => [16] @ "\12\10\02" +Btest1/Brng*/Brng* ::= Brng Brng* @ "\12\10\02" +Btest1/Brng*/Brng*/Brng @ "\12\10\02" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\12\10\02" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 18 @ "\10\02" +Btest1/Brng*/Brng*/Brng => 18 @ "\10\02" +Btest1/Brng*/Brng*/Brng* ::= eps @ "\10\02" +Btest1/Brng*/Brng*/Brng* ::= eps => [] @ "\10\02" +Btest1/Brng*/Brng* ::= Brng Brng* => [18] @ "\10\02" +Btest1/Brng* ::= Brng Brng* => [16 18] @ "\10\02" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* @ "\10\02" +Btest1/Brng*/Brng*/Brng*/Brng @ "\10\02" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\10\02" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "\02" +Btest1/Brng*/Brng*/Brng*/Brng => 16 @ "\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps @ "\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps => [] @ "\02" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* => [16] @ "\02" +Btest1/Brng*/Brng* ::= Brng Brng* => [18 16] @ "\02" +Btest1/Brng* ::= Brng Brng* => [16 18 16] @ "\02" +Btest1 ::= 0x01 Brng* 0x02 => [16 18 16] @ "" +Btest1 => [16 18 16] @ "" +[16 18 16] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest1 "\01\10\12\10" +Btest1 @ "\01\10\12\10" +Btest1 ::= 0x01 Brng* 0x02 @ "\01\10\12\10" +Btest1/Brng* ::= eps @ "\10\12\10" +Btest1/Brng* ::= eps => [] @ "\10\12\10" +Btest1/Brng* ::= Brng Brng* @ "\10\12\10" +Btest1/Brng*/Brng @ "\10\12\10" +Btest1/Brng*/Brng ::= 0x10|...|0x20 @ "\10\12\10" +Btest1/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "\12\10" +Btest1/Brng*/Brng => 16 @ "\12\10" +Btest1/Brng*/Brng* ::= eps @ "\12\10" +Btest1/Brng*/Brng* ::= eps => [] @ "\12\10" +Btest1/Brng* ::= Brng Brng* => [16] @ "\12\10" +Btest1/Brng*/Brng* ::= Brng Brng* @ "\12\10" +Btest1/Brng*/Brng*/Brng @ "\12\10" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\12\10" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 18 @ "\10" +Btest1/Brng*/Brng*/Brng => 18 @ "\10" +Btest1/Brng*/Brng*/Brng* ::= eps @ "\10" +Btest1/Brng*/Brng*/Brng* ::= eps => [] @ "\10" +Btest1/Brng*/Brng* ::= Brng Brng* => [18] @ "\10" +Btest1/Brng* ::= Brng Brng* => [16 18] @ "\10" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* @ "\10" +Btest1/Brng*/Brng*/Brng*/Brng @ "\10" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\10" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "" +Btest1/Brng*/Brng*/Brng*/Brng => 16 @ "" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps @ "" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps => [] @ "" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* => [16] @ "" +Btest1/Brng*/Brng* ::= Brng Brng* => [18 16] @ "" +Btest1/Brng* ::= Brng Brng* => [16 18 16] @ "" +Btest1/Brng*/Brng*/Brng*/Brng* ::= Brng Brng* @ "" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng @ "" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 => fail: unexpected end of input @ "" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng => fail: unexpected end of input @ "" +Btest1/Brng*/Brng*/Brng*/Brng* ::= Brng Brng* => fail: unexpected end of input @ "" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* => fail: unexpected end of input @ "" +Btest1/Brng*/Brng* ::= Brng Brng* => fail: unexpected end of input @ "" +Btest1/Brng* ::= Brng Brng* => fail: unexpected end of input @ "" +Btest1 ::= 0x01 Brng* 0x02 => fail: unexpected end of input @ "" +Btest1 => fail: unexpected end of input @ "" +4: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest1 "" +Btest1 @ "" +Btest1 ::= 0x01 Brng* 0x02 @ "" +Btest1 ::= 0x01 Brng* 0x02 => fail: unexpected end of input @ "" +Btest1 => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest1 "\01\10\12\10\02\02" +Btest1 @ "\01\10\12\10\02\02" +Btest1 ::= 0x01 Brng* 0x02 @ "\01\10\12\10\02\02" +Btest1/Brng* ::= eps @ "\10\12\10\02\02" +Btest1/Brng* ::= eps => [] @ "\10\12\10\02\02" +Btest1/Brng* ::= Brng Brng* @ "\10\12\10\02\02" +Btest1/Brng*/Brng @ "\10\12\10\02\02" +Btest1/Brng*/Brng ::= 0x10|...|0x20 @ "\10\12\10\02\02" +Btest1/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "\12\10\02\02" +Btest1/Brng*/Brng => 16 @ "\12\10\02\02" +Btest1/Brng*/Brng* ::= eps @ "\12\10\02\02" +Btest1/Brng*/Brng* ::= eps => [] @ "\12\10\02\02" +Btest1/Brng* ::= Brng Brng* => [16] @ "\12\10\02\02" +Btest1/Brng*/Brng* ::= Brng Brng* @ "\12\10\02\02" +Btest1/Brng*/Brng*/Brng @ "\12\10\02\02" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\12\10\02\02" +Btest1/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 18 @ "\10\02\02" +Btest1/Brng*/Brng*/Brng => 18 @ "\10\02\02" +Btest1/Brng*/Brng*/Brng* ::= eps @ "\10\02\02" +Btest1/Brng*/Brng*/Brng* ::= eps => [] @ "\10\02\02" +Btest1/Brng*/Brng* ::= Brng Brng* => [18] @ "\10\02\02" +Btest1/Brng* ::= Brng Brng* => [16 18] @ "\10\02\02" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* @ "\10\02\02" +Btest1/Brng*/Brng*/Brng*/Brng @ "\10\02\02" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\10\02\02" +Btest1/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 => 16 @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng => 16 @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= eps => [] @ "\02\02" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* => [16] @ "\02\02" +Btest1/Brng*/Brng* ::= Brng Brng* => [18 16] @ "\02\02" +Btest1/Brng* ::= Brng Brng* => [16 18 16] @ "\02\02" +Btest1 ::= 0x01 Brng* 0x02 => [16 18 16] @ "\02" +Btest1 => [16 18 16] @ "\02" +Btest1 => fail: end of input expected @ "\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= Brng Brng* @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng ::= 0x10|...|0x20 => fail: byte 0x10..0x20 expected @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng*/Brng => fail: byte 0x10..0x20 expected @ "\02\02" +Btest1/Brng*/Brng*/Brng*/Brng* ::= Brng Brng* => fail: byte 0x10..0x20 expected @ "\02\02" +Btest1/Brng*/Brng*/Brng* ::= Brng Brng* => fail: unexpected input @ "\02\02" +Btest1/Brng*/Brng* ::= Brng Brng* => fail: unexpected input @ "\02\02" +Btest1/Brng* ::= Brng Brng* => fail: unexpected input @ "\02\02" +Btest1 ::= 0x01 Brng* 0x02 => fail: unexpected input @ "\02\02" +Btest1 => fail: unexpected input @ "\02\02" +5: end of input expected +``` + +```sh +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest2 "\00" +Btest2 @ "\00" +Btest2 ::= 0x00 @ "\00" +Btest2 ::= 0x00 => [] @ "" +Btest2 => [] @ "" +[] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest2 "\11\12\13\00" +Btest2 @ "\11\12\13\00" +Btest2 ::= 0x00 @ "\11\12\13\00" +Btest2 ::= 0x00 => fail: byte 0x00 expected @ "\11\12\13\00" +Btest2 ::= Brng Btest2 @ "\11\12\13\00" +Btest2/Brng @ "\11\12\13\00" +Btest2/Brng ::= 0x10|...|0x20 @ "\11\12\13\00" +Btest2/Brng ::= 0x10|...|0x20 => 17 @ "\12\13\00" +Btest2/Brng => 17 @ "\12\13\00" +Btest2/Btest2 @ "\12\13\00" +Btest2/Btest2 ::= 0x00 @ "\12\13\00" +Btest2/Btest2 ::= 0x00 => fail: byte 0x00 expected @ "\12\13\00" +Btest2/Btest2 ::= Brng Btest2 @ "\12\13\00" +Btest2/Btest2/Brng @ "\12\13\00" +Btest2/Btest2/Brng ::= 0x10|...|0x20 @ "\12\13\00" +Btest2/Btest2/Brng ::= 0x10|...|0x20 => 18 @ "\13\00" +Btest2/Btest2/Brng => 18 @ "\13\00" +Btest2/Btest2/Btest2 @ "\13\00" +Btest2/Btest2/Btest2 ::= 0x00 @ "\13\00" +Btest2/Btest2/Btest2 ::= 0x00 => fail: byte 0x00 expected @ "\13\00" +Btest2/Btest2/Btest2 ::= Brng Btest2 @ "\13\00" +Btest2/Btest2/Btest2/Brng @ "\13\00" +Btest2/Btest2/Btest2/Brng ::= 0x10|...|0x20 @ "\13\00" +Btest2/Btest2/Btest2/Brng ::= 0x10|...|0x20 => 19 @ "\00" +Btest2/Btest2/Btest2/Brng => 19 @ "\00" +Btest2/Btest2/Btest2/Btest2 @ "\00" +Btest2/Btest2/Btest2/Btest2 ::= 0x00 @ "\00" +Btest2/Btest2/Btest2/Btest2 ::= 0x00 => [] @ "" +Btest2/Btest2/Btest2/Btest2 => [] @ "" +Btest2/Btest2/Btest2 ::= Brng Btest2 => [19] @ "" +Btest2/Btest2/Btest2 => [19] @ "" +Btest2/Btest2 ::= Brng Btest2 => [18 19] @ "" +Btest2/Btest2 => [18 19] @ "" +Btest2 ::= Brng Btest2 => [17 18 19] @ "" +Btest2 => [17 18 19] @ "" +[17 18 19] +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest2 "" +Btest2 @ "" +Btest2 ::= 0x00 @ "" +Btest2 ::= 0x00 => fail: unexpected end of input @ "" +Btest2 ::= Brng Btest2 @ "" +Btest2/Brng @ "" +Btest2/Brng ::= 0x10|...|0x20 @ "" +Btest2/Brng ::= 0x10|...|0x20 => fail: unexpected end of input @ "" +Btest2/Brng => fail: unexpected end of input @ "" +Btest2 ::= Brng Btest2 => fail: unexpected end of input @ "" +Btest2 => fail: unexpected end of input @ "" +0: unexpected end of input +$ ../src/exe-watsup/main.exe test.watsup --trace-parse --parse-string Btest2 "\00\00" +Btest2 @ "\00\00" +Btest2 ::= 0x00 @ "\00\00" +Btest2 ::= 0x00 => [] @ "\00" +Btest2 => [] @ "\00" +Btest2 => fail: end of input expected @ "\00" +Btest2 ::= Brng Btest2 @ "\00\00" +Btest2/Brng @ "\00\00" +Btest2/Brng ::= 0x10|...|0x20 @ "\00\00" +Btest2/Brng ::= 0x10|...|0x20 => fail: byte 0x10..0x20 expected @ "\00\00" +Btest2/Brng => fail: byte 0x10..0x20 expected @ "\00\00" +Btest2 ::= Brng Btest2 => fail: byte 0x10..0x20 expected @ "\00\00" +Btest2 => fail: unexpected input @ "\00\00" +1: end of input expected +``` + + +# Types + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bnumtype "\7f" +I32_numtype +``` + +# Values + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bu32 "\00" "\80\00" "\80\80\80\80\00" "\80\80\80\80\80\00" "\81\03" +u32(0) +u32(0) +u32(0) +5: unexpected input +u32(385) +``` + +# Functions + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bfunc "\00\0B" +([], []) +``` + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bcode "\02\00\0B" +([], []) +``` + +# Modules + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bmagic "\00\61\73\6D" +() +``` + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bcustomsec "\00\01\00" "\00\07\03boo\01\02\03" +() +() +``` + +```sh +$ ../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse-string Bmodule "\00\61\73\6D\01\00\00\00" +MODULE_module([], [], [], [], [], [], [], [], ?(), []) +``` + +```sh +$ #../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup --parse Bmodule ../test-interpreter/sample.wasm +``` diff --git a/spectec/test-parser/dune b/spectec/test-parser/dune new file mode 100644 index 0000000000..666ea38811 --- /dev/null +++ b/spectec/test-parser/dune @@ -0,0 +1,9 @@ +(mdx + (libraries spectec) + (deps + (file ../src/exe-watsup/main.exe) + (glob_files_rec ../spec/*) + (glob_files *.watsup) + ) + (files TEST.md) +) diff --git a/spectec/test-parser/test.watsup b/spectec/test-parser/test.watsup new file mode 100644 index 0000000000..b80c50d7b6 --- /dev/null +++ b/spectec/test-parser/test.watsup @@ -0,0 +1,53 @@ +grammar Teps : nat = eps => 42 + +grammar Tbyte : nat = i:0x3A => i + +grammar Ttext : () = "AÄÜ" => () + +grammar Bseq : nat = i:0x03 j:0x04 eps k:0x02 => $(i + j * k) + +grammar Tseq : () = eps "A" eps "BC" "D" => () + +grammar Talt : () = "A" | "BC" | "D" => () +grammar Talt2 : () = "A" | "B" | "BC" | "A" | "DE" | "" => () + +grammar Tprod : nat = "A" => 1 | "BC" => 2 | "D" => 3 | "" => 0 + +grammar Brng : nat = i:0x10 | ... | i:0x20 => i + +var ns : nat* +var no : nat? + +grammar Bstar : nat* = ns:0x01* => ns +grammar Bstar2 : nat* = is*:0x01* => is* +grammar Bstar3 : nat* = (is:0x01)* => is* + +grammar Tstar : () = "AB"* => () + +grammar Bplus : nat* = ns:0x01+ => ns +grammar Bplus2 : nat* = i*:0x01+ => i* +grammar Bplus3 : nat* = (i:0x01)+ => i+ + +grammar Tplus : () = "ABC"+ => () + +grammar Bquest : nat? = no:0x01? => no +grammar Bquest2 : nat? = i?:0x01? => i? +grammar Bquest3 : nat? = (i:0x01)? => i? + +grammar Tquest : () = "ABCD"? => () + +grammar Bnth : nat* = ns:0x01^(2*2) => ns +grammar Bnth2 : nat* = i*:0x01^(2*2) => i* +grammar Bnth3 : nat* = (i:0x01)^(2*2) => i^(2*2) + +grammar Tnth : () = "ABC"^(7-4) => () + +grammar Bdef : nat = i:0x03 j:0x04 => $(i + j) +grammar Bvar : nat = i:0x01 k:Bdef j:0x10 => $(i*j + k) + +grammar Brec : nat* = eps => eps | 0x01 ns:Brec => 1 ns +grammar Brec2 : nat* = eps => eps | 0x01 i*:Brec2 => 1 i* + +grammar Btest1 : nat* = 0x01 i*:Brng* 0x02 => i* + +grammar Btest2 : nat* = 0x00 => eps | i:Brng j*:Btest2 => i j*