@@ -23,6 +23,27 @@ rule token = parse
2323 | eof { EOF }
2424
2525{
26+
27+ module Dynarray = struct
28+ type 'a t = { mutable size : int ;
29+ mutable arr : 'a array ;
30+ default : 'a }
31+ let empty default = { size= 0 ; arr= Array. make 10 default; default= default }
32+ let length arr = arr.size
33+ let get arr idx = Array. get arr.arr idx
34+ let add arr str =
35+ let idx = arr.size in
36+ arr.size < - idx + 1 ;
37+ (if idx = Array. length arr.arr then
38+ let new_arr = Array. make (idx * 2 ) arr.default in
39+ Array. blit arr.arr 0 new_arr 0 idx;
40+ arr.arr < - new_arr
41+ else () );
42+ Array. set arr.arr idx str
43+ end
44+
45+ type 'a dynarray = 'a Dynarray .t
46+
2647let parse_k (str : string ) =
2748 let lexbuf = Lexing. from_string str in Parser. top token lexbuf
2849
@@ -41,7 +62,7 @@ let parse_k_binary_int (s: char Stream.t) : int =
4162 let four = Char. code (Stream. next s) in
4263 (((((one * 256 ) + two) * 256 ) + three) * 256 ) + four
4364
44- let parse_k_binary_string (s : char Stream.t ) (interns : string list ref ) : string =
65+ let parse_k_binary_string (s : char Stream.t ) (interns : string dynarray ) : string =
4566 let idx_in_interns = parse_k_binary_int s in
4667 if idx_in_interns = 0 then
4768 let len = parse_k_binary_int s in
@@ -51,30 +72,33 @@ let parse_k_binary_string (s: char Stream.t) (interns: string list ref) : string
5172 Bytes. set bytes i (Stream. next s)
5273 done ;
5374 let str = Bytes. to_string bytes in
54- interns : = ! interns @ [ str] ;
75+ Dynarray. add interns str;
5576 str
5677 else
57- List. nth ! interns ((List .! interns) - idx_in_interns)
78+ Dynarray. get interns ((Dynarray .- idx_in_interns)
5879
59- let rec parse_k_binary_term (s : char Stream.t ) (stack : k Stack.t ) (interns : string list ref ) : k =
80+ let rec parse_k_binary_term (s : char Stream.t ) (stack : k Stack.t ) (interns : string dynarray ) ( k_interns : k dynarray ) : k =
6081 match Char. code (Stream. next s) with
6182| 1 -> (* ktoken *)
6283 let str = parse_k_binary_string s interns in
6384 let sort = parse_k_binary_string s interns in
6485 Stack. push [ktoken(parse_sort sort)(str)] stack;
65- parse_k_binary_term s stack interns
86+ Dynarray. add k_interns (Stack. top stack);
87+ parse_k_binary_term s stack interns k_interns
6688| 2 -> (* kapply *)
6789 let lbl = parse_k_binary_string s interns in
6890 ignore(Stream. next s);
6991 let arity = parse_k_binary_int s in
7092 let items = parse_k_binary_stack stack arity [] in
7193 Stack. push (Def. eval (KApply ((parse_klabel lbl), items)) [] ) stack;
72- parse_k_binary_term s stack interns
94+ Dynarray. add k_interns (Stack. top stack);
95+ parse_k_binary_term s stack interns k_interns
7396| 3 -> (* ksequence *)
7497 let arity = parse_k_binary_int s in
7598 let items = parse_k_binary_stack stack arity [] in
7699 Stack. push (List. flatten items) stack;
77- parse_k_binary_term s stack interns
100+ Dynarray. add k_interns (Stack. top stack);
101+ parse_k_binary_term s stack interns k_interns
78102| 4 -> (* kvariable *)
79103 failwith " Unsupported: Variables in subject"
80104| 5 -> (* krewrite *)
@@ -83,17 +107,23 @@ let rec parse_k_binary_term (s: char Stream.t) (stack: k Stack.t) (interns: stri
83107 let lbl = parse_k_binary_string s interns in
84108 ignore(Stream. next s);
85109 Stack. push [InjectedKLabel (parse_klabel lbl)] stack;
86- parse_k_binary_term s stack interns
110+ Dynarray. add k_interns (Stack. top stack);
111+ parse_k_binary_term s stack interns k_interns
87112| 7 -> (* end *)
88113 Stack. pop stack
114+ | 8 -> (* back reference *)
115+ let idx = parse_k_binary_int s in
116+ Stack. push (Dynarray. get k_interns ((Dynarray. length k_interns) - idx)) stack;
117+ Dynarray. add k_interns (Stack. top stack);
118+ parse_k_binary_term s stack interns k_interns
89119| _ -> failwith " Unexpected term code in binary KAST"
90120
91121let parse_k_binary (s : char Stream.t ) : k =
92122 if Stream. npeek 5 s <> ['\x7f' ; 'K' ; 'A' ; 'S' ; 'T' ] then failwith " Invalid binary KAST" else
93123 for i = 1 to 5 do Stream. junk s done ;
94- if Stream. npeek 3 s <> ['\x04' ; '\x00' ; '\x00' ] then failwith " Unsupported KAST version" else
124+ if Stream. npeek 3 s <> ['\x04' ; '\x00' ; '\x01' ] && Stream. npeek 3 s <> [ '\x04' ; '\x00' ; '\ x00'then failwith " Unsupported KAST version" else
95125 for i = 1 to 3 do Stream. junk s done ;
96- parse_k_binary_term s (Stack. create () ) (ref [ ]
126+ parse_k_binary_term s (Stack. create () ) (Dynarray. empty " " ) ( Dynarray. empty [ Bottom ])
97127
98128let parse_k_binary_string (s : string ) : k =
99129 parse_k_binary (Stream. of_string s)
0 commit comments