type cic_mask_t =
Blob
| Uri of UriManager.uri
+ | NRef of NReference.reference
| Appl of cic_mask_t list
let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
+ | Ast.NRefPattern nref -> NRef nref, []
| Ast.UriPattern uri -> Uri uri, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> Blob, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> PatternMatcher.Variable
| Ast.UriPattern _
+ | Ast.NRefPattern _
| Ast.ApplPattern _ -> PatternMatcher.Constructor
end
module M = PatternMatcher.Matcher (Pattern32)
let compiler rows =
- let match_cb rows =
- let pl, pid = try List.hd rows with Not_found -> assert false in
- (fun matched_terms constructors ->
+ let match_cb rows matched_terms constructors =
+ HExtlib.list_findopt
+ (fun (pl,pid) _ ->
let env =
try
List.map2
| Ast.VarPattern name -> name, t
| _ -> assert false)
pl matched_terms
- with Invalid_argument _ -> assert false
+ with Invalid_argument _ -> assert false in
+ let rec check_non_linear_patterns =
+ function
+ [] -> true
+ | (name,t)::tl ->
+ List.for_all
+ (fun (name',t') ->
+ name <> name' ||
+ CicUtil.alpha_equivalence
+ (Deannotate.deannotate_term t) (Deannotate.deannotate_term t')
+ ) tl && check_non_linear_patterns tl
in
- Some (env, constructors, pid))
+ if check_non_linear_patterns env then
+ Some (env, constructors, pid)
+ else
+ None
+ ) rows
in
M.compiler rows match_cb (fun () -> None)
end