| Pt.Variable _ -> Variable
| Pt.Magic _
| Pt.Layout _
- | Pt.Literal _ -> assert false
+ | Pt.Literal _ as t ->
+ prerr_endline (CicNotationPp.pp_term 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
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