src/Tools/code/code_package.ML
changeset 24381 560e8ecdf633
parent 24348 c708ea5b109a
child 24423 ae9cd0e92423
     1.1 --- a/src/Tools/code/code_package.ML	Tue Aug 21 13:30:36 2007 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Tue Aug 21 13:30:38 2007 +0200
     1.3 @@ -9,10 +9,12 @@
     1.4  sig
     1.5    (* interfaces *)
     1.6    val eval_conv: theory
     1.7 -    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> thm)
     1.8 +    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
     1.9 +       -> string list -> cterm -> thm)
    1.10      -> cterm -> thm;
    1.11    val eval_term: theory
    1.12 -    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> 'a)
    1.13 +    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
    1.14 +       -> string list -> cterm -> 'a)
    1.15      -> cterm -> 'a;
    1.16    val satisfies_ref: bool option ref;
    1.17    val satisfies: theory -> cterm -> string list -> bool;
    1.18 @@ -285,10 +287,10 @@
    1.19            ##>> exprgen_term thy algbr funcgr rhs;
    1.20        in
    1.21          trns
    1.22 -        |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
    1.23 -        ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.24 +        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.25          ||>> exprgen_typ thy algbr funcgr ty
    1.26 -        |>> (fn ((eqs, vs), ty) => CodeThingol.Fun (eqs, (vs, ty)))
    1.27 +        ||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
    1.28 +        |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
    1.29        end;
    1.30      val defgen = if (is_some o Code.get_datatype_of_constr thy) const
    1.31        then defgen_datatypecons
    1.32 @@ -536,25 +538,28 @@
    1.33      val value_name = "Isabelle_Eval.EVAL.EVAL";
    1.34      fun ensure_eval thy algbr funcgr t = 
    1.35        let
    1.36 +        val ty = fastype_of t;
    1.37 +        val vs = typ_tfrees ty;
    1.38          val defgen_eval =
    1.39 -          exprgen_term' thy algbr funcgr t
    1.40 -          ##>> exprgen_typ thy algbr funcgr (fastype_of t)
    1.41 -          #>> (fn (t, ty) => CodeThingol.Fun ([([], t)], ([], ty)));
    1.42 +          fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.43 +          ##>> exprgen_typ thy algbr funcgr ty
    1.44 +          ##>> exprgen_term' thy algbr funcgr t
    1.45 +          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [([], t)]));
    1.46          fun result (dep, code) =
    1.47            let
    1.48 -            val CodeThingol.Fun ([([], t)], ([], ty)) = Graph.get_node code value_name;
    1.49 +            val CodeThingol.Fun ((vs, ty), [([], t)]) = Graph.get_node code value_name;
    1.50              val deps = Graph.imm_succs code value_name;
    1.51              val code' = Graph.del_nodes [value_name] code;
    1.52              val code'' = CodeThingol.project_code false [] (SOME deps) code';
    1.53 -          in ((code'', (t, ty), deps), (dep, code')) end;
    1.54 +          in ((code'', ((vs, ty), t), deps), (dep, code')) end;
    1.55        in
    1.56          ensure_def thy defgen_eval "evaluation" value_name
    1.57          #> result
    1.58        end;
    1.59      fun h funcgr ct =
    1.60        let
    1.61 -        val (code, (t, ty), deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
    1.62 -      in g code (t, ty) deps ct end;
    1.63 +        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
    1.64 +      in g code vs_ty_t deps ct end;
    1.65    in f thy h end;
    1.66  
    1.67  fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
    1.68 @@ -564,7 +569,7 @@
    1.69  
    1.70  fun satisfies thy ct witnesses =
    1.71    let
    1.72 -    fun evl code (t, ty) deps ct =
    1.73 +    fun evl code ((vs, ty), t) deps ct =
    1.74        let
    1.75          val t0 = Thm.term_of ct
    1.76          val _ = (Term.map_types o Term.map_atyps) (fn _ =>