struct
type pattern_t = Pt.term
type term_t = Pt.term
- let classify = function
+ let rec classify = function
+ | Pt.AttributedTerm (_, t) -> classify t
| Pt.Variable _ -> Variable
| Pt.Magic _
| Pt.Layout _
let mask_of_appl_pattern = function
| Pt.UriPattern uri -> Uri uri, []
+ | Pt.ImplicitPattern
| Pt.VarPattern _ -> Blob, []
| Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
type term_t = Cic.annterm
let classify = function
+ | Pt.ImplicitPattern
| Pt.VarPattern _ -> Variable
- | _ -> Constructor
+ | Pt.UriPattern _
+ | Pt.ApplPattern _ -> Constructor
end
module M = Matcher (Pattern32)
List.map2
(fun p t ->
match p with
+ | Pt.ImplicitPattern -> Util.fresh_name (), t
| Pt.VarPattern name -> name, t
| _ -> assert false)
pl matched_terms