src/Pure/sign.ML
changeset 18892 51360da418b2
parent 18857 c4b4fbd74ffb
child 18928 042608ffa2ec
equal deleted inserted replaced
18891:9923269dcf06 18892:51360da418b2
   307 val intern_sort = map o intern_class;
   307 val intern_sort = map o intern_class;
   308 val extern_sort = map o extern_class;
   308 val extern_sort = map o extern_class;
   309 
   309 
   310 local
   310 local
   311 
   311 
       
   312 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
       
   313   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
       
   314   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
       
   315 
       
   316 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
       
   317   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
       
   318   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
       
   319   | map_term _ _ _ (t as Bound _) = t
       
   320   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
       
   321   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
       
   322 
   312 fun mapping add_names f t =
   323 fun mapping add_names f t =
   313   let
   324   let
   314     fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   325     fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   315     val tab = List.mapPartial f' (add_names (t, []));
   326     val tab = List.mapPartial f' (add_names (t, []));
   316     fun get x = if_none (AList.lookup (op =) tab x) x;
   327     fun get x = if_none (AList.lookup (op =) tab x) x;
   317   in get end;
   328   in get end;
   318 
   329 
   319 fun typ_mapping f g thy T =
   330 fun typ_mapping f g thy T =
   320   T |> Term.map_typ
   331   T |> map_typ
   321     (mapping add_typ_classes (f thy) T)
   332     (mapping add_typ_classes (f thy) T)
   322     (mapping add_typ_tycons (g thy) T);
   333     (mapping add_typ_tycons (g thy) T);
   323 
   334 
   324 fun term_mapping f g h thy t =
   335 fun term_mapping f g h thy t =
   325   t |> Term.map_term
   336   t |> map_term
   326     (mapping add_term_classes (f thy) t)
   337     (mapping add_term_classes (f thy) t)
   327     (mapping add_term_tycons (g thy) t)
   338     (mapping add_term_tycons (g thy) t)
   328     (mapping add_term_consts (h thy) t);
   339     (mapping add_term_consts (h thy) t);
   329 
   340 
   330 in
   341 in