let open_pred pred =
match pred with
- | 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
;;
* that is used only by the base case
*
* ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
+ * ty_ctx is the type of ctx_d
*)
- let rec aux uri ty left right ctx_d = function
+ let rec aux uri ty left right ctx_d ctx_ty = function
| 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
- mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+ mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
| Cic.LetIn (name,body,rest) ->
(* we should go in body *)
- Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+ Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest)
| 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 m, ctx_c =
+ let m, ctx_c, ty2 =
let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
(* they were under a lambda *)
- let m = CicSubstitution.subst (Cic.Implicit None) m in
+ let m = CicSubstitution.subst hole m in
let ctx_c = CicSubstitution.subst hole ctx_c in
- m, ctx_c
+ let ty2 = CicSubstitution.subst hole ty2 in
+ m, ctx_c, ty2
in
(* create the compound context and put the terms under it *)
let ctx_dc = compose_contexts ctx_d ctx_c in
(* now put the proofs in the compound context *)
let p1 = (* p1: dc_what = d_m *)
if is_not_fixed_lp then
- aux uri ty1 c_what m ctx_d p1
+ aux uri ty2 c_what m ctx_d ctx_ty p1
else
- mk_sym uri_sym ty d_m dc_what
- (aux uri ty1 m c_what ctx_d p1)
+ mk_sym uri_sym ctx_ty d_m dc_what
+ (aux uri ty2 m c_what ctx_d ctx_ty p1)
in
let p2 = (* p2: dc_other = dc_what *)
if avoid_eq_ind then
- mk_sym uri_sym ty dc_what dc_other
- (aux uri ty1 what other ctx_dc p2)
+ mk_sym uri_sym ctx_ty dc_what dc_other
+ (aux uri ty1 what other ctx_dc ctx_ty p2)
else
- aux uri ty1 other what ctx_dc p2
+ aux uri ty1 other what ctx_dc ctx_ty p2
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,
- (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)
in
- mk_trans uri_trans ty a b c paeqb pbeqc
+ mk_trans uri_trans ctx_ty a b c paeqb pbeqc
+ | t when ctx_d = hole -> t
| t ->
let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
let ctx_d = CicSubstitution.lift 1 ctx_d in
put_in_ctx ctx_d (Cic.Rel 1)
in
- let lty = CicSubstitution.lift 1 ty in
+ let lty = CicSubstitution.lift 1 ctx_ty 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
- let refl_eq = mk_refl uri ty d_left in
- mk_sym uri_sym ty d_right d_left
+ let refl_eq = mk_refl uri ctx_ty d_left in
+ mk_sym uri_sym ctx_ty d_right d_left
(mk_eq_ind uri_ind ty left pred refl_eq right t)
in
- aux uri ty left right hole t
+ aux uri ty left right hole ty t
;;
let contextualize_rewrites t ty =
cic, p))
lets (letsno-1,initial)
in
- (proof,se)
- (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
- se *)
+ canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ se
;;
let refl_proof 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 tl1, tl2 = [],[] in
let m1_binding, table_l =
try List.assoc m1 table_l, table_l
with Not_found -> m2, (m1, m2)::table_l
let res, lifted_term =
match term with
| C.Meta (i, l) ->
+ let l = [] in
let l', lifted_l =
List.fold_right
(fun arg (res, lifted_tl) ->
Utils.compare_weights ~normalize:true
(Utils.weight_of_term l) (Utils.weight_of_term r)
in
- let big,small,possmall =
- match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
- in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+
+ if c = Utils.Incomparable then
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ prerr_endline "ZZZ";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+ else
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
;;
(** demodulation, when the target is a goal *)
let rec is_simple_term = function
| Cic.Appl ((Cic.Meta _)::_) -> false
| Cic.Appl l -> List.for_all is_simple_term l
- | Cic.Meta (i, l) -> check_irl 1 l
+ | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
| Cic.Rel _ -> true
| Cic.Const _ -> true
| Cic.MutInd (_, _, []) -> true
active, passive, newa, newp *)
;;
-
let close env new' given =
let new_pos, new_table, min_weight =
List.fold_left
when left = right && iseq uri ->
let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
Some (goalproof, reflproof, 0, Subst.empty_subst,m)
+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
+ when iseq uri ->
+ (let _,context,_ = env in
+ try
+ let s,m,_ =
+ Inference.unification m m context left right CicUniv.empty_ugraph
+ in
+ let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+ let m = Subst.apply_subst_metasenv s m in
+ Some (goalproof, reflproof, 0, s,m)
+ with _ -> None)
| _ -> None
;;
let infer_goal_set_with_current env current goals =
let active_goals, passive_goals = goals in
let _,table,_ = build_table [current] in
+ let _,_,_,_,id = Equality.open_equality current in
active_goals,
List.fold_left
(fun acc g ->
let new' = Indexing.superposition_left env table g in
+ if id = 2 then
+ begin
+ prerr_endline "XXXXXXX";
+ List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ;
+ end;
acc @ new')
passive_goals active_goals
;;
let given_clause
((_,context,_) as env) goals theorems passive active max_iterations max_time
=
+ let names = names_of_context context in
let initial_time = Unix.gettimeofday () in
let iterations_left iterno =
let now = Unix.gettimeofday () in
ParamodulationFailure "No more passive"(*maybe this is a success! *)
else
begin
+ let goals = infer_goal_set env active goals in
+ let goals = infer_goal_set env active goals in
let goals = infer_goal_set env active goals in
let current, passive = select env goals passive in
+ let _,_,goaltype = List.hd (fst goals) in
+ prerr_endline (Printf.sprintf "Current goal = %s\n"
+ (CicPp.pp goaltype names));
prerr_endline (Printf.sprintf "Selected = %s\n"
(Equality.string_of_equality ~env current));
(* SIMPLIFICATION OF CURRENT *)
let res =
- forward_simplify env (Positive, current) ~passive active
+ forward_simplify env (Positive, current) (*~passive*) active
in
match res with
| None -> step goals theorems passive active (iterno+1)
| Some p, Some rp -> simplify (new' @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
+ if iterno = 36 || iterno = 654 then
+ begin
+ prerr_endline "...................";
+ List.iter
+ (fun x -> prerr_endline (Equality.string_of_equality
+~env:env x)) new';
+ prerr_endline "FINE...................";
+ end;
prerr_endline "simpl goal with new";
let goals =
let a,b,_ = build_table new' in
let initial = Equality.add_subst subsumption_subst newproof in
Equality.build_goal_proof goalproof initial type_of_goal side_effects
in
+ let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+ let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
(*prerr_endline (CicPp.pp goal_proof names);*)
(* ?? *)
let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
| None ->
[i,context,ty], (Cic.Meta(i,[]))::acc2,
(Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl)))
- ([],[],[],None) proof_menv
+ ([],[],[],None)
+ (List.filter
+ (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
+ proof_menv)
in
let replace where =
(* we need this fake equality since the metas of the hypothesis may be
projects / helm.git / commitdiff