ftuong
/
citadelle-devel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

generalize 

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13727 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Frédéric Tuong 2019-03-21 14:49:31 +00:00
parent e6ae1e8a1f
commit ac2d05c334
3 changed files with 89 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
C11-FrontEnd/examples/C1.thy
View File

@ -142,15 +142,6 @@ int b = 7 / (3) * 50 /*@@@@ ML \<open>@{reduce}\<close>
*/;
\<close>
C \<comment> \<open>Nesting C code in ML\<close> \<open>
int b = 7 / (3) * 50
/*@@@@ ML \<open>(reduce @{make_string} o tap)
(fn _ => C_Outer_Syntax.C
\<open>int b = 7 / 5 * 2 + 3 * 50 //@ ML \<open>@{reduce}\<close>
;\<close>)\<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>*/
@ -382,6 +373,11 @@ int x /** OWNED_BY foo */, hh /*@
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> */
\<close>
subsection \<open>Reporting of Positions and Contextual Update of Environment\<close>
subsubsection \<open>1\<close>
@ -416,10 +412,27 @@ fun show_env0 make_string f msg context =
val show_env = tap o show_env0 @{make_string} length
fun C src = tap (fn _ => C_Outer_Syntax.C src)
val C' = C_Outer_Syntax.C' (fn _ => fn _ => fn pos =>
tap (fn _ => warning ("Parser: No matching grammar rule " ^ Position.here pos)))
\<close>
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 _ =>
C \<open>int b = a + a + a + a + a + a + a
;\<close> \<close> */;
\<close>
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 =>
C' env \<open>int b = a + a + a + a + a + a + a
;\<close> \<close> */;
\<close>
C \<comment> \<open>Propagation of Updates\<close> \<open>
typedef int i, j;
int j = 0;
@ -428,7 +441,7 @@ 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>
k jj = jj + jj;
k jj = jj + jj1;
typedef k l; //@ ML \<open>@{reduce'}\<close>\<close>
#> show_env "POSITION 1"\<close> */
j j = jj1 + jj; //@ ML \<open>@{reduce'}\<close>

61
C11-FrontEnd/src/C_Isar.thy
View File

@ -956,34 +956,41 @@ end
section \<open>\<close>
setup \<open>
C0_Outer_Syntax.command' ("ML", \<^here>) ""
(fn Left stack =>
C_Parse.range C_Parse.ML_source >>
ML\<open>
local
fun command dir name =
C0_Outer_Syntax.command' name ""
(fn Left 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 ML_Context.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) =>
(fn f => Reduce (stack, (range, f)))
(fn rule =>
let val hook = "hook"
in ML_Context.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 pair range)
let val setup = "setup"
in ML_Context.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))
(Shift o (fn x => (range, dir, x)))
let val setup = "setup"
in ML_Context.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))
in
val _ = Theory.setup ( command Bottom_up ("ML", \<^here>)
#> command Top_down ("ML'", \<^here>))
end
\<close>
end

45
C11-FrontEnd/src/C_Parser.thy
View File

@ -41,9 +41,12 @@ begin
section \<open>Instantiation of the Parser with the Lexer\<close>
ML\<open>
type eval_at_reduce = Position.range * (int (*reduce rule number*) -> Context.generic -> Context.generic)
datatype eval_tree = Bottom_up (*during parsing*) | Top_down (*after parsing*)
datatype eval_time = Shift of Position.range * (Context.generic -> Context.generic)
type 'fun eval_at = Position.range * eval_tree * 'fun
type eval_at_reduce = (int (*reduce rule number*) -> Context.generic -> Context.generic) eval_at
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
@ -76,12 +79,14 @@ datatype rule_type = Void
| Shift
| Reduce of int
type ('LrTable_state, 'svalue0, 'pos) rule_reduce =
((int * ('LrTable_state * ('svalue0 * 'pos * 'pos)) * env_lang) * eval_at_reduce) list
type ('LrTable_state, 'svalue0, 'pos) rule_ml =
{ rule_pos : 'pos * 'pos
, rule_type : rule_type
, rule_static : rule_static
, rule_antiq : ((int * ('LrTable_state * ('svalue0 * 'pos * 'pos)) * env_lang)
* eval_at_reduce) list }
, rule_antiq : ('LrTable_state, 'svalue0, 'pos) rule_reduce }
datatype 'a tree = Tree of 'a * 'a tree list
@ -673,12 +678,14 @@ ML\<open>
structure MlyValueM' = struct
open Hsk_c_parser
val To_string0 = String.implode o C_ast_simple.to_list
fun update_env f x = pair () ##> (fn arg => C_Env'.map_output_env (K (SOME (f x (#env_lang arg)))) arg)
val update_env =
fn Bottom_up => (fn f => fn x => fn arg => ((), C_Env.map_env_tree (f x (#env_lang arg) #> #2) arg))
| Top_down => fn f => fn x => pair () ##> (fn arg => C_Env'.map_output_env (K (SOME (f x (#env_lang arg)))) arg)
(*type variable definition*)
val specifier3 : (CDeclSpec list) -> unit monad = update_env (fn l => fn env_lang => fn env_tree =>
val specifier3 : (CDeclSpec list) -> unit monad = update_env Bottom_up (fn l => fn env_lang => fn env_tree =>
( env_lang
, fold
let open C_ast_simple
@ -698,7 +705,7 @@ val type_specifier3 : (CDeclSpec list) -> unit monad = specifier3
(*basic variable definition*)
val primary_expression1 : (CExpr) -> unit monad = update_env (fn e => fn env_lang => fn env_tree =>
val primary_expression1 : (CExpr) -> unit monad = update_env Bottom_up (fn e => fn env_lang => fn env_tree =>
( env_lang
, let open C_ast_simple
in fn CVar0 (Ident0 (i, _, node), _) =>
@ -998,12 +1005,17 @@ 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 (_, exec)) =>
|> fold (fn Antiq_stack (Shift (_, Bottom_up, exec)) =>
I #>>
(fn arg =>
C_Env'.map_context (I #> Stack_Data_Lang.put (stack, #env_lang arg)
#> exec)
arg)
| Antiq_stack (Shift ((pos, _), Top_down, _)) =>
I #>>
(fn arg =>
C_Env'.map_context (fn _ => error ("Style of evaluation not yet implemented" ^ Position.here pos))
arg)
| Antiq_stack (Reduce ((syms_shift, syms), ml_exec)) =>
I #>>
(C_Env.map_stream_hook
@ -1088,14 +1100,14 @@ fun exec_tree msg write (Tree ({rule_pos = (p1, p2), rule_type, rule_static, rul
in msg ^ s1 ^ " " ^ Position.here p1 ^ " " ^ Position.here p2 ^ (case s2 of SOME s2 => " " ^ s2 | NONE => "") end)
#> (case rule_static of SOME rule_static => rule_static #>> SOME | NONE => pair NONE)
#-> (fn env_lang =>
fold (fn ((rule0, stack0, env_lang0), (_, exec)) =>
C_Env.map_context (I #> Stack_Data_Lang.put ([stack0], Option.getOpt (env_lang, env_lang0))
#> exec rule0))
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)
| _ => I)
rule_antiq)
#> fold (exec_tree (msg ^ " ") write) l_tree
fun exec_tree' l env_tree = env_tree
|> C_Env.map_context (Stack_Data_Tree.put [])
|> fold (exec_tree "" let val ctxt = Context.proof_of (#context env_tree)
in if Config.get ctxt C_Options.parser_trace andalso Context_Position.is_visible ctxt
then fn f => tap (tracing o f) else K I end)
@ -1132,7 +1144,14 @@ fun parse env_lang err accept stream_lang =
#> accept env_lang (stack |> hd |> map_svalue0 MlyValue.reduce0))
, fn (stack, arg) => arg |> map_rule_input (K stack)
|> map_rule_output (K empty_rule_output)
, fn arg => (#rule_output arg, arg)
, fn rule_antiq => fn arg =>
( #rule_output arg
, fold (fn ((rule0, stack0, env_lang0), (_, Bottom_up, exec)) =>
C_Env'.map_context (I #> Stack_Data_Lang.put ([stack0], env_lang0)
#> exec rule0)
| _ => I)
rule_antiq
arg)
, #env_lang)
#> snd
#> #env_tree