--- a/datatype.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,486 +0,0 @@
-(* Title: HOL/datatype.ML
- ID: $Id$
- Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
- Copyright 1995 TU Muenchen
-*)
-
-
-(*used for constructor parameters*)
-datatype dt_type = dtVar of string |
- dtTyp of dt_type list * string |
- dtRek of dt_type list * string;
-
-structure Datatype =
-struct
-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 *)
-
-(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *)
-
-fun subst_apps (_,_) [] t = t
- | subst_apps (fname,rpos) 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(rpos,b), drop(rpos,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,map subst (ls @ rs)))
- end
- else list_comb(f, map subst b)
- end
- | subst(t) = t
- in subst t end;
-
-(* abstract rhs *)
-
-fun abst_rec (fname,rpos,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,rpos)
- (map Free rargs ~~ map Free subs) rhs;
- in
- list_abs_free (cargs @ subs @ ls @ rs, subst_rhs)
- 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 rpos = 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"
- ,rpos,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,rpos1,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,rpos,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 rpos <> rpos1 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,rpos,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
- fun typid(dtRek(_,id)) = id
- | typid(dtVar s) = implode (tl (explode s))
- | typid(dtTyp(_,id)) = id;
-
- fun index_vnames(vn::vns,tab) =
- (case assoc(tab,vn) of
- None => if vn mem vns
- then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
- else vn :: index_vnames(vns,tab)
- | Some(i) => (vn^(string_of_int i)) ::
- index_vnames(vns,(vn,i+1)::tab))
- | index_vnames([],tab) = [];
-
- fun mk_var_names types = index_vnames(map typid types,[]);
-
- (*search for free type variables and convert recursive *)
- fun analyse_types (cons, types, 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 types,
- mk_var_names types, 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 *'d) 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));
-
- fun C_exp name vns = name ^ opt_parens(commas vns);
-
- (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
- fun arg_eqs vns vns' =
- let fun mkeq(x,x') = x ^ "=" ^ x'
- in space_implode " & " (map mkeq (vns~~vns')) end
-
- (*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, _, vns, _) :: cs) =
- let val arity = length vns;
- 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;
-
- fun t_inducting ((_, name, types, vns, _) :: cs) =
- let
- val h = if null types then " P(" ^ name ^ ")"
- else " !!" ^ (space_implode " " vns) ^ "." ^
- (assumpt (types, vns, false)) ^
- "P(" ^ C_exp name vns ^ ")";
- 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, _, vns, _) =
- let val args = opt_parens(commas vns)
- 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_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
-
- fun rec_rule n (id,name,ts,vns,_) =
- let val args = commas vns
- val fargs = Args("f",",",1,num_of_cons)
- fun rarg vn = "," ^ t_rec ^ parens(fargs ^ "," ^ vn)
- val rargs = implode (map rarg (rek_vars ts vns))
- 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, _, vns, _) :: cs) =
- if null vns then Ci_ing cs
- else let val vns' = variantlist(vns,vns)
- in ("inject_" ^ id,
- "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
- ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
- end
- | Ci_ing [] = [];
-
- fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
- let val vns2' = variantlist(vns2,vns1)
- val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
- 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, _, vns, _), n) =
- let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (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
-end
-
-(*
-Informal description of functions used in datatype.ML for the Isabelle/HOL
-implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995)
-
-* subst_apps (fname,rpos) pairs t:
- substitute the term
- fname(ls,xk,rs)
- by
- yk(ls,rs)
- in t for (xk,yk) in pairs, where rpos = length ls.
- Applied with :
- fname = function name
- rpos = position of recursive argument
- pairs = list of pairs (xk,yk), where
- xk are the rec. arguments of the constructor in the pattern,
- yk is a variable with name derived from xk
- t = rhs of equation
-
-* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs)
- - filter recursive arguments from constructor arguments cargs,
- - perform substitutions on rhs,
- - derive list subs of new variable names yk for use in subst_apps,
- - abstract rhs with respect to cargs, subs, ls and rs.
-
-* dest_eq t
- destruct a term denoting an equation into lhs and rhs.
-
-* dest_req eq
- destruct an equation of the form
- name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs
- into
- - function name (name)
- - position of the first non-variable parameter (rpos)
- - the list of first rpos parameters (ls = [vl1..vlrpos])
- - the constructor (fst( dest_Const c) = Ci)
- - the arguments of the constructor (cargs = [vi1..vin])
- - the rest of the variables in the pattern (rs = [vr1..vrn])
- - the right hand side of the equation (rhs).
-
-* check_and_sort (n,its)
- check that n = length its holds, and sort elements of its by
- first component.
-
-* trans_recs thy cs' (eq1::eqs)
- destruct eq1 into name1, rpos1, ls1, etc..
- get constructor list with and without type (tcs resp. cs) from cs',
- for every equation:
- destruct it into (name,rpos,ls,c,cargs,rs,rhs)
- get typed constructor tc from c and tcs
- determine the index i of the constructor
- check function name and position of rec. argument by comparison
- with first equation
- check for repeated variable names in pattern
- derive function term f_i which is used as argument of the rec. combinator
- sort the terms f_i according to i and return them together
- with the function name and the parameter of the definition (ls).
-
-* Application:
-
- The rec. combinator is applied to the function terms resulting from
- trans_rec. This results in a function which takes the recursive arg.
- as first parameter and then the arguments corresponding to ls. The
- order of parameters is corrected by setting the rhs equal to
-
- list_abs_free
- (ls @ [(tname,dummyT)]
- ,list_comb(rec_comb
- , fns @ map Bound (0 ::(length ls downto 1))));
-
- Note the de-Bruijn indices counting the number of lambdas between the
- variable and its binding.
-*)