open Utils;;
+type equality =
+ int * (* weight *)
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+;;
+
+
+type proof =
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+ equality
+ | NoProof
+;;
+
+
let string_of_equality ?env =
match env with
| None -> (
function
- | _, (ty, left, right), _, _ ->
- Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
- (CicPp.ppterm left) (CicPp.ppterm right)
+ | _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+ (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
)
| Some (_, context, _) -> (
let names = names_of_context context in
function
- | _, (ty, left, right), _, _ ->
- Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
- (CicPp.pp left names) (CicPp.pp right names)
+ | _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+ (CicPp.pp left names) (string_of_comparison o)
+ (CicPp.pp right names)
)
;;
+let prooftable = Hashtbl.create 2001;;
+
+let store_proof equality proof =
+ if not (Hashtbl.mem prooftable equality) then
+ Hashtbl.add prooftable equality proof
+;;
+
+
+let delete_proof equality =
+(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ Hashtbl.remove prooftable equality
+;;
+
+
+let rec build_term_proof equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof for %s\n"
+ (string_of_equality equality);
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+(* (string_of_equality eq) (string_of_equality eq'); *)
+(* print_newline (); *)
+ let proof' = build_term_proof eq in
+ let eqproof = build_term_proof eq' in
+ let _, (ty, what, other, _), menv', args' = eq in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+;;
+
+
let rec metas_of_term = function
| Cic.Meta (i, c) -> [i]
| Cic.Var (_, ens)
let meta_convertibility_eq eq1 eq2 =
- let _, (ty, left, right), _, _ = eq1
- and _, (ty', left', right'), _, _ = eq2 in
+ let _, (ty, left, right, _), _, _ = eq1
+ and _, (ty', left', right', _), _, _ = eq2 in
if ty <> ty' then
false
else if (left = left') && (right = right') then
;;
-exception MatchingFailure;;
+let rec check_irl start = function
+ | [] -> true
+ | None::tl -> check_irl (start+1) tl
+ | (Some (Cic.Rel x))::tl ->
+ if x = start then check_irl (start+1) tl else false
+ | _ -> false
+;;
-let matching metasenv context t1 t2 ugraph =
- try
- let subst, metasenv, ugraph =
- CicUnification.fo_unif metasenv context t1 t2 ugraph
+let rec is_simple_term = function
+ | Cic.Appl ((Cic.Meta _)::_) -> false
+ | Cic.Appl l -> List.for_all is_simple_term l
+ | Cic.Meta (i, l) -> check_irl 1 l
+ | Cic.Rel _ -> true
+ | _ -> false
+;;
+
+
+let lookup_subst meta subst =
+ match meta with
+ | Cic.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+;;
+
+
+let unification_simple metasenv context t1 t2 ugraph =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup = lookup_subst in
+ let rec occurs_check subst what where =
+ (* Printf.printf "occurs_check %s %s" *)
+ (* (CicPp.ppterm what) (CicPp.ppterm where); *)
+ (* print_newline (); *)
+ match where with
+ | t when what = t -> true
+ | C.Appl l -> List.exists (occurs_check subst what) l
+ | C.Meta _ ->
+ let t = lookup where subst in
+ if t <> where then occurs_check subst what t else false
+ | _ -> false
+ in
+ let rec unif subst menv s t =
+(* Printf.printf "unif %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
+ and t = match t with C.Meta _ -> lookup t subst | _ -> t
in
- let t' = CicMetaSubst.apply_subst subst t1 in
- if not (meta_convertibility t1 t') then
- raise MatchingFailure
+ (* 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 ->
+ unif subst menv t s
+ | C.Meta _, t when occurs_check subst s t ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+(* | C.Meta (i, l), C.Meta (j, l') -> *)
+(* let _, _, ty = CicUtil.lookup_meta i menv in *)
+(* let _, _, ty' = CicUtil.lookup_meta j menv in *)
+(* let binding1 = lookup s subst in *)
+(* let binding2 = lookup t subst in *)
+(* let subst, menv = *)
+(* if binding1 != s then *)
+(* if binding2 != t then *)
+(* unif subst menv binding1 binding2 *)
+(* else *)
+(* if binding1 = t then *)
+(* subst, menv *)
+(* else *)
+(* ((j, (context, binding1, ty'))::subst, *)
+(* List.filter (fun (m, _, _) -> j <> m) menv) *)
+(* else *)
+(* if binding2 != t then *)
+(* if s = binding2 then *)
+(* subst, menv *)
+(* else *)
+(* ((i, (context, binding2, ty))::subst, *)
+(* List.filter (fun (m, _, _) -> i <> m) menv) *)
+(* else *)
+(* ((i, (context, t, ty))::subst, *)
+(* List.filter (fun (m, _, _) -> i <> m) menv) *)
+(* in *)
+(* subst, menv *)
+
+ | 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 _ -> unif subst menv t s
+ | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+ | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
+ try
+ List.fold_left2
+ (fun (subst', menv) s t -> unif subst' menv s t)
+ (subst, menv) tls tlt
+ with e ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+ )
+ | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+ in
+ let subst, menv = unif [] metasenv t1 t2 in
+ (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+ (* print_newline (); *)
+(* let rec fix_term = function *)
+(* | (C.Meta (i, l) as t) -> *)
+(* lookup t subst *)
+(* | C.Appl l -> C.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 *)
+(* List.rev (fix_subst subst), menv, ugraph *)
+ List.rev subst, menv, ugraph
+;;
+
+
+let unification metasenv context t1 t2 ugraph =
+(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+ let subst, menv, ug =
+ if not (is_simple_term t1) || not (is_simple_term t2) then
+ CicUnification.fo_unif metasenv context t1 t2 ugraph
else
- let metas = metas_of_term t1 in
- let fix_subst = function
- | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
- (j, (c, Cic.Meta (i, lc), ty))
- | s -> s
+ 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
in
- let subst = List.map fix_subst subst in
- subst, metasenv, ugraph
- with e ->
- raise MatchingFailure
+ let t' = CicMetaSubst.apply_subst subst t1 in
+ if not (meta_convertibility t1 t') then
+ raise MatchingFailure
+ else
+ let metas = metas_of_term t1 in
+ let fix_subst = function
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ (j, (c, Cic.Meta (i, lc), ty))
+ | s -> s
+ in
+ let subst = List.map fix_subst subst in
+
+(* Printf.printf "matching %s %s:\n%s\n" *)
+(* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
+(* print_newline (); *)
+
+ subst, metasenv, ugraph
+ with e ->
+(* Printf.printf "failed to match %s %s\n" *)
+(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+ raise MatchingFailure
;;
+(* let matching = *)
+(* let profile = CicUtil.profile "Inference.matching" in *)
+(* (fun metasenv context t1 t2 ugraph -> *)
+(* profile (matching metasenv context t1 t2) ugraph) *)
+(* ;; *)
+
let beta_expand ?(metas_ok=true) ?(match_only=false)
what type_of_what where context metasenv ugraph =
(* Printf.printf "provo a unificare %s e %s\n" *)
(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
if match_only then
- matching metasenv context term (S.lift lift_amount what)ugraph
+ matching metasenv context term (S.lift lift_amount what) ugraph
else
CicUnification.fo_unif metasenv context
(S.lift lift_amount what) term ugraph
;;
-type equality =
- Cic.term * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term) * (* right side *)
- Cic.metasenv * (* environment for metas *)
- Cic.term list (* arguments *)
-;;
-
-
let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
let module C = Cic in
let module S = CicSubstitution in
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
- Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), newmetas, args) in
+ store_proof e (BasicProof p);
+ Some e, (newmeta+1)
| _ -> None, newmeta
)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- Some (C.Rel index,
- (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
+ let t1 = S.lift index t1
+ and t2 = S.lift index t2 in
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), [], []) in
+ store_proof e (BasicProof (C.Rel index));
+ Some e, (newmeta+1)
| _ -> None, newmeta
in (
match do_find context term with
;;
-let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
+let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
let table = Hashtbl.create (List.length args) in
let newargs, _ =
List.fold_right
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
(newmeta + (List.length newargs) + 1,
- (repl proof, (ty, left, right), menv', newargs))
+ (weight, (ty, left, right, o), menv', newargs))
;;
let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- (proof, (ty, t1, t2), [], [])
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), [], []) in
+ store_proof e (BasicProof proof);
+ e
+(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
raise TermIsNotAnEquality
;;
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+(*
let superposition_left (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
let module CR = CicReduction in
(* we assume that target is ground (does not contain metavariables): this
* should always be the case (I hope, at least) *)
- let proof, (eq_ty, left, right), _, _ = target in
- let eqproof, (ty, t1, t2), newmetas, args = source in
+ let proof, (eq_ty, left, right, t_order), _, _ = target in
+ let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
let compare_terms = !Utils.compare_terms in
[]
else
let where, is_left =
- match compare_terms left right with
+ match t_order (* compare_terms left right *) with
| Lt -> right, false
| Gt -> left, true
| _ -> (
)
in
let metasenv' = newmetas @ metasenv in
- let result = compare_terms t1 t2 in
+ let result = s_order (* compare_terms t1 t2 *) in
let res1, res2 =
match result with
| Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
| _ -> assert false
in
let equation =
- if is_left then (eq_ty, newgoal, right)
- else (eq_ty, left, newgoal)
+ if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
+ else (eq_ty, left, newgoal, compare_terms left newgoal)
in
- (eqproof, equation, [], [])
+ (newgoalproof (* eqproof *), equation, [], [])
in
let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
- let eqproof, (eq_ty, left, right), newmetas, args = target in
- let eqp', (ty', t1, t2), newm', args' = source in
+ let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
+ let eqp', (ty', t1, t2, s_order), newm', args' = source in
let maxmeta = ref newmeta in
let compare_terms = !Utils.compare_terms in
in
let metasenv' = metasenv @ newmetas @ newm' in
let beta_expand = beta_expand ~metas_ok:false in
- let cmp1 = compare_terms left right
- and cmp2 = compare_terms t1 t2 in
+ let cmp1 = t_order (* compare_terms left right *)
+ and cmp2 = s_order (* compare_terms t1 t2 *) in
let res1, res2, res3, res4 =
let res l r s t =
List.filter
let left, right =
if is_left then (newterm, M.apply_subst s right)
else (M.apply_subst s left, newterm) in
+ let neworder = compare_terms left right in
fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right), newmetas, newargs)
+ (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
in
maxmeta := newmeta;
newequality
and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
let ok = function
- | _, (_, left, right), _, _ ->
+ | _, (_, left, right, _), _, _ ->
not (fst (CR.are_convertible context left right ugraph))
in
- !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+ (!maxmeta,
+ (List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
+*)
let is_identity ((_, context, ugraph) as env) = function
- | ((_, (ty, left, right), _, _) as equality) ->
+ | ((_, (ty, left, right, _), _, _) as equality) ->
let res =
(left = right ||
(fst (CicReduction.are_convertible context left right ugraph)))
;;
+(*
let demodulation newmeta (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
- let proof, (eq_ty, left, right), metas, args = target
- and proof', (ty, t1, t2), metas', args' = source in
+ let proof, (eq_ty, left, right, t_order), metas, args = target
+ and proof', (ty, t1, t2, s_order), metas', args' = source in
let compare_terms = !Utils.compare_terms in
newmeta, target
else
let first_step, get_params =
- match compare_terms t1 t2 with
+ match s_order (* compare_terms t1 t2 *) with
| Gt -> 1, (function
| 1 -> true, t1, t2, HL.Logic.eq_ind_URI
| 0 -> false, t1, t2, HL.Logic.eq_ind_URI
first_step, get_params
in
let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right), metas, args = target in
+ let proof, (eq_ty, left, right, t_order), metas, args = target in
let is_left, what, other, eq_URI = get_params step in
let env = metasenv, context, ugraph in
if is_left then newterm, right
else left, newterm
in
+ let neworder = compare_terms left right in
(* let newmetasenv = metasenv @ metas in *)
(* let newargs = args @ args' in *)
(* fix_metas newmeta *)
(function C.Meta (i, _) -> List.mem i m | _ -> assert false)
args
in
- newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
+ newmeta,
+ (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
in
(* Printf.printf *)
(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
let subsumption env target source =
- let _, (ty, tl, tr), tmetas, _ = target
- and _, (ty', sl, sr), smetas, _ = source in
+ let _, (ty, tl, tr, _), tmetas, _ = target
+ and _, (ty', sl, sr, _), smetas, _ = source in
if ty <> ty' then
false
else
);
res
;;
+*)
+
+
+let extract_differing_subterms t1 t2 =
+ let module C = Cic in
+ let rec aux t1 t2 =
+ match t1, t2 with
+ | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
+ [(t1, t2)]
+ | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
+ let res = List.concat (List.map2 aux tl1 tl2) in
+ if h1 <> h2 then
+ if res = [] then [(h1, h2)] else [(t1, t2)]
+ else
+ if List.length res > 1 then [(t1, t2)] else res
+ | t1, t2 ->
+ if t1 <> t2 then [(t1, t2)] else []
+ in
+ let res = aux t1 t2 in
+ match res with
+ | hd::[] -> Some hd
+ | _ -> None
+;;
projects / helm.git / blobdiff