unify shift and reduce evaluation actions
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13740 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Frédéric Tuong
parent
f9c7a6dea5
commit
4edb931cb3
|
|
@ -146,21 +146,21 @@ in end
|
|||
section \<open>\<close>
|
||||
|
||||
ML\<open>
|
||||
fun reduce make_string f (_, (value, pos1, pos2)) _ thy =
|
||||
fun print_top make_string f _ (_, (value, pos1, pos2)) _ thy =
|
||||
let
|
||||
val () = writeln (make_string value)
|
||||
val () = Position.reports_text [((Position.range (pos1, pos2)
|
||||
|> Position.range_position, Markup.intensify), "")]
|
||||
in f thy end
|
||||
|
||||
fun reduce' _ f (_, (_, pos1, pos2)) env thy =
|
||||
fun print_top' _ f _ (_, (_, pos1, pos2)) env thy =
|
||||
let
|
||||
val () = Position.reports_text [((Position.range (pos1, pos2)
|
||||
|> Position.range_position, Markup.intensify), "")]
|
||||
val () = writeln ("ENV " ^ C_Env.string_of env)
|
||||
in f thy end
|
||||
|
||||
fun shift s make_string (stack, _) thy =
|
||||
fun print_stack s make_string stack _ _ thy =
|
||||
let
|
||||
val () = warning ("SHIFT " ^ (case s of NONE => "" | SOME s => "\"" ^ s ^ "\" ") ^ Int.toString (length stack - 1) ^ " +1 ")
|
||||
val () = stack
|
||||
|
|
@ -170,20 +170,20 @@ fun shift s make_string (stack, _) thy =
|
|||
|> app (fn (i, (value, pos1, pos2)) => writeln (" " ^ Int.toString (length stack - i) ^ " " ^ make_string value ^ " " ^ Position.here pos1 ^ " " ^ Position.here pos2))
|
||||
in thy end
|
||||
|
||||
fun shift' s _ (stack, env) thy =
|
||||
fun print_stack' s _ stack _ env thy =
|
||||
let
|
||||
val () = warning ("SHIFT " ^ (case s of NONE => "" | SOME s => "\"" ^ s ^ "\" ") ^ Int.toString (length stack - 1) ^ " +1 ")
|
||||
val () = writeln ("ENV " ^ C_Env.string_of env)
|
||||
in thy end
|
||||
\<close>
|
||||
|
||||
setup \<open>ML_Antiquotation.inline @{binding reduce}
|
||||
(Args.context >> K ("reduce " ^ ML_Pretty.make_string_fn ^ " I"))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding reduce'}
|
||||
(Args.context >> K ("reduce' " ^ ML_Pretty.make_string_fn ^ " I"))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding shift}
|
||||
(Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("shift " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding shift'}
|
||||
(Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("shift' " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding print_top}
|
||||
(Args.context >> K ("print_top " ^ ML_Pretty.make_string_fn ^ " I"))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding print_top'}
|
||||
(Args.context >> K ("print_top' " ^ ML_Pretty.make_string_fn ^ " I"))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding print_stack}
|
||||
(Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("print_stack " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\<close>
|
||||
setup \<open>ML_Antiquotation.inline @{binding print_stack'}
|
||||
(Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("print_stack' " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\<close>
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -106,18 +106,18 @@ section \<open>Antiquotations\<close>
|
|||
subsection \<open>Actions on the Parsing Stack\<close>
|
||||
|
||||
C \<comment> \<open>Closing C comments \<open>*/\<close> must close anything, even when editing ML code\<close> \<open>
|
||||
int a = (((0 //@ (* inline *) !ML \<open>fn _ => fn context => let in (* */ *) context end\<close>
|
||||
/*@ !ML \<open>K I\<close> (* * / *) */
|
||||
int a = (((0 //@ (* inline *) ML \<open>fn _ => fn _ => fn _ => fn context => let in (* */ *) context end\<close>
|
||||
/*@ ML \<open>(K o K o K) I\<close> (* * / *) */
|
||||
)));
|
||||
\<close>
|
||||
|
||||
C \<comment> \<open>With \<open>!\<close>, execution during SHIFT actions\<close> \<open>
|
||||
int a = (((0))); /*@ !ML \<open>@{shift}\<close> */
|
||||
int a = (((0))); /*@ ML \<open>@{print_stack}\<close> */
|
||||
\<close>
|
||||
|
||||
C \<comment> \<open>Without \<open>!\<close>, execution during REDUCE actions\<close> \<open>
|
||||
int a = (((0
|
||||
+ 5))) /*@ ML \<open>fn (_, (value, pos1, pos2)) => fn _ => fn context =>
|
||||
+ 5))) /*@@ ML \<open>fn _ => fn (_, (value, pos1, pos2)) => fn _ => fn context =>
|
||||
let
|
||||
val () = writeln (@{make_string} value)
|
||||
val () = Position.reports_text [((Position.range (pos1, pos2)
|
||||
|
|
@ -129,23 +129,23 @@ float b = 7 / 3;
|
|||
\<close>
|
||||
|
||||
C \<comment> \<open>Inline comments with antiquotations\<close> \<open>
|
||||
/*@ !ML\<open>K (fn x => K x @{con\
|
||||
/*@ ML\<open>(K o K o K) (fn x => K x @{con\
|
||||
text (**)})\<close> */ // break of line activated everywhere (also in antiquotations)
|
||||
int a = 0; //\
|
||||
@ !ML\<open>K (fn x => K x @{term \<open>a \
|
||||
@ ML\<open>(K o K o K) (fn x => K x @{term \<open>a \
|
||||
+ b (* (**) *\
|
||||
\
|
||||
)\<close>})\<close>
|
||||
\<close>
|
||||
|
||||
C \<comment> \<open>Positional navigation: pointing to deeper sub-trees in the stack\<close> \<open>
|
||||
int b = 7 / (3) * 50 /*@@@@ ML \<open>@{reduce}\<close>
|
||||
int b = 7 / (3) * 50 /*@@@@@ ML \<open>@{print_top}\<close>
|
||||
*/;
|
||||
\<close>
|
||||
|
||||
C \<comment> \<open>Positional navigation: pointing to sub-trees situated after any part of the code\<close> \<open>
|
||||
int b = 7 / (3) * 50;
|
||||
/*@+++@ ML \<open>@{reduce}\<close>*/
|
||||
/*@+++@@ ML \<open>@{print_top}\<close>*/
|
||||
long long f (int a) {
|
||||
while (0) { return 0; }
|
||||
}
|
||||
|
|
@ -159,7 +159,7 @@ int a = 0;
|
|||
/** ML (* Errors: Turned into tracing report information *)
|
||||
*/
|
||||
|
||||
/** ML \<open>fn _ => fn _ => I\<close> (* An example of correct syntax accepted as usual *)
|
||||
/** ML \<open>fn _ => fn _ => fn _ => I\<close> (* An example of correct syntax accepted as usual *)
|
||||
*/
|
||||
\<close>
|
||||
|
||||
|
|
@ -184,8 +184,7 @@ datatype antiq_hol = Invariant of string (* term *)
|
|||
val scan_ident = Scan.one C_Token.is_ident >> (fn tok => (C_Token.content_of tok, C_Token.pos_of tok))
|
||||
val scan_sym_ident_not_stack = Scan.one (fn c => C_Token.is_sym_ident c andalso
|
||||
not (C_Token.is_stack1 c) andalso
|
||||
not (C_Token.is_stack2 c) andalso
|
||||
not (C_Token.is_exec_shift c))
|
||||
not (C_Token.is_stack2 c))
|
||||
>> (fn tok => (C_Token.content_of tok, C_Token.pos_of tok))
|
||||
fun command cmd scan f =
|
||||
C_Annot_Syntax.command' cmd "" (K (Scan.option (Scan.one C_Token.is_colon) -- (scan >> f)
|
||||
|
|
@ -325,14 +324,14 @@ subsection \<open>Mixing Together Any Types of Antiquotations\<close>
|
|||
|
||||
C \<comment> \<open>Permissive Types of Antiquotations\<close> \<open>
|
||||
int a = 0;
|
||||
/*@ ML \<open>fn _ => fn _ => I\<close>
|
||||
/*@ ML \<open>fn _ => fn _ => fn _ => I\<close>
|
||||
ML (* Parsing error of a single command does not propagate to other commands *)
|
||||
ML \<open>fn _ => fn _ => I\<close>
|
||||
ML \<open>fn _ => fn _ => fn _ => I\<close>
|
||||
context
|
||||
*/
|
||||
/** ML \<open>fn _ => fn _ => I\<close>
|
||||
/** ML \<open>fn _ => fn _ => fn _ => I\<close>
|
||||
ML (* Parsing error of a single command does not propagate to other commands *)
|
||||
ML \<open>fn _ => fn _ => I\<close>
|
||||
ML \<open>fn _ => fn _ => fn _ => I\<close>
|
||||
context
|
||||
*/
|
||||
|
||||
|
|
@ -364,19 +363,19 @@ declare[[C_parser_trace]]
|
|||
C \<comment> \<open>Arbitrary interleaving of effects\<close> \<open>
|
||||
int x /** OWNED_BY foo */, hh /*@
|
||||
MODIFIES: [*] x
|
||||
!ML \<open>@{shift "evaluation of 2_shift"}\<close>
|
||||
+++++@ ML \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "2_reduce"\<close>
|
||||
ML \<open>@{print_stack "evaluation of 2_print_stack"}\<close>
|
||||
+++++@@ ML \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "2_print_top"\<close>
|
||||
OWNED_BY bar
|
||||
ML \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "1_reduce"\<close>
|
||||
!ML \<open>@{shift "evaluation of 1_shift"}\<close>
|
||||
@ML \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "1_print_top"\<close>
|
||||
ML \<open>@{print_stack "evaluation of 1_print_stack"}\<close>
|
||||
*/, z;
|
||||
|
||||
int b = 0;
|
||||
\<close>
|
||||
|
||||
C \<comment> \<open>Arbitrary interleaving of effects: \<open>ML\<close> vs \<open>ML'\<close>\<close> \<open>
|
||||
int b,c,d/*@ ML \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "3_reduce"\<close> */,e = 0; /*@ ML \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "4_reduce"\<close> */
|
||||
int b,c,d/*@ ML' \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "6_reduce"\<close> */,e = 0; /*@ ML' \<open>fn x => fn env => @{reduce} x env #> add_ex "evaluation of " "5_reduce"\<close> */
|
||||
C \<comment> \<open>Arbitrary interleaving of effects: \<open>ML\<close> vs \<open>ML_reverse\<close>\<close> \<open>
|
||||
int b,c,d/*@@ ML \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "3_print_top"\<close> */,e = 0; /*@@ ML \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "4_print_top"\<close> */
|
||||
int b,c,d/*@@ ML_reverse \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "6_print_top"\<close> */,e = 0; /*@@ ML_reverse \<open>fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "5_print_top"\<close> */
|
||||
\<close>
|
||||
|
||||
subsection \<open>Reporting of Positions and Contextual Update of Environment\<close>
|
||||
|
|
@ -388,7 +387,7 @@ declare [[C_lexer_trace = false]]
|
|||
|
||||
C \<comment> \<open>Reporting of Positions\<close> \<open>
|
||||
typedef int i, j;
|
||||
/*@ ML \<open>@{reduce'}\<close> */ //@ +++++ ML \<open>@{reduce'}\<close>
|
||||
/*@@ ML \<open>@{print_top'}\<close> */ //@ +++++@ ML \<open>@{print_top'}\<close>
|
||||
int j = 0;
|
||||
typedef int i, j;
|
||||
j jj1 = 0;
|
||||
|
|
@ -421,7 +420,7 @@ val C' = C_Outer_Syntax.C' (fn _ => fn _ => fn pos =>
|
|||
C \<comment> \<open>Nesting C code without propagating the C environment\<close> \<open>
|
||||
int a = 0;
|
||||
int b = 7 / (3) * 50
|
||||
/*@@@@ ML \<open>fn _ => fn _ =>
|
||||
/*@@@@@ ML \<open>fn _ => fn _ => fn _ =>
|
||||
C \<open>int b = a + a + a + a + a + a + a
|
||||
;\<close> \<close> */;
|
||||
\<close>
|
||||
|
|
@ -429,7 +428,7 @@ int b = 7 / (3) * 50
|
|||
C \<comment> \<open>Nesting C code and propagating the C environment\<close> \<open>
|
||||
int a = 0;
|
||||
int b = 7 / (3) * 50
|
||||
/*@@@@ ML \<open>fn _ => fn env =>
|
||||
/*@@@@@ ML \<open>fn _ => fn _ => fn env =>
|
||||
C' env \<open>int b = a + a + a + a + a + a + a
|
||||
;\<close> \<close> */;
|
||||
\<close>
|
||||
|
|
@ -439,14 +438,14 @@ typedef int i, j;
|
|||
int j = 0;
|
||||
typedef int i, j;
|
||||
j jj1 = 0;
|
||||
j jj = jj1; /*@ ML \<open>fn _ => fn _ => show_env "POSITION 0"\<close> ML \<open>@{reduce'}\<close> */
|
||||
typedef int k; /*@ ML \<open>fn _ => fn env =>
|
||||
C' env \<open>k jj = jj; //@ ML \<open>@{reduce'}\<close>
|
||||
j jj = jj1; /*@@ ML \<open>fn _ => fn _ => fn _ => show_env "POSITION 0"\<close> @ML \<open>@{print_top'}\<close> */
|
||||
typedef int k; /*@@ ML \<open>fn _ => fn _ => fn env =>
|
||||
C' env \<open>k jj = jj; //@@ ML \<open>@{print_top'}\<close>
|
||||
k jj = jj + jj1;
|
||||
typedef k l; //@ ML \<open>@{reduce'}\<close>\<close>
|
||||
typedef k l; //@@ ML \<open>@{print_top'}\<close>\<close>
|
||||
#> show_env "POSITION 1"\<close> */
|
||||
j j = jj1 + jj; //@ ML \<open>@{reduce'}\<close>
|
||||
typedef i j; /*@ ML \<open>fn _ => fn _ => show_env "POSITION 2"\<close> */
|
||||
j j = jj1 + jj; //@@ ML \<open>@{print_top'}\<close>
|
||||
typedef i j; /*@@ ML \<open>fn _ => fn _ => fn _ => show_env "POSITION 2"\<close> */
|
||||
typedef i j;
|
||||
typedef i j;
|
||||
i jj = jj;
|
||||
|
|
|
|||
|
|
@ -187,9 +187,6 @@ val is_stack1 = fn Token (_, (Token.Sym_Ident, l)) => forall (fn (s, _) => s = "
|
|||
val is_stack2 = fn Token (_, (Token.Sym_Ident, l)) => forall (fn (s, _) => s = "@") l
|
||||
| _ => false;
|
||||
|
||||
val is_exec_shift = fn Token (_, (Token.Sym_Ident, l)) => forall (fn (s, _) => s = "!") l
|
||||
| _ => false;
|
||||
|
||||
val is_modifies_star = fn Token (_, (Token.Sym_Ident, l)) => Symbol_Pos.content l = "[*]"
|
||||
| _ => false;
|
||||
|
||||
|
|
@ -254,7 +251,7 @@ fun completion_report tok =
|
|||
fun reports keywords tok =
|
||||
if is_command tok then
|
||||
keyword_reports tok (command_markups keywords (content_of tok))
|
||||
else if is_stack1 tok orelse is_stack2 tok orelse is_exec_shift tok then
|
||||
else if is_stack1 tok orelse is_stack2 tok then
|
||||
keyword_reports tok [Markup.keyword2 |> Markup.keyword_properties]
|
||||
else if is_kind Token.Keyword tok then
|
||||
keyword_reports tok
|
||||
|
|
@ -356,7 +353,6 @@ fun scan_token keywords = Scanner.!!! "bad input"
|
|||
$$$ ":" >> pair Token.Keyword ||
|
||||
Scan.repeats1 ($$$ "+") >> pair Token.Sym_Ident ||
|
||||
Scan.repeats1 ($$$ "@") >> pair Token.Sym_Ident ||
|
||||
$$$ "!" >> pair Token.Sym_Ident ||
|
||||
$$$ "[" @@@ $$$ "*" @@@ $$$ "]" >> pair Token.Sym_Ident)) >> uncurry token);
|
||||
|
||||
fun recover msg =
|
||||
|
|
@ -588,7 +584,7 @@ fun err_dup_command name ps =
|
|||
(* command parsers *)
|
||||
|
||||
datatype command_parser =
|
||||
Parser of (Symbol_Pos.T list * Symbol_Pos.T list, C_Token.T) either -> eval_time c_parser;
|
||||
Parser of Symbol_Pos.T list * Symbol_Pos.T list -> eval_time c_parser;
|
||||
|
||||
datatype command = Command of
|
||||
{comment: string,
|
||||
|
|
@ -670,8 +666,7 @@ fun command' (name, pos) comment parse =
|
|||
(* parse commands *)
|
||||
|
||||
val before_command =
|
||||
Scan.one C_Token.is_exec_shift >> Right
|
||||
|| C_Token.scan_stack C_Token.is_stack1 -- C_Token.scan_stack C_Token.is_stack2 >> Left
|
||||
C_Token.scan_stack C_Token.is_stack1 -- C_Token.scan_stack C_Token.is_stack2
|
||||
|
||||
fun parse_command thy =
|
||||
Scan.ahead (before_command |-- C_Parse.position C_Parse.command_) :|-- (fn (name, _) =>
|
||||
|
|
@ -969,36 +964,35 @@ fun expression range name constraint body ants context = context |>
|
|||
|
||||
fun command dir name =
|
||||
C_Annot_Syntax.command' name ""
|
||||
(fn Left stack =>
|
||||
(fn stack =>
|
||||
C_Parse.range C_Parse.ML_source >>
|
||||
(fn (src, range) =>
|
||||
(fn f => Reduce (stack, (range, dir, f)))
|
||||
(fn rule =>
|
||||
let val hook = "hook"
|
||||
in expression
|
||||
(Input.range_of src)
|
||||
hook
|
||||
(MlyValue.type_reduce rule ^ " stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")
|
||||
("fn context => \
|
||||
\let val (stack, env_lang) = Stack_Data_Lang.get context \
|
||||
\in " ^ hook ^ " (stack |> hd |> map_svalue0 MlyValue.reduce" ^ Int.toString rule ^ ") env_lang end context")
|
||||
(ML_Lex.read_source false src)
|
||||
end))
|
||||
| Right _ =>
|
||||
C_Parse.range C_Parse.ML_source >>
|
||||
(fn (src, range) =>
|
||||
(Shift o (fn x => (range, dir, x)))
|
||||
let val setup = "setup"
|
||||
in expression
|
||||
(Input.range_of src)
|
||||
setup
|
||||
"Stack_Data_Lang.T -> Context.generic -> Context.generic"
|
||||
("fn context => " ^ setup ^ " (Stack_Data_Lang.get context) context")
|
||||
(ML_Lex.read_source false src) end))
|
||||
(fn f => Once (stack, (range, dir, f)))
|
||||
(fn NONE =>
|
||||
let val setup = "setup"
|
||||
in expression
|
||||
(Input.range_of src)
|
||||
setup
|
||||
"stack_data -> stack_data_elem -> C_Env.env_lang -> Context.generic -> Context.generic"
|
||||
("fn context => \
|
||||
\let val (stack, env_lang) = Stack_Data_Lang.get context \
|
||||
\in " ^ setup ^ " stack (stack |> hd) env_lang end context")
|
||||
(ML_Lex.read_source false src) end
|
||||
| SOME rule =>
|
||||
let val hook = "hook"
|
||||
in expression
|
||||
(Input.range_of src)
|
||||
hook
|
||||
("stack_data -> " ^ MlyValue.type_reduce rule ^ " stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")
|
||||
("fn context => \
|
||||
\let val (stack, env_lang) = Stack_Data_Lang.get context \
|
||||
\in " ^ hook ^ " stack (stack |> hd |> map_svalue0 MlyValue.reduce" ^ Int.toString rule ^ ") env_lang end context")
|
||||
(ML_Lex.read_source false src)
|
||||
end)))
|
||||
|
||||
in
|
||||
val _ = Theory.setup ( command Bottom_up ("ML", \<^here>)
|
||||
#> command Top_down ("ML'", \<^here>))
|
||||
#> command Top_down ("ML_reverse", \<^here>))
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -48,16 +48,17 @@ ML\<open>
|
|||
structure C_Annot_Result =
|
||||
struct
|
||||
|
||||
datatype eval_tree = Bottom_up (*during parsing*) | Top_down (*after parsing*)
|
||||
datatype env_propagation = Bottom_up (*during parsing*) | Top_down (*after parsing*)
|
||||
|
||||
type 'fun eval_at = Position.range * eval_tree * 'fun
|
||||
type eval_at_reduce = (int (*reduce rule number*) -> Context.generic -> Context.generic) eval_at
|
||||
type eval_node = Position.range
|
||||
* env_propagation
|
||||
* (int (*reduce rule number*) option (* NONE: shift action *)
|
||||
-> Context.generic -> Context.generic)
|
||||
|
||||
datatype eval_time = Shift of (Context.generic -> Context.generic) eval_at
|
||||
| Reduce of (Symbol_Pos.T list (* length = number of tokens to advance *)
|
||||
* Symbol_Pos.T list (* length = number of steps back in stack *))
|
||||
* eval_at_reduce
|
||||
| Never
|
||||
datatype eval_time = Once of (Symbol_Pos.T list (* length = number of tokens to advance *)
|
||||
* Symbol_Pos.T list (* length = number of steps back in stack *))
|
||||
* eval_node
|
||||
| Never (* to be manually treated by the semantic back-end, and analyzed there *)
|
||||
|
||||
datatype antiq_language = Antiq_stack of eval_time
|
||||
| Antiq_none of C_Lex.token
|
||||
|
|
@ -99,7 +100,7 @@ datatype rule_type = Void
|
|||
| Reduce of int
|
||||
|
||||
type ('LrTable_state, 'svalue0, 'pos) rule_reduce =
|
||||
((int * ('LrTable_state * ('svalue0 * 'pos * 'pos)) * env_lang) * eval_at_reduce) list
|
||||
((int * ('LrTable_state * ('svalue0 * 'pos * 'pos)) * env_lang) * eval_node) list
|
||||
|
||||
type ('LrTable_state, 'svalue0, 'pos) rule_ml =
|
||||
{ rule_pos : 'pos * 'pos
|
||||
|
|
@ -118,7 +119,7 @@ type T = { env_lang : env_lang
|
|||
, env_tree : env_tree
|
||||
, rule_output : rule_output
|
||||
, rule_input : class_Pos list * int
|
||||
, stream_hook : (Symbol_Pos.T list * Symbol_Pos.T list * eval_at_reduce) list list
|
||||
, stream_hook : (Symbol_Pos.T list * Symbol_Pos.T list * eval_node) list list
|
||||
, stream_lang : (C_Antiquote.antiq * antiq_language list) stream }
|
||||
|
||||
(**)
|
||||
|
|
|
|||
|
|
@ -441,7 +441,7 @@ type ('LrTable_state, 'a, 'Position_T) stack_elem0 = 'LrTable_state * ('a * 'Pos
|
|||
type ('LrTable_state, 'a, 'Position_T) stack0 = ('LrTable_state, 'a, 'Position_T) stack_elem0 list
|
||||
type ('LrTable_state, 'a, 'Position_T) stack' =
|
||||
('LrTable_state, 'a, 'Position_T) stack0
|
||||
* eval_at_reduce list list
|
||||
* eval_node list list
|
||||
* ('Position_T * 'Position_T) list
|
||||
* ('LrTable_state, 'a, 'Position_T) C_Env.rule_ml C_Env.tree list
|
||||
type cString = CString
|
||||
|
|
@ -728,11 +728,13 @@ which interprets a automata-like format generated from smlyacc.\<close>
|
|||
|
||||
ML\<open>
|
||||
type 'a stack_elem = (LrTable.state, 'a, Position.T) stack_elem0
|
||||
type stack_data = (LrTable.state, StrictCLrVals.Tokens.svalue0, Position.T) stack0
|
||||
type stack_data_elem = (LrTable.state, StrictCLrVals.Tokens.svalue0, Position.T) stack_elem0
|
||||
|
||||
fun map_svalue0 f (st, (v, pos1, pos2)) = (st, (f v, pos1, pos2))
|
||||
|
||||
structure Stack_Data_Lang = Generic_Data
|
||||
(type T = (LrTable.state, StrictCLrVals.Tokens.svalue0, Position.T) stack0 * C_Env.env_lang
|
||||
(type T = stack_data * C_Env.env_lang
|
||||
val empty = ([], C_Env.empty_env_lang)
|
||||
val extend = I
|
||||
val merge = #2)
|
||||
|
|
@ -762,20 +764,37 @@ fun makeLexer ((stack, stack_ml, stack_pos, stack_tree), arg) =
|
|||
let val (arg, stack_ml) =
|
||||
case #stream_hook arg
|
||||
of l :: ls =>
|
||||
( C_Env.map_stream_hook (K ls) arg
|
||||
, fold_rev (fn (_, syms, ml_exec) => fn stack_ml =>
|
||||
let
|
||||
val () =
|
||||
if length stack_ml = 1 orelse length stack_ml - length syms = 1 then
|
||||
warning ("Unevaluated code as the hook is pointing to an internal initial value" ^ Position.here (ml_exec |> #1 |> Position.range_position))
|
||||
else ()
|
||||
val () =
|
||||
if length stack_ml - length syms <= 0 then
|
||||
error ("Maximum depth reached (" ^ Int.toString (length syms - length stack_ml + 1) ^ " in excess)" ^ Position.here (Symbol_Pos.range syms |> Position.range_position))
|
||||
else ()
|
||||
in nth_map (length syms) (cons ml_exec) stack_ml end)
|
||||
l
|
||||
stack_ml)
|
||||
(arg, stack_ml)
|
||||
|> fold_rev
|
||||
(fn (_, syms, ml_exec) => fn (arg, stack_ml) =>
|
||||
let
|
||||
val len = length syms
|
||||
in
|
||||
if len = 0 then
|
||||
case ml_exec of
|
||||
(_, Bottom_up, exec) =>
|
||||
( C_Env_Ext.map_context (I #> Stack_Data_Lang.put (stack, #env_lang arg)
|
||||
#> exec NONE)
|
||||
arg
|
||||
, stack_ml)
|
||||
| ((pos, _), _, _) =>
|
||||
( C_Env_Ext.map_context (fn _ => error ("Style of evaluation not yet implemented" ^ Position.here pos)) arg
|
||||
, stack_ml)
|
||||
else
|
||||
let
|
||||
val len = len - 1
|
||||
val () =
|
||||
if length stack_ml = 1 orelse length stack_ml - len = 1 then
|
||||
warning ("Unevaluated code as the hook is pointing to an internal initial value" ^ Position.here (ml_exec |> #1 |> Position.range_position))
|
||||
else ()
|
||||
val () =
|
||||
if length stack_ml - len <= 0 then
|
||||
error ("Maximum depth reached (" ^ Int.toString (len - length stack_ml + 1) ^ " in excess)" ^ Position.here (Symbol_Pos.range syms |> Position.range_position))
|
||||
else ()
|
||||
in (arg, nth_map len (cons ml_exec) stack_ml) end
|
||||
end)
|
||||
l
|
||||
|>> C_Env.map_stream_hook (K ls)
|
||||
| [] => (arg, stack_ml)
|
||||
val (token, arg) = C_Env_Ext.map_stream_lang' (fn [] => (NONE, []) | x :: xs => (SOME x, xs)) arg
|
||||
fun return0 x = (x, ((stack, stack_ml, stack_pos, stack_tree), arg))
|
||||
|
|
@ -795,18 +814,7 @@ fun makeLexer ((stack, stack_ml, stack_pos, stack_tree), arg) =
|
|||
makeLexer
|
||||
( (stack, stack_ml, stack_pos, stack_tree)
|
||||
, (arg, false)
|
||||
|> fold (fn Antiq_stack (Shift (_, Bottom_up, exec)) =>
|
||||
I #>>
|
||||
(fn arg =>
|
||||
C_Env_Ext.map_context (I #> Stack_Data_Lang.put (stack, #env_lang arg)
|
||||
#> exec)
|
||||
arg)
|
||||
| Antiq_stack (Shift ((pos, _), Top_down, _)) =>
|
||||
I #>>
|
||||
(fn arg =>
|
||||
C_Env_Ext.map_context (fn _ => error ("Style of evaluation not yet implemented" ^ Position.here pos))
|
||||
arg)
|
||||
| Antiq_stack (Reduce ((syms_shift, syms), ml_exec)) =>
|
||||
|> fold (fn Antiq_stack (Once ((syms_shift, syms), ml_exec)) =>
|
||||
I #>>
|
||||
(C_Env.map_stream_hook
|
||||
(fn stream_hook =>
|
||||
|
|
@ -892,7 +900,7 @@ fun exec_tree msg write (Tree ({rule_pos = (p1, p2), rule_type, rule_static, rul
|
|||
#-> (fn env_lang =>
|
||||
fold (fn ((rule0, stack0, env_lang0), (_, Top_down, exec)) =>
|
||||
C_Env.map_context (I #> Stack_Data_Lang.put ([stack0], Option.getOpt (env_lang, env_lang0))
|
||||
#> exec rule0)
|
||||
#> exec (SOME rule0))
|
||||
| _ => I)
|
||||
rule_antiq)
|
||||
#> fold (exec_tree (msg ^ " ") write) l_tree
|
||||
|
|
@ -938,7 +946,7 @@ fun parse env_lang err accept stream_lang =
|
|||
( #rule_output arg
|
||||
, fold (fn ((rule0, stack0, env_lang0), (_, Bottom_up, exec)) =>
|
||||
C_Env_Ext.map_context (I #> Stack_Data_Lang.put ([stack0], env_lang0)
|
||||
#> exec rule0)
|
||||
#> exec (SOME rule0))
|
||||
| _ => I)
|
||||
rule_antiq
|
||||
arg)
|
||||
|
|
|
|||
Loading…
Reference in New Issue