src/HOL/Modelcheck/mucke_oracle.ML
author wenzelm
Fri, 17 Jun 2005 18:33:14 +0200
changeset 16429 e871f4b1a4f0
parent 16258 f3d913abf7e5
child 16486 1a12cdb6ee6b
permissions -rw-r--r--
replaced obsolete theory_of_sign by theory_of_thm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16152
7294283b0c45 no_tac;
wenzelm
parents: 15574
diff changeset
     1
7294283b0c45 no_tac;
wenzelm
parents: 15574
diff changeset
     2
(* $Id$ *)
7294283b0c45 no_tac;
wenzelm
parents: 15574
diff changeset
     3
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
     4
exception MuckeOracleExn of term;
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
     5
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
     6
val trace_mc = ref false; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
     7
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
     8
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
     9
(* transform_case post-processes output strings of the syntax "Mucke" *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    10
(* with respect to the syntax of the case construct                   *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    11
local
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    12
  fun extract_argument [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    13
  | extract_argument ("*"::_) = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    14
  | extract_argument (x::xs) = x::(extract_argument xs);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    15
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    16
  fun cut_argument [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    17
  | cut_argument ("*"::r) = r
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    18
  | cut_argument (_::xs) = cut_argument xs;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    19
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    20
  fun insert_case_argument [] s = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    21
  | insert_case_argument ("*"::"="::xl) (x::xs) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    22
         (explode(x)@(" "::"="::(insert_case_argument xl (x::xs))))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    23
  | insert_case_argument ("c"::"a"::"s"::"e"::"*"::xl) s =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    24
        (let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    25
        val arg=implode(extract_argument xl);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    26
        val xr=cut_argument xl
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    27
        in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    28
         "c"::"a"::"s"::"e"::" "::(insert_case_argument xr (arg::s))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    29
        end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    30
  | insert_case_argument ("e"::"s"::"a"::"c"::"*"::xl) (x::xs) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    31
        "e"::"s"::"a"::"c"::(insert_case_argument xl xs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    32
  | insert_case_argument (x::xl) s = x::(insert_case_argument xl s);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    33
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    34
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    35
fun transform_case s = implode(insert_case_argument (explode s) []);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    36
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    37
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    38
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    39
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    40
(* if_full_simp_tac is a tactic for rewriting non-boolean ifs *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    41
local
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    42
  (* searching an if-term as below as possible *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    43
  fun contains_if (Abs(a,T,t)) = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    44
  contains_if (Const("If",T) $ b $ a1 $ a2) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    45
  let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    46
  fun tn (Type(s,_)) = s |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    47
  tn _ = error "cannot master type variables in if term";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    48
  val s = tn(body_type T);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    49
  in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    50
  if (s="bool") then [] else [b,a1,a2]
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    51
  end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    52
  contains_if (a $ b) = if ((contains_if b)=[]) then (contains_if a)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    53
		        else (contains_if b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    54
  contains_if _ = [];
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    55
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    56
  fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(variant_abs(a,T,t))) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    57
  find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    58
  (if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    59
  else (a $ b,contains_if(a $ b))|
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    60
  find_replace_term t = (t,[]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    61
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    62
  fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    63
  if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    64
  if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    65
		        else (a$(if_substi b t)) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    66
  if_substi t v = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    67
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    68
  fun deliver_term (t,[]) = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    69
  deliver_term (t,[b,a1,a2]) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    70
  [
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    71
  Const("Trueprop",Type("fun",[Type("bool",[]),Type("prop",[])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    72
  (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    73
Const("op =",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    74
  $ t $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    75
  (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    76
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    77
  $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    78
  (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    79
Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    80
  $ b $ (if_substi t a1))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    81
  $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    82
  (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    83
Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    84
  $ (Const("Not",Type("fun",[Type("bool",[]),Type("bool",[])])) $ b) $ (if_substi t a2))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    85
  ))] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    86
  deliver_term _ =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    87
  error "tactic failed due to occurence of malformed if-term" (* shouldnt occur *);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    88
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    89
  fun search_if (*((Const("==",_)) $ _ $*) (a) = deliver_term(find_replace_term a);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    90
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    91
  fun search_ifs [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    92
  search_ifs (a::r) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    93
  let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    94
  val i = search_if a
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    95
  in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    96
  if (i=[]) then (search_ifs r) else i
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    97
  end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    98
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
    99
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   100
fun if_full_simp_tac sset i state =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   101
let val sign = #sign (rep_thm state);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   102
        val (subgoal::_) = Library.drop(i-1,prems_of state);
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   103
        val prems = Logic.strip_imp_prems subgoal;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   104
	val concl = Logic.strip_imp_concl subgoal;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   105
	val prems = prems @ [concl];
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   106
        val itrm = search_ifs prems;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   107
in
16152
7294283b0c45 no_tac;
wenzelm
parents: 15574
diff changeset
   108
if (itrm = []) then no_tac state else
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   109
(
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   110
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   111
val trm = hd(itrm)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   112
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   113
(
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   114
push_proof();
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   115
goalw_cterm [] (cterm_of sign trm);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   116
by (simp_tac (simpset()) 1);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   117
        let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   118
        val if_tmp_result = result()
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   119
        in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   120
        (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   121
        pop_proof();
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   122
        CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   123
        end
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   124
)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   125
end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   126
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   127
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   128
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   129
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   130
(********************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   131
(* All following stuff serves for defining mk_mc_oracle *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   132
(********************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   133
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   134
(***************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   135
(* SECTION 0: some auxiliary functions *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   136
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   137
fun list_contains_key [] _ = false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   138
list_contains_key ((a,l)::r) t = if (a=t) then true else (list_contains_key r t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   139
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   140
fun search_in_keylist [] _ = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   141
search_in_keylist ((a,l)::r) t = if (a=t) then l else (search_in_keylist r t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   142
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   143
(* delivers the part of a qualified type/const-name after the last dot *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   144
fun post_last_dot str =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   145
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   146
fun fl [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   147
fl (a::r) = if (a=".") then [] else (a::(fl r));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   148
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   149
implode(rev(fl(rev(explode str))))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   150
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   151
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   152
(* OUTPUT - relevant *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   153
(* converts type to string by a mucke-suitable convention *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   154
fun type_to_string_OUTPUT (Type(a,[])) = post_last_dot a |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   155
type_to_string_OUTPUT (Type("*",[a,b])) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   156
         "P_" ^ (type_to_string_OUTPUT a) ^ "_AI_" ^ (type_to_string_OUTPUT b) ^ "_R" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   157
type_to_string_OUTPUT (Type(a,l)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   158
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   159
fun ts_to_string [] = "" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   160
ts_to_string (a::[]) = type_to_string_OUTPUT a |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   161
ts_to_string (a::l) = (type_to_string_OUTPUT a) ^ "_I_" ^ (ts_to_string l);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   162
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   163
(post_last_dot a) ^ "_A_" ^ (ts_to_string l) ^ "_C"
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   164
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   165
type_to_string_OUTPUT _ =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   166
error "unexpected type variable in type_to_string";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   167
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   168
(* delivers type of a term *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   169
fun type_of_term (Const(_,t)) = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   170
type_of_term (Free(_,t)) = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   171
type_of_term (Var(_,t)) = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   172
type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(variant_abs(x,t,trm)))]) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   173
type_of_term (a $ b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   174
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   175
 fun accept_fun_type (Type("fun",[x,y])) = (x,y) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   176
 accept_fun_type _ =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   177
 error "no function type returned, where it was expected (in type_of_term)";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   178
 val (x,y) = accept_fun_type(type_of_term a)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   179
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   180
y
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   181
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   182
type_of_term _ = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   183
error "unexpected bound variable when calculating type of a term (in type_of_term)";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   184
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   185
(* makes list [a1..an] and ty to type an -> .. -> a1 -> ty *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   186
fun fun_type_of [] ty = ty |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   187
fun_type_of (a::r) ty = fun_type_of r (Type("fun",[a,ty]));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   188
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   189
(* creates a constructor term from constructor and its argument terms *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   190
fun con_term_of t [] = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   191
con_term_of t (a::r) = con_term_of (t $ a) r;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   192
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   193
(* creates list of constructor terms *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   194
fun con_term_list_of trm [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   195
con_term_list_of trm (a::r) = (con_term_of trm a)::(con_term_list_of trm r);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   196
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   197
(* list multiplication *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   198
fun multiply_element a [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   199
multiply_element a (l::r) = (a::l)::(multiply_element a r);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   200
fun multiply_list [] l = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   201
multiply_list (a::r) l = (multiply_element a l)@(multiply_list r l);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   202
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   203
(* To a list of types, delivers all lists of proper argument terms; tl has to *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   204
(* be a preprocessed type list with element type: (type,[(string,[type])])    *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   205
fun arglist_of sg tl [] = [[]] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   206
arglist_of sg tl (a::r) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   207
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   208
fun ispair (Type("*",x::y::[])) = (true,(x,y)) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   209
ispair x = (false,(x,x));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   210
val erg =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   211
(if (fst(ispair a))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   212
 then (let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   213
        val (x,y) = snd(ispair a)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   214
       in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   215
        con_term_list_of (Const("pair",Type("fun",[x,Type("fun",[y,a])])))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   216
			 (arglist_of sg tl [x,y])
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   217
       end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   218
 else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   219
 (let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   220
  fun deliver_erg sg tl _ [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   221
  deliver_erg sg tl typ ((c,tyl)::r) = let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   222
                        val ft = fun_type_of (rev tyl) typ;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   223
                        val trm = #t(rep_cterm(read_cterm sg (c,ft)));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   224
                        in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   225
                        (con_term_list_of trm (arglist_of sg tl tyl))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   226
			@(deliver_erg sg tl typ r)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   227
                        end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   228
  val cl = search_in_keylist tl a;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   229
  in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   230
  deliver_erg sg tl a cl
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   231
  end))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   232
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   233
multiply_list erg (arglist_of sg tl r)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   234
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   235
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   236
(*******************************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   237
(* SECTION 1: Robert Sandner's source was improved and extended by *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   238
(* generation of function declarations                             *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   239
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   240
fun dest_Abs (Abs s_T_t) = s_T_t
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   241
  | dest_Abs t = raise TERM("dest_Abs", [t]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   242
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   243
(*
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   244
fun force_Abs (Abs s_T_t) = Abs s_T_t
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   245
  | force_Abs t = Abs("x", hd(fst(strip_type (type_of t))),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   246
		      (incr_boundvars 1 t) $ (Bound 0));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   247
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   248
fun etaexp_dest_Abs t = dest_Abs (force_Abs t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   249
*)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   250
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   251
(* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   252
   and thm.instantiate *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   253
fun freeze_thaw t =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   254
  let val used = add_term_names (t, [])
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   255
          and vars = term_vars t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   256
      fun newName (Var(ix,_), (pairs,used)) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   257
          let val v = variant used (string_of_indexname ix)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   258
          in  ((ix,v)::pairs, v::used)  end;
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   259
      val (alist, _) = foldr newName ([], used) vars;
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   260
      fun mk_inst (Var(v,T)) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   261
          (Var(v,T),
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   262
           Free(valOf (assoc(alist,v)), T));
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   263
      val insts = map mk_inst vars;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   264
  in subst_atomic insts t end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   265
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   266
fun make_fun_type (a::b::l) = Type("fun",a::(make_fun_type (b::l))::[]) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   267
  | make_fun_type (a::l) = a;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   268
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   269
fun make_decl muckeType id isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   270
  let val constMuckeType = Const(muckeType,isaType);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   271
      val constId = Const(id,isaType);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   272
      val constDecl = Const("_decl", make_fun_type [isaType,isaType,isaType]); 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   273
  in (constDecl $ constMuckeType) $ constId end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   274
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   275
fun make_MuTerm muDeclTerm ParamDeclTerm muTerm isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   276
  let val constMu = Const("_mu",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   277
			  make_fun_type [isaType,isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   278
      val t1 = constMu $ muDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   279
      val t2 = t1 $ ParamDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   280
      val t3 = t2 $  muTerm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   281
  in t3 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   282
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   283
fun make_MuDecl muDeclTerm ParamDeclTerm isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   284
  let val constMu = Const("_mudec",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   285
                          make_fun_type [isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   286
      val t1 = constMu $ muDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   287
      val t2 = t1 $ ParamDeclTerm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   288
  in t2 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   289
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   290
fun make_NuTerm muDeclTerm ParamDeclTerm muTerm isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   291
  let val constMu = Const("_nu",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   292
                          make_fun_type [isaType,isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   293
      val t1 = constMu $ muDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   294
      val t2 = t1 $ ParamDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   295
      val t3 = t2 $  muTerm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   296
  in t3 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   297
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   298
fun make_NuDecl muDeclTerm ParamDeclTerm isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   299
  let val constMu = Const("_nudec",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   300
                          make_fun_type [isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   301
      val t1 = constMu $ muDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   302
      val t2 = t1 $ ParamDeclTerm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   303
  in t2 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   304
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   305
fun is_mudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.mu",_)) $ t2)) = true
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   306
  | is_mudef _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   307
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   308
fun is_nudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.nu",_)) $ t2)) = true
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   309
  | is_nudef _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   310
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   311
fun make_decls sign Dtype (Const(str,tp)::n::Clist) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   312
    let val const_decls = Const("_decls",make_fun_type [Dtype,Dtype,Dtype]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   313
        val decl = make_decl (type_to_string_OUTPUT tp) str Dtype;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   314
    in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   315
    ((const_decls $ decl) $ (make_decls sign Dtype (n::Clist)))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   316
    end
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   317
  | make_decls sign Dtype [Const(str,tp)] = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   318
      make_decl (type_to_string_OUTPUT tp) str Dtype;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   319
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   320
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   321
(* make_mu_def transforms an Isabelle Mu-Definition into Mucke format
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   322
   Takes equation of the form f = Mu Q. % x. t *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   323
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   324
fun dest_atom (Const t) = dest_Const (Const t)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   325
  | dest_atom (Free t)  = dest_Free (Free t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   326
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   327
fun get_decls sign Clist (Abs(s,tp,trm)) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   328
    let val VarAbs = variant_abs(s,tp,trm);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   329
    in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   330
    end
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   331
  | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   332
  | get_decls sign Clist trm = (Clist,trm);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   333
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   334
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   335
  let 	val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   336
	val MuType = Type("bool",[]); (* always ResType of mu, also serves
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   337
					 as dummy type *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   338
	val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   339
  	val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   340
	val PConsts = rev PCon_LHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   341
	val muDeclTerm = make_decl "bool" LHSStr MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   342
	val PDeclsTerm = make_decls sign MuType PConsts;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   343
	val MuDefTerm = make_MuTerm muDeclTerm PDeclsTerm MMuTerm MuType;		
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   344
  in MuDefTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   345
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   346
fun make_mu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   347
  let   val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   348
        val MuType = Type("bool",[]); (* always ResType of mu, also serves
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   349
                                         as dummy type *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   350
        val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   351
        val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   352
        val PConsts = rev PCon_LHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   353
        val muDeclTerm = make_decl "bool" LHSStr MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   354
        val PDeclsTerm = make_decls sign MuType PConsts;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   355
        val MuDeclTerm = make_MuDecl muDeclTerm PDeclsTerm MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   356
  in MuDeclTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   357
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   358
fun make_nu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   359
  let   val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   360
        val MuType = Type("bool",[]); (* always ResType of mu, also serves
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   361
                                         as dummy type *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   362
        val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   363
        val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   364
        val PConsts = rev PCon_LHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   365
        val muDeclTerm = make_decl "bool" LHSStr MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   366
        val PDeclsTerm = make_decls sign MuType PConsts;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   367
        val NuDefTerm = make_NuTerm muDeclTerm PDeclsTerm MMuTerm MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   368
  in NuDefTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   369
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   370
fun make_nu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   371
  let   val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   372
        val MuType = Type("bool",[]); (* always ResType of mu, also serves
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   373
                                         as dummy type *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   374
        val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   375
        val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   376
        val PConsts = rev PCon_LHS; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   377
        val muDeclTerm = make_decl "bool" LHSStr MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   378
        val PDeclsTerm = make_decls sign MuType PConsts; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   379
        val NuDeclTerm = make_NuDecl muDeclTerm PDeclsTerm MuType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   380
  in NuDeclTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   381
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   382
fun make_FunMuckeTerm FunDeclTerm ParamDeclTerm Term isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   383
  let 	val constFun = Const("_fun",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   384
			    make_fun_type [isaType,isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   385
      	val t1 = constFun $ FunDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   386
      	val t2 = t1 $ ParamDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   387
      	val t3 = t2 $  Term
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   388
  in t3 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   389
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   390
fun make_FunMuckeDecl FunDeclTerm ParamDeclTerm isaType =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   391
  let   val constFun = Const("_dec",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   392
                            make_fun_type [isaType,isaType,isaType]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   393
      val t1 = constFun $ FunDeclTerm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   394
      val t2 = t1 $ ParamDeclTerm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   395
  in t2 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   396
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   397
fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   398
is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   399
| is_fundef _ = false; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   400
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   401
fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   402
  let 	(* fun dest_atom (Const t) = dest_Const (Const t)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   403
          | dest_atom (Free t)  = dest_Free (Free t); *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   404
	val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   405
	val LHSResType = body_type(snd(dest_atom LHS));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   406
	val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   407
(*	val (_,AbsType,RawTerm) = dest_Abs(RHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   408
*)	val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   409
	val Consts_LHS = rev Consts_LHS_rev;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   410
	val PDeclsTerm = make_decls sign LHSResType Consts_LHS; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   411
		(* Boolean functions only, list necessary in general *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   412
	val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   413
	val MuckeDefTerm = make_FunMuckeTerm DeclTerm PDeclsTerm Free_RHS
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   414
					 LHSResType;	
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   415
  in MuckeDefTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   416
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   417
fun make_mucke_fun_decl sign ((_ $ LHS) $ RHS) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   418
  let   (* fun dest_atom (Const t) = dest_Const (Const t)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   419
          | dest_atom (Free t)  = dest_Free (Free t); *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   420
        val LHSStr = fst (dest_atom LHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   421
	val LHSResType = body_type(snd(dest_atom LHS));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   422
        val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   423
(*      val (_,AbsType,RawTerm) = dest_Abs(RHS);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   424
*)      val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   425
        val Consts_LHS = rev Consts_LHS_rev;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   426
        val PDeclsTerm = make_decls sign LHSResType Consts_LHS;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   427
                (* Boolean functions only, list necessary in general *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   428
        val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   429
	val MuckeDeclTerm = make_FunMuckeDecl DeclTerm PDeclsTerm LHSResType;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   430
in MuckeDeclTerm end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   431
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   432
fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   433
    (let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   434
     	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   435
	 val VarAbs = variant_abs(str,tp,t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   436
	 val BoundConst = Const(fst VarAbs,tp);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   437
	 val t1 = ExConst $ TypeConst;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   438
	 val t2 = t1 $ BoundConst;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   439
 	 val t3 = elim_quantifications sign (snd VarAbs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   440
     in t2 $ t3 end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   441
  |  elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   442
    (let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   443
    	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   444
	 val VarAbs = variant_abs(str,tp,t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   445
	 val BoundConst = Const(fst VarAbs,tp);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   446
	 val t1 = AllConst $ TypeConst;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   447
	 val t2 = t1 $ BoundConst;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   448
	 val t3 = elim_quantifications sign (snd VarAbs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   449
     in t2 $ t3 end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   450
  | elim_quantifications sign (t1 $ t2) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   451
   	(elim_quantifications sign t1) $ (elim_quantifications sign t2)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   452
  | elim_quantifications sign (Abs(_,_,t)) = elim_quantifications sign t
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   453
  | elim_quantifications sign t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   454
fun elim_quant_in_list sign [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   455
  | elim_quant_in_list sign (trm::list) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   456
			(elim_quantifications sign trm)::(elim_quant_in_list sign list);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   457
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   458
fun dummy true = writeln "True\n" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   459
    dummy false = writeln "Fals\n";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   460
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   461
fun transform_definitions sign [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   462
  | transform_definitions sign (trm::list) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   463
      if is_mudef trm 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   464
      then (make_mu_def sign trm)::(transform_definitions sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   465
      else 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   466
	if is_nudef trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   467
	 then (make_nu_def sign trm)::(transform_definitions sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   468
     	 else 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   469
	   if is_fundef trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   470
 	   then (make_mucke_fun_def sign trm)::(transform_definitions sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   471
		     else trm::(transform_definitions sign list);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   472
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   473
fun terms_to_decls sign [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   474
 | terms_to_decls sign (trm::list) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   475
      if is_mudef trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   476
      then (make_mu_decl sign trm)::(terms_to_decls sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   477
      else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   478
        if is_nudef trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   479
         then (make_nu_decl sign trm)::(terms_to_decls sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   480
         else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   481
           if is_fundef trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   482
           then (make_mucke_fun_decl sign trm)::(terms_to_decls sign list)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   483
                     else (transform_definitions sign list);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   484
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   485
fun transform_terms sign list = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   486
let val DefsOk = transform_definitions sign list;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   487
in elim_quant_in_list sign DefsOk
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   488
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   489
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   490
fun string_of_terms sign terms =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   491
let fun make_string sign [] = "" |
14818
ad83019a66a4 Output.output;
wenzelm
parents: 7305
diff changeset
   492
 	make_string sign (trm::list) =
14980
267cc670317a got rid of Output.output for default print mode;
wenzelm
parents: 14818
diff changeset
   493
           Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   494
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   495
(setmp print_mode ["Mucke"] (make_string sign) terms)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   496
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   497
6491
7954ffeb93f3 fixed IO;
wenzelm
parents: 6473
diff changeset
   498
fun callmc s =
7954ffeb93f3 fixed IO;
wenzelm
parents: 6473
diff changeset
   499
  let
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   500
    val mucke_home = getenv "MUCKE_HOME";
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   501
    val mucke =
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   502
      if mucke_home = "" then error "Environment variable MUCKE_HOME not set"
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   503
      else mucke_home ^ "/mucke";
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   504
    val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   505
    val _ = File.write mucke_input_file s;
16258
f3d913abf7e5 File.shell_path;
wenzelm
parents: 16152
diff changeset
   506
    val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   507
  in
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   508
    if not (!trace_mc) then (File.rm mucke_input_file) else (); 
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   509
    result
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   510
  end;
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   511
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   512
(* extract_result looks for true value before *) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   513
(* finishing line "===..." of mucke output    *)
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   514
(* ------------------------------------------ *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   515
(* Be Careful:                                *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   516
(* If the mucke version changes, some changes *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   517
(* have also to be made here:                 *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   518
(* In extract_result, the value               *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   519
(* answer_with_info_lines checks the output   *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   520
(* of the muche version, where the output     *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   521
(* finishes with information about memory and *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   522
(* time (segregated from the "true" value by  *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   523
(* a line of equality signs).                 *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   524
(* For older versions, where this line does   *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   525
(* exist, value general_answer checks whether *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   526
(* "true" stand at the end of the output.     *)
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   527
local
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   528
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   529
infix is_prefix_of contains at_post string_contains string_at_post;
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   530
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   531
  val is_blank : string -> bool =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   532
      fn " " => true | "\t" => true | "\n" => true | "\^L" => true 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   533
       | "\160" => true | _ => false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   534
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   535
  fun delete_blanks [] = []
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   536
    | delete_blanks (":"::xs) = delete_blanks xs
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   537
    | delete_blanks (x::xs) = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   538
        if (is_blank x) then (delete_blanks xs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   539
	       	        else x::(delete_blanks xs);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   540
  
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   541
  fun delete_blanks_string s = implode(delete_blanks (explode s));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   542
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   543
  fun [] is_prefix_of s = true
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   544
    | (p::ps) is_prefix_of  [] = false
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   545
    | (p::ps) is_prefix_of (x::xs) = (p = x) andalso (ps is_prefix_of xs);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   546
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   547
  fun [] contains [] = true
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   548
    | [] contains s = false
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   549
    | (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   550
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   551
  fun [] at_post [] = true
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   552
    | [] at_post s = false
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   553
    | (x::xs) at_post s = (s = (x::xs)) orelse (xs at_post s);
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   554
 
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   555
  fun s string_contains s1 = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   556
      (explode s) contains (explode s1);
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   557
  fun s string_at_post s1 =
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   558
      (explode s) at_post (explode s1);
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   559
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   560
in 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   561
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   562
fun extract_result goal answer =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   563
  let 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   564
    val search_text_true = "istrue===";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   565
    val short_answer = delete_blanks_string answer;
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   566
    val answer_with_info_lines = short_answer string_contains search_text_true;
7305
dad3b686941c mucke -res;
wenzelm
parents: 7295
diff changeset
   567
    (* val general_answer = short_answer string_at_post "true" *) 
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   568
  in
7305
dad3b686941c mucke -res;
wenzelm
parents: 7295
diff changeset
   569
    (answer_with_info_lines) (* orelse (general_answer) *)
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   570
  end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   571
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   572
end; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   573
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   574
(**************************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   575
(* SECTION 2: rewrites case-constructs over complex datatypes *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   576
local
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   577
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   578
(* check_case checks, whether a term is of the form a $ "(case x of ...)", *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   579
(* where x is of complex datatype; the second argument of the result is    *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   580
(* the number of constructors of the type of x                             *) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   581
fun check_case sg tl (a $ b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   582
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   583
 (* tl_contains_complex returns true in the 1st argument when argument type is *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   584
 (* complex; the 2nd argument is the number of constructors                    *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   585
 fun tl_contains_complex [] _ = (false,0) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   586
 tl_contains_complex ((a,l)::r) t =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   587
 let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   588
  fun check_complex [] p = p |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   589
  check_complex ((a,[])::r) (t,i) = check_complex r (t,i+1) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   590
  check_complex ((a,_)::r) (t,i) = check_complex r (true,i+1);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   591
 in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   592
	if (a=t) then (check_complex l (false,0)) else (tl_contains_complex r t)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   593
 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   594
 fun check_head_for_case sg (Const(s,_)) st 0 = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   595
	if (post_last_dot(s) = (st ^ "_case")) then true else false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   596
 check_head_for_case sg (a $ (Const(s,_))) st 0 = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   597
	if (post_last_dot(s) = (st ^ "_case")) then true else false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   598
 check_head_for_case _ _ _ 0 = false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   599
 check_head_for_case sg (a $ b) st n = check_head_for_case sg a st (n-1) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   600
 check_head_for_case _ _ _ _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   601
 fun qtn (Type(a,_)) = a | 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   602
 qtn _ = error "unexpected type variable in check_case";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   603
 val t = type_of_term b;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   604
 val (bv,n) = tl_contains_complex tl t
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   605
 val st = post_last_dot(qtn t); 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   606
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   607
 if (bv) then ((check_head_for_case sg a st n),n) else (false,n) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   608
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   609
check_case sg tl trm = (false,0);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   610
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   611
(* enrich_case_with_terms enriches a case term with additional *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   612
(* conditions according to the context of the case replacement *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   613
fun enrich_case_with_terms sg [] t = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   614
enrich_case_with_terms sg [trm] (Abs(x,T,t)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   615
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   616
 val v = variant_abs(x,T,t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   617
 val f = fst v;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   618
 val s = snd v
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   619
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   620
(Const("Ex",Type("fun",[Type("fun",[T,Type("bool",[])]),Type("bool",[])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   621
(Abs(x,T,
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   622
abstract_over(Free(f,T),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   623
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   624
$
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   625
(Const("op =",Type("fun",[T,Type("fun",[T,Type("bool",[])])])) $ (Free(f,T)) $ trm)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   626
$ s))))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   627
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   628
enrich_case_with_terms sg (a::r) (Abs(x,T,t)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   629
        enrich_case_with_terms sg [a] (Abs(x,T,(enrich_case_with_terms sg r t))) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   630
enrich_case_with_terms sg (t::r) trm =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   631
let val ty = type_of_term t
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   632
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   633
(Const("Ex",Type("fun",[Type("fun",[ ty ,Type("bool",[])]),Type("bool",[])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   634
Abs("a", ty,
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   635
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   636
$
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   637
(Const("op =",Type("fun",[ ty ,Type("fun",[ ty ,Type("bool",[])])])) $ Bound(0) $ t)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   638
$
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   639
enrich_case_with_terms sg r (trm $ (Bound(length(r))))))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   640
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   641
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   642
fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   643
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   644
 fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(variant_abs(x,T,t))) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   645
 heart_of_trm t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   646
 fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   647
 replace_termlist_with_args sg _ trm _ [a] _ ([],[]) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   648
	if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   649
	(enrich_case_with_terms sg a trm) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   650
 replace_termlist_with_args sg tl trm con [] t (l1,l2) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   651
	(replace_termlist_with_constrs sg tl l1 l2 t) | 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   652
 replace_termlist_with_args sg tl trm con (a::r) t (l1,l2) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   653
 let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   654
  val tty = type_of_term t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   655
  val con_term = con_term_of con a;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   656
 in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   657
	(Const("If",Type("fun",[Type("bool",[]),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   658
        Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   659
	(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   660
        t $ con_term) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   661
	(if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   662
	(enrich_case_with_terms sg a trm)) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   663
	(replace_termlist_with_args sg tl trm con r t (l1,l2)))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   664
 end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   665
 val arglist = arglist_of sg tl (snd c);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   666
 val tty = type_of_term t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   667
 val con_typ = fun_type_of (rev (snd c)) tty;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   668
 val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   669
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   670
 replace_termlist_with_args sg tl a con arglist t (l1,l2)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   671
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   672
replace_termlist_with_constrs _ _ _ _ _ = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   673
error "malformed arguments in replace_termlist_with_constrs" (* shouldnt occur *);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   674
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   675
(* rc_in_termlist constructs a cascading if with the case terms in trm_list, *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   676
(* which were found in rc_in_term (see replace_case)                         *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   677
fun rc_in_termlist sg tl trm_list trm =  
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   678
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   679
 val ty = type_of_term trm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   680
 val constr_list = search_in_keylist tl ty;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   681
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   682
	replace_termlist_with_constrs sg tl trm_list constr_list trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   683
end;  
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   684
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   685
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   686
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   687
(* replace_case replaces each case statement over a complex datatype by a cascading if; *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   688
(* it is normally called with a 0 in the 4th argument, it is positive, if in the course *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   689
(* of calculation, a "case" is discovered and then indicates the distance to that case  *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   690
fun replace_case sg tl (a $ b) 0 =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   691
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   692
 (* rc_in_term changes the case statement over term x to a cascading if; the last *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   693
 (* indicates the distance to the "case"-constant                                 *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   694
 fun rc_in_term sg tl (a $ b) l x 0 =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   695
	 (replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) |  
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   696
 rc_in_term sg tl  _ l x 0 = rc_in_termlist sg tl l x |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   697
 rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   698
 rc_in_term sg _ trm _ _ n =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   699
 error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   700
 val (bv,n) = check_case sg tl (a $ b);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   701
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   702
 if (bv) then 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   703
	(let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   704
	val t = (replace_case sg tl a n) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   705
	in 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   706
	rc_in_term sg tl t [] b n	
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   707
	end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   708
 else ((replace_case sg tl a 0) $ (replace_case sg tl b 0))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   709
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   710
replace_case sg tl (a $ b) 1 = a $ (replace_case sg tl b 0) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   711
replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   712
replace_case sg tl (Abs(x,T,t)) _ = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   713
let 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   714
 val v = variant_abs(x,T,t);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   715
 val f = fst v;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   716
 val s = snd v
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   717
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   718
 Abs(x,T,abstract_over(Free(f,T),replace_case sg tl s 0))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   719
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   720
replace_case _ _ t _ = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   721
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   722
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   723
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   724
(*******************************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   725
(* SECTION 3: replacing variables being part of a constructor term *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   726
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   727
(* transforming terms so that nowhere a variable is subterm of *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   728
(* a constructor term; the transformation uses cascading ifs   *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   729
fun remove_vars sg tl (Abs(x,ty,trm)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   730
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   731
(* checks freeness of variable x in term *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   732
fun xFree x (a $ b) = if (xFree x a) then true else (xFree x b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   733
xFree x (Abs(a,T,trm)) = xFree x trm |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   734
xFree x (Free(y,_)) = if (x=y) then true else false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   735
xFree _ _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   736
(* really substitues variable x by term c *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   737
fun real_subst sg tl x c (a$b) = (real_subst sg tl x c a) $ (real_subst sg tl x c b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   738
real_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,real_subst sg tl x c trm) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   739
real_subst sg tl x c (Free(y,t)) = if (x=y) then c else Free(y,t) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   740
real_subst sg tl x c t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   741
(* substituting variable x by term c *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   742
fun x_subst sg tl x c (a $ b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   743
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   744
 val t = (type_of_term (a $ b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   745
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   746
 if ((list_contains_key tl t) andalso (xFree x (a$b)))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   747
 then (real_subst sg tl x c (a$b)) else ((x_subst sg tl x c a) $ (x_subst sg tl x c b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   748
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   749
x_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,x_subst sg tl x c trm) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   750
x_subst sg tl x c t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   751
(* genearting a cascading if *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   752
fun casc_if sg tl x ty (c::l) trm =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   753
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   754
 val arglist = arglist_of sg tl (snd c);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   755
 val con_typ = fun_type_of (rev (snd c)) ty;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   756
 val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   757
 fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   758
 casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   759
 casc_if2 sg tl x con (a::r) ty trm cl =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   760
        Const("If",Type("fun",[Type("bool",[]),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   761
        Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   762
        ])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   763
     (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   764
        Free(x,ty) $ (real_subst sg tl x (con_term_of con a) (Free(x,ty)))) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   765
   (x_subst sg tl x (con_term_of con a) trm) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   766
   (casc_if2 sg tl x con r ty trm cl) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   767
 casc_if2 sg tl x con [] ty trm cl = casc_if sg tl x ty cl trm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   768
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   769
 casc_if2 sg tl x con arglist ty trm l
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   770
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   771
casc_if _ _ _ _ [] trm = trm (* should never occur *); 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   772
fun if_term sg tl x ty trm =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   773
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   774
 val tyC_list = search_in_keylist tl ty;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   775
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   776
 casc_if sg tl x ty tyC_list trm
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   777
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   778
(* checking whether a variable occurs in a constructor term *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   779
fun constr_term_contains_var sg tl (a $ b) x =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   780
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   781
 val t = type_of_term (a $ b)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   782
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   783
 if ((list_contains_key tl t) andalso (xFree x (a$b))) then true
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   784
 else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   785
 (if (constr_term_contains_var sg tl a x) then true 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   786
  else (constr_term_contains_var sg tl b x))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   787
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   788
constr_term_contains_var sg tl (Abs(y,ty,trm)) x =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   789
         constr_term_contains_var sg tl (snd(variant_abs(y,ty,trm))) x |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   790
constr_term_contains_var _ _ _ _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   791
val vt = variant_abs(x,ty,trm);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   792
val tt = remove_vars sg tl (snd(vt))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   793
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   794
if (constr_term_contains_var sg tl tt (fst vt))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   795
(* fst vt muss frei vorkommen, als ECHTER TeilKonstruktorterm *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   796
then (Abs(x,ty,
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   797
        abstract_over(Free(fst vt,ty),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   798
	if_term sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) (fst vt) ty tt)))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   799
else Abs(x,ty,abstract_over(Free(fst vt,ty),tt))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   800
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   801
remove_vars sg tl (a $ b) = (remove_vars sg tl a) $ (remove_vars sg tl b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   802
remove_vars sg tl t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   803
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   804
(* dissolves equalities "=" of boolean terms, where one of them is a complex term *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   805
fun remove_equal sg tl (Abs(x,ty,trm)) = Abs(x,ty,remove_equal sg tl trm) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   806
remove_equal sg tl (Const("op =",Type("fun",[Type("bool",[]),
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   807
	Type("fun",[Type("bool",[]),Type("bool",[])])])) $ lhs $ rhs) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   808
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   809
fun complex_trm (Abs(_,_,_)) = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   810
complex_trm (_ $ _) = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   811
complex_trm _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   812
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   813
(if ((complex_trm lhs) orelse (complex_trm rhs)) then
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   814
(let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   815
val lhs = remove_equal sg tl lhs;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   816
val rhs = remove_equal sg tl rhs
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   817
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   818
(
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   819
Const("op &",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   820
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   821
(Const("op -->",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   822
 Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   823
	lhs $ rhs) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   824
(Const("op -->",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   825
 Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   826
	rhs $ lhs)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   827
)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   828
end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   829
else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   830
(Const("op =",
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   831
 Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   832
	lhs $ rhs))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   833
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   834
remove_equal sg tl (a $ b) = (remove_equal sg tl a) $ (remove_equal sg tl b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   835
remove_equal sg tl trm = trm;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   836
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   837
(* rewrites constructor terms (without vars) for mucke *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   838
fun rewrite_dt_term sg tl (Abs(x,ty,t)) = Abs(x,ty,(rewrite_dt_term sg tl t)) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   839
rewrite_dt_term sg tl (a $ b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   840
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   841
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   842
(* OUTPUT - relevant *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   843
(* transforms constructor term to a mucke-suitable output *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   844
fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   845
		(term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   846
term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   847
term_OUTPUT sg (Const(s,t)) = post_last_dot s |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   848
term_OUTPUT _ _ = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   849
error "term contains an unprintable constructor term (in term_OUTPUT)";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   850
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   851
fun contains_bound i (Bound(j)) = if (j>=i) then true else false |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   852
contains_bound i (a $ b) = if (contains_bound i a) then true else (contains_bound i b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   853
contains_bound i (Abs(_,_,t)) = contains_bound (i+1) t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   854
contains_bound _ _ = false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   855
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   856
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   857
        if (contains_bound 0 (a $ b)) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   858
	then ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   859
        else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   860
        (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   861
        let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   862
        val t = type_of_term (a $ b);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   863
        in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   864
        if (list_contains_key tl t) then (Const((term_OUTPUT sg (a $ b)),t)) else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   865
        ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   866
        end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   867
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   868
rewrite_dt_term sg tl t = t;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   869
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   870
fun rewrite_dt_terms sg tl [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   871
rewrite_dt_terms sg tl (a::r) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   872
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   873
 val c = (replace_case sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) a 0);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   874
 val rv = (remove_vars sg tl c);  
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   875
 val rv = (remove_equal sg tl rv);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   876
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   877
 ((rewrite_dt_term sg tl rv) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   878
 :: (rewrite_dt_terms sg tl r))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   879
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   880
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   881
(**********************************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   882
(* SECTION 4: generating type declaration and preprocessing type list *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   883
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   884
fun make_type_decls [] tl = "" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   885
make_type_decls ((a,l)::r) tl = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   886
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   887
fun comma_list_of [] = "" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   888
comma_list_of (a::[]) = a |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   889
comma_list_of (a::r) = a ^ "," ^ (comma_list_of r);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   890
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   891
(* OUTPUT - relevant *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   892
(* produces for each type of the 2nd argument its constant names (see *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   893
(* concat_constr) and appends them to prestring (see concat_types)    *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   894
fun generate_constnames_OUTPUT prestring [] _ = [prestring] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   895
generate_constnames_OUTPUT prestring ((Type("*",[a,b]))::r) tl =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   896
 generate_constnames_OUTPUT prestring (a::b::r) tl |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   897
generate_constnames_OUTPUT prestring (a::r) tl =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   898
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   899
 fun concat_constrs [] _ = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   900
 concat_constrs ((c,[])::r) tl = c::(concat_constrs r tl)  |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   901
 concat_constrs ((c,l)::r) tl =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   902
         (generate_constnames_OUTPUT (c ^ "_I_") l tl) @ (concat_constrs r tl);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   903
 fun concat_types _ [] _ _ = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   904
 concat_types prestring (a::q) [] tl = [prestring ^ a] 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   905
				       @ (concat_types prestring q [] tl) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   906
 concat_types prestring (a::q) r tl = 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   907
		(generate_constnames_OUTPUT (prestring ^ a ^ "_I_") r tl) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   908
		@ (concat_types prestring q r tl);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   909
 val g = concat_constrs (search_in_keylist tl a) tl;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   910
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   911
 concat_types prestring g r tl
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   912
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   913
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   914
fun make_type_decl a tl =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   915
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   916
        val astr = type_to_string_OUTPUT a;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   917
        val dl = generate_constnames_OUTPUT "" [a] tl;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   918
        val cl = comma_list_of dl;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   919
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   920
        ("enum " ^ astr ^ " {" ^ cl ^ "};\n")
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   921
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   922
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   923
 (make_type_decl a tl) ^ (make_type_decls r tl)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   924
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   925
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   926
fun check_finity gl [] [] true = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   927
check_finity gl bl [] true = (check_finity gl [] bl false) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   928
check_finity _ _ [] false =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   929
error "used datatypes are not finite" |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   930
check_finity gl bl ((t,cl)::r) b =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   931
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   932
fun listmem [] _ = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   933
listmem (a::r) l = if (a mem l) then (listmem r l) else false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   934
fun snd_listmem [] _ = true |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   935
snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   936
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   937
(if (snd_listmem cl gl) then (check_finity (t::gl) bl r true)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   938
else (check_finity gl ((t,cl)::bl) r b))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   939
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   940
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   941
fun preprocess_td sg [] done = [] |
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   942
preprocess_td sg (a::b) done =
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   943
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   944
fun extract_hd sg (_ $ Abs(_,_,r)) = extract_hd sg r |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   945
extract_hd sg (Const("Trueprop",_) $ r) = extract_hd sg r |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   946
extract_hd sg (Var(_,_) $ r) = extract_hd sg r |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   947
extract_hd sg (a $ b) = extract_hd sg a |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   948
extract_hd sg (Const(s,t)) = post_last_dot s |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   949
extract_hd _ _ =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   950
error "malformed constructor term in a induct-theorem";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   951
fun list_of_param_types sg tl pl (_ $ Abs(_,t,r)) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   952
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   953
 fun select_type [] [] t = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   954
 select_type (a::r) (b::s) t =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   955
 if (t=b) then a else (select_type r s t) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   956
 select_type _ _ _ =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   957
 error "wrong number of argument of a constructor in a induct-theorem";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   958
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   959
 (select_type tl pl t) :: (list_of_param_types sg tl pl r)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   960
end |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   961
list_of_param_types sg tl pl (Const("Trueprop",_) $ r) = list_of_param_types sg tl pl r |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   962
list_of_param_types _ _ _ _ = [];
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   963
fun split_constr sg tl pl a = (extract_hd sg a,list_of_param_types sg tl pl a);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   964
fun split_constrs _ _ _ [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   965
split_constrs sg tl pl (a::r) = (split_constr sg tl pl a) :: (split_constrs sg tl pl r);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   966
fun new_types [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   967
new_types ((t,l)::r) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   968
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   969
 fun ex_bool [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   970
 ex_bool ((Type("bool",[]))::r) = ex_bool r |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   971
 ex_bool ((Type("*",[a,b]))::r) = ex_bool (a::b::r) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   972
 ex_bool (s::r) = s:: (ex_bool r);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   973
 val ll = ex_bool l
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   974
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   975
 (ll @ (new_types r))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   976
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   977
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   978
        if (a mem done)
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   979
        then (preprocess_td sg b done)
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   980
        else
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   981
        (let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   982
	 fun qtn (Type(a,tl)) = (a,tl) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   983
	 qtn _ = error "unexpected type variable in preprocess_td";
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   984
	 val s =  post_last_dot(fst(qtn a));
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   985
	 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t)))))  = t |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   986
	 param_types _ = error "malformed induct-theorem in preprocess_td";	
16429
e871f4b1a4f0 replaced obsolete theory_of_sign by theory_of_thm;
wenzelm
parents: 16258
diff changeset
   987
	 val pl = param_types (concl_of (get_thm sg (s ^ ".induct", NONE)));		
e871f4b1a4f0 replaced obsolete theory_of_sign by theory_of_thm;
wenzelm
parents: 16258
diff changeset
   988
         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE)));
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   989
	 val ntl = new_types l;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   990
        in 
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
   991
        ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   992
        end)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   993
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   994
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   995
fun extract_type_names_prems sg [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   996
extract_type_names_prems sg (a::b) =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   997
let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   998
fun analyze_types sg [] = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
   999
analyze_types sg [Type(a,[])] =
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1000
(let
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1001
 val s = (Sign.string_of_typ sg (Type(a,[])))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1002
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1003
 (if (s="bool") then ([]) else ([Type(a,[])]))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1004
end) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1005
analyze_types sg [Type("*",l)] = analyze_types sg l |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1006
analyze_types sg [Type("fun",l)] = analyze_types sg l |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1007
analyze_types sg [Type(t,l)] = ((Type(t,l))::(analyze_types sg l)) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1008
analyze_types sg (a::l) = (analyze_types sg [a]) @ (analyze_types sg l);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1009
fun extract_type_names sg (Const("==",_)) = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1010
extract_type_names sg (Const("Trueprop",_)) = [] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1011
extract_type_names sg (Const(_,typ)) = analyze_types sg [typ] |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1012
extract_type_names sg (a $ b) = (extract_type_names sg a) @ (extract_type_names sg b) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1013
extract_type_names sg (Abs(x,T,t)) = (analyze_types sg [T]) @ (extract_type_names sg t) |
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1014
extract_type_names _ _ = [];
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1015
in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1016
 (extract_type_names sg a) @ extract_type_names_prems sg b
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1017
end;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1018
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1019
(**********************************************************)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1020
(* mk_mc_oracle:  new argument of MuckeOracleExn: source_thy *)
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1021
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
  1022
fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) = 
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1023
  let 	val Freesubgoal = freeze_thaw subgoal;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1024
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1025
	val prems = Logic.strip_imp_prems Freesubgoal; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1026
	val concl = Logic.strip_imp_concl Freesubgoal; 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1027
	
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1028
	val Muckedecls = terms_to_decls sign prems;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1029
	val decls_str = string_of_terms sign Muckedecls;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1030
	
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1031
	val type_list = (extract_type_names_prems sign (prems@[concl]));
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6491
diff changeset
  1032
	val ctl =  preprocess_td sign type_list [];
6473
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1033
	val b = if (ctl=[]) then true else (check_finity [Type("bool",[])] [] ctl false);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1034
	val type_str = make_type_decls ctl 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1035
				((Type("bool",[]),("True",[])::("False",[])::[])::ctl);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1036
	
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1037
	val mprems = rewrite_dt_terms sign ctl prems;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1038
	val mconcl = rewrite_dt_terms sign ctl [concl];
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1039
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1040
	val Muckeprems = transform_terms sign mprems;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1041
        val prems_str = transform_case(string_of_terms sign Muckeprems);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1042
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1043
        val Muckeconcl = elim_quant_in_list sign mconcl;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1044
	val concl_str = transform_case(string_of_terms sign Muckeconcl);
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1045
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1046
	val MCstr = (
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1047
		"/**** type declarations: ****/\n" ^ type_str ^
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1048
		"/**** declarations: ****/\n" ^ decls_str ^
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1049
		"/**** definitions: ****/\n" ^ prems_str ^ 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1050
		"/**** formula: ****/\n" ^ concl_str ^";");
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1051
	val result = callmc MCstr;
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1052
  in
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1053
(if !trace_mc then 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1054
	(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1055
          else ();
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1056
(case (extract_result concl_str result) of 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1057
	true  =>  (Logic.strip_imp_concl subgoal) | 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1058
	false => (error ("Mucke couldn't solve subgoal: \n" ^result)))) 
7411f5d6bad7 added for mucke translation;
mueller
parents:
diff changeset
  1059
  end;