Datatype.ML

     Copyright    1994 TU Muenchen
 *)
 
 
 (*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
-val dtK = 5;
+local val dtK = 5
+in
 
 local open ThyParse in
 val datatype_decls =
   let fun cat s1 s2 = s1 ^ " " ^ s2;
 

         tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
     
       val typ =
          ident                  >> (cat "dtId" o quote)
         ||
-         type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^
+         type_var_list -- ident >> (fn (ts, id) => "dtComp (" ^ mk_list ts ^
   				  ", " ^ quote id ^ ")")
         ||
          tvar;
     
       val typ_list = "(" $$-- list1 typ --$$ ")" || empty;

 end;
 
 (*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;
-
-local open Syntax.Mixfix in
+                   dtComp of dt_type list * string |
+                   dtRek of dt_type list * string;
+
+local open Syntax.Mixfix
+      exception Impossible
+in
 fun add_datatype (typevars, tname, cons_list') thy = 
   let fun cat s1 s2 = s1 ^ " " ^ s2;
 
       val pars = parents "(" ")";
       val brackets = parents "[" "]";

                        (dtVar v) :: analyse typlist
                      else error ("Variable " ^ v ^ " is free.")
                   | analyse ((dtId s) :: typlist) =
                      if tname<>s then (dtId s) :: analyse typlist
                      else if null typevars then 
-                       Rek ([], tname) :: analyse typlist
+                       dtRek ([], tname) :: analyse typlist
                      else error (s ^ " used in different ways")
-                  | analyse (Comp (typl,s) :: typlist) =
-                     if tname <> s then Comp (analyse typl, s)
+                  | analyse (dtComp (typl,s) :: typlist) =
+                     if tname <> s then dtComp (analyse typl, s)
                                      :: analyse typlist
                      else if typevars = typl then
-                       Rek (typl, s) :: analyse typlist
+                       dtRek (typl, s) :: analyse typlist
                      else 
                        error (s ^ " used in different ways")
                   | analyse [] = []
-                  | analyse ((Rek _) :: _) = raise Impossible;
+                  | analyse ((dtRek _) :: _) = raise Impossible;
             in (cons, analyse typlist, syn) end;
 
       (*test if there are elements that are not recursive, i.e. if the type is
         not empty*)
       fun one_not_rek (cs : ('a * dt_type list * 'c) list) = 
-        let val contains_no_rek = forall (fn Rek _ => false | _ => true);
+        let val contains_no_rek = forall (fn dtRek _ => false | _ => true);
         in exists (contains_no_rek o #2) cs orelse
            error("Empty type not allowed!") end;
 
       val dummy = check_cons cons_list';
       val cons_list = map analyse_types cons_list';

 
       (*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
+        | pp_typ (dtComp (typvars, id)) = (pp_typlist1 typvars) ^ id
+        | pp_typ (dtRek (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);
 

             if (dtVar s) mem typlist then 
 	      create_typevar (dtVar (s ^ "'")) typlist 
             else s
         | create_typevar _ _ = raise Impossible;
 
-      fun assumpt (Rek _ :: ts, v :: vs ,found) =
+      fun assumpt (dtRek _ :: 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 ""

             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)
+      fun insert_types (dtRek (l,id) :: ts) tab =
+            insert_types ts (insert (dtRek(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 (dtComp (l,id) :: ts) tab =
+            insert_types ts (insert (dtComp(l,id)) id tab)
         | insert_types [] tab = tab;
 
-      fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs
+      fun update(dtRek _, s, v :: vs, (dtRek _) :: 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) =
+      fun update_n (dtRek r1, s, v :: vs, (dtRek 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 (dtRek r1, s, vs, ts, n+1))
+                       else v :: (update_n (dtRek 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 (_,_,[],[],_) = []

      |> add_arities arities
      |> add_consts consts
      |> add_trrules xrules
      |> add_axioms rules
   end
+end
 end;