Merge pull request #3251 from FStarLang/gabriel_dont_normalize_domain…

…_hnf

Do not normalize domains of arrows with HNF.

src/typechecker/FStar.TypeChecker.Env.fsti

@@ -36,7 +36,7 @@ type step =
   | ZetaFull        //fixed points, even under blocked matches
   | Exclude of step //the first three kinds are included by default, unless Excluded explicity
   | Weak            //Do not descend into binders
-  | HNF             //Only produce a head normal form
+  | HNF             //Only produce a head normal form: Do not descend into function arguments or into binder types
   | Primops         //reduce primitive operators like +, -, *, /, etc.
   | Eager_unfolding
   | Inlining

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -1534,7 +1534,8 @@ let rec norm : cfg -> env -> stack -> term -> term =
             then rebuild cfg env stack (closure_as_term cfg env t)
             else let bs, c = open_comp bs c in
                  let c = norm_comp cfg (bs |> List.fold_left (fun env _ -> dummy::env) env) c in
-                 let t = arrow (norm_binders cfg env bs) c in
+                 let bs = if cfg.steps.hnf then (close_binders cfg env bs)._1 else norm_binders cfg env bs in
+                 let t = arrow bs c in
                  rebuild cfg env stack t
 
           | Tm_ascribed {tm=t1; eff_opt=l} when cfg.steps.unascribe ->

tests/tactics/WeakVsHNF.fst

@@ -114,3 +114,26 @@ let _ = assert True
              debug ("WHNF  :  " ^ term_to_string t);
              guard (term_eq t (`(fun () -> W (1 + 1))))
         )
+
+let b = unit
+let _ = assert True
+         by (let t0 = `(b -> b) in
+             debug "";
+             debug ("Term  :  " ^ term_to_string t0);
+
+             let t = norm_term [delta] t0 in
+             debug ("Full  :  " ^ term_to_string t);
+             guard (term_eq t (`(unit -> unit)));
+
+             let t = norm_term [delta; weak] t0 in
+             debug ("Weak  :  " ^ term_to_string t);
+             guard (term_eq t (`(b -> b)));
+
+             let t = norm_term [delta; hnf] t0 in
+             debug ("HNF   :  " ^ term_to_string t);
+             guard (term_eq t (`(b -> unit)));
+
+             let t = norm_term [delta; weak; hnf] t0 in
+             debug ("WHNF  :  " ^ term_to_string t);
+             guard (term_eq t (`(b -> b)))
+        )

ulib/FStar.Pervasives.fsti

@@ -167,7 +167,7 @@ val simplify : norm_step
 (** Weak reduction: Do not reduce under binders *)
 val weak : norm_step
 
-(** Head normal form *)
+(** Head normal form: Do not reduce in function arguments or in binder types *)
 val hnf : norm_step
 
 (** Reduce primitive operators, e.g., [1 + 1 ~> 2] *)