From 9393a9f9370014c904244358abe4ec6e11a9d158 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Feb 2006 13:04:35 +0000 Subject: [PATCH] added support for "polymorphic" coercions --- components/cic_unification/cicMetaSubst.ml | 3 +- components/cic_unification/cicRefine.ml | 258 ++++++++++++++++++--- components/cic_unification/cicRefine.mli | 3 + components/grafite_engine/grafiteEngine.ml | 34 ++- components/grafite_engine/grafiteSync.ml | 8 +- components/grafite_engine/grafiteSync.mli | 7 +- components/library/.depend | 7 +- components/library/Makefile | 1 + components/library/cicCoercion.ml | 171 ++++++++++---- components/library/cicCoercion.mli | 1 + components/library/coercDb.ml | 7 +- components/library/coercDb.mli | 7 +- components/library/coercGraph.ml | 17 ++ components/library/coercGraph.mli | 1 + components/library/librarySync.ml | 133 +++-------- components/library/librarySync.mli | 10 +- components/library/refinementTool.ml | 41 ++++ components/tactics/proofEngineTypes.ml | 13 +- matita/library/algebra/groups.ma | 30 +-- matita/library/algebra/monoids.ma | 2 +- matita/matita.ml | 11 + matita/matitaScript.ml | 6 +- matita/scripts/crontab.sh | 2 +- 23 files changed, 546 insertions(+), 227 deletions(-) create mode 100644 components/library/refinementTool.ml diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 5870089be..53efcf96e 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -1,4 +1,5 @@ (* Copyright (C) 2003, HELM Team. + * * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -230,7 +231,7 @@ let apply_subst_gen ~appl_fun subst term = in C.CoFix (i, fl') in - LibrarySync.merge_coercions (um_aux term) + um_aux term ;; let apply_subst = diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 620f66f18..b74d40296 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -58,7 +58,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = Cic.CicHash.find localization_tbl t with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); - assert false + raise exn' in raise (HExtlib.Localized (loc,exn')) @@ -81,19 +81,80 @@ let rec split l n = let exp_impl metasenv subst context = function | Some `Type -> - let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) + let (metasenv', idx) = + CicMkImplicit.mk_implicit_type metasenv subst context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) | Some `Closed -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in - metasenv', Cic.Meta (idx, []) + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) | None -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) | _ -> assert false ;; +let is_a_double_coercion t = + let last_of l = + let rec aux = function + | x::[] -> x + | x::tl -> aux tl + | [] -> assert false + in + aux l + in + let dummyres = + false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None + in + match t with + | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> + (match last_of tl with + | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + let head = last_of tl2 in + true, c1, c2, head + | _ -> dummyres) + | _ -> dummyres + +let avoid_double_coercion context subst metasenv ugraph t ty = + let arity_of con = + try + let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in + let rec count_pi = function + | Cic.Prod (_,_,t) -> 1 + count_pi t + | _ -> 0 + in + count_pi ty + with Invalid_argument _ -> assert false (* all coercions have an uri *) + in + let rec mk_implicits tail = function + | 0 -> [tail] + | n -> Cic.Implicit None :: mk_implicits tail (n-1) + in + let b, c1, c2, head = is_a_double_coercion t in + if b then + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CicMetaSubst.apply_subst subst ty in + (match CoercGraph.look_for_coercion source_carr tgt_carr + with + | CoercGraph.SomeCoercion c -> + let arity = arity_of c in + let args = mk_implicits head (arity - 1) in + let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in + let newt = Cic.Appl (c_bo::args) in + let subst, metasenv, ugraph = + CicUnification.fo_unif_subst subst context metasenv newt t ugraph + in + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args)))); + Cic.Appl (c::args), ty, subst, metasenv, ugraph + | _ -> assert false) (* the composite coercion must exist *) + else + t, ty, subst, metasenv, ugraph let rec type_of_constant uri ugraph = let module C = Cic in @@ -110,7 +171,8 @@ let rec type_of_constant uri ugraph = | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise - (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) + (RefineFailure + (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) and type_of_variable uri ugraph = let module C = Cic in @@ -345,7 +407,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion c -> let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion + avoid_double_coercion context subst metasenv ugraph (Cic.Appl[c;t]) coercion_tgt in @@ -389,7 +451,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match boh with | CoercGraph.SomeCoercion c -> let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion + avoid_double_coercion context subst' metasenv' ugraph1 (Cic.Appl[c;s']) coercion_tgt in @@ -452,7 +514,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 in - avoid_double_coercion + avoid_double_coercion context subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> @@ -851,19 +913,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t relocalize localization_tbl t t'; res - and avoid_double_coercion subst metasenv ugraph t ty = - match t with - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when - CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> - let source_carr = CoercGraph.source_of c2 in - let tgt_carr = CicMetaSubst.apply_subst subst ty in - (match CoercGraph.look_for_coercion source_carr tgt_carr - with - | CoercGraph.SomeCoercion c -> - Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph - | _ -> assert false) (* the composite coercion must exist *) - | _ -> t, ty, subst, metasenv, ugraph - (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) @@ -1059,7 +1108,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t try fo_unif_subst subst context metasenv hetype hetype' ugraph with exn -> - debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" + debug_print + (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" (CicPp.ppterm hetype) (CicPp.ppterm hetype') (CicMetaSubst.ppmetasenv [] metasenv) @@ -1113,7 +1163,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> let newt, _, subst, metasenv, ugraph = - avoid_double_coercion + avoid_double_coercion context subst metasenv ugraph (Cic.Appl[c;hete]) tgt_carr in try @@ -1365,6 +1415,158 @@ let typecheck metasenv uri obj ~localization_tbl = are_all_occurrences_positive metasenv ugraph uri tys paramsno in Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph +;; + +(* sara' piu' veloce che raffinare da zero? mah.... *) +let pack_coercion metasenv t = + let module C = Cic in + let rec merge_coercions ctx = + let aux = (fun (u,t) -> u,merge_coercions ctx t) in + function + | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t + | C.Meta (n,subst) -> + let subst' = + List.map + (function None -> None | Some t -> Some (merge_coercions ctx t)) subst + in + C.Meta (n,subst') + | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty) + | C.Prod (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.Lambda (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.LetIn (name,so,dest) -> + let ctx' = Some (name,(C.Def (so,None)))::ctx in + C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.Appl l as t -> + let b,_,_,_ = is_a_double_coercion t in + (* prerr_endline "CANDIDATO!!!!"; *) + let newt = + if b then + let ugraph = CicUniv.empty_ugraph in + let old_insert_coercions = !insert_coercions in + insert_coercions := false; + let newt, _, menv, _ = + try + type_of_aux' metasenv ctx t ugraph + with RefineFailure _ | Uncertain _ -> + prerr_endline (CicPp.ppterm t); + t, t, [], ugraph + in + insert_coercions := old_insert_coercions; + if metasenv <> [] || menv = [] then + newt + else + (prerr_endline "PUO' SUCCEDERE!!!!!";t) + else + t + in + (match newt with + | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l) + | _ -> assert false) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Var (uri, exp_named_subst) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Const (uri, exp_named_subst) + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutInd (uri,tyno,exp_named_subst) + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutConstruct (uri,tyno,consno,exp_named_subst) + | C.MutCase (uri,tyno,out,te,pl) -> + let pl = List.map (merge_coercions ctx) pl in + C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl) + | C.Fix (fno, fl) -> + let ctx = + List.fold_left + (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,idx,ty,bo) -> + (name,idx,merge_coercions ctx ty,merge_coercions ctx bo)) + fl + in + C.Fix (fno, fl) + | C.CoFix (fno, fl) -> + let ctx = + List.fold_left + (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,ty,bo) -> + (name, merge_coercions ctx ty, merge_coercions ctx bo)) + fl + in + C.CoFix (fno, fl) + in + merge_coercions [] t +;; + +let pack_coercion_obj obj = + let module C = Cic in + match obj with + | C.Constant (id, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] body) + in + let ty = pack_coercion [] ty in + C.Constant (id, body, ty, params, attrs) + | C.Variable (name, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] body) + in + let ty = pack_coercion [] ty in + C.Variable (name, body, ty, params, attrs) + | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> + let conjectures = + List.map + (fun (i, ctx, ty) -> + let ctx = + List.map + (function + | Some (name, C.Decl t) -> + Some (name, C.Decl (pack_coercion conjectures t)) + | Some (name, C.Def (t,None)) -> + Some (name, C.Def (pack_coercion conjectures t, None)) + | Some (name, C.Def (t,Some ty)) -> + Some (name, C.Def (pack_coercion conjectures t, + Some (pack_coercion conjectures ty))) + | None -> None) + ctx + in + ((i,ctx,pack_coercion conjectures ty))) + conjectures + in + let body = pack_coercion conjectures body in + let ty = pack_coercion conjectures ty in + C.CurrentProof (name, conjectures, body, ty, params, attrs) + | C.InductiveDefinition (indtys, params, leftno, attrs) -> + let indtys = + List.map + (fun (name, ind, arity, cl) -> + let arity = pack_coercion [] arity in + let cl = + List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl + in + (name, ind, arity, cl)) + indtys + in + C.InductiveDefinition (indtys, params, leftno, attrs) +;; + (* DEBUGGING ONLY let type_of_aux' metasenv context term = diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli index 224a7586c..c3ab49e0a 100644 --- a/components/cic_unification/cicRefine.mli +++ b/components/cic_unification/cicRefine.mli @@ -46,3 +46,6 @@ val typecheck : val insert_coercions: bool ref (* initially true *) +(* given a closed term returns it with all coercions packed *) +val pack_coercion_obj: Cic.obj -> Cic.obj + diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index c55bf8d9e..26fc540d8 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -392,11 +392,34 @@ type 'a eval_from_moo = let coercion_moo_statement_of uri = GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false) +let refinement_toolkit = { + RefinementTool.type_of_aux' = + (fun ?localization_tbl e c t u -> + let saved = !CicRefine.insert_coercions in + CicRefine.insert_coercions:= false; + let rc = + try + let t, ty, metasenv, ugraph = + CicRefine.type_of_aux' ?localization_tbl e c t u in + RefinementTool.Success (t, ty, metasenv, ugraph) + with + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s -> RefinementTool.Exception s + in + CicRefine.insert_coercions := saved; + rc); + RefinementTool.ppsubst = CicMetaSubst.ppsubst; + RefinementTool.apply_subst = CicMetaSubst.apply_subst; + RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; + RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; + } + let eval_coercion status ~add_composites uri = let basedir = Helm_registry.get "matita.basedir" in let status,compounds = prerr_endline "evaluating a coercion command"; - GrafiteSync.add_coercion ~basedir ~add_composites status uri in + GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in let moo_content = coercion_moo_statement_of uri in let status = GrafiteTypes.add_moo_content [moo_content] status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, @@ -505,10 +528,11 @@ let add_coercions_of_record_to_moo obj lemmas status = | _ -> None) fields in + (* prerr_endline "wanted coercions:"; List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - wanted_coercions; + wanted_coercions; *) let coercions, moo_content = List.split (HExtlib.filter_map @@ -521,10 +545,10 @@ let add_coercions_of_record_to_moo obj lemmas status = None) lemmas) in - prerr_endline "actual coercions:"; + (* prerr_endline "actual coercions:"; List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - coercions; + coercions; *) let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, @@ -532,7 +556,7 @@ let add_coercions_of_record_to_moo obj lemmas status = let add_obj uri obj status = let basedir = Helm_registry.get "matita.basedir" in - let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in + let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in status, lemmas let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index 37a3132e7..f23b42ecc 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -27,13 +27,13 @@ open Printf -let add_obj ~basedir uri obj status = - let lemmas = LibrarySync.add_obj uri obj basedir in +let add_obj refinement_toolkit ~basedir uri obj status = + let lemmas = LibrarySync.add_obj refinement_toolkit uri obj basedir in {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects}, lemmas -let add_coercion ~basedir ~add_composites status uri = - let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in +let add_coercion refinement_toolkit ~basedir ~add_composites status uri = + let compounds = LibrarySync.add_coercion ~add_composites ~basedir refinement_toolkit uri in {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions}, compounds diff --git a/components/grafite_engine/grafiteSync.mli b/components/grafite_engine/grafiteSync.mli index ce3c04250..f686eb2d8 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -24,12 +24,15 @@ *) val add_obj: + RefinementTool.kit -> basedir:string -> UriManager.uri -> Cic.obj -> GrafiteTypes.status -> GrafiteTypes.status * UriManager.uri list val add_coercion: - basedir:string -> add_composites:bool -> GrafiteTypes.status -> - UriManager.uri -> GrafiteTypes.status * UriManager.uri list + RefinementTool.kit -> + basedir:string -> add_composites:bool -> GrafiteTypes.status -> + UriManager.uri -> + GrafiteTypes.status * UriManager.uri list val time_travel: present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit diff --git a/components/library/.depend b/components/library/.depend index 5054959da..416a3ce3e 100644 --- a/components/library/.depend +++ b/components/library/.depend @@ -1,4 +1,5 @@ -cicCoercion.cmi: coercDb.cmi +cicCoercion.cmi: refinementTool.cmo coercDb.cmi +librarySync.cmi: refinementTool.cmo cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi cicRecord.cmo: cicRecord.cmi @@ -9,8 +10,8 @@ libraryDb.cmo: libraryDb.cmi libraryDb.cmx: libraryDb.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi -cicCoercion.cmo: coercDb.cmi cicCoercion.cmi -cicCoercion.cmx: coercDb.cmx cicCoercion.cmi +cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi +cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi coercGraph.cmo: coercDb.cmi coercGraph.cmi coercGraph.cmx: coercDb.cmx coercGraph.cmi librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \ diff --git a/components/library/Makefile b/components/library/Makefile index 4f0ca3eb8..69a10919d 100644 --- a/components/library/Makefile +++ b/components/library/Makefile @@ -14,6 +14,7 @@ INTERFACE_FILES = \ libraryClean.mli \ $(NULL) IMPLEMENTATION_FILES = \ + refinementTool.ml \ $(INTERFACE_FILES:%.mli=%.ml) include ../../Makefile.defs diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index fe636ee35..40def8238 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -60,35 +60,104 @@ let get_closure_coercions src tgt uri coercions = let obj_attrs = [`Class `Coercion; `Generated] +exception UnableToCompose + (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure c1 c2 univ = +let generate_composite_closure rt c1 c2 univ = + let module RT = RefinementTool in let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in - let rec mk_rels n = + let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in + let rec mk_implicits n = match n with | 0 -> [] - | _ -> (Cic.Rel n) :: (mk_rels (n-1)) + | _ -> (Cic.Implicit None) :: mk_implicits (n-1) in - let rec compose k = - function - | Cic.Prod (name,src,tgt) -> - let name = - match name with - | Cic.Anonymous -> Cic.Name "x" - | _ -> name - in - Cic.Lambda (name,src,compose (k+1) tgt) - | Cic.Appl (he::tl) -> - Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) - | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) + let rec mk_lambda_spline c = function + | 0 -> c + | n -> + Cic.Lambda + (Cic.Name ("A" ^ string_of_int (n-1)), + (Cic.Implicit None), + mk_lambda_spline c (n-1)) + in + let rec count_saturations_needed n = function + | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t + | _ -> n + 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 = + List.sort + (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2) + metasenv + 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 -> + CicSubstitution.subst (Cic.Rel ~-100) t + | Cic.Lambda (name, s, t) -> + Cic.Lambda (name, s, aux t) + | t -> t + in + aux t in - let c = compose 0 c1_ty 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 = count_saturations_needed 0 c1_ty in + let saturations_for_c2 = count_saturations_needed 0 c2_ty 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 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 subst = create_subst_from_metas_to_rels spline_len body_metasenv in + debug_print (lazy("SUBST: "^rt.RT.ppsubst 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 as exn -> + with CicTypeChecker.TypeCheckerFailure s -> debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" (CicPp.ppterm c) (Lazy.force s))); - raise exn + raise UnableToCompose in let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty @@ -110,45 +179,47 @@ let filter_duplicates l coercions = (* 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 = +let close_coercion_graph rt src tgt uri = (* 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 let new_coercions = - List.map ( + HExtlib.filter_map ( fun (src, l , tgt) -> - match l with - | [] -> assert false - | he :: tl -> - let first_step = - Cic.Constant ("", - Some (CoercDb.term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs) - in - let o,_ = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri - coer)) univ + try + (match l with + | [] -> assert false + | he :: tl -> + let first_step = + Cic.Constant ("", + Some (CoercDb.term_of_carr (CoercDb.Uri he)), + Cic.Sort Cic.Prop, [], obj_attrs) + 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 + | _ -> 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 name = name_tgt ^ "_of_" ^ name_src in + let buri = UriManager.buri_of_uri uri in + let c_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) | _ -> 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 name = name_tgt ^ "_of_" ^ name_src in - let buri = UriManager.buri_of_uri uri in - let c_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - 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)) + in + Some ((src,tgt,c_uri,named_obj))) + with UnableToCompose -> None ) todo_list in new_coercions diff --git a/components/library/cicCoercion.mli b/components/library/cicCoercion.mli index c9eaf0aac..7e4f03ab8 100644 --- a/components/library/cicCoercion.mli +++ b/components/library/cicCoercion.mli @@ -26,6 +26,7 @@ (* This module implements the Coercions transitive closure *) val close_coercion_graph: + RefinementTool.kit -> CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index 8e2c62f31..7203f3647 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -43,14 +43,17 @@ let coerc_carr_of_term t = | t -> Term t ;; -let name_of_carr = function +let rec name_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 t -> (* CicPp.ppterm t *) assert false + | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t) + | Term t -> + prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); + "FixTheNameMangler" let eq_carr src tgt = match src, tgt with diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index 9e8bf5e9c..1f5df8933 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -32,7 +32,11 @@ (** XXX WARNING: non-reentrant *) -type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term +type coerc_carr = + | Uri of UriManager.uri (* const, mutind, mutconstr *) + | Sort of Cic.sort (* Prop, Set, Type *) + | Term of Cic.term (* nothing supported *) + exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed val eq_carr: coerc_carr -> coerc_carr -> bool @@ -56,3 +60,4 @@ val is_a_coercion: UriManager.uri -> bool val get_carr: UriManager.uri -> coerc_carr * coerc_carr val term_of_carr: coerc_carr -> Cic.term + diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index cd958a8f6..62a89b0a7 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -94,4 +94,21 @@ let target_of t = CoercDb.term_of_carr (snd (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) +let generate_dot_file () = + let l = CoercDb.to_list () in + let preamble = " + digraph pippo { + node [fontsize=9, width=.4, height=.4]; + edge [fontsize=10]; + \n" + in + let conclusion = " } \n" in + let data = List.fold_left + (fun acc (src,tgt,c) -> + acc ^ CoercDb.name_of_carr src ^ " -> " ^ + CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ + "\"];\n") "" l + in + preamble ^ data ^ conclusion + (* EOF *) diff --git a/components/library/coercGraph.mli b/components/library/coercGraph.mli index 1923a964a..283d8a484 100644 --- a/components/library/coercGraph.mli +++ b/components/library/coercGraph.mli @@ -38,3 +38,4 @@ val is_a_coercion: Cic.term -> bool val source_of: Cic.term -> Cic.term val target_of: Cic.term -> Cic.term +val generate_dot_file: unit -> string diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 7363697d5..7209af691 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -37,87 +37,6 @@ let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 * *) let coercion_hashtbl = UriManager.UriHashtbl.create 3 -let rec merge_coercions = - let module C = Cic in - let aux = (fun (u,t) -> u,merge_coercions t) in - function - C.Rel _ | C.Sort _ | C.Implicit _ as t -> t - | C.Meta (n,subst) -> - let subst' = - List.map - (function None -> None | Some t -> Some (merge_coercions t)) subst - in - C.Meta (n,subst') - | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty) - | C.Prod (name,so,dest) -> - C.Prod (name, merge_coercions so, merge_coercions dest) - | C.Lambda (name,so,dest) -> - C.Lambda (name, merge_coercions so, merge_coercions dest) - | C.LetIn (name,so,dest) -> - C.LetIn (name, merge_coercions so, merge_coercions dest) - | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when - CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> - let source_carr = CoercGraph.source_of c2 in - let tgt_carr = CoercGraph.target_of c1 in - (match CoercGraph.look_for_coercion source_carr tgt_carr - with - | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ] - | _ -> assert false) (* the composite coercion must exist *) - | C.Appl l -> C.Appl (List.map merge_coercions l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Var (uri, exp_named_subst) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Const (uri, exp_named_subst) - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutInd (uri,tyno,exp_named_subst) - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutConstruct (uri,tyno,consno,exp_named_subst) - | C.MutCase (uri,tyno,out,te,pl) -> - let pl = List.map merge_coercions pl in - C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl) - | C.Fix (fno, fl) -> - let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in - C.Fix (fno, fl) - | C.CoFix (fno, fl) -> - let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in - C.CoFix (fno, fl) - -let merge_coercions_in_obj obj = - let module C = Cic in - match obj with - | C.Constant (id, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (merge_coercions body) - in - let ty = merge_coercions ty in - C.Constant (id, body, ty, params, attrs) - | C.Variable (name, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (merge_coercions body) - in - let ty = merge_coercions ty in - C.Variable (name, body, ty, params, attrs) - | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) -> - assert false - | C.InductiveDefinition (indtys, params, leftno, attrs) -> - let indtys = - List.map - (fun (name, ind, arity, cl) -> - let arity = merge_coercions arity in - let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in - (name, ind, arity, cl)) - indtys - in - C.InductiveDefinition (indtys, params, leftno, attrs) - let uris_of_obj uri = let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in @@ -185,12 +104,13 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_single_obj uri obj ~basedir = +let add_single_obj uri obj refinement_toolkit ~basedir = + let module RT = RefinementTool in let obj = if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) then - merge_coercions_in_obj obj + refinement_toolkit.RT.pack_coercion_obj obj else obj in @@ -253,12 +173,12 @@ let remove_single_obj uri = (*** GENERATION OF AUXILIARY LEMMAS ***) -let generate_elimination_principles ~basedir uri = +let generate_elimination_principles ~basedir uri refinement_toolkit = let uris = ref [] in let elim sort = try let uri,obj = CicElim.elim_of ~sort uri 0 in - add_single_obj uri obj ~basedir; + add_single_obj uri obj refinement_toolkit ~basedir; uris := uri :: !uris with CicElim.Can_t_eliminate -> () in @@ -275,7 +195,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~basedir ~add_composites uri = +let add_coercion ~basedir ~add_composites refinement_toolkit uri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -293,30 +213,30 @@ let add_coercion ~basedir ~add_composites uri = *) let extract_last_two_p ty = let rec aux = function - | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> - assert false - (* not implemented: aux (Cic.Prod(n,t1,t2)) *) + | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> + aux t | Cic.Prod( _, src, tgt) -> src, tgt | _ -> assert false in aux ty in let ty_src, ty_tgt = extract_last_two_p coer_ty in - let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in - let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in - let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in + let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in + let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in + let new_coercions = + CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in (* update the DB *) List.iter (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) new_coercions; - CoercDb.add_coercion (src_uri, tgt_uri, uri); + CoercDb.add_coercion (src_carr, tgt_carr, uri); (* add the composites obj and they eventual lemmas *) let lemmas = if add_composites then List.fold_left (fun acc (_,_,uri,obj) -> - add_single_obj ~basedir uri obj; + add_single_obj ~basedir uri obj refinement_toolkit; uri::acc) composite_uris new_coercions else @@ -324,9 +244,12 @@ let add_coercion ~basedir ~add_composites uri = 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 *) - prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composite_uris; + (* + prerr_endline ("adding: " ^ + string_of_bool add_composites ^ UriManager.string_of_uri uri); + 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 []); lemmas @@ -351,7 +274,7 @@ let remove_coercion uri = Not_found -> () (* mhh..... *) -let generate_projections ~basedir uri fields = +let generate_projections ~basedir refinement_toolkit uri fields = let uris = ref [] in let projections = CicRecord.projections_of uri (List.map fst fields) in try @@ -362,10 +285,10 @@ let generate_projections ~basedir uri fields = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj ~basedir uri obj; + add_single_obj ~basedir uri obj refinement_toolkit; let composites = if coercion then - add_coercion ~basedir ~add_composites:true uri + add_coercion ~basedir ~add_composites:true refinement_toolkit uri else [] in @@ -386,15 +309,16 @@ let generate_projections ~basedir uri fields = raise exn -let add_obj uri obj ~basedir = - add_single_obj uri obj ~basedir; +let add_obj refinement_toolkit uri obj ~basedir = + add_single_obj uri obj refinement_toolkit ~basedir; let uris = ref [] in try begin match obj with | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> - uris := !uris @ generate_elimination_principles ~basedir uri; + uris := !uris @ + generate_elimination_principles ~basedir uri refinement_toolkit; let rec get_record_attrs = function | [] -> None @@ -404,7 +328,8 @@ let add_obj uri obj ~basedir = (match get_record_attrs attrs with | None -> () (* not a record *) | Some fields -> - uris := !uris @ (generate_projections ~basedir uri fields)) + uris := !uris @ + (generate_projections ~basedir refinement_toolkit uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end; diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index d063b3282..812685c53 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -25,12 +25,13 @@ exception AlreadyDefined of UriManager.uri -val merge_coercions: Cic.term -> Cic.term - (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) (* it returns the list of the uris of the auxiliary lemmas generated *) -val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list +val add_obj: + RefinementTool.kit -> + UriManager.uri -> Cic.obj -> basedir:string -> + UriManager.uri list (* inverse of add_obj; *) (* Warning: it does not remove the dependencies on the object and on its *) @@ -42,7 +43,8 @@ val remove_obj: UriManager.uri -> unit (* is true are added to the library. *) (* The list of added objects is returned. *) val add_coercion: - basedir:string -> add_composites:bool -> UriManager.uri -> + basedir:string -> add_composites:bool -> + RefinementTool.kit -> UriManager.uri -> UriManager.uri list (* inverse of add_coercion, removes both the eventually created composite *) diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml new file mode 100644 index 000000000..70af8740b --- /dev/null +++ b/components/library/refinementTool.ml @@ -0,0 +1,41 @@ +(* Copyright (C) 2006, 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/ + *) + +type type_of_rc = + | Success of Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph + | Exception of string Lazy.t + + (* these are the same functions of cic_unification/ (eventually wrapped) *) +type kit = { + type_of_aux': + ?localization_tbl:Token.flocation Cic.CicHash.t -> + Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> + type_of_rc; + pack_coercion_obj: Cic.obj -> Cic.obj; + apply_subst: Cic.substitution -> Cic.term -> Cic.term ; + ppsubst: Cic.substitution -> string; + ppmetasenv: Cic.substitution -> Cic.metasenv -> string; +} + diff --git a/components/tactics/proofEngineTypes.ml b/components/tactics/proofEngineTypes.ml index 68ea561f9..4eb043ca8 100644 --- a/components/tactics/proofEngineTypes.ml +++ b/components/tactics/proofEngineTypes.ml @@ -87,11 +87,18 @@ let conclusion_pattern t = exception Fail of string Lazy.t (** - calls the opaque tactic on the status, restoring the original - universe graph if the tactic Fails + calls the opaque tactic on the status *) let apply_tactic t status = - t status + let (uri,metasenv,bo,ty), gl = t status in + match + CicRefine.pack_coercion_obj + (Cic.CurrentProof ("",metasenv,bo,ty,[],[])) + with + | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> + (uri,metasenv,bo,ty), gl + | _ -> assert false +;; (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma index 970a5e388..7a675e377 100644 --- a/matita/library/algebra/groups.ma +++ b/matita/library/algebra/groups.ma @@ -25,7 +25,7 @@ record PreGroup : Type ≝ }. record isGroup (G:PreGroup) : Prop ≝ - { is_monoid: isMonoid G; + { is_monoid:> isMonoid G; inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G); inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G) }. @@ -73,11 +73,11 @@ intros; unfold left_cancellable; unfold injective; intros (x y z); -rewrite < (e_is_left_unit ? (is_monoid ? G)); -rewrite < (e_is_left_unit ? (is_monoid ? G) z); +rewrite < (e_is_left_unit ? G); +rewrite < (e_is_left_unit ? G z); rewrite < (inv_is_left_inverse ? G x); -rewrite > (associative ? (is_semi_group ? (is_monoid ? G))); -rewrite > (associative ? (is_semi_group ? (is_monoid ? G))); +rewrite > (associative ? (is_semi_group ? ( G))); +rewrite > (associative ? (is_semi_group ? ( G))); apply eq_f; assumption. qed. @@ -90,11 +90,11 @@ unfold right_cancellable; unfold injective; simplify;fold simplify (op G); intros (x y z); -rewrite < (e_is_right_unit ? (is_monoid ? G)); -rewrite < (e_is_right_unit ? (is_monoid ? G) z); +rewrite < (e_is_right_unit ? ( G)); +rewrite < (e_is_right_unit ? ( G) z); rewrite < (inv_is_right_inverse ? G x); -rewrite < (associative ? (is_semi_group ? (is_monoid ? G))); -rewrite < (associative ? (is_semi_group ? (is_monoid ? G))); +rewrite < (associative ? (is_semi_group ? ( G))); +rewrite < (associative ? (is_semi_group ? ( G))); rewrite > H; reflexivity. qed. @@ -128,9 +128,9 @@ theorem eq_opxy_z_to_eq_x_opzinvy: ∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1. intros; apply (eq_op_x_y_op_z_y_to_eq ? y); -rewrite > (associative ? (is_semi_group ? (is_monoid ? G))); +rewrite > (associative ? G); rewrite > (inv_is_left_inverse ? G); -rewrite > (e_is_right_unit ? (is_monoid ? G)); +rewrite > (e_is_right_unit ? G); assumption. qed. @@ -138,7 +138,7 @@ theorem eq_opxy_z_to_eq_y_opinvxz: ∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z. intros; apply (eq_op_x_y_op_x_z_to_eq ? x); -rewrite < (associative ? (is_semi_group ? (is_monoid ? G))); +rewrite < (associative ? G); rewrite > (inv_is_right_inverse ? G); rewrite > (e_is_left_unit ? (is_monoid ? G)); assumption. @@ -161,9 +161,9 @@ theorem morphism_to_eq_f_1_1: ∀G,G'.∀f:morphism G G'.f˜1 = 1. intros; apply (eq_op_x_y_op_z_y_to_eq G' (f˜1)); -rewrite > (e_is_left_unit ? (is_monoid ? G') ?); +rewrite > (e_is_left_unit ? G' ?); rewrite < (f_morph ? ? f); -rewrite > (e_is_left_unit ? (is_monoid ? G)); +rewrite > (e_is_left_unit ? G); reflexivity. qed. @@ -264,7 +264,7 @@ unfold belongs_to_subgroup in H1; elim H1; clear H1; exists; -[ +[apply ((a \sub H)\sup-1 · x1) | ]. qed. diff --git a/matita/library/algebra/monoids.ma b/matita/library/algebra/monoids.ma index c3f3cc48e..fc6c8f956 100644 --- a/matita/library/algebra/monoids.ma +++ b/matita/library/algebra/monoids.ma @@ -26,7 +26,7 @@ interpretation "premonoid magma coercion" 'pmmagma M = (cic:/matita/algebra/monoids/magma.con M). record isMonoid (M:PreMonoid) : Prop ≝ - { is_semi_group: isSemiGroup M; + { is_semi_group:> isSemiGroup M; e_is_left_unit: is_left_unit (mk_SemiGroup ? is_semi_group) (e M); e_is_right_unit: diff --git a/matita/matita.ml b/matita/matita.ml index 07f7f900a..d498f2ab6 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -141,6 +141,17 @@ let _ = (UriManager.name_of_uri u ^ ":" ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) (CoercDb.to_list ())); + addDebugItem "show coercions graph" (fun _ -> + let str = CoercGraph.generate_dot_file () in + let filename, oc = Filename.open_temp_file "xx" ".dot" in + output_string oc str; + close_out oc; + let ps = Filename.temp_file "yy" ".png" in + ignore (Sys.command ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename)); + ignore (Sys.command ("/usr/bin/display " ^ ps)); + Sys.remove ps; + Sys.remove filename); + addDebugItem "print top-level grammar entries" CicNotationParser.print_l2_pattern; addDebugItem "dump moo to stderr" (fun _ -> diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 322fcbf41..b8c950549 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -417,7 +417,7 @@ class script ~(source_view: GSourceView.source_view) () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in -let initial_statuses = +let initial_statuses () = (* these include_paths are used only to load the initial notation *) let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in @@ -458,7 +458,7 @@ object (self) val mutable statements = [] (** executed statements *) - val mutable history = [ initial_statuses ] + val mutable history = [ initial_statuses () ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -648,7 +648,7 @@ object (self) method private reset_buffer = statements <- []; - history <- [ initial_statuses ]; + history <- [ initial_statuses () ]; userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; diff --git a/matita/scripts/crontab.sh b/matita/scripts/crontab.sh index 5ad50de5e..65578a87c 100644 --- a/matita/scripts/crontab.sh +++ b/matita/scripts/crontab.sh @@ -14,7 +14,7 @@ mkdir -p $TMPDIRNAME rm -rf $TMPDIRNAMEOLD cd $TMPDIRNAME rm -rf helm -svn co ${SVNROOT}helm/matita/scripts/ > LOG.svn 2>&1 +svn co ${SVNROOT}helm/software/matita/scripts/ > LOG.svn 2>&1 scripts/profile_svn.sh 2> LOG MARK=`echo "select distinct mark from bench where mark like '$TODAY%' order by mark" | mysql -u helm matita | tail -n 1` -- 2.39.2