author  ballarin 
Thu, 19 Feb 2004 15:57:34 +0100  
changeset 14398  c5c47703f763 
child 14445  4392cb82018b 
permissions  rwrr 
14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1 
(* 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

2 
Title: Transitivity reasoner for partial and linear orders 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

3 
Id: $Id$ 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

4 
Author: Oliver Kutter 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

5 
Copyright: TU Muenchen 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

6 
*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

7 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

8 
(* TODO: reduce number of input thms, reduce code duplication *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

9 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

10 
(* 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

11 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

12 
The packages provides tactics partial_tac and linear_tac that use all 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

13 
premises of the form 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

14 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

15 
t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

16 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

17 
to 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

18 
1. either derive a contradiction, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

19 
in which case the conclusion can be any term, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

20 
2. or prove the conclusion, which must be of the same form as the 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

21 
premises (excluding ~(t < u) and ~(t <= u) for partial orders) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

22 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

23 
The package is implemented as an ML functor and thus not limited to the 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

24 
relation <= and friends. It can be instantiated to any partial and/or 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

25 
linear order  for example, the divisibility relation "dvd". In 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

26 
order to instantiate the package for a partial order only, supply 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

27 
dummy theorems to the rules for linear orders, and don't use 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

28 
linear_tac! 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

29 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

30 
*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

31 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

32 
signature LESS_ARITH = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

33 
sig 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

34 
(* Theorems for partial orders *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

35 
val less_reflE: thm (* x < x ==> P *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

36 
val le_refl: thm (* x <= x *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

37 
val less_imp_le: thm (* x < y ==> x <= y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

38 
val eqI: thm (* [ x <= y; y <= x ] ==> x = y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

39 
val eqD1: thm (* x = y ==> x <= y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

40 
val eqD2: thm (* x = y ==> y <= x *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

41 
val less_trans: thm (* [ x <= y; y <= z ] ==> x <= z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

42 
val less_le_trans: thm (* [ x <= y; y < z ] ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

43 
val le_less_trans: thm (* [ x < y; y <= z ] ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

44 
val le_trans: thm (* [ x < y; y < z ] ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

45 
val le_neq_trans : thm (* [ x <= y ; x ~= y ] ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

46 
val neq_le_trans : thm (* [ x ~= y ; x <= y ] ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

47 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

48 
(* Additional theorems for linear orders *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

49 
val not_lessD: thm (* ~(x < y) ==> y <= x *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

50 
val not_leD: thm (* ~(x <= y) ==> y < x *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

51 
val not_lessI: thm (* y <= x ==> ~(x < y) *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

52 
val not_leI: thm (* y < x ==> ~(x <= y) *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

53 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

54 
(* Additional theorems for subgoals of form x ~= y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

55 
val less_imp_neq : thm (* x < y ==> x ~= y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

56 
val eq_neq_eq_imp_neq : thm (* [ x = u ; u ~= v ; v = z] ==> x ~= z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

57 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

58 
(* Analysis of premises and conclusion *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

59 
(* decomp_x (`x Rel y') should yield (x, Rel, y) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

60 
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

61 
other relation symbols cause an error message *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

62 
val decomp_part: Sign.sg > term > (term * string * term) option 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

63 
val decomp_lin: Sign.sg > term > (term * string * term) option 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

64 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

65 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

66 
signature TRANS_TAC = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

67 
sig 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

68 
val partial_tac: int > tactic 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

69 
val linear_tac: int > tactic 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

70 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

71 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

72 
functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

73 
struct 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

74 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

75 
(* Extract subgoal with signature *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

76 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

77 
fun SUBGOAL goalfun i st = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

78 
goalfun (List.nth(prems_of st, i1), i, sign_of_thm st) st 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

79 
handle Subscript => Seq.empty; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

80 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

81 
(* Internal datatype for the proof *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

82 
datatype proof 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

83 
= Asm of int 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

84 
 Thm of proof list * thm; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

85 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

86 
exception Cannot; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

87 
(* Internal exception, raised if conclusion cannot be derived from 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

88 
assumptions. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

89 
exception Contr of proof; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

90 
(* Internal exception, raised if contradiction ( x < x ) was derived *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

91 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

92 
fun prove asms = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

93 
let fun pr (Asm i) = nth_elem (i, asms) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

94 
 pr (Thm (prfs, thm)) = (map pr prfs) MRS thm 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

95 
in pr end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

96 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

97 
(* Internal datatype for inequalities *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

98 
datatype less 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

99 
= Less of term * term * proof 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

100 
 Le of term * term * proof 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

101 
 NotEq of term * term * proof; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

102 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

103 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

104 
(* Misc functions for datatype less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

105 
fun lower (Less (x, _, _)) = x 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

106 
 lower (Le (x, _, _)) = x 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

107 
 lower (NotEq (x,_,_)) = x; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

108 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

109 
fun upper (Less (_, y, _)) = y 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

110 
 upper (Le (_, y, _)) = y 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

111 
 upper (NotEq (_,y,_)) = y; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

112 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

113 
fun getprf (Less (_, _, p)) = p 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

114 
 getprf (Le (_, _, p)) = p 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

115 
 getprf (NotEq (_,_, p)) = p; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

116 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

117 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

118 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

119 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

120 
(* mkasm_partial sign (t, n) : Sign.sg > (Term.term * int) > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

121 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

122 
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

123 
(* translated to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

124 
(* Partial orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

125 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

126 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

127 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

128 
fun mkasm_partial sign (t, n) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

129 
case Less.decomp_part sign t of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

130 
Some (x, rel, y) => (case rel of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

131 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

132 
else [Less (x, y, Asm n)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

133 
 "~<" => [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

134 
 "<=" => [Le (x, y, Asm n)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

135 
 "~<=" => [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

136 
 "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

137 
Le (y, x, Thm ([Asm n], Less.eqD2))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

138 
 "~=" => if (x aconv y) then 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

139 
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

140 
else [ NotEq (x, y, Asm n), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

141 
NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

142 
 _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

143 
"''returned by decomp_part.")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

144 
 None => []; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

145 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

146 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

147 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

148 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

149 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

150 
(* mkasm_linear sign (t, n) : Sign.sg > (Term.term * int) > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

151 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

152 
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

153 
(* translated to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

154 
(* Linear orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

155 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

156 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

157 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

158 
fun mkasm_linear sign (t, n) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

159 
case Less.decomp_lin sign t of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

160 
Some (x, rel, y) => (case rel of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

161 
"<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

162 
else [Less (x, y, Asm n)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

163 
 "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

164 
 "<=" => [Le (x, y, Asm n)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

165 
 "~<=" => if (x aconv y) then 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

166 
raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

167 
else [Less (y, x, Thm ([Asm n], Less.not_leD))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

168 
 "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

169 
Le (y, x, Thm ([Asm n], Less.eqD2))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

170 
 "~=" => if (x aconv y) then 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

171 
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

172 
else [ NotEq (x, y, Asm n), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

173 
NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

174 
 _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

175 
"''returned by decomp_lin.")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

176 
 None => []; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

177 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

178 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

179 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

180 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

181 
(* mkconcl_partial sign t : Sign.sg > Term.term > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

182 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

183 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

184 
(* Partial orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

185 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

186 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

187 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

188 
fun mkconcl_partial sign t = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

189 
case Less.decomp_part sign t of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

190 
Some (x, rel, y) => (case rel of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

191 
"<" => ([Less (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

192 
 "<=" => ([Le (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

193 
 "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

194 
Thm ([Asm 0, Asm 1], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

195 
 "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

196 
 _ => raise Cannot) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

197 
 None => raise Cannot; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

198 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

199 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

200 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

201 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

202 
(* mkconcl_linear sign t : Sign.sg > Term.term > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

203 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

204 
(* Translates conclusion t to an element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

205 
(* Linear orders only. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

206 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

207 
(* ************************************************************************ *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

208 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

209 
fun mkconcl_linear sign t = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

210 
case Less.decomp_lin sign t of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

211 
Some (x, rel, y) => (case rel of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

212 
"<" => ([Less (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

213 
 "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

214 
 "<=" => ([Le (x, y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

215 
 "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

216 
 "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

217 
Thm ([Asm 0, Asm 1], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

218 
 "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

219 
 _ => raise Cannot) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

220 
 None => raise Cannot; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

221 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

222 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

223 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

224 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

225 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

226 
(* mergeLess (less1,less2): less * less > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

227 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

228 
(* Merge to elements of type less according to the following rules *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

229 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

230 
(* x < y && y < z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

231 
(* x < y && y <= z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

232 
(* x <= y && y < z ==> x < z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

233 
(* x <= y && y <= z ==> x <= z *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

234 
(* x <= y && x ~= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

235 
(* x ~= y && x <= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

236 
(* x < y && x ~= y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

237 
(* x ~= y && x < y ==> x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

238 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

239 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

240 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

241 
fun mergeLess (Less (x, _, p) , Less (_ , z, q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

242 
Less (x, z, Thm ([p,q] , Less.less_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

243 
 mergeLess (Less (x, _, p) , Le (_ , z, q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

244 
Less (x, z, Thm ([p,q] , Less.less_le_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

245 
 mergeLess (Le (x, _, p) , Less (_ , z, q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

246 
Less (x, z, Thm ([p,q] , Less.le_less_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

247 
 mergeLess (Le (x, z, p) , NotEq (x', z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

248 
if (x aconv x' andalso z aconv z' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

249 
then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

250 
else error "linear/partial_tac: internal error le_neq_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

251 
 mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

252 
if (x aconv x' andalso z aconv z') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

253 
then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

254 
else error "linear/partial_tac: internal error neq_le_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

255 
 mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

256 
if (x aconv x' andalso z aconv z') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

257 
then Less ((x' , z', q)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

258 
else error "linear/partial_tac: internal error neq_less_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

259 
 mergeLess (Less (x, z, p) , NotEq (x', z', q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

260 
if (x aconv x' andalso z aconv z') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

261 
then Less (x, z, p) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

262 
else error "linear/partial_tac: internal error less_neq_trans" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

263 
 mergeLess (Le (x, _, p) , Le (_ , z, q)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

264 
Le (x, z, Thm ([p,q] , Less.le_trans)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

265 
 mergeLess (_, _) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

266 
error "linear/partial_tac: internal error: undefined case"; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

267 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

268 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

269 
(* ******************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

270 
(* tr checks for valid transitivity step *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

271 
(* ******************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

272 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

273 
infix tr; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

274 
fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

275 
 (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

276 
 (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

277 
 (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

278 
 _ tr _ = false; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

279 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

280 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

281 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

282 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

283 
(* transPath (Lesslist, Less): (less list * less) > less *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

284 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

285 
(* If a path represented by a list of elements of type less is found, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

286 
(* this needs to be contracted to a single element of type less. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

287 
(* Prior to each transitivity step it is checked whether the step is *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

288 
(* valid. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

289 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

290 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

291 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

292 
fun transPath ([],lesss) = lesss 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

293 
 transPath (x::xs,lesss) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

294 
if lesss tr x then transPath (xs, mergeLess(lesss,x)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

295 
else error "linear/partial_tac: internal error transpath"; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

296 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

297 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

298 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

299 
(* less1 subsumes less2 : less > less > bool *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

300 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

301 
(* subsumes checks whether less1 implies less2 *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

302 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

303 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

304 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

305 
infix subsumes; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

306 
fun (Less (x, y, _)) subsumes (Le (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

307 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

308 
 (Less (x, y, _)) subsumes (Less (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

309 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

310 
 (Le (x, y, _)) subsumes (Le (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

311 
(x aconv x' andalso y aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

312 
 (Less (x, y, _)) subsumes (NotEq (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

313 
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

314 
 (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

315 
(x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

316 
 (Le _) subsumes (Less _) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

317 
error "linear/partial_tac: internal error: Le cannot subsume Less" 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

318 
 _ subsumes _ = false; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

319 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

320 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

321 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

322 
(* triv_solv less1 : less > proof Library.option *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

323 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

324 
(* Solves trivial goal x <= x. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

325 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

326 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

327 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

328 
fun triv_solv (Le (x, x', _)) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

329 
if x aconv x' then Some (Thm ([], Less.le_refl)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

330 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

331 
 triv_solv _ = None; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

332 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

333 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

334 
(* Graph functions *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

335 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

336 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

337 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

338 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

339 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

340 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

341 
(* General: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

342 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

343 
(* Inequalities are represented by various types of graphs. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

344 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

345 
(* 1. (Term.term * Term.term list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

346 
(*  Graph of this type is generated from the assumptions, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

347 
(* does not contain information on which edge stems from which *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

348 
(* assumption. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

349 
(*  Used to compute strong components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

350 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

351 
(* 2. (Term.term * (Term.term * less) list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

352 
(*  Graph of this type is generated from the assumptions, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

353 
(* it does contain information on which edge stems from which *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

354 
(* assumption. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

355 
(*  Used to reconstruct paths. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

356 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

357 
(* 3. (int * (int * less) list ) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

358 
(*  Graph of this type is generated from the strong components of *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

359 
(* graph of type 2. It consists of the strong components of *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

360 
(* graph 2, where nodes are indices of the components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

361 
(* Only edges between components are part of this graph. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

362 
(*  Used to reconstruct paths between several components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

363 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

364 
(* 4. (int * int list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

365 
(*  Graph of this type is generated from graph of type 3, but *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

366 
(* edge information of type less is removed. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

367 
(*  Used to *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

368 
(*  Compute transposed graphs of type 4. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

369 
(*  Compute list of components reachable from a component. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

370 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

371 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

372 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

373 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

374 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

375 
(* *********************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

376 
(* Functions for constructing graphs *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

377 
(* *********************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

378 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

379 
fun addLessEdge (v,d,[]) = [(v,d)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

380 
 addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

381 
else (u,dl):: (addLessEdge(v,d,el)); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

382 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

383 
fun addTermEdge (v,u,[]) = [(v,[u])] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

384 
 addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

385 
else (x,adj) :: addTermEdge (v,u,el); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

386 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

387 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

388 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

389 
(* buildGraphs constructs three graphs from a list of type less: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

390 
(* g1: graph for the <= relation *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

391 
(* g2: graph for the <= relation with additional information for *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

392 
(* proof reconstruction *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

393 
(* neqEdges: all edges that are candidates for a ~= *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

394 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

395 
(* ********************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

396 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

397 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

398 
fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

399 
 buildGraphs (l::ls,g1,g2,neqEdges) = case l of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

400 
(Less (x,y,p)) =>( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

401 
let val g1' = addTermEdge (x,y,g1) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

402 
and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

403 
in buildGraphs (ls,g1',g2',l::neqEdges) end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

404 
 (Le (x,y,p)) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

405 
( let val g1' = addTermEdge (x,y,g1) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

406 
and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

407 
in buildGraphs (ls,g1',g2',neqEdges) end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

408 
 (NotEq (x,y,p)) => ( buildGraphs (ls,g1,g2,l::neqEdges) ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

409 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

410 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

411 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

412 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

413 
(* adjacent_term g u : (Term.term * 'a list ) list > Term.term > 'a list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

414 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

415 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

416 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

417 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

418 
fun adjacent_term ((v,adj)::el) u = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

419 
if u aconv v then adj else adjacent_term el u 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

420 
 adjacent_term nil _ = [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

421 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

422 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

423 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

424 
(* adjacent_term g u : (''a * 'b list ) list > ''a > 'b list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

425 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

426 
(* List of successors of u in graph g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

427 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

428 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

429 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

430 
fun adjacent ((v,adj)::el) u = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

431 
if u = v then adj else adjacent el u 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

432 
 adjacent nil _ = [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

433 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

434 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

435 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

436 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

437 
(* transpose_term g: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

438 
(* (Term.term * Term.term list) list > (Term.term * Term.term list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

439 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

440 
(* Computes transposed graph g' from g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

441 
(* by reversing all edges u > v to v > u *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

442 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

443 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

444 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

445 
fun transpose_term g = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

446 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

447 
(* Compute list of reversed edges for each adjacency list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

448 
fun flip (u,v::el) = (v,u) :: flip (u,el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

449 
 flip (_,nil) = nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

450 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

451 
(* Compute adjacency list for node u from the list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

452 
and return a likewise reduced list of edges. The list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

453 
is searches for edges starting from u, and these edges are removed. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

454 
fun gather (u,(v,w)::el) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

455 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

456 
val (adj,edges) = gather (u,el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

457 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

458 
if u aconv v then (w::adj,edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

459 
else (adj,(v,w)::edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

460 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

461 
 gather (_,nil) = (nil,nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

462 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

463 
(* For every node in the input graph, call gather to find all reachable 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

464 
nodes in the list of edges *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

465 
fun assemble ((u,_)::el) edges = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

466 
let val (adj,edges) = gather (u,edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

467 
in (u,adj) :: assemble el edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

468 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

469 
 assemble nil _ = nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

470 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

471 
(* Compute, for each adjacency list, the list with reversed edges, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

472 
and concatenate these lists. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

473 
val flipped = foldr (op @) ((map flip g),nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

474 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

475 
in assemble g flipped end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

476 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

477 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

478 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

479 
(* transpose g: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

480 
(* (''a * ''a list) list > (''a * ''a list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

481 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

482 
(* Computes transposed graph g' from g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

483 
(* by reversing all edges u > v to v > u *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

484 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

485 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

486 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

487 
fun transpose g = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

488 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

489 
(* Compute list of reversed edges for each adjacency list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

490 
fun flip (u,v::el) = (v,u) :: flip (u,el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

491 
 flip (_,nil) = nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

492 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

493 
(* Compute adjacency list for node u from the list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

494 
and return a likewise reduced list of edges. The list of edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

495 
is searches for edges starting from u, and these edges are removed. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

496 
fun gather (u,(v,w)::el) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

497 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

498 
val (adj,edges) = gather (u,el) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

499 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

500 
if u = v then (w::adj,edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

501 
else (adj,(v,w)::edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

502 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

503 
 gather (_,nil) = (nil,nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

504 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

505 
(* For every node in the input graph, call gather to find all reachable 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

506 
nodes in the list of edges *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

507 
fun assemble ((u,_)::el) edges = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

508 
let val (adj,edges) = gather (u,edges) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

509 
in (u,adj) :: assemble el edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

510 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

511 
 assemble nil _ = nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

512 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

513 
(* Compute, for each adjacency list, the list with reversed edges, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

514 
and concatenate these lists. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

515 
val flipped = foldr (op @) ((map flip g),nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

516 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

517 
in assemble g flipped end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

518 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

519 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

520 
(* scc_term : (term * term list) list > term list list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

521 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

522 
(* The following is based on the algorithm for finding strongly 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

523 
connected components described in Introduction to Algorithms, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

524 
by Cormon, Leiserson, and Rivest, section 23.5. The input G 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

525 
is an adjacency list description of a directed graph. The 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

526 
output is a list of the strongly connected components (each a 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

527 
list of vertices). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

528 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

529 
fun scc_term G = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

530 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

531 
(* Ordered list of the vertices that DFS has finished with; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

532 
most recently finished goes at the head. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

533 
val finish : term list ref = ref nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

534 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

535 
(* List of vertices which have been visited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

536 
val visited : term list ref = ref nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

537 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

538 
fun been_visited v = exists (fn w => w aconv v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

539 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

540 
(* Given the adjacency list rep of a graph (a list of pairs), 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

541 
return just the first element of each pair, yielding the 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

542 
vertex list. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

543 
val members = map (fn (v,_) => v) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

544 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

545 
(* Returns the nodes in the DFS tree rooted at u in g *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

546 
fun dfs_visit g u : term list = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

547 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

548 
val _ = visited := u :: !visited 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

549 
val descendents = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

550 
foldr (fn (v,ds) => if been_visited v then ds 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

551 
else v :: dfs_visit g v @ ds) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

552 
((adjacent_term g u) ,nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

553 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

554 
finish := u :: !finish; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

555 
descendents 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

556 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

557 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

558 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

559 
(* DFS on the graph; apply dfs_visit to each vertex in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

560 
the graph, checking first to make sure the vertex is 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

561 
as yet unvisited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

562 
app (fn u => if been_visited u then () 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

563 
else (dfs_visit G u; ())) (members G); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

564 
visited := nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

565 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

566 
(* We don't reset finish because its value is used by 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

567 
revfold below, and it will never be used again (even 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

568 
though dfs_visit will continue to modify it). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

569 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

570 
(* DFS on the transpose. The vertices returned by 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

571 
dfs_visit along with u form a connected component. We 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

572 
collect all the connected components together in a 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

573 
list, which is what is returned. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

574 
foldl (fn (comps,u) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

575 
if been_visited u then comps 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

576 
else ((u :: dfs_visit (transpose_term G) u) :: comps)) (nil,(!finish)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

577 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

578 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

579 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

580 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

581 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

582 
(* dfs_int_reachable g u: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

583 
(* (int * int list) list > int > int list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

584 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

585 
(* Computes list of all nodes reachable from u in g. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

586 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

587 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

588 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

589 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

590 
fun dfs_int_reachable g u = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

591 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

592 
(* List of vertices which have been visited. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

593 
val visited : int list ref = ref nil 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

594 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

595 
fun been_visited v = exists (fn w => w = v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

596 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

597 
fun dfs_visit g u : int list = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

598 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

599 
val _ = visited := u :: !visited 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

600 
val descendents = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

601 
foldr (fn (v,ds) => if been_visited v then ds 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

602 
else v :: dfs_visit g v @ ds) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

603 
( ((adjacent g u)) ,nil) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

604 
in descendents end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

605 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

606 
in u :: dfs_visit g u end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

607 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

608 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

609 
fun indexComps components = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

610 
ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components 1)); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

611 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

612 
fun indexNodes IndexComp = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

613 
flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

614 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

615 
fun getIndex v [] = ~1 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

616 
 getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

617 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

618 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

619 
(* ***************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

620 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

621 
(* evalcompgraph components g ntc : *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

622 
(* Term.term list list > *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

623 
(* (Term.term * (Term.term * less) list) list > *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

624 
(* (Term.term * int) list > (int * (int * less) list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

625 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

626 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

627 
(* Computes, from graph g, list of all its components and the list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

628 
(* ntc (nodes, index of component) a graph whose nodes are the *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

629 
(* indices of the components of g. Egdes of the new graph are *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

630 
(* only the edges of g linking two components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

631 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

632 
(* ***************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

633 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

634 
fun evalcompgraph components g ntc = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

635 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

636 
(* Liste (Index der Komponente, Komponente *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

637 
val IndexComp = indexComps components; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

638 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

639 
(* Compute new graph with the property that it only contains edges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

640 
between components. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

641 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

642 
(* k is index of current start component. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

643 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

644 
fun processComponent (k, comp) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

645 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

646 
(* all edges pointing away from the component *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

647 
(* (Term.term * less) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

648 
val allEdges = flat (map (adjacent_term g) comp); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

649 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

650 
(* choose those edges pointing to nodes outside 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

651 
the current component *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

652 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

653 
fun selectEdges [] = [] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

654 
 selectEdges ((v,l)::es) = let val k' = getIndex v ntc in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

655 
if k' = k then selectEdges es else (k', l) :: (selectEdges es) end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

656 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

657 
(* Insert edge into sorted list of edges, where edge is 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

658 
only added if 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

659 
 it is found for the first time 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

660 
 it is a <= edge and no parallel < edge was found earlier 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

661 
 it is a < edge 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

662 
*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

663 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

664 
fun insert (h,l) [] = [(h,l)] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

665 
 insert (h,l) ((k',l')::es) = if h = k' then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

666 
case l of (Less (_, _, _)) => (h,l)::es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

667 
 _ => (case l' of (Less (_, _, _)) => (h,l')::es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

668 
 _ => (k',l)::es) ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

669 
else (k',l'):: insert (h,l) es; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

670 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

671 
(* Reorganise list of edges such that 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

672 
 duplicate edges are removed 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

673 
 if a < edge and a <= edge exist at the same time, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

674 
remove <= edge *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

675 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

676 
fun sortEdges [] sorted = sorted: (int * less) list 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

677 
 sortEdges (e::es) sorted = sortEdges es (insert e sorted); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

678 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

679 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

680 
(k, (sortEdges (selectEdges allEdges) [])) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

681 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

682 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

683 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

684 
in map processComponent IndexComp end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

685 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

686 
(* Remove ``less'' edge info from graph *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

687 
(* type ('a * ('a * less) list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

688 
fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

689 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

690 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

691 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

692 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

693 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

694 
(* dfs_term g u v: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

695 
(* (Term.term *(Term.term * less) list) list > *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

696 
(* Term.term > Term.term > (bool * less list) *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

697 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

698 
(* Depth first search of v from u. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

699 
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

700 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

701 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

702 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

703 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

704 
fun dfs_term g u v = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

705 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

706 
(* TODO: this comment is unclear *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

707 
(* Liste der gegangenen Kanten, 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

708 
die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

709 
für die gilt (upper e) = u *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

710 
val pred : less list ref = ref nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

711 
val visited: term list ref = ref nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

712 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

713 
fun been_visited v = exists (fn w => w aconv v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

714 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

715 
fun dfs_visit u' = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

716 
let val _ = visited := u' :: (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

717 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

718 
fun update l = let val _ = pred := l ::(!pred) in () end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

719 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

720 
in if been_visited v then () 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

721 
else (app (fn (v',l) => if been_visited v' then () else ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

722 
update l; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

723 
dfs_visit v'; ()) )) (adjacent_term g u') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

724 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

725 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

726 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

727 
dfs_visit u; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

728 
if (been_visited v) then (true, (!pred)) else (false , []) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

729 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

730 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

731 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

732 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

733 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

734 
(* completeTermPath u v g: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

735 
(* Term.term > Term.term > (Term.term * (Term.term * less) list) list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

736 
(* > less list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

737 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

738 
(* Complete the path from u to v in graph g. Path search is performed *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

739 
(* with dfs_term g u v. This yields for each node v' its predecessor u' *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

740 
(* and the edge u' > v'. Allows traversing graph backwards from v and *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

741 
(* finding the path u > v. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

742 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

743 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

744 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

745 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

746 
fun completeTermPath u v g = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

747 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

748 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

749 
val (found, pred) = dfs_term g u v; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

750 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

751 
fun path x y = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

752 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

753 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

754 
(* find predecessor u of node v and the edge u > v *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

755 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

756 
fun lookup v [] = raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

757 
 lookup v (e::es) = if (upper e) aconv v then e else lookup v es; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

758 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

759 
(* traverse path backwards and return list of visited edges *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

760 
fun rev_path v = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

761 
let val l = lookup v pred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

762 
val u = lower l; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

763 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

764 
if u aconv x then [l] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

765 
else (rev_path u) @ [l] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

766 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

767 
in rev_path y end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

768 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

769 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

770 
if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

771 
else path u v ) else raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

772 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

773 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

774 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

775 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

776 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

777 
(* dfs_int g u v: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

778 
(* (int *(int * less) list) list > int > int *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

779 
(* > (bool *(int* less) list) *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

780 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

781 
(* Depth first search of v from u. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

782 
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

783 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

784 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

785 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

786 
fun dfs_int g u v = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

787 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

788 
val pred : (int * less ) list ref = ref nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

789 
val visited: int list ref = ref nil; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

790 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

791 
fun been_visited v = exists (fn w => w = v) (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

792 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

793 
fun dfs_visit u' = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

794 
let val _ = visited := u' :: (!visited) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

795 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

796 
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

797 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

798 
in if been_visited v then () 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

799 
else (app (fn (v',l) => if been_visited v' then () else ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

800 
update (v',l); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

801 
dfs_visit v'; ()) )) (adjacent g u') 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

802 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

803 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

804 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

805 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

806 
dfs_visit u; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

807 
if (been_visited v) then (true, (!pred)) else (false , []) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

808 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

809 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

810 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

811 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

812 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

813 
(* findProof (g2, cg2, neqEdges, components, ntc) subgoal: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

814 
(* (Term.term * (Term.term * less) list) list * *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

815 
(* (int * (int * less) list) list * less list * Term.term list list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

816 
(* * ( (Term.term * int) > proof *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

817 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

818 
(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

819 
(* subgoal. Raises exception Cannot if this is not possible. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

820 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

821 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

822 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

823 
fun findProof (g2, cg2, neqEdges, components, ntc ) subgoal = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

824 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

825 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

826 
(* complete path x y from component graph *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

827 
fun completeComponentPath x y predlist = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

828 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

829 
val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

830 
val yi = getIndex y ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

831 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

832 
fun lookup k [] = raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

833 
 lookup k ((h,l)::us) = if k = h then l else lookup k us; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

834 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

835 
fun rev_completeComponentPath y' = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

836 
let val edge = lookup (getIndex y' ntc) predlist 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

837 
val u = lower edge 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

838 
val v = upper edge 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

839 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

840 
if (getIndex u ntc) = xi then 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

841 
(completeTermPath x u g2)@[edge]@(completeTermPath v y' g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

842 
else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

843 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

844 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

845 
if x aconv y then 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

846 
[(Le (x, y, (Thm ([], Less.le_refl))))] 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

847 
else ( if xi = yi then completeTermPath x y g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

848 
else rev_completeComponentPath y ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

849 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

850 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

851 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

852 
(* findLess e x y xi yi xreachable yreachable *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

853 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

854 
(* Find a path from x through e to y, of weight < *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

855 
(* ******************************************************************* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

856 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

857 
fun findLess e x y xi yi Xreachable Yreachable = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

858 
let val u = lower e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

859 
val v = upper e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

860 
val ui = getIndex u ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

861 
val vi = getIndex v ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

862 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

863 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

864 
if ui mem Xreachable andalso vi mem Xreachable andalso 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

865 
ui mem Yreachable andalso vi mem Yreachable then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

866 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

867 
(case e of (Less (_, _, _)) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

868 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

869 
val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

870 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

871 
if xufound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

872 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

873 
val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

874 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

875 
if vyfound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

876 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

877 
val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

878 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

879 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

880 
if xyLesss subsumes subgoal then Some (getprf xyLesss) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

881 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

882 
end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

883 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

884 
end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

885 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

886 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

887 
 _ => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

888 
let val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

889 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

890 
if xufound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

891 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

892 
val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

893 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

894 
if uvfound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

895 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

896 
val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

897 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

898 
if vyfound then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

899 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

900 
val uvpath = completeComponentPath u v uvpred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

901 
val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

902 
val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

903 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

904 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

905 
if xyLesss subsumes subgoal then Some (getprf xyLesss) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

906 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

907 
end ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

908 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

909 
end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

910 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

911 
end ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

912 
else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

913 
end ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

914 
) else None 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

915 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

916 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

917 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

918 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

919 
(* looking for x <= y: any path from x to y is sufficient *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

920 
case subgoal of (Le (x, y, _)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

921 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

922 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

923 
val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

924 
val yi = getIndex y ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

925 
(* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

926 
zu der in der y liegt *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

927 
val (found, pred) = dfs_int cg2 xi yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

928 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

929 
if found then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

930 
let val xypath = completeComponentPath x y pred 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

931 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

932 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

933 
(case xyLesss of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

934 
(Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], Less.less_imp_le)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

935 
else raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

936 
 _ => if xyLesss subsumes subgoal then (getprf xyLesss) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

937 
else raise Cannot) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

938 
end ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

939 
else raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

940 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

941 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

942 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

943 
(* looking for x < y: particular path required, which is not necessarily 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

944 
found by normal dfs *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

945 
 (Less (x, y, _)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

946 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

947 
val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

948 
val yi = getIndex y ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

949 
val cg2' = stripOffLess cg2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

950 
val cg2'_transpose = transpose cg2' 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

951 
(* alle von x aus erreichbaren Komponenten *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

952 
val xreachable = dfs_int_reachable cg2' xi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

953 
(* all comonents reachable from y in the transposed graph cg2' *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

954 
val yreachable = dfs_int_reachable cg2'_transpose yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

955 
(* for all edges u ~= v or u < v check if they are part of path x < y *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

956 
fun processNeqEdges [] = raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

957 
 processNeqEdges (e::es) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

958 
case (findLess e x y xi yi xreachable yreachable) of (Some prf) => prf 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

959 
 _ => processNeqEdges es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

960 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

961 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

962 
processNeqEdges neqEdges 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

963 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

964 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

965 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

966 
 (NotEq (x, y, _)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

967 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

968 
let val xi = getIndex x ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

969 
val yi = getIndex y ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

970 
val cg2' = stripOffLess cg2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

971 
val cg2'_transpose = transpose cg2' 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

972 
val xreachable = dfs_int_reachable cg2' xi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

973 
val yreachable = dfs_int_reachable cg2'_transpose yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

974 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

975 
fun processNeqEdges [] = raise Cannot 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

976 
 processNeqEdges (e::es) = ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

977 
let val u = lower e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

978 
val v = upper e 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

979 
val ui = getIndex u ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

980 
val vi = getIndex v ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

981 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

982 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

983 
(* if x ~= y follows from edge e *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

984 
if e subsumes subgoal then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

985 
case e of (Less (u, v, q)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

986 
if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

987 
else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

988 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

989 
 (NotEq (u,v, q)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

990 
if u aconv x andalso v aconv y then q 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

991 
else (Thm ([q], thm "not_sym")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

992 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

993 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

994 
(* if SCC_x is linked to SCC_y via edge e *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

995 
else if ui = xi andalso vi = yi then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

996 
case e of (Less (_, _,_)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

997 
let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

998 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

999 
in (Thm ([getprf xyLesss], Less.less_imp_neq)) end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1000 
 _ => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1001 
let val xupath = completeTermPath x u g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1002 
val uxpath = completeTermPath u x g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1003 
val vypath = completeTermPath v y g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1004 
val yvpath = completeTermPath y v g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1005 
val xuLesss = transPath (tl xupath, hd xupath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1006 
val uxLesss = transPath (tl uxpath, hd uxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1007 
val vyLesss = transPath (tl vypath, hd vypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1008 
val yvLesss = transPath (tl yvpath, hd yvpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1009 
val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1010 
val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1011 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1012 
(Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1013 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1014 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1015 
) else if ui = yi andalso vi = xi then ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1016 
case e of (Less (_, _,_)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1017 
let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1018 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1019 
in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1020 
 _ => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1021 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1022 
let val yupath = completeTermPath y u g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1023 
val uypath = completeTermPath u y g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1024 
val vxpath = completeTermPath v x g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1025 
val xvpath = completeTermPath x v g2 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1026 
val yuLesss = transPath (tl yupath, hd yupath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1027 
val uyLesss = transPath (tl uypath, hd uypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1028 
val vxLesss = transPath (tl vxpath, hd vxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1029 
val xvLesss = transPath (tl xvpath, hd xvpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1030 
val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1031 
val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1032 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1033 
(Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1034 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1035 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1036 
) else ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1037 
(* there exists a path x < y or y < x such that 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1038 
x ~= y may be concluded *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1039 
case (findLess e x y xi yi xreachable yreachable) of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1040 
(Some prf) => (Thm ([prf], Less.less_imp_neq)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1041 
 None => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1042 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1043 
val yr = dfs_int_reachable cg2' yi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1044 
val xr = dfs_int_reachable cg2'_transpose xi 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1045 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1046 
case (findLess e y x yi xi yr xr) of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1047 
(Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1048 
 _ => processNeqEdges es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1049 
end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1050 
) end) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1051 
in processNeqEdges neqEdges end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1052 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1053 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1054 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1055 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1056 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1057 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1058 
(* checkComponents g components ntc neqEdges: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1059 
(* (Term.term * (Term.term * less) list) list > Term.term list list > *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1060 
(* (Term.term * int) > less list > bool *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1061 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1062 
(* For each edge in the list neqEdges check if it leads to a contradiction.*) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1063 
(* We have a contradiction for edge u ~= v and u < v if: *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1064 
(*  u and v are in the same component, *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1065 
(* that is, a path u <= v and a path v <= u exist, hence u = v. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1066 
(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1067 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1068 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1069 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1070 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1071 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1072 
fun checkComponents g components ntc neqEdges = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1073 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1074 
(* Construct proof by contradiction for edge *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1075 
fun handleContr edge = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1076 
(case edge of 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1077 
(Less (x, y, _)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1078 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1079 
val xxpath = edge :: (completeTermPath y x g) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1080 
val xxLesss = transPath (tl xxpath, hd xxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1081 
val q = getprf xxLesss 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1082 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1083 
raise (Contr (Thm ([q], Less.less_reflE ))) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1084 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1085 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1086 
 (NotEq (x, y, _)) => ( 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1087 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1088 
val xypath = (completeTermPath x y g) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1089 
val yxpath = (completeTermPath y x g) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1090 
val xyLesss = transPath (tl xypath, hd xypath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1091 
val yxLesss = transPath (tl yxpath, hd yxpath) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1092 
val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1093 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1094 
raise (Contr (Thm ([q], Less.less_reflE ))) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1095 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1096 
) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1097 
 _ => error "trans_tac/checkCompoents/handleContr: invalid Contradiction"); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1098 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1099 
(* Check each edge in neqEdges for contradiction. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1100 
If there is a contradiction, call handleContr, otherwise do nothing. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1101 
fun checkNeqEdges [] = () 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1102 
 checkNeqEdges (e::es) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1103 
(case e of (Less (u, v, _)) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1104 
if (getIndex u ntc) = (getIndex v ntc) then handleContr e g 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1105 
else checkNeqEdges es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1106 
 (NotEq (u, v, _)) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1107 
if (getIndex u ntc) = (getIndex v ntc) then handleContr e g 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1108 
else checkNeqEdges es 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1109 
 _ => checkNeqEdges es) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1110 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1111 
in if g = [] then () else checkNeqEdges neqEdges end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1112 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1113 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1114 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1115 
(* solvePartialOrder sign (asms,concl) : *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1116 
(* Sign.sg > less list * Term.term > proof list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1117 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1118 
(* Find proof if possible for partial orders. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1119 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1120 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1121 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1122 
fun solvePartialOrder sign (asms, concl) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1123 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1124 
val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1125 
val components = scc_term g1 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1126 
val ntc = indexNodes (indexComps components) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1127 
val cg2 = evalcompgraph components g2 ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1128 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1129 
(* Check for contradiction within assumptions *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1130 
checkComponents g2 components ntc neqEdges; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1131 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1132 
val (subgoals, prf) = mkconcl_partial sign concl 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1133 
fun solve facts less = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1134 
(case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1135 
 Some prf => prf ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1136 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1137 
map (solve asms) subgoals 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1138 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1139 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1140 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1141 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1142 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1143 
(* solveTotalOrder sign (asms,concl) : *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1144 
(* Sign.sg > less list * Term.term > proof list *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1145 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1146 
(* Find proof if possible for linear orders. *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1147 
(* *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1148 
(* *********************************************************************** *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1149 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1150 
fun solveTotalOrder sign (asms, concl) = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1151 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1152 
val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1153 
val components = scc_term g1 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1154 
val ntc = indexNodes (indexComps components) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1155 
val cg2 = evalcompgraph components g2 ntc 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1156 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1157 
checkComponents g2 components ntc neqEdges; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1158 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1159 
val (subgoals, prf) = mkconcl_linear sign concl 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1160 
fun solve facts less = 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1161 
(case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1162 
 Some prf => prf ) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1163 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1164 
map (solve asms) subgoals 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1165 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1166 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1167 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1168 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1169 
(* partial_tac  solves linear/total orders *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1170 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1171 
val partial_tac = SUBGOAL (fn (A, n, sign) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1172 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1173 
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1174 
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1175 
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1176 
val lesss = flat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs  1))) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1177 
val prfs = solvePartialOrder sign (lesss, C); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1178 
val (subgoals, prf) = mkconcl_partial sign C; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1179 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1180 
METAHYPS (fn asms => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1181 
let val thms = map (prove asms) prfs 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1182 
in rtac (prove thms prf) 1 end) n 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1183 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1184 
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1185 
 Cannot => no_tac 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1186 
); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1187 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1188 
(* linear_tac  solves linear/total orders *) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1189 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1190 
val linear_tac = SUBGOAL (fn (A, n, sign) => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1191 
let 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1192 
val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1193 
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1194 
val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1195 
val lesss = flat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs  1))) 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1196 
val prfs = solveTotalOrder sign (lesss, C); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1197 
val (subgoals, prf) = mkconcl_linear sign C; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1198 
in 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1199 
METAHYPS (fn asms => 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1200 
let val thms = map (prove asms) prfs 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1201 
in rtac (prove thms prf) 1 end) n 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1202 
end 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1203 
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1204 
 Cannot => no_tac); 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1205 

c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1206 
end; 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
diff
changeset

1207 