# HG changeset patch
# User haftmann
# Date 1174077142 -3600
# Node ID 164e7be2773663a636cb3f93042967d79a06a4f0
# Parent  d0e12f0d4e444e8b09f8af9eb37cf9f05dc7a09d
added "satisfies" interface

diff -r d0e12f0d4e44 -r 164e7be27736 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Mar 16 21:32:21 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 16 21:32:22 2007 +0100
@@ -10,6 +10,8 @@
   include BASIC_CODEGEN_THINGOL;
   val codegen_term: theory -> term -> iterm;
   val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
+  val satisfies_ref: bool option ref;
+  val satisfies: theory -> term -> string list -> bool;
   val codegen_command: theory -> string -> unit;
 
   type appgen;
@@ -570,13 +572,22 @@
     val t' = Thm.term_of ct';
   in generate thy funcgr (SOME []) exprgen_term' t' end;
 
-fun eval_term thy (ref_spec, t) =
+fun raw_eval_term thy (ref_spec, t) args =
   let
     val _ = (Term.fold_types o Term.fold_atyps) (fn _ =>
-      error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
+      error ("Term" ^ Sign.string_of_term thy t ^ "is polymorphic"))
       t;
     val t' = codegen_term thy t;
-  in CodegenSerializer.eval_term thy CodegenNames.labelled_name (Code.get thy) (ref_spec, t') end;
+  in
+    CodegenSerializer.eval_term thy CodegenNames.labelled_name
+      (Code.get thy) (ref_spec, t') args
+  end;
+
+val satisfies_ref : bool option ref = ref NONE;
+
+fun eval_term thy t = raw_eval_term thy t [];
+fun satisfies thy t witnesses = raw_eval_term thy
+  (("CodegenPackage.satisfies_ref", satisfies_ref), t) witnesses;
 
 
 (* constant specifications with wildcards *)
diff -r d0e12f0d4e44 -r 164e7be27736 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 16 21:32:21 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Mar 16 21:32:22 2007 +0100
@@ -36,7 +36,7 @@
 
   val eval_verbose: bool ref;
   val eval_term: theory -> (theory -> string -> string) -> CodegenThingol.code
-    -> (string * 'a option ref) * CodegenThingol.iterm -> 'a;
+    -> (string * 'a option ref) * CodegenThingol.iterm -> string list -> 'a;
   val code_width: int ref;
 end;
 
@@ -1629,10 +1629,11 @@
 
 val eval_verbose = ref false;
 
-fun eval_term thy labelled_name code ((ref_name, reff), t) =
+fun eval_term thy labelled_name code ((ref_name, reff), t) args =
   let
     val val_name = "eval.EVAL.EVAL";
     val val_name' = "ROOT.eval.EVAL";
+    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
     val data = (the o Symtab.lookup (CodegenSerializerData.get thy)) "SML"
     val reserved = the_reserved data;
     val { alias, prolog } = the_syntax_modl data;
@@ -1643,7 +1644,7 @@
       if !eval_verbose then Pretty.writeln p else ();
       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
         ((Pretty.output o Pretty.chunks) [p,
-          str ("val _ = (" ^ ref_name ^ " := SOME " ^ val_name' ^ ")")
+          str ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))")
         ]);
       case !reff
        of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name