From 3f7a99984895c904d10a2c1c6908dfe42f73a667 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 28 Jun 2023 17:01:54 -0700 Subject: [PATCH 1/9] tc: print sigelt (in short form) for --timing/--profile This allows to distinguish a `val x` from a `let x`, and is in general clearer at the cost of not much more verbosity. --- src/typechecker/FStar.TypeChecker.Tc.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index 3c6cadcb5c5..55c08b6fcd5 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -1075,7 +1075,7 @@ let tc_decls env ses = let r = Profiling.profile (fun () -> process_one_decl acc se) - (Some (Ident.string_of_lid (Env.current_module env))) + (Some (Print.sigelt_to_string_short se)) "FStar.TypeChecker.Tc.process_one_decl" // ^ See a special case for this phase in FStar.Options. --timing // enables it. From 1b9961ae54d04d9262502929683bf29bf6b7c36d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 28 Jun 2023 17:01:42 -0700 Subject: [PATCH 2/9] tc: rel: slightly improving norm call, short-circuit --- src/typechecker/FStar.TypeChecker.Rel.fst | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 59112e849c5..03941ba651a 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -4146,9 +4146,15 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = (string_of_bool (Env.is_interpreted wl.tcenv head2)); (string_of_bool (no_free_uvars t2))] in - let equal t1 t2 = - (U.eq_tm t1 t2 = U.Equal) || - (let steps = [ + let equal t1 t2 : bool = + (* Try comparing the terms as they are. If we get Equal or NotEqual, + we are done. If we get an Unknown, attempt some normalization. *) + let r = U.eq_tm t1 t2 in + match r with + | U.Equal -> true + | U.NotEqual -> false + | U.Unknown -> + let steps = [ Env.UnfoldUntil delta_constant; Env.Primops; Env.Beta; @@ -4157,7 +4163,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = let env = p_env wl orig in let t1 = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.2" steps env t1 in let t2 = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.3" steps env t2 in - U.eq_tm t1 t2 = U.Equal) + U.eq_tm t1 t2 = U.Equal in if (Env.is_interpreted wl.tcenv head1 || Env.is_interpreted wl.tcenv head2) //we have something like (+ x1 x2) =?= (- y1 y2) && problem.relation = EQ From 0d9594ae5a1608a8bcd82fc867812db8abafdd45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 29 Jun 2023 08:53:35 -0700 Subject: [PATCH 3/9] snap --- .../generated/FStar_TypeChecker_Rel.ml | 516 ++++++++++-------- .../generated/FStar_TypeChecker_Tc.ml | 4 +- 2 files changed, 277 insertions(+), 243 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 0c3aa12e1fe..8df40492563 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -10176,26 +10176,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10309,26 +10312,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10442,26 +10448,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10575,26 +10584,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10708,26 +10720,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10841,26 +10856,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -10974,26 +10992,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -11107,26 +11128,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -11240,26 +11264,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -11373,26 +11400,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -11506,26 +11536,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) @@ -11639,26 +11672,29 @@ and (solve_t' : tprob -> worklist -> solution) = uu___11 else ()); (let equal t11 t21 = - (let uu___10 = FStar_Syntax_Util.eq_tm t11 t21 in - uu___10 = FStar_Syntax_Util.Equal) || - (let steps = - [FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota] in - let env = p_env wl orig in - let t12 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.2" steps - env t11 in - let t22 = - norm_with_steps - "FStar.TypeChecker.Rel.norm_with_steps.3" steps - env t21 in - let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in - uu___10 = FStar_Syntax_Util.Equal) in + let r = FStar_Syntax_Util.eq_tm t11 t21 in + match r with + | FStar_Syntax_Util.Equal -> true + | FStar_Syntax_Util.NotEqual -> false + | FStar_Syntax_Util.Unknown -> + let steps = + [FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Eager_unfolding; + FStar_TypeChecker_Env.Iota] in + let env = p_env wl orig in + let t12 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.2" steps + env t11 in + let t22 = + norm_with_steps + "FStar.TypeChecker.Rel.norm_with_steps.3" steps + env t21 in + let uu___10 = FStar_Syntax_Util.eq_tm t12 t22 in + uu___10 = FStar_Syntax_Util.Equal in let uu___10 = ((FStar_TypeChecker_Env.is_interpreted wl.tcenv head1) || (FStar_TypeChecker_Env.is_interpreted wl.tcenv head2)) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index 90dcfcc8ea7..0203f77c874 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -4715,9 +4715,7 @@ let (tc_decls : | (uu___2, env1) -> let r = let uu___3 = - let uu___4 = - let uu___5 = FStar_TypeChecker_Env.current_module env1 in - FStar_Ident.string_of_lid uu___5 in + let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in FStar_Pervasives_Native.Some uu___4 in FStar_Profiling.profile (fun uu___4 -> process_one_decl acc se) uu___3 From 765fcb37ab8ab6a2bc9e4992b0be28c7931b359f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Weng=20Shiwei=20=E7=BF=81=E5=A3=AB=E4=BC=9F?= Date: Fri, 30 Jun 2023 16:10:34 -0400 Subject: [PATCH 4/9] Update part1_termination.rst unify subscripts --- doc/book/part1/part1_termination.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/book/part1/part1_termination.rst b/doc/book/part1/part1_termination.rst index 1a0ce4277ee..220a668c664 100755 --- a/doc/book/part1/part1_termination.rst +++ b/doc/book/part1/part1_termination.rst @@ -65,7 +65,7 @@ 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. @@ -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. From e1dad08248bd2b031098b12ab199f844a097fdb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Weng=20Shiwei=20=E7=BF=81=E5=A3=AB=E4=BC=9F?= Date: Fri, 30 Jun 2023 16:23:49 -0400 Subject: [PATCH 5/9] Update part1_termination.rst --- doc/book/part1/part1_termination.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/book/part1/part1_termination.rst b/doc/book/part1/part1_termination.rst index 220a668c664..89c0055a160 100755 --- a/doc/book/part1/part1_termination.rst +++ b/doc/book/part1/part1_termination.rst @@ -72,7 +72,7 @@ if any of the following are true: 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 From 4e2cf19cc01305bdf326317f75b8d535959c3591 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 3 Jul 2023 13:05:37 -0700 Subject: [PATCH 6/9] Fixing incremental parsing of syntax extensions (need to rewind the lexer properly) --- ocaml/fstar-lib/FStar_Parser_LexFStar.ml | 11 ++-- ocaml/fstar-lib/FStar_Parser_Parse.mly | 59 ++++++++++--------- ocaml/fstar-lib/FStar_Parser_ParseIt.ml | 22 +++---- ocaml/fstar-lib/FStar_Sedlexing.ml | 7 +++ ocaml/fstar-lib/generated/FStar_Parser_AST.ml | 3 + .../fstar-tests/generated/FStar_Tests_Pars.ml | 14 ++--- src/parser/FStar.Parser.AST.fst | 2 + src/tests/FStar.Tests.Pars.fst | 16 +++-- 8 files changed, 74 insertions(+), 60 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Parser_LexFStar.ml b/ocaml/fstar-lib/FStar_Parser_LexFStar.ml index 71cb45bd96a..4ea558cc159 100644 --- a/ocaml/fstar-lib/FStar_Parser_LexFStar.ml +++ b/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 = diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index 1147660bcf1..2c508218c06 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/ocaml/fstar-lib/FStar_Parser_Parse.mly @@ -117,7 +117,7 @@ let parse_extension_blob (extension_name:string) (s:string) r : FStar_Parser_AST %token OPPREFIX OPINFIX0a OPINFIX0b OPINFIX0c OPINFIX0d OPINFIX1 OPINFIX2 OPINFIX3 OPINFIX4 %token OP_MIXFIX_ASSIGNMENT OP_MIXFIX_ACCESS -%token BLOB +%token BLOB /* These are artificial */ %token EOF @@ -145,7 +145,7 @@ let parse_extension_blob (extension_name:string) (s:string) r : FStar_Parser_AST %start warn_error_list %start oneDeclOrEOF %type inputFragment -%type oneDeclOrEOF +%type <(FStar_Parser_AST.decl * FStar_Sedlexing.snap option) option> oneDeclOrEOF %type term %type lident %type <(FStar_Errors_Codes.error_flag * string) list> warn_error_list @@ -160,37 +160,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,7 +344,7 @@ rawDecl: { Polymonadic_subcomp c } | blob=BLOB { - let ext_name, contents, pos = blob in + let ext_name, contents, pos, _ = blob in parse_extension_blob ext_name contents (rr (pos, pos)) } diff --git a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml b/ocaml/fstar-lib/FStar_Parser_ParseIt.ml index f169e049e9a..417e8993d7a 100644 --- a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml +++ b/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,16 @@ 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 - ); - *) parse ((d, raw_contents)::decls) | Inr err -> List.rev decls, Some err in diff --git a/ocaml/fstar-lib/FStar_Sedlexing.ml b/ocaml/fstar-lib/FStar_Sedlexing.ml index b0434303dc7..0c1e6baa1f2 100644 --- a/ocaml/fstar-lib/FStar_Sedlexing.ml +++ b/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 diff --git a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml index f46d403f05e..db85444602c 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml @@ -2439,6 +2439,9 @@ let (decl_to_string : decl -> Prims.string) = | SubEffect uu___ -> "sub_effect" | Pragma p -> let uu___ = string_of_pragma p in Prims.op_Hat "pragma #" uu___ + | DeclSyntaxExtension (id, content, uu___) -> + Prims.op_Hat "```" + (Prims.op_Hat id (Prims.op_Hat "\n" (Prims.op_Hat content "\n```"))) let (modul_to_string : modul -> Prims.string) = fun m -> match m with diff --git a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml index 772a1415de6..45729b7a615 100644 --- a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml +++ b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml @@ -635,7 +635,7 @@ let (test_hashes : unit -> unit) = let (parse_incremental_decls : unit -> unit) = fun uu___ -> let source = - "module Demo\nlet f x = match x with | Some x -> true | None -> false\nlet test y = if Some? y then f y else true\nlet some junk )(" in + "module Demo\nlet f x = match x with | Some x -> true | None -> false\nlet test y = if Some? y then f y else true\n```pulse\nfn f() {}\n```\nlet something = more\nlet >< junk" in let input = FStar_Parser_ParseIt.Incremental { @@ -650,14 +650,14 @@ let (parse_incremental_decls : unit -> unit) = ((match parse_err with | FStar_Pervasives_Native.None -> failwith - "Incremental parsing failed: Expected syntax error at (3,15), got no error" + "Incremental parsing failed: Expected syntax error at (7,6), got no error" | FStar_Pervasives_Native.Some (uu___4, uu___5, rng) -> let p = FStar_Compiler_Range_Ops.start_of_range rng in let uu___6 = (let uu___7 = FStar_Compiler_Range_Ops.line_of_pos p in - uu___7 = (Prims.of_int (3))) && + uu___7 = (Prims.of_int (7))) && (let uu___7 = FStar_Compiler_Range_Ops.col_of_pos p in - uu___7 = (Prims.of_int (15))) in + uu___7 = (Prims.of_int (6))) in if uu___6 then () else @@ -669,18 +669,18 @@ let (parse_incremental_decls : unit -> unit) = let uu___11 = FStar_Compiler_Range_Ops.col_of_pos p in FStar_Compiler_Util.string_of_int uu___11 in FStar_Compiler_Util.format2 - "Incremental parsing failed: Expected syntax error at (3,15), got error at (%s, %s)" + "Incremental parsing failed: Expected syntax error at (7,6), got error at (%s, %s)" uu___9 uu___10 in failwith uu___8)); (match decls with - | d0::d1::d2::[] -> () + | d0::d1::d2::d3::d4::[] -> () | uu___4 -> let uu___5 = let uu___6 = FStar_Compiler_Util.string_of_int (FStar_Compiler_List.length decls) in FStar_Compiler_Util.format1 - "Incremental parsing failed; expected 3 decls got %s\n" + "Incremental parsing failed; expected 5 decls got %s\n" uu___6 in failwith uu___5)) | FStar_Parser_ParseIt.ParseError (code, message, range) -> diff --git a/src/parser/FStar.Parser.AST.fst b/src/parser/FStar.Parser.AST.fst index d9b54ec4da0..6236811d8cf 100644 --- a/src/parser/FStar.Parser.AST.fst +++ b/src/parser/FStar.Parser.AST.fst @@ -736,6 +736,8 @@ let decl_to_string (d:decl) = match d.d with ^ (String.concat ";" <| List.map (fun i -> (string_of_id i)) ids) ^ "] (" ^ term_to_string t ^ ")" | SubEffect _ -> "sub_effect" | Pragma p -> "pragma #" ^ string_of_pragma p + | DeclSyntaxExtension (id, content, _) -> + "```" ^ id ^ "\n" ^ content ^ "\n```" let modul_to_string (m:modul) = match m with | Module (_, decls) diff --git a/src/tests/FStar.Tests.Pars.fst b/src/tests/FStar.Tests.Pars.fst index b61b0d7dc8a..5e0040d5acd 100644 --- a/src/tests/FStar.Tests.Pars.fst +++ b/src/tests/FStar.Tests.Pars.fst @@ -201,7 +201,11 @@ let parse_incremental_decls () = "module Demo\n\ let f x = match x with | Some x -> true | None -> false\n\ let test y = if Some? y then f y else true\n\ - let some junk )(" + ```pulse\n\ + fn f() {}\n\ + ```\n\ + let something = more\n\ + let >< junk" in let open FStar.Parser.ParseIt in let input = Incremental { frag_fname = "Demo.fst"; @@ -213,18 +217,18 @@ let parse_incremental_decls () = | IncrementalFragment (decls, _, parse_err) -> ( let _ = match parse_err with | None -> - failwith "Incremental parsing failed: Expected syntax error at (3,15), got no error" + failwith "Incremental parsing failed: Expected syntax error at (7,6), got no error" | Some (_, _, rng) -> let p = start_of_range rng in - if line_of_pos p = 3 && col_of_pos p = 15 + if line_of_pos p = 7 && col_of_pos p = 6 then () - else failwith (format2 "Incremental parsing failed: Expected syntax error at (3,15), got error at (%s, %s)" + else failwith (format2 "Incremental parsing failed: Expected syntax error at (7,6), got error at (%s, %s)" (string_of_int (line_of_pos p)) (string_of_int (col_of_pos p))) in match decls with - | [d0;d1;d2] -> () - | _ -> failwith (format1 "Incremental parsing failed; expected 3 decls got %s\n" + | [d0;d1;d2;d3;d4] -> () + | _ -> failwith (format1 "Incremental parsing failed; expected 5 decls got %s\n" (string_of_int (List.length decls))) ) From 1e7f44834bf704f45a0e5f86c3d380a2074f935c Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 3 Jul 2023 14:20:02 -0700 Subject: [PATCH 7/9] fix ranges of DeclSyntaxExtension, important to get digest checks to match up in vscode --- ocaml/fstar-lib/FStar_Parser_Parse.mly | 16 +++++++++---- ocaml/fstar-lib/FStar_Parser_ParseIt.ml | 5 ++++ ocaml/fstar-lib/generated/FStar_Parser_AST.ml | 16 +++++++++---- .../generated/FStar_ToSyntax_ToSyntax.ml | 24 +++++++++---------- .../fstar-tests/generated/FStar_Tests_Pars.ml | 8 +++---- src/parser/FStar.Parser.AST.fst | 11 +++++++-- src/parser/FStar.Parser.AST.fsti | 4 +++- src/tests/FStar.Tests.Pars.fst | 8 +++---- src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 2 +- 9 files changed, 61 insertions(+), 33 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly index 2c508218c06..88866668ba8 100644 --- a/ocaml/fstar-lib/FStar_Parser_Parse.mly +++ b/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 @@ -344,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 } diff --git a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml b/ocaml/fstar-lib/FStar_Parser_ParseIt.ml index 417e8993d7a..f99e9ee768d 100644 --- a/ocaml/fstar-lib/FStar_Parser_ParseIt.ml +++ b/ocaml/fstar-lib/FStar_Parser_ParseIt.ml @@ -267,6 +267,11 @@ let parse fn = current_pos lexbuf in let raw_contents = contents_at d.drange in + if FStar_Options.debug_any() + 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 diff --git a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml index db85444602c..70c541debda 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml @@ -810,7 +810,7 @@ type decl' = | Assume of (FStar_Ident.ident * term) | Splice of (Prims.bool * FStar_Ident.ident Prims.list * term) | DeclSyntaxExtension of (Prims.string * Prims.string * - FStar_Compiler_Range_Type.range) + FStar_Compiler_Range_Type.range * FStar_Compiler_Range_Type.range) and decl = { d: decl' ; @@ -909,8 +909,10 @@ let (uu___is_DeclSyntaxExtension : decl' -> Prims.bool) = fun projectee -> match projectee with | DeclSyntaxExtension _0 -> true | uu___ -> false let (__proj__DeclSyntaxExtension__item___0 : - decl' -> (Prims.string * Prims.string * FStar_Compiler_Range_Type.range)) = - fun projectee -> match projectee with | DeclSyntaxExtension _0 -> _0 + decl' -> + (Prims.string * Prims.string * FStar_Compiler_Range_Type.range * + FStar_Compiler_Range_Type.range)) + = fun projectee -> match projectee with | DeclSyntaxExtension _0 -> _0 let (__proj__Mkdecl__item__d : decl -> decl') = fun projectee -> match projectee with | { d; drange; quals; attrs;_} -> d let (__proj__Mkdecl__item__drange : decl -> FStar_Compiler_Range_Type.range) @@ -1008,7 +1010,11 @@ let (mk_decl : match uu___ with | Qualifier q -> FStar_Pervasives_Native.Some q | uu___1 -> FStar_Pervasives_Native.None) decorations in - { d; drange = r; quals = qualifiers1; attrs = attributes_2 } + let range = + match d with + | DeclSyntaxExtension (uu___, uu___1, r1, uu___2) -> r1 + | uu___ -> r in + { d; drange = range; quals = qualifiers1; attrs = attributes_2 } let (mk_binder_with_attrs : binder' -> FStar_Compiler_Range_Type.range -> @@ -2439,7 +2445,7 @@ let (decl_to_string : decl -> Prims.string) = | SubEffect uu___ -> "sub_effect" | Pragma p -> let uu___ = string_of_pragma p in Prims.op_Hat "pragma #" uu___ - | DeclSyntaxExtension (id, content, uu___) -> + | DeclSyntaxExtension (id, content, uu___, uu___1) -> Prims.op_Hat "```" (Prims.op_Hat id (Prims.op_Hat "\n" (Prims.op_Hat content "\n```"))) let (modul_to_string : modul -> Prims.string) = diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 1ded6413831..74577b38560 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -9645,29 +9645,29 @@ and (desugar_decl_noattrs : FStar_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None } in let env1 = FStar_Syntax_DsEnv.push_sigelt env se in (env1, [se]) - | FStar_Parser_AST.DeclSyntaxExtension (extension_name, code, range) - -> + | FStar_Parser_AST.DeclSyntaxExtension + (extension_name, code, uu___, range) -> let extension_parser = FStar_Parser_AST_Util.lookup_extension_parser extension_name in (match extension_parser with | FStar_Pervasives_Native.None -> - let uu___ = - let uu___1 = + let uu___1 = + let uu___2 = FStar_Compiler_Util.format1 "Unknown syntax extension %s" extension_name in - (FStar_Errors_Codes.Fatal_SyntaxError, uu___1) in - FStar_Errors.raise_error uu___ range + (FStar_Errors_Codes.Fatal_SyntaxError, uu___2) in + FStar_Errors.raise_error uu___1 range | FStar_Pervasives_Native.Some parser -> let opens = - let uu___ = + let uu___1 = FStar_Syntax_DsEnv.open_modules_and_namespaces env in - let uu___1 = FStar_Syntax_DsEnv.module_abbrevs env in + let uu___2 = FStar_Syntax_DsEnv.module_abbrevs env in { - FStar_Parser_AST_Util.open_namespaces = uu___; - FStar_Parser_AST_Util.module_abbreviations = uu___1 + FStar_Parser_AST_Util.open_namespaces = uu___1; + FStar_Parser_AST_Util.module_abbreviations = uu___2 } in - let uu___ = parser opens code range in - (match uu___ with + let uu___1 = parser opens code range in + (match uu___1 with | FStar_Pervasives.Inl error -> FStar_Errors.raise_error (FStar_Errors_Codes.Fatal_SyntaxError, diff --git a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml index 45729b7a615..ec70401f869 100644 --- a/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml +++ b/ocaml/fstar-tests/generated/FStar_Tests_Pars.ml @@ -641,7 +641,7 @@ let (parse_incremental_decls : unit -> unit) = { FStar_Parser_ParseIt.frag_fname = "Demo.fst"; FStar_Parser_ParseIt.frag_text = source; - FStar_Parser_ParseIt.frag_line = Prims.int_zero; + FStar_Parser_ParseIt.frag_line = Prims.int_one; FStar_Parser_ParseIt.frag_col = Prims.int_zero } in let uu___1 = FStar_Parser_ParseIt.parse input in @@ -650,12 +650,12 @@ let (parse_incremental_decls : unit -> unit) = ((match parse_err with | FStar_Pervasives_Native.None -> failwith - "Incremental parsing failed: Expected syntax error at (7,6), got no error" + "Incremental parsing failed: Expected syntax error at (8, 6), got no error" | FStar_Pervasives_Native.Some (uu___4, uu___5, rng) -> let p = FStar_Compiler_Range_Ops.start_of_range rng in let uu___6 = (let uu___7 = FStar_Compiler_Range_Ops.line_of_pos p in - uu___7 = (Prims.of_int (7))) && + uu___7 = (Prims.of_int (8))) && (let uu___7 = FStar_Compiler_Range_Ops.col_of_pos p in uu___7 = (Prims.of_int (6))) in if uu___6 @@ -669,7 +669,7 @@ let (parse_incremental_decls : unit -> unit) = let uu___11 = FStar_Compiler_Range_Ops.col_of_pos p in FStar_Compiler_Util.string_of_int uu___11 in FStar_Compiler_Util.format2 - "Incremental parsing failed: Expected syntax error at (7,6), got error at (%s, %s)" + "Incremental parsing failed: Expected syntax error at (8, 6), got error at (%s, %s)" uu___9 uu___10 in failwith uu___8)); (match decls with diff --git a/src/parser/FStar.Parser.AST.fst b/src/parser/FStar.Parser.AST.fst index 6236811d8cf..8810eca2535 100644 --- a/src/parser/FStar.Parser.AST.fst +++ b/src/parser/FStar.Parser.AST.fst @@ -44,7 +44,14 @@ let mk_decl d r decorations = ) in let attributes_ = Util.dflt [] attributes_ in let qualifiers = List.choose (function Qualifier q -> Some q | _ -> None) decorations in - { d=d; drange=r; quals=qualifiers; attrs=attributes_ } + (* for syntax extensions, take the range stored there rather than the callers + range, which may be inaccurate *) + let range = + match d with + | DeclSyntaxExtension(_, _, r, _) -> r + | _ -> r + in + { d=d; drange=range; quals=qualifiers; attrs=attributes_ } let mk_binder_with_attrs b r l i attrs = {b=b; brange=r; blevel=l; aqual=i; battributes=attrs} let mk_binder b r l i = mk_binder_with_attrs b r l i [] @@ -736,7 +743,7 @@ let decl_to_string (d:decl) = match d.d with ^ (String.concat ";" <| List.map (fun i -> (string_of_id i)) ids) ^ "] (" ^ term_to_string t ^ ")" | SubEffect _ -> "sub_effect" | Pragma p -> "pragma #" ^ string_of_pragma p - | DeclSyntaxExtension (id, content, _) -> + | DeclSyntaxExtension (id, content, _, _) -> "```" ^ id ^ "\n" ^ content ^ "\n```" let modul_to_string (m:modul) = match m with diff --git a/src/parser/FStar.Parser.AST.fsti b/src/parser/FStar.Parser.AST.fsti index 9edb2d64ec0..1cd625e555d 100644 --- a/src/parser/FStar.Parser.AST.fsti +++ b/src/parser/FStar.Parser.AST.fsti @@ -235,7 +235,9 @@ type decl' = | Pragma of pragma | Assume of ident * term | Splice of bool * list ident * term (* bool is true for a typed splice *) - | DeclSyntaxExtension of string * string * range + (* The first range is the entire range of the blob. + The second range is the start point of the extension syntax itself *) + | DeclSyntaxExtension of string * string * range * range and decl = { d:decl'; diff --git a/src/tests/FStar.Tests.Pars.fst b/src/tests/FStar.Tests.Pars.fst index 5e0040d5acd..75b577d939c 100644 --- a/src/tests/FStar.Tests.Pars.fst +++ b/src/tests/FStar.Tests.Pars.fst @@ -210,19 +210,19 @@ let parse_incremental_decls () = let open FStar.Parser.ParseIt in let input = Incremental { frag_fname = "Demo.fst"; frag_text = source; - frag_line = 0; + frag_line = 1; frag_col = 0 } in let open FStar.Compiler.Range in match parse input with | IncrementalFragment (decls, _, parse_err) -> ( let _ = match parse_err with | None -> - failwith "Incremental parsing failed: Expected syntax error at (7,6), got no error" + failwith "Incremental parsing failed: Expected syntax error at (8, 6), got no error" | Some (_, _, rng) -> let p = start_of_range rng in - if line_of_pos p = 7 && col_of_pos p = 6 + if line_of_pos p = 8 && col_of_pos p = 6 then () - else failwith (format2 "Incremental parsing failed: Expected syntax error at (7,6), got error at (%s, %s)" + else failwith (format2 "Incremental parsing failed: Expected syntax error at (8, 6), got error at (%s, %s)" (string_of_int (line_of_pos p)) (string_of_int (col_of_pos p))) in diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index e961b1dffa0..a4e1bec7f38 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -4056,7 +4056,7 @@ and desugar_decl_noattrs top_attrs env (d:decl) : (env_t * sigelts) = let env = push_sigelt env se in env, [se] - | DeclSyntaxExtension (extension_name, code, range) -> + | DeclSyntaxExtension (extension_name, code, _, range) -> let extension_parser = FStar.Parser.AST.Util.lookup_extension_parser extension_name in match extension_parser with | None -> From 0deac841c2a1ebf1c326a47fe7eba8cb70fa4ede Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Fri, 7 Jul 2023 10:45:14 +0530 Subject: [PATCH 8/9] fix to the definition of Pure, thanks Yiyuan Cao for noticing it --- doc/book/part4/part4_pure.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/book/part4/part4_pure.rst b/doc/book/part4/part4_pure.rst index b9e88d91822..5b0f0a10c3e 100755 --- a/doc/book/part4/part4_pure.rst +++ b/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 From 859f5d20a443f42a42f77cb7ea646222328c746d Mon Sep 17 00:00:00 2001 From: Thibault Dardinier Date: Mon, 10 Jul 2023 11:45:30 -0700 Subject: [PATCH 9/9] Simple lemma about appending permutations --- ulib/FStar.Seq.Properties.fst | 6 ++++++ ulib/FStar.Seq.Properties.fsti | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/ulib/FStar.Seq.Properties.fst b/ulib/FStar.Seq.Properties.fst index 589ef8290fc..3a7e6b5c6d7 100644 --- a/ulib/FStar.Seq.Properties.fst +++ b/ulib/FStar.Seq.Properties.fst @@ -189,6 +189,12 @@ let lemma_swap_permutes_aux #_ s i j x = end #pop-options +let append_permutations #a s1 s2 s1' s2' = + ( + lemma_append_count s1 s2; + lemma_append_count s1' s2' + ) + let lemma_swap_permutes #a s i j = FStar.Classical.forall_intro #a diff --git a/ulib/FStar.Seq.Properties.fsti b/ulib/FStar.Seq.Properties.fsti index 1c67ecf8b6a..3734681e829 100644 --- a/ulib/FStar.Seq.Properties.fsti +++ b/ulib/FStar.Seq.Properties.fsti @@ -196,6 +196,11 @@ val lemma_swap_permutes_aux: #a:eqtype -> s:seq a -> i:nat{i j:nat{ type permutation (a:eqtype) (s1:seq a) (s2:seq a) = (forall i. count i s1 = count i s2) + +val append_permutations: #a:eqtype -> s1:seq a -> s2:seq a -> s1':seq a -> s2':seq a -> Lemma + (requires permutation a s1 s1' /\ permutation a s2 s2') + (ensures permutation a (append s1 s2) (append s1' s2')) + val lemma_swap_permutes (#a:eqtype) (s:seq a) (i:nat{i