and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
;;
+type goal = goal_proof * Cic.metasenv * Cic.term
+
(* globals *)
let maxid = ref 0;;
let id_to_eq = Hashtbl.create 1024;;
function
| Exact t -> Exact (Subst.apply_subst subst t)
| Step (s,(rule, id1, (pos,id2), pred)) ->
- Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+ Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
;;
let build_proof_step eq lift subst p1 p2 pos l r pred =
try List.assoc id h,l,r with Not_found -> aux p, l, r
in
let rec aux = function
- | Exact term -> CicSubstitution.lift lift term
+ | Exact term ->
+ CicSubstitution.lift lift term
| Step (subst,(rule, id1, (pos,id2), pred)) ->
let p1,_,_ = proof_of_id aux id1 in
let p2,l,r = proof_of_id aux id2 in
| Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
| _ -> assert false
in
- let p = build_proof_step eq lift subst p1 p2 pos l r pred in
+ let p = build_proof_step eq lift subst p1 p2 pos l r pred 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);
cic, p))
lets (letsno-1,initial)
in
- canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+(* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ * *)
+proof,
se
;;
let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
subst, menv, newmeta
+let fix_metas_goal newmeta goal =
+ let (proof, menv, ty) = goal in
+ let to_be_relocated =
+ HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
+ in
+ let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
+ let ty = Subst.apply_subst subst ty in
+ let proof =
+ match proof with
+ | [] -> assert false (* is a nonsense to relocate the initial goal *)
+ | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
+ in
+ newmeta+1,(proof, menv, ty)
+;;
+
let fix_metas newmeta eq =
let w, p, (ty, left, right, o), menv,_ = open_equality eq in
let to_be_relocated =
and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
+type goal = goal_proof * Cic.metasenv * Cic.term
+
val pp_proof:
(Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
Cic.term -> string
val build_goal_proof:
UriManager.uri -> goal_proof -> proof -> Cic.term-> int list ->
Cic.term * Cic.term list
+val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
+val fix_metas_goal: int -> goal -> int * goal
val fix_metas: int -> equality -> int * equality
val metas_of_proof: proof -> int list
+(* this should be used _only_ to apply (efficiently) this subst on the
+ * initial proof passed to build_goal_proof *)
val add_subst : Subst.substitution -> proof -> proof
exception TermIsNotAnEquality;;
(* $Id$ *)
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
module Index = Equality_indexing.DT (* discrimination tree based indexing *)
(*
module Index = Equality_indexing.DT (* path tree based indexing *)
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
-let superposition_left (metasenv, context, ugraph) table goal =
+let superposition_left (metasenv, context, ugraph) table goal maxmeta =
let names = Utils.names_of_context context in
let proof,menv,eq,ty,l,r = open_goal goal in
let c = !Utils.compare_terms l r in
- if c = Utils.Incomparable then
- begin
- let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
- let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
- (* prerr_endline "incomparable";
- 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
- end
- else
- match c with
- | Utils.Gt -> (* prerr_endline "GT"; *)
- let big,small,possmall = l,r,Utils.Right in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
- expansions
- | Utils.Lt -> (* prerr_endline "LT"; *)
- let big,small,possmall = 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
- | Utils.Eq -> []
- | _ ->
- prerr_endline
- ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
- assert false
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ 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
+ end
+ else
+ match c with
+ | Utils.Gt -> (* prerr_endline "GT"; *)
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = 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
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false
+ in
+ (* rinfresco le meta *)
+ List.fold_right
+ (fun g (max,acc) ->
+ let max,g = Equality.fix_metas_goal max g in max,g::acc)
+ newgoals (maxmeta,[])
;;
(** demodulation, when the target is a goal *)
(* $Id$ *)
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
module Index :
sig
module PosEqSet : Set.S
Index.t ->
Equality.equality ->
(Subst.substitution * Equality.equality * bool) option
+
val superposition_left :
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
- Index.t ->
- goal ->
- goal list
+ Index.t -> Equality.goal -> int ->
+ int * Equality.goal list
val superposition_right :
?subterms_only:bool ->
val demodulation_goal :
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- goal ->
- bool * goal
+ Equality.goal ->
+ bool * Equality.goal
val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
;;
let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
let names = names_of_context ctx in
+(*
Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
*)
match ty with
match Indexing.unification env table goal_equation with
| Some (subst, equality, swapped ) ->
prerr_endline
- ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
- prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+ ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+ prerr_endline
+ ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+ prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
let new_passive_goals =
if Utils.metas_of_term t1 = [] then passive_goals
else
- let new' =
- Indexing.superposition_left env (snd active) selected in
+ let newmaxmeta,new' =
+ Indexing.superposition_left env (snd active) selected
+ !maxmeta
+ in
+ maxmeta := newmaxmeta;
passive_goals @ new'
in
selected::active_goals, new_passive_goals
active_goals,
List.fold_left
(fun acc g ->
- let new' = Indexing.superposition_left env table g in
+ let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+ maxmeta := newmaxmeta;
acc @ new')
passive_goals active_goals
;;
prerr_endline
(Equality.pp_proof names goalproof newproof subsumption_subst
subsumption_id type_of_goal);
- prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
prerr_endline "ENDOFPROOFS";
(* generation of the CIC proof *)
let side_effects =
Equality.build_goal_proof
eq_uri goalproof initial type_of_goal side_effects
in
+ prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
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 t = Equality.term_of_equality eq_uri e in
prerr_endline (CicPp.pp t names))
eql;
+ prerr_endline ("\n result proofs: ");
+ List.iter (fun e ->
+ prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+ let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+ Subst.ppsubst s ^ "\n" ^
+ CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
if demod_table <> "" then
begin
let demod =
projects / helm.git / commitdiff