From 81d0d5a3aad863b991996c008f5c19076e771dbb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Nov 2007 14:24:24 +0000 Subject: [PATCH] compose tactic restore and added nocomposites keyword --- .../components/grafite/grafiteAstPp.ml | 4 +- .../grafite_parser/grafiteParser.ml | 6 +- helm/software/components/library/coercDb.ml | 16 ++--- .../components/library/librarySync.ml | 16 ++--- .../components/tactics/closeCoercionGraph.ml | 67 +++++++++++++------ helm/software/components/tactics/compose.ml | 40 ++++++++--- 6 files changed, 98 insertions(+), 51 deletions(-) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index cf9106ea3..fd3c444b9 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -265,9 +265,9 @@ let pp_default what uris = (String.concat " " (List.map UriManager.string_of_uri uris)) let pp_coercion uri do_composites arity saturations= - Printf.sprintf "coercion %s %d %d (* %s *)" + Printf.sprintf "coercion %s %d %d %s" (UriManager.string_of_uri uri) arity saturations - (if do_composites then "compounds" else "no compounds") + (if do_composites then "" else "nocomposites") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index a0fd33358..50a373e49 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -637,11 +637,13 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int -> + | IDENT "coercion" ; suri = URI ; arity = OPT int ; + saturations = OPT int; composites = OPT (IDENT "nocomposites") -> let arity = match arity with None -> 0 | Some x -> x in let saturations = match saturations with None -> 0 | Some x -> x in + let composites = match composites with None -> true | Some _ -> false in GrafiteAst.Coercion - (loc, UriManager.uri_of_string suri, true, arity, saturations) + (loc, UriManager.uri_of_string suri, composites, arity, saturations) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index 14ddf7c86..0ca40eb1c 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -73,16 +73,12 @@ let eq_carr ?(exact=false) src tgt = match src, tgt with | Uri src, Uri tgt -> let coarse_eq = UriManager.eq src tgt in - let src_noxpointer = UriManager.strip_xpointer src in - if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then - match - fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer) - with - | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true - | Cic.Constant _ -> true - | _ -> false - else - coarse_eq + let t = CicUtil.term_of_uri src in + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in + (match ty, exact with + | Cic.Prod _, true -> false + | Cic.Prod _, false -> coarse_eq + | _ -> coarse_eq) | Sort (Cic.Type _), Sort (Cic.Type _) -> true | Sort src, Sort tgt when src = tgt -> true | Term t1, Term t2 -> diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index c6682bd91..c36d84c90 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -318,7 +318,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations (CoercDb.to_list ()) in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[]) + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); + []) else let new_coercions = CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations @@ -337,14 +339,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); (* add the composites obj and they eventual lemmas *) let lemmas = - if add_composites then List.fold_left (fun acc (_,tgt,uri,saturations,obj,arity) -> add_single_obj uri obj refinement_toolkit; (uri,arity,saturations)::acc) [] new_coercions - else - [] in (* store that composite_uris are related to uri. the first component is * the stuff in the DB while the second is stuff for remove_obj *) @@ -354,8 +353,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) composite_uris; *) - UriManager.UriHashtbl.add coercion_hashtbl uri - (composite_uris,if add_composites then composite_uris else []); + UriManager.UriHashtbl.add + coercion_hashtbl uri (composite_uris,composite_uris); (* prerr_endline ("lemmas:"); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) @@ -373,7 +372,8 @@ let remove_coercion uri = List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) composites_in_db;*) UriManager.UriHashtbl.remove coercion_hashtbl uri; - CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u); + CoercDb.remove_coercion + (fun (_,_,u,_) -> UriManager.eq uri u); (* remove from the DB *) List.iter (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1)) @@ -381,7 +381,7 @@ let remove_coercion uri = (* remove composites from the lib *) List.iter remove_single_obj composites_in_lib with - Not_found -> () (* mhh..... *) + Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *) let generate_projections refinement_toolkit uri fields = diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 95b9fd6e0..7ed3c36e6 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -39,21 +39,33 @@ let get_closure_coercions src tgt uri coercions = in let uri = enrich uri tgt in let eq_carr ?exact s t = + debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t)); try - CoercDb.eq_carr ?exact s t + let rc = CoercDb.eq_carr ?exact s t in + debug_print(lazy(string_of_bool rc)); + rc with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false + | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> + debug_print (lazy("false")); + false in match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> + debug_print (lazy ("Uri, Uri4")); let c_from_tgt = List.filter - (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) + (fun (f,t,_) -> + + debug_print (lazy ("Uri, Uri3")); + 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)*)) + (fun (f,t,_) -> + + debug_print (lazy ("Uri, Uri2")); + eq_carr t src (*&& not (eq_carr f tgt)*)) coercions in (HExtlib.flatten_map @@ -70,6 +82,7 @@ let get_closure_coercions src tgt uri coercions = (fun (_,t,u2l) -> HExtlib.flatten_map (fun u1 -> + debug_print (lazy ("Uri, Uri1")); if eq_carr ~exact:true s t || eq_carr ~exact:true s tgt || eq_carr ~exact:true src t @@ -122,8 +135,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= names in let compose c1 nc1 c2 nc2 = - Cic.Appl (CicSubstitution.lift 1 c2 :: mk_implicits (nc2 - sat2 - 1) @ - Cic.Appl (CicSubstitution.lift 1 c1 :: mk_implicits nc1 ) :: + Cic.Appl ((*CicSubstitution.lift 1*) c2 :: mk_implicits (nc2 - sat2 - 1) @ + Cic.Appl ((*CicSubstitution.lift 1*) c1 :: mk_implicits nc1 ) :: mk_implicits sat2) in let rec create_subst_from_metas_to_rels n = function @@ -205,8 +218,14 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= let meta_to_be_coerced = try match List.nth l_c1 (c1_pis - sat1 - 1) with - | Cic.Meta (i,_) -> i - | _ -> assert false + | Cic.Meta (i,_) -> Some i + | t -> + debug_print + (lazy("meta_to_be_coerced: " ^ CicPp.ppterm t)); + debug_print + (lazy("c1_pis: " ^ string_of_int c1_pis ^ + " sat1:" ^ string_of_int sat1)); + None with Failure _ -> assert false in @@ -230,15 +249,20 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= | (i,_,_)::_ when i = n -> acc | _::tl -> position_of n (acc + 1) tl in - debug_print - (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced)); - let position_of_meta_to_be_coerced = - position_of meta_to_be_coerced 0 sorted in - debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^ - string_of_int position_of_meta_to_be_coerced)); - debug_print (lazy ("SATURATIONS: " ^ - string_of_int (List.length sorted - position_of_meta_to_be_coerced - 1))); - sorted, List.length sorted - position_of_meta_to_be_coerced - 1 + let saturations_res = + match meta_to_be_coerced with + | None -> 0 + | Some meta_to_be_coerced -> + debug_print + (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced)); + let position_of_meta_to_be_coerced = + position_of meta_to_be_coerced 0 sorted in + debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^ + string_of_int position_of_meta_to_be_coerced)); + List.length sorted - position_of_meta_to_be_coerced - 1 + in + debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res)); + sorted, saturations_res in let namer l n = let l = List.map (function Cic.Name s -> s | _ -> "A") l in @@ -270,6 +294,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= CicRefine.type_of_aux' metasenv context c univ in debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); + debug_print(lazy("COMPOSED REFINED (pretty): "^ + CicMetaSubst.ppterm_in_context [] ~metasenv term context)); (* let metasenv = order_metasenv metasenv in *) (* debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *) let body_metasenv, lambdas_metasenv = @@ -353,7 +379,7 @@ let filter_duplicates l coercions = try List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2 with - | Invalid_argument "List.for_all2" -> false) + | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false) coercions)) l @@ -404,6 +430,7 @@ let close_coercion_graph src tgt uri saturations baseuri = (* check if the coercion already exists *) let coercions = CoercDb.to_list () in let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in + debug_print (lazy("composed " ^ string_of_int (List.length todo_list))); let todo_list = filter_duplicates todo_list coercions in try let new_coercions = @@ -462,9 +489,9 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;; (* 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 sat2 = +let generate_composite c1 c2 context metasenv univ sat1 sat2 = let a,b,c,_,_ = - generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ + generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ in a,b,c ;; diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml index 317030404..6bc3dd0fa 100644 --- a/helm/software/components/tactics/compose.ml +++ b/helm/software/components/tactics/compose.ml @@ -23,6 +23,11 @@ * http://helm.cs.unibo.it/ *) +let debug = false;; +let debug_print = + if not debug then (fun _ -> ()) else (fun s -> prerr_endline (Lazy.force s)) +;; + let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;; let compose_core t2 t1 (proof, goal) = @@ -34,11 +39,27 @@ let compose_core t2 t1 (proof, goal) = let ty2,_ = CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph in - let saturated_ty2, menv_for_saturated_ty2 = + let saturated_ty2, menv_for_saturated_ty2, args_t2 = let maxm = CicMkImplicit.new_meta metasenv [] in - let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in - ty2, menv + let ty2, menv, args, _ = + TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in + ty2, menv, args + in + let saturations_t2 = + let rec aux n = function + | Cic.Meta (i,_)::tl -> + let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in + if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop) + CicUniv.oblivion_ugraph) + then n else aux (n+1) tl + | _::tl -> aux (n+1) tl + | [] -> n+1 + in + List.length args_t2 - aux 0 args_t2 +1 in + debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context + [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^ + " saturations_t2:" ^ string_of_int saturations_t2)); (* unifies t with saturated_ty2 and gives back a fresh meta of type t *) let unif menv t = let m, menv2 = @@ -64,22 +85,23 @@ let compose_core t2 t1 (proof, goal) = let b, newmenv, sb = unif menv s in if b then (saturations - cur - 1) :: - (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)) + (positions newmenv (cur + 1) saturations + (CicSubstitution.subst sb t)) else positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t) | _ -> [] in - (* position is a list of arities, that is if t1 : a -> b -> c and saturations is - * 0 then the computed term will be (t1 ? t2) of type a -> c - * if saturations is 1 then (t1 t2 ?) of type b -> c *) + (* position is a list of arities, that is if t1 : a -> b -> c and saturations + * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations + * is 1 then (t1 t2 ?) of type b -> c *) let rec generate positions menv acc = match positions with | [] -> acc, menv - | saturations::tl -> + | saturations_t1::tl -> try let t, menv1, _ = CloseCoercionGraph.generate_composite t2 t1 context menv - CicUniv.oblivion_ugraph saturations + CicUniv.oblivion_ugraph saturations_t2 saturations_t1 in assert (List.length menv1 = List.length menv); generate tl menv (t::acc) -- 2.39.2