(*  Title:      Tools/code/code_funcgr.ML

     ID:         $Id$

     Author:     Florian Haftmann, TU Muenchen

 Retrieving, normalizing and structuring defining equations in graph

 with explicit dependencies.

 *)

 signature CODE_FUNCGR =

 sig

   type T

   val timing: bool ref

   val funcs: T -> string -> thm list

   val typ: T -> string -> typ

   val all: T -> string list

   val pretty: theory -> T -> Pretty.T

   val make: theory -> string list -> T

   val make_consts: theory -> string list -> string list * T

   val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm

   val eval_term: theory -> (T -> term -> 'a) -> term -> 'a

 end

 structure CodeFuncgr : CODE_FUNCGR =

 struct

 (** the graph type **)

 type T = (typ * thm list) Graph.T;

 fun funcs funcgr =

   these o Option.map snd o try (Graph.get_node funcgr);

 fun typ funcgr =

   fst o Graph.get_node funcgr;

 fun all funcgr = Graph.keys funcgr;

 fun pretty thy funcgr =

   AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)

   |> (map o apfst) (CodeUnit.string_of_const thy)

   |> sort (string_ord o pairself fst)

   |> map (fn (s, thms) =>

        (Pretty.block o Pretty.fbreaks) (

          Pretty.str s

          :: map Display.pretty_thm thms

        ))

   |> Pretty.chunks;

 (** generic combinators **)

 fun fold_consts f thms =

   thms

   |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)

   |> (fold o fold_aterms) (fn Const c => f c | _ => I);

 fun consts_of (const, []) = []

   | consts_of (const, thms as _ :: _) = 

       let

         fun the_const (c, _) = if c = const then I else insert (op =) c

       in fold_consts the_const thms [] end;

 fun insts_of thy algebra c ty_decl ty =

   let

     val tys_decl = Sign.const_typargs thy (c, ty_decl);

     val tys = Sign.const_typargs thy (c, ty);

     fun class_relation (x, _) _ = x;

     fun type_constructor tyco xs class =

       (tyco, class) :: maps (maps fst) xs;

     fun type_variable (TVar (_, sort)) = map (pair []) sort

       | type_variable (TFree (_, sort)) = map (pair []) sort;

     fun mk_inst ty (TVar (_, sort)) = cons (ty, sort)

       | mk_inst ty (TFree (_, sort)) = cons (ty, sort)

       | mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2;

     fun of_sort_deriv (ty, sort) =

       Sorts.of_sort_derivation (Sign.pp thy) algebra

         { class_relation = class_relation, type_constructor = type_constructor,

           type_variable = type_variable }

         (ty, sort)

   in

     flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))

   end;

 fun drop_classes thy tfrees thm =

   let

     val (_, thm') = Thm.varifyT' [] thm;

     val tvars = Term.add_tvars (Thm.prop_of thm') [];

     val unconstr = map (Thm.ctyp_of thy o TVar) tvars;

     val instmap = map2 (fn (v_i, _) => fn (v, sort) => pairself (Thm.ctyp_of thy)

       (TVar (v_i, []), TFree (v, sort))) tvars tfrees;

   in

     thm'

     |> fold Thm.unconstrainT unconstr

     |> Thm.instantiate (instmap, [])

     |> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy))

   end;

 (** graph algorithm **)

 val timing = ref false;

 local

 exception INVALID of string list * string;

 fun resort_thms algebra tap_typ [] = []

   | resort_thms algebra tap_typ (thms as thm :: _) =

       let

         val thy = Thm.theory_of_thm thm;

         val cs = fold_consts (insert (op =)) thms [];

         fun match_const c (ty, ty_decl) =

           let

             val tys = Sign.const_typargs thy (c, ty);

             val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));

           in fold2 (curry (CodeUnit.typ_sort_inst algebra)) tys sorts end;

         fun match (c, ty) =

           case tap_typ c

            of SOME ty_decl => match_const c (ty, ty_decl)

             | NONE => I;

         val tvars = fold match cs Vartab.empty;

       in map (CodeUnit.inst_thm tvars) thms end;

 fun resort_funcss thy algebra funcgr =

   let

     val typ_funcgr = try (fst o Graph.get_node funcgr);

     fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)

       handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e

                     ^ ",\nfor constant " ^ CodeUnit.string_of_const thy const

                     ^ "\nin defining equations\n"

                     ^ (cat_lines o map string_of_thm) thms)

     fun resort_rec tap_typ (const, []) = (true, (const, []))

       | resort_rec tap_typ (const, thms as thm :: _) =

           let

             val (_, ty) = CodeUnit.head_func thm;

             val thms' as thm' :: _ = resort_thms algebra tap_typ thms

             val (_, ty') = CodeUnit.head_func thm';

           in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;

     fun resort_recs funcss =

       let

         fun tap_typ c =

           AList.lookup (op =) funcss c

           |> these

           |> try hd

           |> Option.map (snd o CodeUnit.head_func);

         val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);

         val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;

       in (unchanged, funcss') end;

     fun resort_rec_until funcss =

       let

         val (unchanged, funcss') = resort_recs funcss;

       in if unchanged then funcss' else resort_rec_until funcss' end;

   in map resort_dep #> resort_rec_until end;

 fun instances_of thy algebra insts =

   let

     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;

     fun all_classparams tyco class =

       these (try (#params o AxClass.get_info thy) class)

       |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))

   in

     Symtab.empty

     |> fold (fn (tyco, class) =>

         Symtab.map_default (tyco, []) (insert (op =) class)) insts

     |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)

          (Graph.all_succs thy_classes classes))) tab [])

   end;

 fun instances_of_consts thy algebra funcgr consts =

   let

     fun inst (cexpr as (c, ty)) = insts_of thy algebra c

       ((fst o Graph.get_node funcgr) c) ty handle CLASS_ERROR => [];

   in

     []

     |> fold (fold (insert (op =)) o inst) consts

     |> instances_of thy algebra

   end;

 fun ensure_const' thy algebra funcgr const auxgr =

   if can (Graph.get_node funcgr) const

     then (NONE, auxgr)

   else if can (Graph.get_node auxgr) const

     then (SOME const, auxgr)

   else if is_some (Code.get_datatype_of_constr thy const) then

     auxgr

     |> Graph.new_node (const, [])

     |> pair (SOME const)

   else let

     val thms = Code.these_funcs thy const

       |> CodeUnit.norm_args

       |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var;

     val rhs = consts_of (const, thms);

   in

     auxgr

     |> Graph.new_node (const, thms)

     |> fold_map (ensure_const thy algebra funcgr) rhs

     |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')

                            | NONE => I) rhs')

     |> pair (SOME const)

   end

 and ensure_const thy algebra funcgr const =

   let

     val timeap = if !timing

       then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const)

       else I;

   in timeap (ensure_const' thy algebra funcgr const) end;

 fun merge_funcss thy algebra raw_funcss funcgr =

   let

     val funcss = raw_funcss

       |> resort_funcss thy algebra funcgr

       |> filter_out (can (Graph.get_node funcgr) o fst);

     fun typ_func c [] = Code.default_typ thy c

       | typ_func c (thms as thm :: _) = case AxClass.inst_of_param thy c

          of SOME (c', tyco) => 

               let

                 val (_, ty) = CodeUnit.head_func thm;

                 val SOME class = AxClass.class_of_param thy c';

                 val sorts_decl = Sorts.mg_domain algebra tyco [class];

                 val tys = Sign.const_typargs thy (c, ty);

                 val sorts = map (snd o dest_TVar) tys;

               in if sorts = sorts_decl then ty

                 else raise INVALID ([c], "Illegal instantation for class operation "

                   ^ CodeUnit.string_of_const thy c

                   ^ "\nin defining equations\n"

                   ^ (cat_lines o map string_of_thm) thms)

               end

           | NONE => (snd o CodeUnit.head_func) thm;

     fun add_funcs (const, thms) =

       Graph.new_node (const, (typ_func const thms, thms));

     fun add_deps (funcs as (const, thms)) funcgr =

       let

         val deps = consts_of funcs;

         val insts = instances_of_consts thy algebra funcgr

           (fold_consts (insert (op =)) thms []);

       in

         funcgr

         |> ensure_consts' thy algebra insts

         |> fold (curry Graph.add_edge const) deps

         |> fold (curry Graph.add_edge const) insts

        end;

   in

     funcgr

     |> fold add_funcs funcss

     |> fold add_deps funcss

   end

 and ensure_consts' thy algebra cs funcgr =

   let

     val auxgr = Graph.empty

       |> fold (snd oo ensure_const thy algebra funcgr) cs;

   in

     funcgr

     |> fold (merge_funcss thy algebra)

          (map (AList.make (Graph.get_node auxgr))

          (rev (Graph.strong_conn auxgr)))

   end handle INVALID (cs', msg)

     => raise INVALID (fold (insert (op =)) cs' cs, msg);

 in

 (** retrieval interfaces **)

 fun ensure_consts thy algebra consts funcgr =

   ensure_consts' thy algebra consts funcgr

     handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "

     ^ commas (map (CodeUnit.string_of_const thy) cs'));

 fun check_consts thy consts funcgr =

   let

     val algebra = Code.coregular_algebra thy;

     fun try_const const funcgr =

       (SOME const, ensure_consts' thy algebra [const] funcgr)

       handle INVALID (cs', msg) => (NONE, funcgr);

     val (consts', funcgr') = fold_map try_const consts funcgr;

   in (map_filter I consts', funcgr') end;

 fun raw_eval thy f ct funcgr =

   let

     val algebra = Code.coregular_algebra thy;

     fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I)

       (Thm.term_of ct) [];

     val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);

     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();

     val thm1 = Code.preprocess_conv ct;

     val ct' = Thm.rhs_of thm1;

     val cs = map fst (consts_of ct');

     val funcgr' = ensure_consts thy algebra cs funcgr;

     val (_, thm2) = Thm.varifyT' [] thm1;

     val thm3 = Thm.reflexive (Thm.rhs_of thm2);

     val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3];

     val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];

     fun inst thm =

       let

         val tvars = Term.add_tvars (Thm.prop_of thm) [];

         val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy)

           (TVar (v_i, sort), TFree (v, sort))) tvars tfrees;

       in Thm.instantiate (instmap, []) thm end;

     val thm5 = inst thm2;

     val thm6 = inst thm4;

     val ct'' = Thm.rhs_of thm6;

     val c_exprs = consts_of ct'';

     val drop = drop_classes thy tfrees;

     val instdefs = instances_of_consts thy algebra funcgr' c_exprs;

     val funcgr'' = ensure_consts thy algebra instdefs funcgr';

   in (f drop thm5 funcgr'' ct'', funcgr'') end;

 fun raw_eval_conv thy conv =

   let

     fun conv' drop_classes thm1 funcgr ct =

       let

         val thm2 = conv funcgr ct;

         val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);

         val thm23 = drop_classes (Thm.transitive thm2 thm3);

       in

         Thm.transitive thm1 thm23 handle THM _ =>

           error ("could not construct proof:\n"

           ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])

       end;

   in raw_eval thy conv' end;

 fun raw_eval_term thy f t =

   let

     fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct);

   in raw_eval thy f' (Thm.cterm_of thy t) end;

 end; (*local*)

 structure Funcgr = CodeDataFun

 (

   type T = T;

   val empty = Graph.empty;

   fun merge _ _ = Graph.empty;

   fun purge _ NONE _ = Graph.empty

     | purge _ (SOME cs) funcgr =

         Graph.del_nodes ((Graph.all_preds funcgr 

           o filter (can (Graph.get_node funcgr))) cs) funcgr;

 );

 fun make thy =

   Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);

 fun make_consts thy =

   Funcgr.change_yield thy o check_consts thy;

 fun eval_conv thy f =

   fst o Funcgr.change_yield thy o raw_eval_conv thy f;

 fun eval_term thy f =

   fst o Funcgr.change_yield thy o raw_eval_term thy f;

 end; (*struct*)