(*
places:
  goal, assumption list, input box with prompts, proof text, search results


*)

(*
theorem searching -n NAME, -o omit, -r rewrite format, -s sort by length, -
save search history and selected results., 

*)

(* Jordan from: 
    eventually merge...  *)

let rec type_set: (string*term) list  -> (term list*term) -> (term list*term)=
  fun tinfo (acclist,utm) -> match acclist with
    | [] -> (acclist,utm)
    | (Var(s,_) as a)::rest ->
         let a' = (assocd s tinfo a) in
           if (a = a') then type_set tinfo (rest,utm)
           else let inst = instantiate (term_match [] a a') in
             type_set tinfo ((map inst rest),inst utm)
    | _ -> failwith "type_set: variable expected"
  ;;

let has_stv t =
  let typ = (type_vars_in_term t) in
  can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;

let typeinfo (asl,w) =   
  let freel = itlist (union o frees o concl o snd) asl (frees w) in
  let pairup  = (function
		   |Var(s,_) as t -> (s,t) 
		   | _ -> failwith "typeinfo: unreachable state" ) in
  map pairup freel;;

let set_types_from_goal (asl,w)  =
  let set_types tinfo t = snd (type_set tinfo ((frees t),t)) in
    set_types (typeinfo(asl,w));;

let TYPE_THEN: term  -> (term -> tactic) -> tactic =
  fun t tac (asl,w) ->
  let t' = set_types_from_goal(asl,w) t in
    (warn ((has_stv t')) "TYPE_THEN: unresolved type variables");
    tac t' (asl,w);;

let TYPEL_THEN: term list -> (term list -> tactic) -> tactic =
  fun t tac (asl,w) ->
  let t' = map (set_types_from_goal(asl,w)) t in 
    (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars");
     tac t' (asl,w);;

help "ABBREV_TAC";;
(* hightlight term, typeover abbrev *)
let MK_ABBREV_TAC: term -> string -> goal -> goalstate = 
  fun oldtext abbrev (asl,w) ->
    let text = set_types_from_goal (asl,w) oldtext in
  let abbrev' = mk_var(abbrev,(type_of text)) in
   ABBREV_TAC (mk_eq (abbrev', text)) (asl,w);;

help "ABS_TAC";;
(* delete the lambda, or the bound variable *)

help "ACCEPT_TAC";; (* ignore for now *)

help "ALL_TAC";; (* ignore for now *)

help "ANTE_RES_THEN";; (* ignore for now *)

help "ANTS_TAC";;  (* delete ant of ant, subgoal button *)

help "AP_TERM_TAC";;  (* delete f in f x = f y, either first or second instance *)

help "AP_THM_TAC";;  (* delete x in f x = g x, either first or second *)

help "ARITH_TAC";;  (* terminator, try if it is an arithmetic expression. *)

help "ASM_CASES_TAC";;  (* needs a term u to split *)

help "ASM_FOL_TAC";; (* ignore forever *)

help "ASM_MESON_TAC";; (* terminator , option -a on MESON_TAC *)

help "ASM_REWRITE_TAC";; (* option -a on REWRITE_TAC *)

help "ASM_SIMP_TAC";; (* option -a on SIMP_TAC *)

help "ASSUME_TAC";; (* needs theorem *)

help "BETA_TAC";; (* delete lambda *)