let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ (* prerr_endline ("matching " ^ CicPp.ppterm term); *)
let cmp = !Utils.compare_terms in
let check = match termty with C.Implicit None -> false | _ -> true in
function
let what' = Subst.apply_subst subst what in
let other' = Subst.apply_subst subst other in
let subst', menv', ug' =
- unif_fun metasenv m context what' other' ugraph
+ unif_fun [] menv context what' other' ugraph
in
(match Subst.merge_subst_if_possible subst subst' with
| None -> ok_all what leftorright tl
;;
let unification_all x y z =
- subsumption_aux_all true x y z
+ prerr_endline "unification_all"; subsumption_aux_all true x y z
;;
let rec demodulation_aux bag ?from ?(typecheck=false)
in
let res =
- demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
+ demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
in
if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
Utils.guarded_simpl context
(apply_subst subst (CicSubstitution.subst other t))
in
- let bo' = apply_subst subst t in
- let ty = apply_subst subst ty in
- let name = Cic.Name "x" in
- let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ let name = Cic.Name "x" in
+ let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
+ let newgoalproofstep = (rule,pos,id,subst,pred) in
bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Founif.filter subst *) menv in
Utils.guarded_simpl context
(apply_subst subst (CicSubstitution.subst other t))
in
- let bo' = apply_subst subst t in
- let ty = apply_subst subst ty in
let name = Cic.Name "x" in
- let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
+ let newgoalproofstep = (rule,pos,id,subst,pred) in
bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Founif.filter subst *) menv in
prerr_endline (string_of_int (List.length expansionsl));
prerr_endline (string_of_int (List.length expansionsr));
*)
+ if expansionsl <> [] then prerr_endline "expansionl";
+ if expansionsr <> [] then prerr_endline "expansionr";
List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
@
List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr