Fixing inconsistencies in inspect_ln

examples/dsls/Makefile.include

@@ -42,7 +42,4 @@ extract_all: $(ALL_ML_FILES)
 clean:
 	rm -rf .depend ._depend
 
-%.fst-in %.fsti-in: $(CACHE_DIR)
-	@echo --include ../core --include $(CACHE_DIR)
-
 .PHONY: verify_all extract_all

examples/dsls/mini_steel/Pulse.Main.fst

@@ -194,8 +194,8 @@ let translate_binder (g:R.env) (b:R.binder)
       let b_ty' = readback_maybe_unknown_ty bv_view.bv_sort in      
       Inl ({binder_ty=b_ty';binder_ppname=bv_view.bv_ppname}, q)
 
-let is_head_fv (t:R.term) (fv:list string) : option (list R.argv) = 
-  let head, args = R.collect_app t in
+let is_head_fv (t:R.term) (fv:list string) : T.Tac (option (list R.argv)) = 
+  let head, args = T.collect_app t in
   match R.inspect_ln head with
   | R.Tv_FVar fv' -> 
     if inspect_fv fv' = fv
@@ -366,7 +366,7 @@ let rec map_err (f:'a -> T.Tac (err 'b)) (l:list 'a)
 let translate_intro (g:RT.fstar_top_env) (t:R.term)
   : T.Tac (err st_term)
   = let open R in
-    let head, args = R.collect_app t in
+    let head, args = T.collect_app t in
     match inspect_ln head with
     | Tv_UInst fv _
     | Tv_FVar fv ->
@@ -392,7 +392,7 @@ let translate_intro (g:RT.fstar_top_env) (t:R.term)
 let translate_admit (g:RT.fstar_top_env) (t:R.term)
   : T.Tac (err st_term)
   = let open R in
-    let head, args = R.collect_app t in
+    let head, args = T.collect_app t in
     match inspect_ln head, args with
     | Tv_UInst v _, [(t, _)]
     | Tv_FVar v, [(t, _)] ->  
@@ -536,7 +536,7 @@ and translate_term (g:RT.fstar_top_env) (t:R.term)
 and translate_while (g:RT.fstar_top_env) (t:R.term)
   : T.Tac (err st_term)
   = let open R in
-    let head, args = R.collect_app t in
+    let head, args = T.collect_app t in
     match inspect_ln head with
     | Tv_FVar v ->
       if inspect_fv v = while_fv
@@ -571,7 +571,7 @@ and translate_rewrite (g:RT.fstar_top_env) (t:R.term)
   : T.Tac (err st_term) =
 
   let open R in
-		let head, args = R.collect_app t in
+		let head, args = T.collect_app t in
 		match inspect_ln head with
 		| Tv_FVar v ->
 			 if inspect_fv v = rewrite_fv
@@ -588,7 +588,7 @@ and translate_par (g:RT.fstar_top_env) (t:R.term)
   : T.Tac (err st_term) =
 
   let open R in
-  let head, args = R.collect_app t in
+  let head, args = T.collect_app t in
   match inspect_ln head with
   | Tv_FVar v ->
     if inspect_fv v = par_fv

examples/dsls/mini_steel/Pulse.Readback.fst

@@ -63,7 +63,7 @@ let try_readback_st_comp
   : T.Tac (option (c:comp{elab_comp c == t})) =
 
   let open R in
-  let hd, args = collect_app t in
+  let hd, args = T.collect_app t in
   match inspect_ln hd with
   | Tv_UInst fv [u] ->
     let fv_lid = inspect_fv fv in
@@ -187,7 +187,7 @@ let rec readback_ty (t:R.term)
         let? arg' = readback_ty a in
         Some (Tm_PureApp hd' (readback_qual q) arg' <: ty:term {elab_term ty == t})
     in
-    let head, args = R.collect_app t in
+    let head, args = T.collect_app t in
     begin
     match inspect_ln head, args with
     | Tv_FVar fv, [(a1,_); (a2,_)] -> 

examples/dsls/stlc/STLC.Infer.fst

@@ -97,7 +97,7 @@ let rec read_back (g:R.env) (t:R.term)
 
     | R.Tv_App _ _ ->
       begin
-      let head, args = R.collect_app t in
+      let head, args = T.collect_app t in
       if not (is_fv head ["STLC"; "Core"; "TArrow"])
       then T.fail "Got an application of type stlc_ty, but head is not a TArrow"
       else match args with

ocaml/fstar-lib/FStar_Unionfind.ml

@@ -119,6 +119,10 @@ let puf_id' (h:'a puf) (x:'a p_uvar) : int =
 let puf_id (h: 'a puf) (x: 'a p_uvar): Prims.int =
     Z.of_int (puf_id' h x)
 
+let puf_unique_id (x: 'a p_uvar): Prims.int =
+  match x with
+  | P a -> Z.of_int a
+
 let puf_fromid (_:'a puf) (id : Prims.int) : 'a p_uvar =
     P (Z.to_int id)