Commit b17f561c authored by Andrei Paskevich's avatar Andrei Paskevich

Lexer: handle 1.. correcty

Incidentally, this also helps with (*)
parent 815970d1
......@@ -219,21 +219,21 @@ module InPlaceRevSeq
s1[i1] <> s2[i2]
predicate no_repet (s: seq loc) =
forall i. 0 <= i < length s -> not (mem s[i] s[i+1 ..])
forall i. 0 <= i < length s -> not (mem s[i] s[i+1..])
lemma non_empty_seq:
forall s: seq 'a. length s > 0 ->
s == cons s[0] s[1 .. ]
s == cons s[0] s[1..]
let rec ghost mem_decomp (x: loc) (s: seq loc) : (seq loc, seq loc)
requires { mem x s }
variant { length s }
returns { (s1,s2) -> s == s1 ++ cons x s2 }
=
if eq_loc s[0] x then (empty, s[1 ..])
if eq_loc s[0] x then (empty, s[1..])
else begin
assert { s == cons s[0] s[1 .. ] };
let (s1, s2) = mem_decomp x s[1 .. ] in (cons s[0] s1, s2)
assert { s == cons s[0] s[1..] };
let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2)
end
use import ref.Ref
......@@ -273,16 +273,16 @@ module InPlaceRevSeq
ensures { l1 == l2 }
= if length l1 > 0 && length l2 > 0 then begin
assert { l1[0] = l2[0] = p };
list_seg_functional next l1[1 ..] l2[1 ..] (Map.get next p)
list_seg_functional next l1[1..] l2[1..] (Map.get next p)
end
let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc)
requires { list_seg next p l1 q }
requires { length l1 > 0 }
variant { length l1 }
ensures { list_seg next (Map.get next p)l1[1 .. ] q }
ensures { list_seg next (Map.get next p)l1[1..] q }
= if length l1 > 1 then
list_seg_tail next l1[1 ..] (Map.get next p) q
list_seg_tail next l1[1..] (Map.get next p) q
let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc)
requires { list_seg next p pM q }
......@@ -290,11 +290,11 @@ module InPlaceRevSeq
variant { length pM }
ensures { list_seg next p (pM ++ qM) r }
= if length pM > 0 then
list_seg_append next (Map.get next p) q r pM[1 .. ] qM
list_seg_append next (Map.get next p) q r pM[1..] qM
lemma seq_tail_append:
forall l1 l2: seq 'a.
length l1 > 0 -> (l1 ++ l2)[1 .. ] == l1[1 .. ] ++ l2
length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2
let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc)
requires { list_seg next p (l1 ++ cons q l2) null }
......@@ -302,7 +302,7 @@ module InPlaceRevSeq
ensures { list_seg next p l1 q }
= if length l1 > 0 then begin
list_seg_tail next (l1 ++ cons q l2) p null;
list_seg_prefix next l1[1 ..] l2 (Map.get next p) q
list_seg_prefix next l1[1..] l2 (Map.get next p) q
end
let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc)
......@@ -312,13 +312,13 @@ module InPlaceRevSeq
= assert { list_seg next p l1 q };
if length l1 > 0 then begin
list_seg_tail next l1 p q;
list_seg_sublistl next l1[1 ..] l2 (Map.get next p) q
list_seg_sublistl next l1[1..] l2 (Map.get next p) q
end
lemma get_tail:
forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1 .. ][i] = s[i+1]
forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1]
lemma tail_suffix:
forall i: int, s: seq 'a. 0 <= i < length s -> s[1 .. ][i .. ] == s[i+1 ..]
forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..]
let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc)
requires { list_seg next p pM null }
......@@ -326,7 +326,7 @@ module InPlaceRevSeq
ensures { no_repet pM }
= if length pM > 0 then begin
let h = pM[0] in
let t = pM[1 .. ] in
let t = pM[1..] in
if mem h t then
(* absurd case *)
let (l1,l2) = mem_decomp h t in
......@@ -334,9 +334,9 @@ module InPlaceRevSeq
list_seg_functional next pM (cons h l2) p;
assert { length pM > length (cons h l2) }
else begin
assert { not (mem pM[0] pM[0+1 .. ]) };
assert { not (mem pM[0] pM[0+1..]) };
list_seg_no_repet next (Map.get next p) t;
assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1 .. ]) }
assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) }
end
end
......@@ -362,7 +362,7 @@ module InPlaceRevSeq
variant { length !pM }
assert { length !pM > 0 };
assert { not (mem !p !l1pM) };
let ghost t = !pM[ 1 .. ] in
let ghost t = !pM[1..] in
ghost l1pM := !l1pM ++ cons !p empty;
ghost pM := t;
p := acc next !p
......@@ -392,7 +392,7 @@ module InPlaceRevSeq
r := !p;
p := n;
rM := cons !pM[0] !rM;
pM := !pM[ 1 .. ]
pM := !pM[1..]
done;
!r
......
......@@ -243,7 +243,7 @@ module RandomAccessListWithSeq
let rec tail (l: ral 'a) : ral 'a
requires { 0 < length (elements l) }
variant { l }
ensures { elements result == (elements l)[1 .. ] }
ensures { elements result == (elements l)[1..] }
=
match l with
| Empty -> absurd
......
......@@ -109,9 +109,9 @@ module SchorrWaite
let ghost tl_stackNodes (stack: stacknodes) : stacknodes
requires { Seq.length stack > 0 }
ensures { result = stack[1 .. ] }
ensures { result = stack[1..] }
ensures { forall n. not_in_stack n stack -> not_in_stack n result }
= stack[1 .. ]
= stack[1..]
(** two lemmas about stacks *)
......@@ -124,7 +124,7 @@ module SchorrWaite
let lemma tl_cons (s1 s2: stacknodes) (p: loc)
requires { Seq.length s2 > 0 }
requires { s1 = s2[1 ..] }
requires { s1 = s2[1..] }
requires { p = Seq.get s2 0 }
ensures { s2 = cons p s1 }
= assert { Seq.(==) s2 (cons p s1) }
......
......@@ -214,8 +214,8 @@ module RingBufferSeq
writes { b.first, b.len, b.sequence }
ensures { length b = (old (length b)) - 1 }
ensures { result = S.get (old b.sequence) 0 }
ensures { b.sequence = (old b.sequence)[1 ..] }
= ghost (b.sequence <- b.sequence[1 ..]);
ensures { b.sequence = (old b.sequence)[1..] }
= ghost (b.sequence <- b.sequence[1..]);
let r = b.data[b.first] in
b.len <- b.len - 1;
let n = Array.length b.data in
......
......@@ -67,15 +67,9 @@ rule token = parse
{ Lexing.new_line lexbuf; token lexbuf }
| space+
{ token lexbuf }
| "(**)"
{ token lexbuf }
| "(*(*"
{ Lexlib.comment lexbuf; Lexlib.comment lexbuf; token lexbuf }
| "(*" '\n'
{ Lexing.new_line lexbuf; Lexlib.comment lexbuf; token lexbuf }
| "(*(*)"
| "(*" eof
| "(*" [^ ')']
| "(*)"
{ Lexlib.backjump lexbuf 2; LEFTPAR }
| "(*"
{ Lexlib.comment lexbuf; token lexbuf }
| '_'
{ UNDERSCORE }
......
......@@ -165,6 +165,10 @@ rule token = parse
{ INTEGER (Number.int_literal_oct (Lexlib.remove_underscores s)) }
| '0' ['b' 'B'] (bin bin_sep* as s)
{ INTEGER (Number.int_literal_bin (Lexlib.remove_underscores s)) }
| (dec+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER (Number.int_literal_dec i) }
| '0' ['x' 'X'] (hex+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER (Number.int_literal_hex i) }
| (dec+ as i) ("" as f) ['e' 'E'] (['-' '+']? dec+ as e)
| (dec+ as i) '.' (dec* as f) (['e' 'E'] (['-' '+']? dec+ as e))?
| (dec* as i) '.' (dec+ as f) (['e' 'E'] (['-' '+']? dec+ as e))?
......@@ -177,15 +181,9 @@ rule token = parse
(['p' 'P'] (['-' '+']? dec+ as e))?
{ REAL (Number.real_const_hex i f
(Opt.map Lexlib.remove_leading_plus e)) }
| "(**)"
{ token lexbuf }
| "(*(*"
{ Lexlib.comment lexbuf; Lexlib.comment lexbuf; token lexbuf }
| "(*" '\n'
{ Lexing.new_line lexbuf; Lexlib.comment lexbuf; token lexbuf }
| "(*(*)"
| "(*" eof
| "(*" [^ ')']
| "(*)"
{ Lexlib.backjump lexbuf 2; LEFTPAR }
| "(*"
{ Lexlib.comment lexbuf; token lexbuf }
| "'" (lident as id)
{ QUOTE_LIDENT id }
......
......@@ -17,6 +17,8 @@ val string : Lexing.lexbuf -> string
val update_loc : Lexing.lexbuf -> string option -> int -> int -> unit
val backjump : Lexing.lexbuf -> int -> unit
val remove_leading_plus : string -> string
val remove_underscores : string -> string
......
......@@ -98,6 +98,13 @@ and string_skip_spaces = parse
pos_bol = pos.pos_cnum - chars;
}
let backjump lexbuf chars =
if chars < 0 || chars > lexbuf.lex_curr_pos - lexbuf.lex_start_pos then
invalid_arg "Lexlib.backjump";
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - chars;
lexbuf.lex_curr_p <- { pos with pos_cnum = pos.pos_cnum - chars }
let remove_leading_plus s =
let n = String.length s in
if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment