Skip to content

Commit

Permalink
Merge pull request #3723 from mtzguido/delta_attr
Browse files Browse the repository at this point in the history 
Normalizer: making delta attributes compose
  • Loading branch information
@mtzguido
mtzguido authored Feb 7, 2025
2 parents 48db48a + cc06edb commit fb57af6
Show file tree
Hide file tree
Showing 4 changed files with 189 additions and 5 deletions.
11 changes: 6 additions & 5 deletions src/typechecker/FStarC.TypeChecker.Cfg.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,7 @@ let default_steps : fsteps = {
}

let fstep_add_one s fs =
let optlist = function None -> [] | Some xs -> xs in
match s with
| Beta -> { fs with beta = true }
| Iota -> { fs with iota = true }
Expand All @@ -193,10 +194,11 @@ let fstep_add_one s fs =
| Inlining -> fs // not a step // ZP : Adding qualification because of name clash
| DoNotUnfoldPureLets -> { fs with do_not_unfold_pure_lets = true }
| UnfoldUntil d -> { fs with unfold_until = Some d }
| UnfoldOnly lids -> { fs with unfold_only = Some lids }
| UnfoldOnce lids -> { fs with unfold_once = Some lids }
| UnfoldFully lids -> { fs with unfold_fully = Some lids }
| UnfoldAttr lids -> { fs with unfold_attr = Some lids }
| UnfoldOnly lids -> { fs with unfold_only = Some <| optlist fs.unfold_only @ lids }
| UnfoldOnce lids -> { fs with unfold_once = Some <| optlist fs.unfold_once @ lids }
| UnfoldFully lids -> { fs with unfold_fully = Some <| optlist fs.unfold_fully @ lids }
| UnfoldAttr lids -> { fs with unfold_attr = Some <| optlist fs.unfold_attr @ lids }
| DontUnfoldAttr lids -> { fs with dont_unfold_attr = Some <| optlist fs.dont_unfold_attr @ lids }
| UnfoldQual strs ->
let fs = { fs with unfold_qual = Some strs } in
if List.contains "pure_subterms_within_computations" strs
Expand All @@ -205,7 +207,6 @@ let fstep_add_one s fs =
| UnfoldNamespace strs ->
{ fs with unfold_namespace =
Some (List.map (fun s -> (Ident.path_of_text s, true)) strs, false) }
| DontUnfoldAttr lids -> { fs with dont_unfold_attr = Some lids }
| PureSubtermsWithinComputations -> { fs with pure_subterms_within_computations = true }
| Simplify -> { fs with simplify = true }
| EraseUniverses -> { fs with erase_universes = true }
Expand Down
4 changes: 4 additions & 0 deletions tests/vale/DeltaAttr.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,10 @@ let test_2 (x:int) : int = synth_by_tactic
let test_3 (x:int) : int = synth_by_tactic
(fun () -> normalize [delta_attr [`%myattr; `%otherattr]] (add (sub_1 (add_1 x))))

(* Multiple delta_attr compose *)
let test_3' (x:int) : int = synth_by_tactic
(fun () -> normalize [delta_attr [`%myattr]; delta_attr[`%otherattr]] (add (sub_1 (add_1 x))))

let test_4 (x:int) : int = synth_by_tactic
(fun () -> normalize [delta_attr [`%myattr]; delta_only [`%(add)]] (add (sub_1 (add_1 x))))

Expand Down
177 changes: 177 additions & 0 deletions tests/vale/DeltaAttr.fst.output.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,177 @@
Module after desugaring:
module DeltaAttr
Declarations: [
irreducible
let myattr = ()
irreducible
let otherattr = ()
let normalize steps x =
(FStar.Stubs.Tactics.V2.Builtins.dup ();
FStar.Tactics.V2.Derived.exact (quote x);
FStar.Stubs.Tactics.V2.Builtins.norm steps;
FStar.Tactics.V2.Derived.trefl ())
<:
FStar.Tactics.Effect.Tac Prims.unit
[@@ DeltaAttr.myattr]
let add_1 x = x + 1 <: Prims.int
[@@ DeltaAttr.myattr]
let sub_1 x = x - 1 <: Prims.int
[@@ DeltaAttr.otherattr]
let add x = x + x <: Prims.int
let test_1 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_2 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_3 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_3' x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"];
FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_4 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"];
FStar.Pervasives.delta_only ["DeltaAttr.add"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_5 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_only ["DeltaAttr.add"];
FStar.Pervasives.delta_only ["DeltaAttr.add_1"];
FStar.Pervasives.delta_only ["DeltaAttr.sub_1"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
]

Module before type checking:
module DeltaAttr
Declarations: [
irreducible
let myattr = ()
irreducible
let otherattr = ()
let normalize steps x =
(FStar.Stubs.Tactics.V2.Builtins.dup ();
FStar.Tactics.V2.Derived.exact (quote x);
FStar.Stubs.Tactics.V2.Builtins.norm steps;
FStar.Tactics.V2.Derived.trefl ())
<:
FStar.Tactics.Effect.Tac Prims.unit
[@@ DeltaAttr.myattr]
let add_1 x = x + 1 <: Prims.int
[@@ DeltaAttr.myattr]
let sub_1 x = x - 1 <: Prims.int
[@@ DeltaAttr.otherattr]
let add x = x + x <: Prims.int
let test_1 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_2 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_3 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_3' x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"];
FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_4 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_attr ["DeltaAttr.myattr"];
FStar.Pervasives.delta_only ["DeltaAttr.add"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
let test_5 x =
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
DeltaAttr.normalize [
FStar.Pervasives.delta_only ["DeltaAttr.add"];
FStar.Pervasives.delta_only ["DeltaAttr.add_1"];
FStar.Pervasives.delta_only ["DeltaAttr.sub_1"]
]
(DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x))))
<:
Prims.int
]

Module after type checking:
module DeltaAttr
Declarations: [
irreducible
let myattr = ()
irreducible
let otherattr = ()
let normalize steps x =
(FStar.Stubs.Tactics.V2.Builtins.dup ();
(let _ = quote x in
FStar.Tactics.V2.Derived.exact _);
FStar.Stubs.Tactics.V2.Builtins.norm steps;
FStar.Tactics.V2.Derived.trefl ())
<:
FStar.Tactics.Effect.Tac Prims.unit
[@@ DeltaAttr.myattr]
let add_1 x = x + 1 <: Prims.int
[@@ DeltaAttr.myattr]
let sub_1 x = x - 1 <: Prims.int
[@@ DeltaAttr.otherattr]
let add x = x + x <: Prims.int
let test_1 x = DeltaAttr.add (x + 1 - 1) <: Prims.int
let test_2 x =
DeltaAttr.sub_1 (DeltaAttr.add_1 x) + DeltaAttr.sub_1 (DeltaAttr.add_1 x) <: Prims.int
let test_3 x = x + 1 - 1 + (x + 1 - 1) <: Prims.int
let test_3' x = x + 1 - 1 + (x + 1 - 1) <: Prims.int
let test_4 x = x + 1 - 1 + (x + 1 - 1) <: Prims.int
let test_5 x = x + 1 - 1 + (x + 1 - 1) <: Prims.int
]

* Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'calc' in file
"Calc.fst".
- Rename "Calc.fst" to avoid conflicts.

Verified module: DeltaAttr
All verification conditions discharged successfully
2 changes: 2 additions & 0 deletions tests/vale/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,3 +14,5 @@ OTHERFLAGS += \

FSTAR_ROOT ?= ../..
include $(FSTAR_ROOT)/mk/test.mk

$(OUTPUT_DIR)/DeltaAttr.fst.output: FSTAR_ARGS+=--dump_module DeltaAttr

0 comments on commit fb57af6

Please sign in to comment.