From 910c252965fe17d6b5af92e4658e7d02bac82d58 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jul 2008 21:01:17 +0000 Subject: [PATCH] simplified coercDb implementation with additional info about the position of the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a coercion and ? are implicits or saturations generated to apply the coercion to x. New case in unification, when there is a triangular pullback and the coerced is not flexible an unfolding of the composed coercion is attempted. this helps in the case: C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z where C = C1 composed C2 but X is rigid abd conversion fails cause x != ? and the heads are different... unfolding C helps --- .../components/acic_content/acic2content.ml | 32 ++-- .../acic_content/termAcicContent.ml | 39 ++-- .../components/cic_unification/cicRefine.ml | 46 ++--- .../cic_unification/cicUnification.ml | 99 ++++++---- .../components/cic_unification/coercGraph.ml | 97 +++++----- .../components/cic_unification/coercGraph.mli | 5 +- .../grafite_engine/grafiteEngine.ml | 10 +- .../components/grafite_engine/grafiteSync.mli | 4 +- .../components/library/cicCoercion.ml | 3 +- .../components/library/cicCoercion.mli | 4 +- helm/software/components/library/coercDb.ml | 172 +++++++----------- helm/software/components/library/coercDb.mli | 46 ++--- .../components/library/librarySync.ml | 54 +++--- .../components/library/librarySync.mli | 2 +- .../components/tactics/closeCoercionGraph.ml | 97 +++++----- .../components/tactics/closeCoercionGraph.mli | 2 +- helm/software/components/tactics/universe.ml | 2 +- .../contribs/dama/dama/models/list_support.ma | 42 +++-- .../models/nat_dedekind_sigma_complete.ma | 2 +- .../contribs/dama/dama/models/nat_lebesgue.ma | 3 +- .../matita/contribs/dama/dama/supremum.ma | 2 +- helm/software/matita/matita.ml | 4 +- helm/software/matita/matitaExcPp.ml | 2 - 23 files changed, 382 insertions(+), 387 deletions(-) diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index b1423c5ab..c8ff783c3 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -561,7 +561,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t raise Not_a_proof | C.AAppl (id,li) -> (try coercion - seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts + seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts @@ -885,21 +885,31 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner } | _ -> raise NotApplicable -and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts = +and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts = match li with | ((Cic.AConst _) as he)::tl | ((Cic.AMutInd _) as he)::tl | ((Cic.AMutConstruct _) as he)::tl when - CoercDb.is_a_coercion' (Deannotate.deannotate_term he) && - !hide_coercions -> - let rec last = - function - [] -> assert false - | [t] -> t - | _::tl -> last tl + (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with + | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl) + && !hide_coercions -> + let cpos,sats = + match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with + | None -> assert false + | Some (_,_,_,sats,cpos) -> cpos, sats in - acic2content - seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl) + let x = List.nth tl cpos in + let _,rest = + try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] + in + if rest = [] then + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + x + else + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + (Cic.AAppl (id,x::rest)) | _ -> raise NotApplicable and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 4c98e1ad9..edb22c944 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -124,34 +124,25 @@ let ast_of_acic0 ~output_type term_info acic k = | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t -> - let last_n n l = - let rec aux = - function - [] -> assert false - | [_] as l -> l,1 - | he::tl -> - let (res,len) as res' = aux tl in - if len < n then - he::res,len + 1 - else - res' - in - match fst (aux l) with - [] -> assert false - | [t] -> t - | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> - idref aid (Ast.Appl (l@tl)) - | l -> idref aid (Ast.Appl l) - in (match LibraryObjects.destroy_nat t with | Some n -> idref aid (Ast.Num (string_of_int n, -1)) | None -> let deannot_he = Deannotate.deannotate_term he in - if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions - then - (match CoercDb.is_a_coercion_to_funclass deannot_he with - | None -> idref aid (last_n 1 (List.map k tl)) - | Some i -> idref aid (last_n (i+1) (List.map k tl))) + let coercion_info = CoercDb.is_a_coercion deannot_he in + if coercion_info <> None && !Acic2content.hide_coercions then + match coercion_info with + | None -> assert false + | Some (_,_,_,sats,cpos) -> + if cpos < List.length tl then + let _,rest = + try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] + in + if rest = [] then + idref aid (List.nth (List.map k tl) cpos) + else + idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest))) + else + idref aid (Ast.Appl (List.map k tl)) else idref aid (Ast.Appl (List.map k args))) | Cic.AAppl (aid,args) -> diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 87b3f7f42..8fa6963aa 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -132,25 +132,27 @@ let exp_impl metasenv subst context = ;; let is_a_double_coercion t = - let last_of l = - let rec aux acc = function - | x::[] -> acc,x - | x::tl -> aux (acc@[x]) tl - | [] -> assert false - in - aux [] l + let rec subst_nth n x l = + match n,l with + | _, [] -> [] + | 0, _::tl -> x :: tl + | n, hd::tl -> hd :: subst_nth (n-1) x tl in let imp = Cic.Implicit None in let dummyres = false,imp, imp,imp,imp in match t with - | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> - (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> - let sib2,head = last_of tl2 in - true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl - (c2::sib2@[imp])]) + | Cic.Appl l1 -> + (match CoercGraph.coerced_arg l1 with + | Some (Cic.Appl l2, pos1) -> + (match CoercGraph.coerced_arg l2 with + | Some (x, pos2) -> + true, List.hd l1, List.hd l2, x, + Cic.Appl (subst_nth (pos1 + 1) + (Cic.Appl (subst_nth (pos2+1) imp l2)) l1) + | _ -> dummyres) | _ -> dummyres) | _ -> dummyres +;; let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn = @@ -1242,12 +1244,11 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci (* given he:hety, gives beack all (c he) such that (c e):?->? *) let fix_arity n metasenv context subst he hetype ugraph = let hetype = CicMetaSubst.apply_subst subst hetype in - let src = CoercDb.coerc_carr_of_term hetype in - let tgt = CoercDb.Fun 0 in + let src = CoercDb.coerc_carr_of_term hetype 0 in + let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in match CoercGraph.look_for_coercion' metasenv subst context src tgt with | CoercGraph.NoCoercion -> [] - | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> + | CoercGraph.NotHandled -> raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> @@ -1366,11 +1367,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci CoercGraph.look_for_coercion metasenv subst context infty expty in match coer with - | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy - "coerce_atom_to_something fails since not meta closed")) | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy + "coerce_atom_to_something fails since no coercions found")) + | CoercGraph.NotHandled when + not (CicUtil.is_meta_closed infty) || + not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy + "coerce_atom_to_something fails since carriers have metas")) + | CoercGraph.NotHandled -> raise (RefineFailure (lazy "coerce_atom_to_something fails since no coercions found")) | CoercGraph.SomeCoercion candidates -> debug_print (lazy (string_of_int (List.length candidates) ^ diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 517c013d4..2bcb09937 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -594,51 +594,85 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | UnificationFailure s | Uncertain s as exn -> (match l1, l2 with - | (((Cic.Const (uri1, ens1)) as c1) :: tl1), - (((Cic.Const (uri2, ens2)) as c2) :: tl2) when - CoercDb.is_a_coercion' c1 && - CoercDb.is_a_coercion' c2 && + | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), + (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when + CoercDb.is_a_coercion cc1 <> None && + CoercDb.is_a_coercion cc2 <> None && not (UriManager.eq uri1 uri2) -> -(*DEBUGGING ONLY: +(*DEBUGGING ONLY: prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); let res = -*) - let rec look_for_first_coercion c tl = - match - CicMetaSubst.apply_subst subst (HExtlib.list_last tl) - with - Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl') - when CoercDb.is_a_coercion' c' -> - look_for_first_coercion c' tl' - | last_tl -> c,last_tl + *) + let inner_coerced t = + let t = CicMetaSubst.apply_subst subst t in + let rec aux c x t = + match t with + | Cic.Appl l -> + (match CoercGraph.coerced_arg l with + | None -> c, x + | Some (t,_) -> aux (List.hd l) t t) + | _ -> c, x + in + aux (Cic.Implicit None) (Cic.Implicit None) t in - let c1,last_tl1 = look_for_first_coercion c1 tl1 in - let c2,last_tl2 = look_for_first_coercion c2 tl2 in - let car1 = - CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in - let car2 = - CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in + let c1,last_tl1 = inner_coerced (Cic.Appl l1) in + let c2,last_tl2 = inner_coerced (Cic.Appl l2) in + let car1, car2 = + match + CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 + with + | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 + | _ -> assert false + in + let head1_c, head2_c = + match + CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 + with + | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 + | _ -> assert false + in + let unfold uri ens args = + let o, _ = + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + in + assert (ens = []); + match o with + | Cic.Constant (_,Some bo,_,_,_) -> + CicReduction.head_beta_reduce ~delta:false + (Cic.Appl (bo::args)) + | _ -> assert false + in if CoercDb.eq_carr car1 car2 then - (match last_tl1,last_tl2 with - C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn - | C.Meta _, _ - | _, C.Meta _ -> + match last_tl1,last_tl2 with + | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn + | _, C.Meta _ + | C.Meta _, _ -> let subst,metasenv,ugraph = fo_unif_subst test_equality_only subst context metasenv last_tl1 last_tl2 ugraph in fo_unif_subst test_equality_only subst context - metasenv (C.Appl l1) (C.Appl l2) ugraph - | _ -> raise exn) + metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph + | _ when CoercDb.eq_carr head1_c head2_c -> + let l1, l2 = + (* composite VS composition + metas avoiding + * coercions not only in coerced position *) + if c1 = cc1 then + unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) + else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 + in + fo_unif_subst test_equality_only subst context + metasenv l1 l2 ugraph + | _ -> raise exn else let meets = CoercGraph.meets metasenv subst context car1 car2 in - (match meets with + (match meets with | [] -> raise exn | (carr,metasenv,to1,to2)::xxx -> (match xxx with - [] -> () + | [] -> () | (m2,_,c2,c2')::_ -> let m1,_,c1,c1' = carr,metasenv,to1,to2 in let unopt = @@ -647,10 +681,10 @@ let res = in HLog.warn ("There are two minimal joins of "^ - CoercDb.name_of_carr car1^" and "^ - CoercDb.name_of_carr car2^": " ^ - CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^ - unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^ + CoercDb.string_of_carr car1^" and "^ + CoercDb.string_of_carr car2^": " ^ + CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^ + unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^ unopt c2^" + "^unopt c2')); let last_tl1',(subst,metasenv,ugraph) = match last_tl1,to1 with @@ -683,6 +717,7 @@ let subst,metasenv,ugraph = res in prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); res *) + (*CSC: This is necessary because of the "elim H" tactic where the type of H is only reducible to an inductive type. This could be extended from inductive diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index ac7441a4c..637944e6b 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -34,22 +34,26 @@ type coercion_search_result = | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion - | NotMetaClosed - | NotHandled of string Lazy.t + | NotHandled let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () let saturate_coercion ul metasenv subst context = let cl = - List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in - let funclass_arityl = - let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in - List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl + List.map + (fun u,saturations -> + let t = CicUtil.term_of_uri u in + let arity = + match CoercDb.is_a_coercion t with + | Some (_,CoercDb.Fun i,_,_,_) -> i + | _ -> 0 + in + arity,t,saturations) ul in let freshmeta = CicMkImplicit.new_meta metasenv subst in - List.map2 - (fun arity (c,saturations) -> + List.map + (fun (arity,c,saturations) -> let ty,_ = CicTypeChecker.type_of_aux' ~subst metasenv context c CicUniv.oblivion_ugraph in @@ -62,27 +66,29 @@ let saturate_coercion ul metasenv subst context = match args with [] -> c | _ -> Cic.Appl (c::args) - ) funclass_arityl cl + ) cl ;; (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion' metasenv subst context src tgt = + let is_dead = function CoercDb.Dead -> true | _ -> false in let pp_l s l = match l with | [] -> debug_print (lazy (sprintf ":-( coercion non trovata[%s] da %s a %s" s - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); + (CoercDb.string_of_carr src) + (CoercDb.string_of_carr tgt))); | _::_ -> debug_print (lazy ( sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); + (CoercDb.string_of_carr src) + (CoercDb.string_of_carr tgt))); in - try + if is_dead src || is_dead tgt then NotHandled + else let l = CoercDb.find_coercion (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) @@ -97,23 +103,23 @@ let look_for_coercion' metasenv subst context src tgt = pp_l "approx" l; (match l with | [] -> NoCoercion - | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) + | ul -> + SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) | ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) - with - | CoercDb.EqCarrNotImplemented s -> NotHandled s - | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed ;; let look_for_coercion metasenv subst context src tgt = - let src_uri = CoercDb.coerc_carr_of_term src in - let tgt_uri = CoercDb.coerc_carr_of_term tgt in + let src_uri = CoercDb.coerc_carr_of_term src 0 in + let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in look_for_coercion' metasenv subst context src_uri tgt_uri let source_of t = - try - let uri = CicUtil.uri_of_term t in - CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) - with Invalid_argument _ -> assert false (* t must be a coercion *) + match CoercDb.is_a_coercion t with + | None -> assert false + | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s + | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u + | Some _ -> assert false (* t must be a coercion not to funclass *) +;; let generate_dot_file () = let module Pp = GraphvizPp.Dot in @@ -123,19 +129,20 @@ let generate_dot_file () = ~edge_attrs:["fontsize", "10"] fmt; let l = CoercDb.to_list () in let pp_description carr = - match CoercDb.uri_of_carr carr with - | None -> () - | Some uri -> - Pp.node (CoercDb.name_of_carr carr) - ~attrs:["href", UriManager.string_of_uri uri] fmt in + match carr with + | CoercDb.Uri uri -> + Pp.node (CoercDb.string_of_carr carr) + ~attrs:["href", UriManager.string_of_uri uri] fmt + | _ -> () + in List.iter (fun (src, tgt, ul) -> - let src_name = CoercDb.name_of_carr src in - let tgt_name = CoercDb.name_of_carr tgt in + let src_name = CoercDb.string_of_carr src in + let tgt_name = CoercDb.string_of_carr tgt in pp_description src; pp_description tgt; List.iter - (fun (u,saturations) -> + (fun (u,saturations,_) -> Pp.edge src_name tgt_name ~attrs:[ "label", (UriManager.name_of_uri u ^ @@ -167,26 +174,12 @@ let is_composite t = let coerced_arg l = match l with - | [] | [_] -> assert false - | c::_ when not (CoercDb.is_a_coercion' c) -> assert false + | [] | [_] -> None | c::tl -> - let arity = - match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a - in - (* decide a decent structure for coercion carriers so that all this stuff is - * useless *) - let pi = - (* this calculation is not complete, since we have strange carriers *) - let rec count_pi = function - | Cic.Prod(_,_,t) -> 1+ (count_pi t) - | _ -> 0 - in - let uri = CicUtil.uri_of_term c in - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - | Cic.Constant (_, _, ty, _, _) -> count_pi ty - | _ -> assert false - in - try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None + match CoercDb.is_a_coercion c with + | None -> None + | Some (_,_,_,_,cpos) -> + if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None ;; (************************* meet calculation stuff ********************) @@ -207,7 +200,7 @@ let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;; let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;; -let splat e l = List.map (fun x -> e, Some x) l;; +let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;; (* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_to carr = diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index 711a1527d..1a3be89f3 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -34,8 +34,7 @@ type coercion_search_result = | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion - | NotMetaClosed - | NotHandled of string Lazy.t + | NotHandled val look_for_coercion : Cic.metasenv -> Cic.substitution -> Cic.context -> @@ -54,7 +53,7 @@ val source_of: Cic.term -> Cic.term val generate_dot_file: unit -> string (* given the Appl contents returns the argument of the head coercion *) -val coerced_arg: Cic.term list -> Cic.term option +val coerced_arg: Cic.term list -> (Cic.term * int) option (* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *) val meets : diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 43906f8cd..679f4246f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -455,7 +455,7 @@ type 'a eval_executable = type 'a eval_from_moo = { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } -let coercion_moo_statement_of (uri,arity, saturations) = +let coercion_moo_statement_of (uri,arity, saturations,_) = GrafiteAst.Coercion (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) @@ -493,11 +493,11 @@ let eval_coercion status ~add_composites uri arity saturations = saturations (GrafiteTypes.get_baseuri status) in let moo_content = - List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds) + List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds) in let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - List.map (fun u,_,_ -> u) compounds + List.map (fun u,_,_,_ -> u) compounds module MatitaStatus = struct @@ -608,9 +608,9 @@ let add_coercions_of_record_to_moo obj lemmas status = in let is_a_coercion, arity_coercion = is_a_coercion uri in if is_a_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_coercion,0)) + Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0)) else if is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_wanted,0)) + Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0)) else None) lemmas) diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli index f66c0e853..aa2749979 100644 --- a/helm/software/components/grafite_engine/grafiteSync.mli +++ b/helm/software/components/grafite_engine/grafiteSync.mli @@ -33,8 +33,8 @@ val add_coercion: add_composites:bool -> GrafiteTypes.status -> UriManager.uri -> int -> int -> string (* baseuri *) -> - GrafiteTypes.status * (UriManager.uri * int * int) list - (* URI, arity, saturations *) + GrafiteTypes.status * (UriManager.uri * int * int * int) list + (* URI, arity, saturations, cpos *) val time_travel: present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml index 638c0ce64..b45599ceb 100644 --- a/helm/software/components/library/cicCoercion.ml +++ b/helm/software/components/library/cicCoercion.ml @@ -29,7 +29,8 @@ let close_coercion_graph_ref = ref (fun _ _ _ _ _ -> [] : CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * + int * int) list) ;; let set_close_coercion_graph f = close_coercion_graph_ref := f;; diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli index 97463b1d6..8356de8cd 100644 --- a/helm/software/components/library/cicCoercion.mli +++ b/helm/software/components/library/cicCoercion.mli @@ -29,12 +29,12 @@ val set_close_coercion_graph : (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *)) list) + int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list) -> unit val close_coercion_graph: CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *) ) list + int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index 80222ad34..50db7a3c1 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -25,48 +25,47 @@ (* $Id$ *) +let debug = false +let debug_print = + if debug then fun x -> prerr_endline (Lazy.force x) + else ignore +;; + type coerc_carr = | Uri of UriManager.uri | Sort of Cic.sort - | Term of Cic.term | Fun of int + | Dead ;; -exception EqCarrNotImplemented of string Lazy.t -exception EqCarrOnNonMetaClosed +type saturations = int +type coerced_pos = int +type coercion_entry = + coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos + +type coerc_db = (* coercion_entry grouped by carrier with molteplicity *) + (coerc_carr * coerc_carr * + (UriManager.uri * int * saturations * coerced_pos) list) list -let db = ref [] +let db = ref ([] : coerc_db) +let dump () = !db +let restore coerc_db = db := coerc_db -let coerc_carr_of_term t = +let rec coerc_carr_of_term t a = try - match t with - | Cic.Sort s -> Sort s - | Cic.Prod _ -> Fun 0 - (* BUG: this should be the real arity. The computation - requires menv, context etc.., but since carrs are compared discharging Fun - arity... it works *) - | Cic.Appl (t::_) - | t -> Uri (CicUtil.uri_of_term t) - with Invalid_argument _ -> - Term t + match t, a with + | Cic.Sort s, 0 -> Sort s + | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a + | t, 0 -> Uri (CicUtil.uri_of_term t) + | _, n -> Fun n + with Invalid_argument _ -> Dead ;; -let uri_of_carr = function - | Uri u -> Some u - | _ -> None - -let rec name_of_carr = function +let string_of_carr = function | Uri u -> UriManager.name_of_uri u | Sort s -> CicPp.ppsort s - | Term (Cic.Appl ((Cic.Const (uri, _))::_)) - | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) - | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> - UriManager.name_of_uri uri - | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t) - | Term t -> - prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); - "FixTheNameMangler" | Fun i -> "FunClass_" ^ string_of_int i + | Dead -> "UnsupportedCarrier" ;; let eq_carr ?(exact=false) src tgt = @@ -81,24 +80,13 @@ let eq_carr ?(exact=false) src tgt = | _ -> coarse_eq) | Sort (Cic.Type _), Sort (Cic.Type _) -> true | Sort src, Sort tgt when src = tgt -> true - | Term t1, Term t2 -> - if t1 = t2 then true - else - if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then - raise - (EqCarrNotImplemented - (lazy ("Unsupported carr for coercions: " ^ - CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) - else raise EqCarrOnNonMetaClosed - | Fun _,Fun _ -> true (* only one Funclass? *) -(* | Fun i,Fun j when i=j -> true *) - | Term t, _ - | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed + | Fun _,Fun _ when not exact -> true (* only one Funclass *) + | Fun i,Fun j when i = j -> true (* only one Funclass *) | _, _ -> false ;; let to_list () = - List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db ;; let rec myfilter p = function @@ -106,14 +94,11 @@ let rec myfilter p = function | (s,t,l)::tl -> let l = HExtlib.filter_map - (fun (u,n,saturations) -> - if p (s,t,u,saturations) then - if n = 1 then - None - else - Some (u,n-1,saturations) - else - Some (u,n,saturations)) + (fun (u,n,saturations,cpos) as e -> + if p (s,t,u,saturations,cpos) then + if n = 1 then None + else Some (u,n-1,saturations,cpos) + else Some e) l in if l = [] then myfilter p tl else (s,t,l)::myfilter p tl @@ -122,75 +107,54 @@ let rec myfilter p = function let remove_coercion p = db := myfilter p !db;; let find_coercion f = - List.map - (fun uri,_,saturations -> uri,saturations) - (List.flatten + List.map + (fun (uri,_,saturations,_) -> uri,saturations) + (List.flatten (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) ;; -let get_carr uri = +let is_a_coercion t = try - let src, tgt, _ = - List.find - (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl) - !db - in - src, tgt - with Not_found -> assert false (* uri must be a coercion *) + let uri = CicUtil.uri_of_term t in + match + HExtlib.filter_map + (fun (src,tgt,xl) -> + let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in + if xl = [] then None else Some (src,tgt,xl)) + !db + with + | [] -> None + | (_,_,[])::_ -> assert false + | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p) + | (src,tgt,(u,_,s,p)::_)::_ -> + debug_print + (lazy "coercion has multiple entries, returning the first one"); + Some (src,tgt,u,s,p) + with Invalid_argument _ -> + debug_print (lazy "this term is not a constant"); + None ;; -let is_a_coercion u = - List.exists - (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl) - !db -;; - -let is_a_coercion' t = - try - let uri = CicUtil.uri_of_term t in - is_a_coercion uri - with Invalid_argument _ -> false -;; - -let is_a_coercion_to_funclass t = - try - let uri = CicUtil.uri_of_term t in - match snd (get_carr uri) with - | Fun i -> Some i - | _ -> None - with Invalid_argument _ -> None - - -let term_of_carr = function - | Uri u -> CicUtil.term_of_uri u - | Sort s -> Cic.Sort s - | Fun _ -> assert false - | Term _ -> assert false -;; - -let add_coercion (src,tgt,u,saturations) = +let add_coercion (src,tgt,u,saturations,cpos) = let f s t = eq_carr s src && eq_carr t tgt in let where = List.filter (fun (s,t,_) -> f s t) !db in let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in match where with - | [] -> db := (src,tgt,[u,1,saturations]) :: !db + | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db | (src,tgt,l)::tl -> assert (tl = []); (* not sure, this may be a feature *) - if List.exists (fun (x,_,_) -> UriManager.eq u x) l then - let l' = List.map - (fun (x,n,saturations') -> + if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then + let l = List.map + (fun (x,n,x_saturations,x_cpos) as e -> if UriManager.eq u x then - (x,n+1,saturations) - else - (x,n,saturations)) + (* not sure, this may be a feature *) + (assert (x_saturations = saturations && x_cpos = cpos); + (x,n+1,saturations,cpos)) + else e) l in - db := (src,tgt,l')::tl @ rest + db := (src,tgt,l)::tl @ rest else - db := (src,tgt,(u,1,saturations)::l)::tl @ rest - + db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest ;; -type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list -let dump () = !db -let restore coerc_db = db := coerc_db diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 3071aecc4..130987df8 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -24,49 +24,41 @@ *) - (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync - * - * and may be merged with CicCoercion... - * - * **) - - - (** XXX WARNING: non-reentrant *) -type coerc_carr = +type coerc_carr = private | Uri of UriManager.uri (* const, mutind, mutconstr *) | Sort of Cic.sort (* Prop, Set, Type *) - | Term of Cic.term (* nothing supported *) | Fun of int + | Dead ;; -exception EqCarrNotImplemented of string Lazy.t -exception EqCarrOnNonMetaClosed val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool -val coerc_carr_of_term: Cic.term -> coerc_carr -val name_of_carr: coerc_carr -> string -val uri_of_carr: coerc_carr -> UriManager.uri option +val string_of_carr: coerc_carr -> string + +(* takes a term in whnf ~delta:false and a desired ariety *) +val coerc_carr_of_term: Cic.term -> int -> coerc_carr val to_list: unit -> - (coerc_carr * coerc_carr * (UriManager.uri * int) list) list + (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list type coerc_db val dump: unit -> coerc_db val restore: coerc_db -> unit -val add_coercion: - coerc_carr * coerc_carr * UriManager.uri * int -> unit +(* src carr, tgt carr, uri, saturations, coerced position + * invariant: + * if the constant pointed by uri has n argments + * n = coerced position + saturations + FunClass arity + *) -val remove_coercion: - (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit +type saturations = int +type coerced_pos = int +type coercion_entry = + coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos +val add_coercion: coercion_entry -> unit +val remove_coercion: (coercion_entry -> bool) -> unit val find_coercion: (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list -val is_a_coercion: UriManager.uri -> bool -val is_a_coercion': Cic.term -> bool -val is_a_coercion_to_funclass: Cic.term -> int option -val get_carr: UriManager.uri -> coerc_carr * coerc_carr - -val term_of_carr: coerc_carr -> Cic.term - +val is_a_coercion: Cic.term -> coercion_entry option diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 4b85d61bc..13596c84e 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -138,12 +138,9 @@ let index_obj = let add_single_obj uri obj refinement_toolkit = let module RT = RefinementTool in let obj = - if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) - not (CoercDb.is_a_coercion' (Cic.Const (uri, []))) - then - refinement_toolkit.RT.pack_coercion_obj obj - else - obj + if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None + then refinement_toolkit.RT.pack_coercion_obj obj + else obj in let dbd = LibraryDb.instance () in if CicEnvironment.in_library uri then @@ -244,7 +241,7 @@ let generate_elimination_principles uri refinement_toolkit = let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; - CoercDb.remove_coercion (fun (_,_,_,_) -> true) + CoercDb.remove_coercion (fun _ -> true) let stack = ref [];; @@ -294,7 +291,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations in aux ty in - let src_carr, tgt_carr = + let src_carr, tgt_carr, no_args = let get_classes arity saturations l = (* this is the ackerman's function revisited *) let rec aux = function @@ -312,18 +309,19 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations in let types = spine2list coer_ty in let src,tgt = get_classes arity saturations types in - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - match tgt with - None -> assert false - | Some `Funclass -> CoercDb.Fun arity - | Some (`Class tgt) -> - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0, + (match tgt with + | None -> assert false + | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity + | Some (`Class tgt) -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0), + List.length types - 1 in let already_in_obj src_carr tgt_carr uri obj = List.exists (fun (s,t,ul) -> List.exists - (fun u,_ -> + (fun u,_,_ -> let bo = match obj with | Cic.Constant (_, Some bo, _, _, _) -> bo @@ -343,8 +341,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations ul) (CoercDb.to_list ()) in + let cpos = no_args - arity - saturations - 1 in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); []) else @@ -353,22 +352,24 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations baseuri in let new_coercions = - List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj)) + List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj)) new_coercions in - let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in + let composite_uris = + List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions + in (* update the DB *) List.iter - (fun (src,tgt,uri,saturations,_,_) -> - CoercDb.add_coercion (src,tgt,uri,saturations)) + (fun (src,tgt,uri,saturations,_,_,cpos) -> + CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) new_coercions; - CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); (* add the composites obj and they eventual lemmas *) let lemmas = List.fold_left - (fun acc (_,tgt,uri,saturations,obj,arity) -> + (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> add_single_obj uri obj refinement_toolkit; - (uri,arity,saturations)::acc) + (uri,arity,saturations,cpos)::acc) [] new_coercions in (* store that composite_uris are related to uri. the first component is @@ -399,10 +400,11 @@ let remove_coercion uri = composites_in_db;*) UriManager.UriHashtbl.remove coercion_hashtbl uri; CoercDb.remove_coercion - (fun (_,_,u,_) -> UriManager.eq uri u); + (fun (_,_,u,_,_) -> UriManager.eq uri u); (* remove from the DB *) List.iter - (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1)) + (fun u -> + CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1)) composites_in_db; (* remove composites from the lib *) List.iter remove_single_obj composites_in_lib @@ -442,7 +444,7 @@ let generate_projections refinement_toolkit uri fields = prerr_endline "---"; *) (*CSC: I throw the arity away. See comment above *) - List.map (fun u,_,_ -> u) x + List.map (fun u,_,_,_ -> u) x end else [] diff --git a/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli index 9dd3f5c3c..13a6479bd 100644 --- a/helm/software/components/library/librarySync.mli +++ b/helm/software/components/library/librarySync.mli @@ -51,7 +51,7 @@ val add_coercion: add_composites:bool -> RefinementTool.kit -> UriManager.uri -> int (* arity *) -> int (* saturations *) -> string (* baseuri *) -> - (UriManager.uri * int * int) list (* URI, arity, saturations *) + (UriManager.uri * int * int * int) list (* URI, arity, saturations, cpos *) (* inverse of add_coercion, removes both the eventually created composite *) (* coercions and the information that [uri] and the composites are coercion *) diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index e9a123ad8..0041685ef 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -33,39 +33,32 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else () * (source, list of coercions to follow, target) *) let get_closure_coercions src tgt uri coercions = - let enrich (uri,sat) tgt = + let enrich (uri,sat,_) tgt = let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in uri,sat,arity 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 - let rc = CoercDb.eq_carr ?exact s t in - debug_print(lazy(string_of_bool rc)); - rc - with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> - debug_print (lazy("false")); - false + debug_print(lazy(CoercDb.string_of_carr s^" VS "^CoercDb.string_of_carr t)); + let rc = CoercDb.eq_carr ?exact s t in + debug_print(lazy(string_of_bool rc)); + rc in match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> - debug_print (lazy ("Uri, Uri4")); + debug_print (lazy ("Uri, Uri4")); let c_from_tgt = List.filter (fun (f,t,_) -> - - debug_print (lazy ("Uri, Uri3")); - eq_carr f tgt (*&& not (eq_carr t src)*)) + debug_print (lazy ("Uri, Uri3")); + eq_carr f tgt) coercions in let c_to_src = List.filter (fun (f,t,_) -> - - debug_print (lazy ("Uri, Uri2")); - eq_carr t src (*&& not (eq_carr f tgt)*)) + debug_print (lazy ("Uri, Uri2")); + eq_carr t src) coercions in (HExtlib.flatten_map @@ -249,9 +242,9 @@ 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 - let saturations_res = + let saturations_res, position_of_meta_to_be_coerced = match meta_to_be_coerced with - | None -> 0 + | None -> 0,0 | Some meta_to_be_coerced -> debug_print (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced)); @@ -259,10 +252,11 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= 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 + List.length sorted - position_of_meta_to_be_coerced - 1, + position_of_meta_to_be_coerced in debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res)); - sorted, saturations_res + sorted, saturations_res, position_of_meta_to_be_coerced in let namer l n = let l = List.map (function Cic.Name s -> s | _ -> "A") l in @@ -287,7 +281,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); let old_insert_coercions = !CicRefine.insert_coercions in - let c, metasenv, univ, saturationsres = + let c, metasenv, univ, saturationsres, cpos = try CicRefine.insert_coercions := false; let term, ty, metasenv, ugraph = @@ -303,7 +297,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= in debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv)); - let body_metasenv, saturationsres = + let body_metasenv, saturationsres, cpos = order_body_menv term body_metasenv c1_pis c2_pis in debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); @@ -340,7 +334,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); debug_print (lazy ("####################")); CicRefine.insert_coercions := old_insert_coercions; - term, metasenv, ugraph, saturationsres + term, metasenv, ugraph, saturationsres, cpos with | CicRefine.RefineFailure s | CicRefine.Uncertain s -> debug_print s; @@ -350,7 +344,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= CicRefine.insert_coercions := old_insert_coercions; raise exn in - c, metasenv, univ, saturationsres, arity2 + c, metasenv, univ, saturationsres, arity2, cpos ;; let build_obj c univ arity = @@ -372,16 +366,18 @@ let build_obj c univ arity = (* 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" -> debug_print (lazy("XXX")); false) - coercions)) + 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" -> + debug_print (lazy("XXX")); false) + coercions)) l +;; let mangle s t l = (*List.fold_left @@ -429,7 +425,7 @@ let number_if_already_defined buri name l = 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 + let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in debug_print (lazy("composed " ^ string_of_int (List.length todo_list))); let todo_list = filter_duplicates todo_list coercions in try @@ -437,47 +433,46 @@ let close_coercion_graph src tgt uri saturations baseuri = List.fold_left (fun acc (src, l , tgt) -> try - (match l with + match l with | [] -> assert false | (he,saturations1,arity1) :: tl -> let first_step = - Cic.Constant ("", - Some (CoercDb.term_of_carr (CoercDb.Uri he)), + Cic.Constant ("", Some (CicUtil.term_of_uri he), Cic.Sort Cic.Prop, [], obj_attrs arity1), saturations1, - arity1 + arity1,0 in let o,_ = List.fold_left (fun (o,univ) (coer,saturations2,arity2) -> match o with - | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 -> - let t, menv, univ, saturationsres, arityres = + | Cic.Constant (_,Some u,_,[],_),saturations1,arity1,_ -> + let t, menv, univ, saturationsres, arityres, cposres = generate_composite' (u,saturations1,arity1) - (CoercDb.term_of_carr (CoercDb.Uri coer), + (CicUtil.term_of_uri coer, saturations2, arity2) [] [] univ in if (menv = []) then HLog.warn "MENV non empty after composing coercions"; let o,univ = build_obj t univ arityres in - (o,saturationsres,arityres),univ + (o,saturationsres,arityres,cposres),univ | _ -> assert false ) (first_step, CicUniv.oblivion_ugraph) tl in - let name_src = CoercDb.name_of_carr src in - let name_tgt = CoercDb.name_of_carr tgt in + let name_src = CoercDb.string_of_carr src in + let name_tgt = CoercDb.string_of_carr tgt in let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) 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) + (List.map (fun (_,_,u,_,_,_,_) -> u) acc) in - let named_obj,saturations,arity = + let named_obj,saturations,arity,cpos = match o with - | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity -> - Cic.Constant (name,bo,ty,vl,attrs),saturations,arity + | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity,cpos -> + Cic.Constant (name,bo,ty,vl,attrs),saturations,arity,cpos | _ -> assert false in - (src,tgt,c_uri,saturations,named_obj,arity))::acc + (src,tgt,c_uri,saturations,named_obj,arity,cpos)::acc with UnableToCompose -> acc ) [] todo_list in @@ -490,7 +485,7 @@ 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 sat1 sat2 = - let a,b,c,_,_ = + let a,b,c,_,_,_ = generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ in a,b,c diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli index 0d5a2e5be..70c4eff9a 100644 --- a/helm/software/components/tactics/closeCoercionGraph.mli +++ b/helm/software/components/tactics/closeCoercionGraph.mli @@ -29,7 +29,7 @@ val close_coercion_graph: CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *)) list + int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list exception UnableToCompose diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index f7c3932dc..8fb710755 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -73,7 +73,7 @@ let rec collapse_head_metas t = let rec dummies_of_coercions = function - | Cic.Appl (c::l) when CoercDb.is_a_coercion' c -> + | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None -> Cic.Meta (-1,[]) | Cic.Appl l -> let l' = List.map dummies_of_coercions l in Cic.Appl l' diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma index 3aec1a024..1125e2a91 100644 --- a/helm/software/matita/contribs/dama/dama/models/list_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma @@ -41,10 +41,24 @@ lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n. intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; qed. -inductive sorted (T:Type) (lt : T → T → Prop): list T → Prop ≝ -| sorted_nil : sorted T lt [] -| sorted_one : ∀x. sorted T lt [x] -| sorted_cons : ∀x,y,tl. lt x y → sorted T lt (y::tl) → sorted T lt (x::y::tl). +record rel : Type ≝ { + rel_T :> Type; + rel_op :2> rel_T → rel_T → Prop +}. + +record trans_rel : Type ≝ { + o_rel :> rel; + o_tra : ∀x,y,z: o_rel.o_rel x y → o_rel y z → o_rel x z +}. + +lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z. +apply o_tra; +qed. + +inductive sorted (lt : trans_rel): list (rel_T lt) → Prop ≝ +| sorted_nil : sorted lt [] +| sorted_one : ∀x. sorted lt [x] +| sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl). lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def. intros; elim i; simplify; [reflexivity;] assumption; qed. @@ -61,25 +75,23 @@ lemma len_gt_non_empty : intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1; qed. -lemma sorted_tail: ∀T,r,x,l.sorted T r (x::l) → sorted T r l. +lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l. intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;] destruct H4; assumption; qed. -lemma sorted_skip: - ∀T,r,x,y,l. - transitive T r → sorted T r (x::y::l) → sorted T r (x::l). -intros; inversion H1; intros; [1,2: destruct H2] -destruct H5; inversion H3; intros; [destruct H5] -[1: destruct H5; constructor 2; -|2: destruct H8; constructor 3; [apply (H ??? H2 H5);] - apply (sorted_tail ???? H3);] +lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l). +intros (r x y l H1); inversion H1; intros; [1,2: destruct H] +destruct H4; inversion H2; intros; [destruct H4] +[1: destruct H4; constructor 2; +|2: destruct H7; constructor 3; [ apply (o_tra ? ??? H H4);] + apply (sorted_tail ??? H2);] qed. -lemma sorted_tail_bigger : ∀T,r,x,l,d.sorted T r (x::l) → ∀i. i < \len l → r x (\nth l d i). +lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i). intros 4; elim l; [ cases (not_le_Sn_O i H1);] cases i in H2; -[2: intros; apply (H d ? n);[apply (sorted_skip ????? H1)|apply le_S_S_to_le; apply H2] +[2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2] |1: intros; inversion H1; intros; [1,2: destruct H3] destruct H6; simplify; assumption;] qed. diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index cb73c2d5f..220601745 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -57,7 +57,7 @@ letin m ≝ (hide ? ( apply le_plus_n_r;] |2,3: clear H6; cases (aux n1) in H5 ⊢ %; intros; - change in match (a 〈w,H5〉) in H6 ⊢ % with (a w); + change in match (a ≪w,H5≫) in H6 ⊢ % with (a w); cases H5; clear H5; cases H7; clear H7; [1: left; split; [ apply (le_S ?? H5); | assumption] |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6); diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma index 8b062b6de..dd1f52b72 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma @@ -15,13 +15,12 @@ include "lebesgue.ma". include "models/nat_order_continuous.ma". -alias symbol "pair" = "dependent pair". theorem nat_lebesgue_oc: ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u]. ∀x:ℕ.a order_converges x → x ∈ [l,u] ∧ ∀h:x ∈ [l,u]. - uniform_converge {[l,u]} ⌊n,〈a n,H n〉⌋ 〈x,h〉. + uniform_converge {[l,u]} ⌊n,≪a n,H n≫⌋ ≪x,h≫. intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption; qed. diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index a48eb164a..a492c8f32 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -217,7 +217,7 @@ qed. definition order_converge ≝ λO:ordered_set.λa:sequence O.λx:O. exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x) - (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ + (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ (u i) is_supremum ⌊w,a (w+i)⌋). notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index c559358c5..b39eb8531 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -255,11 +255,11 @@ let _ = HLog.debug ((String.concat "," (List.map - (fun u,saturations -> + (fun u,saturations,_ -> UriManager.name_of_uri u ^ "(" ^ string_of_int saturations ^ ")") ul)) ^ ":" - ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) + ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t)) (CoercDb.to_list ())); addDebugSeparator (); let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 312a9a4f8..076a5d763 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -145,8 +145,6 @@ let rec to_string = None, "Type checking assertion failed: " ^ Lazy.force msg | LibrarySync.AlreadyDefined s -> None, "Already defined: " ^ UriManager.string_of_uri s - | CoercDb.EqCarrNotImplemented msg -> - None, ("EqCarrNotImplemented: " ^ Lazy.force msg) | DisambiguateChoices.Choice_not_found msg -> None, ("Disambiguation choice not found: " ^ Lazy.force msg) | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> -- 2.39.2