exception CicEnvironmentError;;
+let check_homogeneous_call context indparamsno n uri reduct tl =
+ let last =
+ List.fold_left
+ (fun k x ->
+ if k = 0 then 0
+ else
+ match CicReduction.whd context x with
+ | Cic.Rel m when m = n - (indparamsno - k) -> k - 1
+ | _ -> raise (TypeCheckerFailure (lazy
+ ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+ string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+ "appl:\n"^ CicPp.ppterm reduct))))
+ indparamsno tl
+ in
+ if last <> 0 then
+ raise (TypeCheckerFailure
+ (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+ UriManager.string_of_uri uri)))
+;;
+
+
let rec type_of_constant ~logger uri orig_ugraph =
let module C = Cic in
let module R = CicReduction in
does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
) fl true
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
-(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
-(*CSC strictly_positive *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
-and weakly_positive context n nn uri te =
+(* Inductive types being checked for positivity have *)
+(* indexes x s.t. n < x <= nn. *)
+and weakly_positive context n nn uri indparamsno posuri te =
let module C = Cic in
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+ (*CSC: Not very nice. *)
let leftno =
match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno
| _ -> assert false
in
let dummy = Cic.Sort Cic.Prop in
- (*CSC: mettere in cicSubstitution *)
+ (*CSC: to be moved in cicSubstitution? *)
let rec subst_inductive_type_with_dummy =
function
C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
C.MutConstruct (uri,typeno,consno,exp_named_subst')
| t -> t
in
+ (* this function has the same semantics of are_all_occurrences_positive
+ but the i-th context entry role is played by dummy and some checks
+ are skipped because we already know that are_all_occurrences_positive
+ of uri in te. *)
let rec aux context n nn te =
match CicReduction.whd context te with
| C.Appl (C.Sort C.Prop::tl) ->
| C.Prod (name,source,dest) when
does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
(* dummy abstraction, so we behave as in the anonimous case *)
- strictly_positive context n nn source &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
+ strictly_positive context n nn indparamsno posuri source &&
+ aux ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) dest
| C.Prod (name,source,dest) ->
does_not_occur context n nn source &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
+ aux ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) dest
| _ ->
raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
in
| (C.Cast (te,_), _) -> instantiate_parameters params te
| (t,l) -> raise (AssertFailure (lazy "1"))
-and strictly_positive context n nn te =
+and strictly_positive context n nn indparamsno posuri te =
let module C = Cic in
let module U = UriManager in
match CicReduction.whd context te with
| t when does_not_occur context n nn t -> true
- | C.Rel _ -> true
+ | C.Rel _ when indparamsno = 0 -> true
| C.Cast (te,ty) ->
(*CSC: bisogna controllare ty????*)
- strictly_positive context n nn te
+ strictly_positive context n nn indparamsno posuri te
| C.Prod (name,so,ta) ->
does_not_occur context n nn so &&
- strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
- | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
+ strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
+ indparamsno posuri ta
+ | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
+ check_homogeneous_call context indparamsno n posuri reduct tl;
List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
| C.Appl ((C.MutInd (uri,i,exp_named_subst))::_)
| (C.MutInd (uri,i,exp_named_subst)) as t ->
(fun x i ->
i &&
weakly_positive
- ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
- x
+ ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+ indparamsno posuri x
) cl' true
| t -> false
and are_all_occurrences_positive context uri indparamsno i n nn te =
let module C = Cic in
match CicReduction.whd context te with
- C.Appl ((C.Rel m)::tl) when m = i ->
- (*CSC: riscrivere fermandosi a 0 *)
- (* let's check if the inductive type is applied at least to *)
- (* indparamsno parameters *)
- let last =
- List.fold_left
- (fun k x ->
- if k = 0 then 0
- else
- match CicReduction.whd context x with
- C.Rel m when m = n - (indparamsno - k) -> k - 1
- | _ ->
- raise (TypeCheckerFailure
- (lazy
- ("Non-positive occurence in mutual inductive definition(s) [1]" ^
- UriManager.string_of_uri uri)))
- ) indparamsno tl
- in
- if last = 0 then
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
- else
- raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
- UriManager.string_of_uri uri)))
+ C.Appl ((C.Rel m)::tl) as reduct when m = i ->
+ check_homogeneous_call context indparamsno n uri reduct tl;
+ List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
| C.Rel m when m = i ->
if indparamsno = 0 then
true
| C.Prod (name,source,dest) when
does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
(* dummy abstraction, so we behave as in the anonimous case *)
- strictly_positive context n nn source &&
+ strictly_positive context n nn indparamsno uri source &&
are_all_occurrences_positive
((Some (name,(C.Decl source)))::context) uri indparamsno
(i+1) (n + 1) (nn + 1) dest
in
aux
+and is_non_recursive ctx paramsno t uri =
+ let t = debrujin_constructor uri 1 [] t in
+(* let ctx, t = split_prods ~subst:[] ctx paramsno t in *)
+ let len = List.length ctx in
+ let rec aux ctx n nn t =
+ match CicReduction.whd ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ does_not_occur ctx n nn src &&
+ aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt
+ | (Cic.Rel k)
+ | Cic.Appl (Cic.Rel k :: _) when k = nn -> true
+ | t -> assert false
+ in
+ aux ctx (len-1) len t
+
and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
need_dummy ind arity1 arity2 ugraph =
let module C = Cic in
let non_informative,ugraph =
if cl_len = 0 then true,ugraph
else
- is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
- paramsno (snd (List.nth cl 0)) ugraph
+ let b, ug =
+ is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
+ paramsno (snd (List.nth cl 0)) ugraph
+ in
+ b &&
+ is_non_recursive [Some (C.Name name,C.Decl ty)]
+ paramsno (snd (List.nth cl 0)) uri, ug
in
(* is it a singleton or empty non recursive and non informative
definition? *)
let module R = CicReduction in
let module S = CicSubstitution in
let module U = UriManager in
+(* FG: DEBUG ONLY
+ prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+ prerr_endline ("TC: term :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)
match t with
C.Rel n ->
(try
projects / helm.git / blobdiff