- aux ty @ aux te @
- (List.fold_left (fun x t -> x @ (aux t)) [] patterns)
- | C.Fix (no, funs) ->
- List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
- | C.CoFix (no,funs) ->
- List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
- and aux_obj ?(boo=false) (t,_) =
- (match t with
- C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Constant (_,None,ty,v) -> aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.Variable (_,None ,ty,v) -> aux ty @
- List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v
- | C.InductiveDefinition (l,v,_) ->
- (List.fold_left (
- fun x (_,_,t,l') ->
- x @ aux t @ List.fold_left (
- fun y (_,t) -> y @ aux t)
- [] l')
- [] l) @
- (List.fold_left (
- fun l u ->
- l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
- [] v)
- )
+ 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 (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,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)