add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
authorwenzelm
Tue Oct 28 17:29:48 1997 +0100 (1997-10-28)
changeset 401763878e2587a7
parent 4016 90aebb69c04e
child 4018 09b77900af0f
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;
src/Pure/sign.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/sign.ML	Tue Oct 28 17:28:11 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 28 17:29:48 1997 +0100
     1.3 @@ -305,36 +305,6 @@
     1.4  (* intern / extern names *)
     1.5  
     1.6  local
     1.7 -
     1.8 -  fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs)
     1.9 -    | add_typ_classes (TFree (_, S), cs) = S union cs
    1.10 -    | add_typ_classes (TVar (_, S), cs) = S union cs;
    1.11 -
    1.12 -  fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (Ts, c ins cs)
    1.13 -    | add_typ_tycons (_, cs) = cs;
    1.14 -
    1.15 -  val add_term_classes = it_term_types add_typ_classes;
    1.16 -  val add_term_tycons = it_term_types add_typ_tycons;
    1.17 -
    1.18 -  fun add_term_consts (Const (c, _), cs) = c ins cs
    1.19 -    | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    1.20 -    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    1.21 -    | add_term_consts (_, cs) = cs;
    1.22 -
    1.23 -
    1.24 -  (*map classes, tycons*)
    1.25 -  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.26 -    | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    1.27 -    | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.28 -
    1.29 -  (*map classes, tycons, consts*)
    1.30 -  fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.31 -    | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.32 -    | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.33 -    | map_term _ _ _ (t as Bound _) = t
    1.34 -    | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.35 -    | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.36 -
    1.37    (*prepare mapping of names*)
    1.38    fun mapping f add_xs t =
    1.39      let
    1.40 @@ -356,11 +326,8 @@
    1.41        (mapping (trn typeK) add_term_tycons t)
    1.42        (mapping (trn constK) add_term_consts t);
    1.43  
    1.44 -
    1.45    val spaces_of = #spaces o rep_sg;
    1.46 -
    1.47  in
    1.48 -
    1.49    fun intrn_class spaces = intrn spaces classK;
    1.50    fun extrn_class spaces = extrn spaces classK;
    1.51  
    1.52 @@ -390,7 +357,6 @@
    1.53    val intern_tycons = intrn_tycons o spaces_of;
    1.54  
    1.55    val full_name = full o #path o rep_sg;
    1.56 -
    1.57  end;
    1.58  
    1.59  
    1.60 @@ -869,7 +835,7 @@
    1.61  
    1.62  
    1.63  
    1.64 -(** merge signatures **)    (*exception TERM*)
    1.65 +(** merge signatures **)    	(*exception TERM*)
    1.66  
    1.67  (* merge of sg_refs -- trivial only *)
    1.68  
     2.1 --- a/src/Pure/term.ML	Tue Oct 28 17:28:11 1997 +0100
     2.2 +++ b/src/Pure/term.ML	Tue Oct 28 17:29:48 1997 +0100
     2.3 @@ -543,6 +543,41 @@
     2.4        let val b' = variant used b
     2.5        in  b' :: variantlist (bs, b'::used)  end;
     2.6  
     2.7 +
     2.8 +
     2.9 +(** Consts etc. **)
    2.10 +
    2.11 +fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs)
    2.12 +  | add_typ_classes (TFree (_, S), cs) = S union cs
    2.13 +  | add_typ_classes (TVar (_, S), cs) = S union cs;
    2.14 +
    2.15 +fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (Ts, c ins cs)
    2.16 +  | add_typ_tycons (_, cs) = cs;
    2.17 +
    2.18 +val add_term_classes = it_term_types add_typ_classes;
    2.19 +val add_term_tycons = it_term_types add_typ_tycons;
    2.20 +
    2.21 +fun add_term_consts (Const (c, _), cs) = c ins cs
    2.22 +  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    2.23 +  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    2.24 +  | add_term_consts (_, cs) = cs;
    2.25 +
    2.26 +
    2.27 +(*map classes, tycons*)
    2.28 +fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    2.29 +  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    2.30 +  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    2.31 +
    2.32 +(*map classes, tycons, consts*)
    2.33 +fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    2.34 +  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    2.35 +  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    2.36 +  | map_term _ _ _ (t as Bound _) = t
    2.37 +  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    2.38 +  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    2.39 +
    2.40 +
    2.41 +
    2.42  (** TFrees and TVars **)
    2.43  
    2.44  (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)