eq
;;
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+ let id = -1 in
+ uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+;;
+
+
let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
(weight,proof,(ty,l,r,o),m,id)
->
let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
let pred_of t = CicSubstitution.subst t lhs in
let pred_of_what = pred_of what in
let pred_of_other = pred_of other in
* ====================================
* inject p2: P(what) = P(other)
*)
- let inject ty lhs what other p2 =
+ let rec inject ty lhs what other p2 =
+ match p2 with
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,plm,pmr = open_trans ens tl in
+ mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
+ (inject ty lhs m r pmr) (inject ty lhs l m plm)
+ | _ ->
let liftedty = CicSubstitution.lift 1 ty in
let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
let refl_eq_part =
Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
in
- mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+ (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
(Cic.Lambda (Cic.Name "foo",ty,
(Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
- refl_eq_part what p2
+ [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+ refl_eq_part what p2)
in
mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (mk_sym uri_sym ty pred_of_what pred_of_other
- (inject ty lhs what other p2)
- ) p1
+ (inject ty lhs what other p2) p1
| Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
->
let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
let pred_of t = CicSubstitution.subst t lhs in
let pred_of_what = pred_of what in
let pred_of_other = pred_of other in
* ====================================
* inject p2: P(what) = P(other)
*)
- let inject ty lhs what other p2 =
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
- refl_eq_part what p2
+ let rec inject ty lhs what other p2 =
+ match p2 with
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,plm,pmr = open_trans ens tl in
+ mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
+ (inject ty lhs m l plm)
+ (inject ty lhs r m pmr)
+ | _ ->
+ let liftedty = CicSubstitution.lift 1 ty in
+ let lifted_pred_of_other =
+ CicSubstitution.lift 1 (pred_of other) in
+ let refl_eq_part =
+ Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+ in
+ mk_eq_ind (Utils.eq_ind_URI ()) ty other
+ (Cic.Lambda (Cic.Name "foo",ty,
+ (Cic.Appl
+ [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+ refl_eq_part what p2
in
mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (mk_sym uri_sym ty pred_of_other pred_of_what
- (inject ty lhs what other p2)
- ) p1
+ (inject ty lhs what other p2) p1
| Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
->
let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
let pred_of t = CicSubstitution.subst t rhs in
let pred_of_what = pred_of what in
let pred_of_other = pred_of other in
* ====================================
* inject p2: P(what) = P(other)
*)
- let inject ty lhs what other p2 =
+ let rec inject ty lhs what other p2 =
+ match p2 with
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,plm,pmr = open_trans ens tl in
+ mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
+ (inject ty lhs m r pmr)
+ (inject ty lhs l m plm)
+ | _ ->
let liftedty = CicSubstitution.lift 1 ty in
let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
let refl_eq_part =
Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
in
- mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+ (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
(Cic.Lambda (Cic.Name "foo",ty,
(Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
- refl_eq_part what p2
+ [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
+ refl_eq_part what p2)
in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
- (mk_sym uri_sym ty pred_of_what pred_of_other
- (inject ty rhs other what p2))
+ mk_trans uri_trans ty lhs pred_of_what pred_of_other
+ p1 (inject ty rhs other what p2)
| Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
->
let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
let pred_of t = CicSubstitution.subst t rhs in
let pred_of_what = pred_of what in
let pred_of_other = pred_of other in
* ====================================
* inject p2: P(what) = P(other)
*)
- let inject ty lhs what other p2 =
+ let rec inject ty lhs what other p2 =
+ match p2 with
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,plm,pmr = open_trans ens tl in
+ (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
+ (inject ty lhs m l plm)
+ (inject ty lhs r m pmr))
+ | _ ->
let liftedty = CicSubstitution.lift 1 ty in
let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
let refl_eq_part =
mk_eq_ind (Utils.eq_ind_URI ()) ty other
(Cic.Lambda (Cic.Name "foo",ty,
(Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+ [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
refl_eq_part what p2
in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
- (mk_sym uri_sym ty pred_of_other pred_of_what
- (inject ty rhs other what p2))
+ mk_trans uri_trans ty lhs pred_of_what pred_of_other
+ p1 (inject ty rhs other what p2)
| _, Utils.Left ->
mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
| _, Utils.Right ->
build_proof_step subst p1 p2 pos l r pred
in
aux proof
+;;
+
+let wfo goalproof =
+ let rec aux acc id =
+ let p,_,_ = proof_of_id id in
+ match p with
+ | Exact _ -> if (List.mem id acc) then acc else id :: acc
+ | Step (_,(_,id1, (_,id2), _)) ->
+ let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
+ let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
+ id :: acc
+ in
+ List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
+;;
+
+let string_of_id names id =
+ try
+ let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ match p with
+ | Exact t ->
+ Printf.sprintf "%d = %s: %s = %s" id
+ (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
+ | Step (_,(step,id1, (_,id2), _) ) ->
+ Printf.sprintf "%6d: %s %6d %6d %s = %s" id
+ (if step = SuperpositionRight then "SupR" else "Demo")
+ id1 id2 (CicPp.pp l names) (CicPp.pp r names)
+ with
+ Not_found -> assert false
+
+let pp_proof names goalproof =
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^
+ "\ngoal is demodulated with " ^
+ (String.concat " "
+ ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
let build_goal_proof l initial =
let proof =
projects / helm.git / blobdiff