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 _ -> assert false
+ | Pt.Literal _ as t -> assert false
| _ -> Constructor
let tag_of_pattern = CicNotationTag.get_tag
let tag_of_term = CicNotationTag.get_tag
| _ -> assert false)
pl tl
- let decls_of_pattern p =
- List.map Env.declaration_of_var (Util.variables_of_term p)
-
let rec compiler rows =
let rows', magic_maps =
List.split
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) ->
in
magichooser candidates
in
- M.compiler rows match_cb (fun _ -> None)
+ M.compiler rows' match_cb (fun _ -> None)
and compile_magic = function
| Pt.Fold (kind, p_base, names, p_rec) ->
- let p_rec_decls = decls_of_pattern p_rec in
+ let p_rec_decls = Env.declarations_of_term p_rec in
let acc_name = try List.hd names with Failure _ -> assert false in
- let t_magic = [p_base, 0; p_rec, 1] in
- let compiled = compiler t_magic in
+ let compiled = compiler [p_base, 0; p_rec, 1] in
(fun term env ->
let rec aux term =
match compiled term with
| None -> None
| Some (base_env, rec_envl) ->
Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
+ | Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
+ let p_some_decls = Env.declarations_of_term p_some in
+ let none_env = List.map Env.opt_binding_of_name p_some_decls in
+ let compiled = compiler [p_some, 0] in
+ (fun term env ->
+ match compiled term with
+ | None -> Some none_env
+ | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+ | _ -> assert false)
| _ -> assert false
end
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 s -> Uri (UriManager.uri_of_string s), []
| 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 =