diff --git a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml b/ocaml/fstar-lib/FStar_Parser_ParseIt.ml index 8913c92cd6a..e12b09fb32f 100644 --- a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml +++ b/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) diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 903db479548..882e8a733d2 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -83,7 +83,7 @@ let (uu___is_Valid : tc_result_t -> Prims.bool) = fun projectee -> match projectee with | Valid _0 -> true | uu___ -> false let (__proj__Valid__item___0 : tc_result_t -> Prims.string) = fun projectee -> match projectee with | Valid _0 -> _0 -let (uu___46 : tc_result_t FStar_Class_Show.showable) = +let (uu___44 : tc_result_t FStar_Class_Show.showable) = { FStar_Class_Show.show = (fun uu___ -> diff --git a/ocaml/fstar-lib/generated/FStar_Errors.ml b/ocaml/fstar-lib/generated/FStar_Errors.ml index 02a3a9fc4b4..0c823af9be4 100644 --- a/ocaml/fstar-lib/generated/FStar_Errors.ml +++ b/ocaml/fstar-lib/generated/FStar_Errors.ml @@ -755,7 +755,7 @@ let (set_option_warning_callback_range : FStar_Compiler_Range_Type.range FStar_Pervasives_Native.option -> unit) = fun ropt -> FStar_Options.set_option_warning_callback (warn_unsafe_options ropt) -let (uu___390 : +let (uu___389 : (((Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) * (unit -> FStar_Errors_Codes.error_setting Prims.list))) = @@ -801,10 +801,10 @@ let (uu___390 : (set_callbacks, get_error_flags) let (t_set_parse_warn_error : (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) = - match uu___390 with + match uu___389 with | (t_set_parse_warn_error1, error_flags) -> t_set_parse_warn_error1 let (error_flags : unit -> FStar_Errors_Codes.error_setting Prims.list) = - match uu___390 with + match uu___389 with | (t_set_parse_warn_error1, error_flags1) -> error_flags1 let (set_parse_warn_error : (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index 845a92f0cb0..58364a35728 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -406,7 +406,7 @@ let (init : unit -> unit) = FStar_Compiler_List.iter set_option' defaults let (clear : unit -> unit) = fun uu___ -> FStar_Compiler_Effect.op_Colon_Equals history [[]]; init () -let (uu___154 : unit) = clear () +let (uu___145 : unit) = clear () let (get_option : Prims.string -> option_val) = fun s -> let uu___ = @@ -997,7 +997,7 @@ let (interp_quake_arg : Prims.string -> (Prims.int * Prims.int * Prims.bool)) let uu___ = ios f1 in let uu___1 = ios f2 in (uu___, uu___1, true) else FStar_Compiler_Effect.failwith "unexpected value for --quake" | uu___ -> FStar_Compiler_Effect.failwith "unexpected value for --quake" -let (uu___451 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) +let (uu___442 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) = let cb = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None in let set1 f = @@ -1009,11 +1009,11 @@ let (uu___451 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) | FStar_Pervasives_Native.Some f -> f msg in (set1, call) let (set_option_warning_callback_aux : (Prims.string -> unit) -> unit) = - match uu___451 with + match uu___442 with | (set_option_warning_callback_aux1, option_warning_callback) -> set_option_warning_callback_aux1 let (option_warning_callback : Prims.string -> unit) = - match uu___451 with + match uu___442 with | (set_option_warning_callback_aux1, option_warning_callback1) -> option_warning_callback1 let (set_option_warning_callback : (Prims.string -> unit) -> unit) = @@ -2113,7 +2113,7 @@ let rec (specs_with_types : = let uu___144 = - let uu___145 + let uu___146 = text "Print full names (deprecated; use --print_full_names instead)" in @@ -2122,13 +2122,13 @@ let rec (specs_with_types : (Const (Bool true)), - uu___145) in - let uu___145 - = + uu___146) in let uu___146 = let uu___147 = + let uu___148 + = text "Proof recovery mode: before failing an SMT query, retry 3 times, increasing rlimits. If the query goes through after retrying, verification will succeed, but a warning will be emitted. This feature is useful to restore a project after some change to its libraries or F* upgrade. Importantly, then, this option cannot be used in a pragma (#set-options, etc)." in (FStar_Getopt.noshort, @@ -2136,23 +2136,23 @@ let rec (specs_with_types : (Const (Bool true)), - uu___147) in - let uu___147 - = + uu___148) in let uu___148 = let uu___149 = let uu___150 = - text - "Repeats SMT queries to check for robustness" in let uu___151 = + text + "Repeats SMT queries to check for robustness" in let uu___152 = let uu___153 = + let uu___154 + = let uu___155 = text @@ -2186,33 +2186,33 @@ let rec (specs_with_types : :: uu___156 in FStar_Errors_Msg.bulleted - uu___153 in - let uu___153 + uu___154 in + let uu___154 = text "Using --quake disables --retry. When quake testing, queries are not splitted for error reporting unless '--split_queries always' is given. Queries from the smt_sync tactic are not quake-tested." in FStar_Pprint.op_Hat_Hat - uu___152 - uu___153 in + uu___153 + uu___154 in FStar_Pprint.op_Hat_Hat - uu___150 - uu___151 in + uu___151 + uu___152 in (FStar_Getopt.noshort, "quake", (PostProcessed ((fun - uu___150 + uu___151 -> - match uu___150 + match uu___151 with | String s -> - let uu___151 + let uu___152 = interp_quake_arg s in - (match uu___151 + (match uu___152 with | (min, @@ -2233,19 +2233,19 @@ let rec (specs_with_types : false); String s)) | - uu___151 + uu___152 -> FStar_Compiler_Effect.failwith "impos"), (SimpleStr "positive integer or pair of positive integers"))), - uu___149) in - let uu___149 - = + uu___150) in let uu___150 = let uu___151 = + let uu___152 + = text "Keep a running cache of SMT queries to make verification faster. Only available in the interactive mode. NOTE: This feature is experimental and potentially unsound! Hence why\n it is not allowed in batch mode (where it is also less useful). If you\n find a query that is mistakenly accepted with the cache, please\n report a bug to the F* issue tracker on GitHub." in (FStar_Getopt.noshort, @@ -2253,13 +2253,13 @@ let rec (specs_with_types : (Const (Bool true)), - uu___151) in - let uu___151 - = + uu___152) in let uu___152 = let uu___153 = + let uu___154 + = text "Print SMT query statistics" in (FStar_Getopt.noshort, @@ -2267,8 +2267,8 @@ let rec (specs_with_types : (Const (Bool true)), - uu___153) in - let uu___153 + uu___154) in + let uu___154 = let uu___155 = @@ -3431,21 +3431,21 @@ let rec (specs_with_types : uu___155 :: uu___156 in - uu___152 + uu___153 :: - uu___153 in - uu___150 + uu___154 in + uu___151 :: - uu___151 in - uu___148 + uu___152 in + uu___149 :: - uu___149 in - uu___146 + uu___150 in + uu___147 :: - uu___147 in + uu___148 in uu___144 :: - uu___145 in + uu___146 in uu___142 :: uu___143 in @@ -3724,7 +3724,7 @@ let (settable_specs : (fun uu___ -> match uu___ with | ((uu___1, x, uu___2), uu___3) -> settable x) all_specs -let (uu___672 : +let (uu___669 : (((unit -> FStar_Getopt.parse_cmdline_res) -> unit) * (unit -> FStar_Getopt.parse_cmdline_res))) = @@ -3741,11 +3741,11 @@ let (uu___672 : (set1, call) let (set_error_flags_callback_aux : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = - match uu___672 with + match uu___669 with | (set_error_flags_callback_aux1, set_error_flags) -> set_error_flags_callback_aux1 let (set_error_flags : unit -> FStar_Getopt.parse_cmdline_res) = - match uu___672 with + match uu___669 with | (set_error_flags_callback_aux1, set_error_flags1) -> set_error_flags1 let (set_error_flags_callback : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml index 68bbe5b0212..1ae9c2057db 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml @@ -41,6 +41,8 @@ type term' = | Projector of (FStar_Ident.lid * FStar_Ident.ident) | Construct of (FStar_Ident.lid * (term * imp) Prims.list) | Abs of (pattern Prims.list * term) + | Function of ((pattern * term FStar_Pervasives_Native.option * term) + Prims.list * FStar_Compiler_Range_Type.range) | App of (term * term * imp) | Let of (let_qualifier * (term Prims.list FStar_Pervasives_Native.option * (pattern * term)) Prims.list * term) @@ -191,6 +193,14 @@ let (uu___is_Abs : term' -> Prims.bool) = fun projectee -> match projectee with | Abs _0 -> true | uu___ -> false let (__proj__Abs__item___0 : term' -> (pattern Prims.list * term)) = fun projectee -> match projectee with | Abs _0 -> _0 +let (uu___is_Function : term' -> Prims.bool) = + fun projectee -> + match projectee with | Function _0 -> true | uu___ -> false +let (__proj__Function__item___0 : + term' -> + ((pattern * term FStar_Pervasives_Native.option * term) Prims.list * + FStar_Compiler_Range_Type.range)) + = fun projectee -> match projectee with | Function _0 -> _0 let (uu___is_App : term' -> Prims.bool) = fun projectee -> match projectee with | App _0 -> true | uu___ -> false let (__proj__App__item___0 : term' -> (term * term * imp)) = @@ -1170,29 +1180,7 @@ let (mk_function : FStar_Compiler_Range_Type.range -> term) = fun branches -> - fun r1 -> - fun r2 -> - let x = FStar_Ident.gen r1 in - let uu___ = - let uu___1 = - let uu___2 = - let uu___3 = - mk_pattern (PatVar (x, FStar_Pervasives_Native.None, [])) r1 in - [uu___3] in - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = FStar_Ident.lid_of_ids [x] in Var uu___8 in - mk_term uu___7 r1 Expr in - (uu___6, FStar_Pervasives_Native.None, - FStar_Pervasives_Native.None, branches) in - Match uu___5 in - mk_term uu___4 r2 Expr in - (uu___2, uu___3) in - Abs uu___1 in - mk_term uu___ r2 Expr + fun r1 -> fun r2 -> mk_term (Function (branches, r1)) r2 Expr let (un_function : pattern -> term -> (pattern * term) FStar_Pervasives_Native.option) = fun p -> @@ -1935,6 +1923,17 @@ let rec (term_to_string : term -> Prims.string) = FStar_Compiler_Util.format2 "%s%s" (imp_to_string imp1) uu___3) args in FStar_Compiler_Util.format2 "(%s %s)" uu___ uu___1 + | Function (branches, r) -> + let uu___ = + to_string_l " | " + (fun uu___1 -> + match uu___1 with + | (p, w, e) -> + let uu___2 = pat_to_string p in + let uu___3 = term_to_string e in + FStar_Compiler_Util.format2 "%s -> %s" uu___2 uu___3) + branches in + FStar_Compiler_Util.format1 "(function %s)" uu___ | Abs (pats, t) -> let uu___ = to_string_l " " pat_to_string pats in let uu___1 = term_to_string t in diff --git a/ocaml/fstar-lib/generated/FStar_Parser_AST_Util.ml b/ocaml/fstar-lib/generated/FStar_Parser_AST_Util.ml index bd2e385b862..24f4c127581 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_AST_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_AST_Util.ml @@ -169,6 +169,8 @@ and (eq_term' : | (FStar_Parser_AST.Construct (l1, args1), FStar_Parser_AST.Construct (l2, args2)) -> (FStar_Ident.lid_equals l1 l2) && (eq_args args1 args2) + | (FStar_Parser_AST.Function (brs1, _r1), FStar_Parser_AST.Function + (brs2, _r2)) -> eq_list eq_branch brs1 brs2 | (FStar_Parser_AST.Abs (ps1, t11), FStar_Parser_AST.Abs (ps2, t21)) -> (eq_list eq_pattern ps1 ps2) && (eq_term t11 t21) | (FStar_Parser_AST.App (h1, t11, i1), FStar_Parser_AST.App @@ -692,6 +694,8 @@ and (lidents_of_term' : (fun uu___1 -> match uu___1 with | (t1, uu___2) -> lidents_of_term t1) ts in lid :: uu___ + | FStar_Parser_AST.Function (brs, uu___) -> + (concat_map ()) lidents_of_branch brs | FStar_Parser_AST.Abs (ps, t1) -> let uu___ = (concat_map ()) lidents_of_pattern ps in let uu___1 = lidents_of_term t1 in diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index a299876e169..62f521bc168 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -1570,6 +1570,8 @@ let (collect_one : (fun uu___3 -> match uu___3 with | (t, uu___4) -> collect_term t) termimps) + | FStar_Parser_AST.Function (branches, uu___2) -> + collect_branches branches | FStar_Parser_AST.Abs (pats, t) -> (collect_patterns pats; collect_term t) | FStar_Parser_AST.App (t1, t2, uu___2) -> diff --git a/ocaml/fstar-lib/generated/FStar_Parser_ToDocument.ml b/ocaml/fstar-lib/generated/FStar_Parser_ToDocument.ml index 2c2022ec9dd..b0aaa84f7ad 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_ToDocument.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_ToDocument.ml @@ -2989,27 +2989,6 @@ and (p_noSeqTerm' : FStar_Pprint.op_Hat_Hat lbs_doc uu___2 in FStar_Pprint.group uu___1 in let uu___1 = paren_if ps in uu___1 uu___ - | FStar_Parser_AST.Abs - ({ - FStar_Parser_AST.pat = FStar_Parser_AST.PatVar - (x, typ_opt, uu___); - FStar_Parser_AST.prange = uu___1;_}::[], - { - FStar_Parser_AST.tm = FStar_Parser_AST.Match - (maybe_x, FStar_Pervasives_Native.None, - FStar_Pervasives_Native.None, branches); - FStar_Parser_AST.range = uu___2; - FStar_Parser_AST.level = uu___3;_}) - when matches_var maybe_x x -> - let uu___4 = - let uu___5 = - let uu___6 = str "function" in - let uu___7 = - separate_map_last FStar_Pprint.hardline p_patternBranch - branches in - FStar_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in - FStar_Pprint.group uu___5 in - let uu___5 = paren_if (ps || pb) in uu___5 uu___4 | FStar_Parser_AST.Quote (e1, FStar_Parser_AST.Dynamic) -> let uu___ = let uu___1 = str "quote" in @@ -3852,6 +3831,16 @@ and (p_simpleTerm : fun pb -> fun e -> match e.FStar_Parser_AST.tm with + | FStar_Parser_AST.Function (branches, uu___) -> + let uu___1 = + let uu___2 = + let uu___3 = str "function" in + let uu___4 = + separate_map_last FStar_Pprint.hardline p_patternBranch + branches in + FStar_Pprint.op_Hat_Slash_Hat uu___3 uu___4 in + FStar_Pprint.group uu___2 in + let uu___2 = paren_if (ps || pb) in uu___2 uu___1 | FStar_Parser_AST.Abs (pats, e1) -> let uu___ = p_term_sep false pb e1 in (match uu___ with diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index efb00c37a1a..1a224001856 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -1371,7 +1371,7 @@ let (ans_fail : answer) = tried_recovery = (ans_ok.tried_recovery); errs = (ans_ok.errs) } -let (uu___556 : answer FStar_Class_Show.showable) = +let (uu___555 : answer FStar_Class_Show.showable) = { FStar_Class_Show.show = (fun ans -> diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 3e29eebe6e6..164a69cf412 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -685,6 +685,7 @@ and (free_vars : | FStar_Parser_AST.SeqLiteral ts -> FStar_Compiler_List.collect (free_vars tvars_only env) ts | FStar_Parser_AST.Abs uu___1 -> [] + | FStar_Parser_AST.Function uu___1 -> [] | FStar_Parser_AST.Let uu___1 -> [] | FStar_Parser_AST.LetOpen uu___1 -> [] | FStar_Parser_AST.If uu___1 -> [] @@ -3099,6 +3100,36 @@ and (desugar_term_maybe_top : b2.FStar_Syntax_Syntax.binder_bv f1 in setpos uu___5 in (uu___4, noaqs))) + | FStar_Parser_AST.Function (branches, r1) -> + let x = FStar_Ident.gen r1 in + let t' = + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Parser_AST.mk_pattern + (FStar_Parser_AST.PatVar + (x, FStar_Pervasives_Native.None, [])) r1 in + [uu___5] in + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + let uu___9 = + let uu___10 = FStar_Ident.lid_of_ids [x] in + FStar_Parser_AST.Var uu___10 in + FStar_Parser_AST.mk_term uu___9 r1 + FStar_Parser_AST.Expr in + (uu___8, FStar_Pervasives_Native.None, + FStar_Pervasives_Native.None, branches) in + FStar_Parser_AST.Match uu___7 in + FStar_Parser_AST.mk_term uu___6 + top.FStar_Parser_AST.range FStar_Parser_AST.Expr in + (uu___4, uu___5) in + FStar_Parser_AST.Abs uu___3 in + FStar_Parser_AST.mk_term uu___2 top.FStar_Parser_AST.range + FStar_Parser_AST.Expr in + desugar_term_maybe_top top_level env t' | FStar_Parser_AST.Abs (binders, body) -> let bvss = FStar_Compiler_List.map gather_pattern_bound_vars binders in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 43f93a08a9b..cd53629dc1d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -170,7 +170,7 @@ let (uu___is_DeferAny : defer_ok_t -> Prims.bool) = let (uu___is_DeferFlexFlexOnly : defer_ok_t -> Prims.bool) = fun projectee -> match projectee with | DeferFlexFlexOnly -> true | uu___ -> false -let (uu___85 : defer_ok_t FStar_Class_Show.showable) = +let (uu___52 : defer_ok_t FStar_Class_Show.showable) = { FStar_Class_Show.show = (fun uu___ -> @@ -8163,7 +8163,7 @@ and (solve_t_flex_flex : let uu___23 = let uu___24 = FStar_Class_Show.show - uu___85 + uu___52 wl.defer_ok in FStar_Compiler_Util.format1 "flex-flex: occurs\n defer_ok=%s\n" @@ -14752,7 +14752,7 @@ let (try_solve_deferred_constraints : (let uu___4 = FStar_Compiler_Effect.op_Bang dbg_Rel in if uu___4 then - let uu___5 = FStar_Class_Show.show uu___85 defer_ok in + let uu___5 = FStar_Class_Show.show uu___52 defer_ok in let uu___6 = FStar_Class_Show.show (FStar_Class_Show.printableshow diff --git a/src/parser/FStar.Parser.AST.Util.fst b/src/parser/FStar.Parser.AST.Util.fst index 806f5babb18..5f1241370c0 100644 --- a/src/parser/FStar.Parser.AST.Util.fst +++ b/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 diff --git a/src/parser/FStar.Parser.AST.fst b/src/parser/FStar.Parser.AST.fst index 7d6382d6a92..bde493644ac 100644 --- a/src/parser/FStar.Parser.AST.fst +++ b/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) diff --git a/src/parser/FStar.Parser.AST.fsti b/src/parser/FStar.Parser.AST.fsti index c12da790f1a..6cc7869e6c2 100644 --- a/src/parser/FStar.Parser.AST.fsti +++ b/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 diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index f8a94e825fa..39f95fb6c29 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/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 diff --git a/src/parser/FStar.Parser.ToDocument.fst b/src/parser/FStar.Parser.ToDocument.fst index 8cc6bacb89a..11431e738fb 100644 --- a/src/parser/FStar.Parser.ToDocument.fst +++ b/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 diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 509709c0314..cf27f0ca66e 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/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