Fix embedding of ident (fixes FStarLang#2444)

W95Psp · Feb 4, 2022 · 3ce15e0 · 3ce15e0
1 parent c66cc0e
commit 3ce15e0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/src/reflection/FStar.Reflection.Embeddings.fs b/src/reflection/FStar.Reflection.Embeddings.fs
@@ -613,10 +613,10 @@ let e_sigelt =
     mk_emb embed_sigelt unembed_sigelt fstar_refl_sigelt
 
 let e_ident : embedding<I.ident> =
-    let repr = e_tuple2 e_string e_range in
+    let repr = e_tuple2 e_range e_string in
     embed_as repr
-             I.mk_ident
-             (fun i -> I.string_of_id i, I.range_of_id i)
+             (fun (r, s) -> I.mk_ident (s, r))
+             (fun i -> I.range_of_id i, I.string_of_id i)
              (Some fstar_refl_ident)
 
 let e_univ_name =

diff --git a/src/reflection/FStar.Reflection.NBEEmbeddings.fs b/src/reflection/FStar.Reflection.NBEEmbeddings.fs
@@ -565,13 +565,13 @@ let e_sigelt =
 // embed_as : ('a -> 'b) -> ('b -> 'a) -> embedding<'a> -> embedding<'b>
 // so we don't write these things
 let e_ident : embedding<I.ident> =
-    let repr = e_tuple2 e_range e_string in
+    let repr = e_tuple2 e_string e_range in
     let embed_ident cb (i:I.ident) : t =
-        embed repr cb (I.range_of_id i, I.string_of_id i)
+        embed repr cb (I.string_of_id i, I.range_of_id i)
     in
     let unembed_ident cb (t:t) : option<I.ident> =
         match unembed repr cb t with
-        | Some (rng, s) -> Some (I.mk_ident (s, rng))
+        | Some (rng, s) -> Some (I.mk_ident (rng, s))
         | None -> None
     in
     let range_fv = (lid_as_fv PC.range_lid  delta_constant None) in