else
ug,ul,obj
| None ->
- CicUnivUtils.clean_and_fill uri obj inferred_ugraph
+ CicUnivUtils.clean_and_fill uri obj inferred_ugraph
;;
let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
exception CicEnvironmentError;;
-let rec type_of_constant ~logger uri ugraph =
+let rec type_of_constant ~logger uri orig_ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph =
- match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+ match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
let inferred_ugraph =
match uobj with
C.Constant (_,Some te,ty,_,_) ->
- let _,ugraph = type_of ~logger ty ugraph in
+ let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
let type_of_te,ugraph = type_of ~logger te ugraph in
let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
if not b then
ugraph
| C.Constant (_,None,ty,_,_) ->
(* only to check that ty is well-typed *)
- let _,ugraph = type_of ~logger ty ugraph in
+ let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
ugraph
| C.CurrentProof (_,conjs,te,ty,_,_) ->
let _,ugraph =
List.fold_left
(fun (metasenv,ugraph) ((_,context,ty) as conj) ->
let _,ugraph =
- type_of_aux' ~logger metasenv context ty ugraph
+ type_of_aux' ~logger metasenv context ty ugraph
in
(metasenv @ [conj],ugraph)
- ) ([],ugraph) conjs
+ ) ([],CicUniv.empty_ugraph) conjs
in
let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
logger#log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
in
| _ ->
raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
-and type_of_variable ~logger uri ugraph =
+and type_of_variable ~logger uri orig_ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
- match CicEnvironment.is_type_checked ~trust:true ugraph uri with
- CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
- | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) ->
+ match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
+ | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+ | CicEnvironment.UncheckedObj
+ (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph)
+ ->
logger#log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
- let _,ugraph = type_of ~logger ty ugraph in
+ let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
let inferred_ugraph =
match bo with
None -> ugraph
else
ugraph
in
- let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+ let ugraph, ul, obj =
+ check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj
+ in
CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
logger#log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
| _ ->
- raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
+ raise (TypeCheckerFailure (lazy
+ ("Unknown variable:" ^ U.string_of_uri uri)))
and does_not_occur ?(subst=[]) context n nn te =
let module C = Cic in
with
CicUtil.Subst_not_found _ -> true)
| C.Cast (te,ty) ->
- does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
+ does_not_occur ~subst context n nn te &&
+ does_not_occur ~subst context n nn ty
| C.Prod (name,so,dest) ->
does_not_occur ~subst context n nn so &&
does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
(nn + 1) dest
| C.Lambda (name,so,dest) ->
does_not_occur ~subst context n nn so &&
- does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
dest
| C.LetIn (name,so,ty,dest) ->
does_not_occur ~subst context n nn so &&
does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
(n + 1) (nn + 1) dest
| C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
+ List.for_all (does_not_occur ~subst context n nn) l
| C.Var (_,exp_named_subst)
| C.Const (_,exp_named_subst)
| C.MutInd (_,_,exp_named_subst)
| C.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
- exp_named_subst true
+ List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x)
+ exp_named_subst
| C.MutCase (_,_,out,te,pl) ->
- does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
+ does_not_occur ~subst context n nn out &&
+ does_not_occur ~subst context n nn te &&
+ List.for_all (does_not_occur ~subst context n nn) pl
| C.Fix (_,fl) ->
let len = List.length fl in
let n_plus_len = n + len in
lazy ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri)))
-and type_of_mutual_inductive_defs ~logger uri i ugraph =
+and type_of_mutual_inductive_defs ~logger uri i orig_ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph1 =
- match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+ match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
- let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in
+ let inferred_ugraph =
+ check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph
+ in
let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
logger#log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
)
in
- match cobj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity,ugraph1
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
+ match cobj with
+ | C.InductiveDefinition (dl,_,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity,ugraph1
+ | _ ->
+ raise (TypeCheckerFailure
+ (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
-and type_of_mutual_inductive_constr ~logger uri i j ugraph =
+and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph1 =
- match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+ match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
let inferred_ugraph =
- check_mutual_inductive_defs ~logger uri uobj ugraph
+ check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph
in
let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
logger#log (`Type_checking_completed uri) ;
(match
- CicEnvironment.is_type_checked ~trust:false ugraph uri
+ CicEnvironment.is_type_checked ~trust:false orig_ugraph uri
with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ ->
cl
in
name, isind, arity, cl)
- tl
+ tl, paramsno
| _ -> assert false)
| _ -> assert false
| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
| C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
- let tys =
+ let tys,_ =
specialize_inductive_type ~logger ~subst ~metasenv context term
in
- let tys_ctx =
- List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+ let tys_ctx,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ([],0) tys
in
let _,isinductive,_,cl = List.nth tys i in
if not isinductive then
=
let module C = Cic in
let module U = UriManager in
- match CicReduction.whd ~subst context t with
+ let t = CicReduction.whd ~delta:false ~subst context t in
+ let res =
+ match t with
C.Rel m when m > n && m <= nn -> false
| C.Rel m ->
(match List.nth context (m-1) with
List.for_all
(guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
tl &&
- let tys =
+ let tys,_ =
specialize_inductive_type ~logger ~subst ~metasenv context t
in
- let tys_ctx =
- List.map
- (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+ let tys_ctx,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ([],0) tys
in
let _,isinductive,_,cl = List.nth tys i in
if not isinductive then
List.fold_right
(fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
tl true
+ in
+ if res then res
+ else
+ let t' = CicReduction.whd ~subst context t in
+ if t = t' then
+ false
+ else
+ guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
(* the boolean h means already protected *)
(* args is the list of arguments the type of the constructor that may be *)
(* found in head position must be applied to. *)
-and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~logger ~subst ~metasenv indURI =
let module C = Cic in
- (*CSC: There is a lot of code replication between the cases X and *)
- (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
- (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
+ let rec aux context n nn h te =
match CicReduction.whd ~subst context te with
- C.Rel m when m > n && m <= nn -> h
- | C.Rel _ -> true
- | C.Meta _
+ | C.Rel m when m > n && m <= nn -> h
+ | C.Rel _
+ | C.Meta _ -> true
| C.Sort _
| C.Implicit _
| C.Cast _
| C.Prod _
- | C.LetIn _ ->
- (* the term has just been type-checked *)
- raise (AssertFailure (lazy "17"))
+ | C.MutInd _
+ | C.LetIn _ -> raise (AssertFailure (lazy "17"))
| C.Lambda (name,so,de) ->
does_not_occur ~subst context n nn so &&
- guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
- (n + 1) (nn + 1) h de args coInductiveTypeURI
+ aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
- h &&
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
- | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
- let consty =
- let obj,_ =
- try
- CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- let (_,cons) = List.nth cl (j - 1) in
- CicSubstitution.subst_vars exp_named_subst cons
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+ h && List.for_all (does_not_occur ~subst context n nn) tl
+ | C.MutConstruct (_,_,_,exp_named_subst) ->
+ List.for_all
+ (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst
+ | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t ->
+ List.for_all
+ (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst &&
+ let consty, len_tys, tys_ctx, paramsno =
+ let tys, paramsno =
+ specialize_inductive_type ~logger ~subst ~metasenv context t in
+ let _,_,_,cl = List.nth tys i in
+ let _,ty = List.nth cl (j-1) in
+ ty, List.length tys,
+ fst(List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1)
+ ([],0) tys), paramsno
in
- let rec analyse_branch context ty te =
- match CicReduction.whd ~subst context ty with
- C.Meta _ -> raise (AssertFailure (lazy "34"))
- | C.Rel _
- | C.Var _
- | C.Sort _ ->
- does_not_occur ~subst context n nn te
- | C.Implicit _
- | C.Cast _ ->
- raise (AssertFailure (lazy "24"))(* due to type-checking *)
- | C.Prod (name,so,de) ->
- analyse_branch ((Some (name,(C.Decl so)))::context) de te
- | C.Lambda _
- | C.LetIn _ ->
- raise (AssertFailure (lazy "25"))(* due to type-checking *)
- | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
- guarded_by_constructors ~subst context n nn true te []
- coInductiveTypeURI
- | C.Appl ((C.MutInd (uri,_,_))::_) ->
- guarded_by_constructors ~subst context n nn true te tl
- coInductiveTypeURI
- | C.Appl _ ->
- does_not_occur ~subst context n nn te
- | C.Const _ -> raise (AssertFailure (lazy "26"))
- | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
- guarded_by_constructors ~subst context n nn true te []
- coInductiveTypeURI
- | C.MutInd _ ->
- does_not_occur ~subst context n nn te
- | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
- (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
- (*CSC: in head position. *)
- | C.MutCase _
- | C.Fix _
- | C.CoFix _ ->
- raise (AssertFailure (lazy "28"))(* due to type-checking *)
- in
- let rec analyse_instantiated_type context ty l =
- match CicReduction.whd ~subst context ty with
- C.Rel _
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit _
- | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
- | C.Prod (name,so,de) ->
- begin
- match l with
- [] -> true
- | he::tl ->
- analyse_branch context so he &&
- analyse_instantiated_type
- ((Some (name,(C.Decl so)))::context) de tl
- end
- | C.Lambda _
- | C.LetIn _ ->
- raise (AssertFailure (lazy "30"))(* due to type-checking *)
- | C.Appl _ ->
- List.fold_left
- (fun i x -> i && does_not_occur ~subst context n nn x) true l
- | C.Const _ -> raise (AssertFailure (lazy "31"))
- | C.MutInd _ ->
- List.fold_left
- (fun i x -> i && does_not_occur ~subst context n nn x) true l
- | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
- (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
- (*CSC: in head position. *)
- | C.MutCase _
- | C.Fix _
- | C.CoFix _ ->
- raise (AssertFailure (lazy "33"))(* due to type-checking *)
- in
- let rec instantiate_type args consty =
- function
- [] -> true
- | tlhe::tltl as l ->
- let consty' = CicReduction.whd ~subst context consty in
- match args with
- he::tl ->
- begin
- match consty' with
- C.Prod (_,_,de) ->
- let instantiated_de = CicSubstitution.subst he de in
- (*CSC: siamo sicuri che non sia troppo forte? *)
- does_not_occur ~subst context n nn tlhe &
- instantiate_type tl instantiated_de tltl
- | _ ->
- (*CSC:We do not consider backbones with a MutCase, a *)
- (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
- raise (AssertFailure (lazy "23"))
- end
- | [] -> analyse_instantiated_type context consty' l
- (* These are all the other cases *)
+ let rec_params =
+ let c =
+ debrujin_constructor ~check_exp_named_subst:false
+ indURI len_tys context consty
in
- instantiate_type args consty tl
- | C.Appl ((C.CoFix (_,fl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl
- in
- List.fold_right
- (fun (_,ty,bo) i ->
- i && does_not_occur ~subst context n nn ty &&
- guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
- h bo args coInductiveTypeURI
- ) fl true
- | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
- does_not_occur ~subst context n nn out &&
- does_not_occur ~subst context n nn te &&
- List.fold_right
- (fun x i ->
- i &&
- guarded_by_constructors ~subst context n nn h x args
- coInductiveTypeURI
- ) pl true
- | C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
- | C.Var (_,exp_named_subst)
- | C.Const (_,exp_named_subst) ->
- List.fold_right
- (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
- | C.MutInd _ -> assert false
- | C.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right
- (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
- | C.MutCase (_,_,out,te,pl) ->
+ let len_ctx = List.length context in
+ recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c
+ in
+ let rec analyse_instantiated_type rec_spec args =
+ match rec_spec, args with
+ | h::rec_spec, he::args ->
+ aux context n nn h he &&
+ analyse_instantiated_type rec_spec args
+ | _,[] -> true
+ | _ -> raise (AssertFailure (lazy
+ ("Too many args for constructor: " ^ String.concat " "
+ (List.map (fun x-> CicPp.ppterm x) args))))
+ in
+ let left, args = HExtlib.split_nth paramsno tl in
+ List.for_all (does_not_occur ~subst context n nn) left &&
+ analyse_instantiated_type rec_params args
+ | C.Appl ((C.MutCase (_,_,out,te,pl))::_)
+ | C.MutCase (_,_,out,te,pl) as t ->
+ let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+ List.for_all (does_not_occur ~subst context n nn) tl &&
does_not_occur ~subst context n nn out &&
- does_not_occur ~subst context n nn te &&
- List.fold_right
- (fun x i ->
- i &&
- guarded_by_constructors ~subst context n nn h x args
- coInductiveTypeURI
- ) pl true
- | C.Fix (_,fl) ->
+ does_not_occur ~subst context n nn te &&
+ List.for_all (aux context n nn h ) pl
+ | C.Fix (_,fl)
+ | C.Appl (C.Fix (_,fl)::_) as t ->
+ let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
let len = List.length fl in
let n_plus_len = n + len
and nn_plus_len = nn + len
- (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
and tys,_ =
List.fold_left
(fun (types,len) (n,_,ty,_) ->
(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
len+1)
- ) ([],0) fl
+ ) ([],0) fl
in
- List.fold_right
- (fun (_,_,ty,bo) i ->
- i && does_not_occur ~subst context n nn ty &&
- does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
- ) fl true
- | C.CoFix (_,fl) ->
- let len = List.length fl in
+ List.for_all (does_not_occur ~subst context n nn) tl &&
+ List.for_all
+ (fun (_,_,ty,bo) ->
+ does_not_occur ~subst context n nn ty &&
+ aux (tys@context) n_plus_len nn_plus_len h bo)
+ fl
+ | C.Appl ((C.CoFix (_,fl))::_)
+ | C.CoFix (_,fl) as t ->
+ let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+ let len = List.length fl in
let n_plus_len = n + len
and nn_plus_len = nn + len
- (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
and tys,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
- List.fold_right
- (fun (_,ty,bo) i ->
- i && does_not_occur ~subst context n nn ty &&
- guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
- h bo
- args coInductiveTypeURI
- ) fl true
+ List.for_all (does_not_occur ~subst context n nn) tl &&
+ List.for_all
+ (fun (_,ty,bo) ->
+ does_not_occur ~subst context n nn ty &&
+ aux (tys@context) n_plus_len nn_plus_len h bo)
+ fl
+ | C.Var _
+ | C.Const _
+ | C.Appl _ as t -> does_not_occur ~subst context n nn t
+ in
+ aux
and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
need_dummy ind arity1 arity2 ugraph =
let's control the guarded by constructors
conditions C{f,M}
*)
- if not (guarded_by_constructors ~subst
- (types @ context) 0 len false bo [] uri) then
+ if not (guarded_by_constructors ~logger ~subst ~metasenv uri
+ (types @ context) 0 len false bo) then
raise
(TypeCheckerFailure
(lazy "CoFix: not guarded by constructors"))
let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
logger#log (`Type_checking_completed uri);
- match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
| CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| _ -> raise CicEnvironmentError
;;
projects / helm.git / blobdiff