module Ast = NotationPt
module Util = NotationUtil
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
-
module Matcher32 =
struct
module Pattern32 =
| NRef of NReference.reference
| Appl of cic_mask_t list
- let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
-
let mask_of_cic = function
| NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl
| NCic.Const nref -> NRef nref, []
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
- | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), []
| Ast.NRefPattern nref -> NRef nref, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> Blob, []
type pattern_t = Ast.cic_appl_pattern
type term_t = NCic.term
+ (* Debugging functions only *)
let string_of_pattern = NotationPp.pp_cic_appl_pattern
let string_of_term t =
- (*CSC: ??? *)
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
+ (new NCicPp.status)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
let classify = function
| Ast.ImplicitPattern
| Ast.VarPattern _ -> PatternMatcher.Variable
- | Ast.UriPattern _
| Ast.NRefPattern _
| Ast.ApplPattern _ -> PatternMatcher.Constructor
end
module M = PatternMatcher.Matcher (Pattern32)
- let compiler rows =
+ let compiler status rows =
let match_cb rows matched_terms constructors =
HExtlib.list_findopt
(fun (pl,pid) _ ->
| (name,t)::tl ->
List.for_all
(fun (name',t') ->
- name <> name' || NCicReduction.alpha_eq [] [] [] t t'
+ name <> name' || NCicReduction.alpha_eq status [] [] [] t t'
) tl && check_non_linear_patterns tl
in
if check_non_linear_patterns env then