Merge pull request #3964 from mtzguido/lid_range

Syntax: no need to add a range to `var`, a lident already has one

Author: mtzguido

src/basic/FStarC.MachineInts.fst

@@ -158,8 +158,8 @@ instance nbe_machint (k : machint_kind) : Tot (NBE.embedding (machint k)) =
     in
     match a.nbe_t with
     | FV (fv1, [], [(a, _)])
-      when Ident.lid_equals (fv1.fv_name.v) (int_to_t_lid_for k)
-      || Ident.lid_equals (fv1.fv_name.v) (__int_to_t_lid_for k) ->
+      when Ident.lid_equals (fv1.fv_name) (int_to_t_lid_for k)
+      || Ident.lid_equals (fv1.fv_name) (__int_to_t_lid_for k) ->
       let! a : int = unembed e_int cbs a in
       Some (Mk a m)
     | _ -> None

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -360,7 +360,7 @@ let extract_typ_abbrev env quals attrs lb
     //eta expansion is important; see issue #490, including unrefining and unascribing
     let lbdef = FStarC.TypeChecker.Normalize.eta_expand_with_type tcenv lbdef lbtyp in
     let fv = Inr?.v lb.lbname in
-    let lid = fv.fv_name.v in
+    let lid = fv.fv_name in
     let def = SS.compress lbdef |> U.unmeta |> U.un_uinst in
     let def =
         match def.n with
@@ -426,7 +426,7 @@ let extract_let_rec_type env quals attrs lb
     let bs, _ = U.arrow_formals lbtyp in
     let env1, ml_bs = binders_as_mlty_binders env bs in
     let fv = Inr?.v lb.lbname in
-    let lid = fv.fv_name.v in
+    let lid = fv.fv_name in
     let body = MLTY_Top in
     let metadata = extract_metadata attrs @ List.choose flag_of_qual quals in
     let assumed = false in
@@ -565,7 +565,7 @@ let extract_reifiable_effect g ed
         match (SS.compress tm).n with
         | Tm_uinst (tm, _) -> extract_fv tm
         | Tm_fvar fv ->
-            let mlp = mlpath_of_lident g fv.fv_name.v in
+            let mlp = mlpath_of_lident g fv.fv_name in
             let ({exp_b_tscheme=tysc}) = UEnv.lookup_fv tm.pos g fv in
             with_ty MLTY_Top <| MLE_Name mlp, tysc
         | _ -> failwith (Format.fmt2 "(%s) Not an fv: %s"
@@ -1254,7 +1254,7 @@ and extract_sig_let (g:uenv) (se:sigelt) : uenv & list mlmodule1 =
                   then env, ml_lbs
                   else
                       // debug g (fun () -> printfn "Translating source lb %s at type %s to %A" (show lbname) (show t) (must (mllb.mllb_tysc)));
-                      let lb_lid = (Inr?.v lbname).fv_name.v in
+                      let lb_lid = (Inr?.v lbname).fv_name in
                       let flags'' =
                           match (SS.compress t).n with
                           | Tm_arrow {comp={ n = Comp { effect_name = e }}}

src/extraction/FStarC.Extraction.ML.RegEmb.fst

@@ -307,13 +307,13 @@ let rec embedding_for
   all of them, using a name prefix __knot_e, and later define the e_X at the
   top-level by unthunking.
   *)
-  | Tm_fvar fv when List.existsb (Ident.lid_equals fv.fv_name.v) mutuals ->
-    let head = mk <| MLE_Var ("__knot_e_" ^ Ident.string_of_id (Ident.ident_of_lid fv.fv_name.v)) in
+  | Tm_fvar fv when List.existsb (Ident.lid_equals fv.fv_name) mutuals ->
+    let head = mk <| MLE_Var ("__knot_e_" ^ Ident.string_of_id (Ident.ident_of_lid fv.fv_name)) in
     mk (MLE_App (head, [ml_unit]))
 
   (* An fv for which we have an embedding already registered. *)
-  | Tm_fvar fv when Some? (find_fv_embedding' fv.fv_name.v) ->
-    let emb_data = find_fv_embedding fv.fv_name.v in
+  | Tm_fvar fv when Some? (find_fv_embedding' fv.fv_name) ->
+    let emb_data = find_fv_embedding fv.fv_name in
     begin match k with
     | SyntaxTerm -> ml_name emb_data.syn_emb
     | NBETerm ->
@@ -332,7 +332,7 @@ let rec embedding_for
   | Tm_fvar fv when Env.fv_has_attr tcenv fv PC.plugin_attr ->
     begin match k with
     | SyntaxTerm ->
-      let lid = fv.fv_name.v in
+      let lid = fv.fv_name in
       as_name (List.map Ident.string_of_id (Ident.ns_of_lid lid),
                "e_" ^ Ident.string_of_id (Ident.ident_of_lid lid))
     | NBETerm ->
@@ -350,7 +350,7 @@ type wrapped_term = mlexpr & mlexpr & int & bool
 
 let interpret_plugin_as_term_fun (env:UEnv.uenv) (fv:fv) (t:typ) (arity_opt:option int) (ml_fv:mlexpr')
     : option wrapped_term =
-    let fv_lid = fv.fv_name.v in
+    let fv_lid = fv.fv_name in
     let tcenv = UEnv.tcenv_of_uenv env in
     let t = N.normalize [
       Env.EraseUniverses;
@@ -513,7 +513,7 @@ let interpret_plugin_as_term_fun (env:UEnv.uenv) (fv:fv) (t:typ) (arity_opt:opti
         | [] ->
           let arg_unembeddings = List.rev accum_embeddings in
           let res_embedding = embedding_for tcenv [] loc tvar_context result_typ in
-          let fv_lid = fv.fv_name.v in
+          let fv_lid = fv.fv_name in
           if U.is_pure_comp c
           then begin
             let cb = str_to_name "cb" in
@@ -572,7 +572,7 @@ let interpret_plugin_as_term_fun (env:UEnv.uenv) (fv:fv) (t:typ) (arity_opt:opti
         Some (w, w', a, b)
     with
     | NoEmbedding msg ->
-      not_implemented_warning (Ident.range_of_lid fv.fv_name.v)
+      not_implemented_warning (Ident.range_of_lid fv.fv_name)
                               (show fv)
                               msg;
       None
@@ -689,7 +689,7 @@ let __do_handle_plugin (g: uenv) (arity_opt: option int) (se: sigelt) : list mlm
   | Sig_let {lbs} ->
       let mk_registration lb : list mlmodule1 =
          let fv = Inr?.v lb.lbname in
-         let fv_lid = fv.fv_name.v in
+         let fv_lid = fv.fv_name in
          let fv_t = lb.lbtyp in
          let ml_name_str = MLE_Const (MLC_String (Ident.string_of_lid fv_lid)) in
          match interpret_plugin_as_term_fun g fv fv_t arity_opt ml_name_str with

src/extraction/FStarC.Extraction.ML.Term.fst

@@ -180,7 +180,7 @@ let rec is_arity_aux tcenv t =
         FStarC.TypeChecker.Env.lookup_definition
           [Env.Unfold delta_constant]
           tcenv
-          fv.fv_name.v
+          fv.fv_name
       in
       begin
       match topt with
@@ -732,7 +732,7 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty =
                  translate_term_to_mlty g a
             else (
               let formals, _ =
-                let (_, fvty), _ = FStarC.TypeChecker.Env.lookup_lid (tcenv_of_uenv g) fv.fv_name.v in
+                let (_, fvty), _ = FStarC.TypeChecker.Env.lookup_lid (tcenv_of_uenv g) fv.fv_name in
                 let fvty = N.normalize [Env.UnfoldUntil delta_constant; Env.ForExtraction] (tcenv_of_uenv g) fvty in
                 U.arrow_formals fvty in
               let mlargs = List.map (arg_as_mlty g) args in
@@ -742,7 +742,7 @@ let rec translate_term_to_mlty' (g:uenv) (t0:term) : mlty =
                 then let _, rest = BU.first_N n_args formals in
                      mlargs @ (List.map (fun _ -> MLTY_Erased) rest)
                 else mlargs in
-              let nm = UEnv.mlpath_of_lident g fv.fv_name.v in
+              let nm = UEnv.mlpath_of_lident g fv.fv_name in
               MLTY_Named (mlargs, nm)
             )
         )
@@ -1016,7 +1016,7 @@ let rec extract_one_pat (imp : bool)
           | Some ({exp_b_expr={expr=MLE_Name n}; exp_b_tscheme=ttys}) -> n, ttys
           | Some _ -> failwith "Expected a constructor"
           | None ->
-            Errors.raise_error f.fv_name.p  Errors.Error_ErasedCtor
+            Errors.raise_error f Errors.Error_ErasedCtor
               (Format.fmt1 "Cannot extract this pattern, the %s constructor was erased" (show f))
         in
         // The prefix of the pattern are dot patterns matching the type parameters

src/extraction/FStarC.Extraction.ML.UEnv.fst

@@ -181,9 +181,9 @@ let try_lookup_fv (r:Range.t) (g:uenv) (fv:fv) : option exp_binding =
     (* Log an error/warning and return None *)
     let open FStarC.Errors.Msg in
     Errors.log_issue r Errors.Error_CallToErased [
-       text <| Format.fmt1 "Will not extract reference to variable `%s` since it has the `noextract` qualifier." (string_of_lid fv.fv_name.v);
+       text <| Format.fmt1 "Will not extract reference to variable `%s` since it has the `noextract` qualifier." (string_of_lid fv.fv_name);
        text <| Format.fmt2 "Either remove the noextract qualifier from %s (defined in %s) or add it to this definition."
-                 (string_of_lid fv.fv_name.v) (show pos);
+                 (string_of_lid fv.fv_name) (show pos);
        text <| Format.fmt1 "This error can be ignored with `--warn_error -%s`." (show Errors.call_to_erased_errno)];
     None
   | NotFound ->
@@ -195,8 +195,8 @@ let lookup_fv (r:Range.t) (g:uenv) (fv:fv) : exp_binding =
   | Found t -> t
   | res ->
     failwith (Format.fmt3 "Internal error: (%s) free variable %s not found during extraction (res=%s)\n"
-              (Range.string_of_range fv.fv_name.p)
-              (show fv.fv_name.v)
+              (Range.string_of_range (pos fv))
+              (show fv.fv_name)
               (show res))
 
 (** An F* local variable (bv) can be mapped either to
@@ -546,7 +546,7 @@ let extend_fv (g:uenv) (x:fv) (t_x:mltyscheme) (add_unit:bool)
         let ml_ty = match t_x with
             | ([], t) -> t
             | _ -> MLTY_Top in
-        let mlpath, g = new_mlpath_of_lident g x.fv_name.v in
+        let mlpath, g = new_mlpath_of_lident g x.fv_name in
         let mlsymbol = snd mlpath in
         let mly = MLE_Name mlpath in
         let mly = if add_unit then with_ty MLTY_Top <| MLE_App(with_ty MLTY_Top mly, [ml_unit]) else with_ty ml_ty mly in
@@ -575,7 +575,7 @@ let extend_lb (g:uenv) (l:lbname) (t:typ) (t_x:mltyscheme) (add_unit:bool)
 (** Extend with an abbreviation [fv] for the type scheme [ts] *)
 let extend_tydef (g:uenv) (fv:fv) (ts:mltyscheme) (meta:FStarC.Extraction.ML.Syntax.metadata)
   : tydef & mlpath & uenv =
-    let name, g = new_mlpath_of_lident g fv.fv_name.v in
+    let name, g = new_mlpath_of_lident g fv.fv_name in
     let tydef = {
         tydef_fv = fv;
         tydef_mlmodule_name=fst name;
@@ -592,7 +592,7 @@ let extend_with_tydef_declaration u l =
 
 (** Extend with [fv], the identifer for an F* inductive type *)
 let extend_type_name (g:uenv) (fv:fv) : mlpath & uenv =
-  let name, g = new_mlpath_of_lident g fv.fv_name.v in
+  let name, g = new_mlpath_of_lident g fv.fv_name in
   name,
   {g with type_names=(fv,name)::g.type_names}
 

src/fstar/FStarC.CheckedFiles.fst

@@ -34,7 +34,7 @@ let dbg = Debug.get_toggle "CheckedFiles"
  * detect when loading the cache that the version number is same
  * It needs to be kept in sync with Prims.fst
  *)
-let cache_version_number = 74
+let cache_version_number = 75
 
 (*
  * Abbreviation for what we store in the checked files (stages as described below)

src/reflection/FStarC.Reflection.V1.NBEEmbeddings.fst

@@ -58,7 +58,7 @@ let mkFV fv us ts = mkFV fv (List.rev us) (List.rev ts)
 let mkConstruct fv us ts = mkConstruct fv (List.rev us) (List.rev ts)
 (* ^ We still need to match on them in reverse order though, so this is pretty dumb *)
 
-let fv_as_emb_typ fv = S.ET_app (FStarC.Ident.string_of_lid fv.fv_name.v, [])
+let fv_as_emb_typ fv = S.ET_app (FStarC.Ident.string_of_lid fv.fv_name, [])
 let mk_emb' x y fv = mk_emb x y (fun () -> mkFV fv [] []) (fun () -> fv_as_emb_typ fv)
 
 let mk_lazy cb obj ty kind =

src/reflection/FStarC.Reflection.V2.NBEEmbeddings.fst

@@ -54,7 +54,7 @@ let mkFV fv us ts = mkFV fv (List.rev us) (List.rev ts)
 let mkConstruct fv us ts = mkConstruct fv (List.rev us) (List.rev ts)
 (* ^ We still need to match on them in reverse order though, so this is pretty dumb *)
 
-let fv_as_emb_typ fv = S.ET_app (FStarC.Ident.string_of_lid fv.fv_name.v, [])
+let fv_as_emb_typ fv = S.ET_app (FStarC.Ident.string_of_lid fv.fv_name, [])
 let mk_emb' x y fv = mk_emb x y (fun () -> mkFV fv [] []) (fun () -> fv_as_emb_typ fv)
 
 let mk_lazy cb obj ty kind =

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -380,13 +380,13 @@ let primitive_type_axioms : env -> lident -> string -> term -> list decl =
             | Some(_, f) -> f env s tt)
 
 let encode_smt_lemma env fv t =
-    let lid = fv.fv_name.v in
+    let lid = fv.fv_name in
     let form, decls = encode_function_type_as_formula t env in
     decls@([Util.mkAssume(form, Some ("Lemma: " ^ (string_of_lid lid)), ("lemma_"^(string_of_lid lid)))]
            |> mk_decls_trivial)
 
 let encode_free_var uninterpreted env fv tt t_norm quals :decls_t & env_t =
-    let lid = fv.fv_name.v in
+    let lid = fv.fv_name in
     if not <| (U.is_pure_or_ghost_function t_norm || is_smt_reifiable_function env.tcenv t_norm)
     || U.is_lemma t_norm
     || uninterpreted
@@ -560,11 +560,11 @@ let encode_free_var uninterpreted env fv tt t_norm quals :decls_t & env_t =
 
 
 let declare_top_level_let env x t t_norm : fvar_binding & decls_t & env_t =
-  match lookup_fvar_binding env x.fv_name.v with
+  match lookup_fvar_binding env x.fv_name with
   (* Need to introduce a new name decl *)
   | None ->
       let decls, env = encode_free_var false env x t t_norm [] in
-      let fvb = lookup_lid env x.fv_name.v in
+      let fvb = lookup_lid env x.fv_name in
       fvb, decls, env
 
   (* already declared, only need an equation *)
@@ -1267,7 +1267,7 @@ let encode_datacon (env:env_t) (se:sigelt)
             data_arg_params
             arg_params
         in
-        let ty = maybe_curry_fvb fv.fv_name.p encoded_head_fvb arg_vars in
+        let ty = maybe_curry_fvb (pos fv.fv_name) encoded_head_fvb arg_vars in
         let xvars = List.map mkFreeV vars in
         let dapp =  mkApp(ddconstrsym, xvars) in //arity ok; |xvars| = |formals| = arity
         let ty_pred = mk_HasTypeWithFuel (Some s_fuel_tm) dapp ty in
@@ -1632,7 +1632,7 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t & env_t) =
           || se.sigattrs |> BU.for_some is_opaque_to_smt ->
        let attrs = se.sigattrs in
        let env, decls = BU.fold_map (fun env lb ->
-        let lid = (Inr?.v lb.lbname).fv_name.v in
+        let lid = (Inr?.v lb.lbname).fv_name in
         if None? <| Env.try_lookup_val_decl env.tcenv lid
         then let val_decl = { se with sigel = Sig_declare_typ {lid; us=lb.lbunivs; t=lb.lbtyp};
                                       sigquals = S.Irreducible :: se.sigquals } in
@@ -1643,12 +1643,12 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t & env_t) =
 
      (* Special encoding for b2t *)
      | Sig_let {lbs=(_, [{lbname=Inr b2t}])} when S.fv_eq_lid b2t Const.b2t_lid ->
-       let tname, ttok, env = new_term_constant_and_tok_from_lid env b2t.fv_name.v 1 in
+       let tname, ttok, env = new_term_constant_and_tok_from_lid env b2t.fv_name 1 in
        let xx = mk_fv ("x", Term_sort) in
        let x = mkFreeV xx in
        let b2t_x = mkApp("Prims.b2t", [x]) in
        let valid_b2t_x = mkApp("Valid", [b2t_x]) in //NS: Explicitly avoid the Vaild(b2t t) inlining
-       let bool_ty = lookup_free_var env (withsort Const.bool_lid) in
+       let bool_ty = lookup_free_var env Const.bool_lid in
        let decls = [Term.DeclFun(tname, [Term_sort], Term_sort, None);
                     Util.mkAssume(mkForall (S.range_of_fv b2t) ([[b2t_x]], [xx],
                                            mkEq(valid_b2t_x, mkApp(snd boxBoolFun, [x]))),
@@ -1682,7 +1682,7 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t & env_t) =
      //Projectors are also are encoded directly via (our encoding of) theory of datatypes
      //Except in some cases where the front-end does not emit a declare_typ for some projector, because it doesn't know how to compute it
      let fv = Inr?.v lb.lbname in
-     let l = fv.fv_name.v in
+     let l = fv.fv_name in
      begin match try_lookup_free_var env l with
         | Some _ ->
           [], env //already encoded

src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst

@@ -88,7 +88,7 @@ let head_normal env t =
     | Tm_abs _
     | Tm_constant _ -> true
     | Tm_fvar fv
-    | Tm_app {hd={n=Tm_fvar fv}} -> Env.lookup_definition [Env.Eager_unfolding_only] env.tcenv fv.fv_name.v |> None?
+    | Tm_app {hd={n=Tm_fvar fv}} -> Env.lookup_definition [Env.Eager_unfolding_only] env.tcenv fv.fv_name |> None?
     | _ -> false
 
 let head_redex env t =
@@ -99,7 +99,7 @@ let head_redex env t =
       || List.existsb (function TOTAL -> true | _ -> false) rc.residual_flags
 
     | Tm_fvar fv ->
-      Env.lookup_definition [Env.Eager_unfolding_only] env.tcenv fv.fv_name.v |> Some?
+      Env.lookup_definition [Env.Eager_unfolding_only] env.tcenv fv.fv_name |> Some?
 
     | _ -> false
 
@@ -1155,7 +1155,7 @@ and encode_term (t:typ) (env:env_t) : (term         (* encoding of t, expects t
                 | Tm_uinst({n=Tm_name x}, _)
                 | Tm_name x -> Some x.sort
                 | Tm_uinst({n=Tm_fvar fv}, _)
-                | Tm_fvar fv -> Some (Env.lookup_lid env.tcenv fv.fv_name.v |> fst |> snd)
+                | Tm_fvar fv -> Some (Env.lookup_lid env.tcenv fv.fv_name |> fst |> snd)
                 | Tm_ascribed {asc=(Inl t, _, _)} -> Some t
                 | Tm_ascribed {asc=(Inr c, _, _)} -> Some (U.comp_result c)
                 | _ -> None
@@ -1413,13 +1413,13 @@ and encode_pat (env:env_t) (pat:S.pat) : (env_t & pattern) =
             mkEq(scrutinee, tm)
         | Pat_cons(f, _, args) ->
             let is_f =
-                let tc_name = Env.typ_of_datacon env.tcenv f.fv_name.v in
+                let tc_name = Env.typ_of_datacon env.tcenv f.fv_name in
                 match Env.datacons_of_typ env.tcenv tc_name with
                 | _, [_] -> mkTrue //single constructor type; no need for a test
-                | _ -> mk_data_tester env f.fv_name.v scrutinee
+                | _ -> mk_data_tester env f.fv_name scrutinee
             in
             let sub_term_guards = args |> List.mapi (fun i (arg, _) ->
-                let proj = primitive_projector_by_pos env.tcenv f.fv_name.v i in
+                let proj = primitive_projector_by_pos env.tcenv f.fv_name i in
                 mk_guard arg (mkApp(proj, [scrutinee]))) in //arity ok, primitive projector (#1383)
             mk_and_l (is_f::sub_term_guards)
     in
@@ -1434,7 +1434,7 @@ and encode_pat (env:env_t) (pat:S.pat) : (env_t & pattern) =
         | Pat_cons(f, _, args) ->
             args
             |> List.mapi (fun i (arg, _) ->
-                let proj = primitive_projector_by_pos env.tcenv f.fv_name.v i in
+                let proj = primitive_projector_by_pos env.tcenv f.fv_name i in
                 mk_projections arg (mkApp(proj, [scrutinee]))) //arity ok, primitive projector (#1383)
             |> List.flatten
     in