(* Title:  ProgLang/Program.thy

    Author: Walther Neuper, Sep.2019

    (c) due to copyright terms

 *)

 theory Program

   imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

 begin

 text \<open>Abstract:

   Theorems required by Isac's rewrite engine for evaluating assumptions of theorems/rules.

   Basic functions for Isac programs and theorems

 \<close>

 subsection \<open>General constants: TODO shift to appropriate files\<close>

 consts

   Arbfix :: "real"

   Undef :: "real"  (* WN190823 probably an outdated design for DiffApp *)

   bool_undef :: "bool"

 subsection \<open>Theorems specific for evaluation of assumptions of theorems/rules\<close>

 axiomatization where

   rle_refl:           "(n::real) <= n" and

   not_true:           "(~ True) = False" and

   not_false:          "(~ False) = True" and

   and_true:           "(a & True) = a" and

   and_false:          "(a & False) = False" and

   or_true:            "(a | True) = True" and

   or_false:           "(a | False) = a" and

   and_commute:        "(a & b) = (b & a)" and

   or_commute:         "(a | b) = (b | a)" 

 subsection \<open>TODO\<close>

 ML \<open>

 \<close> ML \<open>

 signature PROGRAM =

 sig

   type T

   datatype leaf = Expr of term | Tac of term

   val rep_stacexpr: leaf -> term

   val prep_program : thm -> term        (*ren prepare*)

   val get_fun_id: term -> string * typ  (*ren fun_id*)

   val formal_args : term -> term list

   val body_of : term -> term            (*ren body*)

   val to_string: Rule_Def.program -> string

 end

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 ML \<open>

 \<close> ML \<open>

 (**)

 structure Program(**): PROGRAM(**) =

 struct

 (**)

 type T = Rule.program

 datatype leaf = Tac of term | Expr of term

 fun rep_stacexpr (Tac t ) = t

   | rep_stacexpr (Expr t) = 

     raise ERROR ("rep_stacexpr called with t= " ^ UnparseC.term t);

 (* the lucas-interpreter LI requires programs in this specific format *)

 fun prep_program thm = (thm

   |> Thm.prop_of

   |> HOLogic.dest_Trueprop

   |> Logic.unvarify_global

   |> TermC.inst_abs)

   handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])

 (* get identifier of partial_function *)

 fun get_fun_id (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ fun_and_args $ _) =

       fun_and_args |> strip_comb |> fst |> dest_Const

   | get_fun_id t = raise TERM ("get_fun_id", [t])

 (* get the arguments of the script out of the scripts parsetree *)

 fun formal_args tm = (tm

   |> HOLogic.dest_eq

   |> fst

   |> strip_comb

   |> snd)

   handle TERM _ => raise TERM ("formal_args", [tm])

 (* get the body of a program *)

 fun body_of tm = (tm

   |> HOLogic.dest_eq

   |> snd)

   handle TERM _ => raise TERM ("body_of", [tm])

 fun to_string Rule_Def.Empty_Prog = "Empty_Prog"

   | to_string (Rule_Def.Prog s) = "Prog " ^ UnparseC.term s

   | to_string (Rule_Def.Rfuns _)  = "Rfuns";

 (**)end(**)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end