- | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r]))
+ | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r]))
when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
| _ -> prerr_endline (CicPp.ppterm pred); assert false
;;
when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
| _ -> prerr_endline (CicPp.ppterm pred); assert false
;;
* that is used only by the base case
*
* ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
* that is used only by the base case
*
* ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
| Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
when LibraryObjects.is_sym_eq_URI uri_sym ->
let ty,l,r,p = open_sym ens tl in
| Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
when LibraryObjects.is_sym_eq_URI uri_sym ->
let ty,l,r,p = open_sym ens tl in
| Cic.LetIn (name,body,rest) ->
(* we should go in body *)
| Cic.LetIn (name,body,rest) ->
(* we should go in body *)
| Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
| Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
let is_not_fixed_lp = is_not_fixed lp in
let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
(* extract the context and the fixed term from the predicate *)
let is_not_fixed_lp = is_not_fixed lp in
let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
(* extract the context and the fixed term from the predicate *)
let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
(* they were under a lambda *)
let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
(* they were under a lambda *)
in
(* create the compound context and put the terms under it *)
let ctx_dc = compose_contexts ctx_d ctx_c in
in
(* create the compound context and put the terms under it *)
let ctx_dc = compose_contexts ctx_d ctx_c in
in
(* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
in
(* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
dc_other,dc_what,d_m,p2,p1
else
d_m,dc_what,dc_other,
dc_other,dc_what,d_m,p2,p1
else
d_m,dc_what,dc_other,
- (mk_sym uri_sym ty dc_what d_m p1),
- (mk_sym uri_sym ty dc_other dc_what p2)
+ (mk_sym uri_sym ctx_ty dc_what d_m p1),
+ (mk_sym uri_sym ctx_ty dc_other dc_what p2)
| t ->
let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
| t ->
let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
in
let d_left = put_in_ctx ctx_d left in
let d_right = put_in_ctx ctx_d right in
Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
in
let d_left = put_in_ctx ctx_d left in
let d_right = put_in_ctx ctx_d right in
Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
;;
Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
;;
let p1 = Subst.apply_subst_lift lift subst p1 in
let p2 = Subst.apply_subst_lift lift subst p2 in
let l = CicSubstitution.lift lift l in
let p1 = Subst.apply_subst_lift lift subst p1 in
let p2 = Subst.apply_subst_lift lift subst p2 in
let l = CicSubstitution.lift lift l in
- if sym then
- let uri,pl,pr =
- let eq,_,pl,pr = open_eq body in
- LibraryObjects.sym_eq_URI ~eq, pl, pr
- in
- let l = CicSubstitution.subst other pl in
- let r = CicSubstitution.subst other pr in
- mk_sym uri ty l r p
- else
- let parameters = CicUtil.metas_of_term p
-@ CicUtil.metas_of_term l
-@ CicUtil.metas_of_term r
-in (* ?if they are under a lambda? *)
+ let parameters =
+ CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r
+ in (* ?if they are under a lambda? *)
| Step (_,(_,id1,(_,id2),_)) ->
let m = find_deps m id1 in
let m = find_deps m id2 in
| Step (_,(_,id1,(_,id2),_)) ->
let m = find_deps m id1 in
let m = find_deps m id2 in
- M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+ (* without the uniq there is a stack overflow doing concatenation *)
+ let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in
+ let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
+ M.add i xxx m
(* now h is complete *)
let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
let proofs = List.filter (fun (_,c) -> c > 1) proofs in
(* now h is complete *)
let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
let proofs = List.filter (fun (_,c) -> c > 1) proofs in
let proof_of_id aux id =
let p,l,r = proof_of_id id in
try List.assoc id h,l,r with Not_found -> aux p, l, r
let proof_of_id aux id =
let p,l,r = proof_of_id id in
try List.assoc id h,l,r with Not_found -> aux p, l, r
| Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
| _ -> assert false
in
| Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
| _ -> assert false
in
(* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
if not cond then
prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
(* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
if not cond then
prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
let se = List.map (fun i -> Cic.Meta (i,[])) se in
let lets = get_duplicate_step_in_wfo l initial in
let letsno = List.length lets in
let _,mty,_,_ = open_eq ty in
let se = List.map (fun i -> Cic.Meta (i,[])) se in
let lets = get_duplicate_step_in_wfo l initial in
let letsno = List.length lets in
let _,mty,_,_ = open_eq ty in
| [] -> current_proof,se
| (rule,pos,id,subst,pred)::tl ->
let p,l,r = proof_of_id id in
| [] -> current_proof,se
| (rule,pos,id,subst,pred)::tl ->
let p,l,r = proof_of_id id in
in
let proof,se = aux se proof tl in
Subst.apply_subst_lift letsno subst proof,
List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
in
in
let proof,se = aux se proof tl in
Subst.apply_subst_lift letsno subst proof,
List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
in
-let refl_proof ty term =
- Cic.Appl
- [Cic.MutConstruct
- (Utils.eq_URI (), 0, 1, []);
- ty; term]
+let refl_proof eq_uri ty term =
+ Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term]
let rec aux ((table_l, table_r) as table) t1 t2 =
match t1, t2 with
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
let rec aux ((table_l, table_r) as table) t1 t2 =
match t1, t2 with
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
let m1_binding, table_l =
try List.assoc m1 table_l, table_l
with Not_found -> m2, (m1, m2)::table_l
let m1_binding, table_l =
try List.assoc m1 table_l, table_l
with Not_found -> m2, (m1, m2)::table_l
- | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
+ when LibraryObjects.is_eq_URI uri -> true
- | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
+ when LibraryObjects.is_eq_URI uri ->
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = Utils.compute_equality_weight stat in
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = Utils.compute_equality_weight stat in
let _, _, (ty, left, right, _), menv, _= open_equality equality in
let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
let argsno = List.length menv in
let t =
CicSubstitution.lift argsno
let _, _, (ty, left, right, _), menv, _= open_equality equality in
let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
let argsno = List.length menv in
let t =
CicSubstitution.lift argsno