nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
authorwenzelm
Thu Feb 24 15:57:36 2000 +0100 (2000-02-24)
changeset 82907015d6b11b56
parent 8289 5b288a96bc61
child 8291 5469b894f30b
nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Feb 24 15:34:49 2000 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 24 15:57:36 2000 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    val classes: sg -> class list
     1.5    val defaultS: sg -> sort
     1.6    val subsort: sg -> sort * sort -> bool
     1.7 -  val nodup_Vars: term -> unit
     1.8 +  val nodup_vars: term -> term
     1.9    val norm_sort: sg -> sort -> sort
    1.10    val of_sort: sg -> typ * sort -> bool
    1.11    val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    1.12 @@ -563,44 +563,50 @@
    1.13  
    1.14  (* certify_term *)
    1.15  
    1.16 -(*check for duplicate TVars with distinct sorts*)
    1.17 -fun nodup_TVars (tvars, T) =
    1.18 -  (case T of
    1.19 -    Type (_, Ts) => nodup_TVars_list (tvars, Ts)
    1.20 -  | TFree _ => tvars
    1.21 -  | TVar (v as (a, S)) =>
    1.22 +(*check for duplicate occurrences of TFree/TVar with distinct sorts*)
    1.23 +fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts)
    1.24 +  | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) =
    1.25 +      (case assoc_string (tfrees, a) of
    1.26 +        Some S' =>
    1.27 +          if S = S' then env
    1.28 +          else raise TYPE ("Type variable " ^ quote a ^
    1.29 +            " has two distinct sorts", [TFree (a, S'), T], [])
    1.30 +      | None => (v :: tfrees, tvars))
    1.31 +  | nodup_tvars (env as (tfrees, tvars), T as TVar (v as (a, S))) =
    1.32        (case assoc_string_int (tvars, a) of
    1.33          Some S' =>
    1.34 -          if S = S' then tvars
    1.35 -          else raise TYPE ("Type variable " ^ Syntax.string_of_vname a ^
    1.36 +          if S = S' then env
    1.37 +          else raise TYPE ("Type variable " ^ quote (Syntax.string_of_vname a) ^
    1.38              " has two distinct sorts", [TVar (a, S'), T], [])
    1.39 -      | None => v :: tvars))
    1.40 -(*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.41 -and nodup_TVars_list (tvars, []) = tvars
    1.42 -  | nodup_TVars_list (tvars, T :: Ts) =
    1.43 -      nodup_TVars_list (nodup_TVars (tvars, T), Ts);
    1.44 +      | None => (tfrees, v :: tvars))
    1.45 +(*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*)
    1.46 +and nodup_tvars_list (env, []) = env
    1.47 +  | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts);
    1.48  
    1.49 -(*check for duplicate Vars with distinct types*)
    1.50 -fun nodup_Vars tm =
    1.51 +(*check for duplicate occurrences of Free/Var with distinct types*)
    1.52 +fun nodup_vars tm =
    1.53    let
    1.54 -    fun nodups vars tvars tm =
    1.55 +    fun nodups (envs as (env as (frees, vars), envT)) tm =
    1.56        (case tm of
    1.57 -        Const (c, T) => (vars, nodup_TVars (tvars, T))
    1.58 -      | Free (a, T) => (vars, nodup_TVars (tvars, T))
    1.59 +        Const (c, T) => (env, nodup_tvars (envT, T))
    1.60 +      | Free (v as (a, T)) =>
    1.61 +          (case assoc_string (frees, a) of
    1.62 +            Some T' =>
    1.63 +              if T = T' then (env, nodup_tvars (envT, T))
    1.64 +              else raise TYPE ("Variable " ^ quote a ^
    1.65 +                " has two distinct types", [T', T], [])
    1.66 +          | None => ((v :: frees, vars), nodup_tvars (envT, T)))
    1.67        | Var (v as (ixn, T)) =>
    1.68            (case assoc_string_int (vars, ixn) of
    1.69              Some T' =>
    1.70 -              if T = T' then (vars, nodup_TVars (tvars, T))
    1.71 -              else raise TYPE ("Variable " ^ Syntax.string_of_vname ixn ^
    1.72 +              if T = T' then (env, nodup_tvars (envT, T))
    1.73 +              else raise TYPE ("Variable " ^ quote (Syntax.string_of_vname ixn) ^
    1.74                  " has two distinct types", [T', T], [])
    1.75 -          | None => (v :: vars, tvars))
    1.76 -      | Bound _ => (vars, tvars)
    1.77 -      | Abs (_, T, t) => nodups vars (nodup_TVars (tvars, T)) t
    1.78 -      | s $ t =>
    1.79 -          let val (vars',tvars') = nodups vars tvars s in
    1.80 -            nodups vars' tvars' t
    1.81 -          end);
    1.82 -  in nodups [] [] tm; () end;
    1.83 +          | None => ((frees, v :: vars), nodup_tvars (envT, T)))
    1.84 +      | Bound _ => envs
    1.85 +      | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t
    1.86 +      | s $ t => nodups (nodups envs s) t)
    1.87 +  in nodups (([], []), ([], [])) tm; tm end;
    1.88  
    1.89  (*compute and check type of the term*)
    1.90  fun type_check sg tm =
    1.91 @@ -656,7 +662,7 @@
    1.92        (case it_term_types (Type.typ_errors tsig) (tm, []) of
    1.93          [] => Type.norm_term tsig tm
    1.94        | errs => raise TYPE (cat_lines errs, [], [tm]));
    1.95 -    val _ = nodup_Vars norm_tm;
    1.96 +    val _ = nodup_vars norm_tm;
    1.97    in
    1.98      (case foldl_aterms atom_err ([], norm_tm) of
    1.99        [] => (norm_tm, type_check sg norm_tm, maxidx_of_term norm_tm)