src/HOL/datatype.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1465 5d7a7e439cec
child 1668 8ead1fe65aad
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
clasohm@923
     1
(* Title:       HOL/datatype.ML
clasohm@923
     2
   ID:          $Id$
clasohm@923
     3
   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
clasohm@923
     4
   Copyright 1995 TU Muenchen
clasohm@923
     5
*)
clasohm@923
     6
clasohm@923
     7
clasohm@923
     8
(*used for constructor parameters*)
clasohm@923
     9
datatype dt_type = dtVar of string |
clasohm@923
    10
  dtTyp of dt_type list * string |
clasohm@923
    11
  dtRek of dt_type list * string;
clasohm@923
    12
clasohm@923
    13
structure Datatype =
clasohm@923
    14
struct
clasohm@923
    15
local 
clasohm@923
    16
clasohm@923
    17
val mysort = sort;
clasohm@923
    18
open ThyParse HOLogic;
clasohm@923
    19
exception Impossible;
clasohm@923
    20
exception RecError of string;
clasohm@923
    21
clasohm@923
    22
val is_dtRek = (fn dtRek _ => true  |  _  => false);
clasohm@923
    23
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 
clasohm@923
    24
clasohm@923
    25
(* ----------------------------------------------------------------------- *)
clasohm@923
    26
(* Derivation of the primrec combinator application from the equations     *)
clasohm@923
    27
clasohm@923
    28
(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs  *) 
clasohm@923
    29
clasohm@923
    30
fun subst_apps (_,_) [] t = t
clasohm@923
    31
  | subst_apps (fname,rpos) pairs t =
clasohm@923
    32
    let 
clasohm@923
    33
    fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
clasohm@923
    34
      | subst (funct $ body) = 
clasohm@1465
    35
        let val (f,b) = strip_comb (funct$body)
clasohm@1465
    36
        in 
clasohm@1465
    37
          if is_Const f andalso fst(dest_Const f) = fname 
clasohm@1465
    38
            then 
clasohm@1465
    39
              let val (ls,rest) = (take(rpos,b), drop(rpos,b));
clasohm@1465
    40
                val (xk,rs) = (hd rest,tl rest)
clasohm@1465
    41
                  handle LIST _ => raise RecError "not enough arguments \
clasohm@1465
    42
                   \ in recursive application on rhs"
clasohm@923
    43
              in 
clasohm@1465
    44
                (case assoc (pairs,xk) of 
clasohm@1574
    45
                   None   => list_comb(f, map subst b)
clasohm@1574
    46
                 | Some U => list_comb(U, map subst (ls @ rs)))
clasohm@1465
    47
              end
clasohm@1465
    48
          else list_comb(f, map subst b)
clasohm@1465
    49
        end
clasohm@923
    50
      | subst(t) = t
clasohm@923
    51
    in subst t end;
clasohm@923
    52
  
clasohm@923
    53
(* abstract rhs *)
clasohm@923
    54
clasohm@923
    55
fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) =       
clasohm@923
    56
  let val rargs = (map fst o 
clasohm@1465
    57
                   (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
clasohm@923
    58
      val subs = map (fn (s,T) => (s,dummyT))
clasohm@1465
    59
                   (rev(rename_wrt_term rhs rargs));
clasohm@923
    60
      val subst_rhs = subst_apps (fname,rpos)
clasohm@1465
    61
                        (map Free rargs ~~ map Free subs) rhs;
clasohm@923
    62
  in 
clasohm@923
    63
      list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) 
clasohm@923
    64
  end;
clasohm@923
    65
clasohm@923
    66
(* parsing the prim rec equations *)
clasohm@923
    67
clasohm@923
    68
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
clasohm@923
    69
                 = (lhs, rhs)
clasohm@923
    70
   | dest_eq _ = raise RecError "not a proper equation"; 
clasohm@923
    71
clasohm@923
    72
fun dest_rec eq = 
clasohm@923
    73
  let val (lhs,rhs) = dest_eq eq; 
clasohm@923
    74
    val (name,args) = strip_comb lhs; 
clasohm@923
    75
    val (ls',rest)  = take_prefix is_Free args; 
clasohm@923
    76
    val (middle,rs') = take_suffix is_Free rest;
clasohm@923
    77
    val rpos = length ls';
clasohm@923
    78
    val (c,cargs') = strip_comb (hd middle)
clasohm@923
    79
      handle LIST "hd" => raise RecError "constructor missing";
clasohm@923
    80
    val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
clasohm@1465
    81
                         , map dest_Free rs')
clasohm@923
    82
      handle TERM ("dest_Free",_) => 
clasohm@1465
    83
          raise RecError "constructor has illegal argument in pattern";
clasohm@923
    84
  in 
clasohm@923
    85
    if length middle > 1 then 
clasohm@923
    86
      raise RecError "more than one non-variable in pattern"
clasohm@923
    87
    else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
clasohm@923
    88
      raise RecError "repeated variable name in pattern" 
clasohm@1465
    89
         else (fst(dest_Const name) handle TERM _ => 
clasohm@1465
    90
               raise RecError "function is not declared as constant in theory"
clasohm@1465
    91
                 ,rpos,ls,fst( dest_Const c),cargs,rs,rhs)
clasohm@923
    92
  end; 
clasohm@923
    93
clasohm@923
    94
(* check function specified for all constructors and sort function terms *)
clasohm@923
    95
clasohm@923
    96
fun check_and_sort (n,its) = 
clasohm@923
    97
  if length its = n 
clasohm@923
    98
    then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
clasohm@923
    99
  else raise error "Primrec definition error:\n\
clasohm@923
   100
   \Please give an equation for every constructor";
clasohm@923
   101
clasohm@923
   102
(* translate rec equations into function arguments suitable for rec comb *)
clasohm@923
   103
(* theory parameter needed for printing error messages                   *) 
clasohm@923
   104
clasohm@923
   105
fun trans_recs _ _ [] = error("No primrec equations.")
clasohm@923
   106
  | trans_recs thy cs' (eq1::eqs) = 
clasohm@923
   107
    let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1
clasohm@923
   108
      handle RecError s =>
clasohm@1465
   109
        error("Primrec definition error: " ^ s ^ ":\n" 
clasohm@1465
   110
              ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
clasohm@923
   111
      val tcs = map (fn (_,c,T,_,_) => (c,T)) cs';  
clasohm@923
   112
      val cs = map fst tcs;
clasohm@923
   113
      fun trans_recs' _ [] = []
clasohm@923
   114
        | trans_recs' cis (eq::eqs) = 
clasohm@1465
   115
          let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
clasohm@1465
   116
            val tc = assoc(tcs,c);
clasohm@1465
   117
            val i = (1 + find (c,cs))  handle LIST "find" => 0; 
clasohm@1465
   118
          in
clasohm@1465
   119
          if name <> name1 then 
clasohm@1465
   120
            raise RecError "function names inconsistent"
clasohm@1465
   121
          else if rpos <> rpos1 then 
clasohm@1465
   122
            raise RecError "position of rec. argument inconsistent"
clasohm@1465
   123
          else if i = 0 then 
clasohm@1465
   124
            raise RecError "illegal argument in pattern" 
clasohm@1465
   125
          else if i mem cis then
clasohm@1465
   126
            raise RecError "constructor already occured as pattern "
clasohm@1465
   127
               else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs))
clasohm@1465
   128
                     :: trans_recs' (i::cis) eqs 
clasohm@1465
   129
          end
clasohm@1465
   130
          handle RecError s =>
clasohm@1465
   131
                error("Primrec definition error\n" ^ s ^ "\n" 
clasohm@1465
   132
                      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
clasohm@923
   133
    in (  name1, ls1
clasohm@1465
   134
        , check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
clasohm@923
   135
    end ;
clasohm@923
   136
clasohm@923
   137
in
clasohm@923
   138
  fun add_datatype (typevars, tname, cons_list') thy = 
clasohm@923
   139
    let
clasohm@923
   140
      fun typid(dtRek(_,id)) = id
clasohm@923
   141
        | typid(dtVar s) = implode (tl (explode s))
clasohm@923
   142
        | typid(dtTyp(_,id)) = id;
clasohm@923
   143
clasohm@923
   144
      fun index_vnames(vn::vns,tab) =
clasohm@923
   145
            (case assoc(tab,vn) of
clasohm@923
   146
               None => if vn mem vns
clasohm@923
   147
                       then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
clasohm@923
   148
                       else vn :: index_vnames(vns,tab)
clasohm@923
   149
             | Some(i) => (vn^(string_of_int i)) ::
clasohm@923
   150
                          index_vnames(vns,(vn,i+1)::tab))
clasohm@923
   151
        | index_vnames([],tab) = [];
clasohm@923
   152
clasohm@923
   153
      fun mk_var_names types = index_vnames(map typid types,[]);
clasohm@923
   154
clasohm@923
   155
      (*search for free type variables and convert recursive *)
clasohm@923
   156
      fun analyse_types (cons, types, syn) =
clasohm@1465
   157
        let fun analyse(t as dtVar v) =
clasohm@923
   158
                  if t mem typevars then t
clasohm@923
   159
                  else error ("Free type variable " ^ v ^ " on rhs.")
clasohm@1465
   160
              | analyse(dtTyp(typl,s)) =
clasohm@1465
   161
                  if tname <> s then dtTyp(analyses typl, s)
clasohm@923
   162
                  else if typevars = typl then dtRek(typl, s)
clasohm@923
   163
                       else error (s ^ " used in different ways")
clasohm@1465
   164
              | analyse(dtRek _) = raise Impossible
clasohm@1465
   165
            and analyses ts = map analyse ts;
clasohm@1465
   166
        in (cons, Syntax.const_name cons syn, analyses types,
clasohm@923
   167
            mk_var_names types, syn)
clasohm@923
   168
        end;
clasohm@923
   169
clasohm@923
   170
     (*test if all elements are recursive, i.e. if the type is empty*)
clasohm@923
   171
      
clasohm@923
   172
      fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = 
clasohm@1465
   173
        not(forall (exists is_dtRek o #3) cs) orelse
clasohm@1465
   174
        error("Empty datatype not allowed!");
clasohm@923
   175
clasohm@923
   176
      val cons_list = map analyse_types cons_list';
clasohm@923
   177
      val dummy = non_empty cons_list;
clasohm@923
   178
      val num_of_cons = length cons_list;
clasohm@923
   179
clasohm@923
   180
     (* Auxiliary functions to construct argument and equation lists *)
clasohm@923
   181
clasohm@923
   182
     (*generate 'var_n, ..., var_m'*)
clasohm@923
   183
      fun Args(var, delim, n, m) = 
clasohm@1465
   184
        space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
clasohm@923
   185
clasohm@923
   186
      fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns);
clasohm@923
   187
clasohm@923
   188
     (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
clasohm@923
   189
      fun arg_eqs vns vns' =
clasohm@923
   190
        let fun mkeq(x,x') = x ^ "=" ^ x'
clasohm@923
   191
        in space_implode " & " (map mkeq (vns~~vns')) end;
clasohm@923
   192
clasohm@923
   193
     (*Pretty printers for type lists;
clasohm@923
   194
       pp_typlist1: parentheses, pp_typlist2: brackets*)
nipkow@1279
   195
      fun pp_typ (dtVar s) = "(" ^ s ^ "::term)"
clasohm@923
   196
        | pp_typ (dtTyp (typvars, id)) =
clasohm@1465
   197
          if null typvars then id else (pp_typlist1 typvars) ^ id
clasohm@923
   198
        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
clasohm@923
   199
      and
clasohm@1465
   200
        pp_typlist' ts = commas (map pp_typ ts)
clasohm@923
   201
      and
clasohm@1465
   202
        pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
clasohm@923
   203
clasohm@923
   204
      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
clasohm@923
   205
clasohm@923
   206
     (* Generate syntax translation for case rules *)
clasohm@923
   207
      fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = 
clasohm@1465
   208
        let val arity = length vns;
clasohm@1465
   209
          val body  = "z" ^ string_of_int(c_nr);
clasohm@1465
   210
          val args1 = if arity=0 then ""
clasohm@1465
   211
                      else " " ^ Args ("y", " ", y_nr, y_nr+arity-1);
clasohm@1465
   212
          val args2 = if arity=0 then ""
clasohm@1465
   213
                      else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
clasohm@1465
   214
                        ^ ". ";
clasohm@1465
   215
          val (rest1,rest2) = 
clasohm@1465
   216
            if null cs then ("","")
clasohm@1465
   217
            else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
clasohm@1465
   218
            in (" | " ^ h1, " " ^ h2) end;
clasohm@1465
   219
        in (name ^ args1 ^ " => " ^ body ^ rest1,
clasohm@964
   220
            args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2)
clasohm@923
   221
        end
clasohm@923
   222
        | calc_xrules _ _ [] = raise Impossible;
clasohm@923
   223
      
clasohm@923
   224
      val xrules =
clasohm@1465
   225
        let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
clasohm@1465
   226
        in [("logic", "case x of " ^ first_part) <->
clasohm@1465
   227
             ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
clasohm@1465
   228
        end;
clasohm@923
   229
clasohm@923
   230
     (*type declarations for constructors*)
clasohm@923
   231
      fun const_type (id, _, typlist, _, syn) =
clasohm@1465
   232
        (id,  
clasohm@1465
   233
         (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
clasohm@1465
   234
            pp_typlist1 typevars ^ tname, syn);
clasohm@923
   235
clasohm@923
   236
clasohm@923
   237
      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
clasohm@1465
   238
        let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
clasohm@1465
   239
        in h ^ (assumpt (ts, vs, true)) end
clasohm@923
   240
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
clasohm@923
   241
      | assumpt ([], [], found) = if found then "|] ==>" else ""
clasohm@923
   242
        | assumpt _ = raise Impossible;
clasohm@923
   243
clasohm@923
   244
      fun t_inducting ((_, name, types, vns, _) :: cs) =
clasohm@1465
   245
        let
clasohm@1465
   246
          val h = if null types then " P(" ^ name ^ ")"
clasohm@1465
   247
                  else " !!" ^ (space_implode " " vns) ^ "." ^
clasohm@1465
   248
                    (assumpt (types, vns, false)) ^
clasohm@923
   249
                    "P(" ^ C_exp name vns ^ ")";
clasohm@1465
   250
          val rest = t_inducting cs;
clasohm@1465
   251
        in if rest = "" then h else h ^ "; " ^ rest end
clasohm@923
   252
        | t_inducting [] = "";
clasohm@923
   253
clasohm@923
   254
      fun t_induct cl typ_name =
clasohm@923
   255
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
clasohm@923
   256
clasohm@923
   257
      fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) =
clasohm@1465
   258
        let val h = if (length ts) > 0
clasohm@1465
   259
                      then pp_typlist2(f ts) ^ "=>"
clasohm@1465
   260
                    else ""
clasohm@1465
   261
        in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
clasohm@923
   262
        | gen_typlist _ _ [] = "";
clasohm@923
   263
clasohm@923
   264
clasohm@923
   265
(* -------------------------------------------------------------------- *)
clasohm@1465
   266
(* The case constant and rules                                          *)
clasohm@1465
   267
                
clasohm@923
   268
      val t_case = tname ^ "_case";
clasohm@923
   269
clasohm@923
   270
      fun case_rule n (id, name, _, vns, _) =
clasohm@1465
   271
        let val args = if vns = [] then "" else " " ^ space_implode " " vns
clasohm@1465
   272
        in (t_case ^ "_" ^ id,
clasohm@1465
   273
            t_case ^ " " ^ Args("f", " ", 1, num_of_cons)
clasohm@1465
   274
            ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
clasohm@1465
   275
        end
clasohm@923
   276
clasohm@923
   277
      fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
clasohm@923
   278
        | case_rules _ [] = [];
clasohm@923
   279
clasohm@923
   280
      val datatype_arity = length typevars;
clasohm@923
   281
clasohm@923
   282
      val types = [(tname, datatype_arity, NoSyn)];
clasohm@923
   283
clasohm@923
   284
      val arities = 
clasohm@923
   285
        let val term_list = replicate datatype_arity termS;
clasohm@923
   286
        in [(tname, term_list, termS)] 
clasohm@1465
   287
        end;
clasohm@923
   288
clasohm@923
   289
      val datatype_name = pp_typlist1 typevars ^ tname;
clasohm@923
   290
clasohm@923
   291
      val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
clasohm@923
   292
clasohm@923
   293
      val case_const =
clasohm@1465
   294
        (t_case,
clasohm@1465
   295
         "[" ^ gen_typlist new_tvar_name I cons_list 
clasohm@1465
   296
         ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term",
clasohm@1465
   297
         NoSyn);
clasohm@923
   298
clasohm@923
   299
      val rules_case = case_rules 1 cons_list;
clasohm@923
   300
clasohm@923
   301
(* -------------------------------------------------------------------- *)
clasohm@1465
   302
(* The prim-rec combinator                                              *) 
clasohm@923
   303
clasohm@923
   304
      val t_rec = tname ^ "_rec"
clasohm@923
   305
clasohm@923
   306
(* adding type variables for dtRek types to end of list of dt_types      *)   
clasohm@923
   307
clasohm@923
   308
      fun add_reks ts = 
clasohm@1465
   309
        ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
clasohm@923
   310
clasohm@923
   311
(* positions of the dtRek types in a list of dt_types, starting from 1  *)
clasohm@923
   312
      fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
clasohm@923
   313
clasohm@923
   314
      fun rec_rule n (id,name,ts,vns,_) = 
clasohm@1465
   315
        let val args = opt_parens(space_implode ") (" vns)
clasohm@1465
   316
          val fargs = opt_parens(Args("f", ") (", 1, num_of_cons))
clasohm@1465
   317
          fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")"
clasohm@1465
   318
          val rargs = opt_parens(space_implode ") ("
clasohm@964
   319
                                 (map rarg (rek_vars ts vns)))
clasohm@1465
   320
        in
clasohm@1465
   321
          (t_rec ^ "_" ^ id,
clasohm@1465
   322
           t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f"
clasohm@1465
   323
           ^ string_of_int(n) ^ args ^ rargs)
clasohm@1465
   324
        end
clasohm@923
   325
clasohm@923
   326
      fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
clasohm@1465
   327
        | rec_rules _ [] = [];
clasohm@923
   328
clasohm@923
   329
      val rec_const =
clasohm@1465
   330
        (t_rec,
clasohm@1465
   331
         "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
clasohm@1465
   332
         ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term",
clasohm@1465
   333
         NoSyn);
clasohm@923
   334
clasohm@923
   335
      val rules_rec = rec_rules 1 cons_list
clasohm@923
   336
clasohm@923
   337
(* -------------------------------------------------------------------- *)
clasohm@923
   338
      val consts = 
clasohm@1465
   339
        map const_type cons_list
clasohm@1465
   340
        @ (if num_of_cons < dtK then []
clasohm@1465
   341
           else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
clasohm@1465
   342
        @ [case_const,rec_const];
clasohm@923
   343
clasohm@923
   344
clasohm@923
   345
      fun Ci_ing ((id, name, _, vns, _) :: cs) =
clasohm@1465
   346
           if null vns then Ci_ing cs
clasohm@1465
   347
           else let val vns' = variantlist(vns,vns)
clasohm@923
   348
                in ("inject_" ^ id,
clasohm@1465
   349
                    "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
clasohm@1465
   350
                    ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
clasohm@923
   351
                end
clasohm@1465
   352
        | Ci_ing [] = [];
clasohm@923
   353
clasohm@923
   354
      fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
clasohm@923
   355
            let val vns2' = variantlist(vns2,vns1)
clasohm@923
   356
                val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
clasohm@1465
   357
        in (id1 ^ "_not_" ^ id2, ax) end;
clasohm@923
   358
clasohm@923
   359
      fun Ci_neg1 [] = []
clasohm@1465
   360
        | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
clasohm@923
   361
clasohm@923
   362
      fun suc_expr n = 
clasohm@1465
   363
        if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
clasohm@923
   364
clasohm@923
   365
      fun Ci_neg2() =
clasohm@1465
   366
        let val ord_t = tname ^ "_ord";
clasohm@1465
   367
          val cis = cons_list ~~ (0 upto (num_of_cons - 1))
clasohm@1465
   368
          fun Ci_neg2equals ((id, name, _, vns, _), n) =
clasohm@1465
   369
            let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
clasohm@1465
   370
            in (ord_t ^ "_" ^ id, ax) end
clasohm@1465
   371
        in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
clasohm@1465
   372
          (map Ci_neg2equals cis)
clasohm@1465
   373
        end;
clasohm@923
   374
clasohm@923
   375
      val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
clasohm@1465
   376
                           else Ci_neg2();
clasohm@923
   377
clasohm@923
   378
      val rules_inject = Ci_ing cons_list;
clasohm@923
   379
clasohm@923
   380
      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
clasohm@923
   381
clasohm@923
   382
      val rules = rule_induct ::
clasohm@1465
   383
        (rules_inject @ rules_distinct @ rules_case @ rules_rec);
clasohm@923
   384
clasohm@923
   385
      fun add_primrec eqns thy =
clasohm@1465
   386
        let val rec_comb = Const(t_rec,dummyT)
clasohm@1465
   387
          val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
clasohm@1465
   388
          val (fname,ls,fns) = trans_recs thy cons_list teqns
clasohm@1465
   389
          val rhs = 
clasohm@1465
   390
            list_abs_free
clasohm@1465
   391
            (ls @ [(tname,dummyT)]
clasohm@1465
   392
             ,list_comb(rec_comb
clasohm@1465
   393
                        , fns @ map Bound (0 ::(length ls downto 1))));
clasohm@923
   394
          val sg = sign_of thy;
clasohm@1574
   395
          val defpair = (fname ^ "_" ^ tname ^ "_def",
clasohm@1574
   396
                         Logic.mk_equals (Const(fname,dummyT), rhs))
clasohm@1465
   397
          val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
clasohm@1465
   398
          val varT = Type.varifyT T;
clasohm@923
   399
          val ftyp = the (Sign.const_type sg fname);
clasohm@1574
   400
        in add_defs_i [defpairT] thy end;
clasohm@923
   401
clasohm@1360
   402
    in
clasohm@1455
   403
      datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
clasohm@1360
   404
      (thy |> add_types types
clasohm@1360
   405
           |> add_arities arities
clasohm@1360
   406
           |> add_consts consts
clasohm@1360
   407
           |> add_trrules xrules
clasohm@1360
   408
           |> add_axioms rules, add_primrec)
clasohm@923
   409
    end
clasohm@923
   410
end
clasohm@923
   411
end
clasohm@923
   412
clasohm@923
   413
(*
clasohm@923
   414
Informal description of functions used in datatype.ML for the Isabelle/HOL
clasohm@923
   415
implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) 
clasohm@923
   416
clasohm@923
   417
* subst_apps (fname,rpos) pairs t:
clasohm@923
   418
   substitute the term 
clasohm@923
   419
       fname(ls,xk,rs) 
clasohm@923
   420
   by 
clasohm@923
   421
      yk(ls,rs) 
clasohm@923
   422
   in t for (xk,yk) in pairs, where rpos = length ls. 
clasohm@923
   423
   Applied with : 
clasohm@923
   424
     fname = function name 
clasohm@923
   425
     rpos = position of recursive argument 
clasohm@923
   426
     pairs = list of pairs (xk,yk), where 
clasohm@923
   427
          xk are the rec. arguments of the constructor in the pattern,
clasohm@923
   428
          yk is a variable with name derived from xk 
clasohm@923
   429
     t = rhs of equation 
clasohm@923
   430
clasohm@923
   431
* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs)
clasohm@923
   432
  - filter recursive arguments from constructor arguments cargs,
clasohm@923
   433
  - perform substitutions on rhs, 
clasohm@923
   434
  - derive list subs of new variable names yk for use in subst_apps, 
clasohm@923
   435
  - abstract rhs with respect to cargs, subs, ls and rs. 
clasohm@923
   436
clasohm@923
   437
* dest_eq t 
clasohm@923
   438
  destruct a term denoting an equation into lhs and rhs. 
clasohm@923
   439
clasohm@923
   440
* dest_req eq 
clasohm@923
   441
  destruct an equation of the form 
clasohm@923
   442
      name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs
clasohm@923
   443
  into 
clasohm@923
   444
  - function name  (name) 
clasohm@923
   445
  - position of the first non-variable parameter  (rpos)
clasohm@923
   446
  - the list of first rpos parameters (ls = [vl1..vlrpos]) 
clasohm@923
   447
  - the constructor (fst( dest_Const c) = Ci)
clasohm@923
   448
  - the arguments of the constructor (cargs = [vi1..vin])
clasohm@923
   449
  - the rest of the variables in the pattern (rs = [vr1..vrn])
clasohm@923
   450
  - the right hand side of the equation (rhs).  
clasohm@923
   451
 
clasohm@923
   452
* check_and_sort (n,its)
clasohm@923
   453
  check that  n = length its holds, and sort elements of its by 
clasohm@923
   454
  first component. 
clasohm@923
   455
clasohm@923
   456
* trans_recs thy cs' (eq1::eqs)
clasohm@923
   457
  destruct eq1 into name1, rpos1, ls1, etc.. 
clasohm@923
   458
  get constructor list with and without type (tcs resp. cs) from cs',  
clasohm@923
   459
  for every equation:  
clasohm@923
   460
    destruct it into (name,rpos,ls,c,cargs,rs,rhs)
clasohm@923
   461
    get typed constructor tc from c and tcs 
clasohm@923
   462
    determine the index i of the constructor 
clasohm@923
   463
    check function name and position of rec. argument by comparison
clasohm@923
   464
    with first equation 
clasohm@923
   465
    check for repeated variable names in pattern
clasohm@923
   466
    derive function term f_i which is used as argument of the rec. combinator
clasohm@923
   467
    sort the terms f_i according to i and return them together
clasohm@923
   468
      with the function name and the parameter of the definition (ls). 
clasohm@923
   469
clasohm@923
   470
* Application:
clasohm@923
   471
clasohm@923
   472
  The rec. combinator is applied to the function terms resulting from
clasohm@923
   473
  trans_rec. This results in a function which takes the recursive arg. 
clasohm@923
   474
  as first parameter and then the arguments corresponding to ls. The
clasohm@923
   475
  order of parameters is corrected by setting the rhs equal to 
clasohm@923
   476
clasohm@923
   477
  list_abs_free
clasohm@1465
   478
            (ls @ [(tname,dummyT)]
clasohm@1465
   479
             ,list_comb(rec_comb
clasohm@1465
   480
                        , fns @ map Bound (0 ::(length ls downto 1))));
clasohm@923
   481
clasohm@923
   482
  Note the de-Bruijn indices counting the number of lambdas between the
clasohm@923
   483
  variable and its binding. 
clasohm@923
   484
*)