(* 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 simps : 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;
val simps = inject @ ineq @ cases;
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);