src/Pure/unify.ML
changeset 15531 08c8dad8e399
parent 15275 baa90469961a
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/unify.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/unify.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -50,14 +50,14 @@
     1.4  fun body_type(Envir.Envir{iTs,...}) = 
     1.5  let fun bT(Type("fun",[_,T])) = bT T
     1.6        | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
     1.7 -		None => T | Some(T') => bT T')
     1.8 +		NONE => T | SOME(T') => bT T')
     1.9        | bT T = T
    1.10  in bT end;
    1.11  
    1.12  fun binder_types(Envir.Envir{iTs,...}) = 
    1.13  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.14        | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    1.15 -		None => [] | Some(T') => bTs T')
    1.16 +		NONE => [] | SOME(T') => bTs T')
    1.17        | bTs _ = []
    1.18  in bTs end;
    1.19  
    1.20 @@ -72,7 +72,7 @@
    1.21  	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    1.22  	| etif (TVar(ixn,_),t) = 
    1.23  	    (case Vartab.lookup (iTs,ixn) of
    1.24 -		  None => t | Some(T) => etif(T,t))
    1.25 +		  NONE => t | SOME(T) => etif(T,t))
    1.26  	| etif (_,t) = t;
    1.27        fun eta_nm (rbinder, Abs(a,T,body)) =
    1.28  	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
    1.29 @@ -98,8 +98,8 @@
    1.30  	      (*no need to lookup: v has no assignment*)
    1.31  	    else (seen := w:: !seen;  
    1.32  	          case  Envir.lookup(env,w)  of
    1.33 -		      None    => false
    1.34 -		    | Some t => occur t)
    1.35 +		      NONE    => false
    1.36 +		    | SOME t => occur t)
    1.37  	| occur (Abs(_,_,body)) = occur body
    1.38  	| occur (f$t) = occur t  orelse   occur f
    1.39    in  occurs ts  end;
    1.40 @@ -110,7 +110,7 @@
    1.41  fun head_of_in (env,t) : term = case t of
    1.42      f$_ => head_of_in(env,f)
    1.43    | Var (v,_) => (case  Envir.lookup(env,v)  of  
    1.44 -			Some u => head_of_in(env,u)  |  None   => t)
    1.45 +			SOME u => head_of_in(env,u)  |  NONE   => t)
    1.46    | _ => t;
    1.47  
    1.48  
    1.49 @@ -160,8 +160,8 @@
    1.50  	    else if eq_ix(v,w) then Rigid
    1.51  	    else (seen := w:: !seen;  
    1.52  	          case  Envir.lookup(env,w)  of
    1.53 -		      None    => NoOcc
    1.54 -		    | Some t => occur t)
    1.55 +		      NONE    => NoOcc
    1.56 +		    | SOME t => occur t)
    1.57  	| occur (Abs(_,_,body)) = occur body
    1.58  	| occur (t as f$_) =  (*switch to nonrigid search?*)
    1.59  	   (case head_of_in (env,f) of
    1.60 @@ -283,7 +283,7 @@
    1.61  (* changed(env,t) checks whether the head of t is a variable assigned in env*)
    1.62  fun changed (env, f$_) = changed (env,f)
    1.63    | changed (env, Var (v,_)) =
    1.64 -      (case Envir.lookup(env,v) of None=>false  |  _ => true)
    1.65 +      (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
    1.66    | changed _ = false;
    1.67  
    1.68  
    1.69 @@ -358,7 +358,7 @@
    1.70  		val dp = (rbinder, list_comb(targ, map plugin args), u);
    1.71  		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
    1.72  		    (*may raise exception CANTUNIFY*)
    1.73 -	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
    1.74 +	    in  SOME ((list_comb(head,args), (env2, frigid@fflex)),
    1.75  			tail)
    1.76  	    end  handle CANTUNIFY => Seq.pull tail)
    1.77  	end handle CANTUNIFY => tail;
    1.78 @@ -400,8 +400,8 @@
    1.79        fun new_dset (u', (env',dpairs')) =
    1.80  	  (*if v was updated to s, must unify s with u' *)
    1.81  	  case Envir.lookup(env',v) of
    1.82 -	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
    1.83 -	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
    1.84 +	      NONE => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
    1.85 +	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
    1.86    in Seq.map new_dset
    1.87           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
    1.88    end;
    1.89 @@ -575,7 +575,7 @@
    1.90  		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
    1.91  		SIMPL (env,dpairs))
    1.92  	  in case flexrigid of
    1.93 -	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
    1.94 +	      [] => SOME (foldr add_ffpair (flexflex, (env',[])), reseq)
    1.95  	    | dp::frigid' => 
    1.96  		if tdepth > !search_bound then
    1.97  		    (warning "Unification bound exceeded"; Seq.pull reseq)