| BasicProof of Cic.term
| ProofBlock of
Cic.substitution * UriManager.uri *
+ (Cic.name * Cic.term) * Cic.term *
(* name, ty, eq_ty, left, right *)
- (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
+(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *)
(Utils.pos * equality) * proof
- | ProofGoalBlock of proof * equality
+ | ProofGoalBlock of proof * proof (* equality *)
| ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
;;
(* (string_of_equality equality); *)
Cic.Implicit None
| BasicProof term -> term
- | ProofGoalBlock (proofbit, equality) ->
+ | ProofGoalBlock (proofbit, proof (* equality *)) ->
print_endline "found ProofGoalBlock, going up...";
- let _, proof, _, _, _ = equality in
+(* let _, proof, _, _, _ = equality in *)
do_build_goal_proof proofbit proof
| ProofSymBlock (ens, proof) ->
let proof = do_build_proof proof in
Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
proof
]
- | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
+ | 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, (* CicSubstitution.lift 1 *) bo) in
+(* 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 (); *)
(* | BasicProof _ -> do_build_proof proof *)
(* | proofbit -> *)
match proof with
- | ProofGoalBlock (pb, eq) ->
- do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
+ | ProofGoalBlock (pb, p(* eq *)) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
(* let _, proof, _, _, _ = eq in *)
(* let newproof = replace_proof proofbit proof in *)
(* do_build_proof newproof *)
| _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
and replace_proof newproof = function
- | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
- let uri = eq_URI in
-(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
-(* HelmLibraryObjects.Logic.eq_ind_r_URI *)
-(* else *)
-(* HelmLibraryObjects.Logic.eq_ind_URI *)
-(* in *)
+ | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
let eqproof' = replace_proof newproof eqproof in
- ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
-(* ProofBlock (subst, eq_URI, t', poseq, newproof) *)
- | ProofGoalBlock (pb, equality) ->
+ ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
+ | ProofGoalBlock (pb, p(* equality *)) ->
let pb' = replace_proof newproof pb in
- ProofGoalBlock (pb', equality)
+ ProofGoalBlock (pb', p(* equality *))
(* let w, proof, t, menv, args = equality in *)
(* let proof' = replace_proof newproof proof in *)
(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
perche' questo cacchio di teorema rompe le scatole :'( *)
"cic:/Rocq/SUBST/comparith/mult_n_2.con";
]
-;;
+ ;;
let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
let module C = Cic in
(fun t (newargs, index) ->
match t with
| Cic.Meta (i, l) ->
- Hashtbl.add table i index;
-(* if index = 5469 then ( *)
-(* Printf.printf "?5469 COMES FROM (%d): %s\n" *)
-(* i (string_of_equality equality); *)
-(* print_newline (); *)
-(* is_this_case := true *)
-(* ); *)
- ((Cic.Meta (index, l))::newargs, index+1)
+ if Hashtbl.mem table i then
+ let idx = Hashtbl.find table i in
+ ((Cic.Meta (idx, l))::newargs, index+1)
+ else
+ let _ = Hashtbl.add table i index in
+ ((Cic.Meta (index, l))::newargs, index+1)
| _ -> assert false)
args ([], newmeta+1)
in
and left = repl left
and right = repl right in
let metas = (metas_of_term left) @ (metas_of_term right) in
- let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
- and newargs =
+ let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
+ let newargs =
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'
+ 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 -> BasicProof (repl term)
- | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
+ | 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)
+ | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
(* (string_of_equality equality) (print_subst subst); *)
-
+
+(* debug_print "table is:"; *)
+(* Hashtbl.iter *)
+(* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
+(* table; *)
let subst' =
List.fold_left
(fun s arg ->
if List.mem_assoc i subst then
s
else
-(* let _, context, ty = CicUtil.lookup_meta j menv' in *)
-(* (i, (context, Cic.Meta (j, l), ty))::s *)
let _, context, ty = CicUtil.lookup_meta i menv in
(i, (context, Cic.Meta (j, l), ty))::s
- with Not_found -> s
+ with Not_found ->
+(* debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
+ s
)
| _ -> assert false)
[] args
in
-(* let subst'' = *)
-(* List.map *)
-(* (fun (i, e) -> *)
-(* try let j = Hashtbl.find table i in (j, e) *)
-(* with _ -> (i, e)) subst *)
-(* in *)
(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
(* print_newline (); *)
- ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
-(* | ProofSymBlock (ens, p) -> *)
-(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
-(* ProofSymBlock (ens', fix_proof p) *)
+ ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
| p -> assert false
in
-(* (newmeta + (List.length newargs) + 2, *)
let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
-(* if !is_this_case then ( *)
-(* print_endline "\nTHIS IS THE TROUBLE!!!"; *)
-(* let pt = build_proof_term neweq in *)
-(* Printf.printf "equality: %s\nproof: %s\n" *)
-(* (string_of_equality neweq) (CicPp.ppterm pt); *)
-(* print_endline (String.make 79 '-'); *)
-(* ); *)
(newmeta + 1, neweq)
-(* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
;;
let is_identity ((_, context, ugraph) as env) = function
| ((_, _, (ty, left, right, _), _, _) as equality) ->
(left = right ||
+ (meta_convertibility left right) ||
(fst (CicReduction.are_convertible context left right ugraph)))
;;
projects / helm.git / blobdiff