From e764936e17ab96ddb6f6549bb65cc419e4e4ccac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Oct 2005 08:12:04 +0000 Subject: [PATCH] fixed clean_and_fill that now fills the object (used to fill only graph) --- helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 125 +++++++++--------- .../ocaml/cic_proof_checking/cicUnivUtils.mli | 2 +- 2 files changed, 66 insertions(+), 61 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml index 1f3b698d3..ace4f844f 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml @@ -50,81 +50,76 @@ let universes_of_obj uri t = let add_result l = results := l :: !results in (* the iterators *) let rec aux = function - | C.Const (u,exp_named_subst) + | C.Const (u,exp_named_subst) when is_not_visited u -> + aux_uri u; + visited u; + C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst) | C.Var (u,exp_named_subst) when is_not_visited u -> aux_uri u; visited u; - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.Const (u,exp_named_subst) + C.Var (u, List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.Const (u,exp_named_subst) -> + C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst) | C.Var (u,exp_named_subst) -> - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.MutInd (u,_,exp_named_subst) when is_not_visited u -> + C.Var (u, List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.MutInd (u,x,exp_named_subst) when is_not_visited u -> + aux_uri u; visited u; - (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with - | C.InductiveDefinition (l,_,_,_) -> - List.iter - (fun (_,_,t,l') -> - aux t; - List.iter (fun (_,t) -> aux t) l') - l - | _ -> assert false); - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.MutInd (_,_,exp_named_subst) -> - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.MutConstruct (u,_,_,exp_named_subst) when is_not_visited u -> + C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.MutInd (u,x,exp_named_subst) -> + C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u -> + aux_uri u; visited u; - (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with - | C.InductiveDefinition (l,_,_,_) -> - List.iter - (fun (_,_,t,l') -> - aux t; - List.iter (fun (_,t) -> aux t) l') - l - | _ -> assert false); - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.iter (fun (_,t) -> aux t) exp_named_subst - | C.Meta (n,l1) -> - List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1 - | C.Sort ( C.Type i) -> add_result [i] + C.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.MutConstruct (x,y,z,exp_named_subst) -> + C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst) + | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1) + | C.Sort (C.Type i) -> add_result [i]; + C.Sort (C.Type (CicUniv.name_universe i uri)) | C.Rel _ | C.Sort _ - | C.Implicit _ -> () - | C.Cast (v,t) -> aux v; aux t - | C.Prod (b,s,t) - | C.Lambda (b,s,t) - | C.LetIn (b,s,t) -> aux s; aux t - | C.Appl li -> List.iter (fun t -> aux t) li + | C.Implicit _ as x -> x + | C.Cast (v,t) -> C.Cast (aux v, aux t) + | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t) + | C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t) + | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t) + | C.Appl li -> C.Appl (List.map aux li) | C.MutCase (uri,n1,ty,te,patterns) -> - aux ty; aux te; (List.iter (fun t -> aux t) patterns) - | C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs - | C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs + C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns) + | C.Fix (no, funs) -> + C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs) + | C.CoFix (no,funs) -> + C.CoFix(no, List.map (fun (x,b,c) -> (x,aux b,aux c)) funs) and aux_uri u = if is_not_visited u then let _, _, l = CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in add_result l and aux_obj = function - | C.Constant (_,Some te,ty,v,_) - | C.Variable (_,Some te,ty,v,_) -> - aux te; - aux ty; - List.iter aux_uri v - | C.Constant (_,None, ty, v,_) - | C.Variable (_,None, ty, v,_) -> - aux ty; - List.iter aux_uri v + | C.Constant (x,Some te,ty,v,y) -> + List.iter aux_uri v; + C.Constant (x,Some (aux te),aux ty,v,y) + | C.Variable (x,Some te,ty,v,y) -> + List.iter aux_uri v; + C.Variable (x,Some (aux te),aux ty,v,y) + | C.Constant (x,None, ty, v,y) -> + List.iter aux_uri v; + C.Constant (x,None, aux ty, v,y) + | C.Variable (x,None, ty, v,y) -> + List.iter aux_uri v; + C.Variable (x,None, aux ty, v,y) | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false - | C.InductiveDefinition (l,v,_,_) -> - List.iter - (fun (_,_,t,l') -> - aux t; - List.iter (fun (_,t) -> aux t) l') - l; - List.iter aux_uri v + | C.InductiveDefinition (l,v,x,y) -> + List.iter aux_uri v; + C.InductiveDefinition ( + List.map + (fun (x,y,t,l') -> + (x,y,aux t, List.map (fun (x,t) -> x,aux t) l')) + l,v,x,y) in - aux_obj t; - List.flatten !results + let o = aux_obj t in + List.flatten !results, o let rec list_uniq = function | [] -> [] @@ -135,12 +130,22 @@ let rec list_uniq = function let list_uniq l = list_uniq (List.fast_sort CicUniv.compare l) +let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile + let clean_and_fill uri obj ugraph = - let list_of_universes = universes_of_obj uri obj in + (* universes of obj fills the universes of the obj with the right uri *) + let list_of_universes, obj = universes_of_obj uri obj in let list_of_universes = list_uniq list_of_universes in +(* CicUniv.print_ugraph ugraph;*) +(* List.iter (fun u -> prerr_endline (CicUniv.string_of_universe u))*) +(* list_of_universes;*) let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in +(* CicUniv.print_ugraph ugraph;*) let ugraph, list_of_universes = CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri in - ugraph, list_of_universes + ugraph, list_of_universes, obj +let clean_and_fill u o g = + profiler (clean_and_fill u o) g + diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli index f3dfe3f09..eb55a47eb 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli @@ -28,5 +28,5 @@ *) val clean_and_fill: UriManager.uri -> Cic.obj -> CicUniv.universe_graph -> - CicUniv.universe_graph * CicUniv.universe list + CicUniv.universe_graph * CicUniv.universe list * Cic.obj -- 2.39.2