(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
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 ->
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 ->
(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
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 *)
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))
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))
(* 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 =
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
(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
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
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
| (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
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 =
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
(* 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 =
(* 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
;;
* 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) =
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 =
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)
projects / helm.git / commitdiff