From c37b4fe14d912758eca96c03cb0577beb404dc2e Mon Sep 17 00:00:00 2001 From: Benjamin Bonneau Date: Thu, 28 Jul 2022 16:25:20 +0200 Subject: [PATCH] Switch to a custom F* version To have access to the `unascribe` normalisation step --- .versions | 2 +- experiment/Experiment.Steel.fst | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/.versions b/.versions index 7d503b8..a297dd0 100644 --- a/.versions +++ b/.versions @@ -1,2 +1,2 @@ -F* : master a46a208c59b502b427e300e7a9e7b7cf9fb58ad7 +F* : custom d64d37ee546aaf7bdaaaae37a5504c285fce3a5e KRML : master 82169f72d593ed74632d89a6ea6e1f571523fc4a diff --git a/experiment/Experiment.Steel.fst b/experiment/Experiment.Steel.fst index 2375b7e..7a28039 100644 --- a/experiment/Experiment.Steel.fst +++ b/experiment/Experiment.Steel.fst @@ -154,7 +154,7 @@ let __normal_M : list norm_step = [ `%L.map; `%SE.Mkvprop'?.t; `%UV.lift_dom]; delta_attr [`%__tac_helper__; `%__repr_M__; `%SE.__reduce__]; delta_qualifier ["unfold"]; - iota; zeta + iota; zeta; unascribe ] let __normal_lc_sub_push : list norm_step = [ @@ -165,7 +165,7 @@ let __normal_lc_sub_push : list norm_step = [ `%Perm.perm_f_cons_snoc]); delta_attr [`%LV.__lin_cond__; `%Msk.__mask__; `%__tac_helper__]; delta_qualifier ["unfold"]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_LV2SF : list norm_step = [ @@ -179,14 +179,14 @@ let __normal_LV2SF : list norm_step = [ `%Mktuple2?._1; `%Mktuple2?._2]; delta_attr [`%__LV2SF__; `%LV.__lin_cond__; `%Msk.__mask__; `%__tac_helper__; `%SE.__reduce__]; delta_qualifier ["unfold"]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_Fun : list norm_step = [ delta_only [`%SF2Fun.repr_Fun_of_SF; `%SF2Fun.shape_Fun_of_SF; `%SF.Mkprog_shape?.post_len; `%SF.Mkprog_shape?.shp]; delta_qualifier ["unfold"]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_Fun_elim_returns_0 : list norm_step = [ @@ -203,7 +203,7 @@ let __normal_Fun_elim_returns_0 : list norm_step = [ `%L.length; `%L.index; `%L.hd; `%L.tl; `%L.tail; `%Ll.initi ]; delta_qualifier ["unfold"]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_Fun_elim_returns_1 : list norm_step = [ @@ -223,7 +223,7 @@ let __normal_Fun_spec : list norm_step = [ `%Vpl.vprop_of_list; `%Vpl.vprop_of_list']; delta_qualifier ["unfold"]; delta_attr [`%SE.__steel_reduce__; `%Msk.__mask__; `%UV.__universe__]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_vprop_list : list norm_step = [ @@ -232,12 +232,12 @@ let __normal_vprop_list : list norm_step = [ `%Dl.index; `%Dl.initi_g; `%L.length; `%L.index; `%L.map; `%L.hd; `%L.tl; `%L.tail]; delta_attr [`%SE.__reduce__]; - iota; zeta; primops + iota; zeta; primops; unascribe ] let __normal_extract : list norm_step = [ delta_qualifier ["inline_for_extraction"; "unfold"]; - iota; zeta; primops + iota; zeta; primops; unascribe ]