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
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
(* 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 *)
+ let rec_params =
+ let c =
+ debrujin_constructor ~check_exp_named_subst:false
+ indURI len_tys context consty
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 *)
- 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"))
projects / helm.git / commitdiff