exception CicEnvironmentError;;
-let rec type_of_constant ~logger uri (ugraph as orig_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
| _ ->
raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
-and type_of_variable ~logger uri (ugraph as orig_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 orig_ugraph uri with
| 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
(* constructors using Prods *)
let len = List.length itl in
let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
+ List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
let _,ugraph2 =
List.fold_right
- (fun (_,_,_,cl) (i,ugraph) ->
+ (fun (_,_,ty,cl) (i,ugraph) ->
+ let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
let ugraph'' =
List.fold_left
(fun ugraph (name,te) ->
- let debrujinedte = debrujin_constructor uri len [] te in
- let augmented_term =
- List.fold_right
- (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
- itl debrujinedte
- in
- let _,ugraph' = type_of ~logger augmented_term ugraph in
+ let te = debrujin_constructor uri len [] te in
+ let context,te = split_prods ~subst:[] tys indparamsno te in
+ let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
+ let ugraph =
+ match
+ CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
+ with
+ Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) ->
+ CicUniv.add_ge u2 u1 ugraph
+ | Cic.Sort _, Cic.Sort Cic.Prop
+ | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp
+ | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
+ | _, _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy ("Wrong constructor or inductive arity shape"))) in
(* let's check also the positivity conditions *)
if
not
- (are_all_occurrences_positive tys uri indparamsno i 0 len
- debrujinedte)
+ (are_all_occurrences_positive context uri indparamsno
+ (i+indparamsno) indparamsno (len+indparamsno) te)
then
begin
prerr_endline (UriManager.string_of_uri uri);
(TypeCheckerFailure
(lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end
else
- ugraph'
+ ugraph
) ugraph cl in
(i + 1),ugraph''
) itl (1,ugrap1)
lazy ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri)))
-and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_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) ;
| 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 as orig_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);
let module R = CicReduction in
match (n, R.whd ~subst context te) with
(0, _) -> context,te
- | (n, C.Prod (name,so,ta)) when n > 0 ->
+ | (n, C.Sort _) when n <= 0 -> context,te
+ | (n, C.Prod (name,so,ta)) ->
split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
| (_, _) -> raise (AssertFailure (lazy "8"))
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 =
| C.Var (uri,exp_named_subst) ->
incr fdebug ;
let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
in
let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
| C.Const (uri,exp_named_subst) ->
incr fdebug ;
let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
in
let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
let cty1 =
| C.MutInd (uri,i,exp_named_subst) ->
incr fdebug ;
let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
in
- (* TASSI: da me c'era anche questa, ma in CVS no *)
let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
- (* fine parte dubbia *)
let cty =
CicSubstitution.subst_vars exp_named_subst mty
in
cty,ugraph2
| C.MutConstruct (uri,i,j,exp_named_subst) ->
let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
in
- (* TASSI: idem come sopra *)
let mty,ugraph2 =
type_of_mutual_inductive_constr ~logger uri i j ugraph1
in
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 (_,ty,_) = List.nth fl i in
ty,ugraph2
- and check_exp_named_subst ~logger ~subst context =
+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+ let params =
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match obj with
+ Cic.Constant (_,_,_,params,_) -> params
+ | Cic.Variable (_,_,_,params,_) -> params
+ | Cic.CurrentProof (_,_,_,_,params,_) -> params
+ | Cic.InductiveDefinition (_,params,_,_) -> params
+ ) in
+ let rec check_same_order params ens =
+ match params,ens with
+ | _,[] -> ()
+ | [],_::_ ->
+ raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+ | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+ check_same_order tl tl'
+ | _::tl,l -> check_same_order tl l
+ in
let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
match l with
[] -> ugraph
raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
end
in
- check_exp_named_subst_aux ~logger []
+ check_same_order params ens ;
+ check_exp_named_subst_aux ~logger [] ens ugraph
and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
let module C = Cic in
projects / helm.git / blobdiff