WIP using core, for phase2

Author: mtzguido

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -457,6 +457,15 @@ let tc_sig_let env r se lbs lids : list sigelt & list sigelt & Env.env =
     (* 2. Turn the top-level lb into a Tm_let with a unit body *)
     let e = mk (Tm_let {lbs=(fst lbs, lbs'); body=mk (Tm_constant (Const_unit)) r}) r in
 
+    (* For the second phase (if any), we will call the core typechecker
+       for terms marked with a @@"core" attribute, or if the extension
+       "core_phase2" is enabled. *)
+    let use_core =
+      do_two_phases env && (
+        Options.Ext.enabled "core_phase2"
+        || List.existsb (U.term_eq (U.exp_string "core")) se.sigattrs)
+    in
+
     (* 3. Type-check the Tm_let and convert it back to Sig_let *)
     let env' = { env with top_level = true; generalize = should_generalize } in
     let e =
@@ -493,14 +502,25 @@ let tc_sig_let env r se lbs lids : list sigelt & list sigelt & Env.env =
         if Debug.medium () || !dbg_TwoPhases then
           Format.print1 "Let binding after phase 1, before removing uvars: %s\n" (show e);
 
-        let e = N.remove_uvar_solutions env' e |> drop_lbtyp in
+        let e = N.remove_uvar_solutions env' e in
+
+        (* Wart: the normal typechecker drops the lbtyp to avoid double
+        ascriptions. But we need it to call the core checker. *)
+        let e =
+          if use_core
+          then e
+          else drop_lbtyp e
+        in
 
         if Debug.medium () || !dbg_TwoPhases then
           Format.print1 "Let binding after phase 1, uvars removed: %s\n" (show e);
         e)
       else e
     in
 
+    (* Phony, just so that we can print the result from Core below. *)
+    let _ : Class.Show.showable Core.guard_commit_token_cb = { show = (fun _ -> "_") } in
+
     let env' =
         match (SS.compress e).n with
         | Tm_let {lbs} ->
@@ -511,12 +531,53 @@ let tc_sig_let env r se lbs lids : list sigelt & list sigelt & Env.env =
     in
     Errors.stop_if_err ();
     let r =
-        //We already generalized phase1; don't need to generalize again
-      let should_generalize = not (do_two_phases env') in
-      Profiling.profile (fun () -> tc_maybe_toplevel_term { env' with generalize = should_generalize } e)
-                        (Some (Ident.string_of_lid (Env.current_module env)))
-                        "FStarC.TypeChecker.Tc.tc_sig_let-tc-phase2"
+      let fallback () =
+        // We already generalized phase1; don't need to generalize again
+        let should_generalize = not (do_two_phases env') in
+        Profiling.profile (fun () -> tc_maybe_toplevel_term { env' with generalize = should_generalize } e)
+                          (Some (Ident.string_of_lid (Env.current_module env)))
+                          "FStarC.TypeChecker.Tc.tc_sig_let-tc-phase2"
+      in
+      if not use_core then
+        fallback ()
+      else (
+        if Debug.any () then
+          Format.print1 "Using core as phase2 for let binding: %s\n" (show e);
+        match (SS.compress e).n with
+        | Tm_let {lbs=(_, [lb])} -> (
+          // Format.print1 "GGG lbdef = %s\n" (show lb.lbdef);
+          // Format.print1 "GGG lbtyp = %s\n" (show lb.lbtyp);
+          let env'= push_univ_vars env' lb.lbunivs in
+          let _, def = SS.open_univ_vars lb.lbunivs lb.lbdef in
+          let _, typ = SS.open_univ_vars lb.lbunivs lb.lbtyp in
+          let core_res = Core.check_term env' def typ true in
+          // Format.print1 "Core computed type: %s\n" (show core_res);
+          match core_res with
+          | Inl gopt ->
+            begin match gopt with
+            | Some (g, _) -> ignore (Rel.discharge_guard env' (Env.guard_of_guard_formula (NonTrivial g)))
+            | None -> ()
+            end;
+            // Format.print1 "Core type: %s\n" (show typ);
+            let lcomp =
+              // match tg with
+              // | Core.E_Total ->
+              lcomp_of_comp (S.mk_Total typ)
+              // | Core.E_Ghost -> lcomp_of_comp (S.mk_GTotal typ)
+            in
+            e, lcomp, Env.trivial_guard
+
+          | Inr err ->
+            let open FStarC.Pprint in
+            Errors.diag e [
+              text "Core (for phase 2) failed:" ^/^ doc_of_string (show err);
+            ];
+            fallback ()
+        )
+        | _ -> failwith "unexpected: not a let"
+      )
     in
+
     let se, lbs = match r with
       | {n=Tm_let {lbs; body=e}}, _, g when Env.is_trivial g ->
         U.check_mutual_universes (snd lbs);

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -3977,12 +3977,13 @@ and check_inner_let env e =
        let _ =
         if (is_inline_let || is_inline_let_vc)  //inline let is allowed only if it is pure or ghost
         && not (pure_or_ghost || Env.is_erasable_effect env c1.eff_name)  //inline let is allowed on erasable effects
-        then raise_error e1
-               Errors.Fatal_ExpectedPureExpression
-               (Format.fmt2 "Definitions marked @inline_let are expected to be pure or ghost; \
-                            got an expression \"%s\" with effect \"%s\""
-                             (show e1)
-                             (show c1.eff_name))
+        then
+          let open FStarC.Pprint in
+          raise_error e1 Errors.Fatal_ExpectedPureExpression [
+               text "Definitions marked @inline_let are expected to be pure or ghost.";
+               prefix 2 1 (text "Got an expression") (pp e1) ^/^
+               prefix 2 1 (text "with effect") (pp c1.eff_name) ^^ dot;
+          ]
        in
        let x = {Inl?.v lb.lbname with sort=c1.res_typ} in
        let xb, e2 = SS.open_term [S.mk_binder x] e2 in
@@ -4380,8 +4381,10 @@ and check_let_bound_def top_level env lb
     (* 1. extract the annotation of the let-bound term, e1, if any *)
     let topt, wf_annot, univ_vars, univ_opening, env1 = check_lbtyp top_level env lb in
 
-    if not top_level && univ_vars <> []
-    then raise_error e1 Errors.Fatal_UniversePolymorphicInnerLetBound "Inner let-bound definitions cannot be universe polymorphic";
+    if not top_level && univ_vars <> [] then
+      raise_error e1 Errors.Fatal_UniversePolymorphicInnerLetBound [
+        text "Inner let-bound definitions cannot be universe polymorphic."
+      ];
 
     (* 2. type-check e1 *)
     (* Only toplevel terms should have universe openings *)