diff -r 4f20eb450a64 -r 5e0570ea8b70 Datatype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Datatype.ML Fri Mar 18 20:33:32 1994 +0100 @@ -0,0 +1,499 @@ +(* Title: Datentypdeklarationen mit Isabelle + Author: Max Breitling + 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 induct_tac : string -> int -> tactic +end; + +signature DATATYPEDEF = +sig + val base : theory + val data : string + val declare_consts : bool +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; + +exception Impossible; + +open Parse; + +fun list_of1 ph = ph -- repeat("," $$-- ph) >> (op::); (* Redefinition *) + +(* ---------------------------------------------------------------------- *) + +val type_var = + typevar >> Var; + + +val type_var_list = + type_var >> (fn s => s::nil) + || + "(" $$-- list_of1 (type_var) --$$ ")" ; + + +val typ = + + id >> Id + || + type_var_list -- id >> Comp + || + type_var; + + +val typ_list = + (* + typ >> (fn t => t::nil) + output (std_out, || *) + "(" $$-- list_of1(typ) --$$ ")" + || + empty; + + +val cons = + + ( stg + || + id ) + -- typ_list; + + +fun constructs toks = +( + cons --$$ "|" -- constructs >> op:: + || + cons >> (fn c => c::nil) +) toks; + + +val type_def = + + (type_var_list || empty) -- id --$$ "=" -- constructs; + +(* --------------------------------------------------------------------- + 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 + +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 [] = "" +; + +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")); + +(* ------------------------------------------------------------------------ +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 analyse (deftyp,(cons,typlist) :: cs) = + (cons, analyseOne(deftyp,typlist))::analyse(deftyp,cs) + | analyse (_,[])=[]; + + +(* ------------------------------------------------------------------------ *) +(* 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 *) + +(* 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 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 (_,[]) = []; + +(* --------------------------------------------------------------------- *) + + +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 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 suc_expr n = if n=0 then "0" + else "Suc(" ^ suc_expr(n-1) ^ ")"; + + +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 (_, [], _) = []; + + +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)")] + 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)]; + + +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; + + +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 ""; + +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^")"; + +(* -------------------------------------------------------------------- *) +(* 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 _ [] = ""; + +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 _ _ _ [] = []; + +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 *) + +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 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; + +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); + +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 []; + + +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; + +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 thy = extend_theory base_thy thy_name + ([],[],types,[],arities,consts,sextopt) rules; + + +val inject = getaxioms rules_inject thy; + +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 cases = getaxioms rules_case thy; + +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); + + +