Merge branch 'master' into master

doc/book/part1/part1_termination.rst

@@ -65,14 +65,14 @@ if any of the following are true:
 
 1. **The ordering on integers**:
 
-   ``t1 = nat`` and ``t2 = nat`` and ``v1 < v₂``
+   ``t1 = nat`` and ``t2 = nat`` and ``v1 < v2``
 
    Negative integers are not related by the `<<` relation, which is
    only a _partial_ order.
 
 2. **The sub-term ordering on inductive types**
 
-    If ``v₂ = D u1 ... un``, where ``D`` is a constructor of an
+    If ``v2 = D u1 ... un``, where ``D`` is a constructor of an
     inductive type fully applied to arguments ``u1`` to ``un``, then
     ``v1 << v2`` if either
 
@@ -150,7 +150,7 @@ F* also provides a convenience to enhance the well-founded ordering
 lists of terms ``v1, ..., vn`` and ``u1, ..., un``, F* accepts that
 the following lexicographic ordering::
 
-   v1 << u1 ‌‌\/ (v1 == u1 /\ (v₂ << u₂ ‌‌\/ (v₂ == u₂ /\ ( ... vn << un))))
+   v1 << u1 ‌‌\/ (v1 == u1 /\ (v2 << u2 ‌‌\/ (v2 == u2 /\ ( ... vn << un))))
 
 is also well-founded. In fact, it is possible to prove in F* that this
 ordering is well-founded, provided ``<<`` is itself well-founded.

doc/book/part4/part4_pure.rst

@@ -698,7 +698,7 @@ defined as shown below in ``prims.fst``:
 .. code-block:: fstar
 
    effect Pure (a:Type) (req:Type0) (ens:a -> Type0) =
-          PURE a (fun post -> req /\ (forall x. ens x /\ post x))
+          PURE a (fun post -> req /\ (forall x. ens x ==> post x))
 
 The signature of ``Pure`` is ``Pure a req ens``, where ``req`` is the
 precondition and ``ens:a -> Type0`` is the postcondition. Using

ocaml/fstar-lib/FStar_Parser_LexFStar.ml

@@ -446,8 +446,9 @@ match%sedlex lexbuf with
    let s = L.lexeme lexbuf in
    let name = BatString.lchop ~n:3 s in
    Buffer.clear blob_buffer;
+   let snap = Sedlexing.snapshot lexbuf in
    let pos = L.current_pos lexbuf in
-   uninterpreted_blob name pos blob_buffer lexbuf
+   uninterpreted_blob snap name pos blob_buffer lexbuf
  | "`%" -> BACKTICK_PERC
  | "`#" -> BACKTICK_HASH
  | "`@" -> BACKTICK_AT
@@ -637,19 +638,19 @@ match%sedlex lexbuf with
    comment inner buffer startpos lexbuf
  | _ -> assert false
 
-and uninterpreted_blob name pos buffer lexbuf =
+and uninterpreted_blob snap name pos buffer lexbuf =
 match %sedlex lexbuf with
  | "```" ->
-   BLOB(name, Buffer.contents buffer, pos)
+   BLOB(name, Buffer.contents buffer, pos, snap)
  | eof ->
    EOF
  | newline ->
    L.new_line lexbuf;
    Buffer.add_string buffer (L.lexeme lexbuf);
-   uninterpreted_blob name pos buffer lexbuf
+   uninterpreted_blob snap name pos buffer lexbuf
  | any ->
    Buffer.add_string buffer (L.lexeme lexbuf);
-   uninterpreted_blob name pos buffer lexbuf
+   uninterpreted_blob snap name pos buffer lexbuf
  | _ -> assert false
 
 and ignore_endline lexbuf =

ocaml/fstar-lib/FStar_Parser_Parse.mly

@@ -52,8 +52,11 @@ let none_to_empty_list x =
   | None -> []
   | Some l -> l
 
-let parse_extension_blob (extension_name:string) (s:string) r : FStar_Parser_AST.decl' =
-    DeclSyntaxExtension (extension_name, s, r)
+let parse_extension_blob (extension_name:string)
+                         (s:string)
+                         (blob_range:range)
+                         (extension_syntax_start:range) : FStar_Parser_AST.decl' =
+    DeclSyntaxExtension (extension_name, s, blob_range, extension_syntax_start)
 %}
 
 %token <string> STRING
@@ -117,7 +120,7 @@ let parse_extension_blob (extension_name:string) (s:string) r : FStar_Parser_AST
 
 %token<string>  OPPREFIX OPINFIX0a OPINFIX0b OPINFIX0c OPINFIX0d OPINFIX1 OPINFIX2 OPINFIX3 OPINFIX4
 %token<string>  OP_MIXFIX_ASSIGNMENT OP_MIXFIX_ACCESS
-%token<string * string * Lexing.position>  BLOB
+%token<string * string * Lexing.position * FStar_Sedlexing.snap>  BLOB
 
 /* These are artificial */
 %token EOF
@@ -145,7 +148,7 @@ let parse_extension_blob (extension_name:string) (s:string) r : FStar_Parser_AST
 %start warn_error_list
 %start oneDeclOrEOF
 %type <FStar_Parser_AST.inputFragment> inputFragment
-%type <FStar_Parser_AST.decl option> oneDeclOrEOF
+%type <(FStar_Parser_AST.decl * FStar_Sedlexing.snap option) option> oneDeclOrEOF
 %type <FStar_Parser_AST.term> term
 %type <FStar_Ident.ident> lident
 %type <(FStar_Errors_Codes.error_flag * string) list> warn_error_list
@@ -160,37 +163,38 @@ inputFragment:
 
 oneDeclOrEOF:
   | EOF { None }
-  | d=idecl { Some d }
+  | ds=idecl { Some ds }
 
 idecl:
- | d=decl startOfNextDeclToken
-     { d }
+ | d=decl snap=startOfNextDeclToken
+     { d, snap }
 
 
 startOfNextDeclToken:
- | EOF    { () }
- | pragmaStartToken { () }
- | LBRACK_AT { () } (* Attribute start *)
- | LBRACK_AT_AT { () } (* Attribute start *) 
- | qualifier { () }
- | CLASS { () }
- | INSTANCE { () }
- | OPEN  { () }
- | FRIEND  { () }
- | INCLUDE  { () }
- | MODULE  { () }
- | TYPE  { () }
- | EFFECT  { () }
- | LET  { () }
- | VAL  { () }
- | SPLICE  { () }
- | SPLICET  { () }
- | EXCEPTION  { () }
- | NEW_EFFECT  { () }
- | LAYERED_EFFECT  { () }
- | SUB_EFFECT { () }
- | POLYMONADIC_BIND  { () }
- | POLYMONADIC_SUBCOMP  { () }
+ | EOF    { None }
+ | pragmaStartToken { None }
+ | LBRACK_AT { None } (* Attribute start *)
+ | LBRACK_AT_AT { None } (* Attribute start *) 
+ | qualifier { None }
+ | CLASS { None }
+ | INSTANCE { None }
+ | OPEN  { None }
+ | FRIEND  { None }
+ | INCLUDE  { None }
+ | MODULE  { None }
+ | TYPE  { None }
+ | EFFECT  { None }
+ | LET  { None }
+ | VAL  { None }
+ | SPLICE  { None }
+ | SPLICET  { None }
+ | EXCEPTION  { None }
+ | NEW_EFFECT  { None }
+ | LAYERED_EFFECT  { None }
+ | SUB_EFFECT { None }
+ | POLYMONADIC_BIND  { None }
+ | POLYMONADIC_SUBCOMP  { None }
+ | b=BLOB { let _, _, _, snap = b in Some snap }
 
 
 pragmaStartToken:
@@ -343,8 +347,13 @@ rawDecl:
       { Polymonadic_subcomp c }
   | blob=BLOB
       {
-        let ext_name, contents, pos = blob in
-        parse_extension_blob ext_name contents (rr (pos, pos))
+        let ext_name, contents, pos, snap = blob in
+        (* blob_range is the full range of the blob, including the enclosing ``` *)
+        let blob_range = rr (snd snap, snd $loc) in
+        (* extension_syntax_start_range is where the extension syntax starts not incluing
+           the "```ident" prefix *)
+        let extension_syntax_start_range = (rr (pos, pos)) in
+        parse_extension_blob ext_name contents blob_range extension_syntax_start_range
       }
 
 

ocaml/fstar-lib/FStar_Parser_ParseIt.ml

@@ -248,7 +248,7 @@ let parse fn =
         in
         match d with
         | Inl None -> List.rev decls, None
-        | Inl (Some d) -> 
+        | Inl (Some (d, snap_opt)) -> 
           (* The parser may advance the lexer beyond the decls last token.
              E.g., in `let f x = 0 let g = 1`, we will have parsed the decl for `f`
                    but the lexer will have advanced to `let ^ g ...` since the
@@ -257,20 +257,21 @@ let parse fn =
                    requires such lookahead to complete a production.
           *)
           let end_pos =
-              rollback lexbuf;
-              current_pos lexbuf
+            let _ = 
+              match snap_opt with
+              | None -> 
+                rollback lexbuf
+              | Some p -> 
+                restore_snapshot lexbuf p
+            in
+            current_pos lexbuf
           in
           let raw_contents = contents_at d.drange in
-          (*
           if FStar_Options.debug_any()
-          then (
-            FStar_Compiler_Util.print4 "Parsed decl@%s=%s\nRaw contents@%s=%s\n"
-              (FStar_Compiler_Range.string_of_def_range d.drange)
-              (FStar_Parser_AST.decl_to_string d)
-              (FStar_Compiler_Range.string_of_def_range raw_contents.range)
-              raw_contents.code
-          );
-          *)
+          then 
+            FStar_Compiler_Util.print2 "At range %s, got code\n%s\n"
+              (FStar_Compiler_Range.string_of_range raw_contents.range)
+              (raw_contents.code);
           parse ((d, raw_contents)::decls)
         | Inr err -> List.rev decls, Some err
       in

ocaml/fstar-lib/FStar_Sedlexing.ml

@@ -72,6 +72,13 @@ let backtrack b =
   b.cur_p <- b.mark_p;
   b.mark_val
 
+type snap = int * pos
+
+let snapshot b = b.start, b.start_p
+let restore_snapshot b (cur, cur_p) =
+  b.cur <- cur;
+  b.cur_p <- cur_p
+
 let next b =
   if b.cur = b.len then None
   else