Some reflection/tactics updates

examples/Makefile

@@ -21,7 +21,7 @@ ALL_EXAMPLE_DIRS += metatheory
 ALL_EXAMPLE_DIRS += misc
 ALL_EXAMPLE_DIRS += oplss2021
 ALL_EXAMPLE_DIRS += paradoxes
-# ALL_EXAMPLE_DIRS += param # WIP
+ALL_EXAMPLE_DIRS += param
 ALL_EXAMPLE_DIRS += preorders
 ALL_EXAMPLE_DIRS += printf
 ALL_EXAMPLE_DIRS += regional

examples/miniparse/MiniParse.Spec.TEnum.fst

@@ -37,7 +37,7 @@ let rec mk_tenum_branches (ty: T.term) (vty: T.term) (v: nat) (accu: list T.bran
     begin match q with
     | [] ->
       let b = T.fresh_binder ty in
-      let pat = T.Pat_Var (T.bv_of_binder b) in
+      let pat = T.Pat_Var (T.bv_of_binder b) (Sealed.seal (T.binder_sort b)) in
       let br = (pat, v) in
       accu' `List.Tot.append` [br]
     | _ -> mk_tenum_branches ty vty v' accu' q

examples/param/Param.fst

@@ -233,17 +233,11 @@ and param_pat (s:param_state) (p : pattern) : Tac (param_state & (pattern & patt
           Pat_Cons fv us pats1,
           Pat_Cons fv' us patsr))
 
-  | Pat_Var bv ->
-    let (s', (b0, b1, bR)) = push_binder (mk_binder bv) s in
-    (s', (Pat_Var (bv_of_binder b0),
-          Pat_Var (bv_of_binder b1),
-          Pat_Var (bv_of_binder bR)))
-
-  | Pat_Wild bv ->
-    let (s', (b0, b1, bR)) = push_binder (mk_binder bv) s in
-    (s', (Pat_Wild (bv_of_binder b0),
-          Pat_Wild (bv_of_binder b1),
-          Pat_Wild (bv_of_binder bR)))
+  | Pat_Var bv sort ->
+    let (s', (b0, b1, bR)) = push_binder (mk_binder bv (unseal sort)) s in
+    (s', (Pat_Var (bv_of_binder b0) (Sealed.seal (binder_sort b0)),
+          Pat_Var (bv_of_binder b1) (Sealed.seal (binder_sort b1)),
+          Pat_Var (bv_of_binder bR) (Sealed.seal (binder_sort bR))))
 
   | Pat_Dot_Term t ->
     fail "no dot pats"
@@ -256,7 +250,7 @@ and param_pat (s:param_state) (p : pattern) : Tac (param_state & (pattern & patt
     let b = fresh_bv_named "cR" in
     (s, (Pat_Constant c,
          Pat_Constant c,
-         Pat_Wild b))
+         Pat_Var b (seal (`_))))
 
 and param_br (s:param_state) (br : branch) : Tac branch =
   let (pat, t) = br in

examples/tactics/Printers.fst

@@ -80,7 +80,7 @@ let mk_printer_fun (dom : term) : Tac term =
             let (name, t) = ctor in
             let pn = String.concat "." name in
             let t_args, _ = collect_arr t in
-            let bv_ty_pats = TU.map (fun ti -> let bv = fresh_bv_named "a" in ((bv, ti), (Pat_Var bv, false))) t_args in
+            let bv_ty_pats = TU.map (fun ti -> let bv = fresh_bv_named "a" in ((bv, ti), (Pat_Var bv (seal ti), false))) t_args in
             let bvs, pats = List.Tot.split bv_ty_pats in
             let head = pack (Tv_Const (C_String pn)) in
             let bod = mk_concat (mk_stringlit " ") (head :: TU.map (mk_print_bv xt_ns fftm) bvs) in