51 |
51 |
52 |
52 |
53 type binderlist = (string * typ) list; |
53 type binderlist = (string * typ) list; |
54 |
54 |
55 type dpair = binderlist * term * term; |
55 type dpair = binderlist * term * term; |
56 |
|
57 fun body_type env = |
|
58 let |
|
59 val tyenv = Envir.type_env env; |
|
60 fun bT (Type ("fun", [_, T])) = bT T |
|
61 | bT (T as TVar v) = |
|
62 (case Type.lookup tyenv v of |
|
63 NONE => T |
|
64 | SOME T' => bT T') |
|
65 | bT T = T; |
|
66 in bT end; |
|
67 |
|
68 fun binder_types env = |
|
69 let |
|
70 val tyenv = Envir.type_env env; |
|
71 fun bTs (Type ("fun", [T, U])) = T :: bTs U |
|
72 | bTs (TVar v) = |
|
73 (case Type.lookup tyenv v of |
|
74 NONE => [] |
|
75 | SOME T' => bTs T') |
|
76 | bTs _ = []; |
|
77 in bTs end; |
|
78 |
|
79 fun strip_type env T = (binder_types env T, body_type env T); |
|
80 |
56 |
81 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; |
57 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; |
82 |
58 |
83 |
59 |
84 (* eta normal form *) |
60 (* eta normal form *) |
232 If v occurs nonrigidly then must use full algorithm. *) |
208 If v occurs nonrigidly then must use full algorithm. *) |
233 fun assignment thy (rbinder, t, u) env = |
209 fun assignment thy (rbinder, t, u) env = |
234 let val vT as (v,T) = get_eta_var (rbinder, 0, t) in |
210 let val vT as (v,T) = get_eta_var (rbinder, 0, t) in |
235 (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of |
211 (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of |
236 NoOcc => |
212 NoOcc => |
237 let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env |
213 let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env |
238 in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end |
214 in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end |
239 | Nonrigid => raise ASSIGN |
215 | Nonrigid => raise ASSIGN |
240 | Rigid => raise CANTUNIFY) |
216 | Rigid => raise CANTUNIFY) |
241 end; |
217 end; |
242 |
218 |
281 | SIMRANDS (_, _, env) = (env, flexflex, flexrigid); |
257 | SIMRANDS (_, _, env) = (env, flexflex, flexrigid); |
282 in |
258 in |
283 (case (head_of t, head_of u) of |
259 (case (head_of t, head_of u) of |
284 (Var (_, T), Var (_, U)) => |
260 (Var (_, T), Var (_, U)) => |
285 let |
261 let |
286 val T' = body_type env T and U' = body_type env U; |
262 val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U; |
287 val env = unify_types thy (T', U') env; |
263 val env = unify_types thy (T', U') env; |
288 in (env, dp :: flexflex, flexrigid) end |
264 in (env, dp :: flexflex, flexrigid) end |
289 | (Var _, _) => |
265 | (Var _, _) => |
290 ((assignment thy (rbinder,t,u) env, flexflex, flexrigid) |
266 ((assignment thy (rbinder,t,u) env, flexflex, flexrigid) |
291 handle ASSIGN => (env, flexflex, dp :: flexrigid)) |
267 handle ASSIGN => (env, flexflex, dp :: flexrigid)) |
338 (*Abstraction over a list of types*) |
314 (*Abstraction over a list of types*) |
339 fun types_abs ([], u) = u |
315 fun types_abs ([], u) = u |
340 | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); |
316 | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); |
341 |
317 |
342 (*Abstraction over the binder of a type*) |
318 (*Abstraction over the binder of a type*) |
343 fun type_abs (env, T, t) = types_abs (binder_types env T, t); |
319 fun type_abs (env, T, t) = types_abs (Envir.binder_types env ~1 T, t); |
344 |
320 |
345 |
321 |
346 (*MATCH taking "big steps". |
322 (*MATCH taking "big steps". |
347 Copies u into the Var v, using projection on targs or imitation. |
323 Copies u into the Var v, using projection on targs or imitation. |
348 A projection is allowed unless SIMPL raises an exception. |
324 A projection is allowed unless SIMPL raises an exception. |
364 (env, dpairs))); |
340 (env, dpairs))); |
365 (*Produce sequence of all possible ways of copying the arg list*) |
341 (*Produce sequence of all possible ways of copying the arg list*) |
366 fun copyargs [] = Seq.cons ([], ed) Seq.empty |
342 fun copyargs [] = Seq.cons ([], ed) Seq.empty |
367 | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); |
343 | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); |
368 val (uhead, uargs) = strip_comb u; |
344 val (uhead, uargs) = strip_comb u; |
369 val base = body_type env (fastype env (rbinder, uhead)); |
345 val base = Envir.body_type env ~1 (fastype env (rbinder, uhead)); |
370 fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); |
346 fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); |
371 (*attempt projection on argument with given typ*) |
347 (*attempt projection on argument with given typ*) |
372 val Ts = map (curry (fastype env) rbinder) targs; |
348 val Ts = map (curry (fastype env) rbinder) targs; |
373 fun projenv (head, (Us, bary), targ, tail) = |
349 fun projenv (head, (Us, bary), targ, tail) = |
374 let |
350 let |
393 (Bound(length Ts), T, targ) :: make_projs (Ts,targs) |
369 (Bound(length Ts), T, targ) :: make_projs (Ts,targs) |
394 | make_projs ([],[]) = [] |
370 | make_projs ([],[]) = [] |
395 | make_projs _ = raise TERM ("make_projs", u::targs); |
371 | make_projs _ = raise TERM ("make_projs", u::targs); |
396 (*try projections and imitation*) |
372 (*try projections and imitation*) |
397 fun matchfun ((bvar,T,targ)::projs) = |
373 fun matchfun ((bvar,T,targ)::projs) = |
398 (projenv(bvar, strip_type env T, targ, matchfun projs)) |
374 (projenv(bvar, Envir.strip_type env ~1 T, targ, matchfun projs)) |
399 | matchfun [] = (*imitation last of all*) |
375 | matchfun [] = (*imitation last of all*) |
400 (case uhead of |
376 (case uhead of |
401 Const _ => Seq.map joinargs (copyargs uargs) |
377 Const _ => Seq.map joinargs (copyargs uargs) |
402 | Free _ => Seq.map joinargs (copyargs uargs) |
378 | Free _ => Seq.map joinargs (copyargs uargs) |
403 | _ => Seq.empty) (*if Var, would be a loop!*) |
379 | _ => Seq.empty) (*if Var, would be a loop!*) |
420 |
396 |
421 (*Call matchcopy to produce assignments to the variable in the dpair*) |
397 (*Call matchcopy to produce assignments to the variable in the dpair*) |
422 fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq = |
398 fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq = |
423 let |
399 let |
424 val (Var (vT as (v, T)), targs) = strip_comb t; |
400 val (Var (vT as (v, T)), targs) = strip_comb t; |
425 val Ts = binder_types env T; |
401 val Ts = Envir.binder_types env ~1 T; |
426 fun new_dset (u', (env', dpairs')) = |
402 fun new_dset (u', (env', dpairs')) = |
427 (*if v was updated to s, must unify s with u' *) |
403 (*if v was updated to s, must unify s with u' *) |
428 (case Envir.lookup env' vT of |
404 (case Envir.lookup env' vT of |
429 NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs') |
405 NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs') |
430 | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs')); |
406 | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs')); |
440 Attempts to update t with u, raising ASSIGN if impossible*) |
416 Attempts to update t with u, raising ASSIGN if impossible*) |
441 fun ff_assign thy (env, rbinder, t, u) : Envir.env = |
417 fun ff_assign thy (env, rbinder, t, u) : Envir.env = |
442 let val vT as (v, T) = get_eta_var (rbinder, 0, t) in |
418 let val vT as (v, T) = get_eta_var (rbinder, 0, t) in |
443 if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN |
419 if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN |
444 else |
420 else |
445 let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env |
421 let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env |
446 in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end |
422 in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end |
447 end; |
423 end; |
448 |
424 |
449 |
425 |
450 (*If an argument contains a banned Bound, then it should be deleted. |
426 (*If an argument contains a banned Bound, then it should be deleted. |
520 Force an assignment, if possible, by sorting the arguments. |
496 Force an assignment, if possible, by sorting the arguments. |
521 Update its head; squash indices in arguments. *) |
497 Update its head; squash indices in arguments. *) |
522 fun clean_term banned (env,t) = |
498 fun clean_term banned (env,t) = |
523 let |
499 let |
524 val (Var (v, T), ts) = strip_comb t; |
500 val (Var (v, T), ts) = strip_comb t; |
525 val (Ts, U) = strip_type env T |
501 val (Ts, U) = Envir.strip_type env ~1 T |
526 and js = length ts - 1 downto 0; |
502 and js = length ts - 1 downto 0; |
527 val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) []) |
503 val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) []) |
528 val ts' = map #t args; |
504 val ts' = map #t args; |
529 in |
505 in |
530 if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts'))) |
506 if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts'))) |
662 Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) |
638 Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) |
663 fun smash_flexflex1 (t, u) env : Envir.env = |
639 fun smash_flexflex1 (t, u) env : Envir.env = |
664 let |
640 let |
665 val vT as (v, T) = var_head_of (env, t) |
641 val vT as (v, T) = var_head_of (env, t) |
666 and wU as (w, U) = var_head_of (env, u); |
642 and wU as (w, U) = var_head_of (env, u); |
667 val (env', var) = Envir.genvar (#1 v) (env, body_type env T); |
643 val (env', var) = Envir.genvar (#1 v) (env, Envir.body_type env ~1 T); |
668 val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env'; |
644 val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env'; |
669 in |
645 in |
670 if vT = wU then env'' (*the other update would be identical*) |
646 if vT = wU then env'' (*the other update would be identical*) |
671 else Envir.vupdate (vT, type_abs (env', T, var)) env'' |
647 else Envir.vupdate (vT, type_abs (env', T, var)) env'' |
672 end; |
648 end; |