* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $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 *)
let s =
match mode with
| Matching ->
- let _ = <:start<retrieve_generalizations>> in
- <:stop<retrieve_generalizations
Index.retrieve_generalizations tree term
- >>
| Unification ->
- let _ = <:start<retrieve_unifiables>> in
- <:stop<retrieve_unifiables
Index.retrieve_unifiables tree term
- >>
in
Index.PosEqSet.elements s
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
in
- if sign = Utils.Positive then
(bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
(Cic.Lambda (name, ty, bo'))))))
- else
- assert false
-(*
- begin
- prerr_endline "***************************************negative";
- let metaproof =
- incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let proof'_old' =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof'_old)
- in
- let proof'_new' = assert false (* not implemented *) in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0, (proof'_new',proof'_old'),
- (ty, other, what, Utils.Incomparable),menv')
- in
- let target_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- assert false, (* not implemented *)
- (match snd proof with
- | Equality.BasicProof _ ->
- (* print_endline "replacing a BasicProof"; *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
- (* print_endline "replacing another ProofGoalBlock"; *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false)
- in
- let refl =
- C.Appl [C.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);
- eq_ty; if is_left then right else left]
- in
- (bo,
- (assert false, (* not implemented *)
- Equality.ProofGoalBlock
- (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
- end
-*)
in
- let newmenv = (* Inference.filter subst *) menv in
-(*
- let _ =
- if Utils.debug_metas then
- try ignore(CicTypeChecker.type_of_aux'
- newmenv context
- (Equality.build_proof_term newproof) ugraph);
- ()
- with exc ->
- prerr_endline "sempre lui";
- prerr_endline (Subst.ppsubst subst);
- prerr_endline (CicPp.ppterm
- (Equality.build_proof_term newproof));
- prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
- prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
- prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
- prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
- newmenv));
- raise exc;
- else ()
- in
-*)
+ let newmenv = menv in
let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, ordering) in
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table sign newtarget
+ demodulation_equality ?from eq_uri newmeta env table newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table sign newtarget
+ demodulation_equality ?from eq_uri newmeta env table newtarget
| None ->
newmeta, target
in
| C.Appl l ->
let l', lifted_l =
- List.fold_right
- (fun arg (res, lifted_tl) ->
+ List.fold_left
+ (fun (res, lifted_tl) arg ->
let arg_res, lifted_arg =
betaexpand_term metasenv context ugraph table lift_amount arg
in
lifted_arg::r, s, m, ug, eq_found)
res),
lifted_arg::lifted_tl)
- ) l ([], [])
+ ) ([], []) (List.rev l)
in
(List.map
(fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
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_weights ~normalize:true
- (Utils.weight_of_term l) (Utils.weight_of_term r)
+ let c = !Utils.compare_terms l r in
+ 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
-
- 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
- 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
+ (* 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 *)
| None -> do_right ()
;;
-let get_stats () = <:show<Indexing.>> ;;
+let get_stats () = "" ;;
projects / helm.git / blobdiff