From 0694808861d2428b2a552e3291c643b2d13b2fcc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 21 Aug 2017 22:40:52 -0300 Subject: [PATCH] unifying normalization interfaces --- examples/native_tactics/Canon.fst | 2 +- examples/tactics/Normalization.fst | 12 ++-- examples/tactics/Synthesis.fst | 2 +- examples/tactics/Trace.fst | 2 +- src/parser/FStar.Parser.Const.fs | 14 +++-- src/reflection/FStar.Reflection.Basic.fs | 31 ---------- src/reflection/FStar.Reflection.Data.fs | 22 ------- src/syntax/FStar.Syntax.Embeddings.fs | 56 ++++++++++++++++++ src/syntax/FStar.Syntax.Embeddings.fsi | 22 ++++++- src/syntax/FStar.Syntax.Syntax.fs | 2 +- src/syntax/FStar.Syntax.Syntax.fsi | 1 - src/tactics/FStar.Tactics.Basic.fs | 19 ++---- src/tactics/ml/FStar_Tactics_Builtins.ml | 19 +++++- src/tactics/ml/FStar_Tactics_Derived.ml | 59 ++++++++++--------- .../FStar.TypeChecker.Normalize.fs | 37 +++++------- .../FStar.TypeChecker.Normalize.fsi | 4 +- ulib/FStar.Reflection.Data.fst | 8 --- ulib/FStar.Tactics.BV.fst | 2 +- ulib/FStar.Tactics.Canon.fst | 2 +- ulib/FStar.Tactics.Derived.fst | 6 +- ulib/ml/prims.ml | 17 ++++++ ulib/prims.fst | 29 ++++++--- 22 files changed, 212 insertions(+), 156 deletions(-) diff --git a/examples/native_tactics/Canon.fst b/examples/native_tactics/Canon.fst index d98e018ac52..de8cc743ab7 100644 --- a/examples/native_tactics/Canon.fst +++ b/examples/native_tactics/Canon.fst @@ -299,7 +299,7 @@ let rec canon_point : unit -> Tac unit = fun () -> ( // Fold constants | Inr (Plus (Lit _) (Lit _)) | Inr (Mult (Lit _) (Lit _)) -> - norm [Delta; Primops];; + norm [delta; primops];; trefl // Forget about negations diff --git a/examples/tactics/Normalization.fst b/examples/tactics/Normalization.fst index 6189366ff98..76ad3d252de 100644 --- a/examples/tactics/Normalization.fst +++ b/examples/tactics/Normalization.fst @@ -27,10 +27,10 @@ let def_of (#t:Type) (x:t) : tactic term = let add_1 (x:int) : int = x + 1 (* add_2 is defined to be (x + 1) + 1 *) -let add_2 (x:int) : int = synth_by_tactic (normalize [Primops; Delta] (add_1 (add_1 x))) +let add_2 (x:int) : int = synth_by_tactic (normalize [primops; delta] (add_1 (add_1 x))) (* `four` is defined as `4` ... *) -let four : int = synth_by_tactic (normalize [Primops; Delta] (add_2 2)) +let four : int = synth_by_tactic (normalize [primops; delta] (add_2 2)) (* .. as we can check by inspecting its definition *) let _ = assert_by_tactic True @@ -42,7 +42,7 @@ let _ = assert_by_tactic True (* If we only allow for Delta steps, then there's no primitive computation and we * end up with (2 + 1) + 1 *) -let four' : int = synth_by_tactic (normalize [Delta] (add_2 2)) +let four' : int = synth_by_tactic (normalize [delta] (add_2 2)) let _ = assert_by_tactic True (t <-- def_of four'; @@ -53,10 +53,10 @@ let _ = assert_by_tactic True (* Here, we allow for primitive computation but don't allow for `add_2` to be expanded to * its definition, so the final result is `add_2 1` *) -let unfold_add_1: norm_step = UnfoldOnly [pack_fv ["Normalization"; "add_1"]] +let unfold_add_1: norm_step = delta_only ["Normalization.add_1"] let three : int = synth_by_tactic - (normalize [Delta; unfold_add_1; Primops] (add_2 (add_1 0))) + (normalize [delta; unfold_add_1; primops] (add_2 (add_1 0))) let _ = assert_by_tactic True (t <-- def_of three; @@ -69,7 +69,7 @@ let _ = assert_by_tactic True * when this definition is type-checked, and not when it's called. So, this function is just an * identity function with no special semantics. *) let does_not_normalize (#t:Type) (x:t) : t = - synth_by_tactic #t #unit (normalize [Primops; Delta] x) + synth_by_tactic #t #unit (normalize [primops; delta] x) let four'' : int = does_not_normalize (2+2) diff --git a/examples/tactics/Synthesis.fst b/examples/tactics/Synthesis.fst index 0a7c7b80568..b889a9fbfa2 100644 --- a/examples/tactics/Synthesis.fst +++ b/examples/tactics/Synthesis.fst @@ -26,7 +26,7 @@ let rec fib_norm (n : int) : tactic unit = dup;; apply (quote op_Addition);; iseq [fib_norm (n - 1); fib_norm (n - 2)];; - norm [Primops];; + norm [primops];; trefl ) diff --git a/examples/tactics/Trace.fst b/examples/tactics/Trace.fst index a5f47ea02b8..5b72fcb217b 100644 --- a/examples/tactics/Trace.fst +++ b/examples/tactics/Trace.fst @@ -119,7 +119,7 @@ let instrument (f : 'a) : tactic unit = } in (* Apply the function to the arguments and unfold it. This will only * unfold it once, so recursive calls are present *) - t <-- norm_term [Delta] (mk_e_app t ii.args); + t <-- norm_term [delta] (mk_e_app t ii.args); dup;; t <-- instrument_body ii t; dump "";; diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs index 04c9c85d325..bd5ca710e6f 100644 --- a/src/parser/FStar.Parser.Const.fs +++ b/src/parser/FStar.Parser.Const.fs @@ -216,11 +216,15 @@ let inversion_lid = p2l ["FStar"; "Pervasives"; "inversion"] let normalize = pconst "normalize" let normalize_term = pconst "normalize_term" let norm = pconst "norm" -let steps_zeta = pconst "zeta" -let steps_iota = pconst "iota" -let steps_primops = pconst "primops" -let steps_delta = pconst "delta" -let steps_delta_only = pconst "delta_only" + +(* lids for normalizer steps *) +let steps_simpl = pconst "Simpl" +let steps_whnf = pconst "WHNF" +let steps_primops = pconst "Primops" +let steps_zeta = pconst "Zeta" +let steps_iota = pconst "Iota" +let steps_delta = pconst "Delta" +let steps_unfoldonly = pconst "UnfoldOnly" let gen_reset = let x = U.mk_ref 0 in diff --git a/src/reflection/FStar.Reflection.Basic.fs b/src/reflection/FStar.Reflection.Basic.fs index 0431300c99b..3477c12e8be 100644 --- a/src/reflection/FStar.Reflection.Basic.fs +++ b/src/reflection/FStar.Reflection.Basic.fs @@ -474,37 +474,6 @@ let compare_binder (x:binder) (y:binder) : order = let is_free (x:binder) (t:term) : bool = U.is_free_in (fst x) t -let embed_norm_step (n:norm_step) : term = - match n with - | Simpl -> - ref_Simpl - | WHNF -> - ref_WHNF - | Primops -> - ref_Primops - | Delta -> - ref_Delta - | UnfoldOnly l -> - S.mk_Tm_app ref_UnfoldOnly [S.as_arg (embed_list embed_fvar fstar_refl_fvar l)] - None Range.dummyRange - -let unembed_norm_step (t:term) : norm_step = - let t = U.unascribe t in - let hd, args = U.head_and_args t in - match (U.un_uinst hd).n, args with - | Tm_fvar fv, [] when S.fv_eq_lid fv ref_Simpl_lid -> - Simpl - | Tm_fvar fv, [] when S.fv_eq_lid fv ref_WHNF_lid -> - WHNF - | Tm_fvar fv, [] when S.fv_eq_lid fv ref_Primops_lid -> - Primops - | Tm_fvar fv, [] when S.fv_eq_lid fv ref_Delta_lid -> - Delta - | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv ref_UnfoldOnly_lid -> - UnfoldOnly (unembed_list unembed_fvar l) - | _ -> - failwith "not an embedded norm_step" - // Only for inductives, at the moment let lookup_typ (env:Env.env) (ns:list) : sigelt_view = let lid = PC.p2l ns in diff --git a/src/reflection/FStar.Reflection.Data.fs b/src/reflection/FStar.Reflection.Data.fs index 6d56c2460c5..f5d10e36a91 100644 --- a/src/reflection/FStar.Reflection.Data.fs +++ b/src/reflection/FStar.Reflection.Data.fs @@ -52,13 +52,6 @@ type sigelt_view = | Sg_Let of fv * typ * term | Unk -type norm_step = - | Simpl - | WHNF - | Primops - | Delta - | UnfoldOnly of list - let fstar_refl_lid s = Ident.lid_of_path (["FStar"; "Reflection"]@s) Range.dummyRange let fstar_refl_basic_lid s = fstar_refl_lid ["Basic"; s] @@ -151,25 +144,10 @@ let ref_Sg_Let = tdataconstr ref_Sg_Let_lid let ref_Unk = tdataconstr ref_Unk_lid let ref_Ctor = tdataconstr ref_Ctor_lid -let fstar_refl_norm_step = mk_refl_data_lid_as_term "norm_step" - -let ref_Simpl_lid = fstar_refl_data_lid "Simpl" -let ref_WHNF_lid = fstar_refl_data_lid "WHNF" -let ref_Primops_lid = fstar_refl_data_lid "Primops" -let ref_Delta_lid = fstar_refl_data_lid "Delta" -let ref_UnfoldOnly_lid = fstar_refl_data_lid "UnfoldOnly" - -let ref_Simpl = tdataconstr ref_Simpl_lid -let ref_WHNF = tdataconstr ref_WHNF_lid -let ref_Primops = tdataconstr ref_Primops_lid -let ref_Delta = tdataconstr ref_Delta_lid -let ref_UnfoldOnly = tdataconstr ref_UnfoldOnly_lid - let t_binder = tabbrev <| fstar_refl_types_lid "binder" let t_term = tabbrev <| fstar_refl_types_lid "term" let t_fv = tabbrev <| fstar_refl_types_lid "fv" let t_binders = tabbrev <| fstar_refl_types_lid "binders" -let t_norm_step = tabbrev <| fstar_refl_types_lid "norm_step" let ord_Lt_lid = Ident.lid_of_path (["FStar"; "Order"; "Lt"]) Range.dummyRange let ord_Eq_lid = Ident.lid_of_path (["FStar"; "Order"; "Eq"]) Range.dummyRange diff --git a/src/syntax/FStar.Syntax.Embeddings.fs b/src/syntax/FStar.Syntax.Embeddings.fs index 1e7817fc6c2..9ddc9d93b77 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fs +++ b/src/syntax/FStar.Syntax.Embeddings.fs @@ -116,3 +116,59 @@ let rec unembed_list (unembed_a: (term -> 'a)) (l:term) : list<'a> = let embed_string_list ss = embed_list embed_string S.t_string ss let unembed_string_list t = unembed_list unembed_string t +type norm_step = + | Simpl + | WHNF + | Primops + | Delta + | Zeta + | Iota + | UnfoldOnly of list + +(* the steps as terms *) +let steps_Simpl = tdataconstr PC.steps_simpl +let steps_WHNF = tdataconstr PC.steps_whnf +let steps_Primops = tdataconstr PC.steps_primops +let steps_Delta = tdataconstr PC.steps_delta +let steps_Zeta = tdataconstr PC.steps_zeta +let steps_Iota = tdataconstr PC.steps_iota +let steps_UnfoldOnly = tdataconstr PC.steps_unfoldonly + +let embed_norm_step (n:norm_step) : term = + match n with + | Simpl -> + steps_Simpl + | WHNF -> + steps_WHNF + | Primops -> + steps_Primops + | Delta -> + steps_Delta + | Zeta -> + steps_Zeta + | Iota -> + steps_Iota + | UnfoldOnly l -> + S.mk_Tm_app steps_UnfoldOnly [S.as_arg (embed_list embed_string S.t_string l)] + None Range.dummyRange + +let unembed_norm_step (t:term) : norm_step = + let t = U.unascribe t in + let hd, args = U.head_and_args t in + match (U.un_uinst hd).n, args with + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_simpl -> + Simpl + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_whnf -> + WHNF + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_primops -> + Primops + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_delta -> + Delta + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_zeta -> + Zeta + | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_iota -> + Iota + | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonly -> + UnfoldOnly (unembed_list unembed_string l) + | _ -> + failwith "not an embedded norm_step" diff --git a/src/syntax/FStar.Syntax.Embeddings.fsi b/src/syntax/FStar.Syntax.Embeddings.fsi index e0d7fedca58..3382d190666 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fsi +++ b/src/syntax/FStar.Syntax.Embeddings.fsi @@ -26,4 +26,24 @@ val embed_list : ('a -> term) -> term -> list<'a> -> term val unembed_list : (term -> 'a) -> term -> list<'a> val embed_string_list : list -> term -val unembed_string_list : term -> list \ No newline at end of file +val unembed_string_list : term -> list + +type norm_step = + | Simpl + | WHNF + | Primops + | Delta + | Zeta + | Iota + | UnfoldOnly of list + +val steps_Simpl : term +val steps_WHNF : term +val steps_Primops : term +val steps_Delta : term +val steps_Zeta : term +val steps_Iota : term +val steps_UnfoldOnly : term + +val embed_norm_step : norm_step -> term +val unembed_norm_step : term -> norm_step diff --git a/src/syntax/FStar.Syntax.Syntax.fs b/src/syntax/FStar.Syntax.Syntax.fs index 08e6aff1355..bd54ed6d00a 100644 --- a/src/syntax/FStar.Syntax.Syntax.fs +++ b/src/syntax/FStar.Syntax.Syntax.fs @@ -27,6 +27,7 @@ open FStar.Range open FStar.Ident open FStar.Const open FStar.Dyn +module PC = FStar.Parser.Const (* Objects with metadata *) ///[@ PpxDerivingShow ] @@ -565,4 +566,3 @@ let t_tac_unit = mk_Tm_app (mk_Tm_uinst (tabbrev C.u_tac_lid) [U_zero]) [as_a let t_list_of t = mk_Tm_app (mk_Tm_uinst (tabbrev C.list_lid) [U_zero]) [as_arg t] None Range.dummyRange let t_option_of t = mk_Tm_app (mk_Tm_uinst (tabbrev C.option_lid) [U_zero]) [as_arg t] None Range.dummyRange let unit_const = mk (Tm_constant FStar.Const.Const_unit) None Range.dummyRange - diff --git a/src/syntax/FStar.Syntax.Syntax.fsi b/src/syntax/FStar.Syntax.Syntax.fsi index 6e4ba0c3277..db8c96cc299 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsi +++ b/src/syntax/FStar.Syntax.Syntax.fsi @@ -475,4 +475,3 @@ val t_tac_unit : term val t_list_of : term -> term val t_option_of : term -> term val unit_const : term - diff --git a/src/tactics/FStar.Tactics.Basic.fs b/src/tactics/FStar.Tactics.Basic.fs index 0be5b8dd76d..ebf796c1d12 100644 --- a/src/tactics/FStar.Tactics.Basic.fs +++ b/src/tactics/FStar.Tactics.Basic.fs @@ -24,6 +24,7 @@ module TcTerm = FStar.TypeChecker.TcTerm module N = FStar.TypeChecker.Normalize module RD = FStar.Reflection.Data module UF = FStar.Syntax.Unionfind +module EMB = FStar.Syntax.Embeddings type name = bv type env = Env.env @@ -397,28 +398,18 @@ let intro_rec : tac<(binder * binder)> = fail1 "intro_rec: goal is not an arrow (%s)" (Print.term_to_string goal.goal_ty) ) -let tr_steps (s : list) : list = - let tr s = match s with - | RD.Simpl -> [N.Simplify] - | RD.WHNF -> [N.WHNF] - | RD.Primops -> [N.Primops] - | RD.Delta -> [N.UnfoldUntil Delta_constant] - | RD.UnfoldOnly l -> [N.UnfoldOnly (List.map S.lid_of_fv l)] - in - List.flatten (List.map tr s) - -let norm (s : list) : tac = +let norm (s : list) : tac = bind cur_goal (fun goal -> // Translate to actual normalizer steps - let steps = [N.Reify; N.UnfoldTac]@(tr_steps s) in + let steps = [N.Reify; N.UnfoldTac]@(N.tr_norm_steps s) in let w = normalize steps goal.context goal.witness in let t = normalize steps goal.context goal.goal_ty in replace_cur ({goal with goal_ty = t; witness = w}) ) -let norm_term (s : list) (t : term) : tac = +let norm_term (s : list) (t : term) : tac = bind get (fun ps -> - let steps = [N.Reify; N.UnfoldTac]@(tr_steps s) in + let steps = [N.Reify; N.UnfoldTac]@(N.tr_norm_steps s) in let t = normalize steps ps.main_context t in ret t ) diff --git a/src/tactics/ml/FStar_Tactics_Builtins.ml b/src/tactics/ml/FStar_Tactics_Builtins.ml index 3a71f0a1bad..4ce591a19cc 100644 --- a/src/tactics/ml/FStar_Tactics_Builtins.ml +++ b/src/tactics/ml/FStar_Tactics_Builtins.ml @@ -4,6 +4,7 @@ open FStar_Tactics_Effect module E = FStar_Tactics_Effect module B = FStar_Tactics_Basic module RT = FStar_Reflection_Types +module EMB = FStar_Syntax_Embeddings let interpret_tac (t: 'a B.tac) (ps: proofstate): 'a E.__result = match B.run t ps with @@ -15,6 +16,17 @@ let uninterpret_tac (t: 'a __tac) (ps: proofstate): 'a B.result = | E.Success (a, state) -> B.Success (a, state) | E.Failed (s, state) -> B.Failed (s, state) +let tr_repr_steps = + let tr1 = function + | Simpl -> EMB.Simpl + | WHNF -> EMB.WHNF + | Primops -> EMB.Primops + | Delta -> EMB.Delta + | Zeta -> EMB.Zeta + | Iota -> EMB.Iota + | UnfoldOnly ss -> EMB.UnfoldOnly ss + in List.map tr1 + let to_tac_0 (t: 'a __tac): 'a B.tac = (fun (ps: proofstate) -> uninterpret_tac t ps) |> B.mk_tac @@ -59,8 +71,11 @@ let trytac: 'a E.tactic -> unit -> ('a option) __tac = fun t -> fun () -> __tryt let __trivial: unit __tac = from_tac_0 B.trivial let trivial: unit -> unit __tac = fun () -> __trivial -let __norm (s: FStar_Reflection_Data.norm_step list): unit __tac = from_tac_1 B.norm s -let norm: FStar_Reflection_Data.norm_step list -> unit -> unit __tac = fun s -> fun () -> __norm s +let __norm (s: norm_step list): unit __tac = from_tac_1 B.norm (tr_repr_steps s) +let norm: norm_step list -> unit -> unit __tac = fun s -> fun () -> __norm s + +let __norm_term (s: norm_step list) (t: RT.term) : RT.term __tac = from_tac_2 B.norm_term (tr_repr_steps s) t +let norm_term: norm_step list -> RT.term -> unit -> RT.term __tac = fun s t -> fun () -> __norm_term s t let __intro: RT.binder __tac = from_tac_0 B.intro let intro: unit -> RT.binder __tac = fun () -> __intro diff --git a/src/tactics/ml/FStar_Tactics_Derived.ml b/src/tactics/ml/FStar_Tactics_Derived.ml index b36adbc07a0..5d99cd86ce1 100644 --- a/src/tactics/ml/FStar_Tactics_Derived.ml +++ b/src/tactics/ml/FStar_Tactics_Derived.ml @@ -115,15 +115,21 @@ let rec repeatseq: (FStar_Tactics_Builtins.trytac (FStar_Tactics_Builtins.seq (FStar_Tactics_Effect.bind t - (fun uu___38_672 -> FStar_Tactics_Effect.return ())) + (fun uu___50_672 -> FStar_Tactics_Effect.return ())) (repeatseq t))) - (fun uu___39_678 -> FStar_Tactics_Effect.return ()) () + (fun uu___51_678 -> FStar_Tactics_Effect.return ()) () let simpl: Prims.unit FStar_Tactics_Effect.tactic = - FStar_Tactics_Builtins.norm - [FStar_Reflection_Data.Simpl; FStar_Reflection_Data.Primops] + FStar_Tactics_Builtins.norm [Prims.simpl; Prims.primops] let whnf: Prims.unit FStar_Tactics_Effect.tactic = - FStar_Tactics_Builtins.norm - [FStar_Reflection_Data.WHNF; FStar_Reflection_Data.Primops] + FStar_Tactics_Builtins.norm [Prims.whnf; Prims.primops] +let intros: + Prims.unit -> + (FStar_Reflection_Types.binder Prims.list,(FStar_Reflection_Types.binder + Prims.list + FStar_Tactics_Effect.__result, + Obj.t) Prims.l_Forall) + FStar_Tactics_Effect._dm4f_TAC_repr + = repeat FStar_Tactics_Builtins.intro let __cut: 'Ab 'Aa . ('Aa -> 'Ab) -> 'Aa -> 'Ab = fun f -> fun x -> f x let tcut: FStar_Reflection_Types.term -> @@ -139,15 +145,15 @@ let tcut: (FStar_Reflection_Basic.pack (FStar_Reflection_Data.Tv_App (qq, (t, FStar_Reflection_Data.Q_Explicit)))))) - (fun uu___40_733 -> FStar_Tactics_Builtins.intro)) + (fun uu___52_765 -> FStar_Tactics_Builtins.intro)) let rec revert_all: FStar_Reflection_Types.binders -> Prims.unit FStar_Tactics_Effect.tactic = fun bs -> match bs with | [] -> FStar_Tactics_Effect.return () - | uu____746::tl1 -> + | uu____778::tl1 -> FStar_Tactics_Effect.bind FStar_Tactics_Builtins.revert - (fun uu___41_751 -> revert_all tl1) + (fun uu___53_783 -> revert_all tl1) let assumption: Prims.unit FStar_Tactics_Effect.tactic = FStar_Tactics_Effect.bind FStar_Tactics_Builtins.cur_env (fun e -> @@ -172,13 +178,13 @@ let destruct_equality_implication: | FStar_Reflection_Formula.Implies (lhs,rhs) -> (match FStar_Reflection_Formula.term_as_formula' lhs with | FStar_Reflection_Formula.Comp - (FStar_Reflection_Formula.Eq ,uu____821,uu____822,uu____823) -> + (FStar_Reflection_Formula.Eq ,uu____853,uu____854,uu____855) -> FStar_Tactics_Effect.return (FStar_Pervasives_Native.Some ((FStar_Reflection_Formula.term_as_formula' lhs), rhs)) - | uu____834 -> + | uu____866 -> FStar_Tactics_Effect.return FStar_Pervasives_Native.None) - | uu____845 -> FStar_Tactics_Effect.return FStar_Pervasives_Native.None + | uu____877 -> FStar_Tactics_Effect.return FStar_Pervasives_Native.None let rec try_rewrite_equality: FStar_Reflection_Types.term -> FStar_Reflection_Types.binders -> Prims.unit FStar_Tactics_Effect.tactic @@ -192,11 +198,11 @@ let rec try_rewrite_equality: (FStar_Reflection_Basic.type_of_binder x_t) with | FStar_Reflection_Formula.Comp - (FStar_Reflection_Formula.Eq ,uu____883,y,uu____885) -> + (FStar_Reflection_Formula.Eq ,uu____915,y,uu____917) -> if FStar_Reflection_Basic.term_eq x y then FStar_Tactics_Builtins.rewrite x_t else try_rewrite_equality x bs1 - | uu____889 -> try_rewrite_equality x bs1) + | uu____921 -> try_rewrite_equality x bs1) let rec rewrite_all_context_equalities: FStar_Reflection_Types.binders -> Prims.unit FStar_Tactics_Effect.tactic = fun bs -> @@ -208,13 +214,13 @@ let rec rewrite_all_context_equalities: (FStar_Reflection_Basic.type_of_binder x_t) with | FStar_Reflection_Formula.Comp - (FStar_Reflection_Formula.Eq ,uu____916,lhs,uu____918) -> + (FStar_Reflection_Formula.Eq ,uu____948,lhs,uu____950) -> (match FStar_Reflection_Basic.inspect lhs with - | FStar_Reflection_Data.Tv_Var uu____921 -> + | FStar_Reflection_Data.Tv_Var uu____953 -> FStar_Tactics_Builtins.rewrite x_t - | uu____922 -> idtac) - | uu____923 -> idtac) - (fun uu___42_925 -> rewrite_all_context_equalities bs1) + | uu____954 -> idtac) + | uu____955 -> idtac) + (fun uu___54_957 -> rewrite_all_context_equalities bs1) let rewrite_eqs_from_context: Prims.unit FStar_Tactics_Effect.tactic = FStar_Tactics_Effect.bind FStar_Tactics_Builtins.cur_env (fun e -> @@ -240,15 +246,14 @@ let unfold_point: (fun g -> match FStar_Reflection_Formula.term_as_formula g with | FStar_Reflection_Formula.Comp - (FStar_Reflection_Formula.Eq ,uu____992,l,r) -> + (FStar_Reflection_Formula.Eq ,uu____1024,l,r) -> if FStar_Reflection_Basic.term_eq l t then FStar_Tactics_Effect.bind - (FStar_Tactics_Builtins.norm - [FStar_Reflection_Data.Delta]) - (fun uu___43_998 -> FStar_Tactics_Builtins.trefl) + (FStar_Tactics_Builtins.norm [Prims.delta]) + (fun uu___55_1030 -> FStar_Tactics_Builtins.trefl) else FStar_Tactics_Builtins.trefl - | uu____1000 -> fail "impossible")) + | uu____1032 -> fail "impossible")) let unfold_def: FStar_Reflection_Types.term -> Prims.unit FStar_Tactics_Effect.tactic = fun t -> FStar_Tactics_Builtins.pointwise (unfold_point t) @@ -264,13 +269,13 @@ let grewrite': (fun g -> match FStar_Reflection_Formula.term_as_formula g with | FStar_Reflection_Formula.Comp - (FStar_Reflection_Formula.Eq ,uu____1046,l,uu____1048) -> + (FStar_Reflection_Formula.Eq ,uu____1078,l,uu____1080) -> if FStar_Reflection_Basic.term_eq l t1 then FStar_Tactics_Builtins.exact (FStar_Tactics_Effect.return eq1) else FStar_Tactics_Builtins.trefl - | uu____1052 -> fail "impossible") + | uu____1084 -> fail "impossible") let mk_sq_eq: FStar_Reflection_Types.term -> FStar_Reflection_Types.term -> FStar_Reflection_Types.term @@ -314,5 +319,5 @@ let rec iseq: | t::ts1 -> FStar_Tactics_Effect.bind (FStar_Tactics_Builtins.divide (Prims.parse_int "1") t (iseq ts1)) - (fun uu___44_1161 -> FStar_Tactics_Effect.return ()) + (fun uu___56_1193 -> FStar_Tactics_Effect.return ()) | [] -> FStar_Tactics_Effect.return () \ No newline at end of file diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fs b/src/typechecker/FStar.TypeChecker.Normalize.fs index 79416e4d085..efc0d1b629b 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fs +++ b/src/typechecker/FStar.TypeChecker.Normalize.fs @@ -39,6 +39,7 @@ module FC = FStar.Const module PC = FStar.Parser.Const module U = FStar.Syntax.Util module I = FStar.Ident +module EMB = FStar.Syntax.Embeddings (********************************************************************************************** * Reduction of types via the Krivine Abstract Machine (KN), with lazy @@ -820,29 +821,21 @@ let is_norm_request hd args = | _ -> false +let tr_norm_step = function + | EMB.Zeta -> [Zeta] + | EMB.Iota -> [Iota] + | EMB.Delta -> [UnfoldUntil Delta_constant] + | EMB.Simpl -> [Simplify] + | EMB.WHNF -> [WHNF] + | EMB.Primops -> [Primops] + | EMB.UnfoldOnly names -> + [UnfoldUntil Delta_constant; UnfoldOnly (List.map I.lid_of_str names)] + +let tr_norm_steps s = + List.concatMap tr_norm_step s + let get_norm_request (full_norm:term -> term) args = - let parse_steps s = - let unembed_step s = - match (U.un_uinst s).n with - | Tm_fvar fv when S.fv_eq_lid fv PC.steps_zeta -> - Zeta - | Tm_fvar fv when S.fv_eq_lid fv PC.steps_iota -> - Iota - | Tm_fvar fv when S.fv_eq_lid fv PC.steps_primops -> - Primops - | Tm_fvar fv when S.fv_eq_lid fv PC.steps_delta -> - UnfoldUntil Delta_constant - | Tm_fvar fv when S.fv_eq_lid fv PC.steps_delta_only -> - UnfoldUntil Delta_constant - | Tm_app({n=Tm_fvar fv}, [(names, _)]) - when S.fv_eq_lid fv PC.steps_delta_only -> - let names = FStar.Syntax.Embeddings.unembed_string_list names in - let lids = names |> List.map Ident.lid_of_str in - UnfoldOnly lids - | _ -> failwith "Not an embedded `Prims.step`" - in - FStar.Syntax.Embeddings.unembed_list unembed_step s - in + let parse_steps s = tr_norm_steps <| EMB.unembed_list EMB.unembed_norm_step s in match args with | [_; (tm, _)] | [(tm, _)] -> diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fsi b/src/typechecker/FStar.TypeChecker.Normalize.fsi index 1a191dc762f..0b0127e3eb1 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fsi +++ b/src/typechecker/FStar.TypeChecker.Normalize.fsi @@ -64,4 +64,6 @@ val ghost_to_pure_lcomp: Env.env -> lcomp -> lcomp val normalize_with_primitive_steps : list -> list -> Env.env -> term -> term val term_to_string: Env.env -> term -> string val comp_to_string: Env.env -> comp -> string -val elim_uvars: Env.env -> sigelt -> sigelt \ No newline at end of file +val elim_uvars: Env.env -> sigelt -> sigelt + +val tr_norm_steps : list -> list diff --git a/ulib/FStar.Reflection.Data.fst b/ulib/FStar.Reflection.Data.fst index d10ba486953..72d49785dbe 100644 --- a/ulib/FStar.Reflection.Data.fst +++ b/ulib/FStar.Reflection.Data.fst @@ -69,11 +69,3 @@ type sigelt_view = sigelt_view | Unk - -noeq -type norm_step = - | Simpl - | WHNF - | Primops - | Delta - | UnfoldOnly : list fv -> norm_step diff --git a/ulib/FStar.Tactics.BV.fst b/ulib/FStar.Tactics.BV.fst index d974ccef330..367106b455f 100644 --- a/ulib/FStar.Tactics.BV.fst +++ b/ulib/FStar.Tactics.BV.fst @@ -124,7 +124,7 @@ let rec arith_expr_to_bv e : tactic unit = trefl let arith_to_bv_tac : tactic unit = - // norm [Simpl];; + // norm [simpl];; g <-- cur_goal; let f = term_as_formula g in match f with diff --git a/ulib/FStar.Tactics.Canon.fst b/ulib/FStar.Tactics.Canon.fst index 5177b7699e3..5dc3116e69e 100644 --- a/ulib/FStar.Tactics.Canon.fst +++ b/ulib/FStar.Tactics.Canon.fst @@ -105,7 +105,7 @@ let rec canon_point : unit -> Tac unit = fun () -> ( // Fold constants | Inr (Plus (Lit _) (Lit _)) | Inr (Mult (Lit _) (Lit _)) -> - norm [Delta; Primops];; // Need this to turn op_Star into op_Multiply, as there's no primop for it + norm [delta; primops];; // Need this to turn op_Star into op_Multiply, as there's no primop for it trefl // Forget about negations diff --git a/ulib/FStar.Tactics.Derived.fst b/ulib/FStar.Tactics.Derived.fst index 49102b8f421..9413d2d3d74 100644 --- a/ulib/FStar.Tactics.Derived.fst +++ b/ulib/FStar.Tactics.Derived.fst @@ -64,8 +64,8 @@ let repeat1 (#a:Type) (t : tactic a) : tactic (list a) = let rec repeatseq (#a:Type) (t : tactic a) () : Tac unit = (trytac (seq (t;; return ()) (repeatseq t));; return ()) () -let simpl : tactic unit = norm [Simpl; Primops] -let whnf : tactic unit = norm [WHNF; Primops] +let simpl : tactic unit = norm [simpl; primops] +let whnf : tactic unit = norm [whnf; primops] let intros : tactic (list binder) = repeat intro @@ -149,7 +149,7 @@ let unfold_point (t:term) : tactic unit = match f with | Comp Eq _ l r -> if term_eq l t - then (norm [Delta];; trefl) + then (norm [delta];; trefl) else trefl | _ -> fail "impossible" diff --git a/ulib/ml/prims.ml b/ulib/ml/prims.ml index e82767a5ec2..faa3d7cf847 100644 --- a/ulib/ml/prims.ml +++ b/ulib/ml/prims.ml @@ -130,3 +130,20 @@ let __proj__Cons__item__tl = function | _ -> failwith "Impossible" let min = min + +type norm_step = + | Simpl + | WHNF + | Primops + | Delta + | Zeta + | Iota + | UnfoldOnly : string list -> norm_step + +let simpl : norm_step = Simpl +let whnf : norm_step = WHNF +let primops : norm_step = Primops +let delta : norm_step = Delta +let zeta : norm_step = Zeta +let iota : norm_step = Iota +let delta_only (s:string list) : norm_step = UnfoldOnly s diff --git a/ulib/prims.fst b/ulib/prims.fst index 80d6f8bbc2d..3204ac5ac95 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -322,13 +322,28 @@ assume val string_of_int: int -> Tot string (*********************************************************************************) abstract let normalize_term (#a:Type) (x:a) : a = x abstract let normalize (a:Type0) = a -abstract let step : Type0 = unit -abstract let zeta : step = () -abstract let iota : step = () -abstract let primops : step = () -abstract let delta : step = () -abstract let delta_only (s:list string) : step = () -abstract let norm (s:list step) (#a:Type) (x:a) : a = x + +abstract +type norm_step = + | Simpl + | WHNF + | Primops + | Delta + | Zeta + | Iota + | UnfoldOnly : list string -> norm_step // each string is a fully qualified name like `A.M.f` + +// Helpers, so we don't expose the actual inductive +let simpl : norm_step = Simpl +let whnf : norm_step = WHNF +let primops : norm_step = Primops +let delta : norm_step = Delta +let zeta : norm_step = Zeta +let iota : norm_step = Iota +let delta_only (s:list string) : norm_step = UnfoldOnly s + +// Normalization marker +abstract let norm (s:list norm_step) (#a:Type) (x:a) : a = x val assert_norm : p:Type -> Pure unit (requires (normalize p)) (ensures (fun _ -> p)) let assert_norm p = ()