X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=13596c84e27e696b91168d8c2086da8cdeeea0fd;hb=76ec6b95c6f462f7fdedf0bc87354fb874ef4a46;hp=9c6c53aeef5e2d43465b98e524c21aecb67112ef;hpb=9f2c21d0360979096999aaecd5265cc12ac86fef;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 9c6c53aee..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 @@ -159,8 +156,10 @@ let add_single_obj uri obj refinement_toolkit = (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" (univ_time *. 100. /. total_time) (total_time) (univ_time) (UriManager.name_of_uri uri));*) - let _, ugraph, univlist = - CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in + let obj, ugraph, univlist = + try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri + with CicEnvironment.Object_not_found _ -> assert false + in try index_obj ~dbd ~uri; (* 2 must be in the env *) try @@ -228,7 +227,7 @@ let generate_elimination_principles uri refinement_toolkit = List.iter remove_single_obj !uris; raise exn in - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in + let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, _, _, _) -> let counter = ref 0 in @@ -242,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 [];; @@ -272,7 +271,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in - CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph in (* we have to get the source and the tgt type uri * in Coq syntax we have already their names, but @@ -292,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 @@ -310,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 @@ -341,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 @@ -351,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 @@ -397,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 @@ -419,8 +423,8 @@ let generate_projections refinement_toolkit uri fields = (fun (uri, name, bo) (_name, coercion, arity) -> let saturations = 0 in try - let ty, ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let ty, _ = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in add_single_obj uri obj refinement_toolkit; @@ -440,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 [] @@ -478,31 +482,31 @@ let List.fold_right (fun (name,idx,ty,bo) (n,uris) -> if name = name_to_avoid then - (n+1,uris) + (n-1,uris) else let uri = UriManager.uri_of_string (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.Fix (n,funs) in + let bo = Cic.Fix (n-1,funs) in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj uri obj refinement_toolkit; - (n+1,uri::uris) - ) funs (1,[])) + (add_single_obj uri obj refinement_toolkit; + (n-1,uri::uris))) + funs (List.length funs,[])) | Cic.CoFix (_,funs) -> snd ( List.fold_right (fun (name,ty,bo) (n,uris) -> if name = name_to_avoid then - (n+1,uris) + (n-1,uris) else let uri = UriManager.uri_of_string (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.CoFix (n,funs) in + let bo = Cic.CoFix (n-1,funs) in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in add_single_obj uri obj refinement_toolkit; - (n+1,uri::uris) - ) funs (1,[])) + (n-1,uri::uris) + ) funs (List.length funs,[])) | _ -> assert false let add_obj refinement_toolkit uri obj = @@ -519,21 +523,25 @@ let add_obj refinement_toolkit uri obj = generate_sibling_mutual_definitions refinement_toolkit uri attrs name bo | Cic.Constant _ -> () - | Cic.InductiveDefinition (_,_,_,attrs) -> - uris := !uris @ - generate_elimination_principles uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit uri obj; - let rec get_record_attrs = - function - | [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - | None -> () (* not a record *) - | Some fields -> - uris := !uris @ - (generate_projections refinement_toolkit uri fields)) + | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> + let _,inductive,_,_ = List.hd inductivefuns in + if inductive then + begin + uris := !uris @ + generate_elimination_principles uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit uri obj; + end ; + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> () (* not a record *) + | Some fields -> + uris := !uris @ + (generate_projections refinement_toolkit uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end;