Ide fixes

ocaml/fstar-lib/FStar_Parser_ParseIt.ml

@@ -158,10 +158,13 @@ let parse_incremental_decls
     let start_pos = current_pos lexbuf in
     let d =
       try
-        (* Reset the gensym between decls, to ensure determinism, 
-            otherwise, every _ is parsed as different name *)
-        FStar_GenSym.reset_gensym();
-        Inl (parse_one lexer)
+        (* Reset the gensym before parsing decls, to ensure determinism,
+            otherwise, every _ is parsed as different name. However, make
+            sure to not affect the external state. *)
+        FStar_GenSym.with_frozen_gensym (fun () ->
+          FStar_GenSym.reset_gensym();
+          Inl (parse_one lexer)
+        )
       with 
       | FStar_Errors.Error(e, msg, r, ctx) ->
         Inr (e, msg, r)

src/parser/FStar.Parser.AST.Util.fst

@@ -164,6 +164,8 @@ and eq_term' (t1 t2:term')
     | Construct (l1, args1), Construct (l2, args2) ->
       Ident.lid_equals l1 l2 &&
       eq_args args1 args2
+    | Function (brs1, _r1), Function (brs2, _r2) ->
+      eq_list eq_branch brs1 brs2
     | Abs (ps1, t1), Abs (ps2, t2) ->
       eq_list eq_pattern ps1 ps2 &&
       eq_term t1 t2
@@ -600,6 +602,7 @@ and lidents_of_term' (t:term')
   | Name lid -> [lid]
   | Projector (lid, _) -> [lid]
   | Construct (lid, ts) -> lid :: concat_map (fun (t, _) -> lidents_of_term t) ts
+  | Function (brs, _) -> concat_map lidents_of_branch brs
   | Abs (ps, t) -> concat_map lidents_of_pattern ps @ lidents_of_term t
   | App (t1, t2, _) -> lidents_of_term t1 @ lidents_of_term t2
   | Let (_, lbs, t) -> concat_map (fun (_, (p, t)) -> lidents_of_pattern p @ lidents_of_term t) lbs @ lidents_of_term t

src/parser/FStar.Parser.AST.fst

@@ -61,10 +61,8 @@ let un_curry_abs ps body = match body.tm with
     | Abs(p', body') -> Abs(ps@p', body')
     | _ -> Abs(ps, body)
 let mk_function branches r1 r2 =
-  let x = Ident.gen r1 in
-  mk_term (Abs([mk_pattern (PatVar(x,None,[])) r1],
-               mk_term (Match(mk_term (Var(lid_of_ids [x])) r1 Expr, None, None, branches)) r2 Expr))
-    r2 Expr
+  mk_term (Function (branches, r1)) r2 Expr
+
 let un_function p tm = match p.pat, tm.tm with
     | PatVar _, Abs(pats, body) -> Some (mk_pattern (PatApp(p, pats)) p.prange, body)
     | _ -> None
@@ -409,6 +407,12 @@ let rec term_to_string (x:term) = match x.tm with
 
   | Construct (l, args) ->
     Util.format2 "(%s %s)" (string_of_lid l) (to_string_l " " (fun (a,imp) -> Util.format2 "%s%s" (imp_to_string imp) (term_to_string a)) args)
+  | Function (branches, r) ->
+    Util.format1 "(function %s)"
+      (to_string_l " | " (fun (p,w,e) -> Util.format2 "%s -> %s"
+        (p |> pat_to_string)
+        (e |> term_to_string)) branches)
+
   | Abs(pats, t) ->
     Util.format2 "(fun %s -> %s)" (to_string_l " " pat_to_string pats) (t|> term_to_string)
   | App(t1, t2, imp) -> Util.format3 "%s %s%s" (t1|> term_to_string) (imp_to_string imp) (t2|> term_to_string)

src/parser/FStar.Parser.AST.fsti

@@ -50,7 +50,8 @@ type term' =
                                 followed by one  of its actions or
                                 "fields" *)
   | Construct of lid & list (term&imp)               (* data, type: bool in each arg records an implicit *)
-  | Abs       of list pattern & term
+  | Abs       of list pattern & term                 (* fun p1 p2 .. pn -> body *)
+  | Function  of list branch & range                 (* function | p1 -> e1 | ... | pn -> en; range is for binder *)
   | App       of term & term & imp                    (* aqual marks an explicitly provided implicit parameter *)
   | Let       of let_qualifier & list (option attributes_ & (pattern & term)) & term
   | LetOperator   of list (ident & pattern & term) & term

src/parser/FStar.Parser.Dep.fst

@@ -961,6 +961,8 @@ let collect_one
         | Construct (lid, termimps) ->
             add_to_parsing_data (P_lid lid);
             List.iter (fun (t, _) -> collect_term t) termimps
+        | Function (branches, _) ->
+          collect_branches branches
         | Abs (pats, t) ->
             collect_patterns pats;
             collect_term t

src/parser/FStar.Parser.ToDocument.fst

@@ -1466,9 +1466,6 @@ and p_noSeqTerm' ps pb e = match e.tm with
     let lbs_doc = group (separate break1 lbs_docs) in
     paren_if ps (group (lbs_doc ^^ hardline ^^ p_term false pb e))
 
-  | Abs([{pat=PatVar(x, typ_opt, _)}], {tm=Match(maybe_x, None, None, branches)}) when matches_var maybe_x x ->
-    paren_if (ps || pb) (
-      group (str "function" ^/^ separate_map_last hardline p_patternBranch branches))
   | Quote (e, Dynamic) ->
     group (str "quote" ^/^ p_noSeqTermAndComment ps pb e)
   | Quote (e, Static) ->
@@ -1696,6 +1693,10 @@ and p_conjunctivePats pats =
     group (separate_map (semi ^^ break1) p_appTerm pats)
 
 and p_simpleTerm ps pb e = match e.tm with
+    | Function(branches, _) ->
+      paren_if (ps || pb) (
+        group (str "function" ^/^ separate_map_last hardline p_patternBranch branches))
+
     | Abs(pats, e) ->
         let comm, doc = p_term_sep false pb e in
         let prefix = str "fun" ^/+^ separate_map break1 p_atomicPattern pats ^/^ rarrow in

src/tosyntax/FStar.ToSyntax.ToSyntax.fst

@@ -439,6 +439,7 @@ and free_vars tvars_only env t = match (unparen t).tm with
     List.collect (free_vars tvars_only env) ts
 
   | Abs _  (* not closing implicitly over free vars in all these forms: TODO: Fixme! *)
+  | Function _
   | Let _
   | LetOpen _
   | If _
@@ -1402,6 +1403,15 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an
           setpos <| U.refine b.binder_bv f, noaqs
       end
 
+    | Function (branches, r1) ->
+      let x = Ident.gen r1 in
+      let t' =
+        mk_term (Abs([mk_pattern (PatVar(x,None,[])) r1],
+                   mk_term (Match(mk_term (Var(lid_of_ids [x])) r1 Expr, None, None, branches)) top.range Expr))
+        top.range Expr
+      in
+      desugar_term_maybe_top top_level env t'
+
     | Abs(binders, body) ->
       (* First of all, forbid definitions such as `f x x = ...` *)
       let bvss = List.map gather_pattern_bound_vars binders in