src/Pure/unify.ML
author clasohm
Mon Jan 29 14:16:13 1996 +0100 (1996-01-29)
changeset 1460 5a6f2aabd538
parent 1458 fd510875fb71
child 1505 14f4c55bbe9a
permissions -rw-r--r--
inserted tabs again
clasohm@1460
     1
(*  Title: 	unify
clasohm@0
     2
    ID:         $Id$
clasohm@1460
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   Cambridge University 1992
clasohm@0
     5
clasohm@0
     6
Higher-Order Unification
clasohm@0
     7
clasohm@0
     8
Potential problem: type of Vars is often ignored, so two Vars with same
clasohm@0
     9
indexname but different types can cause errors!
lcp@646
    10
lcp@646
    11
Types as well as terms are unified.  The outermost functions assume the
lcp@646
    12
terms to be unified already have the same type.  In resolution, this is
lcp@646
    13
assured because both have type "prop".
clasohm@0
    14
*)
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
signature UNIFY = 
clasohm@0
    18
sig
clasohm@0
    19
  structure Sign: SIGN
clasohm@0
    20
  structure Envir : ENVIR
clasohm@0
    21
  structure Sequence : SEQUENCE
clasohm@0
    22
  (*references for control and tracing*)
clasohm@0
    23
  val trace_bound: int ref
clasohm@0
    24
  val trace_simp: bool ref
clasohm@0
    25
  val trace_types: bool ref
clasohm@0
    26
  val search_bound: int ref
clasohm@0
    27
  (*other exports*)
clasohm@0
    28
  val combound : (term*int*int) -> term
clasohm@0
    29
  val rlist_abs: (string*typ)list * term -> term   
clasohm@0
    30
  val smash_unifiers : Sign.sg * Envir.env * (term*term)list
clasohm@1460
    31
	-> (Envir.env Sequence.seq)
clasohm@0
    32
  val unifiers: Sign.sg * Envir.env * ((term*term)list)
clasohm@1460
    33
	-> (Envir.env * (term * term)list) Sequence.seq
clasohm@0
    34
end;
clasohm@0
    35
clasohm@0
    36
functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
clasohm@0
    37
                  and Pattern:PATTERN
clasohm@0
    38
                  sharing type Sign.sg = Pattern.sg
clasohm@0
    39
                  and     type Envir.env = Pattern.env)
clasohm@1460
    40
	: UNIFY = 
clasohm@0
    41
struct
clasohm@0
    42
clasohm@0
    43
structure Sign = Sign;
clasohm@0
    44
structure Envir = Envir;
clasohm@0
    45
structure Sequence = Sequence;
clasohm@0
    46
structure Pretty = Sign.Syntax.Pretty;
clasohm@0
    47
clasohm@0
    48
(*Unification options*)
clasohm@0
    49
clasohm@1460
    50
val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
clasohm@1460
    51
and search_bound = ref 20	(*unification quits above this depth*)
clasohm@1460
    52
and trace_simp = ref false	(*print dpairs before calling SIMPL*)
clasohm@1460
    53
and trace_types = ref false	(*announce potential incompleteness
clasohm@1460
    54
				  of type unification*)
clasohm@0
    55
clasohm@922
    56
val sgr = ref(Sign.proto_pure);
clasohm@0
    57
clasohm@0
    58
type binderlist = (string*typ) list;
clasohm@0
    59
clasohm@0
    60
type dpair = binderlist * term * term;
clasohm@0
    61
clasohm@0
    62
fun body_type(Envir.Envir{iTs,...}) = 
clasohm@0
    63
let fun bT(Type("fun",[_,T])) = bT T
clasohm@0
    64
      | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
clasohm@1460
    65
		None => T | Some(T') => bT T')
clasohm@0
    66
      | bT T = T
clasohm@0
    67
in bT end;
clasohm@0
    68
clasohm@0
    69
fun binder_types(Envir.Envir{iTs,...}) = 
clasohm@0
    70
let fun bTs(Type("fun",[T,U])) = T :: bTs U
clasohm@0
    71
      | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
clasohm@1460
    72
		None => [] | Some(T') => bTs T')
clasohm@0
    73
      | bTs _ = []
clasohm@0
    74
in bTs end;
clasohm@0
    75
clasohm@0
    76
fun strip_type env T = (binder_types env T, body_type env T);
clasohm@0
    77
clasohm@0
    78
clasohm@0
    79
(*Put a term into head normal form for unification.
clasohm@0
    80
  Operands need not be in normal form.  Does eta-expansions on the head,
clasohm@0
    81
  which involves renumbering (thus copying) the args.  To avoid this 
clasohm@0
    82
  inefficiency, avoid partial application:  if an atom is applied to
clasohm@0
    83
  any arguments at all, apply it to its full number of arguments.
clasohm@0
    84
  For
clasohm@1460
    85
    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
clasohm@0
    86
    args  =   [arg1,...,argn]
clasohm@0
    87
  the value of 
clasohm@0
    88
      (xm,...,x1)(head(arg1,...,argn))  remains invariant.
clasohm@0
    89
*)
clasohm@0
    90
clasohm@0
    91
local exception SAME
clasohm@0
    92
in
clasohm@0
    93
  fun head_norm (env,t) : term =
clasohm@0
    94
    let fun hnorm (Var (v,T)) = 
clasohm@1460
    95
	      (case Envir.lookup (env,v) of
clasohm@1460
    96
		  Some u => head_norm (env, u)
clasohm@1460
    97
		| None   => raise SAME)
clasohm@1460
    98
	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
clasohm@1460
    99
	  | hnorm (Abs(_,_,body) $ t) =
clasohm@1460
   100
	      head_norm (env, subst_bounds([t], body))
clasohm@1460
   101
	  | hnorm (f $ t) =
clasohm@1460
   102
	      (case hnorm f of
clasohm@1460
   103
		 Abs(_,_,body) =>
clasohm@1460
   104
		   head_norm (env, subst_bounds([t], body))
clasohm@1460
   105
	       | nf => nf $ t)
clasohm@1460
   106
	  | hnorm _ =  raise SAME
clasohm@0
   107
    in  hnorm t  handle SAME=> t  end
clasohm@0
   108
end;
clasohm@0
   109
clasohm@0
   110
clasohm@0
   111
(*finds type of term without checking that combinations are consistent
clasohm@0
   112
  rbinder holds types of bound variables*)
clasohm@0
   113
fun fastype (Envir.Envir{iTs,...}) =
clasohm@0
   114
let val funerr = "fastype: expected function type";
clasohm@0
   115
    fun fast(rbinder, f$u) =
clasohm@1460
   116
	(case (fast (rbinder, f)) of
clasohm@1460
   117
	   Type("fun",[_,T]) => T
clasohm@1460
   118
	 | TVar(ixn,_) =>
clasohm@1460
   119
		(case assoc(iTs,ixn) of
clasohm@1460
   120
		   Some(Type("fun",[_,T])) => T
clasohm@1460
   121
		 | _ => raise TERM(funerr, [f$u]))
clasohm@1460
   122
	 | _ => raise TERM(funerr, [f$u]))
clasohm@0
   123
      | fast (rbinder, Const (_,T)) = T
clasohm@0
   124
      | fast (rbinder, Free (_,T)) = T
clasohm@0
   125
      | fast (rbinder, Bound i) =
clasohm@1460
   126
	(#2 (nth_elem (i,rbinder))
clasohm@1460
   127
  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
clasohm@0
   128
      | fast (rbinder, Var (_,T)) = T 
clasohm@0
   129
      | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
clasohm@0
   130
in fast end;
clasohm@0
   131
clasohm@0
   132
clasohm@0
   133
(*Eta normal form*)
clasohm@0
   134
fun eta_norm(env as Envir.Envir{iTs,...}) =
clasohm@0
   135
  let fun etif (Type("fun",[T,U]), t) =
clasohm@1460
   136
	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
clasohm@1460
   137
	| etif (TVar(ixn,_),t) = 
clasohm@1460
   138
	    (case assoc(iTs,ixn) of
clasohm@1460
   139
		  None => t | Some(T) => etif(T,t))
clasohm@1460
   140
	| etif (_,t) = t;
clasohm@0
   141
      fun eta_nm (rbinder, Abs(a,T,body)) =
clasohm@1460
   142
	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
clasohm@1460
   143
	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
clasohm@0
   144
  in eta_nm end;
clasohm@0
   145
clasohm@0
   146
clasohm@0
   147
(*OCCURS CHECK
clasohm@0
   148
  Does the uvar occur in the term t?  
clasohm@0
   149
  two forms of search, for whether there is a rigid path to the current term.
clasohm@0
   150
  "seen" is list of variables passed thru, is a memo variable for sharing.
clasohm@0
   151
  This version searches for nonrigid occurrence, returns true if found. *)
clasohm@0
   152
fun occurs_terms (seen: (indexname list) ref,
clasohm@1460
   153
 		  env: Envir.env, v: indexname, ts: term list): bool =
clasohm@0
   154
  let fun occurs [] = false
clasohm@1460
   155
	| occurs (t::ts) =  occur t  orelse  occurs ts
clasohm@0
   156
      and occur (Const _)  = false
clasohm@1460
   157
	| occur (Bound _)  = false
clasohm@1460
   158
	| occur (Free _)  = false
clasohm@1460
   159
	| occur (Var (w,_))  = 
clasohm@1460
   160
	    if w mem !seen then false
clasohm@1460
   161
	    else if v=w then true
clasohm@1460
   162
	      (*no need to lookup: v has no assignment*)
clasohm@1460
   163
	    else (seen := w:: !seen;  
clasohm@1460
   164
	          case  Envir.lookup(env,w)  of
clasohm@1460
   165
		      None    => false
clasohm@1460
   166
		    | Some t => occur t)
clasohm@1460
   167
	| occur (Abs(_,_,body)) = occur body
clasohm@1460
   168
	| occur (f$t) = occur t  orelse   occur f
clasohm@0
   169
  in  occurs ts  end;
clasohm@0
   170
clasohm@0
   171
clasohm@0
   172
clasohm@0
   173
(* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
clasohm@0
   174
fun head_of_in (env,t) : term = case t of
clasohm@0
   175
    f$_ => head_of_in(env,f)
clasohm@0
   176
  | Var (v,_) => (case  Envir.lookup(env,v)  of  
clasohm@1460
   177
			Some u => head_of_in(env,u)  |  None   => t)
clasohm@0
   178
  | _ => t;
clasohm@0
   179
clasohm@0
   180
clasohm@0
   181
datatype occ = NoOcc | Nonrigid | Rigid;
clasohm@0
   182
clasohm@0
   183
(* Rigid occur check
clasohm@0
   184
Returns Rigid    if it finds a rigid occurrence of the variable,
clasohm@0
   185
        Nonrigid if it finds a nonrigid path to the variable.
clasohm@0
   186
        NoOcc    otherwise.
clasohm@0
   187
  Continues searching for a rigid occurrence even if it finds a nonrigid one.
clasohm@0
   188
clasohm@0
   189
Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
clasohm@0
   190
   a rigid path to the variable, appearing with no arguments.
clasohm@0
   191
Here completeness is sacrificed in order to reduce danger of divergence:
clasohm@0
   192
   reject ALL rigid paths to the variable.
clasohm@0
   193
Could check for rigid paths to bound variables that are out of scope.  
clasohm@0
   194
Not necessary because the assignment test looks at variable's ENTIRE rbinder.
clasohm@0
   195
clasohm@0
   196
Treatment of head(arg1,...,argn):
clasohm@0
   197
If head is a variable then no rigid path, switch to nonrigid search
clasohm@0
   198
for arg1,...,argn. 
clasohm@0
   199
If head is an abstraction then possibly no rigid path (head could be a 
clasohm@0
   200
   constant function) so again use nonrigid search.  Happens only if
clasohm@0
   201
   term is not in normal form. 
clasohm@0
   202
clasohm@0
   203
Warning: finds a rigid occurrence of ?f in ?f(t).
clasohm@0
   204
  Should NOT be called in this case: there is a flex-flex unifier
clasohm@0
   205
*)
clasohm@0
   206
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
clasohm@0
   207
  let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
clasohm@1460
   208
		       else NoOcc
clasohm@0
   209
      fun occurs [] = NoOcc
clasohm@1460
   210
	| occurs (t::ts) =
clasohm@0
   211
            (case occur t of
clasohm@0
   212
               Rigid => Rigid
clasohm@0
   213
             | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
clasohm@0
   214
      and occomb (f$t) =
clasohm@0
   215
            (case occur t of
clasohm@0
   216
               Rigid => Rigid
clasohm@0
   217
             | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
clasohm@0
   218
        | occomb t = occur t
clasohm@0
   219
      and occur (Const _)  = NoOcc
clasohm@1460
   220
	| occur (Bound _)  = NoOcc
clasohm@1460
   221
	| occur (Free _)  = NoOcc
clasohm@1460
   222
	| occur (Var (w,_))  = 
clasohm@1460
   223
	    if w mem !seen then NoOcc
clasohm@1460
   224
	    else if v=w then Rigid
clasohm@1460
   225
	    else (seen := w:: !seen;  
clasohm@1460
   226
	          case  Envir.lookup(env,w)  of
clasohm@1460
   227
		      None    => NoOcc
clasohm@1460
   228
		    | Some t => occur t)
clasohm@1460
   229
	| occur (Abs(_,_,body)) = occur body
clasohm@1460
   230
	| occur (t as f$_) =  (*switch to nonrigid search?*)
clasohm@1460
   231
	   (case head_of_in (env,f) of
clasohm@1460
   232
	      Var (w,_) => (*w is not assigned*)
clasohm@1460
   233
		if v=w then Rigid  
clasohm@1460
   234
		else  nonrigid t
clasohm@1460
   235
	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
clasohm@1460
   236
	    | _ => occomb t)
clasohm@0
   237
  in  occur t  end;
clasohm@0
   238
clasohm@0
   239
clasohm@1460
   240
exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
clasohm@1460
   241
exception ASSIGN;	(*Raised if not an assignment*)
clasohm@0
   242
clasohm@0
   243
clasohm@0
   244
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
nipkow@1435
   245
  if T=U then env
nipkow@1435
   246
  else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr)))
nipkow@1435
   247
                                                maxidx iTs (U,T)
nipkow@1435
   248
       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
nipkow@1435
   249
       handle Sign.Type.TUNIFY => raise CANTUNIFY;
clasohm@0
   250
clasohm@0
   251
fun test_unify_types(args as (T,U,_)) =
clasohm@0
   252
let val sot = Sign.string_of_typ (!sgr);
clasohm@0
   253
    fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
clasohm@0
   254
    val env' = unify_types(args)
clasohm@0
   255
in if is_TVar(T) orelse is_TVar(U) then warn() else ();
clasohm@0
   256
   env'
clasohm@0
   257
end;
clasohm@0
   258
clasohm@0
   259
(*Is the term eta-convertible to a single variable with the given rbinder?
clasohm@0
   260
  Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
clasohm@0
   261
  Result is var a for use in SIMPL. *)
clasohm@0
   262
fun get_eta_var ([], _, Var vT)  =  vT
clasohm@0
   263
  | get_eta_var (_::rbinder, n, f $ Bound i) =
clasohm@1460
   264
	if  n=i  then  get_eta_var (rbinder, n+1, f) 
clasohm@1460
   265
		 else  raise ASSIGN
clasohm@0
   266
  | get_eta_var _ = raise ASSIGN;
clasohm@0
   267
clasohm@0
   268
clasohm@0
   269
(* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
clasohm@0
   270
fun rlist_abs ([], body) = body
clasohm@0
   271
  | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
clasohm@0
   272
clasohm@0
   273
clasohm@0
   274
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
clasohm@0
   275
  If v occurs rigidly then nonunifiable.
clasohm@0
   276
  If v occurs nonrigidly then must use full algorithm. *)
clasohm@0
   277
fun assignment (env, rbinder, t, u) =
clasohm@0
   278
    let val (v,T) = get_eta_var(rbinder,0,t)
clasohm@0
   279
    in  case rigid_occurs_term (ref[], env, v, u) of
clasohm@1460
   280
	      NoOcc => let val env = unify_types(body_type env T,
clasohm@1460
   281
						 fastype env (rbinder,u),env)
clasohm@1460
   282
		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
clasohm@1460
   283
	    | Nonrigid =>  raise ASSIGN
clasohm@1460
   284
	    | Rigid =>  raise CANTUNIFY
clasohm@0
   285
    end;
clasohm@0
   286
clasohm@0
   287
clasohm@0
   288
(*Extends an rbinder with a new disagreement pair, if both are abstractions.
clasohm@0
   289
  Tries to unify types of the bound variables!
clasohm@0
   290
  Checks that binders have same length, since terms should be eta-normal;
clasohm@0
   291
    if not, raises TERM, probably indicating type mismatch.
clasohm@0
   292
  Uses variable a (unless the null string) to preserve user's naming.*) 
clasohm@0
   293
fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
clasohm@1460
   294
	let val env' = unify_types(T,U,env)
clasohm@1460
   295
	    val c = if a="" then b else a
clasohm@1460
   296
	in new_dpair((c,T) :: rbinder, body1, body2, env') end
clasohm@0
   297
    | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
clasohm@0
   298
    | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
clasohm@0
   299
    | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
clasohm@0
   300
clasohm@0
   301
clasohm@0
   302
fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
clasohm@0
   303
     new_dpair (rbinder,
clasohm@1460
   304
		eta_norm env (rbinder, head_norm(env,t)),
clasohm@1460
   305
	  	eta_norm env (rbinder, head_norm(env,u)), env);
clasohm@0
   306
clasohm@0
   307
clasohm@0
   308
clasohm@0
   309
(*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
clasohm@0
   310
  Does not perform assignments for flex-flex pairs:
lcp@646
   311
    may create nonrigid paths, which prevent other assignments.
lcp@646
   312
  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
lcp@646
   313
    do so caused numerous problems with no compensating advantage.
lcp@646
   314
*)
clasohm@0
   315
fun SIMPL0 (dp0, (env,flexflex,flexrigid))
clasohm@1460
   316
	: Envir.env * dpair list * dpair list =
clasohm@0
   317
    let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
clasohm@1460
   318
	    fun SIMRANDS(f$t, g$u, env) =
clasohm@1460
   319
			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
clasohm@1460
   320
	      | SIMRANDS (t as _$_, _, _) =
clasohm@1460
   321
		raise TERM ("SIMPL: operands mismatch", [t,u])
clasohm@1460
   322
	      | SIMRANDS (t, u as _$_, _) =
clasohm@1460
   323
		raise TERM ("SIMPL: operands mismatch", [t,u])
clasohm@1460
   324
	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
clasohm@0
   325
    in case (head_of t, head_of u) of
clasohm@0
   326
       (Var(_,T), Var(_,U)) =>
clasohm@1460
   327
	    let val T' = body_type env T and U' = body_type env U;
clasohm@1460
   328
		val env = unify_types(T',U',env)
clasohm@1460
   329
	    in (env, dp::flexflex, flexrigid) end
clasohm@0
   330
     | (Var _, _) =>
clasohm@1460
   331
	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
clasohm@1460
   332
	     handle ASSIGN => (env, flexflex, dp::flexrigid))
clasohm@0
   333
     | (_, Var _) =>
clasohm@1460
   334
	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
clasohm@1460
   335
	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
clasohm@0
   336
     | (Const(a,T), Const(b,U)) =>
clasohm@1460
   337
	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
clasohm@1460
   338
	    else raise CANTUNIFY
clasohm@0
   339
     | (Bound i,    Bound j)    =>
clasohm@1460
   340
	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
clasohm@0
   341
     | (Free(a,T),  Free(b,U))  =>
clasohm@1460
   342
	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
clasohm@1460
   343
	    else raise CANTUNIFY
clasohm@0
   344
     | _ => raise CANTUNIFY
clasohm@0
   345
    end;
clasohm@0
   346
clasohm@0
   347
clasohm@0
   348
(* changed(env,t) checks whether the head of t is a variable assigned in env*)
clasohm@0
   349
fun changed (env, f$_) = changed (env,f)
clasohm@0
   350
  | changed (env, Var (v,_)) =
clasohm@0
   351
      (case Envir.lookup(env,v) of None=>false  |  _ => true)
clasohm@0
   352
  | changed _ = false;
clasohm@0
   353
clasohm@0
   354
clasohm@0
   355
(*Recursion needed if any of the 'head variables' have been updated
clasohm@0
   356
  Clever would be to re-do just the affected dpairs*)
clasohm@0
   357
fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
clasohm@0
   358
    let val all as (env',flexflex,flexrigid) =
clasohm@1460
   359
	    foldr SIMPL0 (dpairs, (env,[],[]));
clasohm@1460
   360
	val dps = flexrigid@flexflex
clasohm@0
   361
    in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
clasohm@0
   362
       then SIMPL(env',dps) else all
clasohm@0
   363
    end;
clasohm@0
   364
clasohm@0
   365
clasohm@0
   366
(*computes t(Bound(n+k-1),...,Bound(n))  *)
clasohm@0
   367
fun combound (t, n, k) = 
clasohm@0
   368
    if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
clasohm@0
   369
clasohm@0
   370
clasohm@0
   371
(*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
clasohm@0
   372
  Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
clasohm@0
   373
  The B.j are bound vars of binder.
clasohm@0
   374
  The terms are not made in eta-normal-form, SIMPL does that later.  
clasohm@0
   375
  If done here, eta-expansion must be recursive in the arguments! *)
clasohm@0
   376
fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
clasohm@0
   377
  | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
clasohm@0
   378
       let fun funtype T = binder--->T;
clasohm@1460
   379
	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
clasohm@0
   380
       in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
clasohm@0
   381
clasohm@0
   382
clasohm@0
   383
(*Abstraction over a list of types, like list_abs*)
clasohm@0
   384
fun types_abs ([],u) = u
clasohm@0
   385
  | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
clasohm@0
   386
clasohm@0
   387
(*Abstraction over the binder of a type*)
clasohm@0
   388
fun type_abs (env,T,t) = types_abs(binder_types env T, t);
clasohm@0
   389
clasohm@0
   390
clasohm@0
   391
(*MATCH taking "big steps".
clasohm@0
   392
  Copies u into the Var v, using projection on targs or imitation.
clasohm@0
   393
  A projection is allowed unless SIMPL raises an exception.
clasohm@0
   394
  Allocates new variables in projection on a higher-order argument,
clasohm@0
   395
    or if u is a variable (flex-flex dpair).
clasohm@0
   396
  Returns long sequence of every way of copying u, for backtracking
clasohm@0
   397
  For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
clasohm@0
   398
  The order for trying projections is crucial in ?b'(?a)   
clasohm@0
   399
  NB "vname" is only used in the call to make_args!!   *)
clasohm@0
   400
fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
clasohm@1460
   401
	: (term * (Envir.env * dpair list))Sequence.seq =
clasohm@0
   402
let (*Produce copies of uarg and cons them in front of uargs*)
clasohm@0
   403
    fun copycons uarg (uargs, (env, dpairs)) =
clasohm@1460
   404
	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
clasohm@1460
   405
	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
clasohm@1460
   406
		 (env, dpairs)));
clasohm@1460
   407
	(*Produce sequence of all possible ways of copying the arg list*)
clasohm@0
   408
    fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
clasohm@0
   409
      | copyargs (uarg::uargs) =
clasohm@1460
   410
	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
clasohm@0
   411
    val (uhead,uargs) = strip_comb u;
clasohm@0
   412
    val base = body_type env (fastype env (rbinder,uhead));
clasohm@0
   413
    fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
clasohm@0
   414
    (*attempt projection on argument with given typ*)
clasohm@0
   415
    val Ts = map (curry (fastype env) rbinder) targs;
clasohm@0
   416
    fun projenv (head, (Us,bary), targ, tail) = 
clasohm@1460
   417
	let val env = if !trace_types then test_unify_types(base,bary,env)
clasohm@1460
   418
		      else unify_types(base,bary,env)
clasohm@1460
   419
	in Sequence.seqof (fn () =>  
clasohm@1460
   420
	    let val (env',args) = make_args vname (Ts,env,Us);
clasohm@1460
   421
		(*higher-order projection: plug in targs for bound vars*)
clasohm@1460
   422
		fun plugin arg = list_comb(head_of arg, targs);
clasohm@1460
   423
		val dp = (rbinder, list_comb(targ, map plugin args), u);
clasohm@1460
   424
		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
clasohm@1460
   425
		    (*may raise exception CANTUNIFY*)
clasohm@1460
   426
	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
clasohm@1460
   427
			tail)
clasohm@1460
   428
	    end  handle CANTUNIFY => Sequence.pull tail)
clasohm@1460
   429
	end handle CANTUNIFY => tail;
clasohm@0
   430
    (*make a list of projections*)
clasohm@0
   431
    fun make_projs (T::Ts, targ::targs) =
clasohm@1460
   432
	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
clasohm@0
   433
      | make_projs ([],[]) = []
clasohm@0
   434
      | make_projs _ = raise TERM ("make_projs", u::targs);
clasohm@0
   435
    (*try projections and imitation*)
clasohm@0
   436
    fun matchfun ((bvar,T,targ)::projs) =
clasohm@1460
   437
	       (projenv(bvar, strip_type env T, targ, matchfun projs))
clasohm@0
   438
      | matchfun [] = (*imitation last of all*)
clasohm@1460
   439
	      (case uhead of
clasohm@1460
   440
		 Const _ => Sequence.maps joinargs (copyargs uargs)
clasohm@1460
   441
	       | Free _  => Sequence.maps joinargs (copyargs uargs)
clasohm@1460
   442
	       | _ => Sequence.null)  (*if Var, would be a loop!*)
clasohm@0
   443
in case uhead of
clasohm@1460
   444
	Abs(a, T, body) =>
clasohm@1460
   445
	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
clasohm@1460
   446
		(mc ((a,T)::rbinder,
clasohm@1460
   447
			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
clasohm@0
   448
      | Var (w,uary) => 
clasohm@1460
   449
	    (*a flex-flex dpair: make variable for t*)
clasohm@1460
   450
	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
clasohm@1460
   451
		val tabs = combound(newhd, 0, length Ts)
clasohm@1460
   452
		val tsub = list_comb(newhd,targs)
clasohm@1460
   453
	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
clasohm@1460
   454
	    end
clasohm@0
   455
      | _ =>  matchfun(rev(make_projs(Ts, targs)))
clasohm@0
   456
end
clasohm@0
   457
in mc end;
clasohm@0
   458
clasohm@0
   459
clasohm@0
   460
(*Call matchcopy to produce assignments to the variable in the dpair*)
clasohm@0
   461
fun MATCH (env, (rbinder,t,u), dpairs)
clasohm@1460
   462
	: (Envir.env * dpair list)Sequence.seq = 
clasohm@0
   463
  let val (Var(v,T), targs) = strip_comb t;
clasohm@0
   464
      val Ts = binder_types env T;
clasohm@0
   465
      fun new_dset (u', (env',dpairs')) =
clasohm@1460
   466
	  (*if v was updated to s, must unify s with u' *)
clasohm@1460
   467
	  case Envir.lookup(env',v) of
clasohm@1460
   468
	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
clasohm@1460
   469
	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
clasohm@0
   470
  in Sequence.maps new_dset
clasohm@0
   471
         (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
clasohm@0
   472
  end;
clasohm@0
   473
clasohm@0
   474
clasohm@0
   475
clasohm@0
   476
(**** Flex-flex processing ****)
clasohm@0
   477
clasohm@0
   478
(*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
clasohm@0
   479
  Attempts to update t with u, raising ASSIGN if impossible*)
clasohm@0
   480
fun ff_assign(env, rbinder, t, u) : Envir.env = 
clasohm@0
   481
let val (v,T) = get_eta_var(rbinder,0,t)
clasohm@0
   482
in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
lcp@651
   483
   else let val env = unify_types(body_type env T,
clasohm@1460
   484
				  fastype env (rbinder,u),
clasohm@1460
   485
				  env)
clasohm@1460
   486
	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
clasohm@0
   487
end;
clasohm@0
   488
clasohm@0
   489
clasohm@0
   490
(*Flex argument: a term, its type, and the index that refers to it.*)
clasohm@0
   491
type flarg = {t: term,  T: typ,  j: int};
clasohm@0
   492
clasohm@0
   493
clasohm@0
   494
(*Form the arguments into records for deletion/sorting.*)
clasohm@0
   495
fun flexargs ([],[],[]) = [] : flarg list
clasohm@0
   496
  | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
clasohm@0
   497
  | flexargs _ = error"flexargs";
clasohm@0
   498
clasohm@0
   499
clasohm@0
   500
(*If an argument contains a banned Bound, then it should be deleted.
lcp@651
   501
  But if the only path is flexible, this is difficult; the code gives up!
lcp@651
   502
  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
lcp@651
   503
exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
clasohm@0
   504
clasohm@0
   505
lcp@651
   506
(*Check whether the 'banned' bound var indices occur rigidly in t*)
lcp@651
   507
fun rigid_bound (lev, banned) t = 
clasohm@0
   508
  let val (head,args) = strip_comb t 
lcp@651
   509
  in  
lcp@651
   510
      case head of
clasohm@1460
   511
	  Bound i => (i-lev) mem banned  orelse
clasohm@1460
   512
	      	     exists (rigid_bound (lev, banned)) args
clasohm@1460
   513
	| Var _ => false	(*no rigid occurrences here!*)
clasohm@1460
   514
	| Abs (_,_,u) => 
clasohm@1460
   515
	       rigid_bound(lev+1, banned) u  orelse
clasohm@1460
   516
	       exists (rigid_bound (lev, banned)) args
clasohm@1460
   517
	| _ => exists (rigid_bound (lev, banned)) args
clasohm@0
   518
  end;
clasohm@0
   519
lcp@651
   520
(*Squash down indices at level >=lev to delete the banned from a term.*)
lcp@651
   521
fun change_bnos banned =
lcp@651
   522
  let fun change lev (Bound i) = 
clasohm@1460
   523
	    if i<lev then Bound i
clasohm@1460
   524
	    else  if (i-lev) mem banned  
clasohm@1460
   525
		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
clasohm@1460
   526
	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
clasohm@1460
   527
	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
clasohm@1460
   528
	| change lev (t$u) = change lev t $ change lev u
clasohm@1460
   529
	| change lev t = t
lcp@651
   530
  in  change 0  end;
clasohm@0
   531
clasohm@0
   532
(*Change indices, delete the argument if it contains a banned Bound*)
lcp@651
   533
fun change_arg banned ({j,t,T}, args) : flarg list =
clasohm@1460
   534
    if rigid_bound (0, banned) t  then  args	(*delete argument!*)
lcp@651
   535
    else  {j=j, t= change_bnos banned t, T=T} :: args;
clasohm@0
   536
clasohm@0
   537
clasohm@0
   538
(*Sort the arguments to create assignments if possible:
clasohm@0
   539
  create eta-terms like ?g(B.1,B.0) *)
clasohm@0
   540
fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
clasohm@0
   541
  | arg_less (_:flarg, _:flarg) = false;
clasohm@0
   542
clasohm@0
   543
(*Test whether the new term would be eta-equivalent to a variable --
clasohm@0
   544
  if so then there is no point in creating a new variable*)
clasohm@0
   545
fun decreasing n ([]: flarg list) = (n=0)
clasohm@0
   546
  | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
clasohm@0
   547
clasohm@0
   548
(*Delete banned indices in the term, simplifying it.
clasohm@0
   549
  Force an assignment, if possible, by sorting the arguments.
clasohm@0
   550
  Update its head; squash indices in arguments. *)
clasohm@0
   551
fun clean_term banned (env,t) =
clasohm@0
   552
    let val (Var(v,T), ts) = strip_comb t
clasohm@1460
   553
	val (Ts,U) = strip_type env T
clasohm@1460
   554
	and js = length ts - 1  downto 0
clasohm@1460
   555
	val args = sort arg_less
clasohm@1460
   556
		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
clasohm@1460
   557
	val ts' = map (#t) args
clasohm@0
   558
    in
clasohm@0
   559
    if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
clasohm@0
   560
    else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
clasohm@1460
   561
	     val body = list_comb(v', map (Bound o #j) args)
clasohm@1460
   562
	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
clasohm@1460
   563
	     (*the vupdate affects ts' if they contain v*)
clasohm@1460
   564
	 in  
clasohm@1460
   565
	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
clasohm@0
   566
         end
clasohm@0
   567
    end;
clasohm@0
   568
clasohm@0
   569
clasohm@0
   570
(*Add tpair if not trivial or already there.
clasohm@0
   571
  Should check for swapped pairs??*)
clasohm@0
   572
fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
clasohm@0
   573
  if t0 aconv u0 then tpairs  
clasohm@0
   574
  else
clasohm@0
   575
  let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
clasohm@0
   576
      fun same(t',u') = (t aconv t') andalso (u aconv u')
clasohm@0
   577
  in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
clasohm@0
   578
clasohm@0
   579
clasohm@0
   580
(*Simplify both terms and check for assignments.
clasohm@0
   581
  Bound vars in the binder are "banned" unless used in both t AND u *)
clasohm@0
   582
fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
clasohm@0
   583
  let val loot = loose_bnos t  and  loou = loose_bnos u
clasohm@0
   584
      fun add_index (((a,T), j), (bnos, newbinder)) = 
clasohm@0
   585
            if  j mem loot  andalso  j mem loou 
clasohm@1460
   586
            then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
clasohm@1460
   587
            else  (j::bnos, newbinder);		(*remove*)
clasohm@0
   588
      val indices = 0 upto (length rbinder - 1);
clasohm@0
   589
      val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
clasohm@0
   590
      val (env', t') = clean_term banned (env, t);
clasohm@0
   591
      val (env'',u') = clean_term banned (env',u)
clasohm@0
   592
  in  (ff_assign(env'', rbin', t', u'), tpairs)
clasohm@0
   593
      handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
clasohm@0
   594
      handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
clasohm@0
   595
  end
clasohm@0
   596
  handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
clasohm@0
   597
clasohm@0
   598
clasohm@0
   599
(*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
clasohm@0
   600
  eliminates trivial tpairs like t=t, as well as repeated ones
clasohm@0
   601
  trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
clasohm@0
   602
  Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
clasohm@0
   603
fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
clasohm@0
   604
      : Envir.env * (term*term)list =
clasohm@0
   605
  let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
clasohm@0
   606
  in  case  (head_of t, head_of u) of
clasohm@0
   607
      (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
clasohm@1460
   608
	if v=w then		(*...occur check would falsely return true!*)
clasohm@1460
   609
	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
clasohm@1460
   610
	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
clasohm@1460
   611
	else if xless(v,w) then (*prefer to update the LARGER variable*)
clasohm@1460
   612
	     clean_ffpair ((rbinder, u, t), (env,tpairs))
clasohm@0
   613
        else clean_ffpair ((rbinder, t, u), (env,tpairs))
clasohm@0
   614
    | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
clasohm@0
   615
  end;
clasohm@0
   616
clasohm@0
   617
clasohm@0
   618
(*Print a tracing message + list of dpairs.
clasohm@0
   619
  In t==u print u first because it may be rigid or flexible --
clasohm@0
   620
    t is always flexible.*)
clasohm@0
   621
fun print_dpairs msg (env,dpairs) =
clasohm@0
   622
  let fun pdp (rbinder,t,u) =
clasohm@0
   623
        let fun termT t = Sign.pretty_term (!sgr)
clasohm@0
   624
                              (Envir.norm_term env (rlist_abs(rbinder,t)))
clasohm@0
   625
            val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
clasohm@0
   626
                          termT t];
clasohm@0
   627
        in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
clasohm@0
   628
  in  writeln msg;  seq pdp dpairs  end;
clasohm@0
   629
clasohm@0
   630
clasohm@0
   631
(*Unify the dpairs in the environment.
clasohm@0
   632
  Returns flex-flex disagreement pairs NOT IN normal form. 
clasohm@0
   633
  SIMPL may raise exception CANTUNIFY. *)
clasohm@0
   634
fun hounifiers (sg,env, tus : (term*term)list) 
clasohm@0
   635
  : (Envir.env * (term*term)list)Sequence.seq =
clasohm@0
   636
  let fun add_unify tdepth ((env,dpairs), reseq) =
clasohm@1460
   637
	  Sequence.seqof (fn()=>
clasohm@1460
   638
	  let val (env',flexflex,flexrigid) = 
clasohm@1460
   639
	       (if tdepth> !trace_bound andalso !trace_simp
clasohm@1460
   640
		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
clasohm@1460
   641
		SIMPL (env,dpairs))
clasohm@1460
   642
	  in case flexrigid of
clasohm@1460
   643
	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
clasohm@1460
   644
	    | dp::frigid' => 
clasohm@1460
   645
		if tdepth > !search_bound then
clasohm@1460
   646
		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
clasohm@1460
   647
		else
clasohm@1460
   648
		(if tdepth > !trace_bound then
clasohm@1460
   649
		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
clasohm@1460
   650
		 else ();
clasohm@1460
   651
		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
clasohm@1460
   652
			   (MATCH (env',dp, frigid'@flexflex), reseq)))
clasohm@1460
   653
	  end
clasohm@1460
   654
	  handle CANTUNIFY => 
clasohm@1460
   655
	    (if tdepth > !trace_bound then writeln"Failure node" else ();
clasohm@1460
   656
	     Sequence.pull reseq));
clasohm@0
   657
     val dps = map (fn(t,u)=> ([],t,u)) tus
clasohm@0
   658
  in sgr := sg;
clasohm@0
   659
     add_unify 1 ((env,dps), Sequence.null) 
clasohm@0
   660
  end;
clasohm@0
   661
clasohm@0
   662
fun unifiers(params) =
clasohm@0
   663
      Sequence.cons((Pattern.unify(params), []),   Sequence.null)
clasohm@0
   664
      handle Pattern.Unif => Sequence.null
clasohm@0
   665
           | Pattern.Pattern => hounifiers(params);
clasohm@0
   666
clasohm@0
   667
clasohm@0
   668
(*For smash_flexflex1*)
clasohm@0
   669
fun var_head_of (env,t) : indexname * typ =
clasohm@0
   670
  case head_of (strip_abs_body (Envir.norm_term env t)) of
clasohm@0
   671
      Var(v,T) => (v,T)
clasohm@0
   672
    | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
clasohm@0
   673
clasohm@0
   674
clasohm@0
   675
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
clasohm@0
   676
  Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
clasohm@0
   677
  Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
clasohm@1460
   678
	though just ?g->?f is a more general unifier.
clasohm@0
   679
  Unlike Huet (1975), does not smash together all variables of same type --
clasohm@0
   680
    requires more work yet gives a less general unifier (fewer variables).
clasohm@0
   681
  Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
clasohm@0
   682
fun smash_flexflex1 ((t,u), env) : Envir.env =
clasohm@0
   683
  let val (v,T) = var_head_of (env,t)
clasohm@0
   684
      and (w,U) = var_head_of (env,u);
clasohm@0
   685
      val (env', var) = Envir.genvar (#1v) (env, body_type env T)
clasohm@0
   686
      val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
clasohm@0
   687
  in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
clasohm@0
   688
      else Envir.vupdate((v, type_abs(env',T,var)), env'')
clasohm@0
   689
  end;
clasohm@0
   690
clasohm@0
   691
clasohm@0
   692
(*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
clasohm@0
   693
fun smash_flexflex (env,tpairs) : Envir.env =
clasohm@0
   694
  foldr smash_flexflex1 (tpairs, env);
clasohm@0
   695
clasohm@0
   696
(*Returns unifiers with no remaining disagreement pairs*)
clasohm@0
   697
fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
clasohm@0
   698
    Sequence.maps smash_flexflex (unifiers(sg,env,tus));
clasohm@0
   699
clasohm@0
   700
end;