diff -r efd3e5a2d493 -r d3d727449d7b Datatype.ML --- 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