Moving pattern type constraints to pattern AST.

5 files changed, 67 insertions, 37 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 557e2bcb9a..fca1b3045c 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -220,15 +220,15 @@ GEXTEND Gram
         | None -> te
         | Some args -> Loc.tag ~loc:!@loc @@ CTacFun (args, te)
         in
-        (pat, None, te)
+        (pat, te)
     ] ]
   ;
   let_binder:
     [ [ pats = LIST1 input_fun ->
         match pats with
-        | [(_, CPatVar _) as pat, None] -> (pat, None)
-        | ((_, CPatVar (Name id)) as pat, None) :: args -> (pat, Some args)
-        | [pat, None] -> (pat, None)
+        | [(_, CPatVar _) as pat] -> (pat, None)
+        | ((_, CPatVar (Name id)) as pat) :: args -> (pat, Some args)
+        | [pat] -> (pat, None)
         | _ -> CErrors.user_err ~loc:!@loc (str "Invalid pattern")
     ] ]
   ;
@@ -257,8 +257,12 @@ GEXTEND Gram
       | l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ]
   ;
   input_fun:
-    [ [ b = tac2pat LEVEL "0" -> (b, None)
-      | "("; b = tac2pat; t = OPT [ ":"; t = tac2type -> t ]; ")" -> (b, t) ] ]
+    [ [ b = tac2pat LEVEL "0" -> b
+      | "("; b = tac2pat; t = OPT [ ":"; t = tac2type -> t ]; ")" ->
+        match t with
+        | None -> b
+        | Some t -> Loc.tag ~loc:!@loc @@ CPatCnv (b, t)
+    ] ]
   ;
   tac2def_body:
     [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index cefb4b13b8..e48bf02321 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -277,11 +277,15 @@ let fresh_var avoid x =
   in
   Namegen.next_ident_away_from (Id.of_string x) bad
 
+let extract_pattern_type (loc, p as pat) = match p with
+| CPatCnv (pat, ty) -> pat, Some ty
+| CPatVar _ | CPatRef _ -> pat, None
+
 (** Mangle recursive tactics *)
 let inline_rec_tactic tactics =
   let avoid = List.fold_left (fun accu ((_, id), _) -> Id.Set.add id accu) Id.Set.empty tactics in
   let map (id, e) = match snd e with
-  | CTacFun (pat, _) -> (id, pat, e)
+  | CTacFun (pat, _) -> (id, List.map extract_pattern_type pat, e)
   | _ ->
     let loc, _ = id in
     user_err ?loc (str "Recursive tactic definitions must be functions")
@@ -295,11 +299,9 @@ let inline_rec_tactic tactics =
     in
     (** Fresh variables to abstract over the function patterns *)
     let _, vars = List.fold_left fold_var (avoid, []) pat in
-    let map_body ((loc, id), _, e) = (Loc.tag ?loc @@ CPatVar (Name id)), None, e in
+    let map_body ((loc, id), _, e) = (Loc.tag ?loc @@ CPatVar (Name id)), e in
     let bnd = List.map map_body tactics in
-    let pat_of_id (loc, id) =
-      ((Loc.tag ?loc @@ CPatVar (Name id)), None)
-    in
+    let pat_of_id (loc, id) = (Loc.tag ?loc @@ CPatVar (Name id)) in
     let var_of_id (loc, id) =
       let qid = (loc, qualid_of_ident id) in
       Loc.tag ?loc @@ CTacRef (RelId qid)
@@ -590,7 +592,7 @@ let perform_notation syn st =
   let mk loc args =
     let map (na, e) =
       let loc = loc_of_tacexpr e in
-      ((Loc.tag ?loc @@ CPatVar na), None, e)
+      ((Loc.tag ?loc @@ CPatVar na), e)
     in
     let bnd = List.map map args in
     Loc.tag ~loc @@ CTacLet (false, bnd, syn.synext_exp)
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 89152dffe7..60f10d360f 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -91,6 +91,7 @@ type atom =
 type raw_patexpr_r =
 | CPatVar of Name.t
 | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
+| CPatCnv of raw_patexpr * raw_typexpr
 
 and raw_patexpr = raw_patexpr_r located
 
@@ -98,9 +99,9 @@ type raw_tacexpr_r =
 | CTacAtm of atom
 | CTacRef of tacref or_relid
 | CTacCst of ltac_constructor or_tuple or_relid
-| CTacFun of (raw_patexpr * raw_typexpr option) list * raw_tacexpr
+| CTacFun of raw_patexpr list * raw_tacexpr
 | CTacApp of raw_tacexpr * raw_tacexpr list
-| CTacLet of rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
+| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
 | CTacCnv of raw_tacexpr * raw_typexpr
 | CTacSeq of raw_tacexpr * raw_tacexpr
 | CTacCse of raw_tacexpr * raw_taccase list
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 7b35cd55aa..9afdb3aedc 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -556,11 +556,13 @@ type glb_patexpr =
 | GPatVar of Name.t
 | GPatRef of ltac_constructor or_tuple * glb_patexpr list
 
-let rec intern_patexpr env (_, pat) = match pat with
+let rec intern_patexpr env (loc, pat) = match pat with
 | CPatVar na -> GPatVar na
 | CPatRef (qid, pl) ->
   let kn = get_constructor env qid in
   GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
+| CPatCnv (pat, ty) ->
+  user_err ?loc (str "Pattern not handled yet")
 
 type pattern_kind =
 | PKind_empty
@@ -604,11 +606,16 @@ let rec ids_of_pattern accu (_, pat) = match pat with
 | CPatVar (Name id) -> Id.Set.add id accu
 | CPatRef (_, pl) ->
   List.fold_left ids_of_pattern accu pl
+| CPatCnv (pat, _) -> ids_of_pattern accu pat
 
 let loc_of_relid = function
 | RelId (loc, _) -> loc
 | AbsKn _ -> None
 
+let extract_pattern_type (loc, p as pat) = match p with
+| CPatCnv (pat, ty) -> pat, Some ty
+| CPatVar _ | CPatRef _ -> pat, None
+
 (** Expand pattern: [p => t] becomes [x => match x with p => t end] *)
 let expand_pattern avoid bnd =
   let fold (avoid, bnd) (pat, t) =
@@ -667,6 +674,7 @@ let rec intern_rec env (loc, e) = match e with
   let kn = get_constructor env qid in
   intern_constructor env loc kn []
 | CTacFun (bnd, e) ->
+  let bnd = List.map extract_pattern_type bnd in
   let map (_, t) = match t with
   | None -> GTypVar (fresh_id env)
   | Some t -> intern_type env t
@@ -689,8 +697,9 @@ let rec intern_rec env (loc, e) = match e with
   let map arg =
     (** Thunk alias arguments *)
     let loc = loc_of_tacexpr arg in
-    let var = [Loc.tag ?loc @@ CPatVar Anonymous, Some (Loc.tag ?loc @@ CTypRef (AbsKn (Tuple 0), []))] in
-    Loc.tag ?loc @@ CTacFun (var, arg)
+    let t_unit = Loc.tag ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
+    let var = Loc.tag ?loc @@ CPatCnv (Loc.tag ?loc @@ CPatVar Anonymous, t_unit) in
+    Loc.tag ?loc @@ CTacFun ([var], arg)
   in
   let args = List.map map args in
   intern_rec env (Loc.tag ?loc @@ CTacApp (e, args))
@@ -706,6 +715,11 @@ let rec intern_rec env (loc, e) = match e with
   let ret = unify_arrow ?loc env ft t in
   (GTacApp (f, args), ret)
 | CTacLet (is_rec, el, e) ->
+  let map (pat, e) =
+    let (pat, ty) = extract_pattern_type pat in
+    (pat, ty, e)
+  in
+  let el = List.map map el in
   let fold accu (pat, _, e) =
     let ids = ids_of_pattern Id.Set.empty pat in
     let common = Id.Set.inter ids accu in
@@ -826,7 +840,7 @@ and intern_let_rec env loc ids el e =
     let (loc, pat) = pat in
     let na = match pat with
     | CPatVar na -> na
-    | CPatRef _ ->
+    | CPatRef _ | CPatCnv _ ->
       user_err ?loc (str "This kind of pattern is forbidden in let-rec bindings")
     in
     let id = fresh_id env in
@@ -961,6 +975,8 @@ and intern_case env loc e pl =
             else warn_redundant_clause ?loc ()
         in
         brT
+      | CPatCnv _ ->
+        user_err ?loc (str "Pattern not handled yet")
       in
       let () = unify ?loc:(loc_of_tacexpr br) env tbr ret in
       intern_branch rem
@@ -1216,10 +1232,10 @@ let rec globalize ids (loc, er as e) = match er with
   let knc = get_constructor () qid in
   Loc.tag ?loc @@ CTacCst (AbsKn knc)
 | CTacFun (bnd, e) ->
-  let fold (pats, accu) (pat, t) =
+  let fold (pats, accu) pat =
     let accu = ids_of_pattern accu pat in
     let pat = globalize_pattern ids pat in
-    ((pat, t) :: pats, accu)
+    (pat :: pats, accu)
   in
   let bnd, ids = List.fold_left fold ([], ids) bnd in
   let bnd = List.rev bnd in
@@ -1230,13 +1246,14 @@ let rec globalize ids (loc, er as e) = match er with
   let el = List.map (fun e -> globalize ids e) el in
   Loc.tag ?loc @@ CTacApp (e, el)
 | CTacLet (isrec, bnd, e) ->
-  let fold accu (pat, _, _) = ids_of_pattern accu pat in
+  let fold accu (pat, _) = ids_of_pattern accu pat in
   let ext = List.fold_left fold Id.Set.empty bnd in
   let eids = Id.Set.union ext ids in
   let e = globalize eids e in
-  let map (qid, t, e) =
+  let map (qid, e) =
     let ids = if isrec then eids else ids in
-    (qid, t, globalize ids e)
+    let qid = globalize_pattern ids qid in
+    (qid, globalize ids e)
   in
   let bnd = List.map map bnd in
   Loc.tag ?loc @@ CTacLet (isrec, bnd, e)
@@ -1281,6 +1298,9 @@ and globalize_pattern ids (loc, pr as p) = match pr with
   let cst = AbsKn knc in
   let pl = List.map (fun p -> globalize_pattern ids p) pl in
   Loc.tag ?loc @@ CPatRef (cst, pl)
+| CPatCnv (pat, ty) ->
+  let pat = globalize_pattern ids pat in
+  Loc.tag ?loc @@ CPatCnv (pat, ty)
 
 (** Kernel substitution *)
 
@@ -1419,6 +1439,10 @@ let rec subst_rawpattern subst (loc, pr as p) = match pr with
   let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
   let c' = subst_or_relid subst c in
   if pl' == pl && c' == c then p else Loc.tag ?loc @@ CPatRef (c', pl')
+| CPatCnv (pat, ty) ->
+  let pat' = subst_rawpattern subst pat in
+  let ty' = subst_rawtype subst ty in
+  if pat' == pat && ty' == ty then p else Loc.tag ?loc @@ CPatCnv (pat', ty')
 
 (** Used for notations *)
 let rec subst_rawexpr subst (loc, tr as t) = match tr with
@@ -1430,10 +1454,7 @@ let rec subst_rawexpr subst (loc, tr as t) = match tr with
   let ref' = subst_or_relid subst ref in
   if ref' == ref then t else Loc.tag ?loc @@ CTacCst ref'
 | CTacFun (bnd, e) ->
-  let map (na, t as p) =
-    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
-    if t' == t then p else (na, t')
-  in
+  let map pat = subst_rawpattern subst pat in
   let bnd' = List.smartmap map bnd in
   let e' = subst_rawexpr subst e in
   if bnd' == bnd && e' == e then t else Loc.tag ?loc @@ CTacFun (bnd', e')
@@ -1442,10 +1463,10 @@ let rec subst_rawexpr subst (loc, tr as t) = match tr with
   let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
   if e' == e && el' == el then t else Loc.tag ?loc @@ CTacApp (e', el')
 | CTacLet (isrec, bnd, e) ->
-  let map (na, t, e as p) =
-    let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
+  let map (na, e as p) =
+    let na' = subst_rawpattern subst na in
     let e' = subst_rawexpr subst e in
-    if t' == t && e' == e then p else (na, t', e')
+    if na' == na && e' == e then p else (na', e')
   in
   let bnd' = List.smartmap map bnd in
   let e' = subst_rawexpr subst e in
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 399c1199bd..33c4a97de1 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -54,8 +54,10 @@ let std_proj ?loc name =
 let thunk e =
   let t_unit = coq_core "unit" in
   let loc = Tac2intern.loc_of_tacexpr e in
-  let var = [Loc.tag ?loc @@ CPatVar (Anonymous), Some (Loc.tag ?loc @@ CTypRef (AbsKn (Other t_unit), []))] in
-  Loc.tag ?loc @@ CTacFun (var, e)
+  let ty = Loc.tag ?loc @@ CTypRef (AbsKn (Other t_unit), []) in
+  let pat = Loc.tag ?loc @@ CPatVar (Anonymous) in
+  let pat = Loc.tag ?loc @@ CPatCnv (pat, ty) in
+  Loc.tag ?loc @@ CTacFun ([pat], e)
 
 let of_pair f g (loc, (e1, e2)) =
   Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2])
@@ -238,14 +240,14 @@ let abstract_vars loc vars tac =
         let get = global_ref ?loc (kername array_prefix "get")  in
         let args = [of_variable (loc, id0); of_int (loc, n)] in
         let e = Loc.tag ?loc @@ CTacApp (get, args) in
-        let accu = (Loc.tag ?loc @@ CPatVar na, None, e) :: accu in
+        let accu = (Loc.tag ?loc @@ CPatVar na, e) :: accu in
         (n + 1, accu)
       in
       let (_, bnd) = List.fold_left build_bindings (0, []) vars in
       let tac = Loc.tag ?loc @@ CTacLet (false, bnd, tac) in
       (Name id0, tac)
   in
-  Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], tac)
+  Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], tac)
 
 let of_pattern p =
   inj_wit ?loc:p.CAst.loc wit_pattern p
@@ -253,7 +255,7 @@ let of_pattern p =
 let of_conversion (loc, c) = match c with
 | QConvert c ->
   let pat = of_option ?loc of_pattern None in
-  let c = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar Anonymous, None], of_constr c) in
+  let c = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar Anonymous], of_constr c) in
   of_tuple ?loc [pat; c]
 | QConvertWith (pat, c) ->
   let vars = pattern_vars pat in
@@ -389,7 +391,7 @@ let of_constr_matching (loc, m) =
     let vars = Id.Set.elements vars in
     let vars = List.map (fun id -> Name id) vars in
     let e = abstract_vars loc vars tac in
-    let e = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], e) in
+    let e = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], e) in
     let pat = inj_wit ?loc:ploc wit_pattern pat in
     of_tuple [knd; pat; e]
   in
@@ -433,7 +435,7 @@ let of_goal_matching (loc, gm) =
   in
   let map (loc, (pat, tac)) =
     let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in
-    let tac = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar cctx, None], tac) in
+    let tac = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar cctx], tac) in
     let tac = abstract_vars loc subst tac in
     let tac = abstract_vars loc hctx tac in
     let tac = abstract_vars loc hyps tac in