Datatype.ML

ML-like datatype decalaration facility. Axiomatic.

(*  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);