--- a/Datatype.ML Wed Jun 15 19:28:35 1994 +0200
+++ b/Datatype.ML Fri Jun 17 14:15:38 1994 +0200
@@ -1,502 +1,397 @@
-(* Title: Datentypdeklarationen mit Isabelle
- Author: Max Breitling
+(* Title: HOL/Datatype
+ ID: $Id$
+ Author: Max Breitling / Carsten Clasohm
Copyright 1994 TU Muenchen
*)
-signature DATATYPE =
-sig
- val thy : theory
- val induct : thm
- val inject : thm list
- val ineq : thm list
- val cases : thm list
- val simps : thm list
- val induct_tac : string -> int -> tactic
-end;
+(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
+val dtK = 5;
+
+local open ThyParse in
+val datatype_decls =
+ let fun cat s1 s2 = s1 ^ " " ^ s2;
+
+ val pars = parents "(" ")";
+ val brackets = parents "[" "]";
+
+ val mk_list = brackets o commas;
+
+ val tvar = type_var >> cat "dtVar";
-signature DATATYPEDEF =
-sig
- val base : theory
- val data : string
- val declare_consts : bool
+ val type_var_list =
+ tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
+
+ val typ =
+ ident >> (cat "dtId" o quote)
+ ||
+ type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^
+ ", " ^ quote id ^ ")")
+ ||
+ tvar;
+
+ val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
+
+ val cons = name -- typ_list;
+
+ fun constructs ts =
+ ( cons --$$ "|" -- constructs >> op::
+ ||
+ cons >> (fn c => [c])) ts;
+
+ val mk_cons = map (fn (s, ts) => pars (s ^ ", " ^ mk_list ts));
+
+ (*remove all quotes from a string*)
+ fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s));
+
+ (*generate names of ineq axioms*)
+ fun rules_ineq cs tname =
+ let (*combine all constructor names with all others w/o duplicates*)
+ fun negOne _ [] = []
+ | negOne (c : string * 'b) ((c2 : string * 'b) :: cs) =
+ quote ("ineq_" ^ rem_quotes (#1 c) ^ "_" ^
+ rem_quotes (#1 c2)) :: negOne c cs;
+
+ fun neg1 [] = []
+ | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
+ in if length cs < dtK then neg1 cs
+ else map (fn n => quote (tname ^ "_ord" ^ string_of_int n))
+ (0 upto (length cs))
+ end;
+
+ fun arg1 (id, ts) = not (null ts);
+
+ (*generate string calling 'add_datatype'*)
+ fun mk_params ((ts, tname), cons) =
+ ("|> add_datatype\n" ^
+ pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]),
+ "structure " ^ tname ^ " =\n\
+ \struct\n\
+ \ val inject = map (get_axiom thy) " ^
+ mk_list (map (fn (s,_) => quote ("inject_" ^ rem_quotes s))
+ (filter arg1 cons)) ^ ";\n\
+ \ val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "")
+ ^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^
+ (if length cons < dtK then
+ " in ineq' @ (map (fn t => sym COMP (t RS contrapos)) ineq') end"
+ else "") ^ ";\n\
+ \ val induct = get_axiom thy \"induct\";\n\
+ \ val cases = map (get_axiom thy) " ^
+ mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s))
+ cons) ^ ";\n\
+ \ val simps = inject @ ineq @ cases;\n\
+ \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
+ \end;\n");
+ in (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params end
end;
-
-functor DatatypeFUN(Input: DATATYPEDEF) : DATATYPE =
-struct
-
-structure Keyword =
- struct
- val alphas = []
- val symbols = ["(",")",",","|","="]
- end;
-
-val K = 5; (* Diese Schranke enscheidet zwischen den beiden
- Ci_neg-Axiomen-Schemata *)
-
-structure Lex = LexicalFUN (Keyword);
-structure Parse = ParseFUN(Lex);
-
-datatype Typ = Var of string |
- Id of string |
- Comp of Typ list * string |
- Rek of Typ list * string;
-
-type InternalRep = (Typ list * string) * (string * Typ list) list;
+(*used for constructor parameters*)
+datatype dt_type = dtVar of string |
+ dtId of string |
+ Comp of dt_type list * string |
+ Rek of dt_type list * string;
exception Impossible;
-open Parse;
-
-fun list_of1 ph = ph -- repeat("," $$-- ph) >> (op::); (* Redefinition *)
+local open Syntax.Mixfix in
+fun add_datatype (typevars, tname, cons_list') thy =
+ let fun cat s1 s2 = s1 ^ " " ^ s2;
-(* ---------------------------------------------------------------------- *)
-
-val type_var =
- typevar >> Var;
+ val pars = parents "(" ")";
+ val brackets = parents "[" "]";
+ val mk_list = brackets o commas;
-val type_var_list =
- type_var >> (fn s => s::nil)
- ||
- "(" $$-- list_of1 (type_var) --$$ ")" ;
-
-
-val typ =
+ (*check if constructor names are unique*)
+ fun check_cons cs =
+ (case findrep (map fst cs) of
+ [] => true
+ | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"));
- id >> Id
- ||
- type_var_list -- id >> Comp
- ||
- type_var;
-
+ (*search for free type variables and convert recursive *)
+ fun analyse ((cons, typlist) :: cs) =
+ let fun analyseOne ((dtVar v) :: typlist) =
+ if ((dtVar v) mem typevars) then
+ (dtVar v) :: analyseOne typlist
+ else error ("Variable " ^ v ^ " is free.")
+ | analyseOne ((dtId s) :: typlist) =
+ if tname<>s then (dtId s) :: analyseOne typlist
+ else if null typevars then
+ Rek ([], tname) :: analyseOne typlist
+ else error (s ^ " used in different ways")
+ | analyseOne (Comp (typl,s) :: typlist) =
+ if tname <> s then Comp (analyseOne typl, s)
+ :: analyseOne typlist
+ else if typevars = typl then
+ Rek (typl, s) :: analyseOne typlist
+ else
+ error (s ^ " used in different ways")
+ | analyseOne [] = []
+ | analyseOne ((Rek _) :: _) = raise Impossible;
+ in (cons, analyseOne typlist) :: analyse cs end
+ | analyse [] = [];
-val typ_list =
- (*
- typ >> (fn t => t::nil)
- output (std_out, || *)
- "(" $$-- list_of1(typ) --$$ ")"
- ||
- empty;
-
-
-val cons =
-
- ( stg
- ||
- id )
- -- typ_list;
-
+ (*test if there are elements that are not recursive, i.e. if the type is
+ not empty*)
+ fun one_not_rek cs =
+ let val contains_no_rek = forall (fn Rek _ => false | _ => true);
+ in exists (contains_no_rek o snd) cs orelse
+ error("Empty type not allowed!") end;
-fun constructs toks =
-(
- cons --$$ "|" -- constructs >> op::
- ||
- cons >> (fn c => c::nil)
-) toks;
-
-
-val type_def =
+ val _ = check_cons cons_list';
+ val cons_list = analyse cons_list';
+ val _ = one_not_rek cons_list;
- (type_var_list || empty) -- id --$$ "=" -- constructs;
+ (*Pretty printers for type lists;
+ pp_typlist1: parentheses, pp_typlist2: brackets*)
+ fun pp_typ (dtVar s) = s
+ | pp_typ (dtId s) = s
+ | pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id
+ | pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id
+ and
+ pp_typlist' ts = commas (map pp_typ ts)
+ and
+ pp_typlist1 ts = if null ts then "" else pars (pp_typlist' ts);
-(* ---------------------------------------------------------------------
- Pretty-Printer fuer Typlisten
- Variante 1 hat runde Klammern, Variante2 hat ganz aussen eckige Klammern
-*)
-fun pp_typ (Var s) = s
- | pp_typ (Id s) =s
- | pp_typ (Comp (typvars,id)) = (pp_typlist1 typvars) ^ id
- | pp_typ (Rek (typvars,id)) = (pp_typlist1 typvars) ^ id
+ fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
+
+ fun Args(var, delim, n, m) = if n = m then var ^ string_of_int(n)
+ else var ^ string_of_int(n) ^ delim ^
+ Args(var, delim, n+1, m);
-and
- pp_typlist' (typ::typ2::ts) = (pp_typ typ) ^ "," ^ (pp_typlist' (typ2::ts))
- | pp_typlist' (typ::nil) = pp_typ typ
- | pp_typlist' [] = raise Impossible
-
-and
- pp_typlist1 (typ::ts) = "(" ^ (pp_typlist' (typ::ts)) ^ ")"
- | pp_typlist1 [] = ""
-;
+ (* Generate syntax translation for case rules *)
+ fun calc_xrules c_nr y_nr ((c, typlist) :: cs) =
+ let val arity = length typlist;
+ val body = "z" ^ string_of_int(c_nr);
+ val args1 = if arity=0 then ""
+ else pars (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 (c ^ 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(x, " ^ scnd_part ^ ")" )]
+ end;
-fun pp_typlist2 (typ::ts) = "[" ^ pp_typlist' (typ::ts) ^ "]"
- | pp_typlist2 [] = ""
-
-(* ----------------------------------------------------------------------- *)
-
-(* Ueberprueft, ob die Konstruktoren paarweise verschieden sind *)
-
-fun check_cons cs =
- (case findrep (map fst cs) of
- [] => true
- | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"));
+ (*type declarations for constructors*)
+ fun const_types ((c, typlist) :: cs) =
+ (c,
+ (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
+ pp_typlist1 typevars ^ tname, NoSyn)
+ :: const_types cs
+ | const_types [] = [];
-(* ------------------------------------------------------------------------
-Diese Funktion ueberprueft, ob alle Typvariablen nichtfrei sind und wandelt
-erkannte rekursive Bezuege in den "Rek"-Konstruktor um *)
-
-fun analyseOne ((typevars,id), (Var v)::typlist) =
- if ((Var v) mem typevars) then (Var v)::analyseOne((typevars,id),typlist)
- else error("Variable "^v^" is free.")
- | analyseOne ((typevars,id), (Id s)::typlist) =
- if id<>s then (Id s)::analyseOne((typevars,id),typlist)
- else if typevars=[] then Rek([],id)
- ::analyseOne((typevars,id),typlist)
- else error(s^" used in different ways")
- | analyseOne ((typevars,id),(Comp(typl,s))::typlist) =
- if id<>s then Comp(analyseOne((typevars,id),typl),s)
- ::analyseOne((typevars,id),typlist)
- else if typevars=typl then
- Rek(typl,s)::analyseOne((typevars,id),typlist)
- else
- error(s ^ " used in different ways")
- | analyseOne (_,[]) = []
- | analyseOne (_,(Rek _)::_) = raise Impossible;
+ fun create_typevar (dtVar s) typlist =
+ if (dtVar s) mem typlist then
+ create_typevar (dtVar (s ^ "'")) typlist
+ else s
+ | create_typevar _ _ = raise Impossible;
+ fun assumpt (Rek _ :: 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 analyse (deftyp,(cons,typlist) :: cs) =
- (cons, analyseOne(deftyp,typlist))::analyse(deftyp,cs)
- | analyse (_,[])=[];
-
+ (*insert type with suggested name 'varname' into table*)
+ fun insert typ varname ((t, s, n) :: xs) =
+ if typ = t then (t, s, n+1) :: xs
+ else if varname = s then (t,s,n) :: (insert typ (varname ^ "'") xs)
+ else (t,s,n) :: (insert typ varname xs)
+ | insert typ varname [] = [(typ, varname, 1)];
-(* ------------------------------------------------------------------------ *)
-(* testet, ob nicht nur rekusive Elemente in den Typen vorkommen, also ob
- der definierte Typ nichtleer ist *)
-
-val contains_no_rek = forall (fn Rek _ => false | _ => true);
-
-fun one_not_rek cs = exists (contains_no_rek o snd) cs orelse
- error("Empty type not allowed!");
-
-
-(* ------------------------------------------------------------------------ *)
-(* Hilfsfunktionen *)
+ fun insert_types (Rek (l,id) :: ts) tab =
+ insert_types ts (insert (Rek(l,id)) id tab)
+ | insert_types ((dtVar s) :: ts) tab =
+ insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab)
+ | insert_types ((dtId s) :: ts) tab =
+ insert_types ts (insert (dtId s) s tab)
+ | insert_types (Comp (l,id) :: ts) tab =
+ insert_types ts (insert (Comp(l,id)) id tab)
+ | insert_types [] tab = tab;
-(* gibt 'var_n' bis 'var_m' aus, getrennt durch 'delim' *)
-fun Args(var,delim,n,m) = if n=m then var ^ string_of_int(n)
- else var ^ string_of_int(n) ^delim^ Args(var,delim,n+1,m);
-
-(* gibt 'name_1', ... , 'name_n' zurueck *)
-fun C_exp(name,n,var) =
- if n>0 then name ^ "(" ^ Args(var,",",1,n) ^ ")"
- else name;
-
-(* gibt 'x_n = y_n, ... , x_m = y_m' zurueck *)
-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);
-
-(* --------------------------------------------------------------------- *)
-(* Ausgabe der Typdeklarationen fuer die einzelnen Konstruktoren *)
+ fun update(Rek _, s, v :: vs, (Rek _) :: 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 (Rek r1, s, v :: vs, (Rek r2) :: ts, n) =
+ if r1 = r2 then (s ^ string_of_int n) ::
+ (update_n (Rek r1, s, vs, ts, n+1))
+ else v :: (update_n (Rek 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;
-fun const_types ((typevars,id),((c,typlist)::cs)) =
- ([c],
- (if typlist =[] then "" else pp_typlist2(typlist) ^ " => ") ^
- pp_typlist1(typevars) ^ id
- )
- :: const_types ((typevars,id),cs)
- | const_types (_,[]) = [];
+ (*insert type variables into table*)
+ fun convert ((t, s, n) :: ts) var_list typ_list =
+ let val h = if n=1 then update (t, s, var_list, typ_list)
+ else update_n (t, s, var_list, typ_list, 1)
+ in convert ts h typ_list end
+ | convert [] var_list _ = var_list;
-(* --------------------------------------------------------------------- *)
-
+ fun empty_list n = replicate n "";
-fun Ci_ing (c :: cs) =
- let val (name,typlist) = c
- val arity = length typlist
- in
- if arity>0
- then ("inject_" ^ name,
- "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") ^ ") = ("
- ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs)
-
- else (Ci_ing cs)
- end
- | Ci_ing [] = [];
+ fun t_inducting ((name, typl) :: cs) =
+ let val tab = insert_types typl [];
+ val arity = length typl;
+ val var_list = convert tab (empty_list arity) typl;
+ 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 Ci_negOne (c::nil) = []
- | Ci_negOne (c::c1::cs) =
- let val (name1,tl1) = c
- val (name2,tl2) = c1
- val arit1 = length tl1
- val arit2 = length tl2
- val h = "(" ^ C_exp(name1,arit1,"x") ^ "~=" ^
- C_exp(name2,arit2,"y") ^ ")"
- in ("ineq_"^name1^"_"^name2,h):: (Ci_negOne (c::cs))
- end
- | Ci_negOne [] = [];
-
-fun Ci_neg1 (c1::c2::nil) = Ci_negOne(c1::c2::nil)
- | Ci_neg1 (c1::c2::cs) = Ci_negOne(c1::c2::cs) @ Ci_neg1(c2::cs)
- | Ci_neg1 _ = [];
+ fun case_typlist typevar ((c, typlist) :: cs) =
+ let val h = if (length typlist) > 0 then
+ (pp_typlist2 typlist) ^ "=>"
+ else ""
+ in "," ^ h ^ typevar ^ (case_typlist typevar cs) end
+ | case_typlist _ [] = "";
-fun suc_expr n = if n=0 then "0"
- else "Suc(" ^ suc_expr(n-1) ^ ")";
-
+ fun case_rules t_case arity n ((id, typlist) :: cs) =
+ let val args = if null typlist then ""
+ else "(" ^ Args ("x", ",", 1, length typlist) ^ ")"
+ in (t_case ^ "_" ^ id,
+ t_case ^ "(" ^ id ^ args ^ "," ^ Args ("f", ",", 1, arity)
+ ^ ") = f" ^ string_of_int(n) ^ args)
+ :: (case_rules t_case arity (n+1) cs)
+ end
+ | case_rules _ _ _ [] = [];
-fun Ci_neg2equals (ord_t,((c,typlist)::cs), n) =
- let val h = ord_t ^ "(" ^ (C_exp(c,length typlist,"x")) ^ ") = " ^
- (suc_expr n)
- in
- (ord_t^(string_of_int(n+1)),h) :: (Ci_neg2equals (ord_t, cs ,n+1))
- end
- | Ci_neg2equals (_, [], _) = [];
+ val datatype_arity = length typevars;
-
-fun Ci_neg2 ((typlist,id),conslist) =
- let val ord_t = id ^ "_ord"
- in
- (Ci_neg2equals (ord_t, conslist, 0)) @
- [(ord_t^"0",
- "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")]
+ val sign = sign_of thy;
+ val {tsig, ...} = Sign.rep_sg sign;
+
+ val types =
+ let val {args, ...} = Type.rep_tsig tsig;
+ in case assoc (args, tname) of
+ None => [(tname, datatype_arity, NoSyn)]
+ | Some _ => []
end;
-
-(* --------------------------------------------------------------------- *)
-(* Die Funktionen fuer das Induktionsaxiom, mit komplizierer Vergabestrategie
- fuer die Variablennamen *)
-
-(* fuegt einen Typ mit dem vorgeschlagenen Namen varname in die Tabelle ein *)
-fun insert typ varname ((t,s,n)::xs) =
- if typ=t then (t,s,n+1)::xs
- else if varname=s then (t,s,n)::(insert typ (varname^"'") xs)
- else (t,s,n)::(insert typ varname xs)
- | insert typ varname [] = [(typ,varname,1)];
+ val arities =
+ let val {coreg, ...} = Type.rep_tsig tsig;
+ val term_list = replicate datatype_arity ["term"];
+ in case assoc (coreg, tname) of
+ None => [(tname, term_list, ["term"])]
+ | Some _ => []
+ end;
-
-fun insert_types ((Rek(l,id))::ts) tab =
- insert_types ts (insert (Rek(l,id)) id tab)
- | insert_types ((Var s)::ts) tab =
- insert_types ts (insert (Var s) (implode(tl(explode s))) tab)
- | insert_types ((Id s)::ts) tab =
- insert_types ts (insert (Id s) s tab)
- | insert_types (Comp(l,id)::ts) tab =
- insert_types ts (insert (Comp(l,id)) id tab)
- | insert_types [] tab = tab;
-
+ val datatype_name = pp_typlist1 typevars ^ tname;
-fun update(Rek(_),s,v::vs,(Rek(_))::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(Rek(r1),s,v::vs,(Rek(r2))::ts,n) =
- if r1=r2 then (s^(string_of_int n))::(update_n(Rek(r1),s,vs,ts,n+1))
- else v::(update_n(Rek(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;
-
-(* geht durch die Tabelle und traegt die Typvariablen ein *)
-fun convert ((t,s,n)::ts) var_list typ_list =
- let val h = ( if n=1 then update(t,s,var_list,typ_list)
- else update_n(t,s,var_list,typ_list,1))
- in convert ts h typ_list
- end
- | convert [] var_list _ = var_list;
-
-
-fun empty_list n = replicate n "";
+ val (case_const, rules_case) =
+ let val typevar = create_typevar (dtVar "'beta") typevars;
+ val t_case = tname ^ "_case";
+ val arity = length cons_list;
+ val dekl = (t_case, "[" ^ pp_typlist1 typevars ^ tname ^
+ case_typlist typevar cons_list ^ "]=>" ^ typevar, NoSyn)
+ :: nil;
+ val rules = case_rules t_case arity 1 cons_list;
+ in (dekl, rules) end;
-fun assumpt (Rek(_)::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,typl)::cs) =
- let val tab = insert_types typl []
- val arity = length typl
- val var_list = convert tab (empty_list arity) typl
- val h = if arity=0 then " P(" ^ name ^ ")"
- else " !!" ^ (space_implode " " var_list) ^ "." ^
- (assumpt (typl, var_list, false))
- ^ "P(" ^ name ^ "(" ^ (space_implode "," 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^")";
+ val consts =
+ let val {const_tab, ...} = Sign.rep_sg sign;
+ fun const_undef (c, _, _) = case Symtab.lookup (const_tab, c) of
+ Some _ => false
+ | None => true;
+ in (filter const_undef (const_types cons_list)) @
+ (if length cons_list < dtK then []
+ else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
+ @ case_const
+ end;
-(* -------------------------------------------------------------------- *)
-(* Die Funktionen fuer die t_case - Funktion *)
-fun case_typlist typevar ((c,typlist)::cs) =
- let val h = if (length typlist) > 0 then (pp_typlist2 typlist) ^ "=>"
- else ""
- in "," ^ h ^ typevar ^ (case_typlist typevar cs)
- end
- | case_typlist _ [] = "";
+ (*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 case_rules t_case arity n ((id,typlist)::cs) =
- let val args = if (length typlist)>0 then "("^Args("x",",",1,length typlist)
- ^ ")"
- else ""
- in (t_case ^ "_" ^ id,
- t_case ^ "(" ^ id ^ args ^ "," ^ Args("f",",",1,arity) ^ ") = f" ^
- string_of_int(n) ^ args)
- :: (case_rules t_case arity (n+1) cs)
- end
- | case_rules _ _ _ [] = [];
+ (*generate 'name_1', ..., 'name_n'*)
+ fun C_exp(name, n, var) =
+ if n > 0 then name ^ "(" ^ Args (var, ",", 1, n) ^ ")"
+ else name;
-fun create_typevar (Var s) typlist =
- if (Var s) mem typlist then create_typevar (Var (s^"'")) typlist else s
-| create_typevar _ _ = raise Impossible;
-
-
-fun case_consts ((typlist,id),conslist) =
- let val typevar = create_typevar (Var "'beta") typlist
- val t_case = id ^ "_case"
- val arity = length conslist
- val dekl = ([t_case],"[" ^ (pp_typlist1 typlist) ^ id ^
- (case_typlist typevar conslist) ^ "]=>" ^ typevar)::nil
- val rules = case_rules t_case arity 1 conslist
- in (dekl,rules)
- end;
-(* ------------------------------------------------------------------------- *)
-(* Die Funktionen fuer das Erzeugen der Syntax-Umsetzung der case-Regeln *)
+ (*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);
-fun calc_xrules c_nr y_nr ((c,typlist)::cs) =
- let val arity = length typlist
- val body = "z" ^ string_of_int(c_nr)
- val args1 = if arity=0 then ""
- else "("^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 cs = [] then ("","")
- else let val (h1,h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
- in (" | " ^ h1, ", " ^ h2)
- end
- in (c^args1^" => "^body^rest1,
- args2 ^ body ^ rest2)
- end
- | calc_xrules _ _ [] = raise Impossible;
-
-fun xrules ((typlist,id),conslist) =
- let val (first_part,scnd_part) = calc_xrules 1 1 conslist
- in [("logic","case x of " ^ first_part) <->
- ("logic",id ^ "_case(x," ^ scnd_part ^ ")" )]
- end;
-
-(* ------------------------------------------------------------------------- *)
+ fun Ci_ing (c :: cs) =
+ let val (name, typlist) = c
+ val arity = length typlist
+ in if arity>0
+ then ("inject_" ^ name,
+ "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y")
+ ^ ") = (" ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs)
+ else (Ci_ing cs)
+ end
+ | Ci_ing [] = [];
-fun parse InputString =
- let val (deftyp,conslist') = ((reader type_def) o explode) InputString
- val test = check_cons(conslist')
- val conslist = analyse (deftyp,conslist')
- val test2 = one_not_rek conslist
- in (deftyp,conslist)
- end;
-
-
-(* -------------------------------------------------------------------------- *)
-
-val Datatype = parse Input.data;
-
-val datatype_id = (#2 o #1) Datatype;
-val datatype_arity = length ((#1 o #1) Datatype);
-val cons_list = #2 Datatype;
-val datatype_name = pp_typlist1((#1 o #1) Datatype) ^ datatype_id;
+ fun Ci_negOne _ [] = []
+ | Ci_negOne c (c1::cs) =
+ let val (name1, tl1) = c
+ val (name2, tl2) = c1
+ val arit1 = length tl1
+ val arit2 = length tl2
+ val h = "(" ^ C_exp(name1, arit1, "x") ^ "~=" ^
+ C_exp(name2, arit2, "y") ^ ")"
+ in ("ineq_" ^ name1 ^ "_" ^ name2, h):: (Ci_negOne c cs)
+ end;
-val thy_name = datatype_id;
-
-val base_thy = if length(cons_list) < K then Input.base
- else merge_theories(Input.base,Arith.thy);
-
-val (case_const,rules_case) = case_consts Datatype;
-
-val q = (case_const);
+ fun Ci_neg1 [] = []
+ | Ci_neg1 (c1::cs) = Ci_negOne c1 cs @ Ci_neg1 cs;
-val types = if Input.declare_consts then [([datatype_id],datatype_arity)]
- else [];
-
-fun term_list n = replicate n ["term"];
-
-val arities :(string list * (sort list * class))list
- = if Input.declare_consts then
- [([datatype_id],((term_list datatype_arity),"term"))]
- else [];
-
+ fun suc_expr n =
+ if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
-val consts = (if Input.declare_consts then
- (const_types Datatype) else []) @
- (if length(cons_list) < K then []
- else [([datatype_id^"_ord"],datatype_name^"=>nat")]) @
- case_const;
-
-val sextopt = Some(NewSext{mixfix=[],
- xrules=(xrules Datatype),
- parse_ast_translation=[],
- parse_translation=[],
- print_translation=[],
- print_ast_translation=[]});
-
-val rules_ineq = if (length cons_list) < K then Ci_neg1 cons_list
- else Ci_neg2 Datatype;
+ fun Ci_neg2equals (ord_t, ((c, typlist) :: cs), n) =
+ let val h = ord_t ^ "(" ^ (C_exp(c, length typlist, "x")) ^ ") = " ^
+ (suc_expr n)
+ in (ord_t ^ (string_of_int(n+1)), h)
+ :: (Ci_neg2equals (ord_t, cs , n+1))
+ end
+ | Ci_neg2equals (_, [], _) = [];
-val rules_inject = Ci_ing cons_list;
-
-
-val rule_induct = ("induct",t_induct cons_list datatype_id);
-
-val rules = rule_induct::(rules_inject @ rules_ineq @ rules_case);
-
-fun getaxioms ((name,axiom)::axioms) thy = (get_axiom thy name)::
- (getaxioms axioms thy)
- | getaxioms [] _ = [];
-
-fun sym_ineq (t::ts) = (sym COMP (t RS contrapos)) :: (sym_ineq ts)
- | sym_ineq [] = [];
-
-(* -----------------------------------------------------------------------*)
-(* Das folgende wird exportiert *)
+ val Ci_neg2 =
+ let val ord_t = tname ^ "_ord";
+ in (Ci_neg2equals (ord_t, cons_list, 0)) @
+ [(ord_t^"0",
+ "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")]
+ end;
-val thy = extend_theory base_thy thy_name
- ([],[],types,[],arities,consts,sextopt) rules;
-
-
-val inject = getaxioms rules_inject thy;
+ val rules_ineq = if length cons_list < dtK then Ci_neg1 cons_list
+ else Ci_neg2;
-val ineq = let val ineq' = getaxioms rules_ineq thy
- in if length(cons_list) < K then ineq' @ (sym_ineq ineq')
- else ineq'
- end;
-
-val induct = get_axiom thy "induct";
+ val rules_inject = Ci_ing cons_list;
-val cases = getaxioms rules_case thy;
-
-val simps = inject @ ineq @ cases;
+ val rule_induct = ("induct", t_induct cons_list tname);
-fun induct_tac a = res_inst_tac [(datatype_id,a)] induct;
-
-(* ------------------------------------------------------------------- *)
-
-
-end;
-
-
-
-functor Datatype(val base:theory and data:string) : DATATYPE =
- DatatypeFUN(val base=base and data=data and declare_consts=true);
-
-functor DeclaredDatatype(val base:theory and data:string) : DATATYPE =
- DatatypeFUN(val base=base and data=data and declare_consts=false);
-
-
-
+ val rules =rule_induct :: (rules_inject @ rules_ineq @ rules_case);
+ in thy
+ |> add_types types
+ |> add_arities arities
+ |> add_consts consts
+ |> add_trrules xrules
+ |> add_axioms rules
+ end
+end;
\ No newline at end of file