src/Pure/unify.ML
changeset 651 4b0455fbcc49
parent 646 7928c9760667
child 922 196ca0973a6d
     1.1 --- a/src/Pure/unify.ML	Fri Oct 21 09:51:01 1994 +0100
     1.2 +++ b/src/Pure/unify.ML	Fri Oct 21 09:53:38 1994 +0100
     1.3 @@ -479,7 +479,9 @@
     1.4  fun ff_assign(env, rbinder, t, u) : Envir.env = 
     1.5  let val (v,T) = get_eta_var(rbinder,0,t)
     1.6  in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
     1.7 -   else let val env = unify_types(body_type env T,fastype env (rbinder,u),env)
     1.8 +   else let val env = unify_types(body_type env T,
     1.9 +				  fastype env (rbinder,u),
    1.10 +				  env)
    1.11  	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
    1.12  end;
    1.13  
    1.14 @@ -495,31 +497,41 @@
    1.15  
    1.16  
    1.17  (*If an argument contains a banned Bound, then it should be deleted.
    1.18 -  But if the path is flexible, this is difficult; the code gives up!*)
    1.19 -exception CHANGE and CHANGE_FAIL;   (*rigid and flexible occurrences*)
    1.20 +  But if the only path is flexible, this is difficult; the code gives up!
    1.21 +  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
    1.22 +exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
    1.23  
    1.24  
    1.25 -(*Squash down indices at level >=lev to delete the js from a term.
    1.26 -  flex should initially be false, since the empty path is rigid.*)
    1.27 -fun change_bnos (lev, js, flex) t = 
    1.28 +(*Check whether the 'banned' bound var indices occur rigidly in t*)
    1.29 +fun rigid_bound (lev, banned) t = 
    1.30    let val (head,args) = strip_comb t 
    1.31 -      val flex' = flex orelse is_Var head
    1.32 -      val head' = case head of
    1.33 -	    Bound i => 
    1.34 -		if i<lev then Bound i
    1.35 -		else  if (i-lev) mem js  
    1.36 -                      then  if flex then raise CHANGE_FAIL
    1.37 -                                    else raise CHANGE
    1.38 -		else  Bound (i - length (filter (fn j => j < i-lev) js))
    1.39 -	  | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)
    1.40 -	  | _ => head
    1.41 -  in  list_comb (head', map (change_bnos (lev, js, flex')) args)
    1.42 +  in  
    1.43 +      case head of
    1.44 +	  Bound i => (i-lev) mem banned  orelse
    1.45 +	      	     exists (rigid_bound (lev, banned)) args
    1.46 +	| Var _ => false	(*no rigid occurrences here!*)
    1.47 +	| Abs (_,_,u) => 
    1.48 +	       rigid_bound(lev+1, banned) u  orelse
    1.49 +	       exists (rigid_bound (lev, banned)) args
    1.50 +	| _ => exists (rigid_bound (lev, banned)) args
    1.51    end;
    1.52  
    1.53 +(*Squash down indices at level >=lev to delete the banned from a term.*)
    1.54 +fun change_bnos banned =
    1.55 +  let fun change lev (Bound i) = 
    1.56 +	    if i<lev then Bound i
    1.57 +	    else  if (i-lev) mem banned  
    1.58 +		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
    1.59 +	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
    1.60 +	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
    1.61 +	| change lev (t$u) = change lev t $ change lev u
    1.62 +	| change lev t = t
    1.63 +  in  change 0  end;
    1.64  
    1.65  (*Change indices, delete the argument if it contains a banned Bound*)
    1.66 -fun change_arg js ({j,t,T}, args) : flarg list =
    1.67 -    {j=j, t= change_bnos(0,js,false)t, T=T} :: args    handle CHANGE => args;
    1.68 +fun change_arg banned ({j,t,T}, args) : flarg list =
    1.69 +    if rigid_bound (0, banned) t  then  args	(*delete argument!*)
    1.70 +    else  {j=j, t= change_bnos banned t, T=T} :: args;
    1.71  
    1.72  
    1.73  (*Sort the arguments to create assignments if possible:
    1.74 @@ -570,8 +582,8 @@
    1.75    let val loot = loose_bnos t  and  loou = loose_bnos u
    1.76        fun add_index (((a,T), j), (bnos, newbinder)) = 
    1.77              if  j mem loot  andalso  j mem loou 
    1.78 -            then  (bnos, (a,T)::newbinder)
    1.79 -            else  (j::bnos, newbinder);
    1.80 +            then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
    1.81 +            else  (j::bnos, newbinder);		(*remove*)
    1.82        val indices = 0 upto (length rbinder - 1);
    1.83        val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
    1.84        val (env', t') = clean_term banned (env, t);