src/HOL/Matrix_LP/Compute_Oracle/linker.ML

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(*  Title:      HOL/Matrix/Compute_Oracle/linker.ML
    Author:     Steven Obua

This module solves the problem that the computing oracle does not
instantiate polymorphic rules. By going through the PCompute
interface, all possible instantiations are resolved by compiling new
programs, if necessary. The obvious disadvantage of this approach is
that in the worst case for each new term to be rewritten, a new
program may be compiled.
*)

(*
   Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
   and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m

   Find all substitutions S such that
   a) the domain of S is tvars (t_1, ..., t_n)
   b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
      1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
      2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
*)
signature LINKER =
sig
    exception Link of string

    datatype constant = Constant of bool * string * typ
    val constant_of : term -> constant

    type instances
    type subst = Type.tyenv

    val empty : constant list -> instances
    val typ_of_constant : constant -> typ
    val add_instances : theory -> instances -> constant list -> subst list * instances
    val substs_of : instances -> subst list
    val is_polymorphic : constant -> bool
    val distinct_constants : constant list -> constant list
    val collect_consts : term list -> constant list
end

structure Linker : LINKER = struct

exception Link of string;

type subst = Type.tyenv

datatype constant = Constant of bool * string * typ
fun constant_of (Const (name, ty)) = Constant (false, name, ty)
  | constant_of (Free (name, ty)) = Constant (true, name, ty)
  | constant_of _ = raise Link "constant_of"

fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term_Ord.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))


structure Consttab = Table(type key = constant val ord = constant_ord);
structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);

fun typ_of_constant (Constant (_, _, ty)) = ty

val empty_subst = (Vartab.empty : Type.tyenv)

fun merge_subst (A:Type.tyenv) (B:Type.tyenv) =
    SOME (Vartab.fold (fn (v, t) =>
                       fn tab =>
                          (case Vartab.lookup tab v of
                               NONE => Vartab.update (v, t) tab
                             | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
    handle Type.TYPE_MATCH => NONE

fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
    (list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))) (Vartab.dest A, Vartab.dest B)

structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);

fun substtab_union c = Substtab.fold Substtab.update c
fun substtab_unions [] = Substtab.empty
  | substtab_unions [c] = c
  | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)

datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table

fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))

fun distinct_constants cs =
    Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)

fun empty cs =
    let
        val cs = distinct_constants (filter is_polymorphic cs)
        val old_cs = cs
(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (Misc_Legacy.typ_tvars ty) tab
        val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
        fun tvars_of ty = collect_tvars ty Typtab.empty
        val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs

        fun tyunion A B =
            Typtab.fold
                (fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
                A B

        fun is_essential A B =
            Typtab.fold
            (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
            A false

        fun add_minimal (c', tvs') (tvs, cs) =
            let
                val tvs = tyunion tvs' tvs
                val cs = (c', tvs')::cs
            in
                if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
                    SOME (tvs, cs)
                else
                    NONE
            end

        fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)

        fun generate_minimal_subsets subsets [] = subsets
          | generate_minimal_subsets subsets (c::cs) =
            let
                val subsets' = map_filter (add_minimal c) subsets
            in
                generate_minimal_subsets (subsets@subsets') cs
            end*)

        val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)

        val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)

    in
        Instances (
        fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
        Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants),
        minimal_subsets, Substtab.empty)
    end

local
fun calc ctab substtab [] = substtab
  | calc ctab substtab (c::cs) =
    let
        val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
        fun merge_substs substtab subst =
            Substtab.fold (fn (s,_) =>
                           fn tab =>
                              (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
                          substtab Substtab.empty
        val substtab = substtab_unions (map (merge_substs substtab) csubsts)
    in
        calc ctab substtab cs
    end
in
fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
end

fun add_instances thy (Instances (cfilter, ctab,minsets,substs)) cs =
    let
(*      val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
        fun calc_instantiations (constant as Constant (free, name, ty)) instantiations =
            Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>
                           fn instantiations =>
                              if free <> free' orelse name <> name' then
                                  instantiations
                              else case Consttab.lookup insttab constant of
                                       SOME _ => instantiations
                                     | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
                                                handle Type.TYPE_MATCH => instantiations))
                          ctab instantiations
        val instantiations = fold calc_instantiations cs []
        (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
        fun update_ctab (constant', entry) ctab =
            (case Consttab.lookup ctab constant' of
                 NONE => raise Link "internal error: update_ctab"
               | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
        val ctab = fold update_ctab instantiations ctab
        val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs)
                              minsets Substtab.empty
        val (added_substs, substs) =
            Substtab.fold (fn (ns, _) =>
                           fn (added, substtab) =>
                              (case Substtab.lookup substs ns of
                                   NONE => (ns::added, Substtab.update (ns, ()) substtab)
                                 | SOME () => (added, substtab)))
                          new_substs ([], substs)
    in
        (added_substs, Instances (cfilter, ctab, minsets, substs))
    end

fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs


local

fun collect (Var _) tab = tab
  | collect (Bound _) tab = tab
  | collect (a $ b) tab = collect b (collect a tab)
  | collect (Abs (_, _, body)) tab = collect body tab
  | collect t tab = Consttab.update (constant_of t, ()) tab

in
  fun collect_consts tms = Consttab.keys (fold collect tms Consttab.empty)
end

end

signature PCOMPUTE =
sig
    type pcomputer

    val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
    val make_with_cache : Compute.machine -> theory -> term list -> thm list -> Linker.constant list -> pcomputer
    
    val add_instances : pcomputer -> Linker.constant list -> bool 
    val add_instances' : pcomputer -> term list -> bool

    val rewrite : pcomputer -> cterm list -> thm list
    val simplify : pcomputer -> Compute.theorem -> thm

    val make_theorem : pcomputer -> thm -> string list -> Compute.theorem
    val instantiate : pcomputer -> (string * cterm) list -> Compute.theorem -> Compute.theorem
    val evaluate_prem : pcomputer -> int -> Compute.theorem -> Compute.theorem
    val modus_ponens : pcomputer -> int -> thm -> Compute.theorem -> Compute.theorem 

end

structure PCompute : PCOMPUTE = struct

exception PCompute of string

datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list

datatype pcomputer =
  PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
    pattern list Unsynchronized.ref 

(*fun collect_consts (Var x) = []
  | collect_consts (Bound _) = []
  | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
  | collect_consts (Abs (_, _, body)) = collect_consts body
  | collect_consts t = [Linker.constant_of t]*)

fun computer_of (PComputer (_,computer,_,_)) = computer

fun collect_consts_of_thm th = 
    let
        val th = prop_of th
        val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th)
        val (left, right) = Logic.dest_equals th
    in
        (Linker.collect_consts [left], Linker.collect_consts (right::prems))
    end

fun create_theorem th =
let
    val (left, right) = collect_consts_of_thm th
    val polycs = filter Linker.is_polymorphic left
    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (Misc_Legacy.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
    fun check_const (c::cs) cs' =
        let
            val tvars = Misc_Legacy.typ_tvars (Linker.typ_of_constant c)
            val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
        in
            if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
            else
                if null (tvars) then
                    check_const cs (c::cs')
                else
                    check_const cs cs'
        end
      | check_const [] cs' = cs'
    val monocs = check_const right []
in
    if null (polycs) then
        (monocs, MonoThm th)
    else
        (monocs, PolyThm (th, Linker.empty polycs, []))
end

fun create_pattern pat = 
let
    val cs = Linker.collect_consts [pat]
    val polycs = filter Linker.is_polymorphic cs
in
    if null (polycs) then
        MonoPattern pat
    else
        PolyPattern (pat, Linker.empty polycs, [])
end
             
fun create_computer machine thy pats ths =
    let
        fun add (MonoThm th) ths = th::ths
          | add (PolyThm (_, _, ths')) ths = ths'@ths
        fun addpat (MonoPattern p) pats = p::pats
          | addpat (PolyPattern (_, _, ps)) pats = ps@pats
        val ths = fold_rev add ths []
        val pats = fold_rev addpat pats []
    in
        Compute.make_with_cache machine thy pats ths
    end

fun update_computer computer pats ths = 
    let
        fun add (MonoThm th) ths = th::ths
          | add (PolyThm (_, _, ths')) ths = ths'@ths
        fun addpat (MonoPattern p) pats = p::pats
          | addpat (PolyPattern (_, _, ps)) pats = ps@pats
        val ths = fold_rev add ths []
        val pats = fold_rev addpat pats []
    in
        Compute.update_with_cache computer pats ths
    end

fun conv_subst thy (subst : Type.tyenv) =
    map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst)

fun add_monos thy monocs pats ths =
    let
        val changed = Unsynchronized.ref false
        fun add monocs (th as (MonoThm _)) = ([], th)
          | add monocs (PolyThm (th, instances, instanceths)) =
            let
                val (newsubsts, instances) = Linker.add_instances thy instances monocs
                val _ = if not (null newsubsts) then changed := true else ()
                val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
(*              val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
                val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
            in
                (newmonos, PolyThm (th, instances, instanceths@newths))
            end
        fun addpats monocs (pat as (MonoPattern _)) = pat
          | addpats monocs (PolyPattern (p, instances, instancepats)) =
            let
                val (newsubsts, instances) = Linker.add_instances thy instances monocs
                val _ = if not (null newsubsts) then changed := true else ()
                val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
            in
                PolyPattern (p, instances, instancepats@newpats)
            end 
        fun step monocs ths =
            fold_rev (fn th =>
                      fn (newmonos, ths) =>
                         let 
                             val (newmonos', th') = add monocs th 
                         in
                             (newmonos'@newmonos, th'::ths)
                         end)
                     ths ([], [])
        fun loop monocs pats ths =
            let 
                val (monocs', ths') = step monocs ths 
                val pats' = map (addpats monocs) pats
            in
                if null (monocs') then
                    (pats', ths')
                else
                    loop monocs' pats' ths'
            end
        val result = loop monocs pats ths
    in
        (!changed, result)
    end

datatype cthm = ComputeThm of term list * sort list * term

fun thm2cthm th =
    let
        val {hyps, prop, shyps, ...} = Thm.rep_thm th
    in
        ComputeThm (hyps, shyps, prop)
    end

val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord

fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))

structure CThmtab = Table(type key = cthm val ord = cthm_ord)

fun remove_duplicates ths =
    let
        val counter = Unsynchronized.ref 0
        val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
        val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
        fun update th =
            let
                val key = thm2cthm th
            in
                case CThmtab.lookup (!tab) key of
                    NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
                  | _ => ()
            end
        val _ = map update ths
    in
        map snd (Inttab.dest (!thstab))
    end

fun make_with_cache machine thy pats ths cs =
    let
        val ths = remove_duplicates ths
        val (monocs, ths) = fold_rev (fn th => 
                                      fn (monocs, ths) => 
                                         let val (m, t) = create_theorem th in 
                                             (m@monocs, t::ths)
                                         end)
                                     ths (cs, [])
        val pats = map create_pattern pats
        val (_, (pats, ths)) = add_monos thy monocs pats ths
        val computer = create_computer machine thy pats ths
    in
        PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
    end

fun make machine thy ths cs = make_with_cache machine thy [] ths cs

fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = 
    let
        val thy = Theory.deref thyref
        val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths)
    in
        if changed then
            (update_computer computer pats ths;
             rths := ths;
             rpats := pats;
             true)
        else
            false

    end

fun add_instances' pc ts = add_instances pc (Linker.collect_consts ts)

fun rewrite pc cts =
    let
        val _ = add_instances' pc (map term_of cts)
        val computer = (computer_of pc)
    in
        map (fn ct => Compute.rewrite computer ct) cts
    end

fun simplify pc th = Compute.simplify (computer_of pc) th

fun make_theorem pc th vars = 
    let
        val _ = add_instances' pc [prop_of th]

    in
        Compute.make_theorem (computer_of pc) th vars
    end

fun instantiate pc insts th = 
    let
        val _ = add_instances' pc (map (term_of o snd) insts)
    in
        Compute.instantiate (computer_of pc) insts th
    end

fun evaluate_prem pc prem_no th = Compute.evaluate_prem (computer_of pc) prem_no th

fun modus_ponens pc prem_no th' th =
    let
        val _ = add_instances' pc [prop_of th']
    in
        Compute.modus_ponens (computer_of pc) prem_no th' th
    end    
                                                                                                    

end