added add_tyconames; tuned
authorhaftmann
Mon Oct 12 16:16:44 2009 +0200 (2009-10-12)
changeset 3291784a5c684a22e
parent 32914 dc48da9922bd
child 32918 bea03f604656
added add_tyconames; tuned
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Oct 12 15:48:12 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 12 16:16:44 2009 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4    val contains_dictvar: iterm -> bool
     1.5    val locally_monomorphic: iterm -> bool
     1.6    val add_constnames: iterm -> string list -> string list
     1.7 +  val add_tyconames: iterm -> string list -> string list
     1.8    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
     1.9  
    1.10    type naming
    1.11 @@ -162,12 +163,22 @@
    1.12    of (IConst c, ts) => SOME (c, ts)
    1.13     | _ => NONE;
    1.14  
    1.15 -fun add_constnames (IConst (c, _)) = insert (op =) c
    1.16 -  | add_constnames (IVar _) = I
    1.17 -  | add_constnames (t1 `$ t2) = add_constnames t1 #> add_constnames t2
    1.18 -  | add_constnames (_ `|=> t) = add_constnames t
    1.19 -  | add_constnames (ICase (((t, _), ds), _)) = add_constnames t
    1.20 -      #> fold (fn (pat, body) => add_constnames pat #> add_constnames body) ds;
    1.21 +fun fold_constexprs f =
    1.22 +  let
    1.23 +    fun fold' (IConst c) = f c
    1.24 +      | fold' (IVar _) = I
    1.25 +      | fold' (t1 `$ t2) = fold' t1 #> fold' t2
    1.26 +      | fold' (_ `|=> t) = fold' t
    1.27 +      | fold' (ICase (((t, _), ds), _)) = fold' t
    1.28 +          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
    1.29 +  in fold' end;
    1.30 +
    1.31 +val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
    1.32 +
    1.33 +fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
    1.34 +  | add_tycos (ITyVar _) = I;
    1.35 +
    1.36 +val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
    1.37  
    1.38  fun fold_varnames f =
    1.39    let