# HG changeset patch # User clasohm # Date 773661715 -7200 # Node ID a94029edb01fd6f28489e2aea7df96bf24c17a45 # Parent 5c7a69cef18bc95f0231694c9d455dc39266a554 added mixfix annotations to constructor declarations diff -r 5c7a69cef18b -r a94029edb01f Datatype.ML --- a/Datatype.ML Wed Jun 29 12:04:04 1994 +0200 +++ b/Datatype.ML Fri Jul 08 12:01:55 1994 +0200 @@ -32,14 +32,15 @@ val typ_list = "(" $$-- list1 typ --$$ ")" || empty; - val cons = name -- typ_list; + val cons = name -- typ_list -- opt_mixfix; fun constructs ts = ( cons --$$ "|" -- constructs >> op:: || cons >> (fn c => [c])) ts; - val mk_cons = map (fn (s, ts) => pars (s ^ ", " ^ mk_list ts)); + val mk_cons = map (fn ((s, ts), syn) => + pars (commas [s, mk_list ts, syn])); (*remove all quotes from a string*) fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s)); @@ -48,9 +49,10 @@ fun rules_ineq cs tname = let (*combine all constructor names with all others w/o duplicates*) fun negOne _ [] = [] - | negOne (c : string * 'b) ((c2 : string * 'b) :: cs) = - quote ("ineq_" ^ rem_quotes (#1 c) ^ "_" ^ - rem_quotes (#1 c2)) :: negOne c cs; + | negOne (c : (string * 'a) * 'b) ((c2 : (string * 'a) * 'b) + :: cs) = + quote ("ineq_" ^ rem_quotes (#1 (#1 c)) ^ "_" ^ + rem_quotes (#1 (#1 c2))) :: negOne c cs; fun neg1 [] = [] | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs) @@ -59,16 +61,16 @@ (0 upto (length cs)) end; - fun arg1 (id, ts) = not (null ts); + fun arg1 ((_, ts), _) = not (null ts); - (*generate string calling 'add_datatype'*) + (*generate string for calling 'add_datatype'*) fun mk_params ((ts, tname), cons) = ("|> add_datatype\n" ^ pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]), "structure " ^ tname ^ " =\n\ \struct\n\ \ val inject = map (get_axiom thy) " ^ - mk_list (map (fn (s,_) => quote ("inject_" ^ rem_quotes s)) + mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s)) (filter arg1 cons)) ^ ";\n\ \ val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "") ^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^ @@ -77,8 +79,8 @@ else "") ^ ";\n\ \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ \ val cases = map (get_axiom thy) " ^ - mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s)) - cons) ^ ";\n\ + mk_list (map (fn ((s,_),_) => + quote(tname ^ "_case_" ^ rem_quotes s)) cons) ^ ";\n\ \ val simps = inject @ ineq @ cases;\n\ \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ \end;\n"); @@ -103,44 +105,43 @@ val mk_list = brackets o commas; (*check if constructor names are unique*) - fun check_cons cs = - (case findrep (map fst cs) of + fun check_cons (cs : (string * 'b * 'c) list) = + (case findrep (map #1 cs) of [] => true | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice")); (*search for free type variables and convert recursive *) - fun analyse ((cons, typlist) :: cs) = - let fun analyseOne ((dtVar v) :: typlist) = + fun analyse_types (cons, typlist, syn) = + let fun analyse ((dtVar v) :: typlist) = if ((dtVar v) mem typevars) then - (dtVar v) :: analyseOne typlist + (dtVar v) :: analyse typlist else error ("Variable " ^ v ^ " is free.") - | analyseOne ((dtId s) :: typlist) = - if tname<>s then (dtId s) :: analyseOne typlist + | analyse ((dtId s) :: typlist) = + if tname<>s then (dtId s) :: analyse typlist else if null typevars then - Rek ([], tname) :: analyseOne typlist + Rek ([], tname) :: analyse typlist else error (s ^ " used in different ways") - | analyseOne (Comp (typl,s) :: typlist) = - if tname <> s then Comp (analyseOne typl, s) - :: analyseOne typlist + | analyse (Comp (typl,s) :: typlist) = + if tname <> s then Comp (analyse typl, s) + :: analyse typlist else if typevars = typl then - Rek (typl, s) :: analyseOne typlist + Rek (typl, s) :: analyse typlist else error (s ^ " used in different ways") - | analyseOne [] = [] - | analyseOne ((Rek _) :: _) = raise Impossible; - in (cons, analyseOne typlist) :: analyse cs end - | analyse [] = []; + | analyse [] = [] + | analyse ((Rek _) :: _) = 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 = + fun one_not_rek (cs : ('a * dt_type list * 'c) list) = let val contains_no_rek = forall (fn Rek _ => false | _ => true); - in exists (contains_no_rek o snd) cs orelse + in exists (contains_no_rek o #2) cs orelse error("Empty type not allowed!") end; - val _ = check_cons cons_list'; - val cons_list = analyse cons_list'; - val _ = one_not_rek cons_list; + val dummy = check_cons cons_list'; + val cons_list = map analyse_types cons_list'; + val dummy = one_not_rek cons_list; (*Pretty printers for type lists; pp_typlist1: parentheses, pp_typlist2: brackets*) @@ -160,8 +161,9 @@ Args(var, delim, n+1, m); (* Generate syntax translation for case rules *) - fun calc_xrules c_nr y_nr ((c, typlist) :: cs) = - let val arity = length typlist; + fun calc_xrules c_nr y_nr ((id, typlist, syn) :: cs) = + let val name = const_name id syn; + val arity = length typlist; val body = "z" ^ string_of_int(c_nr); val args1 = if arity=0 then "" else pars (Args ("y", ",", y_nr, y_nr+arity-1)); @@ -169,10 +171,10 @@ else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) ^ ". "; val (rest1,rest2) = - if null cs then ("", "") + if null 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 + in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end | calc_xrules _ _ [] = raise Impossible; val xrules = @@ -182,10 +184,10 @@ end; (*type declarations for constructors*) - fun const_types ((c, typlist) :: cs) = - (c, + fun const_types ((id, typlist, syn) :: cs) = + (id, (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ - pp_typlist1 typevars ^ tname, NoSyn) + pp_typlist1 typevars ^ tname, syn) :: const_types cs | const_types [] = []; @@ -246,8 +248,9 @@ fun empty_list n = replicate n ""; - fun t_inducting ((name, typl) :: cs) = - let val tab = insert_types typl []; + fun t_inducting ((id, typl, syn) :: cs) = + let val name = const_name id syn; + 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 ^ ")" @@ -255,24 +258,25 @@ (assumpt (typl, var_list, false)) ^ "P(" ^ name ^ "(" ^ (commas var_list) ^ "))"; val rest = t_inducting cs; - in if rest="" then h else h ^ "; " ^ rest end + in if rest = "" then h else h ^ "; " ^ rest end | t_inducting [] = ""; fun t_induct cl typ_name= "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; - fun case_typlist typevar ((c, typlist) :: cs) = + fun case_typlist typevar ((_, 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 null typlist then "" + fun case_rules t_case arity n ((id, typlist, syn) :: cs) = + let val name = const_name id syn; + val args = if null typlist then "" else "(" ^ Args ("x", ",", 1, length typlist) ^ ")" in (t_case ^ "_" ^ id, - t_case ^ "(" ^ id ^ args ^ "," ^ Args ("f", ",", 1, arity) + t_case ^ "(" ^ name ^ args ^ "," ^ Args ("f", ",", 1, arity) ^ ") = f" ^ string_of_int(n) ^ args) :: (case_rules t_case arity (n+1) cs) end @@ -280,23 +284,11 @@ val datatype_arity = length typevars; - val sign = sign_of thy; - val {tsig, ...} = Sign.rep_sg sign; - - val types = - let val {args, ...} = Type.rep_tsig tsig; - in case assoc (args, tname) of - None => [(tname, datatype_arity, NoSyn)] - | Some _ => [] - end; + val types = [(tname, datatype_arity, NoSyn)]; val arities = - let val {coreg, ...} = Type.rep_tsig tsig; - val term_list = replicate datatype_arity ["term"]; - in case assoc (coreg, tname) of - None => [(tname, term_list, ["term"])] - | Some _ => [] - end; + let val term_list = replicate datatype_arity ["term"]; + in [(tname, term_list, ["term"])] end; val datatype_name = pp_typlist1 typevars ^ tname; @@ -311,15 +303,10 @@ in (dekl, rules) end; val consts = - let val {const_tab, ...} = Sign.rep_sg sign; - fun const_undef (c, _, _) = case Symtab.lookup (const_tab, c) of - Some _ => false - | None => true; - in (filter const_undef (const_types cons_list)) @ - (if length cons_list < dtK then [] + const_types cons_list + @ (if length cons_list < dtK then [] else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) - @ case_const - end; + @ case_const; (*generate 'var_n, ..., var_m'*) fun Args(var, delim, n, m) = @@ -336,26 +323,28 @@ else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ Arg_eql(n+1, m); - fun Ci_ing (c :: cs) = - let val (name, typlist) = c - val arity = length typlist - in if arity>0 - then ("inject_" ^ name, + fun Ci_ing ((id, typlist, syn) :: cs) = + let val name = const_name id syn; + val arity = length typlist; + in if arity > 0 + then ("inject_" ^ id, "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") - ^ ") = (" ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs) + ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs) else (Ci_ing cs) end | Ci_ing [] = []; fun Ci_negOne _ [] = [] | Ci_negOne c (c1::cs) = - let val (name1, tl1) = c - val (name2, tl2) = c1 + let val (id1, tl1, syn1) = c + val (id2, tl2, syn2) = c1 + val name1 = const_name id1 syn1; + val name2 = const_name id2 syn2; 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) + in ("ineq_" ^ id1 ^ "_" ^ id2, h):: (Ci_negOne c cs) end; fun Ci_neg1 [] = [] @@ -364,10 +353,11 @@ 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) + fun Ci_neg2equals (ord_t, ((id, typlist, syn) :: cs), n) = + let val name = const_name id syn; + val h = ord_t ^ "(" ^ (C_exp(name, 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 (_, [], _) = []; diff -r 5c7a69cef18b -r a94029edb01f ex/PL0.thy --- a/ex/PL0.thy Wed Jun 29 12:04:04 1994 +0200 +++ b/ex/PL0.thy Fri Jul 08 12:01:55 1994 +0200 @@ -7,12 +7,6 @@ *) PL0 = HOL + -types 'a pl -arities pl :: (term)term -consts - false :: "'a pl" - "->" :: "['a pl,'a pl] => 'a pl" (infixr 90) - var :: "'a => 'a pl" ("#_") datatype - 'a pl = false | var('a) | "op->" ('a pl,'a pl) + 'a pl = false | var ('a) ("#_") | "->" ('a pl,'a pl) (infixr 90) end