git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13738 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Frédéric Tuong 2019-03-22 15:40:03 +00:00
parent 0f71bd7dba
commit 2079449ffa
2 changed files with 9 additions and 9 deletions

View File

@ -120,8 +120,8 @@ signature LR_PARSER1 =
void_position : '_c,
accept : '_c * '_c -> ('_b, '_c) stack * 'arg -> 'arg,
reduce_init : (('_c * '_c) list * int) * 'arg -> 'arg,
reduce_get : (LrTable.state, '_b, '_c) C_Env_base.rule_reduce -> 'arg -> ('_c * '_c) C_Env_base.rule_output0 * 'arg,
get_env_lang : 'arg -> C_Env_base.env_lang,
reduce_get : (LrTable.state, '_b, '_c) C_Env.rule_reduce -> 'arg -> ('_c * '_c) C_Env.rule_output0 * 'arg,
get_env_lang : 'arg -> C_Env.env_lang,
ec : { is_keyword : LrTable.term -> bool,
noShift : LrTable.term -> bool,
preferred_change : (LrTable.term list * LrTable.term list) list,
@ -403,8 +403,8 @@ signature ARG_PARSER1 =
* pos
* (pos * pos -> stack * arg -> arg)
* (((pos * pos) list * int) * arg -> arg)
* ((Token.LrTable.state, svalue0, pos) C_Env_base.rule_reduce -> arg -> (pos * pos) C_Env_base.rule_output0 * arg)
* (arg -> C_Env_base.env_lang)
* ((Token.LrTable.state, svalue0, pos) C_Env.rule_reduce -> arg -> (pos * pos) C_Env.rule_output0 * arg)
* (arg -> C_Env.env_lang)
-> arg lexer
-> arg lexer
val sameToken : (svalue, pos) Token.token * (svalue, pos) Token.token -> bool

View File

@ -49,7 +49,7 @@ fun printStack(stack: ('a,'b) stack0, n: int) =
fun parse {table, saction, void, void_position, accept, reduce_init, reduce_get, get_env_lang, ec = {showTerminal, error, ...}, ...} =
let fun empty_tree rule_pos rule_type =
C_Env_base.Tree ({rule_pos = rule_pos, rule_type = rule_type, rule_static = NONE, rule_antiq = []}, [])
C_Env.Tree ({rule_pos = rule_pos, rule_type = rule_type, rule_static = NONE, rule_antiq = []}, [])
fun prAction(stack as (state, _) :: _, (TOKEN (term,_),_), action) =
(writeln "Parse: state stack:";
@ -82,7 +82,7 @@ fun parse {table, saction, void, void_position, accept, reduce_init, reduce_get,
||> (f_val #>> (fn value => add_stack ((s, (value, leftPos, rightPos)), stack)
stack_ml
((leftPos, rightPos), stack_pos)
(empty_tree (leftPos, rightPos) C_Env_base.Shift, stack_tree)))
(empty_tree (leftPos, rightPos) C_Env.Shift, stack_tree)))
|> Stream.get
|> parseStep
| REDUCE i =>
@ -104,8 +104,8 @@ fun parse {table, saction, void, void_position, accept, reduce_init, reduce_get,
(goto0, stack')
stack_ml
(pos, stack_pos)
( C_Env_base.Tree ( { rule_pos = pos
, rule_type = C_Env_base.Reduce i
( C_Env.Tree ( { rule_pos = pos
, rule_type = C_Env.Reduce i
, rule_static = #output_env goto0'
, rule_antiq = l_ml }
, rev l_tree )
@ -126,7 +126,7 @@ fun parse {table, saction, void, void_position, accept, reduce_init, reduce_get,
|>> (fn void' => add_stack ((initialState table, (void', void_position, void_position)), [])
[]
((void_position, void_position), [])
(empty_tree (void_position, void_position) C_Env_base.Void, [])))
(empty_tree (void_position, void_position) C_Env.Void, [])))
#> Stream.get
#> parseStep
end