src/Pure/envir.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 35408 b48ab741683b
child 42083 e1209fc7ecdc
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      Pure/envir.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Free-form environments.  The type of a term variable / sort of a type variable is
     5 part of its name.  The lookup function must apply type substitutions,
     6 since they may change the identity of a variable.
     7 *)
     8 
     9 signature ENVIR =
    10 sig
    11   type tenv = (typ * term) Vartab.table
    12   datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
    13   val maxidx_of: env -> int
    14   val term_env: env -> tenv
    15   val type_env: env -> Type.tyenv
    16   val is_empty: env -> bool
    17   val empty: int -> env
    18   val merge: env * env -> env
    19   val insert_sorts: env -> sort list -> sort list
    20   val genvars: string -> env * typ list -> env * term list
    21   val genvar: string -> env * typ -> env * term
    22   val lookup: env * (indexname * typ) -> term option
    23   val lookup': tenv * (indexname * typ) -> term option
    24   val update: ((indexname * typ) * term) * env -> env
    25   val above: env -> int -> bool
    26   val vupdate: ((indexname * typ) * term) * env -> env
    27   val norm_type_same: Type.tyenv -> typ Same.operation
    28   val norm_types_same: Type.tyenv -> typ list Same.operation
    29   val norm_type: Type.tyenv -> typ -> typ
    30   val norm_term_same: env -> term Same.operation
    31   val norm_term: env -> term -> term
    32   val beta_norm: term -> term
    33   val head_norm: env -> term -> term
    34   val eta_contract: term -> term
    35   val beta_eta_contract: term -> term
    36   val fastype: env -> typ list -> term -> typ
    37   val subst_type_same: Type.tyenv -> typ Same.operation
    38   val subst_term_types_same: Type.tyenv -> term Same.operation
    39   val subst_term_same: Type.tyenv * tenv -> term Same.operation
    40   val subst_type: Type.tyenv -> typ -> typ
    41   val subst_term_types: Type.tyenv -> term -> term
    42   val subst_term: Type.tyenv * tenv -> term -> term
    43   val expand_atom: typ -> typ * term -> term
    44   val expand_term: (term -> (typ * term) option) -> term -> term
    45   val expand_term_frees: ((string * typ) * term) list -> term -> term
    46 end;
    47 
    48 structure Envir: ENVIR =
    49 struct
    50 
    51 (** datatype env **)
    52 
    53 (*Updating can destroy environment in 2 ways!
    54    (1) variables out of range
    55    (2) circular assignments
    56 *)
    57 
    58 type tenv = (typ * term) Vartab.table;
    59 
    60 datatype env = Envir of
    61  {maxidx: int,          (*upper bound of maximum index of vars*)
    62   tenv: tenv,           (*assignments to Vars*)
    63   tyenv: Type.tyenv};   (*assignments to TVars*)
    64 
    65 fun make_env (maxidx, tenv, tyenv) =
    66   Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
    67 
    68 fun maxidx_of (Envir {maxidx, ...}) = maxidx;
    69 fun term_env (Envir {tenv, ...}) = tenv;
    70 fun type_env (Envir {tyenv, ...}) = tyenv;
    71 
    72 fun is_empty env =
    73   Vartab.is_empty (term_env env) andalso
    74   Vartab.is_empty (type_env env);
    75 
    76 
    77 (* build env *)
    78 
    79 fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
    80 
    81 fun merge
    82    (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
    83     Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
    84   make_env (Int.max (maxidx1, maxidx2),
    85     Vartab.merge (op =) (tenv1, tenv2),
    86     Vartab.merge (op =) (tyenv1, tyenv2));
    87 
    88 
    89 (*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
    90 val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
    91 
    92 (*Generate a list of distinct variables.
    93   Increments index to make them distinct from ALL present variables. *)
    94 fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
    95   let
    96     fun genvs (_, [] : typ list) : term list = []
    97       | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
    98       | genvs (n, T :: Ts) =
    99           Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
   100             :: genvs (n + 1, Ts);
   101   in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
   102 
   103 (*Generate a variable.*)
   104 fun genvar name (env, T) : env * term =
   105   let val (env', [v]) = genvars name (env, [T])
   106   in (env', v) end;
   107 
   108 fun var_clash xi T T' =
   109   raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
   110     [T', T], []);
   111 
   112 fun lookup_check check tenv (xi, T) =
   113   (case Vartab.lookup tenv xi of
   114     NONE => NONE
   115   | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
   116 
   117 (* When dealing with environments produced by matching instead *)
   118 (* of unification, there is no need to chase assigned TVars.   *)
   119 (* In this case, we can simply ignore the type substitution    *)
   120 (* and use = instead of eq_type.                               *)
   121 
   122 fun lookup' (tenv, p) = lookup_check (op =) tenv p;
   123 
   124 fun lookup2 (tyenv, tenv) =
   125   lookup_check (Type.eq_type tyenv) tenv;
   126 
   127 fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
   128 
   129 fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
   130   Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
   131 
   132 (*Determine if the least index updated exceeds lim*)
   133 fun above (Envir {tenv, tyenv, ...}) lim =
   134   (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
   135   (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
   136 
   137 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   138 fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
   139   (case t of
   140     Var (nT as (name', T)) =>
   141       if a = name' then env     (*cycle!*)
   142       else if Term_Ord.indexname_ord (a, name') = LESS then
   143         (case lookup (env, nT) of  (*if already assigned, chase*)
   144           NONE => update ((nT, Var (a, T)), env)
   145         | SOME u => vupdate ((aU, u), env))
   146       else update ((aU, t), env)
   147   | _ => update ((aU, t), env));
   148 
   149 
   150 
   151 (** beta normalization wrt. environment **)
   152 
   153 (*Chases variables in env.  Does not exploit sharing of variable bindings
   154   Does not check types, so could loop.*)
   155 
   156 local
   157 
   158 fun norm_type0 tyenv : typ Same.operation =
   159   let
   160     fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
   161       | norm (TFree _) = raise Same.SAME
   162       | norm (TVar v) =
   163           (case Type.lookup tyenv v of
   164             SOME U => Same.commit norm U
   165           | NONE => raise Same.SAME);
   166   in norm end;
   167 
   168 fun norm_term1 tenv : term Same.operation =
   169   let
   170     fun norm (Var v) =
   171           (case lookup' (tenv, v) of
   172             SOME u => Same.commit norm u
   173           | NONE => raise Same.SAME)
   174       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   175       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   176       | norm (f $ t) =
   177           ((case norm f of
   178              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   179            | nf => nf $ Same.commit norm t)
   180           handle Same.SAME => f $ norm t)
   181       | norm _ = raise Same.SAME;
   182   in norm end;
   183 
   184 fun norm_term2 tenv tyenv : term Same.operation =
   185   let
   186     val normT = norm_type0 tyenv;
   187     fun norm (Const (a, T)) = Const (a, normT T)
   188       | norm (Free (a, T)) = Free (a, normT T)
   189       | norm (Var (xi, T)) =
   190           (case lookup2 (tyenv, tenv) (xi, T) of
   191             SOME u => Same.commit norm u
   192           | NONE => Var (xi, normT T))
   193       | norm (Abs (a, T, body)) =
   194           (Abs (a, normT T, Same.commit norm body)
   195             handle Same.SAME => Abs (a, T, norm body))
   196       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   197       | norm (f $ t) =
   198           ((case norm f of
   199              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   200            | nf => nf $ Same.commit norm t)
   201           handle Same.SAME => f $ norm t)
   202       | norm _ = raise Same.SAME;
   203   in norm end;
   204 
   205 in
   206 
   207 fun norm_type_same tyenv T =
   208   if Vartab.is_empty tyenv then raise Same.SAME
   209   else norm_type0 tyenv T;
   210 
   211 fun norm_types_same tyenv Ts =
   212   if Vartab.is_empty tyenv then raise Same.SAME
   213   else Same.map (norm_type0 tyenv) Ts;
   214 
   215 fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
   216 
   217 fun norm_term_same (Envir {tenv, tyenv, ...}) =
   218   if Vartab.is_empty tyenv then norm_term1 tenv
   219   else norm_term2 tenv tyenv;
   220 
   221 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
   222 fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
   223 
   224 end;
   225 
   226 
   227 (*Put a term into head normal form for unification.*)
   228 
   229 fun head_norm env =
   230   let
   231     fun norm (Var v) =
   232         (case lookup (env, v) of
   233           SOME u => head_norm env u
   234         | NONE => raise Same.SAME)
   235       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   236       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   237       | norm (f $ t) =
   238           (case norm f of
   239             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   240           | nf => nf $ t)
   241       | norm _ = raise Same.SAME;
   242   in Same.commit norm end;
   243 
   244 
   245 (*Eta-contract a term (fully)*)
   246 
   247 local
   248 
   249 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
   250   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   251   | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
   252   | decr _ _ = raise Same.SAME
   253 and decrh lev t = (decr lev t handle Same.SAME => t);
   254 
   255 fun eta (Abs (a, T, body)) =
   256     ((case eta body of
   257         body' as (f $ Bound 0) =>
   258           if loose_bvar1 (f, 0) then Abs (a, T, body')
   259           else decrh 0 f
   260      | body' => Abs (a, T, body')) handle Same.SAME =>
   261         (case body of
   262           f $ Bound 0 =>
   263             if loose_bvar1 (f, 0) then raise Same.SAME
   264             else decrh 0 f
   265         | _ => raise Same.SAME))
   266   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
   267   | eta _ = raise Same.SAME;
   268 
   269 in
   270 
   271 fun eta_contract t =
   272   if Term.has_abs t then Same.commit eta t else t;
   273 
   274 val beta_eta_contract = eta_contract o beta_norm;
   275 
   276 end;
   277 
   278 
   279 (*finds type of term without checking that combinations are consistent
   280   Ts holds types of bound variables*)
   281 fun fastype (Envir {tyenv, ...}) =
   282   let
   283     val funerr = "fastype: expected function type";
   284     fun fast Ts (f $ u) =
   285           (case Type.devar tyenv (fast Ts f) of
   286             Type ("fun", [_, T]) => T
   287           | TVar v => raise TERM (funerr, [f $ u])
   288           | _ => raise TERM (funerr, [f $ u]))
   289       | fast Ts (Const (_, T)) = T
   290       | fast Ts (Free (_, T)) = T
   291       | fast Ts (Bound i) =
   292           (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
   293       | fast Ts (Var (_, T)) = T
   294       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
   295   in fast end;
   296 
   297 
   298 
   299 (** plain substitution -- without variable chasing **)
   300 
   301 local
   302 
   303 fun subst_type0 tyenv = Term_Subst.map_atypsT_same
   304   (fn TVar v =>
   305         (case Type.lookup tyenv v of
   306           SOME U => U
   307         | NONE => raise Same.SAME)
   308     | _ => raise Same.SAME);
   309 
   310 fun subst_term1 tenv = Term_Subst.map_aterms_same
   311   (fn Var v =>
   312         (case lookup' (tenv, v) of
   313           SOME u => u
   314         | NONE => raise Same.SAME)
   315     | _ => raise Same.SAME);
   316 
   317 fun subst_term2 tenv tyenv : term Same.operation =
   318   let
   319     val substT = subst_type0 tyenv;
   320     fun subst (Const (a, T)) = Const (a, substT T)
   321       | subst (Free (a, T)) = Free (a, substT T)
   322       | subst (Var (xi, T)) =
   323           (case lookup' (tenv, (xi, T)) of
   324             SOME u => u
   325           | NONE => Var (xi, substT T))
   326       | subst (Bound _) = raise Same.SAME
   327       | subst (Abs (a, T, t)) =
   328           (Abs (a, substT T, Same.commit subst t)
   329             handle Same.SAME => Abs (a, T, subst t))
   330       | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   331   in subst end;
   332 
   333 in
   334 
   335 fun subst_type_same tyenv T =
   336   if Vartab.is_empty tyenv then raise Same.SAME
   337   else subst_type0 tyenv T;
   338 
   339 fun subst_term_types_same tyenv t =
   340   if Vartab.is_empty tyenv then raise Same.SAME
   341   else Term_Subst.map_types_same (subst_type0 tyenv) t;
   342 
   343 fun subst_term_same (tyenv, tenv) =
   344   if Vartab.is_empty tenv then subst_term_types_same tyenv
   345   else if Vartab.is_empty tyenv then subst_term1 tenv
   346   else subst_term2 tenv tyenv;
   347 
   348 fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   349 fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   350 fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   351 
   352 end;
   353 
   354 
   355 
   356 (** expand defined atoms -- with local beta reduction **)
   357 
   358 fun expand_atom T (U, u) =
   359   subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   360     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   361 
   362 fun expand_term get =
   363   let
   364     fun expand tm =
   365       let
   366         val (head, args) = Term.strip_comb tm;
   367         val args' = map expand args;
   368         fun comb head' = Term.list_comb (head', args');
   369       in
   370         (case head of
   371           Abs (x, T, t) => comb (Abs (x, T, expand t))
   372         | _ =>
   373           (case get head of
   374             SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   375           | NONE => comb head))
   376       end;
   377   in expand end;
   378 
   379 fun expand_term_frees defs =
   380   let
   381     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   382     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   383   in expand_term get end;
   384 
   385 end;