introduced some new-style AList operations
authorhaftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 172712756a73f63a5
parent 17270 534b6e5e3736
child 17272 c63e5220ed77
introduced some new-style AList operations
src/Provers/blast.ML
src/Pure/Isar/locale.ML
src/Pure/Proof/extraction.ML
src/Pure/tactic.ML
src/Pure/term.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Provers/blast.ML	Tue Sep 06 08:29:17 2005 +0200
     1.2 +++ b/src/Provers/blast.ML	Tue Sep 06 08:30:43 2005 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4  fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts)
     1.5    | fromType alist (Term.TFree(a,_)) = Free a
     1.6    | fromType alist (Term.TVar (ixn,_)) =
     1.7 -	      (case (assoc_string_int(!alist,ixn)) of
     1.8 +	      (case (AList.lookup (op =) (!alist) ixn) of
     1.9  		   NONE => let val t' = Var(ref NONE)
    1.10  		           in  alist := (ixn, t') :: !alist;  t'
    1.11  			   end
    1.12 @@ -381,7 +381,7 @@
    1.13  	| from (Term.Free  (a,_)) = Free a
    1.14  	| from (Term.Bound i)     = Bound i
    1.15  	| from (Term.Var (ixn,T)) = 
    1.16 -	      (case (assoc_string_int(!alistVar,ixn)) of
    1.17 +	      (case (AList.lookup (op =) (!alistVar) ixn) of
    1.18  		   NONE => let val t' = Var(ref NONE)
    1.19  		           in  alistVar := (ixn, t') :: !alistVar;  t'
    1.20  			   end
    1.21 @@ -1214,7 +1214,7 @@
    1.22  	    | Term.Free  (a,_) => apply (Free a)
    1.23  	    | Term.Bound i     => apply (Bound i)
    1.24  	    | Term.Var (ix,_) => 
    1.25 -		  (case (assoc_string_int(!alistVar,ix)) of
    1.26 +		  (case (AList.lookup (op =) (!alistVar) ix) of
    1.27  		       NONE => (alistVar := (ix, (ref NONE, bounds ts))
    1.28  					  :: !alistVar;
    1.29  				Var (hdvar(!alistVar)))
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 06 08:29:17 2005 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 06 08:30:43 2005 +0200
     2.3 @@ -625,7 +625,7 @@
     2.4  (* ren maps names to (new) names and syntax; represented as association list *)
     2.5  
     2.6  fun rename_var ren (x, mx) =
     2.7 -  case assoc_string (ren, x) of
     2.8 +  case AList.lookup (op =) ren x of
     2.9        NONE => (x, mx)
    2.10      | SOME (x', NONE) =>
    2.11          (x', if mx = NONE then mx else SOME Syntax.NoSyn)     (*drop syntax*)
    2.12 @@ -635,7 +635,7 @@
    2.13          else (x', SOME mx');                                (*change syntax*)
    2.14  
    2.15  fun rename ren x =
    2.16 -  case assoc_string (ren, x) of
    2.17 +  case AList.lookup (op =) ren x of
    2.18        NONE => x
    2.19      | SOME (x', _) => x';                                   (*ignore syntax*)
    2.20  
    2.21 @@ -1391,9 +1391,9 @@
    2.22  
    2.23  
    2.24  fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
    2.25 -      (x, assoc_string (parms, x), mx)) fixes)
    2.26 +      (x, AList.lookup (op =) parms x, mx)) fixes)
    2.27    | finish_ext_elem parms _ (Constrains csts, _) =
    2.28 -      Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts)
    2.29 +      Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts)
    2.30    | finish_ext_elem _ close (Assumes asms, propp) =
    2.31        close (Assumes (map #1 asms ~~ propp))
    2.32    | finish_ext_elem _ close (Defines defs, propp) =
     3.1 --- a/src/Pure/Proof/extraction.ML	Tue Sep 06 08:29:17 2005 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Tue Sep 06 08:30:43 2005 +0200
     3.3 @@ -532,7 +532,7 @@
     3.4                    (Bound (length Us), eT :: Us);
     3.5                  val u = list_comb (incr_boundvars (length Us') t,
     3.6                    map Bound (length Us - 1 downto 0));
     3.7 -                val u' = (case assoc_string (types, tname_of T) of
     3.8 +                val u' = (case AList.lookup (op =) types (tname_of T) of
     3.9                      SOME ((_, SOME f)) => f r eT u T
    3.10                    | _ => Const ("realizes", eT --> T --> T) $ r $ u)
    3.11                in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
     4.1 --- a/src/Pure/tactic.ML	Tue Sep 06 08:29:17 2005 +0200
     4.2 +++ b/src/Pure/tactic.ML	Tue Sep 06 08:30:43 2005 +0200
     4.3 @@ -240,7 +240,7 @@
     4.4    let val thy = Thm.theory_of_thm st
     4.5        and params = params_of_state st i
     4.6        and rts = types_sorts rule and (types,sorts) = types_sorts st
     4.7 -      fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm)
     4.8 +      fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
     4.9          | types' ixn = types ixn;
    4.10        val used = Drule.add_used rule (Drule.add_used st []);
    4.11    in read_insts thy rts (types',sorts) used sinsts end;
    4.12 @@ -666,7 +666,7 @@
    4.13      val frees = map Term.dest_Free (Term.term_frees statement);
    4.14      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    4.15      val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    4.16 -    val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    4.17 +    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    4.18  
    4.19      fun err msg = raise ERROR_MESSAGE
    4.20        (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
     5.1 --- a/src/Pure/term.ML	Tue Sep 06 08:29:17 2005 +0200
     5.2 +++ b/src/Pure/term.ML	Tue Sep 06 08:30:43 2005 +0200
     5.3 @@ -736,7 +736,7 @@
     5.4    let
     5.5      val ren = match_bvs (pat, obj, []);
     5.6      fun ren_abs (Abs (x, T, b)) =
     5.7 -          Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b)
     5.8 +          Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b)
     5.9        | ren_abs (f $ t) = ren_abs f $ ren_abs t
    5.10        | ren_abs t = t
    5.11    in if null ren then NONE else SOME (ren_abs t) end;
    5.12 @@ -934,7 +934,7 @@
    5.13    | typ_subst_TVars inst ty =
    5.14        let
    5.15          fun subst (Type (a, Ts)) = Type (a, map subst Ts)
    5.16 -          | subst (T as TVar (xi, _)) = if_none (assoc_string_int (inst, xi)) T
    5.17 +          | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
    5.18            | subst T = T;
    5.19        in subst ty end;
    5.20  
    5.21 @@ -945,7 +945,7 @@
    5.22  fun subst_Vars [] tm = tm
    5.23    | subst_Vars inst tm =
    5.24        let
    5.25 -        fun subst (t as Var (xi, _)) = if_none (assoc_string_int (inst, xi)) t
    5.26 +        fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
    5.27            | subst (Abs (a, T, t)) = Abs (a, T, subst t)
    5.28            | subst (t $ u) = subst t $ subst u
    5.29            | subst t = t;
    5.30 @@ -959,7 +959,7 @@
    5.31          fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
    5.32            | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
    5.33            | subst (t as Var (xi, T)) =
    5.34 -              (case assoc_string_int (inst, xi) of
    5.35 +              (case AList.lookup (op =) inst xi of
    5.36                  NONE => Var (xi, typ_subst_TVars instT T)
    5.37                | SOME t => t)
    5.38            | subst (t as Bound _) = t
     6.1 --- a/src/Pure/type_infer.ML	Tue Sep 06 08:29:17 2005 +0200
     6.2 +++ b/src/Pure/type_infer.ML	Tue Sep 06 08:30:43 2005 +0200
     6.3 @@ -111,7 +111,7 @@
     6.4  fun pretyp_of is_param (params, typ) =
     6.5    let
     6.6      fun add_parms (TVar (xi as (x, _), S)) ps =
     6.7 -          if is_param xi andalso is_none (assoc_string_int (ps, xi))
     6.8 +          if is_param xi andalso is_none (AList.lookup (op =) ps xi)
     6.9            then (xi, mk_param S) :: ps else ps
    6.10        | add_parms (TFree _) ps = ps
    6.11        | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
    6.12 @@ -119,7 +119,7 @@
    6.13      val params' = add_parms typ params;
    6.14  
    6.15      fun pre_of (TVar (v as (xi, _))) =
    6.16 -          (case assoc_string_int (params', xi) of
    6.17 +          (case AList.lookup (op =) params' xi of
    6.18              NONE => PTVar v
    6.19            | SOME p => p)
    6.20        | pre_of (TFree ("'_dummy_", S)) = mk_param S
    6.21 @@ -137,7 +137,7 @@
    6.22  fun preterm_of const_type is_param ((vparams, params), tm) =
    6.23    let
    6.24      fun add_vparm (ps, xi) =
    6.25 -      if is_none (assoc_string_int (ps, xi)) then
    6.26 +      if is_none (AList.lookup (op =) ps xi) then
    6.27          (xi, mk_param []) :: ps
    6.28        else ps;
    6.29  
    6.30 @@ -149,7 +149,7 @@
    6.31        | add_vparms (ps, _) = ps;
    6.32  
    6.33      val vparams' = add_vparms (vparams, tm);
    6.34 -    fun var_param xi = the (assoc_string_int (vparams', xi));
    6.35 +    fun var_param xi = (the o AList.lookup (op =) vparams') xi;
    6.36  
    6.37  
    6.38      val preT_of = pretyp_of is_param;
    6.39 @@ -457,7 +457,7 @@
    6.40            ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
    6.41  
    6.42      fun get xi =
    6.43 -      (case (assoc_string_int (env, xi), def_sort xi) of
    6.44 +      (case (AList.lookup (op =) env xi, def_sort xi) of
    6.45          (NONE, NONE) => Type.defaultS tsig
    6.46        | (NONE, SOME S) => S
    6.47        | (SOME S, NONE) => S