code_funcgr interface includes also sort algebra
authorhaftmann
Mon Dec 01 12:17:02 2008 +0100 (2008-12-01)
changeset 289245c8781b7d6a4
parent 28923 0a981c596372
child 28925 1cb9596498c0
code_funcgr interface includes also sort algebra
src/Tools/code/code_funcgr.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:01 2008 +0100
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:02 2008 +0100
     1.3 @@ -13,9 +13,12 @@
     1.4    val typ: T -> string -> (string * sort) list * typ
     1.5    val all: T -> string list
     1.6    val pretty: theory -> T -> Pretty.T
     1.7 -  val make: theory -> string list -> T
     1.8 -  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
     1.9 -  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
    1.10 +  val make: theory -> string list
    1.11 +    -> ((sort -> sort) * Sorts.algebra) * T
    1.12 +  val eval_conv: theory
    1.13 +    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
    1.14 +  val eval_term: theory
    1.15 +    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    1.16    val timing: bool ref
    1.17  end
    1.18  
    1.19 @@ -235,7 +238,7 @@
    1.20      val consts' = consts_of t'';
    1.21      val dicts = instances_of_consts thy algebra funcgr' consts';
    1.22      val funcgr'' = ensure_consts thy algebra dicts funcgr';
    1.23 -  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
    1.24 +  in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
    1.25  
    1.26  fun proto_eval_conv thy =
    1.27    let
    1.28 @@ -267,7 +270,8 @@
    1.29  );
    1.30  
    1.31  fun make thy =
    1.32 -  Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
    1.33 +  pair (Code.operational_algebra thy)
    1.34 +  o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
    1.35  
    1.36  fun eval_conv thy f =
    1.37    fst o Funcgr.change_yield thy o proto_eval_conv thy f;
    1.38 @@ -280,7 +284,7 @@
    1.39  
    1.40  fun code_depgr thy consts =
    1.41    let
    1.42 -    val gr = make thy consts;
    1.43 +    val (_, gr) = make thy consts;
    1.44      val select = Graph.all_succs gr consts;
    1.45    in
    1.46      gr
     2.1 --- a/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:01 2008 +0100
     2.2 +++ b/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:02 2008 +0100
     2.3 @@ -489,7 +489,7 @@
     2.4  
     2.5  fun ensure_class thy (algbr as (_, algebra)) funcgr class =
     2.6    let
     2.7 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
     2.8 +    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     2.9      val cs = #params (AxClass.get_info thy class);
    2.10      val stmt_class =
    2.11        fold_map (fn superclass => ensure_class thy algbr funcgr superclass
    2.12 @@ -538,8 +538,16 @@
    2.13            Global ((class, tyco), yss)
    2.14        | class_relation (Local (classrels, v), subclass) superclass =
    2.15            Local ((subclass, superclass) :: classrels, v);
    2.16 +    fun norm_typargs ys =
    2.17 +      let
    2.18 +        val raw_sort = map snd ys;
    2.19 +        val sort = Sorts.minimize_sort algebra raw_sort;
    2.20 +      in
    2.21 +        map_filter (fn (y, class) =>
    2.22 +          if member (op =) sort class then SOME y else NONE) ys
    2.23 +      end;
    2.24      fun type_constructor tyco yss class =
    2.25 -      Global ((class, tyco), (map o map) fst yss);
    2.26 +      Global ((class, tyco), map norm_typargs yss);
    2.27      fun type_variable (TFree (v, sort)) =
    2.28        let
    2.29          val sort' = proj_sort sort;
    2.30 @@ -567,7 +575,7 @@
    2.31    end
    2.32  and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
    2.33    let
    2.34 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    2.35 +    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    2.36      val classparams = these (try (#params o AxClass.get_info thy) class);
    2.37      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    2.38      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    2.39 @@ -736,9 +744,9 @@
    2.40  
    2.41  val cached_program = Program.get;
    2.42  
    2.43 -fun invoke_generation thy funcgr f name =
    2.44 +fun invoke_generation thy (algebra, funcgr) f name =
    2.45    Program.change_yield thy (fn naming_program => (NONE, naming_program)
    2.46 -    |> f thy (Code.operational_algebra thy) funcgr name
    2.47 +    |> f thy algebra funcgr name
    2.48      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
    2.49  
    2.50  
    2.51 @@ -789,9 +797,10 @@
    2.52  fun eval thy evaluator t =
    2.53    let
    2.54      val (t', evaluator'') = evaluator t;
    2.55 -    fun evaluator' funcgr =
    2.56 +    fun evaluator' algebra funcgr =
    2.57        let
    2.58 -        val (((naming, program), (vs_ty_t, deps)), _) = invoke_generation thy funcgr ensure_value t';
    2.59 +        val (((naming, program), (vs_ty_t, deps)), _) =
    2.60 +          invoke_generation thy (algebra, funcgr) ensure_value t';
    2.61        in evaluator'' naming program vs_ty_t deps end;
    2.62    in (t', evaluator') end
    2.63