let variable_closure k =
(fun matched_terms terms ->
- prerr_endline "variable_closure";
match terms with
| hd :: tl -> k (hd :: matched_terms) tl
| _ -> assert false)
let constructor_closure ks k =
(fun matched_terms terms ->
- prerr_endline "constructor_closure";
match terms with
| t :: tl ->
(try
| Pt.Variable _ -> Variable
| Pt.Magic _
| Pt.Layout _
- | Pt.Literal _ as t ->
- prerr_endline (CicNotationPp.pp_term t);
- assert false
+ | Pt.Literal _ as t -> assert false
| _ -> Constructor
let tag_of_pattern = CicNotationTag.get_tag
let tag_of_term = CicNotationTag.get_tag
Pt.Variable (Pt.TermVar name)
in
let rec aux = function
- | Pt.AttributedTerm (_, t) -> aux t
+ | Pt.AttributedTerm (_, t) -> assert false
| Pt.Literal _
| Pt.Layout _ -> assert false
| Pt.Variable v -> Pt.Variable v
candidates
in
let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
let candidates =
List.map
(fun (pl, pid) ->
struct
type cic_mask_t =
Blob
- | Uri of string
+ | Uri of UriManager.uri
| 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
- | Pt.UriPattern s -> Uri s, []
+ | Pt.UriPattern uri -> Uri uri, []
| Pt.VarPattern _ -> Blob, []
| Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
let compiler rows =
let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
let pl, pid = try List.hd rows with Not_found -> assert false in
(fun matched_terms ->
let env =