(* 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