(*
This module is primarily responsible for generating checks that
test if typeclass axioms hold for instances.

Axiom checks are written by the user in a form, which is effectively
a database: the user writes just

axiom_check (1,2);

for example, and every axiom which can accept two integers is
then evaluated to see if it is true. Note that an axiom check
is an ordinary executable statement, and in particular it can
be put inside a loop to dynamically generate may test cases.

This module gathers all the axioms, and attempt to specialise
each one to each test case:  this is just ordinary overloading,
except that many matches are permitted. Code to evaluate
all the matches is generated along with a diagnostic which
will explain which axiom failed on what case, if that occurs.

In passing I mention that axiom_checks found a bug in my floating
point axiom set by proving to me that floating point addition
and multiplication are not associative.
**)
open Flx_util
open Flx_ast
open Flx_types
open Flx_btype
open Flx_bexpr
open Flx_bexe
open Flx_bparameter
open Flx_bbdcl
open Flx_print
open Flx_set
open Flx_mtypes2
open Flx_typing
open List
open Flx_unify
open Flx_maps
open Flx_exceptions
open Flx_use
open Flx_typeclass

let string_of_bvs bvs =
  catmap "," (fun (s,i)->s^"<"^si i^">") bvs

let verify syms bsym_table csr e =
  let xx = ref [] in
  iter (fun (id, axsr, parent, axiom_kind, bvs, (bpl,precond), x) ->
    match x with | `BEquation _ -> () | `BPredicate x ->
    (*
    print_endline ("Checking for cases of axiom " ^ id);
    **)
    let param = match bpl with
      | [] -> bexpr_tuple (btyp_tuple []) []
      | [{pindex=i;ptyp=t}] -> bexpr_varname t (i,[])
      | ls ->
        let xs = map (fun { pindex=i; ptyp=t } -> bexpr_varname t (i,[])) ls in
        let ts = map snd xs in
        bexpr_tuple (btyp_tuple ts) xs
    in
    let tvars = map (fun (_,i) -> i) bvs in
    let evars = Flx_bparameter.get_bids bpl in
    let result = expr_maybe_matches bsym_table syms.counter tvars evars param e in
    match result with
    | None -> ()
    | Some (tmgu, emgu) ->
      (*
      print_endline (sbe sym_table e ^  " MATCHES AXIOM " ^ id);
      print_endline ("Axiom vs =" ^ string_of_bvs bvs);
      print_endline ("TMgu=" ^ string_of_varlist sym_table tmgu);
      **)
      let ok = match parent with
      | None -> true
      | Some i ->
        try
          let tc_bsym = Flx_bsym_table.find bsym_table i in
          match Flx_bsym.bbdcl tc_bsym with
          | BBDCL_typeclass (_,tcbvs) ->
            begin
              (*
              print_endline ("Axiom "^id^" is owned by typeclass " ^ tcid);
              print_endline ("Typeclass bvs=" ^ string_of_bvs tcbvs);
              **)
              let ts =
                try
                  Some (map (fun (s,i) -> assoc i tmgu) tcbvs)
                with Not_found ->
                  (*
                  print_endline "Can't instantiate typeclass vars- FAIL";
                  **)
                  None
              in
              match ts with None -> false | Some ts ->
              let insts =
                try
                  Some (Hashtbl.find syms.instances_of_typeclass i)
                with Not_found ->
                  (*
                  print_endline "Typeclass has no instances";
                  **)
                  None
              in
              match insts with | None -> false | Some insts ->
              try
                iter begin fun (instidx,(inst_bvs, inst_traint, inst_ts)) ->
                  match
                    tcinst_chk
                      syms
                      bsym_table
                      id
                      (Flx_bsym.sr tc_bsym)
                      i
                      ts
                      (inst_bvs, inst_traint, inst_ts, instidx)
                  with
                  | `CannotMatch,_,_-> ()
                  | `MaybeMatchesLater,_,_-> ()
                  | `MatchesNow,_,_ -> raise Not_found
                end insts;
                (*
                print_endline "Couldn't find instance";
                **)
                false
              with Not_found ->
                (*
                print_endline "FOUND INSTANCE";
                **)
                true
            end
          | _ -> true
        with
          Not_found ->
          (*
          print_endline "Wha .. can't find axiom's parent";
          **)
          true
      in
      if not ok then () else
      let xsub x = fold_left (fun x (i,e) -> expr_term_subst x i e) x emgu in
      let tsub t = list_subst syms.counter tmgu t in
      (*
      print_endline ("tmgu= " ^ catmap ", " (fun (i,t) -> si i ^ "->" ^ sbt sym_table t) tmgu);
      **)
      let ident x = x in
      let rec aux x = Flx_bexpr.map ~f_btype:tsub ~f_bexpr:aux x in
      let cond = aux (xsub x) in
      let precond = match precond with
      | Some x -> Some (aux (xsub x))
      | None -> None
      in
      let comment = bexe_comment (csr,"Check " ^ id) in
      let ax = bexe_axiom_check2 (csr,axsr,precond,cond) in
(*
      print_endline ("axiom_check2 : " ^ tsbe sym_table cond);
**)
      xx := ax :: comment :: !xx
  )
  !(syms.axioms)
  ;
  !xx

let fixup_exes syms bsym_table gen bexes =
  let rec aux inx outx = match inx with
  | [] -> rev outx
  | BEXE_axiom_check (sr,e) :: t ->
    (*
    print_endline ("Axiom check case "  ^ sbe sym_table e);
    **)
    if gen then
      aux t ((verify syms bsym_table sr e) @ outx)
    else aux t outx

  | h :: t -> aux t (h::outx)
  in
  aux bexes []

let axiom_check syms bsym_table gen =
  Flx_bsym_table.update_bexes (fixup_exes syms bsym_table gen) bsym_table