X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=64f2faa7d796cb2d25fc84e4a0e6f5e9d93b836d;hb=0e3324ad8e6a552ee89f02371412f7bc2e83379f;hp=e35918c689b805b0e6b4037133e001e9583abe8f;hpb=37177f827ce843b30fb882fc39ecc674c1195d3d;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index e35918c68..64f2faa7d 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -323,8 +323,8 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " remove_refl p1 | _ -> Cic.Appl (List.map remove_refl args)) | Cic.Appl l -> Cic.Appl (List.map remove_refl l) - | Cic.LetIn (name,bo,rest) -> - Cic.LetIn (name,remove_refl bo,remove_refl rest) + | Cic.LetIn (name,bo,ty,rest) -> + Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest) | _ -> t in let rec canonical_trough_lambda context = function @@ -335,10 +335,11 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " and canonical context t = match t with - | Cic.LetIn(name,bo,rest) -> + | Cic.LetIn(name,bo,ty,rest) -> let bo = canonical_trough_lambda context bo in - let context' = (Some (name,Cic.Def (bo,None)))::context in - Cic.LetIn(name,bo,canonical context' rest) + let ty = canonical_trough_lambda context ty in + let context' = (Some (name,Cic.Def (bo,ty)))::context in + Cic.LetIn(name,bo,ty,canonical context' rest) | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args) when LibraryObjects.is_sym_eq_URI uri_sym -> (match p_of_sym ens tl with @@ -430,8 +431,10 @@ let contextualize uri ty left right t = when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p) - | Cic.LetIn (name,body,rest) -> - Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest) + | Cic.LetIn (name,body,bodyty,rest) -> + Cic.LetIn + (name,look_ahead (aux uri) body, bodyty, + aux uri ty left right ctx_d ctx_ty rest) | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) when LibraryObjects.is_eq_ind_URI uri_ind || LibraryObjects.is_eq_ind_r_URI uri_ind -> @@ -783,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 @@ -800,13 +804,17 @@ 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.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets + in let proof,se = let rec aux se current_proof = function | [] -> current_proof,se | (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) @@ -830,17 +838,20 @@ let build_goal_proof bag eq l initial ty se context menv = let n,proof = let initial = proof in List.fold_right - (fun (id,cic) (n,p) -> + (fun (id,cic,ty) (n,p) -> n-1, Cic.LetIn ( Cic.Name ("H"^string_of_int id), - cic, p)) + cic, + ty, + 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 = @@ -877,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 = @@ -901,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 @@ -944,9 +959,12 @@ let meta_convertibility_aux table t1 t2 = aux_ens table ens1 ens2 | C.Cast (s1, t1), C.Cast (s2, t2) | C.Prod (_, s1, t1), C.Prod (_, s2, t2) - | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) - | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> + | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) -> + let table = aux table s1 s2 in + aux table t1 t2 + | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) -> let table = aux table s1 s2 in + let table = aux table ty1 ty2 in aux table t1 t2 | C.Appl l1, C.Appl l2 -> ( try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 @@ -1050,13 +1068,13 @@ let meta_convertibility_subst t1 t2 menv = let (_,c,t) = CicUtil.lookup_meta x menv in let irl = CicMkImplicit.identity_relocation_list_for_metavariable c in - (x,(c,Cic.Meta(y,irl),t)) + (y,(c,Cic.Meta(x,irl),t)) with CicUtil.Meta_not_found _ -> try let (_,c,t) = CicUtil.lookup_meta y menv in let irl = CicMkImplicit.identity_relocation_list_for_metavariable c in - (y,(c,Cic.Meta(x,irl),t)) + (x,(c,Cic.Meta(y,irl),t)) with CicUtil.Meta_not_found _ -> assert false) l in Some subst with NotMetaConvertible -> @@ -1201,7 +1219,7 @@ let rec pp_proofterm name t context = | _ -> assert false in let rec skip_letin ctx = function - | Cic.LetIn (n,b,t) -> + | Cic.LetIn (n,b,_,t) -> pp_proofterm (Some (rename "Lemma " n)) b ctx:: skip_letin ((Some n)::ctx) t | t -> @@ -1223,7 +1241,7 @@ let rec pp_proofterm name t context = when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)-> pp true p | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] - when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)-> + when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)-> pp true p | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->