unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise (U.UnificationFailure "Inference.unification.unif")
- | C.Meta (i, l), t ->
- let _, _, ty = CicUtil.lookup_meta i menv in
- let subst =
- if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
- else subst
- in
- let menv = List.filter (fun (m, _, _) -> i <> m) menv in
- subst, menv
+ | C.Meta (i, l), t -> (
+ try
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let subst =
+ if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+ else subst
+ in
+ let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
+ subst, menv
+ with CicUtil.Meta_not_found m ->
+ let names = names_of_context context in
+ debug_print (
+ Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+ (CicPp.pp t1 names) (CicPp.pp t2 names)
+ (print_metasenv menv) (print_metasenv metasenv));
+ assert false
+ )
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
raise (U.UnificationFailure "Inference.unification.unif")
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
- with e ->
+ with Invalid_argument _ ->
raise (U.UnificationFailure "Inference.unification.unif")
)
| _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
in
let subst, menv = unif [] metasenv t1 t2 in
+ let menv =
+ List.filter
+ (fun (m, _, _) ->
+ try let _ = List.find (fun (i, _) -> m = i) subst in false
+ with Not_found -> true)
+ menv
+ in
List.rev subst, menv, ugraph
;;
List.fold_left2
(fun (subst, menv) s t -> do_match subst menv s t)
(subst, menv) ls lt
- with e ->
+ with Invalid_argument _ ->
(* print_endline (Printexc.to_string e); *)
(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
(* print_newline (); *)
(* print_newline (); *)
subst, metasenv, ugraph
- with e ->
+ with
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
(* Printf.printf "failed to match %s %s\n" *)
(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
(* print_endline (Printexc.to_string e); *)
let module S = CicSubstitution in
let module C = Cic in
- let print_info = false in
-
(* let _ = *)
(* let names = names_of_context context in *)
(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
(* else *)
((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
lifted_term)
- with e ->
- if print_info then (
- print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
- );
- res, lifted_term
+ with
+ | MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ res, lifted_term
in
(* Printf.printf "exit aux\n"; *)
retval
(* if match_only then replace_metas (\* context *\) where *)
(* else where *)
(* in *)
- if print_info then (
- Printf.printf "searching %s inside %s\n"
- (CicPp.ppterm what) (CicPp.ppterm where);
- );
aux 0 where context metasenv [] ugraph
in
let mapfun =
"cic:/Coq/Init/Logic/f_equal3.con";
"cic:/Coq/Init/Logic/sym_eq.con";
(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
+(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
]
;;
(* (i, (context, Cic.Meta (j, l), ty))::s *)
let _, context, ty = CicUtil.lookup_meta i menv in
(i, (context, Cic.Meta (j, l), ty))::s
- with _ -> s
+ with Not_found -> s
)
| _ -> assert false)
[] args