Skip to content

Commit

Permalink
unifying normalization interfaces
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtzguido
mtzguido committed Aug 22, 2017
1 parent daad3df commit 0694808
Show file tree
Hide file tree
Showing 22 changed files with 212 additions and 156 deletions.
2 changes: 1 addition & 1 deletion examples/native_tactics/Canon.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 6 additions & 6 deletions examples/tactics/Normalization.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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';
Expand All @@ -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;
Expand All @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion examples/tactics/Synthesis.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)

Expand Down
2 changes: 1 addition & 1 deletion examples/tactics/Trace.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 "";;
Expand Down
14 changes: 9 additions & 5 deletions src/parser/FStar.Parser.Const.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
31 changes: 0 additions & 31 deletions src/reflection/FStar.Reflection.Basic.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<string>) : sigelt_view =
let lid = PC.p2l ns in
Expand Down
22 changes: 0 additions & 22 deletions src/reflection/FStar.Reflection.Data.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,13 +52,6 @@ type sigelt_view =
| Sg_Let of fv * typ * term
| Unk

type norm_step =
| Simpl
| WHNF
| Primops
| Delta
| UnfoldOnly of list<fv>

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]
Expand Down Expand Up @@ -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
Expand Down
56 changes: 56 additions & 0 deletions src/syntax/FStar.Syntax.Embeddings.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<string>

(* 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"
22 changes: 21 additions & 1 deletion src/syntax/FStar.Syntax.Embeddings.fsi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<string> -> term
val unembed_string_list : term -> list<string>
val unembed_string_list : term -> list<string>

type norm_step =
| Simpl
| WHNF
| Primops
| Delta
| Zeta
| Iota
| UnfoldOnly of list<string>

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
2 changes: 1 addition & 1 deletion src/syntax/FStar.Syntax.Syntax.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ]
Expand Down Expand Up @@ -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

1 change: 0 additions & 1 deletion src/syntax/FStar.Syntax.Syntax.fsi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

19 changes: 5 additions & 14 deletions src/tactics/FStar.Tactics.Basic.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<RD.norm_step>) : list<N.step> =
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<RD.norm_step>) : tac<unit> =
let norm (s : list<EMB.norm_step>) : tac<unit> =
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<RD.norm_step>) (t : term) : tac<term> =
let norm_term (s : list<EMB.norm_step>) (t : term) : tac<term> =
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
)
Expand Down
19 changes: 17 additions & 2 deletions src/tactics/ml/FStar_Tactics_Builtins.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 0694808

Please sign in to comment.