--- /dev/null
+open Utils;;
+
+
+exception NotMetaConvertible;;
+
+let meta_convertibility_aux table t1 t2 =
+ let module C = Cic in
+ let rec aux table t1 t2 =
+ match t1, t2 with
+ | t1, t2 when t1 = t2 -> table
+ | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
+ let m1_binding, table =
+ try List.assoc m1 table, table
+ with Not_found -> m2, (m1, m2)::table
+ in
+ if m1_binding <> m2 then
+ raise NotMetaConvertible
+ else (
+ try
+ List.fold_left2
+ (fun res t1 t2 ->
+ match t1, t2 with
+ | None, Some _ | Some _, None -> raise NotMetaConvertible
+ | None, None -> res
+ | Some t1, Some t2 -> (aux res t1 t2))
+ table tl1 tl2
+ with Invalid_argument _ ->
+ raise NotMetaConvertible
+ )
+ | C.Var (u1, ens1), C.Var (u2, ens2)
+ | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
+ aux_ens table ens1 ens2
+ | C.Cast (s1, t1), C.Cast (s2, t2)
+ | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
+ | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
+ | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+ let table = aux table s1 s2 in
+ aux table t1 t2
+ | C.Appl l1, C.Appl l2 -> (
+ try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
+ when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
+ | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
+ when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
+ aux_ens table ens1 ens2
+ | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
+ when (UriManager.eq u1 u2) && i1 = i2 ->
+ let table = aux table s1 s2 in
+ let table = aux table t1 t2 in (
+ try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
+ try
+ List.fold_left2
+ (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
+ if i1 <> i2 then raise NotMetaConvertible
+ else
+ let res = (aux res s1 s2) in aux res t1 t2)
+ table il1 il2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
+ try
+ List.fold_left2
+ (fun res (n1, s1, t1) (n2, s2, t2) ->
+ let res = aux res s1 s2 in aux res t1 t2)
+ table il1 il2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | _, _ -> raise NotMetaConvertible
+
+ and aux_ens table ens1 ens2 =
+ let cmp (u1, t1) (u2, t2) =
+ compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
+ in
+ let ens1 = List.sort cmp ens1
+ and ens2 = List.sort cmp ens2 in
+ try
+ List.fold_left2
+ (fun res (u1, t1) (u2, t2) ->
+ if not (UriManager.eq u1 u2) then raise NotMetaConvertible
+ else aux res t1 t2)
+ table ens1 ens2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ in
+ aux table t1 t2
+;;
+
+
+let meta_convertibility_eq eq1 eq2 =
+ let _, (ty, left, right), _, _ = eq1
+ and _, (ty', left', right'), _, _ = eq2 in
+ if ty <> ty' then
+ false
+ else
+ let print_table t w =
+ Printf.printf "table %s is:\n" w;
+ List.iter
+ (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
+ t;
+ print_newline ();
+ in
+ try
+ let table = meta_convertibility_aux [] left left' in
+(* print_table table "before"; *)
+ let table = meta_convertibility_aux table right right' in
+(* print_table table "after"; *)
+ true
+ with NotMetaConvertible ->
+(* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
+(* (CicPp.ppterm left) (CicPp.ppterm right) *)
+(* (CicPp.ppterm left') (CicPp.ppterm right'); *)
+ false
+;;
+
+
+let meta_convertibility t1 t2 =
+ try
+ let _ = meta_convertibility_aux [] t1 t2 in
+ true
+ with NotMetaConvertible ->
+ false
+;;
+
+
+let beta_expand ?(metas_ok=true) ?(match_only=false)
+ what type_of_what where context metasenv ugraph =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ (*
+ return value:
+ ((list of all possible beta expansions, subst, metasenv, ugraph),
+ lifted term)
+ *)
+ let rec aux lift_amount term context metasenv subst ugraph =
+(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
+ let res, lifted_term =
+ match term with
+ | C.Rel m ->
+ [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
+
+ | C.Var (uri, exp_named_subst) ->
+ let ens', lifted_ens =
+ aux_ens lift_amount exp_named_subst context metasenv subst ugraph
+ in
+ let expansions =
+ List.map
+ (fun (e, s, m, ug) ->
+ (C.Var (uri, e), s, m, ug)) ens'
+ in
+ expansions, C.Var (uri, lifted_ens)
+
+ | C.Meta (i, l) ->
+ let l', lifted_l =
+ List.fold_right
+ (fun arg (res, lifted_tl) ->
+ match arg with
+ | Some arg ->
+ let arg_res, lifted_arg =
+ aux lift_amount arg context metasenv subst ugraph in
+ let l1 =
+ List.map
+ (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
+ arg_res
+ in
+ (l1 @
+ (List.map
+ (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
+ res),
+ (Some lifted_arg)::lifted_tl)
+ | None ->
+ (List.map
+ (fun (r, s, m, ug) -> None::r, s, m, ug)
+ res,
+ None::lifted_tl)
+ ) l ([], [])
+ in
+ let e =
+ List.map
+ (fun (l, s, m, ug) ->
+ (C.Meta (i, l), s, m, ug)) l'
+ in
+ e, C.Meta (i, lifted_l)
+
+ | C.Sort _
+ | C.Implicit _ as t -> [], t
+
+ | C.Cast (s, t) ->
+ let l1, lifted_s =
+ aux lift_amount s context metasenv subst ugraph in
+ let l2, lifted_t =
+ aux lift_amount t context metasenv subst ugraph
+ in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Cast (t, lifted_t), s, m, ug) l1 in
+ let l2' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Cast (lifted_s, t), s, m, ug) l2 in
+ l1'@l2', C.Cast (lifted_s, lifted_t)
+
+ | C.Prod (nn, s, t) ->
+ let l1, lifted_s =
+ aux lift_amount s context metasenv subst ugraph in
+ let l2, lifted_t =
+ aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
+ metasenv subst ugraph
+ in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Prod (nn, t, lifted_t), s, m, ug) l1 in
+ let l2' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Prod (nn, lifted_s, t), s, m, ug) l2 in
+ l1'@l2', C.Prod (nn, lifted_s, lifted_t)
+
+ | C.Lambda (nn, s, t) ->
+ let l1, lifted_s =
+ aux lift_amount s context metasenv subst ugraph in
+ let l2, lifted_t =
+ aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
+ metasenv subst ugraph
+ in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
+ let l2' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
+ l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
+
+ | C.LetIn (nn, s, t) ->
+ let l1, lifted_s =
+ aux lift_amount s context metasenv subst ugraph in
+ let l2, lifted_t =
+ aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
+ metasenv subst ugraph
+ in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
+ let l2' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
+ l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
+
+ | C.Appl l ->
+ let l', lifted_l =
+ aux_list lift_amount l context metasenv subst ugraph
+ in
+ (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
+ C.Appl lifted_l)
+
+ | C.Const (uri, exp_named_subst) ->
+ let ens', lifted_ens =
+ aux_ens lift_amount exp_named_subst context metasenv subst ugraph
+ in
+ let expansions =
+ List.map
+ (fun (e, s, m, ug) ->
+ (C.Const (uri, e), s, m, ug)) ens'
+ in
+ (expansions, C.Const (uri, lifted_ens))
+
+ | C.MutInd (uri, i ,exp_named_subst) ->
+ let ens', lifted_ens =
+ aux_ens lift_amount exp_named_subst context metasenv subst ugraph
+ in
+ let expansions =
+ List.map
+ (fun (e, s, m, ug) ->
+ (C.MutInd (uri, i, e), s, m, ug)) ens'
+ in
+ (expansions, C.MutInd (uri, i, lifted_ens))
+
+ | C.MutConstruct (uri, i, j, exp_named_subst) ->
+ let ens', lifted_ens =
+ aux_ens lift_amount exp_named_subst context metasenv subst ugraph
+ in
+ let expansions =
+ List.map
+ (fun (e, s, m, ug) ->
+ (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
+ in
+ (expansions, C.MutConstruct (uri, i, j, lifted_ens))
+
+ | C.MutCase (sp, i, outt, t, pl) ->
+ let pl_res, lifted_pl =
+ aux_list lift_amount pl context metasenv subst ugraph
+ in
+ let l1, lifted_outt =
+ aux lift_amount outt context metasenv subst ugraph in
+ let l2, lifted_t =
+ aux lift_amount t context metasenv subst ugraph in
+
+ let l1' =
+ List.map
+ (fun (outt, s, m, ug) ->
+ C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
+ let l2' =
+ List.map
+ (fun (t, s, m, ug) ->
+ C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
+ let l3' =
+ List.map
+ (fun (pl, s, m, ug) ->
+ C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
+ in
+ (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
+
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let fl', lifted_fl =
+ List.fold_right
+ (fun (nm, idx, ty, bo) (res, lifted_tl) ->
+ let lifted_ty = S.lift lift_amount ty in
+ let bo_res, lifted_bo =
+ aux (lift_amount+len) bo context metasenv subst ugraph in
+ let l1 =
+ List.map
+ (fun (a, s, m, ug) ->
+ (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
+ bo_res
+ in
+ (l1 @
+ (List.map
+ (fun (r, s, m, ug) ->
+ (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
+ (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
+ ) fl ([], [])
+ in
+ (List.map
+ (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
+ C.Fix (i, lifted_fl))
+
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let fl', lifted_fl =
+ List.fold_right
+ (fun (nm, ty, bo) (res, lifted_tl) ->
+ let lifted_ty = S.lift lift_amount ty in
+ let bo_res, lifted_bo =
+ aux (lift_amount+len) bo context metasenv subst ugraph in
+ let l1 =
+ List.map
+ (fun (a, s, m, ug) ->
+ (nm, lifted_ty, a)::lifted_tl, s, m, ug)
+ bo_res
+ in
+ (l1 @
+ (List.map
+ (fun (r, s, m, ug) ->
+ (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
+ (nm, lifted_ty, lifted_bo)::lifted_tl)
+ ) fl ([], [])
+ in
+ (List.map
+ (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
+ C.CoFix (i, lifted_fl))
+ in
+ let retval =
+ match term with
+ | C.Meta _ when (not metas_ok) ->
+ res, lifted_term
+ | _ ->
+ try
+ let subst', metasenv', ugraph' =
+ CicUnification.fo_unif metasenv context
+ (S.lift lift_amount what) term ugraph
+ in
+ (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
+ (* (CicPp.ppterm (S.lift lift_amount what)); *)
+ (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
+ (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
+ (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
+ let term' = CicMetaSubst.apply_subst subst' term in (
+ if match_only && not (meta_convertibility term term') then (
+(* Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *)
+(* (CicPp.ppterm term) (CicPp.ppterm term'); *)
+ res, lifted_term
+ )
+ else
+(* let _ = *)
+(* if match_only then *)
+(* Printf.printf "OK, trovato match con %s\n" *)
+(* (CicPp.ppterm term) *)
+(* in *)
+ ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
+ lifted_term)
+ )
+ with _ ->
+ res, lifted_term
+ in
+(* Printf.printf "exit aux\n"; *)
+ retval
+
+ and aux_list lift_amount l context metasenv subst ugraph =
+ List.fold_right
+ (fun arg (res, lifted_tl) ->
+ let arg_res, lifted_arg =
+ aux lift_amount arg context metasenv subst ugraph in
+ let l1 = List.map
+ (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
+ in
+ (l1 @ (List.map
+ (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
+ lifted_arg::lifted_tl)
+ ) l ([], [])
+
+ and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
+ List.fold_right
+ (fun (u, arg) (res, lifted_tl) ->
+ let arg_res, lifted_arg =
+ aux lift_amount arg context metasenv subst ugraph in
+ let l1 =
+ List.map
+ (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
+ in
+ (l1 @ (List.map (fun (r, s, m, ug) ->
+ (u, lifted_arg)::r, s, m, ug) res),
+ (u, lifted_arg)::lifted_tl)
+ ) exp_named_subst ([], [])
+
+ in
+ let expansions, _ = aux 0 where context metasenv [] ugraph in
+ List.map
+ (fun (term, subst, metasenv, ugraph) ->
+ let term' = C.Lambda (C.Anonymous, type_of_what, term) in
+(* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
+(* (CicPp.ppterm term') (print_subst subst); *)
+ (term', subst, metasenv, ugraph))
+ expansions
+;;
+
+
+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
+ let module T = CicTypeChecker in
+ let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let rec aux index newmeta = function
+ | [] -> [], newmeta
+ | (Some (_, C.Decl (term)))::tl ->
+ let do_find context term =
+ match term with
+ | C.Prod (name, s, t) ->
+(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
+ let (head, newmetas, args, _) =
+ PrimitiveTactics.new_metasenv_for_apply newmeta proof
+ context (S.lift index term)
+ in
+ let newmeta =
+ List.fold_left
+ (fun maxm arg ->
+ match arg with
+ | C.Meta (i, _) -> (max maxm i)
+ | _ -> assert false)
+ newmeta args
+ in
+ let p =
+ if List.length args = 0 then
+ C.Rel index
+ else
+ C.Appl ((C.Rel index)::args)
+ 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)
+ | _ -> 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)
+ | _ -> None, newmeta
+ in (
+ match do_find context term with
+ | Some p, newmeta ->
+ let tl, newmeta' = (aux (index+1) newmeta tl) in
+ p::tl, max newmeta newmeta'
+ | None, _ ->
+ aux (index+1) newmeta tl
+ )
+ | _::tl ->
+ aux (index+1) newmeta tl
+ in
+ aux 1 newmeta context
+;;
+
+
+let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
+ let newargs, _ =
+ List.fold_right
+ (fun t (newargs, index) ->
+ match t with
+ | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
+ | _ -> assert false)
+ args ([], newmeta)
+ in
+ let repl where =
+ ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
+ ~where
+ in
+ let menv', _ =
+ List.fold_right
+ (fun (i, context, term) (menv, index) ->
+ ((index, context, term)::menv, index+1))
+ menv ([], newmeta)
+ in
+ (newmeta + (List.length newargs) + 1,
+ (repl proof, (repl ty, repl left, repl right), menv', newargs))
+;;
+
+
+exception TermIsNotAnEquality;;
+
+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), [], [])
+ | _ ->
+ 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 M = CicMetaSubst in
+ let module HL = HelmLibraryObjects 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
+
+ (* ALB: TODO check that ty and eq_ty are indeed equal... *)
+ assert (eq_ty = ty);
+
+ let where, is_left =
+ match nonrec_kbo left right with
+ | Lt -> right, false
+ | Gt -> left, true
+ | _ -> (
+ Printf.printf "????????? %s = %s" (CicPp.ppterm left)
+ (CicPp.ppterm right);
+ print_newline ();
+ assert false (* again, for ground terms this shouldn't happen... *)
+ )
+ in
+ let metasenv' = newmetas @ metasenv in
+ let res1 =
+ List.filter
+ (fun (t, s, m, ug) ->
+ nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
+ (beta_expand t1 ty where context metasenv' ugraph)
+ and res2 =
+ List.filter
+ (fun (t, s, m, ug) ->
+ nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
+ (beta_expand t2 ty where context metasenv' ugraph)
+ in
+(* let what, other = *)
+(* if is_left then left, right *)
+(* else right, left *)
+(* in *)
+ let build_new what other eq_URI (t, s, m, ug) =
+ let newgoal, newgoalproof =
+ match t with
+ | C.Lambda (nn, ty, bo) ->
+ let bo' = S.subst (M.apply_subst s other) bo in
+ let bo'' =
+ C.Appl (
+ [C.MutInd (HL.Logic.eq_URI, 0, []);
+ S.lift 1 eq_ty] @
+ if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
+ in
+ let t' = C.Lambda (nn, ty, bo'') in
+ S.subst (M.apply_subst s other) bo,
+ M.apply_subst s
+ (C.Appl [C.Const (eq_URI, []); ty; what; t';
+ proof; other; eqproof])
+ | _ -> assert false
+ in
+ let equation =
+ if is_left then (eq_ty, newgoal, right)
+ else (eq_ty, left, newgoal)
+ in
+ (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
+ new1 @ new2
+;;
+
+
+let superposition_right newmeta (metasenv, context, ugraph) target source =
+ let module C = Cic in
+ let module S = CicSubstitution 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 maxmeta = ref newmeta in
+
+ (* TODO check if ty and ty' are equal... *)
+ assert (eq_ty = ty');
+
+(* let ok term subst other other_eq_side ugraph = *)
+(* match term with *)
+(* | C.Lambda (nn, ty, bo) -> *)
+(* let bo' = S.subst (M.apply_subst subst other) bo in *)
+(* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
+(* not res *)
+(* | _ -> assert false *)
+(* in *)
+ let condition left right what other (t, s, m, ug) =
+ let subst = M.apply_subst s in
+ let cmp1 = nonrec_kbo (subst what) (subst other) in
+ let cmp2 = nonrec_kbo (subst left) (subst right) in
+(* cmp1 = Gt && cmp2 = Gt *)
+ cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
+(* && (ok t s other right ug) *)
+ in
+ let metasenv' = metasenv @ newmetas @ newm' in
+ let beta_expand = beta_expand ~metas_ok:false in
+ let res1 =
+ List.filter
+ (condition left right t1 t2)
+ (beta_expand t1 eq_ty left context metasenv' ugraph)
+ and res2 =
+ List.filter
+ (condition left right t2 t1)
+ (beta_expand t2 eq_ty left context metasenv' ugraph)
+ and res3 =
+ List.filter
+ (condition right left t1 t2)
+ (beta_expand t1 eq_ty right context metasenv' ugraph)
+ and res4 =
+ List.filter
+ (condition right left t2 t1)
+ (beta_expand t2 eq_ty right context metasenv' ugraph)
+ in
+ let newmetas = newmetas @ newm' in
+ let newargs = args @ args' in
+ let build_new what other is_left eq_URI (t, s, m, ug) =
+(* let what, other = *)
+(* if is_left then left, right *)
+(* else right, left *)
+(* in *)
+ let newterm, neweqproof =
+ match t with
+ | C.Lambda (nn, ty, bo) ->
+ let bo' = M.apply_subst s (S.subst other bo) in
+ let bo'' =
+ C.Appl (
+ [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
+ if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
+ in
+ let t' = C.Lambda (nn, ty, bo'') in
+ bo',
+ M.apply_subst s
+ (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp'])
+ | _ -> assert false
+ in
+ let newmeta, newequality =
+ let left, right =
+ if is_left then (newterm, M.apply_subst s right)
+ else (M.apply_subst s left, newterm) in
+ fix_metas !maxmeta
+ (neweqproof, (eq_ty, left, right), newmetas, newargs)
+ in
+ maxmeta := newmeta;
+ newequality
+ in
+ let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
+ and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
+ 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), _, _ ->
+ not (fst (CR.are_convertible context left right ugraph))
+ in
+ !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+;;
+
+
+let demodulation newmeta (metasenv, context, ugraph) target source =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst 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
+ if eq_ty <> ty then
+ newmeta, target
+ else
+ let get_params step =
+ match step with
+ | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
+ | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
+ | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
+ | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
+ | _ -> assert false
+ in
+ let rec demodulate newmeta step metasenv target =
+ let proof, (eq_ty, left, right), metas, args = target in
+ let is_left, what, other, eq_URI = get_params step in
+(* Printf.printf *)
+(* "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
+(* (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *)
+(* (CicPp.ppterm other) (string_of_bool is_left); *)
+(* Printf.printf "step: %d\n" step; *)
+(* print_newline (); *)
+ let ok (t, s, m, ug) =
+ nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
+ in
+ let res =
+ List.filter ok
+ (beta_expand ~metas_ok:false ~match_only:true
+ what ty left context (metasenv @ metas) ugraph)
+ in
+ match res with
+ | [] ->
+ if step = 0 then newmeta, target
+ else demodulate newmeta (step-1) metasenv target
+ | (t, s, m, ug)::_ ->
+ let newterm, newproof =
+ match t with
+ | C.Lambda (nn, ty, bo) ->
+ let bo' = M.apply_subst s (S.subst other bo) in
+ let bo'' =
+ C.Appl (
+ [C.MutInd (HL.Logic.eq_URI, 0, []);
+ S.lift 1 eq_ty] @
+ if is_left then [bo'; S.lift 1 right]
+ else [S.lift 1 left; bo'])
+ in
+ let t' = C.Lambda (nn, ty, bo'') in
+ M.apply_subst s (S.subst other bo),
+ M.apply_subst s
+ (C.Appl [C.Const (eq_URI, []); ty; what; t';
+ proof; other; proof'])
+ | _ -> assert false
+ in
+ let newmeta, newtarget =
+ let left, right =
+ if is_left then (newterm, M.apply_subst s right)
+ else (M.apply_subst s left, newterm) in
+ let newmetasenv = metasenv @ metas in
+ let newargs = args @ args' in
+ fix_metas newmeta
+ (newproof, (eq_ty, left, right), newmetasenv, newargs)
+ in
+ let _, (_, left, right), _, _ = newtarget
+ and _, (_, oldleft, oldright), _, _ = target in
+(* Printf.printf *)
+(* "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *)
+(* (CicPp.ppterm left) (CicPp.ppterm right) *)
+(* (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *)
+(* print_newline (); *)
+ demodulate newmeta step metasenv newtarget
+ in
+ demodulate newmeta 3 (metasenv @ metas') target
+;;
+
+
+(*
+let demodulation newmeta env target source =
+ newmeta, target
+;;
+*)
+
+
--- /dev/null
+open Inference;;
+open Utils;;
+
+type result =
+ | Failure
+ | Success of Cic.term option * environment
+;;
+
+
+type equality_sign = Negative | Positive;;
+
+let string_of_sign = function
+ | Negative -> "Negative"
+ | Positive -> "Positive"
+;;
+
+
+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)
+ )
+ | 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)
+ )
+;;
+
+
+module OrderedEquality =
+struct
+ type t = Inference.equality
+
+ let compare eq1 eq2 =
+ match meta_convertibility_eq eq1 eq2 with
+ | true -> 0
+ | false -> Pervasives.compare eq1 eq2
+end
+
+module EqualitySet = Set.Make(OrderedEquality);;
+
+
+
+let select env passive =
+ match passive with
+ | hd::tl, pos -> (Negative, hd), (tl, pos)
+ | [], hd::tl -> (Positive, hd), ([], tl)
+ | _, _ -> assert false
+;;
+
+
+(*
+let select env passive =
+ match passive with
+ | neg, pos when EqualitySet.is_empty neg ->
+ let elem = EqualitySet.min_elt pos in
+ (Positive, elem), (neg, EqualitySet.remove elem pos)
+ | neg, pos ->
+ let elem = EqualitySet.min_elt neg in
+ (Negative, elem), (EqualitySet.remove elem neg, pos)
+;;
+*)
+
+
+(* TODO: find a better way! *)
+let maxmeta = ref 0;;
+
+let infer env sign current active =
+ let rec infer_negative current = function
+ | [] -> [], []
+ | (Negative, _)::tl -> infer_negative current tl
+ | (Positive, equality)::tl ->
+ let res = superposition_left env current equality in
+ let neg, pos = infer_negative current tl in
+ res @ neg, pos
+
+ and infer_positive current = function
+ | [] -> [], []
+ | (Negative, equality)::tl ->
+ let res = superposition_left env equality current in
+ let neg, pos = infer_positive current tl in
+ res @ neg, pos
+ | (Positive, equality)::tl ->
+ let maxm, res = superposition_right !maxmeta env current equality in
+ let maxm, res' = superposition_right maxm env equality current in
+ maxmeta := maxm;
+ let neg, pos = infer_positive current tl in
+
+(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
+(* (string_of_equality ~env current) (string_of_equality ~env equality) *)
+(* (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
+(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
+(* (string_of_equality ~env equality) (string_of_equality ~env current) *)
+(* (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
+
+ neg, res @ res' @ pos
+ in
+ match sign with
+ | Negative -> infer_negative current active
+ | Positive -> infer_positive current active
+;;
+
+
+let contains_empty env (negative, positive) =
+ let metasenv, context, ugraph = env in
+ try
+ let (proof, _, _, _) =
+ List.find
+ (fun (proof, (ty, left, right), m, a) ->
+ fst (CicReduction.are_convertible context left right ugraph))
+ negative
+ in
+ true, Some proof
+ with Not_found ->
+ false, None
+;;
+
+
+let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
+ let find sign eq1 eq2 =
+ if meta_convertibility_eq eq1 eq2 then (
+(* Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *)
+(* (string_of_sign sign) (string_of_equality eq1); *)
+ true
+ ) else
+ false
+ in
+ let ok sign equalities equality =
+ not (List.exists (find sign equality) equalities)
+ in
+ let neg = List.filter (ok Negative passive_neg) new_neg in
+ let pos = List.filter (ok Positive passive_pos) new_pos in
+(* let neg, pos = new_neg, new_pos in *)
+ (neg @ passive_neg, passive_pos @ pos)
+;;
+
+
+let is_identity ((_, context, ugraph) as env) = function
+ | ((_, (ty, left, right), _, _) as equality) ->
+ let res =
+ (left = right ||
+ (fst (CicReduction.are_convertible context left right ugraph)))
+ in
+(* if res then ( *)
+(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
+(* print_newline (); *)
+(* ); *)
+ res
+;;
+
+
+let forward_simplify env (sign, current) active =
+(* if sign = Negative then *)
+(* Some (sign, current) *)
+(* else *)
+ let rec aux env (sign, current) =
+ function
+ | [] -> Some (sign, current)
+ | (Negative, _)::tl -> aux env (sign, current) tl
+ | (Positive, equality)::tl ->
+ let newmeta, current = demodulation !maxmeta env current equality in
+ maxmeta := newmeta;
+ if is_identity env current then
+ None
+ else
+ aux env (sign, current) tl
+ in
+ aux env (sign, current) active
+;;
+
+
+let forward_simplify_new env (new_neg, new_pos) active =
+ let remove_identities equalities =
+ let ok eq = not (is_identity env eq) in
+ List.filter ok equalities
+ in
+ let rec simpl active target =
+ match active with
+ | [] -> target
+ | (Negative, _)::tl -> simpl tl target
+ | (Positive, source)::tl ->
+ let newmeta, target = demodulation !maxmeta env target source in
+ maxmeta := newmeta;
+ if is_identity env target then target
+ else simpl tl target
+ in
+ let new_neg = List.map (simpl active) new_neg
+ and new_pos = List.map (simpl active) new_pos in
+ new_neg, remove_identities new_pos
+;;
+
+
+let backward_simplify env (sign, current) active =
+ match sign with
+ | Negative -> active
+ | Positive ->
+ let active =
+ List.map
+ (fun (s, equality) ->
+ (* match s with *)
+ (* | Negative -> s, equality *)
+ (* | Positive -> *)
+ let newmeta, equality =
+ demodulation !maxmeta env equality current in
+ maxmeta := newmeta;
+ s, equality)
+ active
+ in
+ let active =
+ List.filter (fun (s, eq) -> not (is_identity env eq)) active
+ in
+ let find eq1 where =
+ List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
+ in
+ List.fold_right
+ (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
+ active []
+;;
+
+
+(*
+let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
+ let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in
+ add_all passive_neg new_neg, add_all passive_pos new_pos
+;;
+*)
+
+
+let rec given_clause env passive active =
+ match passive with
+(* | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *)
+(* Failure *)
+ | [], [] -> Failure
+ | passive ->
+(* Printf.printf "before select\n"; *)
+ let (sign, current), passive = select env passive in
+(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
+(* (string_of_sign sign) (string_of_equality ~env current); *)
+ match forward_simplify env (sign, current) active with
+ | None when sign = Negative ->
+ Printf.printf "OK!!! %s %s" (string_of_sign sign)
+ (string_of_equality ~env current);
+ print_newline ();
+ let proof, _, _, _ = current in
+ Success (Some proof, env)
+ | None ->
+ Printf.printf "avanti... %s %s" (string_of_sign sign)
+ (string_of_equality ~env current);
+ print_newline ();
+ given_clause env passive active
+ | Some (sign, current) ->
+(* Printf.printf "sign: %s\ncurrent: %s\n" *)
+(* (string_of_sign sign) (string_of_equality ~env current); *)
+(* print_newline (); *)
+
+ let new' = infer env sign current active in
+
+ let active =
+ backward_simplify env (sign, current) active
+(* match new' with *)
+(* | [], [] -> backward_simplify env (sign, current) active *)
+(* | _ -> active *)
+ in
+
+ let new' = forward_simplify_new env new' active in
+
+ print_endline "\n================================================";
+ let _ =
+ Printf.printf "active:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e)) active)));
+ print_newline ();
+ in
+(* let _ = *)
+(* match new' with *)
+(* | neg, pos -> *)
+(* Printf.printf "new':\n%s\n" *)
+(* (String.concat "\n" *)
+(* ((List.map *)
+(* (fun e -> "Negative " ^ *)
+(* (string_of_equality ~env e)) neg) @ *)
+(* (List.map *)
+(* (fun e -> "Positive " ^ *)
+(* (string_of_equality ~env e)) pos))); *)
+(* print_newline (); *)
+(* in *)
+ match contains_empty env new' with
+ | false, _ ->
+ let active =
+ match sign with
+ | Negative -> (sign, current)::active
+ | Positive -> active @ [(sign, current)]
+ in
+ let passive = add_to_passive passive new' in
+ given_clause env passive active
+ | true, proof ->
+ Success (proof, env)
+;;
+
+
+let get_from_user () =
+ let dbd = Mysql.quick_connect
+ ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+ let rec get () =
+ match read_line () with
+ | "" -> []
+ | t -> t::(get ())
+ in
+ let term_string = String.concat "\n" (get ()) in
+ let env, metasenv, term, ugraph =
+ List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
+ in
+ term, metasenv, ugraph
+;;
+
+
+let main () =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let term, metasenv, ugraph = get_from_user () in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let proof, goals =
+ PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let goal = List.nth goals 0 in
+ let _, metasenv, meta_proof, _ = proof in
+ let _, context, goal = CicUtil.lookup_meta goal metasenv in
+ let equalities, maxm = find_equalities context proof in
+ maxmeta := maxm; (* TODO ugly!! *)
+ let env = (metasenv, context, ugraph) in
+ try
+ let term_equality = equality_of_term meta_proof goal in
+ let meta_proof, (eq_ty, left, right), _, _ = term_equality in
+ let active = [] in
+(* let passive = *)
+(* (EqualitySet.singleton term_equality, *)
+(* List.fold_left *)
+(* (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *)
+(* in *)
+ let passive = [term_equality], equalities in
+ Printf.printf "\ncurrent goal: %s ={%s} %s\n"
+ (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
+ Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
+ Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+ Printf.printf "\nequalities:\n";
+ List.iter
+ (function (_, (ty, t1, t2), _, _) ->
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ let res = nonrec_kbo t1 t2 in
+ Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
+ (PP.ppterm t1) (string_of_weight w1)
+ (string_of_comparison res)
+ (PP.ppterm t2) (string_of_weight w2))
+ equalities;
+ print_endline "--------------------------------------------------";
+ let start = Sys.time () in
+ print_endline "GO!";
+ let res = given_clause env passive active in
+ let finish = Sys.time () in
+ match res with
+ | Failure ->
+ Printf.printf "NO proof found! :-(\n\n"
+ | Success (Some proof, env) ->
+ Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
+ (finish -. start);
+ | Success (None, env) ->
+ Printf.printf "Success, but no proof?!?\n\n"
+ with exc ->
+ print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
+;;
+
+
+let _ =
+ let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in
+ Helm_registry.load_from configuration_file
+in
+main ()
--- /dev/null
+let print_metasenv metasenv =
+ String.concat "\n--------------------------\n"
+ (List.map (fun (i, context, term) ->
+ (string_of_int i) ^ " [\n" ^ (CicPp.ppcontext context) ^
+ "\n] " ^ (CicPp.ppterm term))
+ metasenv)
+;;
+
+
+let print_subst subst =
+ String.concat "\n"
+ (List.map
+ (fun (i, (c, t, ty)) ->
+ Printf.sprintf "?%d -> %s : %s" i
+ (CicPp.ppterm t) (CicPp.ppterm ty))
+ subst)
+;;
+
+(* (weight of constants, [(meta, weight_of_meta)]) *)
+type weight = int * (int * int) list;;
+
+let string_of_weight (cw, mw) =
+ let s =
+ String.concat ", "
+ (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
+ in
+ Printf.sprintf "[%d; %s]" cw s
+
+
+let weight_of_term term =
+ (* ALB: what to consider as a variable? I think "variables" in our case are
+ Metas and maybe Rels... *)
+ let module C = Cic in
+ let vars_dict = Hashtbl.create 5 in
+ let rec aux = function
+ | C.Meta (metano, _) ->
+ (try
+ let oldw = Hashtbl.find vars_dict metano in
+ Hashtbl.replace vars_dict metano (oldw+1)
+ with Not_found ->
+ Hashtbl.add vars_dict metano 1);
+ 0
+
+ | C.Var (_, ens)
+ | C.Const (_, ens)
+ | C.MutInd (_, _, ens)
+ | C.MutConstruct (_, _, _, ens) ->
+ List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
+
+ | C.Cast (t1, t2)
+ | C.Lambda (_, t1, t2)
+ | C.Prod (_, t1, t2)
+ | C.LetIn (_, t1, t2) ->
+ let w1 = aux t1 in
+ let w2 = aux t2 in
+ w1 + w2 + 1
+
+ | C.Appl l -> List.fold_left (+) 0 (List.map aux l)
+
+ | C.MutCase (_, _, outt, t, pl) ->
+ let w1 = aux outt in
+ let w2 = aux t in
+ let w3 = List.fold_left (+) 0 (List.map aux pl) in
+ w1 + w2 + w3 + 1
+
+ | C.Fix (_, fl) ->
+ List.fold_left (fun w (n, i, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
+
+ | C.CoFix (_, fl) ->
+ List.fold_left (fun w (n, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
+
+ | _ -> 1
+ in
+ let w = aux term in
+ let l =
+ Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] in
+ let compare w1 w2 =
+ match w1, w2 with
+ | (m1, _), (m2, _) -> m2 - m1
+ in
+ (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
+;;
+
+
+(* returns a "normalized" version of the polynomial weight wl (with type
+ * weight list), i.e. a list sorted ascending by meta number,
+ * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
+ * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
+ * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
+let normalize_weight maxmeta (cw, wl) =
+(* Printf.printf "normalize_weight: %d, %s\n" maxmeta *)
+(* (string_of_weight (cw, wl)); *)
+ let rec aux = function
+ | 0 -> []
+ | m -> (m, 0)::(aux (m-1))
+ in
+ let tmpl = aux maxmeta in
+ let wl =
+ List.sort
+ (fun (m, _) (n, _) -> Pervasives.compare m n)
+ (List.fold_left
+ (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
+ in
+ (cw, wl)
+;;
+
+
+let normalize_weights (cw1, wl1) (cw2, wl2) =
+ let rec aux wl1 wl2 =
+ match wl1, wl2 with
+ | [], [] -> [], []
+ | (m, w)::tl1, (n, w')::tl2 when m = n ->
+ let res1, res2 = aux tl1 tl2 in
+ (m, w)::res1, (n, w')::res2
+ | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
+ let res1, res2 = aux tl1 wl2 in
+ (m, w)::res1, (m, 0)::res2
+ | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
+ let res1, res2 = aux wl1 tl2 in
+ (n, 0)::res1, (n, w')::res2
+ | [], (n, w)::tl2 ->
+ let res1, res2 = aux [] tl2 in
+ (n, 0)::res1, (n, w)::res2
+ | (m, w)::tl1, [] ->
+ let res1, res2 = aux tl1 [] in
+ (m, w)::res1, (m, 0)::res2
+ in
+ let cmp (m, _) (n, _) = compare m n in
+ let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
+ (cw1, wl1), (cw2, wl2)
+;;
+
+
+type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
+
+let string_of_comparison = function
+ | Lt -> "<"
+ | Le -> "<="
+ | Gt -> ">"
+ | Ge -> ">="
+ | Eq -> "="
+ | Incomparable -> "I"
+
+
+let compare_weights ?(normalize=false)
+ ((h1, w1) as weight1) ((h2, w2) as weight2)=
+ let (h1, w1), (h2, w2) =
+ if normalize then
+(* let maxmeta = *)
+(* let maxmeta l = *)
+(* try *)
+(* match List.hd l with *)
+(* | (m, _) -> m *)
+(* with Failure _ -> 0 *)
+(* in *)
+(* max (maxmeta w1) (maxmeta w2) *)
+(* in *)
+(* (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *)
+ normalize_weights weight1 weight2
+ else
+ (h1, w1), (h2, w2)
+ in
+ let res, diffs =
+ try
+ List.fold_left2
+ (fun ((lt, eq, gt), diffs) w1 w2 ->
+ match w1, w2 with
+ | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
+ let diffs = (w1 - w2) + diffs in
+ let r = compare w1 w2 in
+ if r < 0 then (lt+1, eq, gt), diffs
+ else if r = 0 then (lt, eq+1, gt), diffs
+ else (lt, eq, gt+1), diffs
+ | (meta1, w1), (meta2, w2) ->
+ Printf.printf "HMMM!!!! %s, %s\n"
+ (string_of_weight weight1) (string_of_weight weight2);
+ assert false)
+ ((0, 0, 0), 0) w1 w2
+ with Invalid_argument _ ->
+ Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
+ (string_of_weight (h1, w1)) (string_of_weight weight1)
+ (string_of_weight (h2, w2)) (string_of_weight weight2)
+ (string_of_bool normalize);
+ assert false
+ in
+ let hdiff = h1 - h2 in
+ match res with
+ | (0, _, 0) ->
+ if hdiff < 0 then Lt
+ else if hdiff > 0 then Gt
+ else Eq (* Incomparable *)
+ | (m, _, 0) ->
+ if hdiff <= 0 then
+ if m > 0 || hdiff < 0 then Lt
+ else if diffs >= (- hdiff) then Le else Incomparable
+ else
+ if diffs >= (- hdiff) then Le else Incomparable
+ | (0, _, m) ->
+ if hdiff >= 0 then
+ if m > 0 || hdiff > 0 then Gt
+ else if (- diffs) >= hdiff then Ge else Incomparable
+ else
+ if (- diffs) >= hdiff then Ge else Incomparable
+ | (m, _, n) when m > 0 && n > 0 ->
+ Incomparable
+;;
+
+
+let rec aux_ordering t1 t2 =
+ let module C = Cic in
+ let compare_uris u1 u2 =
+ let res =
+ compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
+ if res < 0 then Lt
+ else if res = 0 then Eq
+ else Gt
+ in
+ match t1, t2 with
+ | C.Meta _, _
+ | _, C.Meta _ -> Incomparable
+
+ | t1, t2 when t1 = t2 -> Eq
+
+ | C.Rel n, C.Rel m -> if n > m then Lt else Gt (* ALB: changed < to > *)
+ | C.Rel _, _ -> Lt
+ | _, C.Rel _ -> Gt
+
+ | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
+ | C.Const _, _ -> Lt
+ | _, C.Const _ -> Gt
+
+ | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2
+ | C.MutInd _, _ -> Lt
+ | _, C.MutInd _ -> Gt
+
+ | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) ->
+ compare_uris u1 u2
+ | C.MutConstruct _, _ -> Lt
+ | _, C.MutConstruct _ -> Gt
+
+ | C.Appl l1, C.Appl l2 ->
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Eq
+ | _, [] -> Gt
+ | [], _ -> Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o = aux_ordering hd1 hd2 in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ cmp l1 l2
+
+ | t1, t2 ->
+ Printf.printf "These two terms are not comparable:\n%s\n%s\n\n"
+ (CicPp.ppterm t1) (CicPp.ppterm t2);
+ Incomparable
+;;
+
+
+(* w1, w2 are the weights, they should already be normalized... *)
+let nonrec_kbo_w (t1, w1) (t2, w2) =
+ match compare_weights w1 w2 with
+ | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
+ | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
+ | Eq -> aux_ordering t1 t2
+ | res -> res
+;;
+
+
+let nonrec_kbo t1 t2 =
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ match compare_weights ~normalize:true w1 w2 with
+ | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
+ | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
+ | Eq -> aux_ordering t1 t2
+ | res -> res
+;;
+
+
+let names_of_context context =
+ List.map
+ (function
+ | None -> None
+ | Some (n, e) -> Some n)
+ context
+;;
+
projects / helm.git / commitdiff