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