diff --git a/C11-BackEnds/Clean/src/Clean.thy b/C11-BackEnds/Clean/src/Clean.thy
index 7633fe618c8d4c87a4c64569c9eaac25683f1d5a..988268dbda7ae90ebafd183f7e94766b8ed588f1 100644
--- a/C11-BackEnds/Clean/src/Clean.thy
+++ b/C11-BackEnds/Clean/src/Clean.thy
@@ -1415,9 +1415,7 @@ fun mk_seq_C C C' = let val t = fastype_of C
fun mk_seq_assign_C rhs lhs varname vartyp= let
val t1 = fastype_of rhs
val t2 = fastype_of lhs
- val abstractedTerm = Term.abstract_over ((Free (varname, vartyp)),lhs)
- val lambdaExpr = (Abs (varname,vartyp, abstractedTerm))
- in Const(\<^const_name>\<open>bind_SE\<close>, t1 --> (vartyp --> t2) --> t2 ) $ rhs $ lambdaExpr end;
+ in Const(\<^const_name>\<open>bind_SE\<close>, t1 --> (vartyp --> t2) --> t2 ) $ rhs $ absfree (varname, vartyp) lhs end;
fun mk_skip_C sty = Const(\<^const_name>\<open>skip\<^sub>S\<^sub>E\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty)
@@ -1425,34 +1423,26 @@ fun mk_break sty =
Const(\<^const_name>\<open>break\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty )
fun mk_return_C upd rhs =
- let val ty = fastype_of rhs
- val (sty,rty) = case ty of
- Type("fun", [sty,rty]) => (sty,rty)
- | _ => error "mk_return_C: illegal type for body"
- val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty
+ let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
+ | _=>error "mk_return_C: illegal type for update func"
+
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
- in Const(\<^const_name>\<open>return\<^sub>C\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
+ in Const(\<^const_name>\<open>return\<^sub>C\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_assign_global_C upd rhs =
- let val ty = fastype_of rhs
- val (sty,rty) = case ty of
- Type("fun", [sty,rty]) => (sty,rty)
- | _ => error "mk_assign_global_C: illegal type for body"
- val upd_ty = (rty --> rty) --> sty --> sty
+ let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [r_ty,_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
+ | _=>error "mk_assign_global_C: illegal type for update func"
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
- in Const(\<^const_name>\<open>assign_global\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
+ in Const(\<^const_name>\<open>assign_global\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_assign_local_C upd rhs =
- let val ty = fastype_of rhs
- val (sty,rty) = case ty of
- Type("fun", [sty,rty]) => (sty,rty)
- | _ => error "mk_assign_local_C: illegal type for body"
- val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty
+ let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
+ | _=>error "mk_assign_local_C: illegal type for update func"
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
- in Const(\<^const_name>\<open>assign_local\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
+ in Const(\<^const_name>\<open>assign_local\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_call_C opn args =
let val ty = fastype_of opn
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
new file mode 100644
index 0000000000000000000000000000000000000000..dbbc2b58cbfe5c790753feaa9707509fd1be8162
--- /dev/null
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
@@ -0,0 +1,135 @@
+(*In this file the current limitations of the translation from C to Clean are shown.*)
+theory "Coder_Documentation"
+ imports
+ "../src/compiler/Clean_Annotation"
+ "../src/CleanTranslationHook"
+begin
+
+
+section\<open>Architecture remarks\<close>
+text\<open>
+The function \<open>handle_declarations::nodeInfo cTranslationUnit ->Context.generic -> Context.generic\<close>
+can be called with the AST of a translation unit to handle all the definitions. Within that, for every
+function the \<open>convertStmt\<close> (CleanCoder) is called to create a translation of the function body.
+
+The \<open>setup C_Module.C_Term.map_expression\<close> command handles the C-Term-Antiquotation, which is used for the annotations.
+The parsing of the annotation is delayed, for the reason that they need a contet within which sigma (and vars)
+are already defined. For that reason, they are stored in \<open>Data_Clean_Annotations\<close> as functions with the
+signature \<open>Context.generic \<rightarrow> term\<close>. This functions are then called when the new context is available.
+Additionally the position and function names are saved, which are needed for assigning pre- and postconditions to
+the functions and assigning invariants and measures to a loop (via positions).
+
+Importantly, the parsing of the expressions still needs the "old" env because it contains informations
+about local vars and parameters, therefore this is saved in the beginning of the \<open>map_context_annotation_declaration\<close> function.
+The environment is then passed by writing it to the \<open>Data_Surrounding_Env\<close> GenericData-store.
+
+To prevent Isabelle from coercing types of returned terms \<open>Syntax.parse_term\<close> is used instead of \<open>Syntax.read_term\<close>.
+Furthermore as parameters are represented as free variables, all constants that would be "selected" through
+a parameter name need to be hidden (\<open>remove_params_from_proof\<close>).
+
+Environment:
+The scope of a parameter now is visible in the environment's var table. It is either "Global", "Local" or "Parameter".
+Furthermore each identifier has a field \<open>functionArgs\<close> which is an optional list of function parameters.
+When an identifier has \<open>functionArgs = NONE\<close>, then it is a variable. \<open>functionArgs=SOME []\<close> corresponds to a parameterless function.
+
+Nice to know:
+- The environment of the last completely parsed C-context can be retrieved using \<open>C_Module.Data_In_Env\<close>.
+- Intermediate envs, containing parameters and local vars can be retrieved using \<open>C_Env.Data_Lang.get'\<close>.
+See C5.thy in the examples of C11-Frontend.
+\<close>
+
+section\<open>Limitations\<close>
+text\<open>
+- Only two types are currently mapped to isabelle types,
+ namely int -> int and unsigned -> nat.
+
+- Function calls can only occur as statements or on the right hand side of an assignment.
+ For example \<open>a = b + foo();\<close> is not allowed. This must be rewritten as \<open>tmp = foo(); a=b+tmp;\<close>
+
+- Recursive functions must have "void" as return value. This is caused by an issue within
+ Clean and is about to be fixed. The current translation should work for this case then.
+
+- Scoping: refrain from defining variables more than once. A read/write from a local variable
+ always affects the most recent definition. Scoping using curly braces does not work as in C!
+ example:
+ \<open>int foo(){
+ int x = 3;
+ {
+ int x = 5;
+ }
+ return x; // wrongly returns 5
+ }\<close>
+ Also defining global variables twice within one translation unit will result in only one definition,
+ thus the second definition does not "reset" the value of the variable
+
+- Method overloading: Do not use function names multiple times, as this will break the whole
+ translation process in several ways.
+\<close>
+
+section\<open>Some examples\<close>
+text\<open>See \<open>Coder_Test_T_Units\<close> for more examples\<close>
+
+C\<open>
+int sum_of_array(int arr[], int length){
+ int i;
+ int sum;
+ i = 0;
+ sum = 0;
+ while(i < length){
+ /*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>i\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>length\<close>\<close> */
+ /*@ measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>nat \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>length-i\<close>\<close> */
+ sum = sum + arr[i];
+ i = i+1;
+ }
+ return sum;
+}
+\<close>
+(*look at the annotated while loop - it has the inv as first and the measure as snd argument*)
+find_theorems sum_of_array_core
+
+text\<open>The following program would not work in C - Clean admits it however, but produces warnings\<close>
+C\<open>
+int A[5][4];
+int swap_rows(unsigned idx1, unsigned idx2){
+ int tmp[];
+ tmp = A[idx1];
+ A[idx1] = A[idx2];
+ A[idx2] = tmp;
+}
+\<close>
+find_theorems swap_rows_core
+
+text\<open>A fully annotated multiply\<close>
+C\<open>
+int multiply(int a, int b){
+ /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close> \<ge> 0\<close> */
+ /*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int. ret = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a*b\<close>\<close> */
+ int sum;
+ int counter;
+ sum = 0;
+ counter = 0;
+
+ while(counter < a){
+ /*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter*b\<close> = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>sum\<close> \<and> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close>\<close> */
+ sum = sum + b;
+ counter = counter + 1;
+ }
+ return sum;
+}
+\<close>
+find_theorems multiply
+find_theorems multiply_pre
+find_theorems multiply_post
+
+text\<open>A recursive function calculating the factorial of n\<close>
+C\<open>
+int factorial_result;
+void factorial(int n){
+ if(n > 1){
+ factorial(n-1);
+ factorial_result = multiply(factorial_result, n);
+ }else{
+ factorial_result = 1;
+ }
+}\<close>
+find_theorems factorial_core
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
index 4820cab5c50de84629506ab58ae5bebc05835738..5cdd77a886463f760621b76f700edbc703bf0561 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
@@ -203,7 +203,7 @@ val S'' = conv_Cexpr_lifted_term sigma_i A_env2 @{theory} "" (K NONE) ast_expr
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open> Sign.certify_term @{theory} (Syntax.check_term @{context} S) \<close>
(* This local variable space also creates the update function for the return_result. *)
local_vars_test (test_return "int")
@@ -257,7 +257,7 @@ val S = conv_Cexpr_lifted_term sigma_i A_env1 @{theory} "" (K NONE) ast_expr
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
(*7*****************************************************************************************************)
@@ -280,7 +280,7 @@ val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} "" (K NONE) ast_expr
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
section \<open>statements\<close>
@@ -316,7 +316,7 @@ val [S] = (C11_Ast_Lib.fold_cStatement
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
text\<open>Write to array\<close>
@@ -448,7 +448,7 @@ val [S] = (C11_Ast_Lib.fold_cStatement
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
(*3*****************************************************************************************************)
@@ -472,7 +472,7 @@ val [S] = (C11_Ast_Lib.fold_cStatement
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
(*4*****************************************************************************************************)
@@ -499,7 +499,7 @@ val [S] = (C11_Ast_Lib.fold_cStatement
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
(*5*****************************************************************************************************)
@@ -537,7 +537,7 @@ ML\<open> read_N_coerce @{theory} "a" (sigma_i --> intT)\<close>
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
\<comment> \<open>type-check of the latter\<close>
-ML\<open> Sign.certify_term @{theory} S \<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
(* a very serious problem : the inheritance on state spaces is not appropriately mirrored. *)
@@ -744,7 +744,7 @@ val [S] = (C11_Ast_Lib.fold_cStatement
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
-ML\<open>Sign.certify_term @{theory} S\<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
subsection\<open>Call with no return type\<close>
(*Methods call only with sideeffects*)
@@ -769,7 +769,7 @@ term assign_to_a
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
-ML\<open>Sign.certify_term @{theory} S\<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
subsection\<open>Call with return type\<close>
consts fun_with_ret_value :: "(int) \<Rightarrow> (int,'a local_test_return_state_scheme)MON\<^sub>S\<^sub>E "
@@ -806,7 +806,7 @@ term assign_to_a
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
-ML\<open>Sign.certify_term @{theory} S\<close>
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
section \<open>Experiments with Local Scopes\<close>
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits
deleted file mode 100644
index 0caf1f6ce14ca21d54c0bb1922d638a6d9455983..0000000000000000000000000000000000000000
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits
+++ /dev/null
@@ -1,3 +0,0 @@
-theory "Coder_Test_ExprStmt"
- imports "../src/CleanCoder" (* Coder_Test_Env_AEnv *)
-begin
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy
index 267b5e44111fb7a7cc891f525c7b1dd2a9879d4d..36ff8a10e8e6cb8144c72b7abccb7a516bc53592 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy
@@ -1,198 +1,98 @@
theory "Coder_Test_TUnits"
- imports "../src/CleanCoder" (* Coder_Test_Env_AEnv *)
+ imports
"../src/compiler/Clean_Annotation"
+ "../src/CleanTranslationHook"
begin
-ML\<open>
-(*This is an override for the update_Root_Ast function that is registered in C_Command.*)
-
-fun transform_type typ = if typ = HOLogic.intT then "int"
- else if typ = HOLogic.natT then "nat"
- else if is_listTy typ then (transform_type (dest_listTy typ))^" list"
- else if typ = HOLogic.unitT then "unit"
- else error "Unknown variable type"
-
-local open C_AbsEnv HOLogic in
-fun get_hol_type (C_Env.Parsed ret) params = let
- val base_type =the (C11_TypeSpec_2_CleanTyp.conv_cDeclarationSpecifier_typ (SOME ret))
- fun transform_type ((C_Ast.CArrDeclr0 _)::R) base_type = listT (transform_type R base_type)
- | transform_type [] base_type = base_type
- in transform_type params base_type end
-fun map_env_ident_to_identifier (name,(positions,_,data)) =
- let fun get_ident_scope C_Env.Global = Global
- |get_ident_scope C_Env.Local = Local ""
- |get_ident_scope C_Env.Parameter = Parameter ""
- in
- case #functionArgs data of C_Ast.None => Identifier(name, if null positions then @{here} else hd positions,get_hol_type (#ret data) (#params data),get_ident_scope (#scope data))
- |_=> Identifier(name, @{here},intT,FunctionCategory (Final, NONE)) (*this line is wrong because of different function types*)
- end
-end
-
-fun declare_function idents name ast ret_ty recursive ctxt =
- let val param_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Parameter f_name) => f_name = name |_=>false) idents
- val local_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Local f_name) => f_name = name |_=>false) idents
- val global_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Global) => true
- | C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _)=>true
- | _ => false) idents
-
- (*Obtain the parameters and local variables*)
- val params = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ)) (param_idents)
- val locals = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ, NoSyn)) (local_idents)
-
- (*This is necessary, as parameters are represented as free variables.
- When the Invariants, post- and preconditions are read through the term antiquotations,
- Syntax.parse_term (Syntax.read_term does this too) would substitute them by another const,
- which could be a local or global variable*)
- fun remove_params_from_proof ctx = let
- val param_names = List.map (fn C_AbsEnv.Identifier(n,_,_,_) => n) param_idents
- fun filter_by_shortname param_names (n, _) =
- List.exists (fn ele => ele = Long_Name.base_name n) param_names
- val longnames = List.filter (filter_by_shortname param_names) (#constants (Consts.dest (Sign.consts_of (Proof_Context.theory_of ctx))))
- val thy0 = Proof_Context.theory_of ctx
- val thy' = List.foldl (fn (longname, thy')=> thy' |> Sign.hide_const true longname) thy0 (List.map fst longnames)
- in Proof_Context.init_global thy' end
-
- (*Invariants and measuress need to be matched to a loop. This is done by comparing the parse locations of all while loops.
- The following are helper methods, to obtain the function get_invariant: positiona \<rightarrow> (context\<rightarrow>term) option*)
- val invariants:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
- (#invariants (Clean_Annotation.Data_Clean_Annotations.get ctxt))
- val measures:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
- (#measures (Clean_Annotation.Data_Clean_Annotations.get ctxt))
- val loop_pos =Library.distinct (op =) (C11_Ast_Lib.fold_cStatement (fn a => fn b => a@b) C11_Unit_2_Clean.get_loop_positions ast [])
- fun compare_pos ((C_Ast.Position0 (pos1,_,_,_)),(C_Ast.Position0 (pos2,_,_,_))) = Int.compare (pos1,pos2)
- val loop_pos_sorted = Library.sort compare_pos loop_pos
- fun range_less_than_pos (range:Position.range) (C_Ast.Position0 (pos,_,_,_)) = the (Position.offset_of (fst range)) < pos
- fun get_for_position (((inv,inv_pos)::R_inv): ((Context.generic -> term)*Position.range)list)
- (loop_positions: C_Ast.positiona list)
- (pos3: C_Ast.positiona)
- (* search the first invariant, which is not declared before pos3 *)
- = (if range_less_than_pos inv_pos pos3 then get_for_position R_inv loop_positions pos3
- else case loop_positions of (* we found the first invariant after pos3 *)
- (* Now check, if the next loop definition is after the invariant definition.
- Otherwise there is no invariant for the given loop *)
- (pos1::pos2::R) => if pos3 = pos1 andalso range_less_than_pos inv_pos pos2 then SOME inv
- else get_for_position ((inv,inv_pos)::R_inv) (pos2::R) pos3
- | (pos1::R) => if pos3 = pos1 then SOME inv else NONE
- | [] => NONE)
- |get_for_position [] _ _ = NONE
- fun get_invariant pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) invariants) loop_pos_sorted) pos
- fun get_measure pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) measures) loop_pos_sorted) pos
- fun get_loop_annotations pos = (get_invariant pos, get_measure pos)
-
- (*generic function to get the first ele*)
- val get_precond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#preconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
- val get_postcond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#postconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
-
- (*the translation of the precondition*)
- fun get_translation NONE default ctxt= C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type (ctxt)) default
- | get_translation (SOME get_term) _ ctxt= let
- val term = get_term (Context.Proof (remove_params_from_proof ctxt))
- val lifted = C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type ctxt) term
- in
- Syntax.check_term ctxt lifted
- end
- (*The actual translation of the loop body*)
- fun get_translated_fun_bdy ctx _ = let
- val ctx' = remove_params_from_proof ctx
- val v = ((C11_Ast_Lib.fold_cStatement
- C11_Stmt_2_Clean.regroup
- (C11_Stmt_2_Clean.convertStmt false
- (StateMgt.get_state_type ctx')
- (local_idents@param_idents@global_idents)
- (Proof_Context.theory_of ctx')
- name get_loop_annotations)
- ast []))
- in hd v end
-
- val test_function_sem = {binding = Binding.name name,
- locals = locals@[(Binding.name "dummylocalvariable","int", NoSyn)], (*There needs to be at least one local variable*)
- params = params,
- ret_type = transform_type ret_ty,
- read_pre = get_translation get_precond (@{term True}),
- read_post = get_translation get_postcond (Abs ("ret",ret_ty, @{term True})),
- read_variant_opt = NONE,
- read_body = get_translated_fun_bdy}
- val decl = Function_Specification_Parser.checkNsem_function_spec_gen {recursive = recursive} test_function_sem
- in decl end
-
-local open C_AbsEnv HOLogic in
-fun handle_declarations translUnit ctxt =
- (let
- val env = (C_Module.Data_Last_Env.get ctxt)
- (*First we need to get all previously defined global vars and functions*)
- val m = (Symtab.dest (#idents(#var_table(env))))
- val prev_idents =map map_env_ident_to_identifier m
- (*the new identifiers are returned in reverse \<rightarrow> thus reverse *)
- val (new_idents, call_table) = C_AbsEnv.parseTranslUnitIdentifiers translUnit [] prev_idents Symtab.empty
-
- val identifiers = (rev new_idents)@prev_idents
- val map_idents = List.map (fn C_AbsEnv.Identifier(name,_,typ,_) => (Binding.name name, transform_type typ, NoSyn))
-
- fun get_declaration is_global idents = if null idents then I else StateMgt.new_state_record is_global (NONE,idents)
-
- val global_idents = (map_idents (List.filter (fn C_AbsEnv.Identifier(_,_,_,vis) => vis = C_AbsEnv.Global) new_idents))
- val global_declaration =get_declaration true global_idents
-
- val fun_asts =
- List.map (fn C_AbsEnv.Identifier(name,_,ret_ty,C_AbsEnv.FunctionCategory ast) =>
- let fun is_recursive NONE = false
- |is_recursive (SOME calls) = List.exists (fn x => x=name) calls
- in
- (name,the (snd ast),ret_ty, is_recursive (Symtab.lookup call_table name)) end)
- (List.filter (fn a => case a of C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _) => true | _ => false) (rev new_idents))
- val function_declarations = List.map (fn (name,ast,ret_ty, recursive) => declare_function identifiers name ast ret_ty recursive ctxt) (fun_asts)
-
- val function_decl = fold (fn f => fn acc => f acc) function_declarations
- in
- Context.map_theory (function_decl o global_declaration) ctxt
- end);
-end
-\<close>
-ML\<open>
-fun handle_declarations_wrapper ast v2 ctxt =
- let val ctx1 = update_Root_Ast SOME ast v2 ctxt (*Note the call to the original callback - this somehow gets overwritten*)
- in
- case ast of (C_Ast.Left translUnit) => handle_declarations translUnit ctx1
- | _ => ctx1
- end
-\<close>
-setup \<open>Context.theory_map (C_Module.Data_Accept.put (handle_declarations_wrapper))\<close>
-
-(* Note: The hook "C_Module.C_Term.map_translation_unit" is not adequate, as it is
- meant for the term antiquotation (its callback returns a term, not a theory/context *)
-
-setup \<open>C_Module.C_Term.map_expression
- (fn cexpr => fn _ => fn ctxt => let
- val sigma_i = (StateMgt.get_state_type o Context.proof_of )ctxt
- val env = C_Module.Data_Surrounding_Env.get ctxt
- val idents = (Symtab.dest (#idents(#var_table(env))))
- val A_env = List.map map_env_ident_to_identifier idents
- val expr = (hd (C11_Ast_Lib.fold_cExpression (K I)
- (C11_Expr_2_Clean.convertExpr true sigma_i A_env (Context.theory_of ctxt) "" (K NONE))
- cexpr [])) handle ERROR msg => (writeln("ERROR: "^(@{make_string}msg));@{term "1::int"})
-in
- expr
-(* @{term "1::int"}*)
- end
-
-)\<close>
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
-ML\<open>
-val a = (Abs ("\<sigma>", StateMgt.get_state_type ( @{context}),
- Const ("Orderings.ord_class.greater_eq", @{typ "_"}) $ Const ("Groups.one_class.one", @{typ "int"}) $
- Const ("Groups.one_class.one", @{typ "int"})))
-val a' = absfree ("a",@{typ "int"}) (absfree ("b", @{typ "int"}) (Syntax.check_term @{context} a))
+C\<open>
+int foo10(){
+ int b = 0, d123=4, ex=13;
+}
+\<close>
+
+C\<open>
+int foo11(){
+ int var1,var2=3,var3, var4;
+}
+\<close>
+
+C\<open>
+int forloop(){
+ int b=3;
+ for(int i=0; i<10; i=i+1){
+ b=b+1;
+ }
+ return b;
+}
+\<close>
+
+find_theorems d123
+find_theorems foo10_core
+find_theorems forloop_core
+
+text\<open>Apparently currently it is decided based on the stack layout, whether an else branch exists.
+So a previous assignment destroys this code.\<close>
+C\<open>
+int g;
+int foo13(){
+ if(1){
+ }
+ if (g>0){
+ g=1;
+ }
+}
+\<close>
+C\<open>
+int g;
+int foo12(){
+ g = 0;
+ if (g>0){
+ g=1;
+ }
+}
+\<close>
+
+
+C\<open>
+int foo(int a, int b){
+}
+int bar(int b){
+ int a;
+ a = 2;
+}
+\<close>
+
+C\<open>
+int foo1(unsigned par){
+ unsigned tmp;
+ for (tmp = 0; tmp < tmp; tmp=tmp+1) {
+ }
+}
+\<close>
+
+text\<open>Assigning numbers to a non-int variable causes issues\<close>
+C\<open>
+int bar1(){
+ unsigned tmp;
+ tmp = tmp+0;
+}
+\<close>
-val b = HOLogic.mk_case_prod a'
+C\<open>
+unsigned glob_nat;
+int bar2(){
+ glob_nat = 3;
+}
\<close>
C\<open>
int multiply1(int a, int b){
- /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>1 \<ge> 1\<close> */
+ /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>(1::int) \<ge> 1\<close> */
return a;
}\<close>
@@ -210,11 +110,11 @@ int fun_with_pre_test(int u){
int localvar;
localvar = u;
- /* pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1\<close> */
- /* post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int.\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1 \<and> ret > 0\<close> */
+ /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1\<close> */
+ /*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int.\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1 \<and> ret > 0\<close> */
while(localvar>0){
- /* inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> \<ge> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>localvar\<close> \<close> */
+ /*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> \<ge> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>localvar\<close> \<close> */
/*@ measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>nat1\<close>\<close> */
localvar = localvar -1;
}
@@ -289,7 +189,7 @@ term\<open>addPlusThree1\<close>
subsection \<open>Recursive functions\<close>
-
+find_theorems global_integer
rec_function_spec recursive_add1(n::int) returns unit
pre "\<open>True\<close>"
post "\<open>\<lambda>res::unit. True \<close>"
@@ -335,7 +235,7 @@ text\<open>disclaimer: C_expr antiquotation does not yet work\<close>
C\<open>
int multiply(int a, int b){
- /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>1 \<ge> 1\<close> */
+ /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>(1::int) \<ge> 1\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int. ret = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a*b\<close>\<close> */
int s;
int counter;
@@ -357,7 +257,7 @@ int multiply(int a, int b){
return s;
}
\<close>
-
+find_theorems multiply_pre
diff --git a/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy b/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
index 1938d7a4b58f034ce1c8f312da8bf89a63a6e226..edef56617a87f2369f5837c19c5b0ff8d0f35eb0 100644
--- a/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
+++ b/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
@@ -67,10 +67,9 @@ exception WrongFormat of string
exception UnknownTyp of string
-(*renvoie le type final d'une fonction, ou le type d'une constante*)
-fun lastype_of (Type(_, [x])) = x | lastype_of (Type(_, [_, y])) = y
(*renvoie le type du premier attribut d'une fonction, ou le type d'une constante*)
-fun firstype_of (Type(_, [x])) = x | firstype_of (Type(_, x::_)) = x
+fun firstype_of (Type(_, [x])) = x | firstype_of (Type(_, x::_)) = x
+ |firstype_of t = t
(* Creates a result_update_term for the local state *)
fun mk_result_update thy sigma_i=
@@ -80,19 +79,17 @@ fun mk_result_update thy sigma_i=
val s' = String.substring(s, 0, size s - size "_scheme")^".result_value_update"
in Syntax.read_term_global thy s' end;
-fun extract_ids long_id sigma_i =
- let val id = List.last(String.tokens (fn x => x = #".") long_id)
- val Type(ty_name, _) = sigma_i;
- val ty_name = ty_name |> String.tokens (fn x => x = #".") |> tl |> hd
- val local_state = String.substring (ty_name, 0,
- String.size ty_name
- - (String.size "_scheme"))
- (*dangerous. will work only for the local case *)
- in (id, local_state^"."^id) end
-
-fun read_N_coerce_global thy name ty =
- (* a very dirty hack ... but reconstructs the true \<open>const_name\<close> Sign.consts_of thy
+
+fun read_N_coerce thy name ty =
+ (* a very dirty hack ... but reconstructs the true \<open>const_name\<close>
along the subtype hierarchy, but coerces it to the current sigma*)
+ let val s = drop_dark_matter(Syntax.string_of_typ_global thy ty)
+ val str = name ^ " :: " ^ s
+ in Syntax.read_term_global thy str end
+
+fun read_N_coerce_global thy name =
+ (*this function is necessary, to ensure that a global variable is selected, in case
+ a local variable is defined later (as later vars would get selected by default)*)
let
val consts = Sign.consts_of thy
fun filter_by_shortname (n, _) =
@@ -101,17 +98,9 @@ fun read_N_coerce_global thy name ty =
| _ => false)
val longnames = List.filter filter_by_shortname (#constants (Consts.dest consts))
val longname = (fst o hd) longnames
- val s = drop_dark_matter(Syntax.string_of_typ_global thy ty)
- val str = longname ^ " :: " ^ s
- in Syntax.read_term_global thy str end
-
+ in read_N_coerce thy longname end
-fun read_N_coerce thy name ty =
- (* a very dirty hack ... but reconstructs the true \<open>const_name\<close>
- along the subtype hierarchy, but coerces it to the current sigma*)
- let val s = drop_dark_matter(Syntax.string_of_typ_global thy ty)
- val str = name ^ " :: " ^ s
- in Syntax.read_term_global thy str end
+fun get_update_fun thy name = read_N_coerce thy (name^"_update")
\<close>
subsection\<open>C11 Expressions to Clean Terms\<close>
@@ -141,11 +130,22 @@ fun node_content_parser (x : C11_Ast_Lib.node_content) =
val id = hd(tl(String.tokens (fn x => x = #"\"")(drop_dark_matter a_markup)))
in id end (* no type inference *);
-fun convertExpr verbose (sigma_i: typ) env thy function_name get_loop_annotations
+fun is_call a = case a of
+ Const (@{const_name "Clean.call\<^sub>C"},_) $_ $_ => true
+ |_ => false
+
+fun convertExpr verbose (sigma_i: typ) env thy function_name _
(a as { tag, sub_tag, args }:C11_Ast_Lib.node_content)
(b: C_Ast.nodeInfo )
(c : term list) =
((if verbose then print_node_info a b c else ());
+ let fun get_most_general_type t1 t2 =
+ if t1 = natT andalso t2=natT then natT else
+ if (t1 = natT orelse t1 = intT) andalso (t2=natT orelse t2=intT) then intT else
+ if t1 <> natT andalso t1<>intT then t1 else t2 (*this should be the fallback for rational numbers*)
+ fun get_ring_op_type t1 t2 =
+ if get_most_general_type t1 t2 = natT then intT else get_most_general_type t1 t2
+ in
case tag of
(*variables*)
(*here, we get the full name of the variable, then we return the term well named and typed.
@@ -157,30 +157,26 @@ Bound 0 is usefull for the statements, and can easily be deleted if necessary*)
SOME(identifier) => identifier
| NONE => error("(convertExpr) identifier "
^ id ^ " not recognised")
- val Type(local_state_scheme, _) = sigma_i;
- val local_state = String.substring (local_state_scheme, 0,
- String.size local_state_scheme
- - (String.size "_scheme"))
(*dangerous. will work only for the local case *)
- val lid = local_state^"."^id
in case cat of
- C_AbsEnv.Global => read_N_coerce_global thy id (sigma_i --> ty) $ Free("\<sigma>",sigma_i) :: c
+ C_AbsEnv.Global => read_N_coerce_global thy id (sigma_i --> ty) $ Free("\<sigma>",sigma_i)::c
| C_AbsEnv.Local(_) => Const(@{const_name "comp"},
(HOLogic.listT ty --> ty)
--> (sigma_i --> HOLogic.listT ty)
--> sigma_i --> ty)
$ Const(@{const_name "hd"}, HOLogic.listT ty --> ty)
- $ read_N_coerce thy lid (sigma_i --> HOLogic.listT ty)
+ $ read_N_coerce thy id (sigma_i --> HOLogic.listT ty)
$ Free("\<sigma>",sigma_i) :: c
| C_AbsEnv.Parameter(_) => Free (id, ty) :: c
| C_AbsEnv.FunctionCategory(C_AbsEnv.MutuallyRecursive(_), _) =>
error("Mutual recursion is not supported in Clean")
- | C_AbsEnv.FunctionCategory(a, b) =>
+ | C_AbsEnv.FunctionCategory(_, _) =>
let fun get_call_const id = Syntax.read_term_global thy id
+ (* There is no term corresponding to the function. Hence skip the
+ initialization of the type and infer it from the call args (see CCall0)*)
fun get_rec_call_ident id= Free(id,
(TVar (("'a", 0), [])) --> sigma_i --> (Type (@{type_name "option"}, [mk_tupleT [ty, sigma_i]])))
in (if function_name = id then get_rec_call_ident id else get_call_const id) :: c end
- | c => error("(convertExpr) unrecognised category : " ^ @{make_string} c)
end)
|"Vars0" => c
|"CVar0" => c
@@ -189,10 +185,10 @@ Bound 0 is usefull for the statements, and can easily be deleted if necessary*)
(*binary operations*)
|"CBinary0" => (case (drop_dark_matter sub_tag, c) of
(*arithmetic operations*)
- ("CAddOp0",b::a::R) => (Const(@{const_name "plus"}, fastype_of a --> fastype_of b --> intT) $ a $ b :: R)
- | ("CMulOp0",b::a::R) => (Const(@{const_name "times"}, fastype_of a --> fastype_of b --> intT) $ a $ b :: R)
- | ("CDivOp0",b::a::R) => (Const(@{const_name "divide"}, fastype_of a --> fastype_of b --> intT) $ a $ b :: R)
- | ("CSubOp0",b::a::R) => (Const(@{const_name "minus"}, fastype_of a --> fastype_of b --> intT) $ a $ b :: R)
+ ("CAddOp0",b::a::R) => let val ty = get_most_general_type (fastype_of a) (fastype_of b) in (Const(@{const_name "plus"}, ty --> ty --> ty) $ a $ b :: R) end
+ | ("CMulOp0",b::a::R) => let val ty = get_most_general_type (fastype_of a) (fastype_of b) in (Const(@{const_name "times"}, ty --> ty --> ty) $ a $ b :: R) end
+ | ("CDivOp0",b::a::R) => let val ty = get_ring_op_type (fastype_of a) (fastype_of b) in (Const(@{const_name "divide"}, ty --> ty --> ty) $ a $ b :: R) end
+ | ("CSubOp0",b::a::R) => let val ty = get_ring_op_type (fastype_of a) (fastype_of b) in (Const(@{const_name "minus"}, ty --> ty --> ty) $ a $ b :: R) end
(*boolean operations*)
(*for boolean operations, because in C boolean are in fact integers, we need to
translate integers in booleans. That's what term_to_bool t do.
@@ -208,18 +204,22 @@ translate integers in booleans. That's what term_to_bool t do.
| ("CEqOp0", b::a::R) => (mk_eq ( a, b) :: R)
| ("CNeqOp0", b::a::R) => (mk_not (mk_eq ( a, b))::R)
(*comp*)
- | ("CLeOp0", b::a::R) => (Const(@{const_name "less"},
- fastype_of a --> fastype_of b --> boolT)
- $ a $ b :: R)
- | ("CGrOp0", b::a::R) => (Const(@{const_name "less"},
- fastype_of a --> fastype_of b --> boolT)
- $ b $ a :: R)
- | ("CLeqOp0", b::a::R) => (Const(@{const_name "less_eq"},
- fastype_of a --> fastype_of b --> boolT)
- $ a $ b :: R)
- | ("CGeqOp0", b::a::R) => (Const(@{const_name "less_eq"},
- fastype_of a --> fastype_of b --> boolT)
- $ b $ a :: R)
+ | ("CLeOp0", b::a::R) => let val ty =get_most_general_type (fastype_of a) (fastype_of b)
+ in (Const(@{const_name "less"},
+ ty --> ty --> boolT)
+ $ a $ b :: R) end
+ | ("CGrOp0", b::a::R) => let val ty =get_most_general_type (fastype_of a) (fastype_of b)
+ in (Const(@{const_name "less"},
+ ty --> ty --> boolT)
+ $ b $ a :: R) end
+ | ("CLeqOp0", b::a::R) => let val ty =get_most_general_type (fastype_of a) (fastype_of b)
+ in (Const(@{const_name "less_eq"},
+ ty --> ty --> boolT)
+ $ a $ b :: R) end
+ | ("CGeqOp0", b::a::R) => let val ty =get_most_general_type (fastype_of a) (fastype_of b)
+ in (Const(@{const_name "less_eq"},
+ ty --> ty --> boolT)
+ $ b $ a :: R)end
| _ => (writeln ("sub_tag all " ^sub_tag^" :>> "^ @{make_string} c);c ))
(*unary operations*)
|"CUnary0" => (case (drop_dark_matter sub_tag, c) of
@@ -230,7 +230,7 @@ translate integers in booleans. That's what term_to_bool t do.
(*for the constants, we can use the makers*)
|"CConst0" => c (* skip this wrapper *)
|"CInteger0" =>let val C11_Ast_Lib.data_int n = hd args
- in (mk_number intT n)::c end
+ in (mk_number (if n>=0 then natT else intT) n)::c end
|"CIntConst0"=> c (* skip this wrapper *)
|"CString0" => let val C11_Ast_Lib.data_string s = hd args
in (mk_string s)::c end
@@ -274,17 +274,26 @@ translate integers in booleans. That's what term_to_bool t do.
|"CFloatConst0"=> (c) (* skip this wrapper *)
|"CChars0" => (warning "bizarre rule in context float: CChars0"; c)
|"CExpr0" => c (* skip this wrapper *)
- |"CTypeSpec0" => c (* skip this wrapper *)
- |"CDeclr0" => c (* skip this wrapper *)
- |"CInitExpr0" => error "init expression currently unsupported" (* skip this wrapper *)
- |"CDecl0" => let fun handleDeclaration stack = tl stack
+ (*this is a very dirty trick: when declaring variables "int a,b=3,c,d=4;", the accesses to a and c lie
+ on the stack, polluting it. All non-assignments are thus removed, up until this item is met on the stack*)
+ |"CTypeSpec0" => ((Free ("--startofdeclarations--",@{typ unit}))::c)
+ |"CDeclr0" => c
+ |"CDecl0" => let fun is_assignment ((Const (@{const_name "assign_local"},_))$_$_) = true
+ |is_assignment ((Const (@{const_name "assign_global"},_))$_$_) = true
+ |is_assignment _ = false
+ fun remove_dead_idents [] = []
+ |remove_dead_idents (Free("--startofdeclarations--",_)::R) = R
+ |remove_dead_idents (head::R) = if is_assignment head then (head::remove_dead_idents R)
+ else remove_dead_idents R
in
- handleDeclaration c
+ remove_dead_idents c
end
|"CCall0" => c (* skip this wrapper *)
|"CNoArrSize0" => c
|"CArrDeclr0" => c
- | str => error("unsupported expression with parse tag: "^str)) (* global catch all *)
+ | str => error("unsupported expression with parse tag: "^str^"and subtag: "^sub_tag)
+end) (* global catch all *)
+
fun lifted_term sigma_i term = Abs("\<sigma>", sigma_i, abstract_over (Free("\<sigma>", sigma_i), term))
@@ -349,12 +358,10 @@ fun convertStmt verbose sigma_i nEenv thy function_name get_loop_annotations
(a as { tag, sub_tag, args }:C11_Ast_Lib.node_content)
(b: C_Ast.nodeInfo )
(stack : term list) =
- ((if verbose then (writeln("tag:"^tag);print_node_info a b stack) else ());
- case tag of
-
- "CAssign0" => (case stack of
+
+ let fun handle_assign stack = (case stack of
(rhs :: lhs :: R) =>
- ((let
+ ((let
fun getLongId lhs = (case lhs of
Const(name, _) $ _ => name
| _ $ _ $ Const(name, _) $ _ => name
@@ -362,83 +369,70 @@ fun convertStmt verbose sigma_i nEenv thy function_name get_loop_annotations
| Const ("List.nth", _) $ lhs_candidat $ _ => (getLongId lhs_candidat)
| _ => error("(convertStmt) CAssign0 does not recognise term: "
^(@{make_string} lhs)^"With stacK"^(@{make_string} stack)))
- val long_id = getLongId lhs
- val (id, lid) = extract_ids long_id sigma_i
- fun is_id (C_AbsEnv.Identifier(id_name, _, _, _)) = id_name = id
- val C_AbsEnv.Identifier(id, _, ty, cat) =
+ val ident_id = getLongId lhs
+
+ val C_AbsEnv.Identifier(_, _, ty, cat) = let
+ fun is_id (C_AbsEnv.Identifier(id_name, _, _, _)) = id_name = Long_Name.base_name ident_id in
case List.find is_id nEenv of SOME x => x
- | _ => error("id not found: "^ long_id)
+ | _ => error("id not found: "^ ident_id) end
+ val (update_func_ty, mk_assign) = case cat of C_AbsEnv.Global => (((ty --> ty) --> sigma_i --> sigma_i), mk_assign_global_C)
+ |C_AbsEnv.Local _ => (((listT ty --> listT ty) --> sigma_i --> sigma_i), mk_assign_local_C)
+ | _ => error ("Assignment to "^ident_id^" not possible (is it a parameter?)")
+ val update_func = get_update_fun thy ident_id update_func_ty
fun get_base_type lhs ty =
- case lhs of Const ("List.nth", typedef) $ lhs_part1 $ idx_term =>
+ case lhs of Const ("List.nth", _) $ lhs_part1 $ _ =>
get_base_type lhs_part1 (dest_listTy ty)
| _ => ((if (is_listTy ty) then warning "Assigning list of elements to variable. This is not possible in C, however supported by Clean" else ());ty)
val tempvarn = "tmpvar"
+ val tempvart = (get_base_type lhs ty)
val is_fun_assignment = (case rhs of Const (@{const_name "Clean.call\<^sub>C"},_) $_ $_ => true
| _ => false)
- val rhs_old = rhs
- val tempvart = (get_base_type lhs ty)
- val rhs = (if is_fun_assignment then Free (tempvarn, tempvart) else rhs)
- fun mk_list_type ty = Type(@{type_name "list"}, [ty]) (* This is from "isa_termstypes.ML" *)
+ (*Here comes the array part. Since only entire "rows" of arrays can be replaced,
+ for the expression A[1][2] = b, the right hand side of the CLEAN-statement has
+ to include parts of the LHS, which makes this transformation rather ugly, especially
+ in combination with function calls.
+ Based on the LHS, the function get_array_assignment provides, for the above example,
+ a function:
+ \<lambda>rhs. A[1:= (A!1 [2:= rhs])
+ *)
fun mk_list_update_t ty = Const(@{const_name "List.list_update"}, (* This is from "isa_termstypes.ML" *)
- mk_list_type ty --> natT -->
- ty --> mk_list_type ty)
- fun transform_rhs_list_assignment lhs_part value ty=
- case lhs_part of Const ("List.nth", typedef) $ lhs_part1 $ idx_term => (
+ listT ty --> natT --> ty --> listT ty)
+ fun transform_rhs_list_assignment lhs_part ty value=
+ case lhs_part of Const ("List.nth", _) $ lhs_part1 $ idx_term => (
let
-
val lst_update_t = mk_list_update_t ty
val updated = lst_update_t $ lhs_part1 $ idx_term $ value
in
- transform_rhs_list_assignment lhs_part1 updated (listT ty)
+ transform_rhs_list_assignment lhs_part1 (listT ty) updated
end
)
- | _ => value
-
- fun transform_lhs_for_rhs_transformation lhs_part final_term =
- case lhs_part of Const (@{const_name "nth"}, typedef) $ lhs_part1 $ idx_term =>
- Const (@{const_name "nth"}, typedef) $ (transform_lhs_for_rhs_transformation lhs_part1 final_term) $ idx_term
- | _ => final_term
-
- val access_term = case cat of C_AbsEnv.Global => (read_N_coerce_global thy id (sigma_i --> ty) $ Free("\<sigma>",sigma_i))
- |_ => Const(@{const_name "comp"},
- (HOLogic.listT ty --> ty)
- --> (sigma_i --> HOLogic.listT ty)
- --> sigma_i --> ty)
- $ Const(@{const_name "hd"}, HOLogic.listT ty --> ty)
- $ read_N_coerce thy lid (sigma_i --> HOLogic.listT ty)
- $ Free("\<sigma>",sigma_i)
-
-
- val lhs_tmp = transform_lhs_for_rhs_transformation lhs access_term
-
- val new_rhs = transform_rhs_list_assignment lhs_tmp rhs (get_base_type lhs ty)
-
- val (id, lid) = (id ^ "_update", lid ^ "_update")
-
-
- in case cat of
- C_AbsEnv.Global => (if is_fun_assignment then ( mk_seq_assign_C rhs_old (((mk_assign_global_C
- (read_N_coerce_global thy id
- ((ty --> ty) --> sigma_i --> sigma_i)))
- (lifted_term sigma_i new_rhs))) tempvarn tempvart)
- else (
- ((mk_assign_global_C
- (read_N_coerce_global thy id
- ((ty --> ty) --> sigma_i --> sigma_i)))
- (lifted_term sigma_i new_rhs))))::R
- | C_AbsEnv.Parameter(_) => error "assignment to parameter not allowed in Clean"
- | C_AbsEnv.Local(_) => (if is_fun_assignment then (mk_seq_assign_C rhs_old (mk_assign_local_C
- (read_N_coerce thy lid
- ((listT ty --> listT ty) --> sigma_i --> sigma_i))
- (lifted_term sigma_i new_rhs) ) tempvarn tempvart)
- else ((mk_assign_local_C
- (read_N_coerce thy lid
- ((listT ty --> listT ty) --> sigma_i --> sigma_i))
- (lifted_term sigma_i new_rhs) )))::R
- | s => error("(convertStmt) CAssign0 with cat "
- ^ @{make_string} s ^ " is unrecognised")
+ | _ => value
+
+ val get_array_assignment = transform_rhs_list_assignment lhs (get_base_type lhs ty)
+
+
+ val assignment =if is_fun_assignment then ( mk_seq_assign_C
+ rhs
+ (((mk_assign update_func)
+ (lifted_term sigma_i (get_array_assignment (Free (tempvarn,tempvart))))))
+ tempvarn
+ tempvart)
+ else (
+ ((mk_assign
+ update_func)
+ (lifted_term sigma_i (get_array_assignment rhs))))
+ val inferred_assignment = Syntax.check_term (Proof_Context.init_global thy) assignment
+ in assignment::R
end))
|_ => raise WrongFormat("assign"))
+
+ in ((if verbose then (writeln("tag:"^tag);print_node_info a b stack) else ());
+ if tag="CBinary0" andalso
+ case stack of (head::_) => is_call head |_=>false
+ then error ("Function call only allowed on RHS of assignment. Tag: "^tag) else ();
+ case tag of
+ "CAssign0" => handle_assign stack
+ |"CInitExpr0" => handle_assign stack
(*statements*)
(*for return, skip and break, we have makers except that they need types and terms that i didn't
understand so it's unfinished here*)
@@ -459,8 +453,12 @@ if ... then ... else skip*)
| "CBlockStmt0" => stack
| "CBlockDecl0" => stack
| "CNestedFunDef0" => error"Nested Function Declarations not allowed in Clean"
- | "CIf0" => (case stack of
- (a::b::cond::R) => mk_if_C (lifted_term sigma_i cond) b a :: R
+ | "CIf0" => (case stack of (*checking based on how many elements are on the stack is wrong.
+ instead check the type of the condition. It must be a value (i.e. no function)*)
+ (a::b::c::R) => (case fastype_of b of Type ("fun",_)=> mk_if_C (lifted_term sigma_i c) b a :: R (*b is not the condition*)
+ | _ => (mk_if_C (lifted_term sigma_i b) (*b is the cond no else*)
+ (a)
+ (mk_skip_C sigma_i)::R))
| (a::cond::R) => (mk_if_C (lifted_term sigma_i cond)
(a)
(mk_skip_C sigma_i)::R)
@@ -507,24 +505,29 @@ for(ini, cond, evol){body} is translated as ini; while(cond){body; evol;}*)
in ((mk_seq_C init C'))::R end)
|_ => raise WrongFormat("for")) end
| "CCall0" => (let fun extract_fun_args (t :: R) args =
- case t of
+ (case t of
(* very bad way of checking if term represents a function *)
Const(id, ty) => if not (firstype_of ty = sigma_i)
then (args, Const(id, ty), R)
else extract_fun_args R (Const(id, ty) :: args)
- | Free(id, ty) => if id = function_name
+ | Free(id, ty) => if id = function_name (*recursive call*)
then (args, Free(id, ty), R)
else extract_fun_args R (Free(id, ty) :: args)
- | arg => extract_fun_args R (arg :: args)
+ | arg => extract_fun_args R (arg :: args))
+ |extract_fun_args [] _ = error ("\"CCall0\": couldnt find function in stack: "^(@{make_string} stack))
val (args, f, R) = extract_fun_args stack []
- val Type (_, [arg_ty,r_ty]) = fastype_of f
- val Type (_,[old_sigma_ty, r_ty]) = r_ty
- val Type (_,[Type(_, [ret_ty, old_sigma1_ty])]) = r_ty
+ val ret_ty = case fastype_of f of Type (_, [_, (*args \<rightarrow>*)
+ Type (_, [_, (*sigma \<rightarrow>*)
+ Type (_, [ (*'a option*)
+ Type(_, [ret_ty, _])])])]) => ret_ty (* (ret_type, sigma)*)
+ | _ => error ("function type has wrong format: "^(@{make_string} (fastype_of f)))
+
val new_args_ty = mk_tupleT (List.map fastype_of args)
val new_ty = new_args_ty --> sigma_i --> (Type (@{type_name "option"},[Type (@{type_name "prod"}, [ret_ty,sigma_i])]))
fun swap_ty (Const (name, _)) n_ty = Const (name, n_ty)
|swap_ty (Free (name, _)) n_ty = Free (name, n_ty)
+ |swap_ty _ _ = error "unexpected term at swap_ty"
val f_new = swap_ty f new_ty
val fun_args_term = mk_tuple args
@@ -535,6 +538,7 @@ end
(*** -------------- ***)
+end
end
\<close>
diff --git a/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy b/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
index 8c883fb7d66665419ffc666c99c5c22381e47aba..0773f0e28df698a70a4c6b41bdcbaf2cd33f4ace 100644
--- a/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
+++ b/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
@@ -555,9 +555,21 @@ fun parseExternalDeclaration
(selectFromNodeContent ["Ident0", "CTypeSpec0",
"CArrDeclr0", "CDeclr0", "CCall0"])
statement [])
- val (newIdentList, functionCategory, newFunctionCallTable) =
+ (*we need to sort out the local identifiers of previous functions, as they are no longer accessible*)
+ fun sortIdentifiers [] = ([],[])
+ |sortIdentifiers (ident::R) = let
+ val (prev_glob, prev_loc) = sortIdentifiers R
+ in case ident of Identifier (_,_,_,Global)=> (ident::prev_glob, prev_loc)
+ |Identifier (_,_,_,FunctionCategory _) => (ident::prev_glob, prev_loc)
+ |_ => (prev_glob, ident::prev_loc)
+
+ end
+
+ val (previous_global_identifiers, previous_local_identifiers) = sortIdentifiers (identList)
+ val (newIdentList', functionCategory, newFunctionCallTable) =
parseLocals statementContentList functionName functionCallTable
- (paramIdentifiers @ identList) oldIdents
+ (paramIdentifiers@previous_global_identifiers) oldIdents
+ val newIdentList = newIdentList'@previous_local_identifiers
in (Identifier(functionName, posL, functionReturnHOLType,
FunctionCategory(functionCategory, SOME(statement))) :: newIdentList,
newFunctionCallTable)
diff --git a/C11-BackEnds/Clean_wrapper/src/CleanTranslationHook.thy b/C11-BackEnds/Clean_wrapper/src/CleanTranslationHook.thy
new file mode 100644
index 0000000000000000000000000000000000000000..7dfae361f48c2aea08aac0e80938e3220f603ef3
--- /dev/null
+++ b/C11-BackEnds/Clean_wrapper/src/CleanTranslationHook.thy
@@ -0,0 +1,192 @@
+theory "CleanTranslationHook"
+ imports "../src/CleanCoder" (* Coder_Test_Env_AEnv *)
+ "../src/compiler/Clean_Annotation"
+begin
+ML\<open>
+(*This is an override for the update_Root_Ast function that is registered in C_Command.*)
+
+fun transform_type typ = if typ = HOLogic.intT then "int"
+ else if typ = HOLogic.natT then "nat"
+ else if is_listTy typ then (transform_type (dest_listTy typ))^" list"
+ else if typ = HOLogic.unitT then "unit"
+ else error "Unknown variable type"
+
+local open C_AbsEnv HOLogic in
+fun get_hol_type (C_Env.Parsed ret) params = let
+ val base_type =the (C11_TypeSpec_2_CleanTyp.conv_cDeclarationSpecifier_typ (SOME ret))
+ fun transform_type ((C_Ast.CArrDeclr0 _)::R) base_type = listT (transform_type R base_type)
+ | transform_type [] base_type = base_type
+ | transform_type ps _ = error ("First type parameter unknown (maybe pointers): "^(@{make_string} ps))
+ in transform_type params base_type end
+ |get_hol_type a _ = error ("Can not get type of \""^(@{make_string} a)^"\"")
+fun map_env_ident_to_identifier (name,(positions,_,data)) =
+ let fun get_ident_scope C_Env.Global = Global
+ |get_ident_scope C_Env.Local = Local ""
+ |get_ident_scope C_Env.Parameter = Parameter ""
+ in
+ case #functionArgs data of C_Ast.None => Identifier(name, if null positions then @{here} else hd positions,get_hol_type (#ret data) (#params data),get_ident_scope (#scope data))
+ |_=> Identifier(name, @{here},intT,FunctionCategory (Final, NONE)) (*this line is wrong because of different function types*)
+ end
+end
+
+fun declare_function idents name ast ret_ty recursive ctxt =
+ let val param_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Parameter f_name) => f_name = name |_=>false) idents
+ val local_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Local f_name) => f_name = name |_=>false) idents
+ val global_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Global) => true
+ | C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _)=>true
+ | _ => false) idents
+
+ (*Obtain the parameters and local variables*)
+ val params = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ)) (param_idents)
+ val locals = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ, NoSyn)) (local_idents)
+
+ (*This is necessary, as parameters are represented as free variables.
+ When the Invariants, post- and preconditions are read through the term antiquotations,
+ Syntax.parse_term (Syntax.read_term does this too) would substitute them by another const,
+ which could be a local or global variable*)
+ fun remove_params_from_proof ctx = let
+ val param_names = List.map (fn C_AbsEnv.Identifier(n,_,_,_) => n) param_idents
+ fun filter_by_shortname param_names (n, _) =
+ List.exists (fn ele => ele = Long_Name.base_name n) param_names
+ val longnames = List.filter (filter_by_shortname param_names) (#constants (Consts.dest (Sign.consts_of (Proof_Context.theory_of ctx))))
+ val thy0 = Proof_Context.theory_of ctx
+ val thy' = List.foldl (fn (longname, thy')=> thy' |> Sign.hide_const true longname) thy0 (List.map fst longnames)
+ in Proof_Context.init_global thy' end
+
+ (*Invariants and measuress need to be matched to a loop. This is done by comparing the parse locations of all while loops.
+ The following are helper methods, to obtain the function get_invariant::positiona \<rightarrow> (context\<rightarrow>term) option*)
+ val invariants:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
+ (#invariants (Clean_Annotation.Data_Clean_Annotations.get ctxt))
+ val measures:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
+ (#measures (Clean_Annotation.Data_Clean_Annotations.get ctxt))
+ val loop_pos =Library.distinct (op =) (C11_Ast_Lib.fold_cStatement (fn a => fn b => a@b) C11_Unit_2_Clean.get_loop_positions ast [])
+ fun compare_pos ((C_Ast.Position0 (pos1,_,_,_)),(C_Ast.Position0 (pos2,_,_,_))) = Int.compare (pos1,pos2)
+ |compare_pos a = error ("Unable to compare positions (for invariants and measures): "^(@{make_string} a))
+ val loop_pos_sorted = Library.sort compare_pos loop_pos
+ fun range_less_than_pos (range:Position.range) (C_Ast.Position0 (pos,_,_,_)) = the (Position.offset_of (fst range)) < pos
+ |range_less_than_pos a b = error ("Unable to compare positions (for invariants and measures): "^(@{make_string} (a,b)))
+ fun get_for_position (((inv,inv_pos)::R_inv): ((Context.generic -> term)*Position.range)list)
+ (loop_positions: C_Ast.positiona list)
+ (pos3: C_Ast.positiona)
+ (* search the first invariant, which is not declared before pos3 *)
+ = (if range_less_than_pos inv_pos pos3 then get_for_position R_inv loop_positions pos3
+ else case loop_positions of (* we found the first invariant after pos3 *)
+ (* Now check, if the next loop definition is after the invariant definition.
+ Otherwise there is no invariant for the given loop *)
+ (pos1::pos2::R) => if pos3 = pos1 andalso range_less_than_pos inv_pos pos2 then SOME inv
+ else get_for_position ((inv,inv_pos)::R_inv) (pos2::R) pos3
+ | (pos1::_) => if pos3 = pos1 then SOME inv else NONE
+ | [] => NONE)
+ |get_for_position [] _ _ = NONE
+ fun get_invariant pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) invariants) loop_pos_sorted) pos
+ fun get_measure pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) measures) loop_pos_sorted) pos
+ fun get_loop_annotations pos = (get_invariant pos, get_measure pos)
+
+ (*generic function to get the first ele*)
+ val get_precond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#preconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
+ val get_postcond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#postconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
+
+ (*the translation of the precondition*)
+ fun get_translation NONE default ctxt= C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type (ctxt)) default
+ | get_translation (SOME get_term) _ ctxt= let
+ val term = get_term (Context.Proof (remove_params_from_proof ctxt))
+ val lifted = C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type ctxt) term
+ in
+ Syntax.check_term ctxt lifted
+ end
+ (*The actual translation of the loop body*)
+ fun get_translated_fun_bdy ctx _ = let
+ val ctx' = remove_params_from_proof ctx
+ val v = ((C11_Ast_Lib.fold_cStatement
+ C11_Stmt_2_Clean.regroup
+ (C11_Stmt_2_Clean.convertStmt false
+ (StateMgt.get_state_type ctx')
+ (local_idents@param_idents@global_idents)
+ (Proof_Context.theory_of ctx')
+ name get_loop_annotations)
+ ast []))
+ in ( hd) v end
+
+ val test_function_sem = {binding = Binding.name name,
+ locals = locals@[(Binding.name "dummylocalvariable","int", NoSyn)], (*There needs to be at least one local variable*)
+ params = params,
+ ret_type = transform_type ret_ty,
+ read_pre = get_translation get_precond (@{term True}),
+ read_post = get_translation get_postcond (Abs ("ret",ret_ty, @{term True})),
+ read_variant_opt = NONE,
+ read_body = get_translated_fun_bdy}
+ val decl = Function_Specification_Parser.checkNsem_function_spec_gen {recursive = recursive} test_function_sem
+ in decl end
+
+local open C_AbsEnv HOLogic in
+fun handle_declarations translUnit ctxt =
+ (let
+ (*get the OLD environment, which simplifies the parseTranslUnitIdentifiers by a lot.*)
+ val env = (C_Module.Data_Last_Env.get ctxt)
+ (*First we need to get all previously defined global vars and functions*)
+ val prev_idents =map map_env_ident_to_identifier (Symtab.dest (#idents(#var_table(env))))
+ (*the new identifiers are returned in reverse \<rightarrow> thus reverse *)
+ val (new_idents, call_table) = C_AbsEnv.parseTranslUnitIdentifiers translUnit [] prev_idents Symtab.empty
+ val identifiers = (rev new_idents)@prev_idents
+ val map_idents = List.map (fn C_AbsEnv.Identifier(name,_,typ,_) => (Binding.name name, transform_type typ, NoSyn))
+
+ fun get_declaration is_global idents = if null idents then I else StateMgt.new_state_record is_global (NONE,idents)
+
+ val global_idents = (map_idents (List.filter (fn C_AbsEnv.Identifier(_,_,_,vis) => vis = C_AbsEnv.Global) new_idents))
+ val global_declaration =get_declaration true global_idents
+
+ val fun_asts =
+ List.map (fn C_AbsEnv.Identifier(name,_,ret_ty,C_AbsEnv.FunctionCategory ast) =>
+ let fun is_recursive NONE = false
+ |is_recursive (SOME calls) = List.exists (fn x => x=name) calls
+ in
+ (name,the (snd ast),ret_ty, is_recursive (Symtab.lookup call_table name)) end
+ | ident => error ("Expected function identifier. Instead: "^(@{make_string} ident)))
+
+ (List.filter (fn a => case a of C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _) => true | _ => false) (rev new_idents))
+ val function_declarations = List.map (fn (name,ast,ret_ty, recursive) => declare_function identifiers name ast ret_ty recursive ctxt) (fun_asts)
+ val function_decl = fold (fn f => fn acc => f acc) function_declarations
+ in
+ Context.map_theory (function_decl o global_declaration) ctxt
+ end);
+end
+\<close>
+ML\<open>
+fun handle_declarations_wrapper ast v2 ctxt =
+ let val ctx1 = update_Root_Ast SOME ast v2 ctxt (*Note the call to the original callback - this somehow gets overwritten*)
+ in
+ case ast of (C_Ast.Left translUnit) => handle_declarations translUnit ctx1
+ | _ => ctx1
+ end
+\<close>
+setup \<open>C_Module.C_Term.map_expression
+ (fn cexpr => fn _ => fn ctxt => let
+ val sigma_i = (StateMgt.get_state_type o Context.proof_of )ctxt
+ val env = C_Module.Data_Surrounding_Env.get ctxt
+ val idents = (Symtab.dest (#idents(#var_table(env))))
+ val A_env = List.map map_env_ident_to_identifier idents
+ val expr = (hd (C11_Ast_Lib.fold_cExpression (K I)
+ (C11_Expr_2_Clean.convertExpr false sigma_i A_env (Context.theory_of ctxt) "" (K NONE))
+ cexpr [])) handle ERROR msg => (writeln("ERROR: "^(@{make_string}msg));@{term "1::int"})
+in
+ expr
+ end)\<close>
+setup \<open>Context.theory_map (C_Module.Data_Accept.put (handle_declarations_wrapper))\<close>
+
+(* Note: The hook "C_Module.C_Term.map_translation_unit" is not adequate, as it is
+ meant for the term antiquotation (its callback returns a term, not a theory/context *)
+
+setup \<open>C_Module.C_Term.map_expression
+ (fn cexpr => fn _ => fn ctxt => let
+ val sigma_i = (StateMgt.get_state_type o Context.proof_of )ctxt
+ val env = C_Module.Data_Surrounding_Env.get ctxt
+ val idents = (Symtab.dest (#idents(#var_table(env))))
+ val A_env = List.map map_env_ident_to_identifier idents
+ val expr = (hd (C11_Ast_Lib.fold_cExpression (K I)
+ (C11_Expr_2_Clean.convertExpr false sigma_i A_env (Context.theory_of ctxt) "" (K NONE))
+ cexpr [])) handle ERROR msg => (writeln("ERROR: "^(@{make_string}msg));@{term "1::int"})
+in
+ expr
+ end)\<close>
+
+end
\ No newline at end of file
diff --git a/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy b/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
index 84450ef852623ddc54d69d1f44eb6720501dbf0d..12df4f496390b528d0ce1bd54d94ccdf89c90cae 100644
--- a/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
+++ b/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
@@ -79,7 +79,7 @@ structure Data_Clean_Annotations = Generic_Data
fun map_context_annotation_declaration annotation_type src range context0 =
let
- val current_env =snd (C_Stack.Data_Lang.get' context0)
+ val current_env =snd (C_Stack.Data_Lang.get' context0) (*important: antiquotation needs current env*)
fun get_fun_name [(SOME (C_Ast.Ident0 (C_Ast.SS_base (C_Ast.ST name), _, _)),_)] = name
| get_fun_name (_::R) = get_fun_name R
| get_fun_name _ = (warning "unable to find name of surrounding function for CLEAN annotation";"")
diff --git a/C11-FrontEnd/examples/C5.thy b/C11-FrontEnd/examples/C5.thy
new file mode 100644
index 0000000000000000000000000000000000000000..1bb1e23de6c80ddebe8de084c9f847edba87c69e
--- /dev/null
+++ b/C11-FrontEnd/examples/C5.thy
@@ -0,0 +1,100 @@
+theory C5
+ imports "Isabelle_C.C_Main"
+begin
+
+(*This file contains some ways to retrieve the C-environment*)
+
+ML\<open>
+val SPY_ENV = Unsynchronized.ref(NONE:C_Env.env_lang option);\<close>
+declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
+declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
+
+C\<open>
+int globalvar1;
+void test(int param1){
+ int localvariable1;
+
+ return 12; /*@ \<approx>setup \<open>fn _ => fn _ => fn env =>
+ (*The environment can be retrieved using the generic setup command*)
+ ((SPY_ENV := SOME env);I) \<close> */;
+ int localvariable2;
+}
+int globalvar2;
+\<close>
+
+ML\<open>
+(*We can see that the saved env in fact has all the current variables*)
+val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
+ #idents(#var_table(the (!SPY_ENV))))
+))
+val final_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
+ #idents(#var_table(@{C\<^sub>e\<^sub>n\<^sub>v})))))
+\<close>
+
+(*There is a second way to achieve the same, using the context*)
+C\<open>
+int globalvar3;
+void test2(int param1){
+ int localvariable3;
+
+ return 12; /*@ \<approx>setup \<open>fn _ => fn _ => fn _ => fn ctx =>
+ (*The environment can be retrieved using the generic setup command*)
+ ((SPY_ENV := SOME (snd (C_Stack.Data_Lang.get' ctx)));ctx) \<close> */;
+ int localvariable4;
+}
+int globalvar4;
+\<close>
+
+ML\<open>
+(*We can see that the saved env in fact has all the current variables*)
+val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
+ #idents(#var_table(the (!SPY_ENV))))
+))
+\<close>
+
+
+(*Declaring a seperate antiquotation *)
+
+ML\<open>
+val env = @{C\<^sub>e\<^sub>n\<^sub>v}\<close>
+
+ML\<open>
+Theory.setup
+ (C_Inner_Syntax.command_no_range
+ (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup
+ \<open>fn ((_, (_, pos1, pos2)) :: _) =>
+ (fn _ => fn _ =>
+ tap (fn ctx =>
+ (SPY_ENV := SOME (snd (C_Stack.Data_Lang.get' ctx));Position.reports_text [((Position.range (pos1, pos2)
+ |> Position.range_position, Markup.intensify), "")])))
+ | _ => fn _ => fn _ => I\<close>)
+ ("store_and_highlight", \<^here>, \<^here>))
+\<close>
+
+(*this is btw how all previous identifiers can get deleted*)
+setup\<open>Context.theory_map (C_Module.Data_In_Env.put C_Env.empty_env_lang)\<close>
+
+C\<open>
+int globalvar3;
+void test2(int param1){
+ int localvariable3;/*@ store_and_highlight */
+}
+\<close>
+
+ML\<open>
+val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
+ #idents(#var_table(the (!SPY_ENV)))) (*NOTE: localvariable3 is in the environment*)
+))\<close>
+
+setup\<open>Context.theory_map (C_Module.Data_In_Env.put C_Env.empty_env_lang)\<close>
+
+C\<open>
+int globalvar3;
+void test2(int param1){
+ int localvariable3;/*@@@@@ store_and_highlight */
+}
+\<close>
+ML\<open>
+val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
+ #idents(#var_table(the (!SPY_ENV)))) (*NOTE: localvariable3 is NOT in the environment*)
+))\<close>
\ No newline at end of file
diff --git a/C11-FrontEnd/src/C_Ast.thy b/C11-FrontEnd/src/C_Ast.thy
index f5d9f2db8022386d9f5345887ba179133760eb39..09c55d92e67f848d915c1a22b6cf39fc94b83b8a 100644
--- a/C11-FrontEnd/src/C_Ast.thy
+++ b/C11-FrontEnd/src/C_Ast.thy
@@ -875,7 +875,7 @@ and fold_cExpression grp g ast st =
|> g (TT"CCast0") a
| (CUnary0(unop:cUnaryOp, ex: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex
- |> g (TT("CUnary0 "^toString_cUnaryOp unop)) a
+ |> g (TTT"CUnary0" (toString_cUnaryOp unop)) a
| (CSizeofExpr0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CSizeofExpr0") a
| (CSizeofType0(decl:'a cDeclaration,a)) =>