+ unification_simple metasenv context t1 t2 ugraph
+ in
+ let rec fix_term = function
+ | (Cic.Meta (i, l) as t) ->
+ let t' = lookup_subst t subst in
+ if t <> t' then fix_term t' else t
+ | Cic.Appl l -> Cic.Appl (List.map fix_term l)
+ | t -> t
+ in
+ let rec fix_subst = function
+ | [] -> []
+ | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
+ in
+(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
+(* print_endline "|"; *)
+ (* fix_subst *) subst, menv, ug
+;;
+
+(* let unification = CicUnification.fo_unif;; *)
+
+exception MatchingFailure;;
+
+
+let matching_simple metasenv context t1 t2 ugraph =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup meta subst =
+ match meta with
+ | C.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+ in
+ let rec do_match subst menv s t =
+(* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
+(* (print_subst subst); *)
+(* print_newline (); *)
+(* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
+(* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
+ (* Printf.printf "after apply_subst: %s %s\n%s" *)
+ (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
+ (* print_newline (); *)
+ match s, t with
+ | s, t when s = t -> subst, menv
+(* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
+(* do_match subst menv t s *)
+(* | C.Meta _, t when occurs_check subst s t -> *)
+(* raise MatchingFailure *)
+(* | s, C.Meta _ when occurs_check subst t s -> *)
+(* raise MatchingFailure *)
+ | s, C.Meta (i, l) ->
+ let filter_menv i menv =
+ List.filter (fun (m, _, _) -> i <> m) menv
+ in
+ let subst, menv =
+ let value = lookup t subst in
+ match value with
+(* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
+(* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
+ | value when value = t ->
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ (i, (context, s, ty))::subst, filter_menv i menv
+ | value when value <> s ->
+ raise MatchingFailure
+ | value -> do_match subst menv s value
+ in
+ subst, menv
+(* else if value <> s then *)
+(* raise MatchingFailure *)
+(* else 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 _ -> do_match subst menv t s *)
+(* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
+(* raise MatchingFailure *)
+ | C.Appl ls, C.Appl lt -> (
+ try
+ List.fold_left2
+ (fun (subst, menv) s t -> do_match subst menv s t)
+ (subst, menv) ls lt
+ with e ->
+(* print_endline (Printexc.to_string e); *)
+(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(* print_newline (); *)
+ raise MatchingFailure
+ )
+ | _, _ ->
+(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(* print_newline (); *)
+ raise MatchingFailure
+ in
+ let subst, menv = do_match [] metasenv t1 t2 in
+ (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+ (* print_newline (); *)
+ subst, menv, ugraph
+;;
+
+
+let matching metasenv context t1 t2 ugraph =
+(* if (is_simple_term t1) && (is_simple_term t2) then *)
+(* let subst, menv, ug = *)
+(* matching_simple metasenv context t1 t2 ugraph in *)
+(* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
+(* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
+(* (\* print_newline (); *\) *)
+(* subst, menv, ug *)
+(* else *)
+ try
+ let subst, metasenv, ugraph =
+ (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
+ unification metasenv context t1 t2 ugraph