From: Enrico Tassi Date: Fri, 1 Jun 2007 14:58:50 +0000 (+0000) Subject: new compose tactic, still undocumented. X-Git-Tag: 0.4.95@7852~412 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=936f80cf031a7b034dd70fef49abb90e69f2e680;p=helm.git new compose tactic, still undocumented. moved from library to tactics the code for composing coercions. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 2dc077f06..9a453ae42 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -65,6 +65,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident list | ClearBody of loc * 'ident + | Compose of loc * 'term * 'term * 'ident intros_spec | Constructor of loc * int | Contradiction of loc | Cut of loc * 'ident option * 'term diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 811da9ddc..51b002de9 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -107,6 +107,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids) | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id]) | Constructor (_,n) -> "constructor " ^ string_of_int n + | Compose (_,t1, t2, intro_specs) -> + Printf.sprintf "compose %s %s%s" (term_pp t1) (term_pp t1) + (pp_intros_specs " as " intro_specs) | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> "cut " ^ term_pp term ^ diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 97be9ab2d..6b34c687c 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -96,6 +96,9 @@ let rec tactic_of_ast status ast = Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id + | GrafiteAst.Compose (_,t1,t2,(howmany, names)) -> + Tactics.compose t1 t2 ?howmany + ~mk_fresh_name_callback:(namer_of names) | GrafiteAst.Contradiction _ -> Tactics.contradiction | GrafiteAst.Constructor (_, n) -> Tactics.constructor n | GrafiteAst.Cut (_, ident, term) -> diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index d52b0e2de..31b881988 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -195,6 +195,10 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Clear (loc,id) | GrafiteAst.ClearBody (loc,id) -> metasenv,GrafiteAst.ClearBody (loc,id) + | GrafiteAst.Compose (loc, t1, t2, spec) -> + let metasenv,t1 = disambiguate_term context metasenv t1 in + let metasenv,t2 = disambiguate_term context metasenv t2 in + metasenv, GrafiteAst.Compose (loc, t1, t2, spec) | GrafiteAst.Constructor (loc,n) -> metasenv,GrafiteAst.Constructor (loc,n) | GrafiteAst.Contradiction loc -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 17144a852..10a841e2e 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -149,13 +149,16 @@ EXTEND GrafiteAst.AutoBatch (loc,params) | IDENT "cases"; what = tactic_term; specs = intros_spec -> - GrafiteAst.Cases (loc, what, specs) + GrafiteAst.Cases (loc, what, specs) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Change (loc, what, t) + | IDENT "compose"; t1 = tactic_term; t2 = tactic_term; + specs = intros_spec -> + GrafiteAst.Compose (loc, t1, t2, specs) | IDENT "constructor"; n = int -> GrafiteAst.Constructor (loc, n) | IDENT "contradiction" -> diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 6f2443e98..fe1c961fb 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -25,330 +25,16 @@ (* $Id$ *) -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -(* given the new coercion uri from src to tgt returns the list - * of new coercions to create. hte list elements are - * (source, list of coercions to follow, target) - *) -let get_closure_coercions src tgt uri coercions = - let eq_carr s t = - try - CoercDb.eq_carr s t - with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false - in - match src,tgt with - | CoercDb.Uri _, CoercDb.Uri _ -> - let c_from_tgt = - List.filter - (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) - coercions - in - let c_to_src = - List.filter - (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) - coercions - in - (HExtlib.flatten_map - (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ - (HExtlib.flatten_map - (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ - (HExtlib.flatten_map - (fun (s,_,u1l) -> - HExtlib.flatten_map - (fun (_,t,u2l) -> - HExtlib.flatten_map - (fun u1 -> - List.map - (fun u2 -> (s,[u1;uri;u2],t)) - u2l) - u1l) - c_from_tgt) - c_to_src) - | _ -> [] (* do not close in case source or target is not an indty ?? *) -;; - -let obj_attrs n = [`Class (`Coercion n); `Generated] - -exception UnableToCompose - -(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure rt c1 c2 univ arity = - let module RT = RefinementTool in - let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in - let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in - let rec mk_implicits = function - | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) - in - let rec mk_lambda_spline c namer = function - | 0 -> c - | n -> - Cic.Lambda - (namer n, - (Cic.Implicit None), - mk_lambda_spline c namer (n-1)) - in - let count_saturations_needed t arity = - let rec aux acc n = function - | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> - aux (acc@[name]) (n+1) t - | _ -> n,acc - in - let len,names = aux [] 0 t in - let len = len - arity in - List.fold_left - (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) - names - in - let compose c1 nc1 c2 nc2 = - Cic.Lambda - (Cic.Name "x", - (Cic.Implicit None), - Cic.Appl ( c2 :: mk_implicits nc2 @ - [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ])) - in -(* - let order_metasenv metasenv = - let module OT = struct type t = int let compare = Pervasives.compare end in - let module S = HTopoSort.Make (OT) in - let dep i = - let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in - let metas = List.map fst (CicUtil.metas_of_term ty) in - HExtlib.list_uniq (List.sort Pervasives.compare metas) - in - let om = - S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep - in - List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om - in -*) - let rec create_subst_from_metas_to_rels n = function - | [] -> [] - | (metano, ctx, ty)::tl -> - (metano,(ctx,Cic.Rel (n+1),ty)) :: - create_subst_from_metas_to_rels (n-1) tl - in - let split_metasenv metasenv n = - List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv - in - let purge_unused_lambdas metasenv t = - let rec aux = function - | Cic.Lambda (_, Cic.Meta (i,_), t) when - List.exists (fun (j,_,_) -> j = i) metasenv -> - aux (CicSubstitution.subst (Cic.Rel ~-100) t) - | Cic.Lambda (name, s, t) -> - Cic.Lambda (name, s, aux t) - | t -> t - in - aux t - in - let order_body_menv term body_metasenv = - let rec purge_lambdas = function - | Cic.Lambda (_,_,t) -> purge_lambdas t - | t -> t - in - let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in - let metas_that_saturate l = - List.fold_left - (fun (acc,n) t -> - let metas = CicUtil.metas_of_term t in - let metas = List.map fst metas in - let metas = - List.filter - (fun i -> List.for_all (fun (j,_) -> j<>i) acc) - metas - in - let metas = List.map (fun i -> i,n) metas in - metas @ acc, n+1) - ([],0) l - in - let l_c2 = skip_appl (purge_lambdas term) in - let l_c1 = - match HExtlib.list_last l_c2 with - | Cic.Appl l -> List.tl l - | _ -> assert false - in - (* i should cut off the laet elem of l_c2 *) - let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in - List.sort - (fun (i,ctx1,ty1) (j,ctx1,ty1) -> - try List.assoc i meta2no - List.assoc j meta2no - with Not_found -> assert false) - body_metasenv - in - let namer l n = - let l = List.map (function Cic.Name s -> s | _ -> "A") l in - let l = List.fold_left - (fun acc s -> - let rec add' s = - if List.exists ((=) s) acc then add' (s^"'") else s - in - acc@[add' s]) - [] l - in - let l = List.rev l in - Cic.Name (List.nth l (n-1)) - in - debug_print (lazy ("\nCOMPOSING")); - debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty)); - debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty)); - let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in - let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in - let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in - let spline_len = saturations_for_c1 + saturations_for_c2 in - let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in - debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); - let c, univ = - match rt.RT.type_of_aux' [] [] c univ with - | RT.Success (term, ty, metasenv, ugraph) -> - debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); -(* let metasenv = order_metasenv metasenv in *) -(* debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); *) - let body_metasenv, lambdas_metasenv = - split_metasenv metasenv spline_len - in -(* - debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); - debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv)); -*) - let body_metasenv = order_body_menv term body_metasenv in - debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); - let subst = create_subst_from_metas_to_rels spline_len body_metasenv in - debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst)); - let term = rt.RT.apply_subst subst term in - debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term)); - (match rt.RT.type_of_aux' metasenv [] term ugraph with - | RT.Success (term, ty, metasenv, ugraph) -> - let body_metasenv, lambdas_metasenv = - split_metasenv metasenv spline_len - in - let term = purge_unused_lambdas lambdas_metasenv term in - debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term)); - term, ugraph - | RT.Exception s -> debug_print s; raise UnableToCompose) - | RT.Exception s -> debug_print s; raise UnableToCompose - in - let c_ty,univ = - try - CicTypeChecker.type_of_aux' [] [] c univ - with CicTypeChecker.TypeCheckerFailure s -> - debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) (Lazy.force s))); - raise UnableToCompose - in - let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types c_ty - in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in - obj,univ +let close_coercion_graph_ref = ref + (fun _ _ _ _ _ -> [] : + RefinementTool.kit -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list) ;; -(* removes from l the coercions that are in !coercions *) -let filter_duplicates l coercions = - List.filter ( - fun (src,l1,tgt) -> - not (List.exists (fun (s,t,l2) -> - CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt && - try - List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2 - with - | Invalid_argument "List.for_all2" -> false) - coercions)) - l +let set_close_coercion_graph f = close_coercion_graph_ref := f;; -let mangle s t l = - (*List.fold_left - (fun s x -> s ^ "_" ^ x) - (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*) - s ^ "_OF_" ^ t +let close_coercion_graph r c1 c2 u s = + !close_coercion_graph_ref r c1 c2 u s ;; - -exception ManglingFailed of string - -let number_if_already_defined buri name l = - let err () = - raise - (ManglingFailed - ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con")) - in - let rec aux n = - let suffix = if n > 0 then string_of_int n else "" in - let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in - let uri = UriManager.uri_of_string suri in - let retry () = - if n < 100 then - begin - HLog.warn ("Uri " ^ suri ^ " already exists."); - aux (n+1) - end - else - err () - in - if List.exists (UriManager.eq uri) l then retry () - else - try - let _ = Http_getter.resolve' ~writable:true uri in - if Http_getter.exists' uri then retry () else uri - with - | Http_getter_types.Key_not_found _ -> uri - | Http_getter_types.Unresolvable_URI _ -> assert false - in - aux 0 -;; - -(* given a new coercion uri from src to tgt returns - * a list of (new coercion uri, coercion obj, universe graph) - *) -let close_coercion_graph rt src tgt uri baseuri = - (* check if the coercion already exists *) - let coercions = CoercDb.to_list () in - let todo_list = get_closure_coercions src tgt uri coercions in - let todo_list = filter_duplicates todo_list coercions in - try - let new_coercions = - List.fold_left ( - fun acc (src, l , tgt) -> - try - (match l with - | [] -> assert false - | he :: tl -> - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - let first_step = - Cic.Constant ("", - Some (CoercDb.term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs arity) - in - let o,_ = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure rt c - (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity - | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl - in - let name_src = CoercDb.name_of_carr src in - let name_tgt = CoercDb.name_of_carr tgt in - let by = List.map UriManager.name_of_uri l in - let name = mangle name_tgt name_src by in - let c_uri = - number_if_already_defined baseuri name - (List.map (fun (_,_,u,_) -> u) acc) - in - let named_obj = - match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) - | _ -> assert false - in - (src,tgt,c_uri,named_obj))::acc - with UnableToCompose -> acc - ) [] todo_list - in - new_coercions - with ManglingFailed s -> HLog.error s; [] -;; - diff --git a/components/library/cicCoercion.mli b/components/library/cicCoercion.mli index e3ee8dbfc..789e7d00d 100644 --- a/components/library/cicCoercion.mli +++ b/components/library/cicCoercion.mli @@ -25,6 +25,13 @@ (* This module implements the Coercions transitive closure *) +val set_close_coercion_graph : + (RefinementTool.kit -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list) + -> unit + val close_coercion_graph: RefinementTool.kit -> CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> diff --git a/components/tactics/.depend b/components/tactics/.depend index 07d7fc08b..b52cdc6b3 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -17,6 +17,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi +compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi @@ -30,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -61,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +closeCoercionGraph.cmo: closeCoercionGraph.cmi +closeCoercionGraph.cmx: closeCoercionGraph.cmi universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi autoTypes.cmo: autoTypes.cmi @@ -107,6 +111,10 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ variousTactics.cmi +compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \ + closeCoercionGraph.cmi compose.cmi +compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \ + closeCoercionGraph.cmx compose.cmi introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ @@ -196,13 +204,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \ primitiveTactics.cmi negationTactics.cmi inversion.cmi \ introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - auto.cmi tactics.cmi + compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx negationTactics.cmx inversion.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - auto.cmx tactics.cmi + compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/components/tactics/.depend.opt b/components/tactics/.depend.opt index 07d7fc08b..b52cdc6b3 100644 --- a/components/tactics/.depend.opt +++ b/components/tactics/.depend.opt @@ -17,6 +17,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi +compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi @@ -30,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -61,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +closeCoercionGraph.cmo: closeCoercionGraph.cmi +closeCoercionGraph.cmx: closeCoercionGraph.cmi universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi autoTypes.cmo: autoTypes.cmi @@ -107,6 +111,10 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ variousTactics.cmi +compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \ + closeCoercionGraph.cmi compose.cmi +compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \ + closeCoercionGraph.cmx compose.cmi introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ @@ -196,13 +204,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \ primitiveTactics.cmi negationTactics.cmi inversion.cmi \ introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - auto.cmi tactics.cmi + compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx negationTactics.cmx inversion.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - auto.cmx tactics.cmi + compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index e6f63eac0..b576f830b 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -10,6 +10,7 @@ INTERFACE_FILES = \ autoTypes.mli \ autoCache.mli \ paramodulation/utils.mli \ + closeCoercionGraph.mli \ paramodulation/subst.mli \ paramodulation/equality.mli\ paramodulation/founif.mli\ @@ -17,6 +18,7 @@ INTERFACE_FILES = \ paramodulation/indexing.mli \ paramodulation/saturation.mli \ variousTactics.mli \ + compose.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli \ auto.mli \ diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml new file mode 100644 index 000000000..a009944f8 --- /dev/null +++ b/components/tactics/closeCoercionGraph.ml @@ -0,0 +1,371 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *) + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +(* given the new coercion uri from src to tgt returns the list + * of new coercions to create. hte list elements are + * (source, list of coercions to follow, target) + *) +let get_closure_coercions src tgt uri coercions = + let eq_carr s t = + try + CoercDb.eq_carr s t + with + | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false + in + match src,tgt with + | CoercDb.Uri _, CoercDb.Uri _ -> + let c_from_tgt = + List.filter + (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) + coercions + in + let c_to_src = + List.filter + (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) + coercions + in + (HExtlib.flatten_map + (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ + (HExtlib.flatten_map + (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ + (HExtlib.flatten_map + (fun (s,_,u1l) -> + HExtlib.flatten_map + (fun (_,t,u2l) -> + HExtlib.flatten_map + (fun u1 -> + List.map + (fun u2 -> (s,[u1;uri;u2],t)) + u2l) + u1l) + c_from_tgt) + c_to_src) + | _ -> [] (* do not close in case source or target is not an indty ?? *) +;; + +let obj_attrs n = [`Class (`Coercion n); `Generated] + +exception UnableToCompose + +(* generate_composite (c2 (c1 s)) in the universe graph univ + * both living in the same context and metasenv *) +let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = + let module RT = RefinementTool in + let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in + let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in + let rec mk_implicits = function + | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) + in + let rec mk_lambda_spline c namer = function + | 0 -> c + | n -> + Cic.Lambda + (namer n, + (Cic.Implicit None), + mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1)) + in + let count_saturations_needed t arity = + let rec aux acc n = function + | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> + aux (acc@[name]) (n+1) t + | _ -> n,acc + in + let len,names = aux [] 0 t in + let len = len - arity in + List.fold_left + (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) + names + in + let compose c1 nc1 c2 nc2 = + Cic.Lambda + (Cic.Name "x", (Cic.Implicit None), + (Cic.Appl ( CicSubstitution.lift 1 c2 :: mk_implicits nc2 @ + [ Cic.Appl ( CicSubstitution.lift 1 c1 :: mk_implicits nc1 @ + [if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None]) + ]))) + in +(* + let order_metasenv metasenv = + let module OT = struct type t = int let compare = Pervasives.compare end in + let module S = HTopoSort.Make (OT) in + let dep i = + let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in + let metas = List.map fst (CicUtil.metas_of_term ty) in + HExtlib.list_uniq (List.sort Pervasives.compare metas) + in + let om = + S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep + in + List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om + in +*) + let rec create_subst_from_metas_to_rels n = function + | [] -> [] + | (metano, ctx, ty)::tl -> + (metano,(ctx,Cic.Rel (n+1),ty)) :: + create_subst_from_metas_to_rels (n-1) tl + in + let split_metasenv metasenv n = + List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv + in + let purge_unused_lambdas metasenv t = + let rec aux = function + | Cic.Lambda (_, Cic.Meta (i,_), t) when + List.exists (fun (j,_,_) -> j = i) metasenv -> + aux (CicSubstitution.subst (Cic.Rel ~-100) t) + | Cic.Lambda (name, s, t) -> + Cic.Lambda (name, s, aux t) + | t -> t + in + aux t + in + let order_body_menv term body_metasenv = + let rec purge_lambdas = function + | Cic.Lambda (_,_,t) -> purge_lambdas t + | t -> t + in + let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in + let metas_that_saturate l = + List.fold_left + (fun (acc,n) t -> + let metas = CicUtil.metas_of_term t in + let metas = List.map fst metas in + let metas = + List.filter + (fun i -> List.for_all (fun (j,_) -> j<>i) acc) + metas + in + let metas = List.map (fun i -> i,n) metas in + metas @ acc, n+1) + ([],0) l + in + let l_c2 = skip_appl (purge_lambdas term) in + let l_c1 = + match HExtlib.list_last l_c2 with + | Cic.Appl l -> List.tl l + | _ -> assert false + in + (* i should cut off the laet elem of l_c2 *) + let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in + List.sort + (fun (i,ctx1,ty1) (j,ctx1,ty1) -> + try List.assoc i meta2no - List.assoc j meta2no + with Not_found -> + assert false) + body_metasenv + in + let namer l n = + let l = List.map (function Cic.Name s -> s | _ -> "A") l in + let l = List.fold_left + (fun acc s -> + let rec add' s = + if List.exists ((=) s) acc then add' (s^"'") else s + in + acc@[add' s]) + [] l + in + let l = List.rev l in + Cic.Name (List.nth l (n-1)) + in + debug_print (lazy ("\nCOMPOSING")); + debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty)); + debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty)); + let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in + let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in + let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in + let spline_len = saturations_for_c1 + saturations_for_c2 in + let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in + debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); + let c, metasenv, univ = + try + let term, ty, metasenv, ugraph = + CicRefine.type_of_aux' metasenv context c univ + in + debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); +(* let metasenv = order_metasenv metasenv in *) +(* debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *) + let body_metasenv, lambdas_metasenv = + split_metasenv metasenv (spline_len + List.length context) + in + debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); + debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv)); + let body_metasenv = order_body_menv term body_metasenv in + debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); + let subst = create_subst_from_metas_to_rels spline_len body_metasenv in + debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst)); + let term = CicMetaSubst.apply_subst subst term in + debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term)); + let term, ty, metasenv, ugraph = + CicRefine.type_of_aux' metasenv context term ugraph + in + let body_metasenv, lambdas_metasenv = + split_metasenv metasenv (spline_len + List.length context) + in + let term = purge_unused_lambdas lambdas_metasenv term in + debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term)); + debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); + term, metasenv, ugraph + with + | CicRefine.RefineFailure s + | CicRefine.Uncertain s -> debug_print s; + raise UnableToCompose + in + c, metasenv, univ +;; + +let build_obj c univ arity = + let c_ty,univ = + try + CicTypeChecker.type_of_aux' [] [] c univ + with CicTypeChecker.TypeCheckerFailure s -> + debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" + (CicPp.ppterm c) (Lazy.force s))); + raise UnableToCompose + in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types c_ty + in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in + obj,univ +;; + +(* removes from l the coercions that are in !coercions *) +let filter_duplicates l coercions = + List.filter ( + fun (src,l1,tgt) -> + not (List.exists (fun (s,t,l2) -> + CoercDb.eq_carr s src && + CoercDb.eq_carr t tgt && + try + List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2 + with + | Invalid_argument "List.for_all2" -> false) + coercions)) + l + +let mangle s t l = + (*List.fold_left + (fun s x -> s ^ "_" ^ x) + (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*) + s ^ "_OF_" ^ t +;; + +exception ManglingFailed of string + +let number_if_already_defined buri name l = + let err () = + raise + (ManglingFailed + ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con")) + in + let rec aux n = + let suffix = if n > 0 then string_of_int n else "" in + let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in + let uri = UriManager.uri_of_string suri in + let retry () = + if n < 100 then + begin + HLog.warn ("Uri " ^ suri ^ " already exists."); + aux (n+1) + end + else + err () + in + if List.exists (UriManager.eq uri) l then retry () + else + try + let _ = Http_getter.resolve' ~writable:true uri in + if Http_getter.exists' uri then retry () else uri + with + | Http_getter_types.Key_not_found _ -> uri + | Http_getter_types.Unresolvable_URI _ -> assert false + in + aux 0 +;; + +(* given a new coercion uri from src to tgt returns + * a list of (new coercion uri, coercion obj, universe graph) + *) +let close_coercion_graph _ src tgt uri baseuri = + (* check if the coercion already exists *) + let coercions = CoercDb.to_list () in + let todo_list = get_closure_coercions src tgt uri coercions in + let todo_list = filter_duplicates todo_list coercions in + try + let new_coercions = + List.fold_left + (fun acc (src, l , tgt) -> + try + (match l with + | [] -> assert false + | he :: tl -> + let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in + let first_step = + Cic.Constant ("", + Some (CoercDb.term_of_carr (CoercDb.Uri he)), + Cic.Sort Cic.Prop, [], obj_attrs arity) + in + let o,_ = + List.fold_left (fun (o,univ) coer -> + match o with + | Cic.Constant (_,Some c,_,[],_) -> + let t, menv, univ = + generate_composite c + (CoercDb.term_of_carr (CoercDb.Uri coer)) + [] [] univ arity true + in + assert (menv = []); + build_obj t univ arity + | _ -> assert false + ) (first_step, CicUniv.empty_ugraph) tl + in + let name_src = CoercDb.name_of_carr src in + let name_tgt = CoercDb.name_of_carr tgt in + let by = List.map UriManager.name_of_uri l in + let name = mangle name_tgt name_src by in + let c_uri = + number_if_already_defined baseuri name + (List.map (fun (_,_,u,_) -> u) acc) + in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) + | _ -> assert false + in + (src,tgt,c_uri,named_obj))::acc + with UnableToCompose -> acc + ) [] todo_list + in + new_coercions + with ManglingFailed s -> HLog.error s; [] +;; + +CicCoercion.set_close_coercion_graph close_coercion_graph;; diff --git a/components/tactics/closeCoercionGraph.mli b/components/tactics/closeCoercionGraph.mli new file mode 100644 index 000000000..d0bdb4410 --- /dev/null +++ b/components/tactics/closeCoercionGraph.mli @@ -0,0 +1,40 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* This module implements the Coercions transitive closure *) + +val close_coercion_graph: + RefinementTool.kit -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list + +exception UnableToCompose + +val generate_composite: + Cic.term -> Cic.term -> Cic.context -> + Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> + bool (* last lambda goes with innermost arg *) -> + Cic.term * Cic.metasenv * CicUniv.universe_graph diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml new file mode 100644 index 000000000..f090c3dbf --- /dev/null +++ b/components/tactics/compose.ml @@ -0,0 +1,73 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) = + let _,metasenv,_subst,_,_,_ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let ty1,_ = + CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph + in + let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 in + let rec generate arity menv acc = + if arity < 0 then acc, menv + else + try + let t, menv, _ = + CloseCoercionGraph.generate_composite t1 t2 context menv + CicUniv.oblivion_ugraph arity false + in + generate (arity - 1) menv (t::acc) + with + | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc + in + let terms, metasenv = generate (count_pi ty1) metasenv [] in + let proof = + let uri, _, _subst, bo, ty, attrs = proof in + uri, metasenv, _subst, bo, ty, attrs + in + let proof, goal = + List.fold_left + (fun (proof,goal) t -> + let lazy_of t = + ProofEngineTypes.const_lazy_term t + in + let proof, gl = + ProofEngineTypes.apply_tactic + (VariousTactics.generalize_tac (Some (lazy_of t), [], None)) + (proof,goal) + in + assert(List.length gl = 1); + proof,List.hd gl) + (proof,goal) terms + in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ()) + (proof,goal) +;; + +let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 = + ProofEngineTypes.mk_tactic + (compose_tac ?howmany ?mk_fresh_name_callback t1 t2) +;; diff --git a/components/tactics/compose.mli b/components/tactics/compose.mli new file mode 100644 index 000000000..37e69d42f --- /dev/null +++ b/components/tactics/compose.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val compose_tac: + ?howmany:int -> + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term -> Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 527a8abb3..1ccd2adcb 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -71,3 +71,7 @@ let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let unfold = ReductionTactics.unfold_tac let whd = ReductionTactics.whd_tac +let compose = Compose.compose_tac + +(* keep linked *) +let _ = CloseCoercionGraph.close_coercion_graph;; diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 70773a4a7..4307e6b03 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri May 25 11:09:42 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun 1 13:27:04 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -102,3 +102,7 @@ val unfold : Cic.lazy_term option -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val compose : + ?howmany:int -> + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term -> Cic.term -> ProofEngineTypes.tactic diff --git a/matita/matita.lang b/matita/matita.lang index 36a1f0b29..fbf7f2ab2 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -83,12 +83,12 @@ absurd apply assumption - auto - paramodulation + autobatch cases clear clearbody change + compose constructor contradiction cut @@ -178,6 +178,7 @@ check hint set + auto