-and recursive_args context n nn te =
- let module C = Cic in
- match CicReduction.whd context te with
- C.Rel _ -> []
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit _
- | C.Cast _ (*CSC ??? *) ->
- raise (AssertFailure (lazy "3")) (* due to type-checking *)
- | C.Prod (name,so,de) ->
- (not (does_not_occur context n nn so)) ::
- (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
- | C.Lambda _
- | C.LetIn _ ->
- raise (AssertFailure (lazy "4")) (* due to type-checking *)
- | C.Appl _ -> []
- | C.Const _ -> raise (AssertFailure (lazy "5"))
- | C.MutInd _
- | C.MutConstruct _
- | C.MutCase _
- | C.Fix _
- | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
-
-and get_new_safes ~subst context p c rl safes n nn x =
- let module C = Cic in
- let module U = UriManager in
- let module R = CicReduction in
- match (R.whd ~subst context c, R.whd ~subst context p, rl) with
- (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
- (* we are sure that the two sources are convertible because we *)
- (* have just checked this. So let's go along ... *)
- let safes' =
- List.map (fun x -> x + 1) safes
- in
- let safes'' =
- if b then 1::safes' else safes'
- in
- get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
- ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
- | (C.Prod _, (C.MutConstruct _ as e), _)
- | (C.Prod _, (C.Rel _ as e), _)
- | (C.MutInd _, e, [])
- | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
- | (c,p,l) ->
- (* CSC: If the next exception is raised, it just means that *)
- (* CSC: the proof-assistant allows to use very strange things *)
- (* CSC: as a branch of a case whose type is a Prod. In *)
- (* CSC: particular, this means that a new (C.Prod, x,_) case *)
- (* CSC: must be considered in this match. (e.g. x = MutCase) *)
- raise
- (AssertFailure (lazy
- (Printf.sprintf "Get New Safes: c=%s ; p=%s"
- (CicPp.ppterm c) (CicPp.ppterm p))))
-
-and split_prods ~subst context n te =
- let module C = Cic in
- 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 ->
- split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
- | (_, _) -> raise (AssertFailure (lazy "8"))
-
-and eat_lambdas ~subst context n te =
- let module C = Cic in
- let module R = CicReduction in
- match (n, R.whd ~subst context te) with
- (0, _) -> (te, 0, context)
- | (n, C.Lambda (name,so,ta)) when n > 0 ->
- let (te, k, context') =
- eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
- in
- (te, k + 1, context')
- | (n, te) ->
- raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
-
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
-and check_is_really_smaller_arg ~subst context n nn kl x safes te =
- (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
- (*CSC: cfr guarded_by_destructors *)
- let module C = Cic in
- let module U = UriManager in
- match CicReduction.whd ~subst context te with
- C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit _
- | C.Cast _
-(* | C.Cast (te,ty) ->
- check_is_really_smaller_arg ~subst n nn kl x safes te &&
- check_is_really_smaller_arg ~subst n nn kl x safes ty*)
-(* | C.Prod (_,so,ta) ->
- check_is_really_smaller_arg ~subst n nn kl x safes so &&
- check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
- (List.map (fun x -> x + 1) safes) ta*)
- | C.Prod _ -> raise (AssertFailure (lazy "10"))
- | C.Lambda (name,so,ta) ->
- check_is_really_smaller_arg ~subst context n nn kl x safes so &&
- check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.LetIn (name,so,ty,ta) ->
- check_is_really_smaller_arg ~subst context n nn kl x safes so &&
- check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
- check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.Appl (he::_) ->
- (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
- (*CSC: solo perche' non abbiamo trovato controesempi *)
- check_is_really_smaller_arg ~subst context n nn kl x safes he
- | C.Appl [] -> raise (AssertFailure (lazy "11"))
- | C.Const _
- | C.MutInd _ -> raise (AssertFailure (lazy "12"))
- | C.MutConstruct _ -> false
- | C.MutCase (uri,i,outtype,term,pl) ->
- (match term with
- C.Rel m when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
- in
- let (_,isinductive,_,cl) = List.nth tl i in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- List.fold_right
- (fun p i ->
- i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
- pl true
- else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- Invalid_argument _ ->
- raise (TypeCheckerFailure (lazy "not enough patterns"))
- in
- List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
- in
- let (e,safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let (_,isinductive,_,cl) = List.nth tl i in
- let tys =
- List.map (fun (n,_,ty,_) ->
- Some(Cic.Name n,(Cic.Decl ty))) tl
- in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- List.fold_right
- (fun p i ->
- i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
- pl true
- else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- Invalid_argument _ ->
- raise (TypeCheckerFailure (lazy "not enough patterns"))
- in
- (*CSC: supponiamo come prima che nessun controllo sia necessario*)
- (*CSC: sugli argomenti di una applicazione *)
- List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
- in
- let (e, safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | _ ->
- List.fold_right
- (fun p i ->
- i && check_is_really_smaller_arg ~subst context n nn kl x safes p
- ) pl true
- )
- | C.Fix (_, fl) ->
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- 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
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,_,ty,bo) i ->
- i &&
- check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
- | C.CoFix (_, fl) ->
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- 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
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,ty,bo) i ->
- i &&
- check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
-
-and guarded_by_destructors ~subst context n nn kl x safes =
- let module C = Cic in
- let module U = UriManager in
- function
- C.Rel m when m > n && m <= nn -> false
- | C.Rel m ->
- (match List.nth context (n-1) with
- Some (_,C.Decl _) -> true
- | Some (_,C.Def (bo,_)) ->
- guarded_by_destructors ~subst context m nn kl x safes
- (CicSubstitution.lift m bo)
- | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
- )
- | C.Meta _
- | C.Sort _
- | C.Implicit _ -> true
- | C.Cast (te,ty) ->
- guarded_by_destructors ~subst context n nn kl x safes te &&
- guarded_by_destructors ~subst context n nn kl x safes ty
- | C.Prod (name,so,ta) ->
- guarded_by_destructors ~subst context n nn kl x safes so &&
- guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.Lambda (name,so,ta) ->
- guarded_by_destructors ~subst context n nn kl x safes so &&
- guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.LetIn (name,so,ty,ta) ->
- guarded_by_destructors ~subst context n nn kl x safes so &&
- guarded_by_destructors ~subst context n nn kl x safes ty &&
- guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
- let k = List.nth kl (m - n - 1) in
- if not (List.length tl > k) then false
- else
- List.fold_right
- (fun param i ->
- i && guarded_by_destructors ~subst context n nn kl x safes param
- ) tl true &&
- check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
- | C.Appl tl ->
- List.fold_right
- (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
- tl true
- | C.Var (_,exp_named_subst)
- | C.Const (_,exp_named_subst)
- | C.MutInd (_,_,exp_named_subst)
- | C.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right
- (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
- exp_named_subst true
- | C.MutCase (uri,i,outtype,term,pl) ->
- (match CicReduction.whd ~subst context term with
- C.Rel m when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let len = List.length tl in
- let (_,isinductive,_,cl) = List.nth tl i in
- let tys =
- List.map (fun (n,_,ty,_) ->
- Some(Cic.Name n,(Cic.Decl ty))) tl
- in
- let cl' =
- List.map
- (fun (id,ty) ->
- let debrujinedty = debrujin_constructor uri len ty in
- (id, snd (split_prods ~subst tys paramsno ty),
- snd (split_prods ~subst tys paramsno debrujinedty)
- )) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (tys@lefts,len,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- guarded_by_destructors ~subst context n nn kl x safes outtype &&
- guarded_by_destructors ~subst context n nn kl x safes term &&
- (*CSC: manca ??? il controllo sul tipo di term? *)
- List.fold_right
- (fun p i ->
- i && guarded_by_destructors ~subst context n nn kl x safes p)
- pl true
- else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- Invalid_argument _ ->
- raise (TypeCheckerFailure (lazy "not enough patterns"))
- in
- guarded_by_destructors ~subst context n nn kl x safes outtype &&
- (*CSC: manca ??? il controllo sul tipo di term? *)
- List.fold_right
- (fun (p,(_,c,brujinedc)) i ->
- let rl' = recursive_args lefts_and_tys 0 len brujinedc in
- let (e,safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- guarded_by_destructors ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let (_,isinductive,_,cl) = List.nth tl i in
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
- in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (tys@lefts,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- guarded_by_destructors ~subst context n nn kl x safes outtype &&
- guarded_by_destructors ~subst context n nn kl x safes term &&
- (*CSC: manca ??? il controllo sul tipo di term? *)
- List.fold_right
- (fun p i ->
- i && guarded_by_destructors ~subst context n nn kl x safes p)
- pl true
- else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- Invalid_argument _ ->
- raise (TypeCheckerFailure (lazy "not enough patterns"))
- in
- guarded_by_destructors ~subst context n nn kl x safes outtype &&
- (*CSC: manca ??? il controllo sul tipo di term? *)
- List.fold_right
- (fun t i ->
- i && guarded_by_destructors ~subst context n nn kl x safes t)
- tl true &&
- List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
- in
- let (e, safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- guarded_by_destructors ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | _ ->
- guarded_by_destructors ~subst context n nn kl x safes outtype &&
- guarded_by_destructors ~subst context n nn kl x safes term &&
- (*CSC: manca ??? il controllo sul tipo di term? *)
- List.fold_right
- (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
- pl true
- )
- | C.Fix (_, fl) ->
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- 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
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,_,ty,bo) i ->
- i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
- | C.CoFix (_, fl) ->
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- 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
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,ty,bo) i ->
- i &&
- guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
-