forked from CakeML/candle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
drule.ml.patch
89 lines (89 loc) · 2.69 KB
/
drule.ml.patch
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
165c165,166
< let (term_match:term list -> term -> term -> instantiation) =
---
> (* OA: could not get this to type check as one declaration; don't know why *)
>
169c170
< with Failure "find" -> n::l in
---
> with Failure "find" -> n::l ;;
173,174c174,175
< if Pervasives.compare y z = 0 then l else failwith "safe_insert"
< with Failure "find" -> n::l in
---
> if y = z then l else failwith "safe_insert"
> with Failure "find" -> n::l ;;
178c179
< fun ty -> mk_var(name,ty) in
---
> fun ty -> mk_var(name,ty) ;;
184c185
< if Pervasives.compare ctm' ctm = 0 then sofar
---
> if ctm' = ctm then sofar
188c189
< if Pervasives.compare ctm vtm = 0 then sofar
---
> if ctm = vtm then sofar
192,193c193,194
< if Pervasives.compare vname cname = 0 then
< if Pervasives.compare vty cty = 0 then sofar
---
> if vname = cname then
> if vty = cty then sofar
206c207
< if Pervasives.compare vty cty = 0 then insts
---
> if vty = cty then insts
213c214
< term_pmatch lconsts env rv rc sofar' in
---
> term_pmatch lconsts env rv rc sofar' ;;
216c217
< itlist (fun (t,x) -> type_match (snd(dest_var x)) (type_of t)) insts in
---
> itlist (fun (t,x) -> type_match (snd(dest_var x)) (type_of t)) insts ;;
233,234c234,235
< if Pervasives.compare t x' = 0 then fail() else (t,x')) realinsts,
< tyins in
---
> if t = x' then fail() else (t,x')) realinsts,
> tyins ;;
240c241
< if Pervasives.compare ctm vtm = 0
---
> if ctm = vtm
258,259c259,260
< if Pervasives.compare cargs pats = 0 then
< if Pervasives.compare chop vhop = 0
---
> if cargs = pats then
> if chop = vhop
276c277
< term_homatch lconsts tyins' pinsts_homs' in
---
> term_homatch lconsts tyins' pinsts_homs' ;;
277a279
> let (term_match:term list -> term -> term -> instantiation) =
326,327c328,329
< let type_unify : hol_type -> hol_type -> (hol_type * hol_type) list
< -> (hol_type * hol_type) list =
---
> let (type_unify : hol_type -> hol_type -> (hol_type * hol_type) list
> -> (hol_type * hol_type) list) =
362c364
< let term_type_unify : term -> term -> instantiation -> instantiation =
---
> let (term_type_unify : term -> term -> instantiation -> instantiation) =
382c384
< let rec unify tm1 tm2 (tminsts, tyinsts as sofar) =
---
> let rec unify tm1 tm2 ((tminsts, tyinsts) as sofar) =
466c468
< if Pervasives.compare tm' tm = 0 then fth else
---
> if tm' = tm then fth else
484c486
< if Pervasives.compare tm' tm = 0 then fth else
---
> if tm' = tm then fth else