src/Tools/Code/code_preproc.ML
changeset 32873 333945c9ac6a
parent 32872 019201eb7e07
child 33063 4d462963a7db
     1.1 --- a/src/Tools/Code/code_preproc.ML	Mon Oct 05 08:36:33 2009 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Oct 05 15:04:45 2009 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    type code_algebra
     1.5    type code_graph
     1.6    val eqns: code_graph -> string -> (thm * bool) list
     1.7 -  val typ: code_graph -> string -> (string * sort) list * typ
     1.8 +  val sortargs: code_graph -> string -> sort list
     1.9    val all: code_graph -> string list
    1.10    val pretty: theory -> code_graph -> Pretty.T
    1.11    val obtain: theory -> string list -> term list -> code_algebra * code_graph
    1.12 @@ -62,7 +62,7 @@
    1.13    val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
    1.14    fun copy spec = spec;
    1.15    val extend = copy;
    1.16 -  fun merge pp = merge_thmproc;
    1.17 +  fun merge _ = merge_thmproc;
    1.18  );
    1.19  
    1.20  fun the_thmproc thy = case Code_Preproc_Data.get thy
    1.21 @@ -196,10 +196,10 @@
    1.22  (** sort algebra and code equation graph types **)
    1.23  
    1.24  type code_algebra = (sort -> sort) * Sorts.algebra;
    1.25 -type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
    1.26 +type code_graph = ((string * sort) list * (thm * bool) list) Graph.T;
    1.27  
    1.28  fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
    1.29 -fun typ eqngr = fst o Graph.get_node eqngr;
    1.30 +fun sortargs eqngr = map snd o fst o Graph.get_node eqngr
    1.31  fun all eqngr = Graph.keys eqngr;
    1.32  
    1.33  fun pretty thy eqngr =
    1.34 @@ -227,6 +227,14 @@
    1.35    map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
    1.36      o maps (#params o AxClass.get_info thy);
    1.37  
    1.38 +fun typscheme_rhss thy c eqns =
    1.39 +  let
    1.40 +    val tyscm = Code.typscheme_eqns thy c (map fst eqns);
    1.41 +    val rhss = [] |> (fold o fold o fold_aterms)
    1.42 +      (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    1.43 +        (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
    1.44 +  in (tyscm, rhss) end;
    1.45 +
    1.46  
    1.47  (* data structures *)
    1.48  
    1.49 @@ -262,11 +270,11 @@
    1.50  
    1.51  fun obtain_eqns thy eqngr c =
    1.52    case try (Graph.get_node eqngr) c
    1.53 -   of SOME ((lhs, _), eqns) => ((lhs, []), [])
    1.54 +   of SOME (lhs, eqns) => ((lhs, []), [])
    1.55      | NONE => let
    1.56          val eqns = Code.these_eqns thy c
    1.57            |> preprocess thy c;
    1.58 -        val ((lhs, _), rhss) = Code.typscheme_rhss_eqns thy c (map fst eqns);
    1.59 +        val ((lhs, _), rhss) = typscheme_rhss thy c eqns;
    1.60        in ((lhs, rhss), eqns) end;
    1.61  
    1.62  fun obtain_instance thy arities (inst as (class, tyco)) =
    1.63 @@ -413,11 +421,11 @@
    1.64        Vartab.update ((v, 0), sort)) lhs;
    1.65      val eqns = proto_eqns
    1.66        |> (map o apfst) (inst_thm thy inst_tab);
    1.67 -    val (tyscm, rhss') = Code.typscheme_rhss_eqns thy c (map fst eqns);
    1.68 -    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
    1.69 +    val ((vs, _), rhss') = typscheme_rhss thy c eqns;
    1.70 +    val eqngr' = Graph.new_node (c, (vs, eqns)) eqngr;
    1.71    in (map (pair c) rhss' @ rhss, eqngr') end;
    1.72  
    1.73 -fun extend_arities_eqngr thy cs ts (arities, eqngr) =
    1.74 +fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
    1.75    let
    1.76      val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
    1.77        insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
    1.78 @@ -430,7 +438,7 @@
    1.79        (AList.lookup (op =) arities') (Sign.classes_of thy);
    1.80      val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
    1.81      fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
    1.82 -      (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
    1.83 +      (rhs ~~ sortargs eqngr' c);
    1.84      val eqngr'' = fold (fn (c, rhs) => fold
    1.85        (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
    1.86    in (algebra, (arities', eqngr'')) end;