improved documentation.

C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy

@@ -27,12 +27,12 @@ To prevent Isabelle from coercing types of returned terms \<open>Syntax.parse_te
 Furthermore as parameters are represented as free variables, all constants that would be "selected" through
 a parameter name need to be hidden (\<open>remove_params_from_proof\<close>).
 
-Environment:
+\<^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 \<open>functionArgs\<close> which is an optional list of function parameters.
 When an identifier has \<open>functionArgs = NONE\<close>, then it is a variable. \<open>functionArgs=SOME []\<close> corresponds to a parameterless function.
 
-Nice to know:
+\<^bold>\<open>Nice to know:\<close>
 - The environment of the last completely parsed C-context can be retrieved using \<open>C_Module.Data_In_Env\<close>.
 - Intermediate envs, containing parameters and local vars can be retrieved using \<open>C_Env.Data_Lang.get'\<close>.
 See C5.thy in the examples of C11-Frontend.
@@ -40,18 +40,17 @@ See C5.thy in the examples of C11-Frontend.
 
 section\<open>Limitations\<close>
 text\<open>
-- Only two types are currently mapped to isabelle types, 
-  namely int -> int and unsigned -> nat.
+\<^item> Only two types are currently mapped to isabelle types, 
+  namely \<^verbatim>\<open>int -> int\<close> and \<^verbatim>\<open>unsigned -> int\<close>.
 
-- Function calls can only occur as statements or on the right hand side of an assignment.
+\<^item> Function calls can only occur as statements or on the right hand side of an assignment.
   For example \<open>a = b + foo();\<close> is not allowed. This must be rewritten as \<open>tmp = foo(); a=b+tmp;\<close>
 
-- Recursive functions must have "void" as return value. This is caused by an issue within
   Clean and is about to be fixed. The current translation should work for this case then.
 
-- Scoping: refrain from defining variables more than once. A read/write from a local variable
+\<^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:  
+    Example:  
     \<open>int foo(){
         int x = 3;
         {
@@ -62,12 +61,13 @@ text\<open>
   Also defining global variables twice within one translation unit will result in only one definition, 
   thus the second definition does not "reset" the value of the variable
 
-- Method overloading: Do not use function names multiple times, as this will break the whole
+\<^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>
+
+text\<open>See \<open>Coder_Test_T_Units\<close> for more examples:\<close>
 
 C\<open>
 int sum_of_array(int arr[], int length){
@@ -121,7 +121,7 @@ find_theorems multiply
 find_theorems multiply_pre
 find_theorems multiply_post
 
-text\<open>A recursive function calculating the factorial of n\<close>
+text\<open>A recursive function calculating the factorial of \<open>n\<close>\<close>
 C\<open>
 int factorial_result;
 void factorial(int n){
@@ -133,3 +133,5 @@ void factorial(int n){
   }
 }\<close>
 find_theorems factorial_core
+
+end

C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy

+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)
@@ -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;
@@ -143,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" ));
@@ -153,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>

C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy

 (******************************************************************************
  * 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
  *

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
 (*>*)