datatype.ML
author nipkow
Mon, 26 Sep 1994 18:04:43 +0100
changeset 146 85f62d491ff7
parent 143 3226f25f88e7
child 147 8ff6c8c95870
permissions -rw-r--r--
replaced local instantaite_types by inferT_axm
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
129
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     1
(* Title:  HOL/Datatype
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     2
   ID:     $Id$
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     3
   Author: Max Breitling, Carsten Clasohm,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     4
           Tobias Nipkow, Norbert Voelker
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     5
   Copyright 1994 TU Muenchen
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     6
*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     7
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     8
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
     9
(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    10
local
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    11
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    12
  val dtK = 5
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    13
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    14
in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    15
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    16
local open ThyParse in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    17
  val datatype_decls =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    18
    let 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    19
      val tvar = type_var >> (fn s => "dtVar" ^ s);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    20
    
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    21
      val type_var_list = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    22
	tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    23
    
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    24
      val typ =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    25
	ident                  >> (fn s => "dtTyp([]," ^ quote s ^")")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    26
      ||
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    27
	type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    28
				   "," ^ quote id ^ ")")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    29
      ||
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    30
	tvar;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    31
    
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    32
      val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    33
      
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    34
      val cons = name -- typ_list -- opt_mixfix;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    35
  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    36
      fun constructs ts =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    37
	( cons --$$ "|" -- constructs >> op::
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    38
      ||
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    39
	 cons                        >> (fn c => [c])) ts;  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    40
  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    41
      fun mk_cons cs =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    42
	case findrep (map (fst o fst) cs) of
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    43
	  [] => map (fn ((s,ts),syn) => parens(commas [s,mk_list ts,syn])) cs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    44
	| c::_ => error("Constructor \"" ^ c ^ "\" occurs twice");
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    45
      
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    46
      (*remove all quotes from a string*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    47
      val rem_quotes = implode o filter (fn c => c <> "\"") o explode;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    48
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    49
      (*generate names of distinct axioms*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    50
      fun rules_distinct cs tname = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    51
        let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    52
      (*combine all constructor names with all others w/o duplicates*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    53
	  fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    54
	  fun neg1 [] = []
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    55
	    | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    56
	in if length uqcs < dtK then neg1 uqcs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    57
	   else quote (tname ^ "_ord_distinct") ::
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    58
	     map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    59
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    60
         
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    61
      fun rules tname cons pre =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    62
	" map (get_axiom thy) " ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    63
	mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    64
		   cons)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    65
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    66
	(*generate string for calling 'add_datatype'*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    67
      fun mk_params ((ts, tname), cons) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    68
	("val (thy," ^ tname ^ "_add_primrec) =  add_datatype\n" ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    69
	 parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    70
	 " thy\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    71
	  \val thy=thy",
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    72
	 "structure " ^ tname ^ " =\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    73
	  \struct\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    74
	  \  val inject = map (get_axiom thy) " ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    75
	 mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s)) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    76
		  (filter_out (null o snd o fst) cons)) ^ ";\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    77
		   \  val distinct = " ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    78
	 (if length cons < dtK then "let val distinct' = " else "") ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    79
	    "map (get_axiom thy) " ^ mk_list (rules_distinct cons tname) ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    80
	    (if length cons < dtK then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    81
	       "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    82
		\ distinct') end"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    83
	     else "") ^ ";\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    84
	      \  val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    85
	      \  val cases =" ^ rules tname cons "_case_" ^ ";\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    86
	      \  val recs =" ^ rules tname cons "_rec_" ^ ";\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    87
	      \  val simps = inject @ distinct @ cases @ recs;\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    88
	      \  fun induct_tac a =\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    89
	      \res_inst_tac[(" ^ quote tname ^ ", a)]induct;\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    90
	      \end;\n")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    91
    in 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    92
      (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    93
end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    94
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    95
val primrec_decl =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
    96
  let fun mkstrings((fname,tname),axms) =
143
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
    97
        let fun prove (name,eqn) =
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
    98
              "val "^name^"= prove_goalw thy [get_def thy "^fname^"] "^eqn^"\n\
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
    99
              \  (fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
   100
            val axs = mk_list (map (fn (n,a) => mk_pair(quote n,a)) axms)
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
   101
        in ("|> " ^ tname^"_add_primrec " ^ axs, cat_lines(map prove axms))
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
   102
        end
141
9cb51c2358ea Allowed string as function name in primrec header
nipkow
parents: 129
diff changeset
   103
  in name -- long_id -- repeat1 (ident -- string)  >> mkstrings end
129
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   104
end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   105
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   106
(*used for constructor parameters*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   107
datatype dt_type = dtVar of string |
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   108
  dtTyp of dt_type list * string |
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   109
  dtRek of dt_type list * string;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   110
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   111
local 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   112
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   113
val mysort = sort;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   114
open ThyParse
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   115
exception Impossible;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   116
exception RecError of string;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   117
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   118
val is_dtRek = (fn dtRek _ => true  |  _  => false);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   119
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   120
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   121
(* ----------------------------------------------------------------------- *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   122
(* Derivation of the primrec combinator application from the equations     *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   123
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   124
(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   125
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   126
fun subst_apps (_,_) [] t = t
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   127
  | subst_apps (fname,cpos) pairs t =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   128
    let 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   129
    fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   130
      | subst (funct $ body) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   131
	let val (f,b) = strip_comb (funct$body)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   132
	in 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   133
	  if is_Const f andalso fst(dest_Const f) = fname 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   134
	    then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   135
	      let val (ls,rest) = (take(cpos,b), drop (cpos,b));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   136
		val (xk,rs) = (hd rest,tl rest)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   137
		  handle LIST _ => raise RecError "not enough arguments \
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   138
		   \ in recursive application on rhs"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   139
              in 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   140
		(case assoc (pairs,xk) of 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   141
		   None => raise RecError 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   142
		     ("illegal occurence of " ^ fname ^ " on rhs")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   143
		 | Some(U) => list_comb(U,ls @ rs))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   144
	      end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   145
	  else list_comb(f, map subst b)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   146
	end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   147
      | subst(t) = t
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   148
    in subst t end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   149
  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   150
(* abstract rhs *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   151
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   152
fun abst_rec (fname,cpos,tc,ls,cargs,rs,rhs) =       
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   153
  let val rargs = (map fst o 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   154
		   (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   155
      val subs = map (fn (s,T) => (s,dummyT))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   156
	           (rev(rename_wrt_term rhs rargs));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   157
      val subst_rhs = subst_apps (fname,cpos)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   158
	                (map Free rargs ~~ map Free subs) rhs;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   159
      val res = list_abs_free (cargs @ subs @ ls @ rs, subst_rhs);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   160
  in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   161
    if fname mem add_term_names (res,[]) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   162
      then raise RecError ("illegal occurence of " ^ fname ^ " on rhs")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   163
    else res
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   164
  end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   165
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   166
(* parsing the prim rec equations *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   167
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   168
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   169
                 = (lhs, rhs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   170
   | dest_eq _ = raise RecError "not a proper equation"; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   171
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   172
fun dest_rec eq = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   173
  let val (lhs,rhs) = dest_eq eq; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   174
    val (name,args) = strip_comb lhs; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   175
    val (ls',rest)  = take_prefix is_Free args; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   176
    val (middle,rs') = take_suffix is_Free rest;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   177
    val cpos = length ls';
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   178
    val (c,cargs') = strip_comb (hd middle)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   179
      handle LIST "hd" => raise RecError "constructor missing";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   180
    val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   181
			 , map dest_Free rs')
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   182
      handle TERM ("dest_Free",_) => 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   183
	  raise RecError "constructor has illegal argument in pattern";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   184
  in 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   185
    if length middle > 1 then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   186
      raise RecError "more than one non-variable in pattern"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   187
    else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   188
      raise RecError "repeated variable name in pattern" 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   189
	 else (fst(dest_Const name) handle TERM _ => 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   190
	       raise RecError "function is not declared as constant in theory"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   191
		 ,cpos,ls,fst( dest_Const c),cargs,rs,rhs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   192
  end; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   193
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   194
(* check function specified for all constructors and sort function terms *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   195
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   196
fun check_and_sort (n,its) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   197
  if length its = n 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   198
    then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   199
  else raise error "Primrec definition error:\n\
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   200
   \Please give an equation for every constructor";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   201
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   202
(* translate rec equations into function arguments suitable for rec comb *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   203
(* theory parameter needed for printing error messages                   *) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   204
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   205
fun trans_recs _ _ [] = error("No primrec equations.")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   206
  | trans_recs thy cs' (eq1::eqs) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   207
    let val (name1,cpos1,ls1,_,_,_,_) = dest_rec eq1
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   208
      handle RecError s =>
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   209
	error("Primrec definition error: " ^ s ^ ":\n" 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   210
	      ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   211
      val tcs = map (fn (_,c,T,_) => (c,T)) cs';  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   212
      val cs = map fst tcs;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   213
      fun trans_recs' _ [] = []
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   214
        | trans_recs' cis (eq::eqs) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   215
	  let val (name,cpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   216
	    val tc = assoc(tcs,c);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   217
	    val i = (1 + find (c,cs))  handle LIST "find" => 0; 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   218
	  in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   219
	  if name <> name1 then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   220
	    raise RecError "function names inconsistent"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   221
	  else if cpos <> cpos1 then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   222
	    raise RecError "position of rec. argument inconsistent"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   223
	  else if i = 0 then 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   224
	    raise RecError "illegal argument in pattern" 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   225
	  else if i mem cis then
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   226
	    raise RecError "constructor already occured as pattern "
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   227
	       else (i,abst_rec (name,cpos,the tc,ls,cargs,rs,rhs))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   228
		     :: trans_recs' (i::cis) eqs 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   229
	  end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   230
	  handle RecError s =>
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   231
	        error("Primrec definition error\n" ^ s ^ "\n" 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   232
		      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   233
    in (  name1, ls1
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   234
	, check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   235
    end ;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   236
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   237
in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   238
  fun add_datatype (typevars, tname, cons_list') thy = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   239
    let (*search for free type variables and convert recursive *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   240
      fun analyse_types (cons, typlist, syn) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   241
	let fun analyse(t as dtVar v) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   242
	  if t mem typevars then t
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   243
	  else error ("Free type variable " ^ v ^ " on rhs.")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   244
	      | analyse(dtTyp(typl,s)) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   245
		if tname <> s then dtTyp(analyses typl, s)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   246
		else if typevars = typl then dtRek(typl, s)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   247
                     else error (s ^ " used in different ways")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   248
	      | analyse(dtRek _) = raise Impossible
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   249
	    and analyses ts = map analyse ts;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   250
	in (cons, Syntax.const_name cons syn, analyses typlist, syn) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   251
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   252
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   253
     (*test if all elements are recursive, i.e. if the type is empty*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   254
      
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   255
      fun non_empty (cs : ('a * 'b * dt_type list * 'c) list) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   256
	not(forall (exists is_dtRek o #3) cs) orelse
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   257
	error("Empty datatype not allowed!");
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   258
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   259
      val cons_list = map analyse_types cons_list';
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   260
      val dummy = non_empty cons_list;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   261
      val num_of_cons = length cons_list;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   262
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   263
     (* Auxiliary functions to construct argument and equation lists *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   264
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   265
     (*generate 'var_n, ..., var_m'*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   266
      fun Args(var, delim, n, m) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   267
	space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   268
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   269
     (*generate 'name_1', ..., 'name_n'*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   270
      fun C_exp(name, n, var) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   271
        if n > 0 then name ^ parens(Args(var, ",", 1, n)) else name;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   272
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   273
     (*generate 'x_n = y_n, ..., x_m = y_m'*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   274
      fun Arg_eql(n,m) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   275
        if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   276
        else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   277
	  Arg_eql(n+1, m);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   278
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   279
     (*Pretty printers for type lists;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   280
       pp_typlist1: parentheses, pp_typlist2: brackets*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   281
      fun pp_typ (dtVar s) = s
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   282
        | pp_typ (dtTyp (typvars, id)) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   283
	  if null typvars then id else (pp_typlist1 typvars) ^ id
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   284
        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   285
      and
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   286
	pp_typlist' ts = commas (map pp_typ ts)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   287
      and
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   288
	pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   289
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   290
      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   291
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   292
     (* Generate syntax translation for case rules *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   293
      fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   294
	let val arity = length typlist;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   295
	  val body  = "z" ^ string_of_int(c_nr);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   296
	  val args1 = if arity=0 then ""
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   297
		      else parens (Args ("y", ",", y_nr, y_nr+arity-1));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   298
	  val args2 = if arity=0 then ""
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   299
		      else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   300
			^ ". ";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   301
	  val (rest1,rest2) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   302
	    if null cs then ("","")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   303
	    else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   304
	    in (" | " ^ h1, ", " ^ h2) end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   305
	in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   306
        | calc_xrules _ _ [] = raise Impossible;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   307
      
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   308
      val xrules =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   309
	let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   310
	in  [("logic", "case x of " ^ first_part) <->
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   311
	     ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )]
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   312
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   313
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   314
     (*type declarations for constructors*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   315
      fun const_type (id, _, typlist, syn) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   316
	(id,  
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   317
	 (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   318
	    pp_typlist1 typevars ^ tname, syn);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   319
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   320
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   321
      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   322
	let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   323
	in h ^ (assumpt (ts, vs, true)) end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   324
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   325
      | assumpt ([], [], found) = if found then "|] ==>" else ""
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   326
        | assumpt _ = raise Impossible;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   327
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   328
     (*insert type with suggested name 'varname' into table*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   329
      fun insert typ varname ((tri as (t, s, n)) :: xs) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   330
	if typ = t then (t, s, n+1) :: xs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   331
	else tri :: (if varname = s then insert typ (varname ^ "'") xs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   332
		     else insert typ varname xs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   333
        | insert typ varname [] = [(typ, varname, 1)];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   334
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   335
      fun typid(dtRek(_,id)) = id
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   336
        | typid(dtVar s) = implode (tl (explode s))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   337
        | typid(dtTyp(_,id)) = id;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   338
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   339
      val insert_types = foldl (fn (tab,typ) => insert typ (typid typ) tab);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   340
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   341
      fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   342
        | update(t, s, v :: vs, t1 :: ts) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   343
	  if t=t1 then s :: vs else v :: (update (t, s, vs, ts))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   344
        | update _ = raise Impossible;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   345
      
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   346
      fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   347
	if r1 = r2 then (s ^ string_of_int n) :: 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   348
	  (update_n (dtRek r1, s, vs, ts, n+1))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   349
	else v :: (update_n (dtRek r1, s, vs, ts, n))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   350
        | update_n (t, s, v :: vs, t1 :: ts, n) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   351
	  if t = t1 then (s ^ string_of_int n) :: 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   352
	    (update_n (t, s, vs, ts, n+1))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   353
	  else v :: (update_n (t, s, vs, ts, n))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   354
        | update_n (_,_,[],[],_) = []
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   355
        | update_n _ = raise Impossible;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   356
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   357
     (*insert type variables into table*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   358
      fun convert typs =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   359
        let fun conv(vars, (t, s, n)) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   360
	  if n=1 then update (t, s, vars, typs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   361
	  else update_n (t, s, vars, typs, 1)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   362
        in foldl conv 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   363
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   364
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   365
      fun empty_list n = replicate n "";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   366
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   367
      fun t_inducting ((_, name, typl, _) :: cs) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   368
	let val tab = insert_types([],typl);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   369
	  val arity = length typl;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   370
	  val var_list = convert typl (empty_list arity,tab); 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   371
	  val h = if arity = 0 then " P(" ^ name ^ ")"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   372
		  else " !!" ^ (space_implode " " var_list) ^ "." ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   373
		    (assumpt (typl, var_list, false)) ^ "P(" ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   374
		    name ^ "(" ^ (commas var_list) ^ "))";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   375
	  val rest = t_inducting cs;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   376
	in if rest = "" then h else h ^ "; " ^ rest end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   377
        | t_inducting [] = "";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   378
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   379
      fun t_induct cl typ_name =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   380
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   381
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   382
      fun gen_typlist typevar f ((_, _, ts, _) :: cs) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   383
	let val h = if (length ts) > 0
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   384
		      then pp_typlist2(f ts) ^ "=>"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   385
		    else ""
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   386
	in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   387
        | gen_typlist _ _ [] = "";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   388
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   389
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   390
(* -------------------------------------------------------------------- *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   391
(* The case constant and rules 	        				*)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   392
 		
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   393
      val t_case = tname ^ "_case";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   394
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   395
      fun case_rule n (id, name, ts, _) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   396
	let val args = opt_parens(Args("x", ",", 1, length ts))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   397
	in (t_case ^ "_" ^ id,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   398
	    t_case ^ "(" ^ Args("f", ",", 1, num_of_cons)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   399
	    ^ "," ^ name ^ args 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   400
	    ^ ") = f"  ^ string_of_int(n) ^ args)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   401
	end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   402
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   403
      fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   404
        | case_rules _ [] = [];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   405
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   406
      val datatype_arity = length typevars;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   407
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   408
      val types = [(tname, datatype_arity, NoSyn)];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   409
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   410
      val arities = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   411
        let val term_list = replicate datatype_arity ["term"];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   412
        in [(tname, term_list, ["term"])] 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   413
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   414
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   415
      val datatype_name = pp_typlist1 typevars ^ tname;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   416
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   417
      val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   418
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   419
      val case_const =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   420
	(t_case,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   421
	 "[" ^ gen_typlist new_tvar_name I cons_list 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   422
	 ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   423
	 NoSyn);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   424
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   425
      val rules_case = case_rules 1 cons_list;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   426
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   427
(* -------------------------------------------------------------------- *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   428
(* The prim-rec combinator						*) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   429
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   430
      val t_rec = tname ^ "_rec"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   431
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   432
(* adding type variables for dtRek types to end of list of dt_types      *)   
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   433
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   434
      fun add_reks ts = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   435
	ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   436
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   437
(* positions of the dtRek types in a list of dt_types, starting from 1  *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   438
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   439
      fun rek_pos ts = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   440
	map snd (filter (is_dtRek o fst) (ts ~~ (1 upto length ts)))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   441
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   442
      fun rec_rule n (id,name,ts,_) = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   443
	let val args = Args("x",",",1,length ts)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   444
	  val fargs = Args("f",",",1,num_of_cons)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   445
	  fun rarg i = "," ^ t_rec ^ parens(fargs ^ "," ^ "x" ^ 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   446
					    string_of_int(i)) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   447
	  val rargs = implode (map rarg (rek_pos ts)) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   448
	in     
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   449
	  ( t_rec ^ "_" ^ id
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   450
	   , t_rec ^ parens(fargs ^  "," ^ name ^ (opt_parens args)) ^ " = f"
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   451
	   ^ string_of_int(n) ^ opt_parens (args ^ rargs)) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   452
	end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   453
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   454
      fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   455
	| rec_rules _ [] = [];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   456
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   457
      val rec_const =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   458
	(t_rec,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   459
	 "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   460
	 ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   461
	 NoSyn);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   462
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   463
      val rules_rec = rec_rules 1 cons_list
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   464
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   465
(* -------------------------------------------------------------------- *)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   466
      val consts = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   467
	map const_type cons_list
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   468
	@ (if num_of_cons < dtK then []
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   469
	   else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   470
	@ [case_const,rec_const];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   471
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   472
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   473
      fun Ci_ing ((id, name, typlist, _) :: cs) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   474
	let val arity = length typlist;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   475
	in if arity = 0 then Ci_ing cs
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   476
	   else ("inject_" ^ id,
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   477
		 "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   478
		 ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   479
	end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   480
	| Ci_ing [] = [];
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   481
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   482
      fun Ci_negOne (id1, name1, tl1, _) (id2, name2, tl2, _) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   483
	let val ax = C_exp(name1, length tl1, "x") ^ "~=" ^
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   484
	  C_exp(name2, length tl2, "y")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   485
	in (id1 ^ "_not_" ^ id2, ax) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   486
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   487
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   488
      fun Ci_neg1 [] = []
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   489
	| Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   490
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   491
      fun suc_expr n = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   492
	if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   493
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   494
      fun Ci_neg2() =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   495
	let val ord_t = tname ^ "_ord";
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   496
	  val cis = cons_list ~~ (0 upto (num_of_cons - 1))
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   497
	  fun Ci_neg2equals ((id, name, typlist, _), n) =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   498
	    let val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x")) 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   499
	      ^ ") = " ^ (suc_expr n)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   500
	    in (ord_t ^ "_" ^ id, ax) end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   501
	in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   502
	  (map Ci_neg2equals cis)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   503
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   504
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   505
      val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   506
			   else Ci_neg2();
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   507
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   508
      val rules_inject = Ci_ing cons_list;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   509
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   510
      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   511
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   512
      val rules = rule_induct ::
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   513
	(rules_inject @ rules_distinct @ rules_case @ rules_rec);
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   514
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   515
      fun add_primrec eqns thy =
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   516
	let val rec_comb = Const(t_rec,dummyT)
143
3226f25f88e7 improved error reporting for primrec
nipkow
parents: 142
diff changeset
   517
	  val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
129
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   518
	  val (fname,ls,fns) = trans_recs thy cons_list teqns
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   519
	  val rhs = 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   520
	    list_abs_free
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   521
	    (ls @ [(tname,dummyT)]
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   522
	     ,list_comb(rec_comb
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   523
			, fns @ map Bound (0 ::(length ls downto 1))));
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   524
          val sg = sign_of thy;
146
85f62d491ff7 replaced local instantaite_types by inferT_axm
nipkow
parents: 143
diff changeset
   525
          val defpair as (defname,_) =  mk_defpair (Const(fname,dummyT),rhs)
85f62d491ff7 replaced local instantaite_types by inferT_axm
nipkow
parents: 143
diff changeset
   526
	  val (_,tdef as ( _ $ Const(_,T) $ _ )) = inferT_axm sg defpair;
129
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   527
	  val varT = Type.varifyT T;
142
760641387b20 replaced lookup_const by Sign.const_type;
wenzelm
parents: 141
diff changeset
   528
          val Some(ftyp) = Sign.const_type sg fname;
129
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   529
	in
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   530
	  if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   531
	  then add_defs_i [(defname,tdef)] thy
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   532
	  else error("Primrec definition error: \ntype of " ^ fname 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   533
		     ^ " is not instance of type deduced from equations")
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   534
	end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   535
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   536
    in 
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   537
      (thy
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   538
      |> add_types types
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   539
      |> add_arities arities
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   540
      |> add_consts consts
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   541
      |> add_trrules xrules
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   542
      |> add_axioms rules,add_primrec)
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   543
    end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   544
end
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   545
end;
0bba840aa07c New version of datatype.ML with primrec (Norbert).
nipkow
parents:
diff changeset
   546