# HG changeset patch # User wenzelm # Date 1158858289 -7200 # Node ID 00521d5e18385146ce563f6682ae1356370791c4 # Parent 953b68f4a9f30e387e8dc0c63c16dfb4b028d048 tuned; diff -r 953b68f4a9f3 -r 00521d5e1838 src/Pure/Tools/am_compiler.ML --- a/src/Pure/Tools/am_compiler.ML Thu Sep 21 19:04:43 2006 +0200 +++ b/src/Pure/Tools/am_compiler.ML Thu Sep 21 19:04:49 2006 +0200 @@ -106,12 +106,6 @@ "lookup stack "^pattern^" = weak stack ("^term^")" end -fun remove_dups (c::cs) = - let val cs = remove_dups cs in - if (List.exists (fn x => x=c) cs) then cs else c::cs - end - | remove_dups [] = [] - fun constants_of PVar = [] | constants_of (PConst (c, ps)) = c :: maps constants_of ps @@ -133,7 +127,7 @@ "structure "^name^" = struct", "", "datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"] - val constants = remove_dups (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog) + val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog) val _ = map (fn x => write (" | c"^(str x))) constants val _ = writelist [ "", diff -r 953b68f4a9f3 -r 00521d5e1838 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Sep 21 19:04:43 2006 +0200 +++ b/src/Pure/defs.ML Thu Sep 21 19:04:49 2006 +0200 @@ -140,12 +140,11 @@ | SOME subst => SOME (map (apsnd (map subst)) rhs)); fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d); - fun add (NONE, dp) = insert (op =) dp - | add (SOME dps, _) = fold (insert (op =)) dps; val reds = map (`reducts) deps; val deps' = if forall (is_none o #1) reds then NONE - else SOME (fold_rev add reds []); + else SOME (fold_rev + (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); val _ = forall (acyclic pp defs const) (the_default deps deps'); in deps' end; diff -r 953b68f4a9f3 -r 00521d5e1838 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Thu Sep 21 19:04:43 2006 +0200 +++ b/src/Pure/type_infer.ML Thu Sep 21 19:04:49 2006 +0200 @@ -101,7 +101,7 @@ (** raw typs/terms to pretyps/preterms **) -(* pretyp(s)_of *) +(* pretyp_of *) fun anyT S = TFree ("'_dummy_", S); val logicT = anyT []; @@ -113,15 +113,14 @@ (*indicate polymorphic Vars*) fun polymorphicT T = Type ("_polymorphic_", [T]); -fun pretyp_of is_param (params, typ) = +fun pretyp_of is_param typ params = let - fun add_parms (TVar (xi as (x, _), S)) ps = - if is_param xi andalso not (AList.defined (op =) ps xi) - then (xi, mk_param S) :: ps else ps - | add_parms (TFree _) ps = ps - | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps; - - val params' = add_parms typ params; + val params' = fold_atyps + (fn TVar (xi as (x, _), S) => + (fn ps => + if is_param xi andalso not (AList.defined (op =) ps xi) + then (xi, mk_param S) :: ps else ps) + | _ => I) typ params; fun pre_of (TVar (v as (xi, _))) = (case AList.lookup (op =) params' xi of @@ -132,65 +131,59 @@ | pre_of (T as Type (a, Ts)) = if T = dummyT then mk_param [] else PType (a, map pre_of Ts); - in (params', pre_of typ) end; - -fun pretyps_of is_param = foldl_map (pretyp_of is_param); + in (pre_of typ, params') end; -(* preterm(s)_of *) +(* preterm_of *) -fun preterm_of const_type is_param ((vparams, params), tm) = +fun preterm_of const_type is_param tm (vparams, params) = let - fun add_vparm (ps, xi) = - if not (AList.defined (op =) ps xi) then + fun add_vparm xi ps = + if not (AList.defined Term.eq_ix ps xi) then (xi, mk_param []) :: ps else ps; - fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps - | add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi) - | add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1)) - | add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t) - | add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u) - | add_vparms (ps, _) = ps; - - val vparams' = add_vparms (vparams, tm); + val vparams' = fold_aterms + (fn Var (_, Type ("_polymorphic_", _)) => I + | Var (xi, _) => add_vparm xi + | Free (x, _) => add_vparm (x, ~1) + | _ => I) + tm vparams; fun var_param xi = (the o AList.lookup (op =) vparams') xi; val preT_of = pretyp_of is_param; - fun constrain (ps, t) T = - if T = dummyT then (ps, t) + fun constrain T t ps = + if T = dummyT then (t, ps) else - let val (ps', T') = preT_of (ps, T) - in (ps', Constraint (t, T')) end; + let val (T', ps') = preT_of T ps + in (Constraint (t, T'), ps') end; - fun pre_of (ps, Const (c, T)) = + fun pre_of (Const (c, T)) ps = (case const_type c of - SOME U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T + SOME U => constrain T (PConst (c, fst (pretyp_of (K true) U []))) ps | NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) - | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) = - (ps, PVar (xi, snd (pretyp_of (K true) ([], T)))) - | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T - | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T - | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) = - constrain (pre_of (ps, t)) T - | pre_of (ps, Bound i) = (ps, PBound i) - | pre_of (ps, Abs (x, T, t)) = + | pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps = + (PVar (xi, fst (pretyp_of (K true) T [])), ps) + | pre_of (Var (xi, T)) ps = constrain T (PVar (xi, var_param xi)) ps + | pre_of (Free (x, T)) ps = constrain T (PFree (x, var_param (x, ~1))) ps + | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps = + uncurry (constrain T) (pre_of t ps) + | pre_of (Bound i) ps = (PBound i, ps) + | pre_of (Abs (x, T, t)) ps = let - val (ps', T') = preT_of (ps, T); - val (ps'', t') = pre_of (ps', t); - in (ps'', PAbs (x, T', t')) end - | pre_of (ps, t $ u) = + val (T', ps') = preT_of T ps; + val (t', ps'') = pre_of t ps'; + in (PAbs (x, T', t'), ps'') end + | pre_of (t $ u) ps = let - val (ps', t') = pre_of (ps, t); - val (ps'', u') = pre_of (ps', u); - in (ps'', PAppl (t', u')) end; + val (t', ps') = pre_of t ps; + val (u', ps'') = pre_of u ps'; + in (PAppl (t', u'), ps'') end; - val (params', tm') = pre_of (params, tm); - in ((vparams', params'), tm') end; - -fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param); + val (tm', params') = pre_of tm params; + in (tm', (vparams', params')) end; @@ -404,8 +397,8 @@ fun basic_infer_types pp tsig const_type used freeze is_param ts Ts = let (*convert to preterms/typs*) - val (Tps, Ts') = pretyps_of (K true) ([], Ts); - val ((vps, ps), ts') = preterms_of const_type is_param (([], Tps), ts); + val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts []; + val (ts', (vps, ps)) = fold_map (preterm_of const_type is_param) ts ([], Tps); (*run type inference*) val tTs' = ListPair.map Constraint (ts', Ts'); @@ -457,8 +450,8 @@ fun get_sort tsig def_sort map_sort raw_env = let - fun eq ((xi: indexname, S), (xi', S')) = - xi = xi' andalso Type.eq_sort tsig (S, S'); + fun eq ((xi, S), (xi', S')) = + Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S'); val env = distinct eq (map (apsnd map_sort) raw_env); val _ = (case duplicates (eq_fst (op =)) env of [] => ()