tuned;
authorwenzelm
Thu Sep 21 19:04:49 2006 +0200 (2006-09-21)
changeset 2066800521d5e1838
parent 20667 953b68f4a9f3
child 20669 52ba40872033
tuned;
src/Pure/Tools/am_compiler.ML
src/Pure/defs.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Tools/am_compiler.ML	Thu Sep 21 19:04:43 2006 +0200
     1.2 +++ b/src/Pure/Tools/am_compiler.ML	Thu Sep 21 19:04:49 2006 +0200
     1.3 @@ -106,12 +106,6 @@
     1.4  	"lookup stack "^pattern^" = weak stack ("^term^")"
     1.5      end
     1.6  
     1.7 -fun remove_dups (c::cs) = 
     1.8 -    let val cs = remove_dups cs in
     1.9 -	if (List.exists (fn x => x=c) cs) then cs else c::cs
    1.10 -    end
    1.11 -  | remove_dups [] = []
    1.12 -
    1.13  fun constants_of PVar = []
    1.14    | constants_of (PConst (c, ps)) = c :: maps constants_of ps
    1.15  
    1.16 @@ -133,7 +127,7 @@
    1.17  		"structure "^name^" = struct",
    1.18  		"",
    1.19  		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
    1.20 -	val constants = remove_dups (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
    1.21 +	val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
    1.22  	val _ = map (fn x => write (" | c"^(str x))) constants
    1.23  	val _ = writelist [
    1.24  		"",
     2.1 --- a/src/Pure/defs.ML	Thu Sep 21 19:04:43 2006 +0200
     2.2 +++ b/src/Pure/defs.ML	Thu Sep 21 19:04:49 2006 +0200
     2.3 @@ -140,12 +140,11 @@
     2.4        | SOME subst => SOME (map (apsnd (map subst)) rhs));
     2.5      fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
     2.6  
     2.7 -    fun add (NONE, dp) = insert (op =) dp
     2.8 -      | add (SOME dps, _) = fold (insert (op =)) dps;
     2.9      val reds = map (`reducts) deps;
    2.10      val deps' =
    2.11        if forall (is_none o #1) reds then NONE
    2.12 -      else SOME (fold_rev add reds []);
    2.13 +      else SOME (fold_rev
    2.14 +        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
    2.15      val _ = forall (acyclic pp defs const) (the_default deps deps');
    2.16    in deps' end;
    2.17  
     3.1 --- a/src/Pure/type_infer.ML	Thu Sep 21 19:04:43 2006 +0200
     3.2 +++ b/src/Pure/type_infer.ML	Thu Sep 21 19:04:49 2006 +0200
     3.3 @@ -101,7 +101,7 @@
     3.4  
     3.5  (** raw typs/terms to pretyps/preterms **)
     3.6  
     3.7 -(* pretyp(s)_of *)
     3.8 +(* pretyp_of *)
     3.9  
    3.10  fun anyT S = TFree ("'_dummy_", S);
    3.11  val logicT = anyT [];
    3.12 @@ -113,15 +113,14 @@
    3.13  (*indicate polymorphic Vars*)
    3.14  fun polymorphicT T = Type ("_polymorphic_", [T]);
    3.15  
    3.16 -fun pretyp_of is_param (params, typ) =
    3.17 +fun pretyp_of is_param typ params =
    3.18    let
    3.19 -    fun add_parms (TVar (xi as (x, _), S)) ps =
    3.20 -          if is_param xi andalso not (AList.defined (op =) ps xi)
    3.21 -          then (xi, mk_param S) :: ps else ps
    3.22 -      | add_parms (TFree _) ps = ps
    3.23 -      | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
    3.24 -
    3.25 -    val params' = add_parms typ params;
    3.26 +    val params' = fold_atyps
    3.27 +      (fn TVar (xi as (x, _), S) =>
    3.28 +          (fn ps =>
    3.29 +            if is_param xi andalso not (AList.defined (op =) ps xi)
    3.30 +            then (xi, mk_param S) :: ps else ps)
    3.31 +        | _ => I) typ params;
    3.32  
    3.33      fun pre_of (TVar (v as (xi, _))) =
    3.34            (case AList.lookup (op =) params' xi of
    3.35 @@ -132,65 +131,59 @@
    3.36        | pre_of (T as Type (a, Ts)) =
    3.37            if T = dummyT then mk_param []
    3.38            else PType (a, map pre_of Ts);
    3.39 -  in (params', pre_of typ) end;
    3.40 -
    3.41 -fun pretyps_of is_param = foldl_map (pretyp_of is_param);
    3.42 +  in (pre_of typ, params') end;
    3.43  
    3.44  
    3.45 -(* preterm(s)_of *)
    3.46 +(* preterm_of *)
    3.47  
    3.48 -fun preterm_of const_type is_param ((vparams, params), tm) =
    3.49 +fun preterm_of const_type is_param tm (vparams, params) =
    3.50    let
    3.51 -    fun add_vparm (ps, xi) =
    3.52 -      if not (AList.defined (op =) ps xi) then
    3.53 +    fun add_vparm xi ps =
    3.54 +      if not (AList.defined Term.eq_ix ps xi) then
    3.55          (xi, mk_param []) :: ps
    3.56        else ps;
    3.57  
    3.58 -    fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps
    3.59 -      | add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)
    3.60 -      | add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1))
    3.61 -      | add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t)
    3.62 -      | add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u)
    3.63 -      | add_vparms (ps, _) = ps;
    3.64 -
    3.65 -    val vparams' = add_vparms (vparams, tm);
    3.66 +    val vparams' = fold_aterms
    3.67 +      (fn Var (_, Type ("_polymorphic_", _)) => I
    3.68 +        | Var (xi, _) => add_vparm xi
    3.69 +        | Free (x, _) => add_vparm (x, ~1)
    3.70 +        | _ => I)
    3.71 +      tm vparams;
    3.72      fun var_param xi = (the o AList.lookup (op =) vparams') xi;
    3.73  
    3.74  
    3.75      val preT_of = pretyp_of is_param;
    3.76  
    3.77 -    fun constrain (ps, t) T =
    3.78 -      if T = dummyT then (ps, t)
    3.79 +    fun constrain T t ps =
    3.80 +      if T = dummyT then (t, ps)
    3.81        else
    3.82 -        let val (ps', T') = preT_of (ps, T)
    3.83 -        in (ps', Constraint (t, T')) end;
    3.84 +        let val (T', ps') = preT_of T ps
    3.85 +        in (Constraint (t, T'), ps') end;
    3.86  
    3.87 -    fun pre_of (ps, Const (c, T)) =
    3.88 +    fun pre_of (Const (c, T)) ps =
    3.89            (case const_type c of
    3.90 -            SOME U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
    3.91 +            SOME U => constrain T (PConst (c, fst (pretyp_of (K true) U []))) ps
    3.92            | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
    3.93 -      | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) =
    3.94 -          (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
    3.95 -      | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
    3.96 -      | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
    3.97 -      | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) =
    3.98 -          constrain (pre_of (ps, t)) T
    3.99 -      | pre_of (ps, Bound i) = (ps, PBound i)
   3.100 -      | pre_of (ps, Abs (x, T, t)) =
   3.101 +      | pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps =
   3.102 +          (PVar (xi, fst (pretyp_of (K true) T [])), ps)
   3.103 +      | pre_of (Var (xi, T)) ps = constrain T (PVar (xi, var_param xi)) ps
   3.104 +      | pre_of (Free (x, T)) ps = constrain T (PFree (x, var_param (x, ~1))) ps
   3.105 +      | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps =
   3.106 +          uncurry (constrain T) (pre_of t ps)
   3.107 +      | pre_of (Bound i) ps = (PBound i, ps)
   3.108 +      | pre_of (Abs (x, T, t)) ps =
   3.109            let
   3.110 -            val (ps', T') = preT_of (ps, T);
   3.111 -            val (ps'', t') = pre_of (ps', t);
   3.112 -          in (ps'', PAbs (x, T', t')) end
   3.113 -      | pre_of (ps, t $ u) =
   3.114 +            val (T', ps') = preT_of T ps;
   3.115 +            val (t', ps'') = pre_of t ps';
   3.116 +          in (PAbs (x, T', t'), ps'') end
   3.117 +      | pre_of (t $ u) ps =
   3.118            let
   3.119 -            val (ps', t') = pre_of (ps, t);
   3.120 -            val (ps'', u') = pre_of (ps', u);
   3.121 -          in (ps'', PAppl (t', u')) end;
   3.122 +            val (t', ps') = pre_of t ps;
   3.123 +            val (u', ps'') = pre_of u ps';
   3.124 +          in (PAppl (t', u'), ps'') end;
   3.125  
   3.126 -    val (params', tm') = pre_of (params, tm);
   3.127 -  in ((vparams', params'), tm') end;
   3.128 -
   3.129 -fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param);
   3.130 +    val (tm', params') = pre_of tm params;
   3.131 +  in (tm', (vparams', params')) end;
   3.132  
   3.133  
   3.134  
   3.135 @@ -404,8 +397,8 @@
   3.136  fun basic_infer_types pp tsig const_type used freeze is_param ts Ts =
   3.137    let
   3.138      (*convert to preterms/typs*)
   3.139 -    val (Tps, Ts') = pretyps_of (K true) ([], Ts);
   3.140 -    val ((vps, ps), ts') = preterms_of const_type is_param (([], Tps), ts);
   3.141 +    val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts [];
   3.142 +    val (ts', (vps, ps)) = fold_map (preterm_of const_type is_param) ts ([], Tps);
   3.143  
   3.144      (*run type inference*)
   3.145      val tTs' = ListPair.map Constraint (ts', Ts');
   3.146 @@ -457,8 +450,8 @@
   3.147  
   3.148  fun get_sort tsig def_sort map_sort raw_env =
   3.149    let
   3.150 -    fun eq ((xi: indexname, S), (xi', S')) =
   3.151 -      xi = xi' andalso Type.eq_sort tsig (S, S');
   3.152 +    fun eq ((xi, S), (xi', S')) =
   3.153 +      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
   3.154  
   3.155      val env = distinct eq (map (apsnd map_sort) raw_env);
   3.156      val _ = (case duplicates (eq_fst (op =)) env of [] => ()