diff --git a/.gitignore b/.gitignore
index 9c2e31862409d54bf53a74b0b3009d907a363ab6..fd4538e0558cc07e929d1370f2f1ee36bb6921d9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,5 @@ C11-BackEnds/Clean_wrapper/output/document
C11-BackEnds/Clean_wrapper/output/document.pdf
C11-FrontEnd/generated/document
C11-FrontEnd/generated/document.pdf
+*.thy~
+*.thy#
\ No newline at end of file
diff --git a/C11-BackEnds/Clean/examples/Quicksort.thy b/C11-BackEnds/Clean/examples/Quicksort.thy
index 4627cb43bda13eb52bea811531339bfc6c928203..4db779b644ec2fca63bf1eff03424244d8aa50de 100644
--- a/C11-BackEnds/Clean/examples/Quicksort.thy
+++ b/C11-BackEnds/Clean/examples/Quicksort.thy
@@ -88,6 +88,7 @@ section\<open>Clean Encoding of the Global State of Quicksort\<close>
global_vars (state)
A :: "int list"
+ B :: "int list list"
function_spec swap (i::nat,j::nat) \<comment> \<open>TODO: the hovering on parameters produces a number of report equal to the number of \<^ML>\<open>Proof_Context.add_fixes\<close> called in \<^ML>\<open>Function_Specification_Parser.checkNsem_function_spec\<close>\<close>
pre "\<open>i < length A \<and> j < length A\<close>"
@@ -97,6 +98,15 @@ defines " \<open> tmp := A ! i\<close> ;-
\<open> A := list_update A i (A ! j)\<close> ;-
\<open> A := list_update A j tmp\<close> "
+function_spec update_2d_array (i::nat,j::nat, val:: int) \<comment> \<open>TODO: the hovering on parameters produces a number of report equal to the number of \<^ML>\<open>Proof_Context.add_fixes\<close> called in \<^ML>\<open>Function_Specification_Parser.checkNsem_function_spec\<close>\<close>
+pre "\<open>i < length A \<and> j < length A\<close>"
+post "\<open>\<lambda>res. length A = length(old A) \<and> res = ()\<close>"
+local_vars tmp :: int
+defines "
+ \<open> B := list_update B (i+1) (list_update (B!i) j val)\<close>"
+
+find_theorems update_2d_array
+find_theorems update_2d_array_core
function_spec partition (lo::nat, hi::nat) returns nat
pre "\<open>lo < length A \<and> hi < length A\<close>"
@@ -116,6 +126,9 @@ defines " \<open>pivot := A ! hi \<close> ;- \<open>i := lo \<close> ;- \<
call\<^sub>C swap \<open>(i, j)\<close> ;-
return\<^bsub>local_partition_state.result_value_update\<^esub> \<open>i\<close>"
+find_theorems partition
+term partition
+
thm partition_core_def
@@ -137,6 +150,10 @@ thm quicksort_def
thm quicksort_pre_def
thm quicksort_post_def
+find_theorems quicksort_core
+
+
+
section\<open>Possible Application Sketch\<close>
lemma quicksort_correct :
diff --git a/C11-BackEnds/Clean/src/Clean.thy b/C11-BackEnds/Clean/src/Clean.thy
index 55dff1dfed6ddc621d9461269f94c2e086fe37cc..02d3c8ea2a0c6662a1603c584271e9f285941f9e 100644
--- a/C11-BackEnds/Clean/src/Clean.thy
+++ b/C11-BackEnds/Clean/src/Clean.thy
@@ -323,8 +323,8 @@ subsection\<open> The Assignment Operations (embedded in State-Exception Monad)
text\<open>Based on the global variable states, we define \<^term>\<open>break\<close>-aware and \<^term>\<open>return\<close>-aware
version of the assignment. The trick to do this in a generic \<^emph>\<open>and\<close> type-safe way is to provide
the generated accessor and update functions (the ``lens'' representing this global variable,
-cf. \<^cite>\<open>"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
-"DBLP:conf/ictac/FosterZW16"\<close>) to the generic assign operators. This pair of accessor and update
+cf. \cite{"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
+"DBLP:conf/ictac/FosterZW16"} to the generic assign operators. This pair of accessor and update
carries all relevant semantic and type information of this particular variable and \<^emph>\<open>characterizes\<close>
this variable semantically. Specific syntactic support~\<^footnote>\<open>via the Isabelle concept of
cartouche: \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>\<close> will hide away the syntactic overhead
@@ -591,6 +591,9 @@ fun mk_Some t = let val some = \<^const_name>\<open>Option.option.Some\<close>
fun dest_listTy (Type(\<^type_name>\<open>List.list\<close>, [T])) = T;
+fun is_listTy t = case t of (Type(\<^type_name>\<open>List.list\<close>, [T])) => true
+ | _ => false
+
fun mk_hdT t = let val ty = fastype_of t
in Const(\<^const_name>\<open>List.hd\<close>, ty --> (dest_listTy ty)) $ t end
@@ -605,9 +608,13 @@ fun meta_eq_const T = Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> p
fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
+
fun mk_pat_tupleabs [] t = t
| mk_pat_tupleabs [(s,ty)] t = absfree(s,ty)(t)
- | mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t));
+ | mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t))
+fun mk_pat_tupleabs_wrapper [] t = absfree("unitparam",@{typ unit}) t
+ | mk_pat_tupleabs_wrapper R t = mk_pat_tupleabs R t
+
fun read_constname ctxt n = fst(dest_Const(Syntax.read_term ctxt n))
@@ -891,7 +898,7 @@ fun typ_2_string_raw (Type(s,[TFree _])) = if String.isSuffix "_scheme" s
fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
let val state_index = (Int.toString o length o Symtab.dest)
(StateMgt_core.get_state_field_tab_global thy)
- val state_pos = (Binding.pos_of o #1 o hd) raw_fields
+ val state_pos = (Binding.pos_of o #1 o hd) raw_fields (*This hd is probably the reason why we cant have empty local vars*)
val ((raw_params, binding), res_ty) = case aS of
SOME d => d
| NONE => (([], Binding.make(state_index,state_pos)), NONE)
@@ -899,8 +906,6 @@ fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
then mk_global_state_name binding
else mk_local_state_name binding
val raw_parent = SOME(typ_2_string_raw (StateMgt_core.get_state_type_global thy))
- val _ = writeln("XXXXX " ^ @{make_string} raw_params ^ "CCC " ^ @{make_string} binding
- ^ @{make_string} raw_fields)
val pos = Binding.pos_of binding
fun upd_state_typ thy = StateMgt_core.upd_state_type_global
(K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy
@@ -917,8 +922,8 @@ fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
val add_record_cmd = add_record_cmd0 read_fields;
val add_record_cmd' = add_record_cmd0 pair;
-val new_state_record = new_state_record0 add_record_cmd
-val new_state_record' = new_state_record0 add_record_cmd';
+val new_state_record = new_state_record0 add_record_cmd;
+val new_state_record'=new_state_record0 add_record_cmd';
fun clean_ctxt_parser b = Parse.$$$ "("
@@ -1156,13 +1161,13 @@ structure Function_Specification_Parser =
fun define_cond binding f_sty transform_old check_absence_old cond_suffix params read_cond (ctxt:local_theory) =
let val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params
val src' = case transform_old (read_cond ctxt) of
- Abs(nn, sty_pre, term) => mk_pat_tupleabs params' (Abs(nn,sty_pre,term))
- | _ => error ("define abstraction for result" ^ Position.here \<^here>)
+ Abs(nn, sty_pre, term) => mk_pat_tupleabs_wrapper params' (Abs(nn,sty_pre,term))
+ | a => error ("define abstraction for result" ^ (Position.here \<^here>)^(@{make_string}a))
val bdg = Binding.suffix_name cond_suffix binding
val _ = check_absence_old src'
val bdg_ty = HOLogic.mk_tupleT(map (#2) params) --> f_sty HOLogic.boolT
val eq = mk_meta_eq(Free(Binding.name_of bdg, bdg_ty),src')
- val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
+ val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
in StateMgt.cmd args ctxt end
fun define_precond binding sty =
@@ -1177,10 +1182,8 @@ structure Function_Specification_Parser =
val bdg_core_name = Binding.name_of bdg_core
val umty = args_ty --> StateMgt.MON_SE_T @{typ "unit"} sty
-
- val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs params' body)
+ val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs_wrapper params' body)
val args_core =(SOME (bdg_core, SOME umty, NoSyn), (Binding.empty_atts, eq), [], [])
-
in StateMgt.cmd args_core
end
@@ -1199,7 +1202,7 @@ structure Function_Specification_Parser =
val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params
val measure_term = case read_variant_opt of
NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT)
- | SOME f => ((f ctxt) |> mk_pat_tupleabs params')
+ | SOME f => ((f ctxt) |> mk_pat_tupleabs_wrapper params')
val measure = Const(@{const_name "Wellfounded.measure"}, (args_ty --> HOLogic.natT)
--> argsRelSet )
$ measure_term
@@ -1208,7 +1211,7 @@ structure Function_Specification_Parser =
--> args_ty --> rmty) $
Free(bdg_ord_name, args_ty --> HOLogic.natT)
else Free(Binding.name_of binding, args_ty --> rmty)
- val rhs_main = mk_pat_tupleabs params'
+ val rhs_main = mk_pat_tupleabs_wrapper params'
(Const(@{const_name "Clean.block\<^sub>C"}, umty --> umty --> rmty --> rmty)
$ Const(read_constname ctxt (Binding.name_of push_name),umty)
$ (Const(read_constname ctxt bdg_core_name, args_ty --> umty)
@@ -1275,17 +1278,19 @@ val _ = Named_Target.theory_map;
#> define_postcond binding ret_ty sty_old params read_post)
in parse_contract
end
- |> StateMgt.new_state_record false (SOME (([],binding), SOME ret_type),locals)
+ |>(let val v = StateMgt.new_state_record false (SOME (([],binding), SOME ret_type),locals)
+ in v end)
|> theory_map
(fn params => fn ret_ty => fn ctxt =>
- let val sty = StateMgt_core.get_state_type ctxt
+ let
+ val sty = StateMgt_core.get_state_type ctxt
val args_ty = HOLogic.mk_tupleT (map snd params)
val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty
val body = read_body ctxt mon_se_ty
val ctxt' =
if #recursive isrec then
- Proof_Context.add_fixes
- [(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2
+ (Proof_Context.add_fixes
+ [(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2)
else
ctxt
val body = read_body ctxt' mon_se_ty
@@ -1397,7 +1402,7 @@ definition while_C_A :: " (('\<sigma>_ext) control_state_scheme \<Rightarrow> bo
\<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E"
where "while_C_A Inv f c B \<equiv> while_C c B"
-
+
ML\<open>
structure Clean_Term_interface =
@@ -1407,40 +1412,37 @@ fun mk_seq_C C C' = let val t = fastype_of C
val t' = fastype_of C'
in Const(\<^const_name>\<open>bind_SE'\<close>, t --> t' --> t') $ C $ C' end;
+fun mk_seq_assign_C rhs lhs varname vartyp= let
+ val t1 = fastype_of rhs
+ val t2 = fastype_of lhs
+ 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)
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
@@ -1492,17 +1494,19 @@ end;\<close>
section\<open>Function-calls in Expressions\<close>
-text\<open>The precise semantics of function-calls appearing inside expressions is underspecified in C,
+text\<open>The precise semantics of function-calls appearing inside expressions is under-specified in C,
which is a notorious problem for compilers and analysis tools. In Clean, it is impossible by
-construction --- and the type displine --- to have function-calls inside expressions.
+construction --- and the type discipline --- to have function-calls inside expressions.
However, there is a somewhat \<^emph>\<open>recommended coding-scheme\<close> for this feature, which leaves this
issue to decisions in the front-end:
-\begin{verbatim}
- a = f() + g();
-\end{verbatim}
+
+@{verbatim [indent=10, indent=70] \<open>a = f() + g();\<close>}
+
can be represented in Clean by:
-\<open>x \<leftarrow> f(); y \<leftarrow> g(); \<open>a := x + y\<close> \<close> or
-\<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<close> \<close>
+
+@{cartouche [indent=10, indent=70] \<open>x \<leftarrow> f(); y \<leftarrow> g(); \<open>a := x + y\<close> \<close>} or
+@{cartouche [indent=10, indent=70] \<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<close> \<close>}
+
which makes the evaluation order explicit without introducing
local variables or any form of explicit trace on the state-space of the Clean program. We assume,
however, even in this coding scheme, that \<^verbatim>\<open>f()\<close> and \<^verbatim>\<open>g()\<close> are atomic actions; note that this
diff --git a/C11-BackEnds/Clean/src/MonadSE.thy b/C11-BackEnds/Clean/src/MonadSE.thy
index 70ea4d48fdd362c8e530b76cd25c57be1f950610..b6f9589b94931f87440ffad1b8fd4ace40d765df 100644
--- a/C11-BackEnds/Clean/src/MonadSE.thy
+++ b/C11-BackEnds/Clean/src/MonadSE.thy
@@ -69,7 +69,7 @@ syntax (xsymbols)
("(2 _ \<leftarrow> _; _)" [5,8,8]8)
translations
"x \<leftarrow> f; g" == "CONST bind_SE f (% x . g)"
-
+
definition unit_SE :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>E" ("(result _)" 8)
where "unit_SE e = (\<lambda>\<sigma>. Some(e,\<sigma>))"
notation unit_SE ("unit\<^sub>S\<^sub>E")
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..2280718b400d3b357f2c2d59bc2cfc75d7a07d2a
--- /dev/null
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy
@@ -0,0 +1,140 @@
+(*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
+ @{verbatim [indent=10, margin=70]
+ \<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 \<^verbatim>\<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 \<^verbatim>\<open>Data_Clean_Annotations\<close> as functions with the
+signature \<^verbatim>\<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 \<^verbatim>\<open>map_context_annotation_declaration\<close> function.
+The environment is then passed by writing it to the \<^verbatim>\<open>Data_Surrounding_Env\<close> GenericData-store.
+
+To prevent Isabelle from coercing types of returned terms \<^verbatim>\<open>Syntax.parse_term\<close> is used instead of \<^verbatim>\<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 ( \<^verbatim>\<open>remove_params_from_proof\<close>).
+
+\<^bold>\<open>Environment\<close>:
+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 \<^verbatim>\<open>functionArgs\<close> which is an optional list of function parameters.
+When an identifier has \<^verbatim>\<open>functionArgs = NONE\<close>, then it is a variable. \<^verbatim>\<open>functionArgs=SOME []\<close> corresponds to a parameterless function.
+
+\<^bold>\<open>Nice to know:\<close>
+- The environment of the last completely parsed C-context can be retrieved using \<^verbatim>\<open>C_Module.Data_In_Env\<close>.
+- Intermediate envs, containing parameters and local vars can be retrieved using \<^verbatim>\<open>C_Env.Data_Lang.get'\<close>.
+See C5.thy in the examples of C11-Frontend.
+\<close>
+
+section\<open>Limitations\<close>
+text\<open>
+\<^item> Only two types are currently mapped to isabelle types,
+ namely \<^verbatim>\<open>int -> int\<close> and \<^verbatim>\<open>unsigned -> int\<close>.
+
+\<^item> Function calls can only occur as statements or on the right hand side of an assignment.
+ For example \<^verbatim>\<open>a = b + foo();\<close> is not allowed. This must be rewritten as \<open>tmp = foo(); a=b+tmp;\<close>
+
+ Clean and is about to be fixed. The current translation should work for this case then.
+
+\<^item> 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:
+ @{verbatim [indent=10, margin=70]
+ \<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
+
+\<^item> 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 \<open>n\<close>\<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
+
+end
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
index db49ae7f09fdc431e0d362da60e00c5150b9de14..e9efd0875f685b018724748e2076abad4a6afa95 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
@@ -1,10 +1,12 @@
+section \<open>Accessing the \<open>C-Environment\<close> and Conversions to the \<open>Clean Environment\<close>\<close>
+
theory "Coder_Test_Env_AEnv"
imports "../src/CleanCoder"
begin
-section \<open>Accessors to C-Env\<close>
+subsection \<open>Accessors to \<open>C_Env\<close>\<close>
ML\<open>
fun map_option f (SOME X) = SOME(f X)
@@ -12,7 +14,7 @@ fun map_option f (SOME X) = SOME(f X)
fun lookup_Cid_info (C_env:C_Module.Data_In_Env.T) id = Symtab.lookup(#idents(#var_table C_env)) id
-fun is_global_Cid Cenv Cid = map_option (#global o #3) (lookup_Cid_info Cenv Cid);
+fun is_global_Cid Cenv Cid = map_option (#scope o #3) (lookup_Cid_info Cenv Cid);
fun is_fun_Cid Cenv Cid = map_option ((fn [C_Ast.CFunDeclr0 _] => true | _ => false)
o (#params o #3))
(lookup_Cid_info Cenv Cid);
@@ -27,8 +29,9 @@ C11_Ast_Lib.toString_nodeinfo;
C_Ast.SS_base
\<close>
-section \<open>Global Variables, Local Variables, and Local Parameters\<close>
-subsection\<open>An Environment Spy\<close>
+subsection \<open>Global Variables, Local Variables, and Local Parameters\<close>
+
+subsubsection\<open>An Environment Spy\<close>
ML\<open>
val ENV = Unsynchronized.ref (@{C\<^sub>e\<^sub>n\<^sub>v})
@@ -38,7 +41,6 @@ fun print_env' s _ stack _ env thy =
in thy end
\<close>
-ML\<open>open Position\<close>
setup \<open>ML_Antiquotation.inline @{binding print_env'}
(Scan.peek (fn _ => Scan.option Parse.embedded)
>> (fn name => ("print_env' "
@@ -46,7 +48,7 @@ setup \<open>ML_Antiquotation.inline @{binding print_env'}
| SOME s => "(SOME \"" ^ s ^ "\")")
^ " " ^ ML_Pretty.make_string_fn)))\<close>
-subsection\<open>Accessing the C_Env in an Example\<close>
+subsection\<open>Accessing the \<open>C_Env\<close> in an Example\<close>
C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
int a(int b){int c;
@@ -64,8 +66,6 @@ val b_res = lookup_Cid_info (!ENV) "b";
val c_res = lookup_Cid_info (!ENV) "c"
\<close>
-
-(* Problematic : *)
C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
int a (int b){int b;
return b;
@@ -80,9 +80,7 @@ lookup_Cid_info (!ENV) "b"
-
-
-section \<open>Global Declarations via CEnv and via the Clean API\<close>
+subsection \<open>Global Declarations via \<open>C_Env\<close> and via the Clean API\<close>
text \<open>
First, we translate the expressions;
@@ -104,8 +102,9 @@ ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
-C\<open> int a[10+12][34][] = 1;
- short int f(int x [][], long double y)
+C\<open>int a[10+12][34][] = 1;
+ \<close>
+C\<open> short int f(int x [][], long /* double */ y)
{int y; x=x;
/*@@ \<approx>setup \<open>@{print_env'}\<close> */
/*@@ highlight */}
@@ -142,8 +141,6 @@ val [((Some (CDeclr0 (_,t,_,_,_)),_),_)] = B'
end
\<close>
-ML\<open>(#ret o #3 o the)(lookup_Cid_info env_expr "f" );\<close>
-
ML\<open>
C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ;C_Ast.CFunDeclr0;
val S = hd ((#params o #3 o the)(lookup_Cid_info env_expr "f" ));
@@ -152,7 +149,6 @@ val S' = C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ [S] sigma_i
(* and the whole thing a bit more abstract with "a" and "f" *)
ML\<open>
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "a" );
-(* map_option (conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "f" ); *)
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "x" );
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "y" );
\<close>
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
index 8a14a2732e203df2e510984031a696d8d36c03cd..d86d0c17f813de0982de47500df438a988d2ef3f 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
@@ -23,9 +23,9 @@ ML\<open>
open C11_Expr_2_Clean HOLogic;
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i mt_A_env @{theory})
+ (convertExpr false sigma_i mt_A_env @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} "" (K NONE) ast_expr
\<close>
@@ -48,9 +48,9 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i mt_A_env @{theory})
+ (convertExpr false sigma_i mt_A_env @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} "" (K NONE) ast_expr
\<close>
@@ -72,11 +72,10 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i mt_A_env @{theory})
+ (convertExpr false sigma_i mt_A_env @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} "" (K NONE) ast_expr
\<close>
-
\<comment> \<open>pretty print of the latter\<close>
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
@@ -96,9 +95,9 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i mt_A_env @{theory})
+ (convertExpr false sigma_i mt_A_env @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} "" (K NONE) ast_expr
\<close>
@@ -121,9 +120,9 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i mt_A_env @{theory})
+ (convertExpr false sigma_i mt_A_env @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i mt_A_env @{theory} "" (K NONE) ast_expr
\<close>
@@ -147,8 +146,14 @@ C\<open>int a; int b[5];\<close>
global_vars (test) (*intern label *)
a :: "int"
b :: "int list"
-
-
+ c :: "int list list"
+ n1 :: "nat"
+ n2 :: "nat"
+ var1 :: "int"
+ var2 :: "int"
+
+ find_theorems a
+
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "expression"]]
C\<open>1 * a\<close>
@@ -158,7 +163,12 @@ ML\<open>val ast_expr = @{C11_CExpr}
local open C_AbsEnv HOLogic in
(* we construct suitable environments by hand for testing: *)
val A_env0 = [ Identifier("a", @{here}, intT, Global),
- Identifier("b", @{here}, listT intT, Global)];
+ Identifier("b", @{here}, listT intT, Global),
+ Identifier("c", @{here}, listT (listT intT), Global),
+ Identifier("n1", @{here}, natT, Global),
+ Identifier("n2", @{here}, natT, Global),
+ Identifier("localArr", @{here}, listT intT, Local "to some function"),
+ Identifier("localArrArr", @{here}, listT (listT intT), Local "to some function")];
val A_env2 = [ Identifier("a", @{here}, intT, Parameter "of some function")];
val sigma_i = StateMgt.get_state_type_global @{theory}
@@ -168,14 +178,14 @@ end
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env0 @{theory})
+ (convertExpr false sigma_i A_env0 @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} "" (K NONE) ast_expr
val S'' = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env2 @{theory})
+ (convertExpr false sigma_i A_env2 @{theory} "" (K NONE))
ast_expr []);
-val S'' = conv_Cexpr_lifted_term sigma_i A_env2 @{theory} ast_expr
+val S'' = conv_Cexpr_lifted_term sigma_i A_env2 @{theory} "" (K NONE) ast_expr
\<close>
@@ -183,17 +193,21 @@ val S'' = conv_Cexpr_lifted_term sigma_i A_env2 @{theory} 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")
x :: "int"
y :: "int list"
+ localArr :: "int list"
+ localArrArr :: "int list list"
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
C\<open>int x; int y[3];\<close>
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "expression"]]
+term\<open>result_value\<close>
+find_theorems result_value
C\<open>1 * x\<close>
ML\<open>val ast_expr = @{C11_CExpr}
@@ -210,9 +224,9 @@ end
ML\<open>
val S' = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env1 @{theory})
+ (convertExpr false sigma_i A_env1 @{theory} "" (K NONE))
ast_expr []);
-val S' = conv_Cexpr_lifted_term sigma_i A_env1 @{theory} ast_expr
+val S' = conv_Cexpr_lifted_term sigma_i A_env1 @{theory} "" (K NONE) ast_expr
\<close>
@@ -225,15 +239,15 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env1 @{theory})
+ (convertExpr false sigma_i A_env1 @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i A_env1 @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i A_env1 @{theory} "" (K NONE) ast_expr
\<close>
\<comment> \<open>pretty print of the latter\<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>
(*7*****************************************************************************************************)
@@ -246,9 +260,9 @@ ML\<open>val ast_expr = @{C11_CExpr}
ML\<open>
val S = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env0 @{theory})
+ (convertExpr true sigma_i A_env0 @{theory} "" (K NONE))
ast_expr []);
-val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} ast_expr
+val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} "" (K NONE) ast_expr
\<close>
@@ -256,7 +270,7 @@ val S = conv_Cexpr_lifted_term sigma_i A_env0 @{theory} 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>
@@ -282,7 +296,7 @@ ML\<open>val C_Ast.CCompound0(a, b, c) = ast_stmt;\<close> \<comment> \<open>gra
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt true sigma_i A_env0 @{theory})
+ (convertStmt true sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -292,8 +306,115 @@ 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} (Syntax.check_term @{context} S)\<close>
+
+
+text\<open>Write to array\<close>
+
+text\<open>Global\<close>
+C\<open>c[1][a] = a;\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+\<close>
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
+ML\<open> Sign.certify_term @{theory} S \<close>
+
+text\<open>local\<close>
+C\<open>localArrArr[1][a] = a;\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+\<close>
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
ML\<open> Sign.certify_term @{theory} S \<close>
+
+text\<open>Read global array\<close>
+C\<open>a = c[1][a];\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+\<close>
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
+ML\<open> Sign.certify_term @{theory} S \<close>
+
+text\<open>Read local array\<close>
+C\<open>a = localArrArr[1][a];\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+\<close>
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
+ML\<open> Sign.certify_term @{theory} S \<close>
+
+
+text\<open>mode complex array stuff\<close>
+C\<open>localArr[a] = localArrArr[1][b[c[1][2]]];\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+\<close>
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
+ML\<open> Sign.certify_term @{theory} S \<close>
+
+
+
(*2*****************************************************************************************************)
(*if the body is empty, then we put a skip :*)
@@ -308,7 +429,7 @@ ML\<open>val ast_stmt = @{C11_CStat}
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt false sigma_i A_env0 @{theory})
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -317,7 +438,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*****************************************************************************************************)
@@ -332,7 +453,7 @@ for(a = 0; a < 2; a = a + 1){
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt true sigma_i A_env0 @{theory})
+ (convertStmt true sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -341,7 +462,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*****************************************************************************************************)
@@ -359,7 +480,7 @@ ML\<open>val ast_stmt = @{C11_CStat}
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt false sigma_i A_env0 @{theory})
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -368,7 +489,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*****************************************************************************************************)
@@ -390,7 +511,7 @@ ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt false sigma_i A_env0 @{theory})
+ (convertStmt false sigma_i A_env0 @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -406,7 +527,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. *)
@@ -418,7 +539,7 @@ text \<open>The next step is to study the declarations. There are globals or loc
and functions or variables declarations.\<close>
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "external_declaration"]]
-C\<open> int b = a + a;\<close>
+C\<open> int b,a;\<close>
ML\<open>val ast_ext_decl = @{C11_CExtDecl}
val env_ext_decl = @{C\<^sub>e\<^sub>n\<^sub>v}
@@ -427,10 +548,9 @@ ML\<open>val ast_ext_decl = @{C11_CExtDecl}
(* initializers not yet supported; so this gives a local error *)
ML \<open>
val S = (C11_Ast_Lib.fold_cExternalDeclaration regroup
- (convertExpr false sigma_i A_env1 @{theory}) (* DOES THIS MAKE SENSE ??? *)
+ (convertExpr false sigma_i A_env1 @{theory} "" (K (NONE, NONE))) (* DOES THIS MAKE SENSE ??? *)
ast_ext_decl
[])
- handle ERROR _ => (writeln "CATCH ERROR"; []);
\<close>
(*4*****************************************************************************************************)
@@ -444,7 +564,7 @@ ML\<open>val ast_unit = @{C11_CTranslUnit}
val env_unit = @{C\<^sub>e\<^sub>n\<^sub>v}
\<close>
-C\<open>int zzz ;\<close>
+C\<open>int zzz = 13 ;\<close>
ML\<open>val ast_unit' = @{C11_CTranslUnit}
val env_unit' = @{C\<^sub>e\<^sub>n\<^sub>v}
@@ -477,16 +597,116 @@ 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>
-void foo(int xy) { }
+int var1;
+int var2;
+int a;
+int b[];
+void foo(int xy) {
+ int z = xy+2;
+ return z+1;
+}
+
+void three_args_function(int x, int y, int z){
+ x = foo(x);
+}
+
+int fun_with_ret_value(int x){
+ return x;
+}
+\<close>
+
+ML\<open>
+val cenv = @{C\<^sub>e\<^sub>n\<^sub>v}
\<close>
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+(* val translUnit = @{C11_CTranslUnit} *)
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
-val ast_stmt = extractStatement nEnv "foo";
+val ast_stmt = extractStatement nEnv "foo"
end\<close>
+C\<open>
+void test1(int abc, int def) {
+ return abc;
+}
+
+void test2(){
+ return 12;
+}
+\<close>
+
+ML\<open>
+Theory.setup
+ (C_Inner_Syntax.command_no_range
+ (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup
+ \<open>fn ((v1, (v2, pos1, pos2)) :: _) =>
+ (fn v3 => fn v4 =>
+ tap (fn v5 =>
+ Position.reports_text [((Position.range (pos1, pos2)
+ |> Position.range_position, Markup.intensify), "")]))
+ | _ => fn _ => fn _ => I\<close>)
+ ("store_env", \<^here>, \<^here>))
+\<close>
+
+ML \<open>
+
+
+Theory.setup
+ (C_Inner_Syntax.command_no_range
+ (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup
+ \<open>fn ((v1, (v2, pos1, pos2)) :: _) =>
+ (fn v3 => fn v4 =>
+ tap (fn v5 =>
+ (SPY_ENV := SOME (C_Module.env v5);Position.reports_text [((Position.range (pos1, pos2)
+ |> Position.range_position, Markup.intensify), "")])))
+ | _ => fn _ => fn _ => I\<close>)
+ ("store_env1", \<^here>, \<^here>))
+\<close>
+
+ML\<open>
+
+
+\<close>
+
+
+C\<open>
+void test5(){
+}\<close>
+
+ML\<open>
+val SPY_ENV = Unsynchronized.ref(NONE:C_Env.env_lang option);\<close>
+C\<open>
+
+
+void test3(char ab[][], int* *c, int *d){
+ int aasdfwqer;
+
+ return 12; /*@ \<approx>setup \<open>fn a => fn b => fn env =>
+ (writeln(@{make_string} env);(SPY_ENV := SOME env);I) \<close> */;
+
+}
+\<close>
+
+ML\<open>
+val a = let fun last (a::b::R) = last (b::R)
+ | last [a] = a
+
+in last (#scopes (the (!SPY_ENV))) end
+\<close>
+
+ML\<open>
+
+val tmp1 = (map (fn (a,(_,_,b)) => (a,#scope b,#functionArgs b)) (Symtab.dest (
+ #idents(#var_table(the (!SPY_ENV))))
+))
+\<close>
+
+ML\<open>
+val cenv = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
term\<open>skip\<^sub>S\<^sub>E\<close>
ML\<open>StateMgt.MON_SE_T HOLogic.unitT sigma_i\<close>
consts foo :: "int \<Rightarrow> (unit,'a local_test_return_state_scheme)MON\<^sub>S\<^sub>E "
@@ -501,18 +721,83 @@ ML\<open>
local open C_AbsEnv in
val foo_stmt = @{C11_CStat};
end
-
\<close>
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt true sigma_i nEnv @{theory})
+ (convertStmt false sigma_i nEnv @{theory} "" (K (NONE, NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
foo_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
\<close>
+ML\<open>writeln (Syntax.string_of_term_global @{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*)
+consts three_args_function :: "(int * int * int) \<Rightarrow> (unit,'a local_test_return_state_scheme)MON\<^sub>S\<^sub>E "
+C\<open>three_args_function(3+3,4,8);\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i nEnv @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+
+
+\<close>
+term assign_to_a
+
+ML\<open>writeln (Syntax.string_of_term_global @{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 "
+
+C\<open>localArr[0]=fun_with_ret_value(3+3);\<close>
+ML\<open>
+val ast_stmt = @{C11_CStat}
+val env_stmt = @{C\<^sub>e\<^sub>n\<^sub>v}
+\<close>
+
+ML\<open>
+(* build the new env with local vars for test purposes *)
+local open C_AbsEnv HOLogic in
+val localVarEnv = [
+ Identifier("x", @{here}, intT, Local "to some function"),
+ Identifier("localArr", @{here}, listT intT, Local "to some function"),
+ Identifier("localArrArr", @{here}, listT (listT intT), Local "to some function")
+]
+end
+val nEnv1 = nEnv@localVarEnv
+\<close>
+
+ML\<open>
+val [S] = (C11_Ast_Lib.fold_cStatement
+ regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
+ (convertStmt false sigma_i nEnv1 @{theory} "" (K (NONE, NONE)))
+ \<comment> \<open>combinator handlicng an individual statement\<close>
+ ast_stmt \<comment> \<open>C11 ast\<close>
+ [] \<comment> \<open>mt stack\<close>);
+
+
+\<close>
+term assign_to_a
+
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
+ML\<open>Sign.certify_term @{theory} (Syntax.check_term @{context} S)\<close>
+
section \<open>Experiments with Local Scopes\<close>
ML\<open> local open C_Ast
@@ -551,7 +836,8 @@ end
ML \<open>(Symtab.dest)(StateMgt_core.get_state_field_tab_global @{theory})\<close>
setup \<open>conv_transl_unit ast_unit\<close>
ML \<open>(Symtab.dest)(StateMgt_core.get_state_field_tab_global @{theory})\<close>
+(* A Cadaver ...
setup \<open>conv_transl_unit ast_unit'\<close>
ML \<open>(Symtab.dest)(StateMgt_core.get_state_field_tab_global @{theory});\<close>
-
+ *)
end
\ No newline at end of file
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_StmtTUnits.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_StmtTUnits.thy
index 147d53dd86b16698ffce7cff8a6bf13b30820485..015b7abc4dc9b48464976564e1352512a308692a 100644
--- a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_StmtTUnits.thy
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_StmtTUnits.thy
@@ -14,7 +14,7 @@ C\<open>int global1;\<close>
ML\<open>
local open C_AbsEnv in
-val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
@@ -24,7 +24,7 @@ C\<open>int global2[];
ML\<open>
local open C_AbsEnv in
-val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
@@ -34,7 +34,7 @@ unsigned int global6, global7;\<close>
ML\<open>
local open C_AbsEnv in
-val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
@@ -46,7 +46,7 @@ int c = foo(a), d;
ML\<open>
local open C_AbsEnv in
-val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end\<close>
@@ -60,7 +60,7 @@ void test() {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
@@ -69,7 +69,10 @@ end\<close>
function definition of `identity` *)
local_vars_test (identity "int")
z :: "int"
-ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
+ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}
+
+val Type(ty_name, _) = sigma_i
+\<close>
C\<open>int identity(int a) {
return a;
@@ -77,7 +80,7 @@ C\<open>int identity(int a) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "identity"
end
@@ -95,10 +98,12 @@ val lookup=Symtab.lookup state_field p *)
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory} )
+ (convertStmt false sigma_i nEnv @{theory} "" (K (NONE, NONE)))
ast_stmt []);
\<close>
+ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
+
ML\<open>
(* We create an abstraction over the term: iterate backwards using the param list *)
fun mk_final_term identifiers id t =
@@ -133,7 +138,7 @@ float add(int a, int b) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val add_ast = @{C11_CTranslUnit}
val ast_stmt = extractStatement nEnv "add"
@@ -145,12 +150,12 @@ ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory} )
+ (convertStmt false sigma_i nEnv @{theory} "" (K (NONE,NONE)) )
ast_stmt []);
\<close>
ML\<open>
-val final_term = mk_final_term identifiers "add" S
+val final_term = mk_final_term nEnv "add" S
\<close>
ML\<open>
@@ -175,7 +180,7 @@ int increment(int a) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "increment";
end
@@ -185,7 +190,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory})
+ (convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => [S];
\<close>
@@ -207,7 +212,7 @@ void foo() {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "foo";
end
@@ -217,7 +222,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt true sigma_i nEnv @{theory} )
+ (convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
@@ -226,7 +231,7 @@ val final_term = mk_final_term identifiers "foo" S
\<close>
ML\<open>
-Sign.certify_term @{theory} final_term
+Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
@@ -251,14 +256,16 @@ local_vars_test (paws "unit")
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
ML\<open>val init_ident = [C_AbsEnv.Identifier("swap", Position.none, @{typ "unit"}, C_AbsEnv.FunctionCategory(C_AbsEnv.Final, NONE))]\<close>
+
+(* TODO: should also be defined analogously to unsigned int, unsigned long, ... *)
C\<open>
-void paws(unsigned int a, unsigned int b) {
+void paws(unsigned a, unsigned b) {
swap(a, b);
}\<close>
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_ident Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_ident [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "paws";
end
@@ -267,7 +274,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt true sigma_i nEnv @{theory})
+ (convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
@@ -326,23 +333,28 @@ ML\<open>val init_idents = parse_state_field_tab @{theory}\<close>
C\<open>
int bar(int a, int b) {
+ int d;
c = 0;
return 0;
+
}
\<close>
+
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_idents Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_idents [Identifier("c",@{here},HOLogic.intT, Global)] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "bar";
+
+val env = @{C\<^sub>e\<^sub>n\<^sub>v}
end
\<close>
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt true sigma_i nEnv @{theory})
+ (convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
@@ -351,7 +363,7 @@ val final_term = mk_final_term identifiers "bar" S
\<close>
ML\<open>
-Sign.certify_term @{theory} final_term
+Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
@@ -373,7 +385,7 @@ int factorial(int n) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "factorial";
end
@@ -384,7 +396,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory} )
+ (convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => (writeln "correct crash: recursion not supported";
[@{term "undefined"}])
@@ -416,7 +428,7 @@ writeln (Syntax.string_of_term_global @{theory} final_term);
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
@@ -427,14 +439,14 @@ local_vars_test (is_even "int")
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
C\<open>
-int is_even(unsigned int n) {
+int is_even(unsigned n) {
if (n == 0)
return 0;
else
return is_odd(n - 1);
}
-int is_odd(unsigned int n) {
+int is_odd(unsigned n) {
if (n == 0)
return -1;
else
@@ -444,7 +456,7 @@ int is_odd(unsigned int n) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "is_even";
end
@@ -454,7 +466,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory})
+ (convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => (writeln "correct crash: recursion not supported";
[@{term "undefined"}]);
@@ -486,7 +498,7 @@ int sqrt(int a) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit}
- init_idents Symtab.empty
+ init_idents [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "sqrt";
end
@@ -495,7 +507,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory})
+ (convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
@@ -504,7 +516,7 @@ val final_term = mk_final_term identifiers "sqrt" S
\<close>
ML\<open>
-Sign.certify_term @{theory} final_term
+Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
@@ -533,16 +545,17 @@ int allzeros(int t[], int n) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit}
- nEnv_0 Symtab.empty
+ nEnv_0 [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "allzeros";
end
\<close>
+(* PROBLEM *)
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
- (convertStmt false sigma_i nEnv @{theory})
+ (convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
@@ -566,7 +579,7 @@ int binarysearch(int t[], int n, int v) {
ML\<open>
local open C_AbsEnv in
-val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end\<close>
@@ -589,7 +602,7 @@ int linearsearch(int x, int t[], int n) {
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
@@ -635,7 +648,7 @@ printf("Sorted list in ascending order:\n");
ML\<open>
local open C_AbsEnv in
-val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
+val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
@@ -690,7 +703,9 @@ fun convertEnv (name,(pos_list,serial,{ global = true , params = [] , ret = Pars
end
\<close>
-ML\<open>val (name,(pos_list,serial,{ global = true , params = P as (C_Ast.CFunDeclr0 G::R) , ret = Z })) = nth menv 5;
+ML\<open>nth menv 5\<close>
+ML\<open>val (name,(pos_list,serial,{ scope = C_Env.Global , functionArgs=_,
+ params = P as (C_Ast.CFunDeclr0 G::R) , ret = Z })) = nth menv 5;
val curried_w_dummyreturn = C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ P dummyT
val (tyS,ty) = strip_type curried_w_dummyreturn
val uncurried_w_dummyreturn = HOLogic.mk_tupleT tyS --> ty
@@ -698,18 +713,13 @@ ML\<open>val (name,(pos_list,serial,{ global = true , params = P as (C_Ast.CFunD
ML\<open>nth menv 5;
\<close>
-(* So ne scheisse. Der return-type ist zwar im AST sichtbar, aber nicht im globalen (Isabelle_C)
- Environment. Da findet sich lediglich : previous in stack. Das verkompliziert die Sache.
-
- Immerhin:
-*)
-
-ML\<open>map_filter convertEnv menv\<close>
+(* dies ist ein Versuch, ein return in einem globalen Kontext auszufuehren.
+ Dieser Test macht keinen Sinn.
ML\<open>
val [body] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
- (convertStmt false (StateMgt_core.get_state_type @{context}) nEnv_0 @{theory})
+ (convertStmt false (StateMgt_core.get_state_type @{context}) nEnv_0 @{theory} "" (K(NONE,NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
@@ -730,4 +740,5 @@ val local_thy = Function_Specification_Parser.define_body_core add_bind ret_typ
param_list body;
Function_Specification_Parser.define_body_core add_bind args_ty sty param_list body ctxt
(*Function_Specification_Parser.define_body_main { recursive = false } add_bind ret_typ sty param_list NONE 0 ctxt*)
-\<close>
\ No newline at end of file
+\<close>
+*)
\ No newline at end of file
diff --git a/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy
new file mode 100644
index 0000000000000000000000000000000000000000..36ff8a10e8e6cb8144c72b7abccb7a516bc53592
--- /dev/null
+++ b/C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy
@@ -0,0 +1,435 @@
+theory "Coder_Test_TUnits"
+ imports
+ "../src/compiler/Clean_Annotation"
+ "../src/CleanTranslationHook"
+begin
+
+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 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>
+
+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::int) \<ge> 1\<close> */
+ return a;
+}\<close>
+
+
+term\<open>nat\<close>
+C\<open>
+int u;
+int arrr[];
+\<close>
+C\<open>
+int globvar;
+unsigned nat1;
+int u;
+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> */
+
+ 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> */
+ /*@ 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;
+ }
+
+ return 1;
+}\<close>
+find_theorems fun_with_pre_test_core
+
+
+section\<open>Demonstration\<close>
+
+subsection\<open>Global definitions\<close>
+C\<open>
+int global_integer;
+unsigned global_nat;
+\<close>
+(*variables are declared accordingly*)
+find_theorems global_integer
+find_theorems global_nat
+term\<open>global_integer\<close>
+term\<open>global_nat\<close>
+
+
+
+
+subsection\<open>Function definitions\<close>
+C\<open>int threefunc(){
+ return 1+2;
+}
+
+int sum5(int p1, int p2){
+ return p1+p2;
+}
+
+void addToGlobalInteger(int value){
+ global_integer = global_integer+value;
+}
+\<close>
+
+find_theorems threefunc_core
+term\<open>threefunc\<close>
+find_theorems sum_core
+term\<open>sum\<close>
+
+
+
+
+subsection\<open>And function calls\<close>
+C\<open>
+void addPlusThree(int val){
+ int three; /*Init expression currently unsupported*/
+ three = threefunc();
+ addToGlobalInteger(three+val);
+}
+\<close>
+
+
+text\<open>we compare this to an equivalent definition\<close>
+function_spec addPlusThree1(val :: int) returns unit
+pre "\<open>True\<close>"
+post "\<open>\<lambda>res::unit. True \<close>"
+local_vars three :: int
+defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C threefunc \<open>()\<close> ; assign_local three_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
+ call\<^sub>C addToGlobalInteger \<open>(three + val)\<close>"
+
+find_theorems addPlusThree_core
+find_theorems addPlusThree1_core
+term\<open>addPlusThree\<close>
+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>"
+local_vars localvar1 :: int
+defines "if\<^sub>C \<open>n > 0\<close>
+ then (\<open> global_integer := global_integer + 1\<close>);-
+ call\<^sub>C recursive_add1 \<open>(n-1)\<close>
+ else skip\<^sub>S\<^sub>E
+ fi"
+
+C\<open>
+void recursive_add(int n){
+ if(n > 0){
+ global_integer = global_integer + 1;
+ recursive_add(n-1);
+ }
+}\<close>
+
+find_theorems recursive_add_core
+find_theorems recursive_add1_core
+term recursive_add
+term recursive_add1
+
+
+
+
+subsection\<open>(multidimensional) arrays are also supported\<close>
+C\<open>
+int globalArray[][];
+int something(){
+ int localvar;
+ localvar = globalArray[0][3];
+}
+\<close>
+
+
+
+
+subsection\<open>A fully annotated program\<close>
+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::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;
+ int counter_b;
+ counter = 0;
+ s = 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>s\<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> */
+ counter_b = 0;
+ while(counter_b < b){
+ /*@ 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> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>b\<close>\<close> */
+ counter_b = counter_b +1;
+ }
+
+ s = s + counter_b;
+ counter = counter + 1;
+ }
+ return s;
+}
+\<close>
+find_theorems multiply_pre
+
+
+
+
+
+
+section\<open>Some other tests\<close>
+
+C\<open>
+int intarr[][][];
+int x;
+\<close>
+term x
+find_theorems x
+C\<open>
+int sum1(int param1,int param2){
+ x = threefunc();
+ intarr[2][3][1] = x + param1 + param2;
+ return 1;
+}
+
+int sum3(int param1,int param2){
+ int x; // test to override
+ x = sum1(param1, param2);
+ return x;
+}\<close>
+find_theorems x
+find_theorems sum1_core
+C\<open>
+int test_scope(){
+ x = 1;
+ return x;
+}
+\<close>
+
+find_theorems sum3_core
+term\<open>intarr\<close>
+
+
+C\<open>
+int a;
+int testfunction(int v1, int v2){
+ global_integer = sum1(v1,v2);
+ return global_integer;
+}
+\<close>
+
+C\<open>
+int b;
+\<close>
+
+text\<open>Now the declaration of local variables\<close>
+C\<open>
+int funwithlocalvars(){
+ int localvar1;
+ localvar1 = threefunc();
+ return localvar1;
+}
+\<close>
+term localvar1
+find_theorems funwithlocalvars_core
+term funwithlocalvars_core
+
+ML\<open>
+val ast = @{C11_CTranslUnit}
+\<close>
+ML\<open>
+val env = @{C\<^sub>e\<^sub>n\<^sub>v}\<close>
+
+function_spec testfunction1(param1 :: int, param2::int) returns int
+pre "\<open>True\<close>"
+post "\<open>\<lambda>res::int. True \<close>"
+local_vars localvar1 :: int
+defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C sum1 \<open>(2::int, 3::int)\<close> ; assign_global global_integer_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
+ return\<^bsub>local_testfunction1_state.result_value_update\<^esub> \<open>global_integer\<close>"
+
+find_theorems testfunction1_core
+term\<open>testfunction1_core\<close>
+
+
+
+(*
+Recursions with return values are currently unsupported in CLEAN, but are about to be fixed by someone else
+
+rec_function_spec recursive_function2(n::int) returns int
+pre "\<open>True\<close>"
+post "\<open>\<lambda>res::int. True \<close>"
+local_vars localvar1 :: int
+defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C recursive_function2 \<open>2::int\<close> ; assign_local localvar1_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
+return\<^bsub>local_recursive_function2_state.result_value_update\<^esub> \<open>1::int\<close>"
+*)
+
+
+text\<open>Now the pre and post conditions\<close>
+
+
+
+C\<open>
+int xx;
+int fun_with_pre(int u){
+ int local1;
+ /*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>xx\<close> > 0\<close> */
+ /*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int.3 > \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close>\<close> */
+ return local1;
+}
+int fun_with_pre2(int 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> > 0\<close> */
+
+ return 1;
+}
+\<close>
+
+ML\<open>
+
+val annotation_data = Clean_Annotation.Data_Clean_Annotations.get (Context.Theory @{theory})
+\<close>
+
+
+text\<open>Invariants are more tricky, as there can be several within one function\<close>
+
+text\<open>Lets start with a simple example with two loops,
+ which computes a*b, given a and b are positive!
+
+ The following program is fully annotated with pre-, and postcondition, aswell as 2 invariants\<close>
+C\<open>int a;\<close>
+C\<open>
+int multiply2(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> > 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;
+ int counter_b;
+
+ while(counter < a){
+ /* here we have a loop without an invariant */
+ counter = counter + 1;
+ }
+ counter = 0;
+ sum = 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\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close>\<close> */
+ counter = counter + 1;
+ }
+
+ while(counter > 0){
+ /* inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>(a-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> \<ge> 0\<close> */
+ counter_b = 0;
+ while(counter_b < b){
+ /* inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>C\<open>counter_b\<close> \<le> b\<close>*/
+ counter_b = counter_b +1;
+ }
+
+ sum = sum + counter_b;
+ counter = counter -1;
+
+ }
+ return sum;
+}
+\<close>
+
+C\<open>
+int globarr[];\<close>
+C\<open>
+void somefunction123(){
+int localArray[];
+
+}\<close>
+
+find_theorems multiply_core
+
+ML\<open>
+val annotation_data = Clean_Annotation.Data_Clean_Annotations.get (Context.Theory @{theory})
+\<close>
+
diff --git a/C11-BackEnds/Clean_wrapper/src/.CleanCoder.thy.marks b/C11-BackEnds/Clean_wrapper/src/.CleanCoder.thy.marks
new file mode 100644
index 0000000000000000000000000000000000000000..1f89f043a1af642d6019bcd0e7f2b7778ba91719
--- /dev/null
+++ b/C11-BackEnds/Clean_wrapper/src/.CleanCoder.thy.marks
@@ -0,0 +1 @@
+!c;26152;26152
diff --git a/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy b/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
index 6cbe4abcec38c4467ad1ee8ddd7023f3b5f128b2..2f6dc44119175cda3e2a63fdb763edcae99ddee1 100644
--- a/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
+++ b/C11-BackEnds/Clean_wrapper/src/CleanCoder.thy
@@ -67,28 +67,20 @@ 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
+
+fun lastype_of (Type(_, [x])) = x | lastype_of (Type(_, [_ , y])) = y
(* Creates a result_update_term for the local state *)
-fun mk_result_update thy =
- let val sigma_i = StateMgt.get_state_type_global thy;
+fun mk_result_update thy sigma_i=
+ let
val Type(ty_name,_) = sigma_i
val s = ty_name |> String.tokens (fn x => x = #".") |> tl |> hd
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 thy name ty =
(* a very dirty hack ... but reconstructs the true \<open>const_name\<close>
@@ -96,6 +88,21 @@ fun read_N_coerce thy name ty =
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, _) =
+ (case Long_Name.explode n of
+ [_, middle, base] => base = name andalso (String.substring (middle,0,6) = "global")
+ | _ => false)
+ val longnames = List.filter filter_by_shortname (#constants (Consts.dest consts))
+ val longname = (fst o hd) longnames
+ in read_N_coerce thy longname end
+
+fun get_update_fun thy name = read_N_coerce thy (name^"_update")
\<close>
subsection\<open>C11 Expressions to Clean Terms\<close>
@@ -125,11 +132,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
+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.
@@ -141,31 +159,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 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(C_AbsEnv.Final, _) =>
- let val Const(id, ty) = Syntax.read_term_global thy id
- val args = firstype_of ty
- val mty = StateMgt_core.MON_SE_T @{typ "unit"} sigma_i
- in Const(id, args --> mty) :: c end
-
- | c => error("(convertExpr) unrecognised category : " ^ @{make_string} c)
+ | 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
end)
|"Vars0" => c
|"CVar0" => c
@@ -174,10 +187,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.
@@ -193,18 +206,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
@@ -215,7 +232,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
@@ -240,7 +257,8 @@ translate integers in booleans. That's what term_to_bool t do.
::c
end
|"CIndex0" => (case c of
- (idx::root::R) => let fun destListT (Type(@{type_name list},[t])) = t
+ (idx::root::R) => let fun destListT arg =
+ case arg of (Type(@{type_name list},[t])) => t
val idx_term = case fastype_of idx of
Type(@{type_name "nat"},[]) => idx
| Type(@{type_name "int"},[]) =>
@@ -258,28 +276,41 @@ 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" => c (* skip this wrapper *)
- |"CDecl0" => error("Local declarations inside a C context are not supported in Clean")
+ (*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
+ remove_dead_idents c
+ end
|"CCall0" => c (* skip this wrapper *)
- | str => error("unsupported expression with parse tag: "^str)) (* global catch all *)
+ |"CNoArrSize0" => c
+ |"CArrDeclr0" => c
+ | 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))
-fun conv_Cexpr_lifted_term sigma_i A_env thy C_expr =
+fun conv_Cexpr_lifted_term sigma_i A_env thy function_name get_loop_annotations C_expr =
let val e::R = (C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false sigma_i A_env thy) C_expr [])
+ (convertExpr false sigma_i A_env thy function_name get_loop_annotations) C_expr [])
in lifted_term sigma_i e end
(*** -------------- ***)
-fun conv_cDerivedDeclarator_cSizeExpr_term (C_Ast.CArrDeclr0 (_,C_Ast.CArrSize0 (_,C_expr),_)) C_env thy =
+fun conv_cDerivedDeclarator_cSizeExpr_term (C_Ast.CArrDeclr0 (_,C_Ast.CArrSize0 (_,C_expr),_)) C_env thy function_name get_loop_annotations=
SOME(hd((C11_Ast_Lib.fold_cExpression (K I)
- (convertExpr false dummyT C_env thy) C_expr [])))
- |conv_cDerivedDeclarator_cSizeExpr_term (C_Ast.CArrDeclr0 (_,C_Ast.CNoArrSize0 Z,_)) _ _ = NONE
- |conv_cDerivedDeclarator_cSizeExpr_term (_) _ _ =
+ (convertExpr false dummyT C_env thy function_name get_loop_annotations) C_expr [])))
+ |conv_cDerivedDeclarator_cSizeExpr_term (C_Ast.CArrDeclr0 (_,C_Ast.CNoArrSize0 Z,_)) _ _ _ _= NONE
+ |conv_cDerivedDeclarator_cSizeExpr_term (_) _ _ _ _=
error("DeclarationSpec format not defined. [Clean restriction]")
@@ -320,53 +351,96 @@ si on a k = 0 : renvoie la term skip
fun block_to_term (Const("_END",_)::Const("_BEGIN",_)::R)
= mk_skip_C dummyT ::R
|block_to_term R =
- let val _ = (writeln("block_to_term::"^ @{make_string } R))
- val (topS, restS) = chop_prefix (fn Const("_BEGIN",_) => false | _ => true) R
+ let val (topS, restS) = chop_prefix (fn Const("_BEGIN",_) => false | _ => true) R
val (Const("_END",_)::topS, Const("_BEGIN",_)::restS) = (topS, restS)
in (foldl1 (uncurry mk_seq_C) (rev topS)) :: restS end
-fun convertStmt verbose sigma_i nEenv thy
+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 val long_id = (case lhs of
+ ((let
+ fun getLongId lhs = (case lhs of
Const(name, _) $ _ => name
| _ $ _ $ Const(name, _) $ _ => name
| Free (name, _) => name
+ | Const ("List.nth", _) $ lhs_candidat $ _ => (getLongId lhs_candidat)
| _ => error("(convertStmt) CAssign0 does not recognise term: "
- ^(@{make_string} 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) =
+ ^(@{make_string} lhs)^"With stacK"^(@{make_string} stack)))
+ 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)
- val (id, lid) = (id ^ "_update", lid ^ "_update")
-
- in case cat of
- C_AbsEnv.Global => (mk_assign_global_C
- (read_N_coerce thy id
- ((ty --> ty) --> sigma_i --> sigma_i))
- (lifted_term sigma_i rhs))::R
- | C_AbsEnv.Parameter(_) => error "assignment to parameter not allowed in Clean"
- | C_AbsEnv.Local(_) => (mk_assign_local_C
- (read_N_coerce thy lid
- ((listT ty --> listT ty) --> sigma_i --> sigma_i))
- (lifted_term sigma_i rhs) )::R
- | s => error("(convertStmt) CAssign0 with cat "
- ^ @{make_string} s ^ " is unrecognised")
- end)
+ | _ => 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", _) $ 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)
+ (*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" *)
+ 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 (listT ty) updated
+ end
+ )
+ | _ => 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*)
- |"CReturn0" => let val rhs = hd stack
- val res_upd = mk_result_update thy
+ |"CReturn0" => let
+ val rhs = hd stack
+ val res_upd = mk_result_update thy sigma_i
in (mk_return_C res_upd (lifted_term sigma_i rhs)) :: (tl stack) end
|"CSkip0" => (mk_skip_C sigma_i)::stack
|"CBreak0" => (mk_break sigma_i)::stack
@@ -381,52 +455,92 @@ 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)
| _ => raise WrongFormat("if")
)
- |"CWhile0" => (case stack of
- (a::b::R) => (mk_while_C (lifted_term sigma_i b) a) :: R
- |(a::R) => (mk_while_C (lifted_term sigma_i a)
+ |"CWhile0" => let val pos = (case b of C_Ast.OnlyPos0 (pos,_) => pos
+ |C_Ast.NodeInfo0 (pos,_,_) => pos)
+ val (get_inv, get_measure) = get_loop_annotations pos
+ val invariant_lifted =get_inv
+ |> Option.map
+ (fn get_inv=>(Syntax.check_term (Proof_Context.init_global thy) ((lifted_term sigma_i) (get_inv (Context.Theory thy)))))
+ val measure_lifted =get_measure
+ |> Option.map
+ (fn get_measure => Syntax.check_term (Proof_Context.init_global thy) ((lifted_term sigma_i) ( get_measure (Context.Theory thy))))
+ val mk_while_func = case (invariant_lifted,measure_lifted)
+ of (NONE,NONE) => mk_while_C
+ |(SOME inv, SOME measure)=>mk_while_anno_C inv measure (*Note the coercion to nat!*)
+ |(SOME inv, NONE)=>mk_while_anno_C inv (lifted_term sigma_i @{term "1::nat"})
+ |(NONE, SOME measure)=>mk_while_anno_C (lifted_term sigma_i @{term "True::bool"}) measure
+
+ in (case stack of
+ (a::b::R) => (mk_while_func (lifted_term sigma_i b) a) :: R
+ |(a::R) => (mk_while_func (lifted_term sigma_i a)
(mk_skip_C dummyT)) :: R (* really dummyT *)
|_ => raise WrongFormat("while")
- )
+ ) end
(*There is no For operator in Clean, so we have to translate it as a while :
for(ini, cond, evol){body} is translated as ini; while(cond){body; evol;}*)
- |"CFor0" => (case stack of
- (body::pace::cond::init::R) => (let val C' = mk_while_C
+ |"CFor0" => let val pos = (case b of C_Ast.OnlyPos0 (pos,_) => pos
+ |C_Ast.NodeInfo0 (pos,_,_) => pos)
+ (*duplicate code from while*)
+ val (get_inv, get_measure) = get_loop_annotations pos
+ val invariant_lifted =get_inv |> Option.map (fn get_inv=> (lifted_term sigma_i) (get_inv (Context.Theory thy)))
+ val measure_lifted =get_measure |> Option.map (fn get_measure => (lifted_term sigma_i) ( get_measure (Context.Theory thy)))
+ val mk_while_func = case (invariant_lifted,measure_lifted)
+ of (NONE,NONE) => mk_while_C
+ |(SOME inv, SOME measure)=>mk_while_anno_C inv measure
+ |(SOME inv, NONE)=>mk_while_anno_C inv (lifted_term sigma_i @{term "1::nat"})
+ |(NONE, SOME measure)=>mk_while_anno_C (lifted_term sigma_i @{term "True::bool"}) measure
+ in (case stack of
+ (body::pace::cond::init::R) => (let val C' = mk_while_func
(lifted_term sigma_i cond)
(mk_seq_C body pace)
in ((mk_seq_C init C'))::R end)
- |_ => raise WrongFormat("for"))
+ |_ => 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)
- | arg => extract_fun_args R (arg :: args)
- fun extract_type_list (arg :: args) =
- (case arg of
- (* should be expanded for the 3 term representations of variables... *)
- Free(_, ty) => ty :: extract_type_list args)
- | extract_type_list [] = []
- (* should be expanded for variable number of args... *)
- fun mk_cross_prod_args [a, b] = Const (@{const_name "Pair"},
- a --> b --> mk_prodT (a, b))
+ | 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))
+ |extract_fun_args [] _ = error ("\"CCall0\": couldnt find function in stack: "^(@{make_string} stack))
val (args, f, R) = extract_fun_args stack []
- val cross_prod_args = mk_cross_prod_args (extract_type_list args)
- val fun_args_term = list_comb (cross_prod_args, args)
- in mk_call_C f (lifted_term sigma_i fun_args_term) :: R end)
- | _ => convertExpr verbose sigma_i nEenv thy a b stack )
+ 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
+ in mk_call_C f_new (lifted_term sigma_i fun_args_term) :: R end)
+ | _ => convertExpr verbose sigma_i nEenv thy function_name get_loop_annotations a b stack )
end
(*** -------------- ***)
+end
end
\<close>
@@ -465,6 +579,16 @@ fun convertCUnit verbose sigma_i env thy
| s => (c)
)
+fun get_loop_positions (a as { tag, sub_tag, args }:C11_Ast_Lib.node_content)
+ (b: C_Ast.nodeInfo )
+ (c : C_Ast.positiona list) =
+ case tag of
+ "CWhile0" => (case b of C_Ast.OnlyPos0 (pos,_) => pos::c
+ |C_Ast.NodeInfo0 (pos,_,_) => pos::c)
+ |"CFor0" => (case b of C_Ast.OnlyPos0 (pos,_) => pos::c
+ |C_Ast.NodeInfo0 (pos,_,_) => pos::c)
+ | _ => c
+
end
end
diff --git a/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy b/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
index a37a071e82b1793f616c70e44507ab73facc6b22..0773f0e28df698a70a4c6b41bdcbaf2cd33f4ace 100644
--- a/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
+++ b/C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
@@ -139,7 +139,7 @@ fun conv_ParseStatus_CDeclSpecS (SOME(C_Env.Parsed S)) = SOME S
|conv_ParseStatus_CDeclSpecS _ = NONE
-fun conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CUnsigType0 _)])) = SOME(HOLogic.intT)
+fun conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CUnsigType0 _)])) = SOME(HOLogic.natT)
|conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CIntType0 _)])) = SOME(HOLogic.intT)
|conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CLongType0 _),
CTypeSpec0 (CIntType0 _)])) = SOME(HOLogic.intT)
@@ -244,6 +244,7 @@ signature C_ABS_ENVIRONMENT =
datatype identifier = Identifier of string * Position.T * typ * identType
val parseTranslUnitIdentifiers: C_Ast.nodeInfo C_Ast.cTranslationUnit
+ -> identifier list
-> identifier list
-> string list Symtab.table
-> identifier list * string list Symtab.table
@@ -335,6 +336,11 @@ fun getMutuallyRecursiveCalls (Identifier(name, pos, ty, idType) :: s) functionN
else getMutuallyRecursiveCalls s functionName
| getMutuallyRecursiveCalls [] _ = []
+fun isCall0
+ ((nc, _) :: R) =
+ if #tag nc = "CCall0" then true
+ else isCall0 R
+ | isCall0 [] = false
fun readCall0
((nc, _) :: R) =
if #tag nc = "CCall0" then R
@@ -349,6 +355,7 @@ fun parseNodeContent
(HOLType: Basic_Term.typ option)
((nc, ni) :: R)
identList
+ oldIdents
functionCallList
(idType: identType) =
let val Left(posL, posR) = C_Grammar_Rule_Lib.decode ni
@@ -356,47 +363,53 @@ fun parseNodeContent
case #tag nc of
"CTypeSpec0" (* this is the start variable declaration list (one or multiple) *)
=> let val HOLType = #sub_tag nc |> str2HOLogic
- in parseNodeContent (SOME HOLType) (cutDownTypeSpec (R)) identList functionCallList idType
+ in parseNodeContent (SOME HOLType) (cutDownTypeSpec (R)) identList oldIdents functionCallList idType
end
| "Ident0"
=> let val name = node_content_parser nc
+ fun transform_list_type ((r,_)::R) ty = if #tag r = "CArrDeclr0" then HOLogic.listT (transform_list_type R ty) else ty
+ | transform_list_type [] ty = ty
+ fun skip_arr_decls ((r,b)::R) = if #tag r = "CArrDeclr0" then skip_arr_decls R else ((r,b)::R)
+ | skip_arr_decls [] = []
in (debug("(parseNodeContent) parsing: " ^ name);
if (* if the identifier already exists, this is either a reference to a variable
(which we ignore) or a declared function call *)
- identifierExists identList name
- then if functionIdentifierExists identList name
- then parseNodeContent NONE R identList (name :: functionCallList) idType
- else parseNodeContent NONE R identList functionCallList idType
- else (* otherwise, it is a variable declaration or an undeclared function call *)
+ (identifierExists (identList@oldIdents) name)
+ then (if functionIdentifierExists (identList@oldIdents) name (*potential error when function is redefined as variable*)
+ then parseNodeContent NONE R identList oldIdents (name :: functionCallList) idType
+ else parseNodeContent NONE R identList oldIdents functionCallList idType)
+ else (* otherwise, it is a variable declaration or an undeclared function call or a reference to a variable defined elsewhere*)
let val (nc2, ni2) :: R = R
in case #tag nc2 of
"CDeclr0" (* this is the end of one variable declaration *)
=> (debug("(parseNodeContent) this is a DECLARATION: "^name);
parseNodeContent HOLType R (Identifier(node_content_parser nc, posL,
- (fn (SOME(a)) => a) HOLType, idType) :: identList) functionCallList idType)
- | "CArrDeclr0" (* this is an array variable declaration, thus we INFER that
+ (fn (SOME(a)) => a) HOLType, idType) :: identList) oldIdents functionCallList idType)
+ | "CArrDeclr0" (* this is an array variable declaration, thus we count how many ArrDecls are here
#tag (hd R) is "CDeclr0" so we skip it *)
- => parseNodeContent HOLType (tl R) (Identifier(node_content_parser nc, posL,
- HOLogic.listT ((fn (SOME(a)) => a) HOLType), idType) :: identList)
+ =>
+ parseNodeContent HOLType (skip_arr_decls R) (Identifier(node_content_parser nc, posL,
+ transform_list_type R (HOLogic.listT (the HOLType)), idType) :: identList) oldIdents
functionCallList idType
| "CTypeSpec0"
=> parseNodeContent HOLType (R) (Identifier(node_content_parser nc, posL,
- (fn (SOME(a)) => a) HOLType, idType) :: identList) functionCallList idType
- | s (* this is a function call, #tag nc2 is either another Ident0 which is a
+ (fn (SOME(a)) => a) HOLType, idType) :: identList) oldIdents functionCallList idType
+ | s =>(* this is a function call, #tag nc2 is either another Ident0 which is a
parameter which we ignore or CCall0 in which the function calls ends *)
- => (debug("function call detected (tag = " ^ s ^ ") : " ^ @{make_string} (R));
- parseNodeContent HOLType (readCall0 ((nc2, ni2) :: R)) identList
- (node_content_parser nc :: functionCallList) idType)
+ if (isCall0 ((nc2, ni2) :: R)) then (debug("function call detected (tag = " ^ s ^ ") : " ^ @{make_string} (R));
+ parseNodeContent HOLType (readCall0 ((nc2, ni2) :: R)) identList oldIdents
+ (node_content_parser nc :: functionCallList) idType) else
+ parseNodeContent HOLType R identList oldIdents functionCallList idType
end)
end
| "CDeclr0" (* artifact: list of params have a CDeclr0 at the end, so we ignore this *)
- => parseNodeContent HOLType R identList functionCallList idType
+ => parseNodeContent HOLType R identList oldIdents functionCallList idType
| "CCall0" (* artifact: list of params have a CDeclr0 at the end, so we ignore this *)
- => parseNodeContent HOLType R identList functionCallList idType
+ => parseNodeContent HOLType R identList oldIdents functionCallList idType
| _
=> error("node content parsing failure: " ^ @{make_string} ((nc, ni) :: R)))
end
- | parseNodeContent _ [] identList functionCallList _ =
+ | parseNodeContent _ [] identList oldIdents functionCallList _ =
(debug("(parseNodeContent) finished: identList--" ^ @{make_string} identList
^ " functionCallList--" ^ @{make_string} functionCallList);
(identList, functionCallList))
@@ -473,7 +486,7 @@ fun parseFunctionCalls
(functionCategory, identList, functionCallTable)
fun parseParams L (functionName: string) =
- let val (identList, _) = parseNodeContent NONE L [] [] (Parameter(functionName))
+ let val (identList, _) = parseNodeContent NONE L [] [] [] (Parameter(functionName))
in identList end
(* Parses identifiers in a function body.
@@ -488,9 +501,11 @@ fun parseLocals
(* Table of previous function names with list of function calls *)
(functionCallTable: string list Symtab.table)
(* Previous identifiers *)
- (identList: identifier list) =
+ (identList: identifier list)
+ (* Identifiers from a previous translation unit (synthesized from env)*)
+ (oldIdents: identifier list) =
(debug("parsing locals: " ^ @{make_string} L);
- let val (identList, functionCalls) = parseNodeContent NONE L identList [] (Local(functionName))
+ let val (identList, functionCalls) = parseNodeContent NONE L identList oldIdents [] (Local(functionName))
val (functionCategory, identList, functionCallTable) =
parseFunctionCalls functionName identList functionCallTable functionCalls Final
in (identList, functionCategory, functionCallTable) end)
@@ -501,6 +516,7 @@ fun parseLocals
fun parseExternalDeclaration
(CDeclExt0(declaration : nodeInfo cDeclaration))
identList
+ oldIdents
functionCallTable =
(* Select Ident0 constructors in a cDeclaration. Here we suppose that there is only 1 *)
let val CDecl0(declarationSpecifierList, _, _) = declaration
@@ -511,7 +527,7 @@ fun parseExternalDeclaration
val nodeContentList = rev (C11_Ast_Lib.fold_cDeclaration (K I)
(selectFromNodeContent ["Ident0", "CTypeSpec0", "CArrDeclr0", "CDeclr0", "CCall0"])
declaration [])
- val (newIdentList, _) = parseNodeContent NONE nodeContentList identList [] Global
+ val (newIdentList, _) = parseNodeContent NONE nodeContentList identList oldIdents [] Global
in (debug("parsing global variable: " ^ @{make_string} nodeContentList);
(newIdentList, functionCallTable))
end
@@ -525,6 +541,7 @@ fun parseExternalDeclaration
statement: nodeInfo cStatement,
ndInfo: nodeInfo)))
identList
+ oldIdents
(functionCallTable: string list Symtab.table) =
let val functionReturnHOLType = conv_cDeclarationSpecifier_typ (SOME(declarationSpecifierList))
|> (fn (SOME(a)) => a)
@@ -538,27 +555,40 @@ 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)
+ (paramIdentifiers@previous_global_identifiers) oldIdents
+ val newIdentList = newIdentList'@previous_local_identifiers
in (Identifier(functionName, posL, functionReturnHOLType,
FunctionCategory(functionCategory, SOME(statement))) :: newIdentList,
newFunctionCallTable)
end
- | parseExternalDeclaration s _ _ = error("Unsupported: " ^ @{make_string} s)
+ | parseExternalDeclaration s _ _ _= error("Unsupported: " ^ @{make_string} s)
fun parseTranslUnitIdentifiers
(CTranslUnit0(externalDeclaration :: R, translUnitNodeInfo))
identList
+ oldIdents
(functionCallTable: string list Symtab.table) =
let val (newIdentList, newFunctionCallTable) =
- parseExternalDeclaration externalDeclaration identList functionCallTable
+ parseExternalDeclaration externalDeclaration identList oldIdents functionCallTable
in (debug("newIdentList (parseTranslUnitIdentifiers): " ^ @{make_string} newIdentList);
parseTranslUnitIdentifiers (CTranslUnit0(R, translUnitNodeInfo))
- newIdentList newFunctionCallTable)
+ newIdentList oldIdents newFunctionCallTable)
end
- | parseTranslUnitIdentifiers _ identList functionCallTable = (identList, functionCallTable)
+ | parseTranslUnitIdentifiers _ identList oldIdents functionCallTable = (identList, functionCallTable)
fun printIdentifier (Identifier(name, pos, typ, idType)) =
writeln("Identifier: " ^ name ^ " " ^ Position.here pos ^
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/Clean_Wrapper.thy b/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
index 5d7c7d02062e4394ea7be15c823e16daf927f540..e10d7daff84d600dd5965e662a2c1e8de454fe07 100644
--- a/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
+++ b/C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
@@ -1,7 +1,7 @@
(******************************************************************************
* Isabelle/C/Clean
*
- * Authors: Frederic Tuong, Burkhart Wolff
+ * Authors: Frederic Tuong, Lorenz Winkler, Burkhart Wolff
*
* Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
*
diff --git a/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy b/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
index 8d9d7adb581b4a38742e8b5bec123308ae6a691b..12df4f496390b528d0ce1bd54d94ccdf89c90cae 100644
--- a/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
+++ b/C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
@@ -8,7 +8,7 @@
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
- *
+
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
@@ -63,20 +63,54 @@ datatype antiq_hol = Invariant of string (* term *)
| End_spec of string (* term *)
| Calls of text_range list
| Owned_by of text_range
+ | Measure of string
+
+(*In the following data structure the annotations are saved*)
+type annotation_data = {
+ preconditions: (string*(Context.generic -> term)*Position.range) list,
+ postconditions: (string*(Context.generic -> term)*Position.range) list,
+ invariants: (string*(Context.generic -> term)*Position.range) list,
+ measures: (string*(Context.generic -> term)*Position.range) list
+}
+structure Data_Clean_Annotations = Generic_Data
+ (type T = annotation_data
+ val empty = {preconditions=[], postconditions=[], invariants=[], measures=[]}
+ val merge = K empty)
+
+fun map_context_annotation_declaration annotation_type src range context0 =
+let
+ 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";"")
+ val term =fn ctxt=>
+ (*Important change: Syntax.read_term does coerce the types of the terms
+ constructed by C_Expr antiquotation. Syntax.parse_term does not do that*)
+ (*It does substitute free variables though, which is quite an issue*)
+ Syntax.parse_term
+ (Context.proof_of (C_Module.Data_Surrounding_Env.put current_env ctxt))
+ (Token.inner_syntax_of src)
+ val function_name = (get_fun_name o #scopes o snd o C_Stack.Data_Lang.get') context0
+ val new_data = [(function_name, term, range)]
-fun toplevel _ = C_Inner_Toplevel.keep''
+ val new_context_map = Data_Clean_Annotations.map (fn {preconditions, postconditions, invariants, measures} => {
+ preconditions = case annotation_type of Spec _ => preconditions@new_data | _ => preconditions,
+ postconditions = case annotation_type of End_spec _ => postconditions@new_data | _ => postconditions,
+ invariants =case annotation_type of Invariant _ => invariants@new_data | _ => invariants,
+ measures =case annotation_type of Measure _ => measures@new_data | _ => measures
+ })
+in new_context_map context0 end
-fun bind scan _ ((stack1, (to_delay, stack2)), _) =
+fun bind scan context_map ((stack1, (to_delay, stack2)), _) =
C_Parse.range scan
>> (fn (src, range) =>
C_Env.Parsing
( (stack1, stack2)
, ( range
, C_Inner_Syntax.bottom_up
- (fn _ => fn context =>
- ML_Context.exec
- (tap (fn _ => Syntax.read_term (Context.proof_of context) (Token.inner_syntax_of src)))
- context)
+ (fn v1 => fn context =>(
+ context_map src range context)
+ )
, Symtab.empty
, to_delay)))
@@ -92,17 +126,18 @@ user-defined annotations is very similar to the registration of ordinary command
platform.\<close>
ML \<open>local open Clean_Annotation
- in fun command keyword f =
+ in fun command keyword annotation_type =
C_Annotation.command' keyword ""
(C_Token.syntax'
(Parse.token Parse.cartouche)
- >>> toplevel f)
- end\<close>
+ >>> map_context_annotation_declaration annotation_type)
+ end\<close>
setup \<open>let open Clean_Annotation
- in command ("pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) Spec
- #> command ("post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) End_spec
- #> command ("inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) Invariant
+ in command ("pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Spec "")
+ #> command ("post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (End_spec "")
+ #> command ("inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Invariant "")
+ #> command ("measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Measure "")
end\<close>
end
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/main/C_Main.thy b/C11-FrontEnd/main/C_Main.thy
index 35899cbe078c1318a056fb968cbecb4baf1f8257..c82132bf5fbc216eb4d0302f910fbac300a902b5 100644
--- a/C11-FrontEnd/main/C_Main.thy
+++ b/C11-FrontEnd/main/C_Main.thy
@@ -40,5 +40,7 @@ theory C_Main
begin
text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
+
+
end
(*>*)
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)) =>
diff --git a/C11-FrontEnd/src/C_Command.thy b/C11-FrontEnd/src/C_Command.thy
index 974aa23533b13402512d0d28daa90dbfe78caa7b..2548d5ed33d647820c46d1001e8170c93310a9d0 100644
--- a/C11-FrontEnd/src/C_Command.thy
+++ b/C11-FrontEnd/src/C_Command.thy
@@ -39,6 +39,7 @@ section \<open>Interface: Inner and Outer Commands\<close>
theory C_Command
imports C_Eval
+ "../../C11-BackEnds/Clean/src/Clean"
keywords "C" :: thy_decl % "ML"
and "C_file" :: thy_load % "ML"
and "C_export_boot" :: thy_decl % "ML"
@@ -153,6 +154,8 @@ signature C_MODULE =
sig
structure Data_Accept : GENERIC_DATA
structure Data_In_Env : GENERIC_DATA
+ structure Data_Last_Env : GENERIC_DATA
+ structure Data_Surrounding_Env : GENERIC_DATA
structure Data_In_Source : GENERIC_DATA
structure Data_Term : GENERIC_DATA
@@ -168,13 +171,13 @@ signature C_MODULE =
val key_external_declaration: Input.source
val key_statement: Input.source
val key_translation_unit: Input.source
- val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
- val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
+ val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
+ val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_external_declaration:
- (C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
- val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
+ (C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
+ val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_translation_unit:
- (C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
+ (C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val tok0_expression: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
val tok0_external_declaration: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
val tok0_statement: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
@@ -265,13 +268,23 @@ structure Data_In_Env = Generic_Data
val empty = C_Env.empty_env_lang
val merge = K empty)
+structure Data_Last_Env = Generic_Data
+ (type T = C_Env.env_lang
+ val empty = C_Env.empty_env_lang
+ val merge = K empty)
+
+structure Data_Surrounding_Env = Generic_Data
+ (type T = C_Env.env_lang
+ val empty = C_Env.empty_env_lang
+ val merge = K empty)
+
structure Data_Accept = Generic_Data
(type T = C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> Context.generic
fun empty _ _ = I
val merge = #2)
structure Data_Term = Generic_Data
- (type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) Symtab.table
+ (type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> term) Symtab.table
val empty = Symtab.empty
val merge = #2)
@@ -348,8 +361,9 @@ fun err0 _ _ pos =
val err = pair () oooo err0
fun accept0 f (env_lang:C_Env.env_lang) ast =
- Data_In_Env.put env_lang
- #> (fn context => f context ast env_lang (Data_Accept.get context ast env_lang context))
+ (fn ctx => Data_Last_Env.put (Data_In_Env.get ctx) ctx)
+ #> Data_In_Env.put env_lang
+ #> (fn context => (f context ast env_lang (Data_Accept.get context ast env_lang context)))
fun accept (env_lang:C_Env.env_lang) (_, (ast, _, _)) =
pair () o C_Env.map_context (accept0 (K (K (K I))) env_lang ast)
@@ -373,18 +387,19 @@ fun accept ctxt start_rule =
val (key, pos) = Input.source_content key
in
( start
- , fn env_lang => fn (_, (ast, _, _)) =>
+ , fn env_lang => fn (_, (ast, _, _)) =>((*This env_lang also contains the previous environment,
+ but returning this would completely override the new env (which would be bad in case of parsing input with ned declarations)*)
C_Env.map_context'
(accept0
- (fn context =>
+ (fn context =>(
pair oo (case Symtab.lookup (Data_Term.get context) key of
NONE => tap (fn _ => warning ("Representation function associated to\
\ \"" ^ key ^ "\"" ^ Position.here pos
^ " not found (returning a dummy term)"))
(fn _ => fn _ => @{term "()"})
- | SOME f => fn ast => fn env_lang => f ast env_lang ctxt))
+ | SOME f => fn ast => fn env_lang => f ast env_lang (Context.Proof ctxt))))
env_lang
- ast))
+ ast)))
end
fun eval_in text context env start_rule =
@@ -423,9 +438,9 @@ fun parse_translation l = l |>
src
(case Context.get_generic_context () of
NONE => Context.Proof ctxt
- | SOME context => Context.mapping I (K ctxt) context)
- (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt
- | SOME (_, env_lang) => env_lang))
+ | SOME context => Context.Proof ctxt)
+ (fn _ => (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt (*HERE: This is a "fix" for starting with the current C_Env when parsing antiquotations.*)
+ | SOME (_, env_lang) => env_lang)) (Context.Proof ctxt))
start_rule
(c_enclose "" "" src)
end
@@ -931,7 +946,7 @@ fun command_ml environment catch_all debug get_file gthy =
val ML = command_ml "" false;
val SML = command_ml ML_Env.SML true;
end;
-\<close>
+\<close>
subsubsection \<open>Initialization\<close>
@@ -1309,6 +1324,7 @@ fun update_Root_Ast filter ast _ ctxt =
end;
+
fun get_Root_Ast filter thy =
let val ctxt = Context.Theory thy
val thid = Context.theory_long_name(Context.theory_of ctxt)
diff --git a/C11-FrontEnd/src/C_Environment.thy b/C11-FrontEnd/src/C_Environment.thy
index 985c19d760479c3af48bad136f7042324c8b563b..ece49874cd815bb5d4033ffc61a00d383d385cb1 100644
--- a/C11-FrontEnd/src/C_Environment.thy
+++ b/C11-FrontEnd/src/C_Environment.thy
@@ -59,11 +59,13 @@ signature C_ENV =
type 'a stream = ('a, C_Lex.token) C_Scan.either list
datatype 'a parse_status = Parsed of 'a | Previous_in_stack
+ datatype variable_scope = Global | Local | Parameter
eqtype markup_global
-
- type markup_ident = {global : markup_global,
+
+ type markup_ident = {scope : markup_global,
params : C_Ast.CDerivedDeclr list,
- ret : C_Ast.CDeclSpec list parse_status}
+ ret : C_Ast.CDeclSpec list parse_status,
+ functionArgs : ((string*(C_Ast.NodeInfo C_Ast.cDeclaration)) list) C_Ast.optiona}
type 'a markup_store = Position.T list * serial * 'a
type var_table = {idents : markup_ident markup_store Symtab.table,
@@ -200,11 +202,14 @@ type env_directives =
datatype 'a parse_status = Parsed of 'a | Previous_in_stack
-type markup_global = bool (*true: global*)
+datatype variable_scope = Global | Local | Parameter
+
+type markup_global = variable_scope (*true: global*)
-type markup_ident = { global : markup_global
+type markup_ident = { scope : markup_global
, params : C_Ast.CDerivedDeclr list
- , ret : C_Ast.CDeclSpec list parse_status }
+ , ret : C_Ast.CDeclSpec list parse_status
+ , functionArgs : ((string*(C_Ast.NodeInfo C_Ast.cDeclaration)) list) C_Ast.optiona}
type var_table = { tyidents : markup_global markup_store Symtab.table (*ident name*)
Symtab.table (*internal
@@ -406,9 +411,9 @@ fun map_idents f {tyidents, idents} =
(**)
fun map_var_table f {var_table, scopes, namesupply, stream_ignored, env_directives} =
- {var_table = f
+ ({var_table = f
var_table, scopes = scopes, namesupply = namesupply,
- stream_ignored = stream_ignored, env_directives = env_directives}
+ stream_ignored = stream_ignored, env_directives = env_directives})
fun map_scopes f {var_table, scopes, namesupply, stream_ignored, env_directives} =
{var_table = var_table, scopes = f
@@ -503,7 +508,9 @@ fun string_of (env_lang : env_lang) =
let fun dest0 x f = x |> Symtab.dest |> map f
fun dest {tyidents, idents} =
(dest0 tyidents #1, dest0 idents (fn (i, (_,_,v)) =>
- (i, if #global v then "global" else "local")))
+ (i, case #scope v of Global => "global"
+ | Local => "local"
+ | Parameter => "parameter")))
in \<^make_string> ( ("var_table", dest (#var_table env_lang))
, ("scopes", map (fn (id, i) =>
( Option.map (fn C_Ast.Ident0 (i, _, _) =>
diff --git a/C11-FrontEnd/src/C_Eval.thy b/C11-FrontEnd/src/C_Eval.thy
index beba4287778df3c5a4066efdccbe397f9eb37df7..54b51839b781c6d4e826fa268231ff75290aeade 100644
--- a/C11-FrontEnd/src/C_Eval.thy
+++ b/C11-FrontEnd/src/C_Eval.thy
@@ -219,7 +219,8 @@ fun makeLexer ((stack, stack_ml, stack_pos, stack_tree), arg) =
|> C_Hook.advance stack
|> f
|> (fn (arg, stack_ml) => rpair ((stack, stack_ml, stack_pos, stack_tree), arg))
- fun return0 x = \<comment> \<open>Warning: \<open>C_Hook.advance\<close> must not be early evaluated here, as it might
+ fun return0 x = \<comment> \<open>Warning: \<open>C_Hook.advance\<close> must not be early evae
+luated here, as it might
generate undesirable markup reporting (in annotation commands).\<close>
\<comment> \<open>Todo: Arrange \<open>C_Hook.advance\<close> as a pure function, so that the overall could
be eta-simplified.\<close>
@@ -760,26 +761,27 @@ fun eval env start err accept (ants, ants_err) {context, reports_text, error_lin
val () = if Config.get ctxt C_Options.lexer_trace andalso Context_Position.is_visible ctxt
then print (map_filter (fn Right x => SOME x | _ => NONE) ants_stack)
else ()
- in
- C_Language.eval env
+ val v = C_Language.eval env
start
err
accept
ants_stack
{context = context, reports_text = reports_text, error_lines = error_lines}
- end
+ in
+ v
+ end
(* derived versions *)
fun eval' env start err accept ants =
Context.>>> (fn context =>
- C_Env_Ext.context_map'
+ let val v =C_Env_Ext.context_map'
(eval (env context) (start context) err accept ants
#> apsnd (Context_Position.reports_enabled_generic context ? tap (Position.reports_text o #reports_text)
#> tap (#error_lines #> (fn [] => () | l => error (cat_lines (rev l))))
#> (C_Env.empty_env_tree o #context)))
- context)
+ context in v end)
end;
fun eval_source env start err accept source =
diff --git a/C11-FrontEnd/src/C_Parser_Language.thy b/C11-FrontEnd/src/C_Parser_Language.thy
index f6af7094b28c0abe2e2f0df9f78388401a40dfee..64c1528f5a1d78d8976143f1be483ee6c6c5e4da 100644
--- a/C11-FrontEnd/src/C_Parser_Language.thy
+++ b/C11-FrontEnd/src/C_Parser_Language.thy
@@ -207,7 +207,7 @@ sig
C_Env.env_tree ->
C_Env.env_lang * C_Env.env_tree
val shadowTypedef0' : C_Ast.CDeclSpec list C_Env.parse_status ->
- bool ->
+ C_Env.variable_scope ->
C_Ast.ident * C_Ast.CDerivedDeclr list ->
C_Env.env_lang ->
C_Env.env_tree ->
@@ -251,6 +251,7 @@ sig
val ident_of_decl : (Ident list, CDecl list * bool) C_Ast.either ->
(Ident * CDerivedDeclr list * CDeclSpec list) list
val doFuncParamDeclIdent : CDeclr -> unit monad
+ val extractFunctionArgs: 'a C_Ast.cDerivedDeclarator list -> ((string * 'a C_Ast.cDeclaration) list) C_Ast.optiona
end
structure C_Grammar_Rule_Lib : C_GRAMMAR_RULE_LIB =
@@ -322,14 +323,29 @@ struct
#> (case typing of NONE => I | SOME x => cons x))
(map (markup_init o Position.make_entity_markup {def = def} id varN o pair name) ps)
end)
-
+ fun extractFunctionArgs ident =
+ let fun getVarName nameDecl = case nameDecl of Some (Ident0 (SS_base (ST name),_,_)) => name
+ | _ => "unknown"
+ fun getTypeSuffix potentialArrDeclaration = case potentialArrDeclaration of ((CArrDeclr0 (_,(CNoArrSize0 false),_)):: Rest) => "[]"^(getTypeSuffix ( Rest))
+ | ((CArrDeclr0 (_,(CArrSize0 _),_)):: Rest) => "[somesize]"^(getTypeSuffix ( Rest))
+ | ((CPtrDeclr0 _):: Rest) => "*"^(getTypeSuffix Rest)
+ | [] => ""
+ | _ => "unknown"
+ fun transformDeclaration decl =
+ case decl of
+ (CDecl0 ([CTypeSpec0 (typespec)],[((Some (CDeclr0 (nameIdent,potentialArrDeclarations,_,_,_)),_),_)],_)) => (getVarName nameIdent,decl)
+ in
+ case ident of [CFunDeclr0 (Right (declarations,_),_,_)] => Some (map transformDeclaration declarations)
+ | _ => None
+ end
fun markup_make' typing get_global desc report =
markup_make
typing
get_global
(fn global =>
- "C " ^ (case global of SOME true => "global "
- | SOME false => "local "
+ "C " ^ (case global of SOME C_Env.Global => "global "
+ | SOME C_Env.Local => "local "
+ | SOME C_Env.Parameter => "parameter "
| NONE => "")
^ desc)
(fn cons' => fn def =>
@@ -344,8 +360,8 @@ struct
I
desc
(fn cons' => fn def =>
- fn true => cons' (if def then Markup.free else Markup.ML_keyword3)
- | false => cons' Markup.skolem)
+ fn C_Env.Global => cons' (if def then Markup.free else Markup.ML_keyword3)
+ | _ => cons' Markup.skolem)
val markup_tvar = markup_tvar0 "type variable"
val markup_var_enum = markup_tvar0 "enum tag"
@@ -411,20 +427,20 @@ struct
val markup_var =
markup_make'
typing
- #global
+ #scope
"variable"
(fn cons' => fn def =>
- fn true => if def then cons' Markup.free else cons' Markup.delimiter (*explicit black color,
+ fn C_Env.Global => if def then cons' Markup.free else cons' Markup.delimiter (*explicit black color,
otherwise the default color of constants might
be automatically chosen (especially in term
cartouches)*)
- | false => cons' Markup.bound)
+ | _ => cons' Markup.bound)
val markup_var_bound =
- markup_make' typing #global "variable" (fn cons' => K (K (cons' Markup.bound)))
+ markup_make' typing #scope "variable" (fn cons' => K (K (cons' Markup.bound)))
val markup_var_improper =
- markup_make' typing #global "variable" (fn cons' => K (K (cons' Markup.improper)))
+ markup_make' typing #scope "variable" (fn cons' => K (K (cons' Markup.improper)))
(**)
val return = pair
@@ -528,7 +544,7 @@ struct
fun addTypedef (Ident0 (_, i, node)) env =
let val name = ident_decode i
val pos1 = [decode_error' node |> #1]
- val data = (pos1, serial (), null (C_Env_Ext.get_scopes env))
+ val data = (pos1, serial (), if null (C_Env_Ext.get_scopes env) then C_Env.Global else C_Env.Local)
in ((), env |> C_Env_Ext.map_idents (Symtab.delete_safe name)
|> C_Env_Ext.map_tyidents_typedef (Symtab.update (name, data))
|> C_Env_Ext.map_reports_text
@@ -540,8 +556,8 @@ struct
fun shadowTypedef0''' name pos data0 env_lang env_tree =
let val data = (pos, serial (), data0)
val update_id = Symtab.update (name, data)
- in ( env_lang |> C_Env_Ext.map_tyidents'_typedef (Symtab.delete_safe name)
- |> C_Env_Ext.map_idents' update_id
+ in (env_lang |> C_Env_Ext.map_tyidents'_typedef (Symtab.delete_safe name)
+ |> C_Env_Ext.map_idents' update_id (*In this line entries get added to the var table*)
, update_id
, env_tree
|> C_Env.map_reports_text
@@ -553,25 +569,25 @@ struct
fun shadowTypedef0'''' name pos data0 env_lang env_tree =
let val (env_lang, _, env_tree) = shadowTypedef0''' name pos data0 env_lang env_tree
in ( env_lang, env_tree) end
- fun shadowTypedef0'' ret global (Ident0 (_, i, node), params) =
+ fun shadowTypedef0'' ret scope (Ident0 (a, i, node), params) =
shadowTypedef0''' (ident_decode i)
[decode_error' node |> #1]
- {global = global, params = params, ret = ret}
+ {scope = scope, params = params, ret = ret, functionArgs = extractFunctionArgs params }
fun shadowTypedef0' ret global ident env_lang env_tree =
- let val (env_lang, _, env_tree) = shadowTypedef0'' ret global ident env_lang env_tree
+ let val (env_lang, _, env_tree) = shadowTypedef0'' ret global ident env_lang env_tree
in (env_lang, env_tree) end
fun shadowTypedef0 ret global f ident env =
let val (update_id, env) =
C_Env.map_env_lang_tree'
(fn env_lang => fn env_tree =>
let val (env_lang, update_id, env_tree) =
- shadowTypedef0'' ret global ident env_lang env_tree
+ shadowTypedef0'' ret global ident env_lang env_tree
in (update_id, (env_lang, env_tree)) end)
env
in ((), f update_id env) end
fun shadowTypedef_fun ident env =
- shadowTypedef0 C_Env.Previous_in_stack
- (case C_Env_Ext.get_scopes env of _ :: [] => true | _ => false)
+ shadowTypedef0 C_Env.Previous_in_stack
+ (case C_Env_Ext.get_scopes env of _ :: [] => C_Env.Global | _ => C_Env.Local)
(fn update_id =>
C_Env_Ext.map_scopes
(fn (NONE, x) :: xs => (SOME (fst ident), C_Env.map_idents update_id x) :: xs
@@ -579,8 +595,10 @@ struct
| [] => error "Not expecting an empty scope"))
ident
env
+ fun shadowTypedef_function_param (i,params, ret) env =
+ shadowTypedef0 (C_Env.Parsed ret) C_Env.Parameter (K I) (i, params) env
fun shadowTypedef (i, params, ret) env =
- shadowTypedef0 (C_Env.Parsed ret) (List.null (C_Env_Ext.get_scopes env)) (K I) (i, params) env
+ shadowTypedef0 (C_Env.Parsed ret) (if List.null (C_Env_Ext.get_scopes env) then C_Env.Global else C_Env.Local) (K I) (i, params) env (*This line is relevant. From here the parameters call origins*)
fun isTypeIdent s0 = Symtab.exists (fn (s1, _) => s0 = s1) o C_Env_Ext.get_tyidents_typedef
fun enterScope env =
((), C_Env_Ext.map_scopes (cons (NONE, C_Env_Ext.get_var_table env)) env)
@@ -588,7 +606,7 @@ struct
case C_Env_Ext.get_scopes env of
[] => error "leaveScope: already in global scope"
| (_, var_table) :: scopes => ((), env |> C_Env_Ext.map_scopes (K scopes)
- |> C_Env_Ext.map_var_table (K var_table))
+ |> C_Env_Ext.map_var_table (K var_table)) (*This line is responsible for scoped vars from the var_table (replacing it with I keeps the vars)*)
val getCurrentPosition = return NoPosition
(* Language.C.Parser.Tokens *)
@@ -709,7 +727,7 @@ struct
| _ => rappend declspecs (liftCAttrs new_attrs)
val emptyDeclr = CDeclrR Nothing empty Nothing [] undefNode
fun mkVarDeclr ident = CDeclrR (Some ident) empty Nothing []
- fun doDeclIdent declspecs (decl as CDeclrR0 (mIdent, _, _, _, _)) =
+ fun doDeclIdent declspecs (decl as CDeclrR0 (mIdent, _,_,_,_)) =
case mIdent of
None => return ()
| Some ident =>
@@ -750,7 +768,7 @@ struct
(case mIdent0 of None => return ()
| Some mIdent0 => shadowTypedef_fun (mIdent0, param0))
>>
- sequence_ shadowTypedef
+ sequence_ shadowTypedef_function_param
(maps (fn CFunDeclr0 (params, _, _) => ident_of_decl params | _ => []) param_fun)
>>
sequence_
@@ -764,7 +782,7 @@ struct
val pos = [decode_error' node |> #1]
val data = ( pos
, serial ()
- , {global = false, params = params, ret = C_Env.Parsed ret})
+ , {scope = C_Env.Local, params = params, ret = C_Env.Parsed ret, functionArgs = extractFunctionArgs params})
in
( env_lang |> Symtab.update (name, data)
, env_tree
@@ -947,7 +965,7 @@ val declarator1 : (CDeclrR) -> unit monad =
val pos = [decode_error' node |> #1]
val data = ( pos
, serial ()
- , {global = false, params = params, ret = C_Env.Parsed ret})
+ , {scope = C_Env.Local, params = params, ret = C_Env.Parsed ret, functionArgs = extractFunctionArgs params})
in
( env_lang |> Symtab.update (name, data)
, env_tree
@@ -1019,7 +1037,7 @@ val declaration : (CDecl) -> unit monad =
fn (env_lang, env_tree) =>
let val name = ident_decode i
val pos1 = [decode_error' node |> #1]
- val data = (pos1, serial (), null (C_Env.get_scopes env_lang))
+ val data = (pos1, serial (), if null (C_Env.get_scopes env_lang) then C_Env.Global else C_Env.Local)
in
( C_Env_Ext.map_tyidents'_enum (Symtab.update (name, data)) env_lang
, C_Env.map_reports_text
@@ -1053,7 +1071,7 @@ val enumerator : ( ( Ident * CExpr Maybe ) ) -> unit monad =
fn (ident as Ident0 (_, _, node), _) =>
C_Grammar_Rule_Lib.shadowTypedef0'
(C_Env.Parsed [CTypeSpec0 (CIntType0 node)])
- (null (C_Env.get_scopes env_lang))
+ (if null (C_Env.get_scopes env_lang) then C_Env.Global else C_Env.Local)
(ident, [])
env_lang
end
diff --git a/README_dev b/README_dev
index ac2d9407b3785a63d37e55eaebe514979308705a..f8dd26eec3f4ce3079a0bcd1782593d05ce2153d 100644
--- a/README_dev
+++ b/README_dev
@@ -9,3 +9,6 @@ START FOR EXAMPLE:
cd Isabelle_C
isabelle jedit -d . C11-BackEnds/Clean_wrapper/examples/Coder_Test_ExprStmt.thy
+Branch LorenzWinkler:
+cd Isabelle_C
+isabelle jedit -d C11-FrontEnd -d C11-BackEnds/Clean C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy