type equality =
- Cic.term * (* proof *)
+ int * (* weight *)
+ proof *
(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 =
+and proof =
| BasicProof of Cic.term
| ProofBlock of
- Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
- equality
+ Cic.substitution * UriManager.uri *
+ (* name, ty, eq_ty, left, right *)
+ (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
+ (Utils.pos * equality) * equality
| NoProof
;;
match env with
| None -> (
function
- | _, (ty, left, right, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (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, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (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
+ let _, proof, _, _, _ = equality in
match proof with
| NoProof ->
Printf.fprintf stderr "WARNING: no proof for %s\n"
Cic.Implicit None
| BasicProof term -> term
| ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+ let name, ty, eq_ty, left, right = t' in
+ let bo =
+ Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ eq_ty; left; right]
+ in
+ let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in
(* 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 _, _, (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;
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
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
+ let (head, newmetas, args, newmeta) =
+ ProofEngineHelpers.saturate_term newmeta []
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
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
let o = !Utils.compare_terms t1 t2 in
- let e = (p, (ty, t1, t2, o), newmetas, args) in
- store_proof e (BasicProof p);
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
Some e, (newmeta+1)
| _ -> None, newmeta
)
let t1 = S.lift index t1
and t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
- let e = (C.Rel index, (ty, t1, t2, o), [], []) in
- store_proof e (BasicProof (C.Rel index));
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
Some e, (newmeta+1)
| _ -> None, newmeta
in (
;;
-let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((w, p, (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, o), menv', newargs))
+ (w, p, (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 ->
let o = !Utils.compare_terms t1 t2 in
- let e = (proof, (ty, t1, t2, o), [], []) in
- store_proof e (BasicProof proof);
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
e
(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
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
(!maxmeta,
(List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
+*)
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
+ | ((_, _, (ty, left, right, _), _, _) as equality) ->
+ (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
);
res
;;
+*)
let extract_differing_subterms t1 t2 =