Removing term from Pulse AST, instead use F* reflection terms and expose a term view to the Pulse checker

src/checker/Pulse.Checker.Abs.fst

@@ -41,11 +41,11 @@ let debug_abs g (s: unit -> T.Tac string) : T.Tac unit =
 (* Infers the the type of the binders from the specification alone, not the body *)
 
 let range_of_st_comp (st:st_comp) =
-  RU.union_ranges (st.pre.range) (st.post.range)
+  RU.union_ranges (RU.range_of_term st.pre) (RU.range_of_term st.post)
 
 let range_of_comp (c:comp) =
   match c with
-  | C_Tot t -> t.range
+  | C_Tot t -> RU.range_of_term t
   | C_ST st -> range_of_st_comp st
   | C_STAtomic _ _ st -> range_of_st_comp st
   | C_STGhost st -> range_of_st_comp st
@@ -68,31 +68,25 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
         let arr, body = arrow_of_abs env body in
         let arr = close_term arr x in
         let body = close_st_term body x in
-        let ty : term = { tm_arrow b q (C_Tot arr) with range = RU.union_ranges b.binder_ty.range arr.range } in
+        let ty : term = wr (tm_arrow b q (C_Tot arr))
+                           (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term arr)) in
         let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body}} in
         ty, prog
 
       | Some c -> ( //we have an annotation
         let c = open_comp_with c (U.term_of_nvar px) in
         match c with
         | C_Tot tannot -> (
-          let tannot' = RU.hnf_lax (elab_env env) (elab_term tannot) in
-          match Pulse.Readback.readback_ty tannot' with
-          | None -> 
-            Env.fail 
-              env 
-              (Some prog.range) 
-              (Printf.sprintf "Unexpected type of abstraction, expected an arrow, got: %s"
-                  (T.term_to_string tannot'))
-          | Some t ->
-            //retain the original annotation, so that we check it wrt the inferred type in maybe_rewrite_body_typing
-            let t = close_term t x in
-            let annot = close_comp c x in
-            let ty : term = { tm_arrow b q (C_Tot t) with range = RU.union_ranges b.binder_ty.range t.range } in
-            let ascription = { annotated = Some annot; elaborated = None } in
-            let body = close_st_term body x in
-            let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in
-            ty, prog
+          let t = RU.hnf_lax (elab_env env) (elab_term tannot) in
+          //retain the original annotation, so that we check it wrt the inferred type in maybe_rewrite_body_typing
+          let t = close_term t x in
+          let annot = close_comp c x in
+          let ty : term = wr (tm_arrow b q (C_Tot t))
+                             (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term t)) in
+          let ascription = { annotated = Some annot; elaborated = None } in
+          let body = close_st_term body x in
+          let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in
+          ty, prog
         )
 
         | _ ->
@@ -109,7 +103,8 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term })
         Env.fail env (Some prog.range) "Unannotated function body"
 
       | Some c -> ( //we're taking the annotation as is; remove it from the abstraction to avoid rechecking it
-        let ty : term = { tm_arrow b q c with range = RU.union_ranges b.binder_ty.range (range_of_comp c) } in
+        let ty : term = wr (tm_arrow b q c)
+                                 (RU.union_ranges (RU.range_of_term b.binder_ty) (range_of_comp c)) in
         let ascription = empty_ascription in
         let body = close_st_term body x in
         let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in
@@ -134,10 +129,10 @@ let rec rebuild_abs (g:env) (t:st_term) (annot:T.term)
     | Tm_Abs { b; q; ascription=asc; body }, R.Tv_Arrow b' c' -> (
       let b' = T.inspect_binder b' in
       qualifier_compat g b.binder_ppname.range q b'.qual;
-      let ty = readback_ty b'.sort in
+      let ty = b'.sort in
       let comp = R.inspect_comp c' in
-      match ty, comp with
-      | Some ty, T.C_Total res_ty -> (
+      match comp with
+      | T.C_Total res_ty -> (
         if Tm_Abs? body.term
         then (
           let b = mk_binder_with_attrs ty b.binder_ppname b.binder_attrs in
@@ -188,15 +183,9 @@ let preprocess_abs
   = let annot, t = arrow_of_abs g t in
     debug_abs g (fun _ -> Printf.sprintf "arrow_of_abs = %s\n" (P.term_to_string annot));
     let annot, _ = Pulse.Checker.Pure.instantiate_term_implicits g annot in
-    match annot.t with
-    | Tm_FStar annot ->
-      let abs = rebuild_abs g t annot in
-      debug_abs g (fun _ -> Printf.sprintf "rebuild_abs = %s\n" (P.st_term_to_string abs));
-      abs
-    | _ ->
-      Env.fail g (Some t.range) 
-                 (Printf.sprintf "Expected an arrow type as an annotation, got %s"
-                          (P.term_to_string annot))
+    let abs = rebuild_abs g t annot in
+    debug_abs g (fun _ -> Printf.sprintf "rebuild_abs = %s\n" (P.st_term_to_string abs));
+    abs
 
 let sub_effect_comp g r (asc:comp_ascription) (c_computed:comp) : T.Tac (option (c2:comp & lift_comp g c_computed c2)) =
   let nop = None in
@@ -251,7 +240,7 @@ let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac
       let tok = T.with_policy T.SMTSync (fun () -> try_check_prop_validity g phi typing) in
       if None? tok then (
         let open Pulse.PP in
-        fail_doc g (Some i.range) [
+        fail_doc g (Some (RU.range_of_term i)) [
           prefix 4 1 (text "Annotated effect expects only invariants in") (pp i) ^/^
           prefix 4 1 (text "to be opened; but computed effect claims that invariants") (pp j) ^/^
           text "are opened"
@@ -306,7 +295,7 @@ let maybe_rewrite_body_typing
     )
     | Some c -> 
       let st = st_comp_of_comp c in
-      Env.fail g (Some st.pre.range) "Unexpected annotation on a function body"
+      Env.fail g (Some (RU.range_of_term st.pre)) "Unexpected annotation on a function body"
 
 let open_ascription (c:comp_ascription) (nv:nvar) : comp_ascription =
   let t = term_of_nvar nv in

src/checker/Pulse.Checker.Admit.fst

@@ -91,7 +91,9 @@ let check_core
 
   assume (open_term (close_term post_opened x) x == post_opened);
   let d = T_Admit _ _ c (STC _ s x t_typing pre_typing post_typing) in
-  prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname) post_hint t.range
+  prove_post_hint (try_frame_pre pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname)
+                  post_hint
+                  (Pulse.RuntimeUtils.range_of_term t)
 
 let check
     (g:env)
@@ -109,7 +111,3 @@ let check
       check_core g pre pre_typing post_hint res_ppname ({ t with term=Tm_Admit {r with ctag=ct}})
     | _ ->
       check_core g pre pre_typing post_hint res_ppname t
-
-
-
-

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -48,9 +48,6 @@ let rec refl_abs_binders (t:R.term) (acc:list binder) : T.Tac (list binder) =
   match inspect_ln t with
   | Tv_Abs b body ->
     let {sort; ppname} = R.inspect_binder b in
-    let sort = option_must (readback_ty sort)
-      (Printf.sprintf "Failed to readback elaborated binder sort %s in refl_abs_binders"
-         (T.term_to_string sort)) in
     refl_abs_binders body
      ((mk_binder_ppname sort (mk_ppname ppname (RU.range_of_term t)))::acc)
   | _ -> L.rev acc  
@@ -60,12 +57,9 @@ let infer_binder_types (g:env) (bs:list binder) (v:vprop)
   match bs with
   | [] -> []
   | _ ->
-    let g = push_context g "infer_binder_types" v.range in
+    let v_rng = Pulse.RuntimeUtils.range_of_term v in
+    let g = push_context g "infer_binder_types" v_rng in
     let tv = elab_term v in
-    if not (is_host_term tv)
-    then fail g (Some v.range)
-           (Printf.sprintf "assert.infer_binder_types: elaborated %s to %s, which failed the host term check"
-              (P.term_to_string v) (T.term_to_string tv));
     let as_binder (b:binder) : R.binder =
       let open R in
       let bv : binder_view = 
@@ -77,16 +71,14 @@ let infer_binder_types (g:env) (bs:list binder) (v:vprop)
     in
     let abstraction = 
       L.fold_right 
-        (fun b (tv:host_term) -> 
+        (fun b (tv:term) -> 
          let b = as_binder b in
          R.pack_ln (R.Tv_Abs b tv))
         bs
         tv
     in
-    let inst_abstraction, _ = PC.instantiate_term_implicits g (tm_fstar abstraction v.range) in
-    match inst_abstraction.t with
-    | Tm_FStar t -> refl_abs_binders t []
-    | _ -> T.fail "Impossible: instantiated abstraction is not embedded F* term, please file a bug-report"
+    let inst_abstraction, _ = PC.instantiate_term_implicits g (wr abstraction v_rng) in
+    refl_abs_binders inst_abstraction []
 
 let rec open_binders (g:env) (bs:list binder) (uvs:env { disjoint uvs g }) (v:term) (body:st_term)
   : T.Tac (uvs:env { disjoint uvs g } & term & st_term) =
@@ -137,23 +129,19 @@ let unfold_defs (g:env) (defs:option (list string)) (t:term)
           | None -> []
         in
         let rt = RU.unfold_def (fstar_env g) head fully t in
-        let rt = option_must rt
-          (Printf.sprintf "unfolding %s returned None" (T.term_to_string t)) in
-        let ty = option_must (readback_ty rt)
-          (Printf.sprintf "error in reading back the unfolded term %s" (T.term_to_string rt)) in
-        debug_log g (fun _ -> Printf.sprintf "Unfolded %s to F* term %s and readback as %s" (T.term_to_string t) (T.term_to_string rt) (P.term_to_string ty));
-        ty
+        option_must rt
+          (Printf.sprintf "unfolding %s returned None" (T.term_to_string t))
       )
     | _ ->
       fail g (Some (RU.range_of_term t))
         (Printf.sprintf "Cannot unfold %s, the head is not an fvar" (T.term_to_string t))
 
-let check_unfoldable g (v:term) : T.Tac unit = 
-  match v.t with
-  | Tm_FStar _ -> ()
+let check_unfoldable g (v:term) : T.Tac unit =
+  match inspect_term v with
+  | None -> ()
   | _ -> 
    fail g 
-      (Some v.range)
+      (Some (Pulse.RuntimeUtils.range_of_term v))
       (Printf.sprintf "`fold` and `unfold` expect a single user-defined predicate as an argument, \
                         but %s is a primitive term that cannot be folded or unfolded"
                         (P.term_to_string v))
@@ -168,31 +156,9 @@ let visit_and_rewrite (p: (R.term & R.term)) (t:term) : T.Tac term =
   | R.Tv_Var n -> (
     let nv = R.inspect_namedv n in
     assume (is_host_term rhs);
-    subst_term t [NT nv.uniq { t = Tm_FStar rhs; range = t.range }]
+    subst_term t [NT nv.uniq (wr rhs (Pulse.RuntimeUtils.range_of_term t))]
     ) 
-  | _ ->
-    let rec aux (t:term) : T.Tac term =
-      match t.t with
-      | Tm_Emp
-      | Tm_VProp
-      | Tm_Inames
-      | Tm_EmpInames
-      | Tm_Inames
-      | Tm_Unknown  -> t
-      | Tm_Inv i ->
-        { t with t = Tm_Inv (aux i) }
-      | Tm_AddInv i is ->
-        { t with t = Tm_AddInv (aux i) (aux is) }
-      | Tm_Pure p -> { t with t = Tm_Pure (aux p) }
-      | Tm_Star l r ->  { t with t = Tm_Star (aux l) (aux r) }
-      | Tm_ExistsSL u b body -> { t with t = Tm_ExistsSL u { b with binder_ty=aux b.binder_ty} (aux body) }
-      | Tm_ForallSL u b body -> { t with t = Tm_ForallSL u { b with binder_ty=aux b.binder_ty} (aux body) }
-      | Tm_FStar h -> 
-        let h = FStar.Tactics.Visit.visit_tm visitor h in
-        assume (is_host_term h);
-        { t with t=Tm_FStar h }
-    in
-    aux t
+  | _ -> FStar.Tactics.Visit.visit_tm visitor t
 
 let visit_and_rewrite_conjuncts (p: (R.term & R.term)) (tms:list term) : T.Tac (list term) =
   T.map (visit_and_rewrite p) tms
@@ -227,22 +193,19 @@ let rec as_subst (p : list (term & term))
     then Some out
     else None
   | (e1, e2)::p -> (
-    match e1.t with
-    | Tm_FStar e1 -> ( 
-      match R.inspect_ln e1 with
-      | R.Tv_Var n -> (
-        let nv = R.inspect_namedv n in
-        as_subst p 
-          (NT nv.uniq e2::out) 
-          (nv.uniq ::domain )
-          (Set.union codomain (freevars e2))
-      ) 
-      | _ -> None
-    )
+    match R.inspect_ln e1 with
+    | R.Tv_Var n -> (
+      let nv = R.inspect_namedv n in
+      as_subst p 
+        (NT nv.uniq e2::out) 
+        (nv.uniq ::domain )
+        (Set.union codomain (freevars e2))
+    ) 
     | _ -> None
   )
 
 
+
 let rewrite_all (g:env) (p: list (term & term)) (t:term) : T.Tac (term & term) =
   match as_subst p [] [] Set.empty with
   | Some s ->
@@ -309,7 +272,9 @@ let check_wild
 
   | _ ->
     let vprops = Pulse.Typing.Combinators.vprop_as_list pre in
-    let ex, rest = List.Tot.partition (fun (v:vprop) -> Tm_ExistsSL? v.t) vprops in
+    let ex, rest = List.Tot.partition (fun (v:vprop) ->
+                                       let vopt = inspect_term v in
+                                       Some? vopt && Tm_ExistsSL? (Some?.v vopt)) vprops in
     match ex with
     | []
     | _::_::_ ->
@@ -323,8 +288,8 @@ let check_wild
           { st with term = Tm_ProofHintWithBinders { ht with hint_type = ASSERT { p = ex_body } }}
         )
         else (
-          match t.t with
-          | Tm_ExistsSL u b body -> peel_binders (n-1) body
+          match inspect_term t with
+          | Some (Tm_ExistsSL u b body) -> peel_binders (n-1) body
           | _ -> 
             fail g (Some st.range)
                (Printf.sprintf "Expected an existential quantifier with at least %d binders; but only found %s with %d binders"
@@ -448,7 +413,7 @@ let check
                                    t2 = rhs };
                range = st.range;
                effect_tag = as_effect_hint STT_Ghost } in
-    let st = { term = Tm_Bind { binder = as_binder (tm_fstar (`unit) st.range);
+    let st = { term = Tm_Bind { binder = as_binder (wr (`unit) st.range);
                                 head = rw; body };
                range = st.range;
                effect_tag = body.effect_tag } in