forked from jrh13/hol-light
-
Notifications
You must be signed in to change notification settings - Fork 2
/
parser.ml.patch
52 lines (52 loc) · 1.74 KB
/
parser.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
24a25,29
> let pp_exn e =
> match e with
> | Noparse -> Pretty_printer.token "Noparse"
> | _ -> pp_exn e;;
>
125c130
< String.make 1 (Char.chr(int_of_string("0x"^h^l))),rst
---
> String.str (Char.chr(int_of_string("0x"^h^l))),rst
127c132
< String.make 1 (Char.chr(int_of_string(a^b^c))),rst
---
> String.str (Char.chr(int_of_string(a^b^c))),rst
182c187
< let mk_prefinty:num->pretype =
---
> let (mk_prefinty:num->pretype) =
288c293,295
< let pdest_eq (Combp(Combp(Varp(("="|"<=>"),_),l),r)) = l,r in
---
> let pdest_eq t =
> match t with
> | Combp(Combp(Varp(("="|"<=>"),_),l),r) -> l,r in
322,323c329,330
< let ns = map (fun i -> Char.code(String.get s i))
< (0--(String.length s - 1)) in
---
> let ns = map (fun i -> Char.ord (String.sub s i))
> (0--(String.size s - 1)) in
364,367c371,374
< Ident s::rst when String.length s >= 2 &&
< String.sub s 0 1 = "\"" &&
< String.sub s (String.length s - 1) 1 = "\""
< -> String.sub s 1 (String.length s - 2),rst
---
> Ident s::rst when String.size s >= 2 &&
> String.sub s 0 = '"' &&
> String.sub s (String.size s - 1) = '"'
> -> String.substring s 1 (String.size s - 2),rst
385c392
< let n_d = power_num (Int 10) (Int (String.length r0)) in
---
> let n_d = power_num (Int 10) (Int (String.size r0)) in
515,517c522,524
< not(String.length s >= 2 &&
< String.sub s 0 1 = "\"" &&
< String.sub s (String.length s - 1) 1 = "\"")
---
> not(String.size s >= 2 &&
> String.sub s 0 = '"' &&
> String.sub s (String.size s - 1) = '"')