-let rec list_iter_default2 f l1 def l2 =
- match l1,l2 with
- | [], _ -> ()
- | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb
- | a::ta, [] -> f a def; list_iter_default2 f ta def []
-;;
-
-
-(*
-(* 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 =
- 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 *)
- match CicReduction.whd ~subst context te with
- C.Rel m when m > n && m <= nn -> h
- | C.Rel _ -> true
- | C.Meta _
- | C.Sort _
- | C.Implicit _
- | C.Cast _
- | C.Prod _
- | C.LetIn _ ->
- (* the term has just been type-checked *)
- 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
- | 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)))
- 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 *)
- 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) ->
- 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) ->
- 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 &&
- does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
- ) fl true
- | C.CoFix (_,fl) ->
- 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
-
- in
- type_of_aux ~logger context t ugraph
-
-;;
-
-(** wrappers which instantiate fresh loggers *)
-
-(* check_allowed_sort_elimination uri i s1 s2
- This function is used outside the kernel to determine in advance whether
- a MutCase will be allowed or not.
- [uri,i] is the type of the term to match
- [s1] is the sort of the term to eliminate (i.e. the head of the arity
- of the inductive type [uri,i])
- [s2] is the sort of the goal (i.e. the head of the type of the outtype
- of the MutCase) *)
-let check_allowed_sort_elimination uri i s1 s2 =
- fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
- ~logger:(new CicLogger.logger) [] uri i true
- (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
- CicUniv.empty_ugraph)
-;;
-
-Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
-
-*)
-
-module C = NCic
-module R = NCicReduction
-module Ref = NReference
-module S = NCicSubstitution
-module U = NCicUtils
-module E = NCicEnvironment
-
-let rec split_prods ~subst context n te =
- match (n, R.whd ~subst context te) with
- | (0, _) -> context,te
- | (n, C.Prod (name,so,ta)) when n > 0 ->
- split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
- | (_, _) -> raise (AssertFailure (lazy "split_prods"))
-;;
-
-let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =