--- /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);
+
+
+