(* auxiliary functions used in scripts

   author: Walther Neuper 000301

   WN0509 shift into Atools ?!? (because used also in where of models !)

   (c) copyright due to lincense terms.

*)

theory Tools imports ListC begin

(*belongs to theory ListC*)

ML {*

val first_isac_thy = @{theory ListC}

*}

(*for Descript.thy*)

  (***********************************************************************)

  (* 'fun is_dsc' in ProgLang/scrtools.smlMUST contain ALL these types !!*)

  (***********************************************************************)

typedecl nam     (* named variables                                             *)

typedecl  una     (* unnamed variables                                           *)

typedecl  unl     (* unnamed variables of type list, elementwise input prohibited*)

typedecl  str     (* structured variables                                        *)

typedecl  toreal  (* var with undef real value: forces typing                    *)

typedecl  toreall (* var with undef real list value: forces typing               *)

typedecl  tobooll (* var with undef bool list value: forces typing               *)

typedecl  unknow  (* input without dsc in fmz=[]                                 *)

typedecl  cpy     (* UNUSED: copy-named variables

             identified by .._0, .._i .._' in pbt                        *)

  (***********************************************************************)

  (* 'fun is_dsc' in ProgLang/scrtools.smlMUST contain ALL these types !!*)

  (***********************************************************************)

consts

  UniversalList   :: "bool list"

  lhs             :: "bool => real"           (*of an equality*)

  rhs             :: "bool => real"           (*of an equality*)

  Vars            :: "'a => real list"        (*get the variables of a term *)

  matches         :: "['a, 'a] => bool"

  matchsub        :: "['a, 'a] => bool"

(*

constdefs

  Testvar   :: "[real, 'a] => bool"  (*is a variable in a term: unused 6.5.03*)

 "Testvar v t == v mem (Vars t)"     (*by rewriting only,no Calcunused 6.5.03*)

*)

ML {* (*the former Tools.ML*)

(* auxiliary functions for scripts  WN.9.00*)

(*11.02: for equation solving only*)

val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";

val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";     

(*+ for Or_to_List +*)

fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)

  | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)

  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = 

    (tracing"### or2list _ = _"; TermC.list2isalist TermC.bool [t])

  | or2list ors =

    (tracing"### or2list _ | _";

    let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =

	    case o2 of

		Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2

	      | _ => ls @ [o1, o2] 

    in (((TermC.list2isalist TermC.bool) o (get [])) ors)

       handle _ => error ("or2list: no ORs= "^(term2str ors)) end

	);

(*>val t = @{term True};

> val t' = or2list t;

> term2str t';

"Atools.UniversalList"

> val t = @{term False};

> val t' = or2list t;

> term2str t';

"[]"

> val t=(Thm.term_of o the o (parse thy)) "x=3";

> val t' = or2list t;

> term2str t';

"[x = 3]"

> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";

> val t' = or2list t;

> term2str t';

"[x = #3, x = #-3, x = #0]" : string *)

(** evaluation on the meta-level **)

(*. evaluate the predicate matches (match on whole term only) .*)

(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)

fun eval_matches (thmid:string) "Tools.matches"

		  (t as Const ("Tools.matches",_) $ pat $ tst) thy = 

    if TermC.matches thy tst pat

    then 

      let

        val prop = TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))

	    in SOME (term_to_string''' thy prop, prop) end

    else 

      let 

        val prop = TermC.Trueprop $ (TermC.mk_equality (t, @{term False}))

	    in SOME (term_to_string''' thy prop, prop) end

  | eval_matches _ _ _ _ = NONE; 

(*

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?x = 0) (1 * x ^^^ 2 = 0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  

----- before ?patterns ---:

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME

    ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",

     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

  : (string * term) option 

> val t = (Thm.term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",

     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

> val t = (Thm.term_of o the o (parse thy)) 

               "matches (a = b) (x + #1 + #-1 * #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))

*)

(*.does a pattern match some subterm ?.*)

fun matchsub thy t pat =  

  let

    fun matchs (t as Const _) = TermC.matches thy t pat

	      | matchs (t as Free _) = TermC.matches thy t pat

	      | matchs (t as Var _) = TermC.matches thy t pat

	      | matchs (Bound _) = false

	      | matchs (t as Abs (_, _, body)) = 

	          if TermC.matches thy t pat then true else TermC.matches thy body pat

	      | matchs (t as f1 $ f2) =

	          if TermC.matches thy t pat then true 

	            else if matchs f1 then true else matchs f2

  in matchs t end;

(*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)

fun eval_matchsub (thmid:string) "Tools.matchsub"

		  (t as Const ("Tools.matchsub",_) $ pat $ tst) thy = 

    if matchsub thy tst pat

    then 

      let val prop = TermC.Trueprop $ (TermC.mk_equality (t, @{term True}))

      in SOME (term_to_string''' thy prop, prop) end

    else 

      let val prop = TermC.Trueprop $ (TermC.mk_equality (t, @{term False}))

      in SOME (term_to_string''' thy prop, prop) end

  | eval_matchsub _ _ _ _ = NONE; 

(*get the variables in an isabelle-term*)

(*("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")):calc*)

fun eval_var (thmid:string) "Tools.Vars" (t as (Const(op0,t0) $ arg)) thy = 

    let 

      val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;

      val thmId = thmid ^ term_to_string''' thy arg;

    in SOME (thmId, TermC.Trueprop $ (TermC.mk_equality (t, t'))) end

  | eval_var _ _ _ _ = NONE;

fun lhs (Const ("HOL.eq",_) $ l $ _) = l

  | lhs t = error("lhs called with (" ^ term2str t ^ ")");

(*("lhs"    ,("Tools.lhs"    ,eval_lhs "")):calc*)

fun eval_lhs _ "Tools.lhs"

	     (t as (Const ("Tools.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ = 

    SOME ((term2str t) ^ " = " ^ (term2str l),

	  TermC.Trueprop $ (TermC.mk_equality (t, l)))

  | eval_lhs _ _ _ _ = NONE;

(*

> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";

> val SOME (id,t') = eval_lhs 0 0 t 0;

val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

> term2str t';

val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

*)

fun rhs (Const ("HOL.eq",_) $ _ $ r) = r

  | rhs t = error("rhs called with (" ^ term2str t ^ ")");

(*("rhs"    ,("Tools.rhs"    ,eval_rhs "")):calc*)

fun eval_rhs _ "Tools.rhs"

	     (t as (Const ("Tools.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ = 

    SOME ((term2str t) ^ " = " ^ (term2str r),

	  TermC.Trueprop $ (TermC.mk_equality (t, r)))

  | eval_rhs _ _ _ _ = NONE;

(*for evaluating scripts*) 

val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")];

*}

setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}

setup {* KEStore_Elems.add_calcs

  [("matches", ("Tools.matches", eval_matches "#matches_")),

    ("matchsub", ("Tools.matchsub", eval_matchsub "#matchsub_")),

    ("Vars", ("Tools.Vars", eval_var "#Vars_")),

    ("lhs", ("Tools.lhs", eval_lhs "")),

    ("rhs", ("Tools.rhs", eval_rhs ""))] *}

end