) fl true
(*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h =
+and guarded_by_constructors n nn h te =
let module C = Cic in
- function
+ (*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 te with
C.Rel m when m > n && m <= nn -> h = 1
| C.Rel _
- | C.Var _
+ | C.Var _ -> true
| C.Meta _
| C.Sort _
- | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
- | C.Cast (te,ty) ->
- guarded_by_constructors n nn h te &&
- guarded_by_constructors n nn h ty
- | C.Prod (_,so,de) ->
+ | C.Implicit
+ | C.Cast _
+ | C.Prod _
+ | C.LetIn _ ->
raise (Impossible 17) (* the term has just been type-checked *)
| C.Lambda (_,so,de) ->
does_not_occur n nn so &&
guarded_by_constructors (n + 1) (nn + 1) h de
- | C.LetIn (_,so,de) ->
- does_not_occur n nn so &&
- guarded_by_constructors (n + 1) (nn + 1) h de
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h = 1 &&
List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
| C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
- let (is_coinductive, rl) =
+ (* Invariant: we are sure that the constructor is a constructor *)
+ (* of the output inductive type of the whole co-fixpoint. *)
+ let rl =
match CicEnvironment.get_cooked_obj uri cookingsno with
C.InductiveDefinition (itl,_,_) ->
let (_,is_inductive,_,cl) = List.nth itl i in
let (_,cons,rrec_args) = List.nth cl (j - 1) in
(match !rrec_args with
None -> raise (Impossible 18)
- | Some rec_args -> (not is_inductive, rec_args)
+ | Some rec_args -> assert (not is_inductive) ; rec_args
)
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(UriManager.string_of_uri uri))
in
- is_coinductive &&
List.fold_right
(fun (x,r) i ->
i &&
if r then
+begin
+let res =
guarded_by_constructors n nn 1 x
+in
+ if not res then
+ begin
+ prerr_endline ("BECCATO: " ^ CicPp.ppterm x) ; flush stderr ; assert false
+ end ;
+ res
+end
else
does_not_occur n nn x
) (List.combine tl rl) true
+ | C.Appl ((C.CoFix (_,fl))::tl) ->
+ List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
+ let len = List.length fl in
+ let n_plus_len = n + len
+ and nn_plus_len = nn + len in
+ List.fold_right
+ (fun (_,ty,bo) i ->
+ i && does_not_occur n_plus_len nn_plus_len ty &&
+ guarded_by_constructors n_plus_len nn_plus_len h bo
+ ) fl true
+ | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
+ List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
+ does_not_occur n nn out &&
+ does_not_occur n nn te &&
+ List.fold_right
+ (fun x i -> i && guarded_by_constructors n nn h x) pl true
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n nn x) l true
- | C.Const _
+ | C.Const _ -> true
| C.Abst _
- | C.MutInd _
- | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
+ | C.MutInd _ -> assert false
+ | C.MutConstruct _ -> true
| C.MutCase (_,_,_,out,te,pl) ->
- let rec returns_a_coinductive =
- function
- (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *)
- (*CSC: effettata solo una volta, per mangiarsi l'astrazione *)
- (*CSC: non dummy *)
- C.Lambda (_,_,de) -> returns_a_coinductive de
- | C.MutInd (uri,_,i) ->
- (*CSC: definire una funzioncina per questo codice sempre replicato *)
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
- | _ ->
- raise (WrongUriToMutualInductiveDefinitions
- (UriManager.string_of_uri uri))
- )
- (*CSC: bug nella prossima riga (manca la whd) *)
- | C.Appl ((C.MutInd (uri,_,i))::_) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
- | _ ->
- raise (WrongUriToMutualInductiveDefinitions
- (UriManager.string_of_uri uri))
- )
- | _ -> false
- in
does_not_occur n nn out &&
does_not_occur n nn te &&
- if returns_a_coinductive out then
List.fold_right
(fun x i -> i && guarded_by_constructors n nn h x) pl true
- else
- List.fold_right (fun x i -> i && does_not_occur n nn x) pl true
| C.Fix (_,fl) ->
let len = List.length fl in
let n_plus_len = n + len
List.fold_right
(fun (_,ty,bo) i ->
i && does_not_occur n_plus_len nn_plus_len ty &&
- does_not_occur n_plus_len nn_plus_len bo
+ guarded_by_constructors n_plus_len nn_plus_len h bo
) fl true
and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
begin
(* let's control the guarded by constructors conditions C{f,M} *)
if not (guarded_by_constructors 0 len 0 bo) then
- raise (NotWellTyped "CoFix: not guarded by constructors")
+ raise (NotWellTyped "CoFix: not guarded by constructors") ;
+ if not (returns_a_coinductive ty) then
+ raise (NotWellTyped "CoFix: does not return a coinductive type")
end
else
raise (NotWellTyped "CoFix: ill-typed bodies")
end
| _ -> raise (NotWellTyped "Appl: wrong Prod-type")
)
+
+ and returns_a_coinductive ty =
+ let module C = Cic in
+ match CicReduction.whd ty with
+ C.MutInd (uri,_,i) ->
+ (*CSC: definire una funzioncina per questo codice sempre replicato *)
+ (match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (itl,_,_) ->
+ let (_,is_inductive,_,_) = List.nth itl i in
+ not is_inductive
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions
+ (UriManager.string_of_uri uri))
+ )
+ | C.Appl ((C.MutInd (uri,_,i))::_) ->
+ (match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (itl,_,_) ->
+ let (_,is_inductive,_,_) = List.nth itl i in
+ not is_inductive
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions
+ (UriManager.string_of_uri uri))
+ )
+ | C.Prod (_,_,de) -> returns_a_coinductive de
+ | _ -> assert false
+
in
type_of_aux env t
projects / helm.git / blobdiff