datatype.ML

replaced store_thm by bind_thm

(* Title:       HOL/datatype.ML
   ID:          $Id$
   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
   Copyright 1994 TU Muenchen
*)


(*used for constructor parameters*)
datatype dt_type = dtVar of string |
  dtTyp of dt_type list * string |
  dtRek of dt_type list * string;

local 

val mysort = sort;
open ThyParse HOLogic;
exception Impossible;
exception RecError of string;

val is_dtRek = (fn dtRek _ => true  |  _  => false);
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 

(* ----------------------------------------------------------------------- *)
(* Derivation of the primrec combinator application from the equations     *)

(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *)

fun subst_apps (_,_) [] t = t
  | subst_apps (fname,cpos) pairs t =
    let 
    fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
      | subst (funct $ body) = 
	let val (f,b) = strip_comb (funct$body)
	in 
	  if is_Const f andalso fst(dest_Const f) = fname 
	    then 
	      let val (ls,rest) = (take(cpos,b), drop (cpos,b));
		val (xk,rs) = (hd rest,tl rest)
		  handle LIST _ => raise RecError "not enough arguments \
		   \ in recursive application on rhs"
              in 
		(case assoc (pairs,xk) of 
		   None => raise RecError 
		     ("illegal occurence of " ^ fname ^ " on rhs")
		 | Some(U) => list_comb(U,ls @ rs))
	      end
	  else list_comb(f, map subst b)
	end
      | subst(t) = t
    in subst t end;
  
(* abstract rhs *)

fun abst_rec (fname,cpos,tc,ls,cargs,rs,rhs) =       
  let val rargs = (map fst o 
		   (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
      val subs = map (fn (s,T) => (s,dummyT))
	           (rev(rename_wrt_term rhs rargs));
      val subst_rhs = subst_apps (fname,cpos)
	                (map Free rargs ~~ map Free subs) rhs;
      val res = list_abs_free (cargs @ subs @ ls @ rs, subst_rhs);
  in
    if fname mem add_term_names (res,[]) 
      then raise RecError ("illegal occurence of " ^ fname ^ " on rhs")
    else res
  end;

(* parsing the prim rec equations *)

fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
                 = (lhs, rhs)
   | dest_eq _ = raise RecError "not a proper equation"; 

fun dest_rec eq = 
  let val (lhs,rhs) = dest_eq eq; 
    val (name,args) = strip_comb lhs; 
    val (ls',rest)  = take_prefix is_Free args; 
    val (middle,rs') = take_suffix is_Free rest;
    val cpos = length ls';
    val (c,cargs') = strip_comb (hd middle)
      handle LIST "hd" => raise RecError "constructor missing";
    val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
			 , map dest_Free rs')
      handle TERM ("dest_Free",_) => 
	  raise RecError "constructor has illegal argument in pattern";
  in 
    if length middle > 1 then 
      raise RecError "more than one non-variable in pattern"
    else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
      raise RecError "repeated variable name in pattern" 
	 else (fst(dest_Const name) handle TERM _ => 
	       raise RecError "function is not declared as constant in theory"
		 ,cpos,ls,fst( dest_Const c),cargs,rs,rhs)
  end; 

(* check function specified for all constructors and sort function terms *)

fun check_and_sort (n,its) = 
  if length its = n 
    then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
  else raise error "Primrec definition error:\n\
   \Please give an equation for every constructor";

(* translate rec equations into function arguments suitable for rec comb *)
(* theory parameter needed for printing error messages                   *) 

fun trans_recs _ _ [] = error("No primrec equations.")
  | trans_recs thy cs' (eq1::eqs) = 
    let val (name1,cpos1,ls1,_,_,_,_) = dest_rec eq1
      handle RecError s =>
	error("Primrec definition error: " ^ s ^ ":\n" 
	      ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
      val tcs = map (fn (_,c,T,_) => (c,T)) cs';  
      val cs = map fst tcs;
      fun trans_recs' _ [] = []
        | trans_recs' cis (eq::eqs) = 
	  let val (name,cpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
	    val tc = assoc(tcs,c);
	    val i = (1 + find (c,cs))  handle LIST "find" => 0; 
	  in
	  if name <> name1 then 
	    raise RecError "function names inconsistent"
	  else if cpos <> cpos1 then 
	    raise RecError "position of rec. argument inconsistent"
	  else if i = 0 then 
	    raise RecError "illegal argument in pattern" 
	  else if i mem cis then
	    raise RecError "constructor already occured as pattern "
	       else (i,abst_rec (name,cpos,the tc,ls,cargs,rs,rhs))
		     :: trans_recs' (i::cis) eqs 
	  end
	  handle RecError s =>
	        error("Primrec definition error\n" ^ s ^ "\n" 
		      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
    in (  name1, ls1
	, check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
    end ;

in
  fun add_datatype (typevars, tname, cons_list') thy = 
    let (*search for free type variables and convert recursive *)
      fun analyse_types (cons, typlist, syn) =
	let fun analyse(t as dtVar v) =
	  if t mem typevars then t
	  else error ("Free type variable " ^ v ^ " on rhs.")
	      | analyse(dtTyp(typl,s)) =
		if tname <> s then dtTyp(analyses typl, s)
		else if typevars = typl then dtRek(typl, s)
                     else error (s ^ " used in different ways")
	      | analyse(dtRek _) = raise Impossible
	    and analyses ts = map analyse ts;
	in (cons, Syntax.const_name cons syn, analyses typlist, syn) 
	end;

     (*test if all elements are recursive, i.e. if the type is empty*)
      
      fun non_empty (cs : ('a * 'b * dt_type list * 'c) list) = 
	not(forall (exists is_dtRek o #3) cs) orelse
	error("Empty datatype not allowed!");

      val cons_list = map analyse_types cons_list';
      val dummy = non_empty cons_list;
      val num_of_cons = length cons_list;

     (* Auxiliary functions to construct argument and equation lists *)

     (*generate 'var_n, ..., var_m'*)
      fun Args(var, delim, n, m) = 
	space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));

     (*generate 'name_1', ..., 'name_n'*)
      fun C_exp(name, n, var) =
        if n > 0 then name ^ parens(Args(var, ",", 1, n)) else name;

     (*generate 'x_n = y_n, ..., x_m = y_m'*)
      fun Arg_eql(n,m) = 
        if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) 
        else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ 
	  Arg_eql(n+1, m);

     (*Pretty printers for type lists;
       pp_typlist1: parentheses, pp_typlist2: brackets*)
      fun pp_typ (dtVar s) = s
        | pp_typ (dtTyp (typvars, id)) =
	  if null typvars then id else (pp_typlist1 typvars) ^ id
        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
      and
	pp_typlist' ts = commas (map pp_typ ts)
      and
	pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);

      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);

     (* Generate syntax translation for case rules *)
      fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) = 
	let val arity = length typlist;
	  val body  = "z" ^ string_of_int(c_nr);
	  val args1 = if arity=0 then ""
		      else parens (Args ("y", ",", y_nr, y_nr+arity-1));
	  val args2 = if arity=0 then ""
		      else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
			^ ". ";
	  val (rest1,rest2) = 
	    if null cs then ("","")
	    else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
	    in (" | " ^ h1, ", " ^ h2) end;
	in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
        | calc_xrules _ _ [] = raise Impossible;
      
      val xrules =
	let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
	in  [("logic", "case x of " ^ first_part) <->
	     ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )]
	end;

     (*type declarations for constructors*)
      fun const_type (id, _, typlist, syn) =
	(id,  
	 (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
	    pp_typlist1 typevars ^ tname, syn);


      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
	let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
	in h ^ (assumpt (ts, vs, true)) end
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
      | assumpt ([], [], found) = if found then "|] ==>" else ""
        | assumpt _ = raise Impossible;

     (*insert type with suggested name 'varname' into table*)
      fun insert typ varname ((tri as (t, s, n)) :: xs) = 
	if typ = t then (t, s, n+1) :: xs
	else tri :: (if varname = s then insert typ (varname ^ "'") xs
		     else insert typ varname xs)
        | insert typ varname [] = [(typ, varname, 1)];

      fun typid(dtRek(_,id)) = id
        | typid(dtVar s) = implode (tl (explode s))
        | typid(dtTyp(_,id)) = id;

      val insert_types = foldl (fn (tab,typ) => insert typ (typid typ) tab);

      fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs
        | update(t, s, v :: vs, t1 :: ts) = 
	  if t=t1 then s :: vs else v :: (update (t, s, vs, ts))
        | update _ = raise Impossible;
      
      fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
	if r1 = r2 then (s ^ string_of_int n) :: 
	  (update_n (dtRek r1, s, vs, ts, n+1))
	else v :: (update_n (dtRek r1, s, vs, ts, n))
        | update_n (t, s, v :: vs, t1 :: ts, n) = 
	  if t = t1 then (s ^ string_of_int n) :: 
	    (update_n (t, s, vs, ts, n+1))
	  else v :: (update_n (t, s, vs, ts, n))
        | update_n (_,_,[],[],_) = []
        | update_n _ = raise Impossible;

     (*insert type variables into table*)
      fun convert typs =
        let fun conv(vars, (t, s, n)) =
	  if n=1 then update (t, s, vars, typs)
	  else update_n (t, s, vars, typs, 1)
        in foldl conv 
	end;

      fun empty_list n = replicate n "";

      fun t_inducting ((_, name, typl, _) :: cs) =
	let val tab = insert_types([],typl);
	  val arity = length typl;
	  val var_list = convert typl (empty_list arity,tab); 
	  val h = if arity = 0 then " P(" ^ name ^ ")"
		  else " !!" ^ (space_implode " " var_list) ^ "." ^
		    (assumpt (typl, var_list, false)) ^ "P(" ^ 
		    name ^ "(" ^ (commas var_list) ^ "))";
	  val rest = t_inducting cs;
	in if rest = "" then h else h ^ "; " ^ rest end
        | t_inducting [] = "";

      fun t_induct cl typ_name =
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";

      fun gen_typlist typevar f ((_, _, ts, _) :: cs) =
	let val h = if (length ts) > 0
		      then pp_typlist2(f ts) ^ "=>"
		    else ""
	in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
        | gen_typlist _ _ [] = "";


(* -------------------------------------------------------------------- *)
(* The case constant and rules 	        				*)
 		
      val t_case = tname ^ "_case";

      fun case_rule n (id, name, ts, _) =
	let val args = opt_parens(Args("x", ",", 1, length ts))
	in (t_case ^ "_" ^ id,
	    t_case ^ "(" ^ Args("f", ",", 1, num_of_cons)
	    ^ "," ^ name ^ args 
	    ^ ") = f"  ^ string_of_int(n) ^ args)
	end

      fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
        | case_rules _ [] = [];

      val datatype_arity = length typevars;

      val types = [(tname, datatype_arity, NoSyn)];

      val arities = 
        let val term_list = replicate datatype_arity termS;
        in [(tname, term_list, termS)] 
	end;

      val datatype_name = pp_typlist1 typevars ^ tname;

      val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";

      val case_const =
	(t_case,
	 "[" ^ gen_typlist new_tvar_name I cons_list 
	 ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name,
	 NoSyn);

      val rules_case = case_rules 1 cons_list;

(* -------------------------------------------------------------------- *)
(* The prim-rec combinator						*) 

      val t_rec = tname ^ "_rec"

(* adding type variables for dtRek types to end of list of dt_types      *)   

      fun add_reks ts = 
	ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 

(* positions of the dtRek types in a list of dt_types, starting from 1  *)

      fun rek_pos ts = 
	map snd (filter (is_dtRek o fst) (ts ~~ (1 upto length ts)))

      fun rec_rule n (id,name,ts,_) = 
	let val args = Args("x",",",1,length ts)
	  val fargs = Args("f",",",1,num_of_cons)
	  fun rarg i = "," ^ t_rec ^ parens(fargs ^ "," ^ "x" ^ 
					    string_of_int(i)) 
	  val rargs = implode (map rarg (rek_pos ts)) 
	in     
	  ( t_rec ^ "_" ^ id
	   , t_rec ^ parens(fargs ^  "," ^ name ^ (opt_parens args)) ^ " = f"
	   ^ string_of_int(n) ^ opt_parens (args ^ rargs)) 
	end

      fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
	| rec_rules _ [] = [];

      val rec_const =
	(t_rec,
	 "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
	 ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name,
	 NoSyn);

      val rules_rec = rec_rules 1 cons_list

(* -------------------------------------------------------------------- *)
      val consts = 
	map const_type cons_list
	@ (if num_of_cons < dtK then []
	   else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
	@ [case_const,rec_const];


      fun Ci_ing ((id, name, typlist, _) :: cs) =
	let val arity = length typlist;
	in if arity = 0 then Ci_ing cs
	   else ("inject_" ^ id,
		 "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") 
		 ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs)
	end
	| Ci_ing [] = [];

      fun Ci_negOne (id1, name1, tl1, _) (id2, name2, tl2, _) =
	let val ax = C_exp(name1, length tl1, "x") ^ "~=" ^
	  C_exp(name2, length tl2, "y")
	in (id1 ^ "_not_" ^ id2, ax) 
	end;

      fun Ci_neg1 [] = []
	| Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;

      fun suc_expr n = 
	if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";

      fun Ci_neg2() =
	let val ord_t = tname ^ "_ord";
	  val cis = cons_list ~~ (0 upto (num_of_cons - 1))
	  fun Ci_neg2equals ((id, name, typlist, _), n) =
	    let val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x")) 
	      ^ ") = " ^ (suc_expr n)
	    in (ord_t ^ "_" ^ id, ax) end
	in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
	  (map Ci_neg2equals cis)
	end;

      val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
			   else Ci_neg2();

      val rules_inject = Ci_ing cons_list;

      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);

      val rules = rule_induct ::
	(rules_inject @ rules_distinct @ rules_case @ rules_rec);

      fun add_primrec eqns thy =
	let val rec_comb = Const(t_rec,dummyT)
	  val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
	  val (fname,ls,fns) = trans_recs thy cons_list teqns
	  val rhs = 
	    list_abs_free
	    (ls @ [(tname,dummyT)]
	     ,list_comb(rec_comb
			, fns @ map Bound (0 ::(length ls downto 1))));
          val sg = sign_of thy;
          val defpair =  mk_defpair (Const(fname,dummyT),rhs)
	  val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
	  val varT = Type.varifyT T;
          val ftyp = the (Sign.const_type sg fname);
	in
	  if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
	  then add_defs_i [defpairT] thy
	  else error("Primrec definition error: \ntype of " ^ fname 
		     ^ " is not instance of type deduced from equations")
	end;

    in 
      (thy
      |> add_types types
      |> add_arities arities
      |> add_consts consts
      |> add_trrules xrules
      |> add_axioms rules,add_primrec)
    end
end