maximize the evaluation for annotations

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

C11-FrontEnd/examples/C1.thy

@@ -269,6 +269,15 @@ int b,c,d/*@@ \<approx>setup\<Down> \<open>fn s => fn x => fn env => @{print_top
                                                 #> add_ex "evaluation of " "5_print_top"\<close> */
 \<close>
 
+subsection \<open>Out of Bound Evaluation for Annotations\<close>
+
+C \<comment> \<open>Bottom-up and top-down\<close> \<open>
+int a = 0 ;
+int     /*@ @    ML \<open>writeln "2"\<close>
+                 ML\<Down>\<open>writeln "1"\<close>  */
+    a = 0;
+\<close>
+
 section \<open>Reporting of Positions and Contextual Update of Environment\<close>
 
 text \<open>

C11-FrontEnd/src/C_Eval.thy

@@ -147,9 +147,12 @@ fun advance00 stack ml_exec =
                                    arg)
   | (_, C_Env.Bottom_up (C_Env.Exec_directive exec), env_dir, _) =>
      C_Env.map_env_lang_tree (curry (exec NONE env_dir))
-  | ((pos, _), _, _, _) =>
-     C_Env_Ext.map_context (fn _ => error ( "Style of evaluation not yet implemented"
-                                          ^ Position.here pos))
+  | ((pos, _), C_Env.Top_down exec, env_dir, _) =>
+     tap (fn _ => warning ("Missing navigation, evaluating as bottom-up style instead of top-down"
+                           ^ Position.here pos))
+     #>
+     (fn arg => C_Env.map_env_tree (C_Stack.stack_exec env_dir (stack, #env_lang arg) (exec NONE))
+                                   arg)
 
 fun advance0 stack (_, syms_reduce, ml_exec) =
   let