(Utils.pos * equality) * proof
| ProofGoalBlock of proof * proof (* equality *)
| ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
+ | SubProof of Cic.term * int * proof
;;
;;
-let build_proof_term equality =
-(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
-(* print_newline (); *)
-
- let indent = ref 0 in
-
+let build_proof_term proof =
let rec do_build_proof proof =
match proof with
| NoProof ->
Printf.fprintf stderr "WARNING: no proof!\n";
-(* (string_of_equality equality); *)
Cic.Implicit None
| BasicProof term -> term
- | ProofGoalBlock (proofbit, proof (* equality *)) ->
+ | ProofGoalBlock (proofbit, proof) ->
print_endline "found ProofGoalBlock, going up...";
-(* let _, proof, _, _, _ = equality in *)
do_build_goal_proof proofbit proof
| ProofSymBlock (ens, proof) ->
let proof = do_build_proof proof in
proof
]
| ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
-(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
-(* print_newline (); *)
-
-(* 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, bo) in
- (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
- (* (string_of_equality eq) (string_of_equality eq'); *)
- (* print_newline (); *)
-
-(* let s = String.make !indent ' ' in *)
-(* incr indent; *)
-
-(* print_endline (s ^ "build proof'------------"); *)
-
let proof' =
let _, proof', _, _, _ = eq in
do_build_proof proof'
in
-(* print_endline (s ^ "END proof'"); *)
-
-(* print_endline (s ^ "build eqproof-----------"); *)
-
let eqproof = do_build_proof eqproof in
-
-(* print_endline (s ^ "END eqproof"); *)
-(* decr indent; *)
-
-
let _, _, (ty, what, other, _), menv', args' = eq in
let what, other =
if pos = Utils.Left then what, other else other, what
CicMetaSubst.apply_subst subst
(Cic.Appl [Cic.Const (eq_URI, []); ty;
what; t'; eqproof; other; proof'])
+ | SubProof (term, meta_index, proof) ->
+ let proof = do_build_proof proof in
+ let eq i = function
+ | Cic.Meta (j, _) -> i = j
+ | _ -> false
+ in
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
and do_build_goal_proof proofbit proof =
(* match proofbit with *)
(* let proof' = replace_proof newproof proof in *)
(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
| BasicProof _ -> newproof
+ | SubProof (term, meta_index, p) ->
+ SubProof (term, meta_index, replace_proof newproof p)
| p -> p
in
- let _, proof, _, _, _ = equality in
+(* let _, proof, _, _, _ = equality in *)
do_build_proof proof
;;
| 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 (U.failure_msg_of_string "Inference.unification.unif"))
+ raise
+ (U.UnificationFailure
+ (U.failure_msg_of_string "Inference.unification.unif"))
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
subst, menv
with CicUtil.Meta_not_found m ->
let names = names_of_context context in
- debug_print (lazy (
- 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)));
+ debug_print
+ (lazy
+ (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 (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure
+ (U.failure_msg_of_string "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 Invalid_argument _ ->
- raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure
+ (U.failure_msg_of_string "Inference.unification.unif"))
)
- | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
+ | _, _ ->
+ raise (U.UnificationFailure
+ (U.failure_msg_of_string "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
let menv =
(* 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 (
- debug_print (lazy (
- Printf.sprintf "NOT SIMPLE TERMS: %s %s"
- (CicPp.ppterm t1) (CicPp.ppterm t2)));
+ debug_print
+ (lazy
+ (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+ (CicPp.ppterm t1) (CicPp.ppterm t2)));
CicUnification.fo_unif metasenv context t1 t2 ugraph
) else
unification_simple metasenv context t1 t2 ugraph
(* (\* print_newline (); *\) *)
(* subst, menv, ug *)
(* else *)
-(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+(* debug_print *)
+(* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
(* print_newline (); *)
try
let subst, metasenv, ugraph =
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
- debug_print (lazy (
- Printf.sprintf "OK: %s" (CicPp.ppterm term)));
-(* debug_print (lazy ( *)
+ debug_print
+ (lazy
+ (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+(* debug_print ( *)
(* Printf.sprintf "args: %s\n" *)
(* (String.concat ", " (List.map CicPp.ppterm args)))); *)
(* debug_print (lazy ( *)
match do_find context term with
| Some p, newmeta ->
let tl, newmeta' = (aux (index+1) newmeta tl) in
- p::tl, max newmeta newmeta'
+ (index, p)::tl, max newmeta newmeta'
| None, _ ->
aux (index+1) newmeta tl
)
| _::tl ->
aux (index+1) newmeta tl
in
- aux 1 newmeta context
+ let il, maxm = aux 1 newmeta context in
+ let indexes, equalities = List.split il in
+ indexes, equalities, maxm
;;
"cic:/Coq/Init/Logic/f_equal.con";
"cic:/Coq/Init/Logic/f_equal2.con";
"cic:/Coq/Init/Logic/f_equal3.con";
+ "cic:/Coq/Init/Logic/f_equal4.con";
+ "cic:/Coq/Init/Logic/f_equal5.con";
"cic:/Coq/Init/Logic/sym_eq.con";
-(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
-(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
-
+ "cic:/Coq/Init/Logic/eq_ind.con";
+ "cic:/Coq/Init/Logic/eq_ind_r.con";
+ "cic:/Coq/Init/Logic/eq_rec.con";
+ "cic:/Coq/Init/Logic/eq_rec_r.con";
+ "cic:/Coq/Init/Logic/eq_rect.con";
+ "cic:/Coq/Init/Logic/eq_rect_r.con";
+ "cic:/Coq/Logic/Eqdep/UIP.con";
+ "cic:/Coq/Logic/Eqdep/UIP_refl.con";
+ "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
+ "cic:/Coq/ZArith/Zcompare/rename.con";
(* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
perche' questo cacchio di teorema rompe le scatole :'( *)
"cic:/Rocq/SUBST/comparith/mult_n_2.con";
]
;;
-let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta =
+let find_library_equalities dbd context status maxmeta =
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
let ty, _ =
CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
in
- (t, ty)::l)
+ (uri, t, ty)::l)
[]
(MetadataQuery.equations_for_goal ~dbd status)
in
in
let rec aux newmeta = function
| [] -> [], newmeta
- | (term, termty)::tl ->
- debug_print (lazy (
- Printf.sprintf "Examining: %s (%s)"
- (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
+ | (uri, term, termty)::tl ->
+ debug_print
+ (lazy
+ (Printf.sprintf "Examining: %s (%s)"
+ (CicPp.ppterm term) (CicPp.ppterm termty)));
let res, newmeta =
match termty with
| C.Prod (name, s, t) ->
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (iseq uri) && (ok_types ty newmetas) ->
- debug_print (lazy (
- Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+ debug_print
+ (lazy
+ (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
match res with
| Some e ->
let tl, newmeta' = aux newmeta tl in
- e::tl, max newmeta newmeta'
+ (uri, e)::tl, max newmeta newmeta'
| None ->
aux newmeta tl
in
let found, maxm = aux maxmeta candidates in
- (List.fold_left
- (fun l e ->
- if List.exists (meta_convertibility_eq e) l then (
- debug_print (lazy (
- Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
- l
- )
- else e::l)
- [] found), maxm
+ let uriset, eqlist =
+ (List.fold_left
+ (fun (s, l) (u, e) ->
+ if List.exists (meta_convertibility_eq e) l then (
+ debug_print
+ (lazy
+ (Printf.sprintf "NO!! %s already there!"
+ (string_of_equality e)));
+ (UriManager.UriSet.add u s, l)
+ ) else (UriManager.UriSet.add u s, e::l))
+ (UriManager.UriSet.empty, []) found)
+ in
+ uriset, eqlist, maxm
+;;
+
+
+let find_library_theorems dbd env status equalities_uris =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let blacklist =
+ let refl_equal =
+ UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
+ UriManager.UriSet.remove refl_equal
+ (UriManager.UriSet.union equalities_uris equations_blacklist)
+ in
+ let metasenv, context, ugraph = env in
+ let candidates =
+ List.fold_left
+ (fun l uri ->
+ if UriManager.UriSet.mem uri blacklist then l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
+ (t, ty, [])::l)
+ [] (MetadataQuery.signature_of_goal ~dbd status)
+ in
+ candidates
+;;
+
+
+let find_context_hypotheses env equalities_indexes =
+ let metasenv, context, ugraph = env in
+ let _, res =
+ List.fold_left
+ (fun (n, l) entry ->
+ match entry with
+ | None -> (n+1, l)
+ | Some _ ->
+ if List.mem n equalities_indexes then
+ (n+1, l)
+ else
+ let t = Cic.Rel n in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' metasenv context t ugraph in
+ (n+1, (t, ty, [])::l))
+ (1, []) context
+ in
+ res
;;
List.filter
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
- let table' = Hashtbl.copy table in
- let first = List.hd metas in
let _ =
- Hashtbl.iter
- (fun k v ->
- if not (List.exists
- (function Cic.Meta (i, _) -> i = v | _ -> assert false)
- newargs) then
- Hashtbl.replace table k first)
- table'
+ if List.length metas > 0 then
+ let first = List.hd metas in
+ Hashtbl.iter
+ (fun k v ->
+ if not (List.exists
+ (function Cic.Meta (i, _) -> i = v | _ -> assert false)
+ newargs) then
+ Hashtbl.replace table k first)
+ (Hashtbl.copy table)
in
-(* debug_print *)
-(* (Printf.sprintf "args: %s\nnewargs: %s\n" *)
-(* (String.concat "; " (List.map CicPp.ppterm args)) *)
-(* (String.concat "; " (List.map CicPp.ppterm newargs))); *)
-
let rec fix_proof = function
| NoProof -> NoProof
- | BasicProof term ->
-(* let term' = repl term in *)
-(* debug_print *)
-(* (Printf.sprintf "term was: %s\nterm' is: %s\n" *)
-(* (CicPp.ppterm term) (CicPp.ppterm term')); *)
- BasicProof (repl term)
+ | BasicProof term -> BasicProof (repl term)
| ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
;;
+let rec string_of_proof = function
+ | NoProof -> "NoProof"
+ | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+ | SubProof (t, i, p) ->
+ Printf.sprintf "SubProof(%s, %s, %s)"
+ (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
+ | ProofSymBlock _ -> "ProofSymBlock"
+ | ProofBlock _ -> "ProofBlock"
+ | ProofGoalBlock (p1, p2) ->
+ Printf.sprintf "ProofGoalBlock(%s, %s)"
+ (string_of_proof p1) (string_of_proof p2)
+;;
projects / helm.git / blobdiff