diff -r a94029edb01f -r bcd0ee8d71aa Datatype.ML --- a/Datatype.ML Fri Jul 08 12:01:55 1994 +0200 +++ b/Datatype.ML Fri Jul 08 17:22:58 1994 +0200 @@ -6,7 +6,8 @@ (*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 = @@ -25,7 +26,7 @@ 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; @@ -90,12 +91,12 @@ (*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; + dtComp of dt_type list * string | + dtRek of dt_type list * string; -exception Impossible; - -local open Syntax.Mixfix in +local open Syntax.Mixfix + exception Impossible +in fun add_datatype (typevars, tname, cons_list') thy = let fun cat s1 s2 = s1 ^ " " ^ s2; @@ -119,23 +120,23 @@ | 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; @@ -147,8 +148,8 @@ 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 @@ -197,7 +198,7 @@ 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 @@ -212,26 +213,26 @@ 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)) @@ -384,4 +385,5 @@ |> add_trrules xrules |> add_axioms rules end -end; \ No newline at end of file +end +end;