added nodup_Vars check in cterm_of. Prevents same var with distinct types.
authornipkow
Tue Feb 13 14:13:23 1996 +0100 (1996-02-13)
changeset 149422f67e796445
parent 1493 e936723cb94d
child 1495 b8b54847c77f
added nodup_Vars check in cterm_of. Prevents same var with distinct types.
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Feb 13 12:57:24 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Feb 13 14:13:23 1996 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4      val const_type: sg -> string -> typ option
     1.5      val classes: sg -> class list
     1.6      val subsort: sg -> sort * sort -> bool
     1.7 +    val nodup_Vars: term -> unit
     1.8      val norm_sort: sg -> sort -> sort
     1.9      val nonempty_sort: sg -> sort list -> sort -> bool
    1.10      val print_sg: sg -> unit
    1.11 @@ -232,6 +233,35 @@
    1.12  
    1.13  fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
    1.14  
    1.15 +(* check for duplicate TVars with distinct sorts *)
    1.16 +fun nodup_TVars(tvars,T) = (case T of
    1.17 +      Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
    1.18 +    | TFree _ => tvars
    1.19 +    | TVar(v as (a,S)) =>
    1.20 +        (case assoc(tvars,a) of
    1.21 +           Some(S') => if S=S' then tvars
    1.22 +                       else raise_type
    1.23 +                            ("Type variable "^Syntax.string_of_vname a^
    1.24 +                             "has two distinct sorts") [TVar(a,S'),T] []
    1.25 +         | None => v::tvars));
    1.26 +
    1.27 +(* check for duplicate Vars with distinct types *)
    1.28 +fun nodup_Vars tm =
    1.29 +let fun nodups vars tvars tm = (case tm of
    1.30 +          Const(c,T) => (vars, nodup_TVars(tvars,T))
    1.31 +        | Free(a,T) => (vars, nodup_TVars(tvars,T))
    1.32 +        | Var(v as (ixn,T)) =>
    1.33 +            (case assoc(vars,ixn) of
    1.34 +               Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
    1.35 +                           else raise_type
    1.36 +                             ("Variable "^Syntax.string_of_vname ixn^
    1.37 +                              "has two distinct types") [T',T] []
    1.38 +             | None => (v::vars,tvars))
    1.39 +        | Bound _ => (vars,tvars)
    1.40 +        | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
    1.41 +        | s$t => let val (vars',tvars') = nodups vars tvars s
    1.42 +                 in nodups vars' tvars' t end);
    1.43 +in nodups [] [] tm; () end;
    1.44  
    1.45  fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
    1.46    | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
    1.47 @@ -256,6 +286,7 @@
    1.48        (case it_term_types (typ_errors tsig) (tm, []) of
    1.49          [] => map_term_types (norm_typ tsig) tm
    1.50        | errs => raise_type (cat_lines errs) [] [tm]);
    1.51 +    val _ = nodup_Vars norm_tm;
    1.52    in
    1.53      (case mapfilt_atoms atom_err norm_tm of
    1.54        [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)