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

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13733 3260e6d1-4efc-4170-b0a7-36055960796d

This commit is contained in:
Burkhart Wolff 2019-03-22 12:02:14 +00:00
parent cb55c33422
commit 4c561f7652
6 changed files with 15 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
C11-FrontEnd/C11-Interface.thy → C11-FrontEnd/C_Main.thy
View File

@ -34,7 +34,7 @@
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
theory "C11-Interface"
theory "C_Main"
imports "src/C_Isar"
keywords "C" :: thy_decl
and "C_import" :: thy_load % "ML"

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

@ -35,7 +35,7 @@
******************************************************************************)
theory C1
imports "../C11-Interface"
imports "../C_Main"
begin
declare[[C_lexer_trace]]
@ -120,7 +120,8 @@ int a = (((0
+ 5))) /*@ ML \<open>fn (_, (value, pos1, pos2)) => fn _ => fn context =>
let
val () = writeln (@{make_string} value)
val () = Position.reports_text [((Position.range (pos1, pos2) |> Position.range_position, Markup.intensify), "")]
val () = Position.reports_text [((Position.range (pos1, pos2)
|> Position.range_position, Markup.intensify), "")]
in context end\<close>
*/
* 4;

2
C11-FrontEnd/examples/C2.thy
View File

@ -35,7 +35,7 @@
******************************************************************************)
theory C2
imports "../C11-Interface"
imports "../C_Main"
begin
ML\<open> @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"} \<close>

2
C11-FrontEnd/examples/C3.thy
View File

@ -35,7 +35,7 @@
******************************************************************************)
theory C3
imports "../C11-Interface"
imports "../C_Main"
begin
C\<open>

10
C11-FrontEnd/src/C_Env.thy
View File

@ -38,13 +38,15 @@ theory C_Env
imports C_Lexer
begin
section \<open>The Generic Annotation Interface\<close>
section \<open>The C Annotation Result Interface\<close>
text\<open>The key element of this following structure is the type \verb+eval_time+ which is relevant for
the generic annotation module. \<close>
ML\<open>
structure C_Annot_Result =
struct
datatype eval_tree = Bottom_up (*during parsing*) | Top_down (*after parsing*)
@ -59,10 +61,14 @@ datatype eval_time = Shift of (Context.generic -> Context.generic) eval_at
datatype antiq_language = Antiq_stack of eval_time
| Antiq_none of C_Lex.token
end;
open C_Annot_Result; (* Temporary hack --- to be removed *)
\<close>
section \<open>The Lexing-based C Environment\<close>
text\<open>It comes in two parts: a basic core tstructure and a (thin) layer of utilities. \<close>
ML\<open>
structure C_Env_base = struct
@ -282,8 +288,6 @@ fun context_map (f : C_Env_base.env_tree -> C_Env_base.env_tree) context =
end
\<close>

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

@ -936,7 +936,7 @@ fun eval'0 env err accept ants {context, reports_text} =
in P.parse env err accept ants_stack {context = context, reports_text = reports_text} end
fun eval' env err accept ants =
Context.>> (C_Env'.context_map
Context.>> (C_Env.context_map
let val tap_report = tap (Position.reports_text o #reports_text)
in eval'0 env
(fn env_lang => fn stack => fn pos => tap_report #> err env_lang stack pos)
@ -977,7 +977,7 @@ fun command dir name =
in expression
(Input.range_of src)
hook
(MlyValue.type_reduce rule ^ " stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")
(MlyValue.type_reduce rule ^ " stack_elem -> C_Env_base.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")