Merge pull request #235 from FStarLang/gebner_gensym

Use gensym from F*

Author: gebner

share/pulse/examples/bug-reports/Bug234.fst

@@ -0,0 +1,18 @@
+module Bug234
+#lang-pulse
+open Pulse
+
+type a =
+type b =
+type c =
+type d =
+type f =
+
+let ok (x:a) (y:b) (z:c) (w:d) (u:f) : slprop =
+  emp
+
+let ty (x:a) (y:b) (z:c) (w:d) = u:f -> stt unit emp (fun r -> ok x y z w u)
+
+fn foo x y z w : ty x y z w  = u {
+  fold ok x y z w u;
+}

src/checker/Pulse.Checker.Base.fst

@@ -285,7 +285,7 @@ let st_equiv_post (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
                          slprop_equiv (push_binding g x ppname_default (comp_res c)) 
                                      (open_term (comp_post c) x)
                                      (open_term post x)))
-  : st_typing g t (comp_st_with_post c post)
+  : Dv (st_typing g t (comp_st_with_post c post))
   = if eq_tm post (comp_post c) then d
     else
       let c' = comp_st_with_post c post in
@@ -298,7 +298,7 @@ let st_equiv_post (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
 
 let simplify_post (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
                   (post:term { comp_post c == tm_star post tm_emp})
-  : st_typing g t (comp_st_with_post c post)
+  : Dv (st_typing g t (comp_st_with_post c post))
   = st_equiv_post d post (fun x -> ve_unit_r (push_binding g x ppname_default (comp_res c)) (open_term post x))
 
 let simplify_lemma (c:comp_st) (c':comp_st) (post_hint:option post_hint_t)
@@ -329,7 +329,7 @@ let comp_with_pre (c:comp_st) (pre:term) =
 let st_equiv_pre (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
                  (pre:term)
                  (veq: slprop_equiv g (comp_pre c) pre)
-  : st_typing g t (comp_with_pre c pre)
+  : Dv (st_typing g t (comp_with_pre c pre))
   = if eq_tm pre (comp_pre c) then d
     else
       let c' = comp_with_pre c pre in
@@ -476,7 +476,7 @@ let st_comp_typing_with_post_hint
       (ctxt_typing:tot_typing g ctxt tm_slprop)
       (post_hint:post_hint_opt g { Some? post_hint })
       (c:comp_st { comp_pre c == ctxt /\ comp_post_matches_hint c post_hint })
-: st_comp_typing g (st_comp_of_comp c)
+: Dv (st_comp_typing g (st_comp_of_comp c))
 = let st = st_comp_of_comp c in
   let Some ph = post_hint in
   let post_typing_src
@@ -582,7 +582,7 @@ let emp_inames_included (g:env) (i:term) (_:tot_typing g i tm_inames)
 let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctxt:slprop)
   (ty_typing:universe_of g ty u)
   (post_hint0:post_hint_opt g { Some? post_hint0 /\ checker_res_matches_post_hint g post_hint0 y ty ctxt})
-: Pure (st_typing_in_ctxt g ctxt post_hint0)
+: Div  (st_typing_in_ctxt g ctxt post_hint0)
        (requires lookup g y == Some ty)
        (ensures fun _ -> True)
 = let Some post_hint = post_hint0 in

src/checker/Pulse.Checker.Exists.fst

@@ -123,7 +123,8 @@ let check_intro_exists
   let Tm_ExistsSL u b p = tv in
 
   Pulse.Typing.FV.tot_typing_freevars t_typing;
-  let ty_typing, _ = Metatheory.tm_exists_inversion #g #u #b.binder_ty #p t_typing (fresh g) in
+  let x = fresh g in
+  let ty_typing, _ = Metatheory.tm_exists_inversion #g #u #b.binder_ty #p t_typing x in
   let (| witness, witness_typing |) = 
     check_term g witness T.E_Ghost b.binder_ty in
   let d = T_IntroExists g u b p witness ty_typing t_typing witness_typing in

src/checker/Pulse.Checker.STApp.fst

@@ -44,7 +44,7 @@ let canon_comp_eq_res (g:env) (c:comp_st)
 #pop-options
 
 let canonicalize_st_typing (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
-  : st_typing g t (canon_comp c)
+  : Dv (st_typing g t (canon_comp c))
   = let c' = canon_comp c in
     let x = fresh g in
     assume ( ~(x `Set.mem` freevars (comp_post c)) /\

src/checker/Pulse.Checker.While.fst

@@ -29,12 +29,12 @@ module RU = Pulse.RuntimeUtils
 
 let while_cond_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                            (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_slprop)
-  : comp_typing_u g (comp_while_cond x inv_body)
+  : Dv (comp_typing_u g (comp_while_cond x inv_body))
   = Metatheory.admit_comp_typing g (comp_while_cond x inv_body)
 
 let while_body_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:term)
                            (inv_typing:tot_typing g (tm_exists_sl u (as_binder ty) inv_body) tm_slprop)
-  : comp_typing_u g (comp_while_body x inv_body)
+  : Dv (comp_typing_u g (comp_while_body x inv_body))
   = Metatheory.admit_comp_typing g (comp_while_body x inv_body)
 
 #push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4"

src/checker/Pulse.RuntimeUtils.fsti

@@ -27,6 +27,7 @@ val print_context (c:context) : T.Tac string
 val debug_at_level_no_module (s:string) : bool
 val debug_at_level (g:env) (s:string) : bool
 val print_exn (e:exn) : string
+val next_id () : Dv nat
 val bv_set_range (x:bv) (r:range) : b:bv{b==x}
 val bv_range (x:bv) : range
 val binder_set_range (x:binder) (r:range) : b:binder{b==x}

src/checker/Pulse.Typing.Combinators.fst

@@ -458,7 +458,7 @@ let apply_frame (#g:env)
                 (#c:comp { stateful_comp c })
                 (t_typing: st_typing g t c)
                 (frame_t:frame_for_req_in_ctxt g ctxt (comp_pre c))
-  : Tot (c':comp_st { comp_pre c' == ctxt /\
+  : Dv  (c':comp_st { comp_pre c' == ctxt /\
                       comp_res c' == comp_res c /\
                       comp_u c' == comp_u c /\
                       comp_post c' == tm_star (comp_post c) (frame_of frame_t) } &

src/checker/Pulse.Typing.Combinators.fsti

@@ -93,7 +93,7 @@ val apply_frame (#g:env)
                 (#c:comp { stateful_comp c })
                 (t_typing: st_typing g t c)
                 (frame_t:frame_for_req_in_ctxt g ctxt (comp_pre c))
-  : Tot (c':comp_st { comp_pre c' == ctxt /\
+  : Dv  (c':comp_st { comp_pre c' == ctxt /\
                       comp_res c' == comp_res c /\
                       comp_u c' == comp_u c /\
                       comp_post c' == tm_star (comp_post c) (frame_of frame_t) } &

src/checker/Pulse.Typing.Env.fst

@@ -96,20 +96,10 @@ let push_binding_bs _ _ _ _ = ()
 
 let push_binding_as_map _ _ _ _ = ()
 
-let rec max (bs:list (var & typ)) (current:var)
-  : v:var { current <= v /\ (forall (b:var & typ). List.Tot.memP b bs ==> fst b <= v) } =
-  match bs with
-  | [] -> current
-  | (x, t)::rest ->
-    let current = if x < current then current else x in
-    max rest current
-
 let fresh g =
-  match g.bs with
-  | [] -> 1
-  | (x, _)::bs_rest ->
-    let max = max bs_rest x in
-    max + 1
+  let v = RU.next_id () in
+  assume ~(v `Set.mem` dom g);
+  v
 
 //
 // TODO: Move to ulib

src/checker/Pulse.Typing.Env.fsti

@@ -93,7 +93,7 @@ let lookup (g:env) (x:var) : option typ =
   let m = as_map g in
   if Map.contains m x then Some (Map.sel m x) else None
 
-val fresh (g:env) : v:var { ~ (Set.mem v (dom g)) }
+val fresh (g:env) : Dv (v:var { ~ (Set.mem v (dom g)) })
 
 let contains (g:env) (x:var) = Map.contains (as_map g) x