X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=64f2faa7d796cb2d25fc84e4a0e6f5e9d93b836d;hb=4f0397e0faf85e400e244c815de4780660652faa;hp=2c1b30d677d9b6b99c6b5d5646f3c5f9ba18dfed;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 2c1b30d67..64f2faa7d 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -786,10 +786,11 @@ let build_proof_term bag eq h lift proof = aux proof ;; -let build_goal_proof bag eq l initial ty se context menv = +let build_goal_proof ?(contextualize=true) ?(forward=false) bag eq l initial ty se context menv = let se = List.map (fun i -> Cic.Meta (i,[])) se in let lets = get_duplicate_step_in_wfo bag l initial in let letsno = List.length lets in + let l = if forward then List.rev l else l in let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in let lets,_,h = List.fold_left @@ -803,15 +804,8 @@ let build_goal_proof bag eq l initial ty se context menv = acc@[id,real_cic],n+1,h) ([],0,[]) lets in - let _,lets = - List.fold_left - (fun (context,res) (id,cic) -> - let ty,_ = - CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph - in - Some (Cic.Name ("H" ^ string_of_int id), - Cic.Def (cic,ty))::context,res@[id,cic,ty] - ) (context,[]) lets + let lets = + List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets in let proof,se = let rec aux se current_proof = function @@ -819,7 +813,8 @@ let build_goal_proof bag eq l initial ty se context menv = | (rule,pos,id,subst,pred)::tl -> let p,l,r = proof_of_id bag id in let p = build_proof_term bag eq h letsno p in - let pos = if pos = Utils.Left then Utils.Right else Utils.Left in + let pos = if forward then pos else + if pos = Utils.Left then Utils.Right else Utils.Left in let varname = match rule with | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) @@ -852,10 +847,11 @@ let build_goal_proof bag eq l initial ty se context menv = p)) lets (letsno-1,initial) in - canonical - (contextualize_rewrites proof (CicSubstitution.lift letsno ty)) - context menv, - se + let proof = + if contextualize + then contextualize_rewrites proof (CicSubstitution.lift letsno ty) + else proof in + canonical proof context menv, se ;; let refl_proof eq_uri ty term = @@ -892,10 +888,12 @@ let relocate newmeta menv to_be_relocated = let irl = [] in let newmeta = Cic.Meta(maxmeta,irl) in let newsubst = Subst.buildsubst i context newmeta ty subst in - newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) + (* newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) *) + newsubst, (maxmeta,[],ty)::metasenv, maxmeta+1) to_be_relocated (Subst.empty_subst, [], newmeta+1) in - let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in + (* let subst = Subst.flatten_subst subst in *) + let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in subst, menv, newmeta let fix_metas_goal newmeta goal = @@ -916,11 +914,13 @@ let fix_metas_goal newmeta goal = let fix_metas bag newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in let to_be_relocated = -(* List.map (fun i ,_,_ -> i) menv *) + List.map (fun i ,_,_ -> i) menv +(* HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term left @ Utils.metas_of_term right @ Utils.metas_of_term ty)) +*) in let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in