# 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