substitutions.sml 22.6 KB
Newer Older
Axel Simon's avatar
Axel Simon committed
1
2
3
4
5
6
7
8
9
10
11
12
structure Substitutions : sig

   exception UnificationFailure of string

   exception SubstitutionBug

   val insertField : Types.rfield * Types.rfield list -> Types.rfield list
   
   type Substs

   val emptySubsts : Substs

Axel Simon's avatar
Axel Simon committed
13
14
15
16
   val substsFilter : Substs * TVar.set -> Substs
   
   val isEmpty : Substs -> bool

Axel Simon's avatar
Axel Simon committed
17
18
19
20
   val showSubstsSI : Substs * TVar.varmap -> string * TVar.varmap
   
   type expand_info
   
Axel Simon's avatar
Axel Simon committed
21
22
   val showExpandInfoSI : expand_info * TVar.varmap ->
                          string * TVar.varmap
23
   val emptyExpandInfo : expand_info
24

25
   val applyExpandInfo : expand_info -> BooleanDomain.bfun -> BooleanDomain.bfun
Axel Simon's avatar
Axel Simon committed
26

27
28
   val expandInfoGetBVars : expand_info * BooleanDomain.bvarset ->
                                    BooleanDomain.bvarset
29
   
Axel Simon's avatar
Axel Simon committed
30
31
32
   val applySizeConstraints : SizeConstraint.size_constraint_set * Substs ->
                              SizeConstraint.size_constraint_set * Substs

Axel Simon's avatar
Axel Simon committed
33
34
35
   val applySubstsToExp : Substs -> Types.texp * expand_info ->
                          Types.texp * expand_info

Axel Simon's avatar
Axel Simon committed
36
37
38
39
   (*create a fresh type by instantiating the variables in the given type,
   plus those in the third set (meant to expand the decode width variables)
   but without those variable in the first set*)
   val instantiateType : TVar.set * Types.texp * TVar.set *
Axel Simon's avatar
Axel Simon committed
40
41
      BooleanDomain.bfun * SizeConstraint.size_constraint_set ->
      Types.texp * BooleanDomain.bfun * SizeConstraint.size_constraint_set
Axel Simon's avatar
Axel Simon committed
42

Axel Simon's avatar
Axel Simon committed
43
   val mgu : Types.texp * Types.texp * Substs -> Substs
Axel Simon's avatar
Axel Simon committed
44
45
46
47

end = struct

   open Types
Axel Simon's avatar
Axel Simon committed
48
49
   structure SC = SizeConstraint

Axel Simon's avatar
Axel Simon committed
50
51
52
53
54
55
   exception UnificationFailure of string

   exception SubstitutionBug
   
   datatype SubstTarget
      = WITH_TYPE of texp
56
      | WITH_FIELD of (rfield list * tvar * BD.bvar)
Axel Simon's avatar
Axel Simon committed
57
58
59
60
61
62
63
   
   type Subst = tvar * SubstTarget
   
   fun mkSubst arg = arg

   datatype Substs = Substs of Subst list

Axel Simon's avatar
Axel Simon committed
64
65
66
67
   fun substsFilter (Substs ss, set) =
     Substs (List.filter (fn (v,_) => TVar.member (set,v)) ss)

   fun isEmpty (Substs ss) = List.null ss
Axel Simon's avatar
Axel Simon committed
68
69
70
71
72
73
74
75
76
77

   val a = freshTVar ()
   val b = freshTVar ()
   val c = freshTVar ()
   val d = freshTVar ()
   val e = freshTVar ()

   fun genTypes () = let
      val (t, f1) = SymbolTable.create(!SymbolTables.fieldTable, Atom.atom "f1", SymbolTable.noSpan)
      val (t, f2) = SymbolTable.create(t,  Atom.atom "f2", SymbolTable.noSpan)
78
      val t1 = FUN([VAR (a,BD.freshBVar ())], RECORD (b, BD.freshBVar (), [RField { name=f1, fty = VEC (VAR (e,BD.freshBVar ())), exists = BD.freshBVar ()},
Axel Simon's avatar
Axel Simon committed
79
      RField { name=f2, fty = VEC (VAR (e,BD.freshBVar ())), exists = BD.freshBVar ()}]))
80
      val t2 = FUN([RECORD (c, BD.freshBVar (), [RField { name=f1, fty = VEC (VAR (d,BD.freshBVar ())), exists = BD.freshBVar ()}])], VAR (a,BD.freshBVar ()))
Axel Simon's avatar
Axel Simon committed
81
82
   in (SymbolTables.fieldTable := t; (f1,f2,t1,t2)) end
      
83
   fun showSubstTargetSI (WITH_TYPE t, si) = showTypeSI (t, si)
84
     | showSubstTargetSI (WITH_FIELD (fs,vNew,bNew), si) =
Axel Simon's avatar
Axel Simon committed
85
86
         let
            val (vNewStr, si) = TVar.varToString (vNew, si)
87
            val bNewStr = BD.showVar bNew
Axel Simon's avatar
Axel Simon committed
88
89
            fun genfStr (RField {name = n, fty = t, exists = b}, (str, si)) =
               let
90
91
                  val (tStr, si) = showTypeSI (t, si)
                  val fStr = BD.showVar b
Axel Simon's avatar
Axel Simon committed
92
93
                  val name = SymbolTable.getString(!SymbolTables.fieldTable, n)
               in
94
                  (str ^ name ^ fStr ^ ": " ^ tStr ^ ", ", si)
Axel Simon's avatar
Axel Simon committed
95
96
97
               end
            val (fsStr, si) = List.foldl genfStr ("", si) fs
         in
98
            (fsStr ^ vNewStr ^ bNewStr ^ ": ...", si)
Axel Simon's avatar
Axel Simon committed
99
100
         end

101
102
103
104
105
106
107
108
   fun showSubstSI ((v,st), si) =
      let
         val (vStr, si) = TVar.varToString (v, si)
         val (stStr, si) = showSubstTargetSI (st, si)
      in
         (vStr ^ "/" ^ stStr, si)
      end
   
Axel Simon's avatar
Axel Simon committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
   fun showSubst subst =
      let val (str, _) = showSubstSI (subst, TVar.emptyShowInfo) in str end
   
   fun showSubstsSI (Substs l, si) =
      let
         fun pr (s, (res, sep, si)) =
            let
               val (str, si) = showSubstSI (s, si)
            in
               (res ^ sep ^ str, ", ", si)
            end
         val (res, _, si) = List.foldl pr ("[", "", si) l
      in
         (res ^ "]", si)
      end

   val emptySubsts = Substs []

127
128
129
130
131
132
   structure TVMap = RedBlackMapFn (
      struct
         type ord_key = TVar.tvar
         val compare = TVar.compare
      end)

133
134
   type expand_detail = { substVars : SubstTarget,
                          instInfo : (BD.bvar * SubstTarget) list }   
135
136
137

   type expand_info = expand_detail TVMap.map

Axel Simon's avatar
Axel Simon committed
138
139
140
141
142
143
144
145
146
147
   fun showExpandInfoSI (ei, si) =
      let
         val siRef = ref si
         fun showVar tv =
            let
               val (vStr, si) = TVar.varToString (tv, !siRef)
               val _ = siRef := si
            in
               vStr
            end
148
149
150
151
152
153
154
155
156
157
158
159
         fun showSubstTarget st =
            let
               val (stStr, si) = showSubstTargetSI (st, !siRef)
               val _ = siRef := si
            in
               stStr
            end
         fun showAll (tv,{substVars = st, instInfo = stList }) =
             showVar tv ^ "\t" ^ showSubstTarget st ^
            List.foldl (fn ((bv,st),str) => str ^ "\n" ^ 
                        BD.showVar bv ^ ":\t" ^ showSubstTarget st)
               "" stList
Axel Simon's avatar
Axel Simon committed
160
161
162
163
164
      in
         (List.foldl (fn (e,str) => str ^ showAll e ^ "\n") "" (TVMap.listItemsi ei)
         , !siRef)
      end

165
166
   val emptyExpandInfo = TVMap.empty : expand_info

167
   fun getTargetVars (WITH_TYPE t) = texpBVarset (op ::) (t,[])
168
     | getTargetVars (WITH_FIELD (fs,var,bvar)) =
169
170
171
      List.foldl
         (fn (RField {name = n, fty = t, exists = b},bs) =>
            texpBVarset (op ::) (t,(false,b)::bs))
172
         [(false,bvar)] fs
173

174
175
176
177
   fun addToExpandInfo (tvar, bvar, target, ei) =
      let
         val detail = case TVMap.find (ei, tvar) of
              SOME detail => detail
178
            | NONE => {substVars = target,
179
                       instInfo = []}
180
         
181
         fun genTargetInstance (WITH_TYPE t) = WITH_TYPE (setFlagsToTop t)
182
183
           | genTargetInstance (WITH_FIELD (fs,var,bvar)) =
               WITH_FIELD (List.map setFlagsToTopF fs, var, BD.freshBVar ())
184
185
186
187
188
189
190
191
         val newTargetRef = ref target
         fun updateII ((v,tgt) :: vts) =
            if BD.eq(v,bvar) then (newTargetRef := tgt; (v,tgt) :: vts) else
            (v,tgt) :: updateII vts
           | updateII [] = (newTargetRef := genTargetInstance target
                           ; [(bvar, !newTargetRef)])
         val { substVars = sVs, instInfo = ii } = detail
         val newDetail = { substVars = sVs, instInfo = updateII ii }
192
      in
193
         (!newTargetRef, TVMap.insert (ei, tvar, newDetail))
194
195
196
197
198
199
      end

   fun applyExpandInfo ei bFun =
      let
         fun aEI ({substVars = sVs, instInfo = infos}, bFun) =
            let
Axel Simon's avatar
Axel Simon committed
200
               (*val bFun = List.foldl
201
                     (fn ((_,inst), bFun) =>
202
                        BD.expand (List.map #2 (getTargetVars sVs), List.map (fn (_,v) => (false,v))
203
                                        inst, bFun)
Axel Simon's avatar
Axel Simon committed
204
                     ) bFun infos*)
205
206
207
208
209
210
211
212
213
214
               fun shave (info as ((_ :: _) :: _)) =
                     SOME (List.map List.hd info, List.map List.tl info)
                 | shave ([] :: _) = NONE
                 | shave _ = raise SubstitutionBug
               val (tvarInfo, insts) = ListPair.unzip infos
               fun expandTVar (insts,bFun) = case shave insts of
                    NONE => bFun
                  | SOME (inst, insts) =>
                     expandTVar (insts, BD.expand (tvarInfo, inst, bFun))
            in
215
               expandTVar (List.map getTargetVars insts, bFun)
216
217
218
219
            end
      in
         List.foldl aEI bFun (TVMap.listItems ei)
      end
Axel Simon's avatar
Axel Simon committed
220

221
   fun expandInfoGetBVars (ei, set) =
222
223
      let
         val texpBVarset = texpBVarset (fn ((_,v),vs) => BD.addToSet (v,vs))
224
225
         fun getBVars (WITH_TYPE t, set) = texpBVarset (t, set)
           | getBVars (WITH_FIELD (fs,_,bvar), set) =
226
227
228
               List.foldl (fn (RField {name, fty = t, exists = b}, set) =>
                  texpBVarset (t, BD.addToSet (b,set))) 
                  (BD.addToSet (bvar, set)) fs
229
230
231
232
         fun getBVarsInfo ({substVars = sVs, instInfo = infos}, set) =
            List.foldl
               (fn ((bVar,st),set) => getBVars (st, BD.addToSet (bVar,set)))
               set infos
233
      in
234
         List.foldl getBVarsInfo set (TVMap.listItems ei)
235
236
      end

Axel Simon's avatar
Axel Simon committed
237
238
239
240
   fun insertField (f, []) = [f]
     | insertField (f1, f2 :: l) = (case compare_rfield (f1,f2) of
          LESS => f1 :: f2 :: l
        | GREATER => f2 :: insertField (f1, l)
241
242
243
        | EQUAL => (*(TextIO.print ("inserting same field " ^ SymbolTable.getString(!SymbolTables.fieldTable, case f1 of RField {name=n,fty,exists} => n) ^
                    " into " ^ showType (RECORD (TVar.freshTVar (),BooleanDomain.freshBVar (), f2 :: l)));*)
            raise SubstitutionBug)
Axel Simon's avatar
Axel Simon committed
244

Axel Simon's avatar
Axel Simon committed
245
246
247
248
   structure SISet = RedBlackSetFn (
      struct
         type ord_key = SymbolTable.symid
         val compare = SymbolTable.compare_symid
Julian Kranz's avatar
Julian Kranz committed
249
      end)
Axel Simon's avatar
Axel Simon committed
250

Axel Simon's avatar
Axel Simon committed
251
252
   fun applySubstToExp (subst as (v, target)) (exp, ei) = let
      val eiRef = ref (ei : expand_info)
253
      fun aS (FUN (f1, f2)) = FUN (List.map aS f1, aS f2)
Axel Simon's avatar
Axel Simon committed
254
255
256
257
258
259
260
261
        | aS (SYN (syn, t)) = SYN (syn, aS t)
        | aS (ZENO) = ZENO
        | aS (FLOAT) = FLOAT
        | aS (UNIT) = UNIT
        | aS (VEC t) = VEC (aS t)
        | aS (CONST c) = CONST c
        | aS (ALG (ty, l)) = ALG (ty, List.map aS l)
        | aS (RECORD (var, b, fs)) =
Axel Simon's avatar
Axel Simon committed
262
263
264
         let
            val (fs, ei) = applySubstToRFields subst (fs, !eiRef)
         in
Axel Simon's avatar
Axel Simon committed
265
            if TVar.eq (var, v) then
Axel Simon's avatar
Axel Simon committed
266
              case addToExpandInfo (var, b, target, ei) of
267
                 (target,ei) => (eiRef := ei; case target of
268
269
                      WITH_FIELD (newFs, newVar, newBVar) =>
                       RECORD (newVar, newBVar, List.foldl insertField fs newFs)
270
271
                    | WITH_TYPE _ => raise SubstitutionBug
                 )
Axel Simon's avatar
Axel Simon committed
272
            else 
Axel Simon's avatar
Axel Simon committed
273
               (eiRef := ei; RECORD (var, b, fs))
Axel Simon's avatar
Axel Simon committed
274
         end
275
        | aS (MONAD (r,f,t)) = MONAD (aS r,aS f,aS t)
Axel Simon's avatar
Axel Simon committed
276
        | aS (VAR (var,b)) = if TVar.eq (var, v) then
277
278
279
              case addToExpandInfo (var, b, target, !eiRef) of
                   (WITH_TYPE t,ei) => (eiRef := ei; t)
                 | (WITH_FIELD _,ei) => raise SubstitutionBug
Axel Simon's avatar
Axel Simon committed
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
           else VAR (var,b)
      in
         (aS exp, !eiRef)
      end
   and applySubstToRField subst
      (RField {name = n, fty = t, exists = b}, ei) =
      let
         val (t,ei) = applySubstToExp subst (t,ei)
      in
         (RField {name = n, fty = t, exists = b}, ei)
      end

   and applySubstsToExp (Substs ss) (exp, ei) =
        List.foldl (fn (s,exp_ei) => applySubstToExp s exp_ei) (exp,ei) ss 

   and applySubstsToRField (Substs ss) (f, ei) =
        List.foldl (fn (s,f_ei) => applySubstToRField s f_ei) (f, ei) ss  

   and applySubstToRFields s (fs, ei) =
      let
         fun app ([], ei) = ([], ei)
           | app (f::fs, ei) =
            let
               val (f, ei) = applySubstToRField s (f,ei)
               val (fs, ei) = app (fs, ei)
            in
               (f::fs, ei)
            end
      in
         app (fs, ei)
      end

Axel Simon's avatar
Axel Simon committed
312
313
314
315
   (*any substitution that is being added must not mention any variable that
   already exists in the domain of the current set of substitutions; if this
   holds, the resulting substitutions remain fully applied*)
   fun addSubst subst (Substs l, ei) =
Axel Simon's avatar
Axel Simon committed
316
      let
Axel Simon's avatar
Axel Simon committed
317
318
         val eiRef = ref ei
         fun doSubst (v2, WITH_TYPE t2) =
Axel Simon's avatar
Axel Simon committed
319
            let
Axel Simon's avatar
Axel Simon committed
320
321
               val (t2, ei) = applySubstToExp subst (t2, !eiRef)
               val _ = eiRef := ei
Axel Simon's avatar
Axel Simon committed
322
            in
Axel Simon's avatar
Axel Simon committed
323
               occursCheck (v2, WITH_TYPE t2)
Axel Simon's avatar
Axel Simon committed
324
            end
325
           | doSubst (v2, WITH_FIELD (fs, v3, bv3)) =
Axel Simon's avatar
Axel Simon committed
326
            let
327
               val t2 = RECORD (v3,bv3,fs)
Axel Simon's avatar
Axel Simon committed
328
329
               val (t2,ei) = applySubstToExp subst (t2,!eiRef)
               val _ = eiRef := ei
330
               val RECORD (v3,bv3,fs) = t2
Axel Simon's avatar
Axel Simon committed
331
            in
Axel Simon's avatar
Axel Simon committed
332
               occursCheck (v2, WITH_FIELD (fs, v3, bv3))
Axel Simon's avatar
Axel Simon committed
333
            end
Axel Simon's avatar
Axel Simon committed
334
         
Axel Simon's avatar
Axel Simon committed
335
336
337
338
         and occursCheck (v2, WITH_TYPE (t2 as (VAR _))) = (v2, WITH_TYPE t2)
            (* the previous case ensures that we don't get annoying error
            messages like a/a is an infinite substitution *)
           | occursCheck (v2, WITH_TYPE t2) =
Axel Simon's avatar
Axel Simon committed
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
            if TVar.member(texpVarset (t2, TVar.empty),v2) then
               let
                  val (vStr,si) = TVar.varToString (v2,TVar.emptyShowInfo)
                  val (tStr,si) = showTypeSI (t2,si)
               in
                  raise UnificationFailure ("infinite type " ^ vStr ^ " = " ^ tStr)
               end
            else (v2, WITH_TYPE t2)
           | occursCheck (v2, WITH_FIELD (fs, v3, bv3)) =
            if TVar.member(texpVarset (RECORD (v3,bv3,fs), TVar.empty),v2) then
               let
                  val (vStr,si) = TVar.varToString (v2,TVar.emptyShowInfo)
                  val (tStr,si) = showTypeSI (RECORD (v3,bv3,fs),si)
               in
                  raise UnificationFailure ("infinite record " ^ vStr ^ " = " ^ tStr)
               end
            else (v2, WITH_FIELD (fs, v3, bv3))

Axel Simon's avatar
Axel Simon committed
357
358
359
360
361
362
         (*val (v,repl) = subst
         val (vStr,si) = TVar.varToString (v,TVar.emptyShowInfo)
         val (tStr,si) = case repl of
              WITH_TYPE t2 => showTypeSI (t2,si)
            | WITH_FIELD (fs, v3) => showTypeSI (
                        RECORD (v3,BooleanDomain.freshBVar (),fs),si)
Axel Simon's avatar
Axel Simon committed
363
         val (sStr,si) = showSubstsSI (Substs l, si)
Axel Simon's avatar
Axel Simon committed
364
         val (rStr,_ ) = showSubstsSI (Substs (subst::List.map doSubst l),si)
Axel Simon's avatar
Axel Simon committed
365
366
367
         val _ = TextIO.print ("adding " ^ vStr ^ "/" ^ tStr ^ " to " ^ sStr ^
                  " yielding " ^ rStr ^ "\n")*)
      in
Axel Simon's avatar
Axel Simon committed
368
         (Substs (occursCheck subst::List.map doSubst l), !eiRef)
Axel Simon's avatar
Axel Simon committed
369
370
371
372
373
374
375
376
377
378
379
      end

   fun findSubstForVar (v, Substs l) =
      let
         fun lookup [] = NONE
           | lookup ((v',r) :: l) =
               if TVar.eq (v,v') then SOME r else lookup l
      in
         lookup l
      end

Axel Simon's avatar
Axel Simon committed
380
381
   fun applySizeConstraints (sCons, substs) =
      let
Axel Simon's avatar
Axel Simon committed
382
         val vs = SC.getVarset sCons
Axel Simon's avatar
Axel Simon committed
383
         val (Substs ss) = substsFilter (substs, vs)
384

Axel Simon's avatar
Axel Simon committed
385
386
387
         fun updateSubsts ((v,WITH_TYPE (CONST c)), (sCons, substs)) =
            (case SC.add (SC.equality (v,[],c), sCons) of
                SC.RESULT (is,sCons) =>
388
389
                  (sCons,
                   List.foldl (fn ((v,c), substs) =>
Axel Simon's avatar
Axel Simon committed
390
391
                     #1 (addSubst (v,WITH_TYPE (CONST c)) (substs, emptyExpandInfo))
                     ) substs is)
Axel Simon's avatar
Axel Simon committed
392
393
394
395
396
397
398
399
400
401
               | SC.UNSATISFIABLE => raise UnificationFailure
                  "size constraints over vectors are unsatisfiable"
               | SC.FRACTIONAL => raise UnificationFailure
                  "solution to size constraint is not integral"
               | SC.NEGATIVE => raise UnificationFailure
                  "constraint implies that vector has non-positive size"
            )
           | updateSubsts ((v1,WITH_TYPE (VAR (v2,_))), (sCons, substs)) =
               (SC.rename (v1,v2,sCons), substs)
           | updateSubsts _ = raise SubstitutionBug
402

Axel Simon's avatar
Axel Simon committed
403
      in
Axel Simon's avatar
Axel Simon committed
404
         List.foldl updateSubsts (sCons, substs) ss
Axel Simon's avatar
Axel Simon committed
405
406
      end

Axel Simon's avatar
Axel Simon committed
407
   fun instantiateType (vs,t,extraTVars,bFun,sCons) =
Axel Simon's avatar
Axel Simon committed
408
      let
Axel Simon's avatar
Axel Simon committed
409
         val toReplace = TVar.difference (texpVarset (t, extraTVars), vs)
410
411
412
413
414
415
         val repl = List.map (fn v => (v, TVar.freshTVar ()))
                        (TVar.listItems toReplace)
         val affectedSCons = SC.filter (toReplace, sCons)
         val newSCons = List.foldl
               (fn ((v1,v2),sCons) => SC.rename (v1,v2,sCons))
               affectedSCons repl
Axel Simon's avatar
Axel Simon committed
416
         val mergedSCons = SC.merge (newSCons, sCons)
417
         val tNew = replaceTVars (t, repl)
418
419
420
421
         val tNew = setFlagsToTop tNew
         val bvs1 = texpBVarset (fn ((_,v),vs) => v :: vs) (t, [])
         val bvs2 = texpBVarset (fn ((_,v),vs) => (false,v) :: vs) (tNew, [])
         val bFunNew = BD.expand (bvs1,bvs2,bFun)
Axel Simon's avatar
Axel Simon committed
422

Axel Simon's avatar
Axel Simon committed
423
         (*val (tStr, si) = showTypeSI (t, TVar.emptyShowInfo)
Axel Simon's avatar
Axel Simon committed
424
         val (tNewStr, si) = showTypeSI (tNew, si)
Axel Simon's avatar
Axel Simon committed
425
426
427
         val (sStr, si) = TVar.setToString (vs, si)
         val (vStr, si) = TVar.setToString (texpVarset (t, TVar.empty), si)
         val (suStr, si) = showSubstsSI (substs, si)
Axel Simon's avatar
Axel Simon committed
428
         val (scStr1,si) = SC.toStringSI (sCons, NONE, si)
Axel Simon's avatar
Axel Simon committed
429
         val (scStr2,si) = SC.toStringSI (mergedSCons, NONE, si)
Axel Simon's avatar
Axel Simon committed
430
         val _ = TextIO.print ("instantiating " ^ tStr ^ " using " ^ suStr ^ " to " ^ tNewStr ^ (*", extending " ^ scStr1 ^ " to " ^ scStr2 ^*) ", old bFun: " ^ BD.showBFun bFun ^ ", new bFun: " ^ BD.showBFun bFunNew ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
431
      in
Axel Simon's avatar
Axel Simon committed
432
         (tNew, bFunNew, mergedSCons)
Axel Simon's avatar
Axel Simon committed
433
434
      end

435
436
437
438
439
440
441
   fun mgu (FUN (f1, f2), FUN (g1, g2), s) = if List.length f1<>List.length g1
      then raise UnificationFailure (
            "function with different number of arguments (" ^
            Int.toString (List.length f1) ^ " and " ^
            Int.toString (List.length g1) ^ ")"
         )
      else mgu (f2, g2, ListPair.foldlEq mgu s (f1,g1))
Axel Simon's avatar
Axel Simon committed
442
443
444
445
446
447
448
449
450
451
452
     | mgu (SYN (_, t1), t2, s) = mgu (t1, t2, s)
     | mgu (t1, SYN (_, t2), s) = mgu (t1, t2, s)
     | mgu (ZENO, ZENO, s) = s
     | mgu (FLOAT, FLOAT, s) = s
     | mgu (UNIT, UNIT, s) = s
     | mgu (VEC t1, VEC t2, s) = mgu (t1, t2, s)
     | mgu (CONST c1, CONST c2, s) =
        if c1=c2 then s else raise UnificationFailure (
         "incompatible bit vectors sizes (" ^ Int.toString c1 ^ " and " ^
         Int.toString c2 ^ ")")
     | mgu (RECORD (v1,b1,l1), RECORD (v2,b2,l2), s) =
Axel Simon's avatar
Axel Simon committed
453
      let
Axel Simon's avatar
Axel Simon committed
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
         fun applySubsts (v, b, fs) = (case findSubstForVar (v, s) of
              NONE => (v,b,fs)
            | SOME (WITH_FIELD (fs',v',b')) => (v', b', List.foldl insertField fs fs')
            | _ => raise SubstitutionBug
         )
         val (v1,b1,l1) = applySubsts (v1,b1,l1)
         val (v2,b2,l2) = applySubsts (v2,b2,l2)

         fun unify (v1, v2, [], [], s) = if TVar.eq (v1,v2) then s else
            #1 (addSubst (v2, WITH_FIELD ([], v1, b1)) (s,emptyExpandInfo))
           | unify (v1, v2, (f1 as RField e1) :: fs1,
                    (f2 as RField e2) :: fs2, s) =
            (case compare_rfield (f1,f2) of
               EQUAL =>
               let
                  val s = mgu (#fty e1, #fty e2, s)
                in
                  unify (v1, v2, fs1, fs2, s)
               end
             | LESS =>
               let
                  val newVar = freshTVar ()
                  val newBVar = BD.freshBVar ()
                  val (f1,ei) = applySubstsToRField s (f1,emptyExpandInfo)
                  val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
               in
                  unify (v1, newVar, fs1, f2 :: fs2, s)
               end
             | GREATER =>
               let
                  val newVar = freshTVar ()
                  val newBVar = BD.freshBVar ()
                  val (f2,ei) = applySubstsToRField s (f2,emptyExpandInfo)
                  val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
               in
                  unify (newVar, v2, f1 :: fs1, fs2, s)
               end
            )
           | unify (v1, v2, f1 :: fs1, [], s) =
Axel Simon's avatar
Axel Simon committed
493
            let
Axel Simon's avatar
Axel Simon committed
494
495
496
497
               val newVar = freshTVar ()
               val newBVar = BD.freshBVar ()
               val (f1,ei) = applySubstsToRField s (f1,emptyExpandInfo)
               val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
Axel Simon's avatar
Axel Simon committed
498
            in
Axel Simon's avatar
Axel Simon committed
499
               unify (v1, newVar, fs1, [], s)
Axel Simon's avatar
Axel Simon committed
500
            end
Axel Simon's avatar
Axel Simon committed
501
           | unify (v1, v2, [], f2 :: fs2, s) =
Axel Simon's avatar
Axel Simon committed
502
            let
Axel Simon's avatar
Axel Simon committed
503
504
505
506
               val newVar = freshTVar ()
               val newBVar = BD.freshBVar ()
               val (f2,ei) = applySubstsToRField s (f2,emptyExpandInfo)
               val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
Axel Simon's avatar
Axel Simon committed
507
            in
Axel Simon's avatar
Axel Simon committed
508
               unify (newVar, v2, [], fs2, s)
Axel Simon's avatar
Axel Simon committed
509
            end
Axel Simon's avatar
Axel Simon committed
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
      in
         unify (v1,v2,l1,l2,s)
      end
     | mgu (MONAD (r1,f1,t1), MONAD (r2,f2,t2), s) =
         mgu (r1, r2, mgu (f1, f2, mgu (t1, t2, s)))
     | mgu (ALG (ty1, l1), ALG (ty2, l2), s) =
      let fun incompat () = raise UnificationFailure (
            "cannot match constructor " ^
            SymbolTable.getString(!SymbolTables.typeTable, ty1) ^
            " with " ^
            SymbolTable.getString(!SymbolTables.typeTable, ty2))
      in case SymbolTable.compare_symid (ty1, ty2) of
        LESS => incompat ()
      | GREATER => incompat ()
      | EQAL => List.foldl (fn ((e1,e2),s) => mgu (e1,e2,s)) s
                  (ListPair.zipEq (l1,l2))
      end
      (*mgu is right-biased in that mgu(a,b) always creates b/a which means
      that the resulting substitution never modifies the lhs if that is
      avoidable*)
     | mgu (e, VAR (v,b), s) =
      let
         fun unifyVars (v,b,e,s) =
               case findSubstForVar (v,s) of
                    NONE => 
535
                     let
Axel Simon's avatar
Axel Simon committed
536
537
                       val (e, ei) = applySubstsToExp s (e, emptyExpandInfo)
                       val (s, ei) = addSubst (v,WITH_TYPE e) (s,ei)
538
                     in
Axel Simon's avatar
Axel Simon committed
539
                        s
540
                     end
Axel Simon's avatar
Axel Simon committed
541
542
543
                  | SOME (WITH_TYPE t) => mgu (e, t, s)
                  | _ => raise SubstitutionBug
      in
Axel Simon's avatar
Axel Simon committed
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
        case e of
           VAR (v',b') => if TVar.eq (v',v) then s else unifyVars (v,b,e,s)
         | _ => unifyVars (v,b,e,s)
      end
     | mgu (VAR (v,b), e, s) =
         (case findSubstForVar (v,s) of
              NONE =>
               let
                 val (e, ei) = applySubstsToExp s (e, emptyExpandInfo)
                 val (s,ei) = addSubst (v,WITH_TYPE e) (s,ei)
               in
                  s
               end
            | SOME (WITH_TYPE t) => mgu (e, t, s)
            | _ => raise SubstitutionBug
         )
      | mgu (t1,t2,s) =
      let fun descr (FUN _) = "a function type"
            | descr (ZENO) = "int"
            | descr (FLOAT) = "float"
            | descr (UNIT) = "()"
            | descr (VEC (CONST c)) = "a vector of " ^ 
                                      Int.toString c ^ " bits"
            | descr (VEC _) = "a bit vector"
            | descr (ALG (ty, _)) = "type " ^
               SymbolTable.getString(!SymbolTables.typeTable, ty)
            | descr (RECORD (_,_,fs)) = "a record {" ^
571
572
573
               List.foldl (fn (RField {name = n, ...},str) =>
                  SymbolTable.getString(!SymbolTables.fieldTable, n) ^
                  ", " ^ str) "..." fs ^ "}"
Axel Simon's avatar
Axel Simon committed
574
575
576
577
578
            | descr (MONAD _) = "an action"
            | descr _ = "something that shouldn't be here"
      in
         raise UnificationFailure ("cannot match " ^ descr t1 ^
                                   " against " ^ descr t2)
Axel Simon's avatar
Axel Simon committed
579
      end
Axel Simon's avatar
Axel Simon committed
580

Axel Simon's avatar
Axel Simon committed
581
582
583
584
585

    fun dbgMgu (t1, t2) =
      let
         val (t1Str, si) = showTypeSI (t1, TVar.emptyShowInfo)
         val (t2Str, si) = showTypeSI (t2, si)
Axel Simon's avatar
Axel Simon committed
586
         val substs = mgu (t1,t2,emptySubsts)
Axel Simon's avatar
Axel Simon committed
587
588
589
590
         val (sStr, si) = showSubstsSI (substs, si)
      in
         ("unifying t1=" ^ t1Str ^ "\nwith     t2=" ^ t2Str ^ "\n" ^ sStr)
      end
Axel Simon's avatar
Axel Simon committed
591

Julian Kranz's avatar
Julian Kranz committed
592
end