Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
ViewVC logotype

Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 421, Sat Sep 4 00:01:22 1999 UTC revision 422, Sun Sep 5 22:49:38 1999 UTC
# Line 1057  Line 1057 
1057   * supports making and checking these inductive assumptions.   * supports making and checking these inductive assumptions.
1058   * Furthermore, we need to avoid unrolling any FIX more than once.   * Furthermore, we need to avoid unrolling any FIX more than once.
1059   *)   *)
1060  structure TcDict = BinaryDict  structure TcDict = BinaryMapFn
1061                         (struct                         (struct
1062                             type ord_key = tyc                             type ord_key = tyc
1063                             val cmpKey = tc_cmp                             val compare = tc_cmp
1064                         end)                         end)
1065  (* for each tyc in this dictionary, we store a dictionary containing  (* for each tyc in this dictionary, we store a dictionary containing
1066   * tycs that are assumed equivalent to it.   * tycs that are assumed equivalent to it.
1067   *)   *)
1068  type eqclass = unit TcDict.dict  type eqclass = unit TcDict.map
1069  type hyp = eqclass TcDict.dict  type hyp = eqclass TcDict.map
1070    
1071  (* the null hypothesis, no assumptions about equality *)  (* the null hypothesis, no assumptions about equality *)
1072  val empty_eqclass : eqclass = TcDict.mkDict()  val empty_eqclass : eqclass = TcDict.empty
1073  val null_hyp : hyp = TcDict.mkDict()  val null_hyp : hyp = TcDict.empty
1074    
1075  (* add assumption t1=t2 to current hypothesis.  returns composite  (* add assumption t1=t2 to current hypothesis.  returns composite
1076   * hypothesis.   * hypothesis.
# Line 1091  Line 1091 
1091  val eq_by_hyp : eqclass option * tyc -> bool  val eq_by_hyp : eqclass option * tyc -> bool
1092      = fn (NONE, t2) => false      = fn (NONE, t2) => false
1093         | (SOME eqclass, t2) =>         | (SOME eqclass, t2) =>
1094           isSome (TcDict.peek (eqclass, t2))           isSome (TcDict.find (eqclass, t2))
1095    
1096  (* have we made any assumptions about `t' already? *)  (* have we made any assumptions about `t' already? *)
1097  val visited : eqclass option -> bool  val visited : eqclass option -> bool
# Line 1103  Line 1103 
1103      of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>      of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>
1104          if not (!Control.FLINT.checkDatatypes) then true          if not (!Control.FLINT.checkDatatypes) then true
1105          else let          else let
1106              val t1eqOpt = TcDict.peek (hyp, t1)              val t1eqOpt = TcDict.find (hyp, t1)
1107          in          in
1108              (* first check the induction hypothesis.  we only ever              (* first check the induction hypothesis.  we only ever
1109               * make hypotheses about FIX nodes, so this test is okay               * make hypotheses about FIX nodes, so this test is okay
# Line 1125  Line 1125 
1125                   *)                   *)
1126                  if visited t1eqOpt then false                  if visited t1eqOpt then false
1127                  else let                  else let
1128                      val t2eqOpt = TcDict.peek (hyp, t2)                      val t2eqOpt = TcDict.find (hyp, t2)
1129                  in                  in
1130                      if visited t2eqOpt then false                      if visited t2eqOpt then false
1131                      else eqop1 (assume_eq (hyp, t1, t1eqOpt,                      else eqop1 (assume_eq (hyp, t1, t1eqOpt,

Legend:
Removed from v.421  
changed lines
  Added in v.422

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0