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!*)
- let dummy_mutind =
- C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
+ (*CSC: Not very nice. *)
+ let leftno =
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
+ | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno
+ | _ -> assert false
in
- (*CSC: mettere in cicSubstitution *)
- let rec subst_inductive_type_with_dummy_mutind =
+ let dummy = Cic.Sort Cic.Prop in
+ (*CSC: to be moved in cicSubstitution? *)
+ let rec subst_inductive_type_with_dummy =
function
C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
- dummy_mutind
+ dummy
| C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
- dummy_mutind
- | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
+ let _, rargs = HExtlib.split_nth leftno tl in
+ if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
+ | C.Cast (te,ty) -> subst_inductive_type_with_dummy te
| C.Prod (name,so,ta) ->
- C.Prod (name, subst_inductive_type_with_dummy_mutind so,
- subst_inductive_type_with_dummy_mutind ta)
+ C.Prod (name, subst_inductive_type_with_dummy so,
+ subst_inductive_type_with_dummy ta)
| C.Lambda (name,so,ta) ->
- C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
- subst_inductive_type_with_dummy_mutind ta)
+ C.Lambda (name, subst_inductive_type_with_dummy so,
+ subst_inductive_type_with_dummy ta)
| C.LetIn (name,so,ty,ta) ->
- C.LetIn (name, subst_inductive_type_with_dummy_mutind so,
- subst_inductive_type_with_dummy_mutind ty,
- subst_inductive_type_with_dummy_mutind ta)
+ C.LetIn (name, subst_inductive_type_with_dummy so,
+ subst_inductive_type_with_dummy ty,
+ subst_inductive_type_with_dummy ta)
| C.Appl tl ->
- C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
+ C.Appl (List.map subst_inductive_type_with_dummy tl)
| C.MutCase (uri,i,outtype,term,pl) ->
C.MutCase (uri,i,
- subst_inductive_type_with_dummy_mutind outtype,
- subst_inductive_type_with_dummy_mutind term,
- List.map subst_inductive_type_with_dummy_mutind pl)
+ subst_inductive_type_with_dummy outtype,
+ subst_inductive_type_with_dummy term,
+ List.map subst_inductive_type_with_dummy pl)
| C.Fix (i,fl) ->
C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
- subst_inductive_type_with_dummy_mutind ty,
- subst_inductive_type_with_dummy_mutind bo)) fl)
+ subst_inductive_type_with_dummy ty,
+ subst_inductive_type_with_dummy bo)) fl)
| C.CoFix (i,fl) ->
C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
- subst_inductive_type_with_dummy_mutind ty,
- subst_inductive_type_with_dummy_mutind bo)) fl)
+ subst_inductive_type_with_dummy ty,
+ subst_inductive_type_with_dummy bo)) fl)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
List.map
- (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+ (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
exp_named_subst
in
C.Const (uri,exp_named_subst')
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map
- (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+ (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
exp_named_subst
in
C.Var (uri,exp_named_subst')
| C.MutInd (uri,typeno,exp_named_subst) ->
let exp_named_subst' =
List.map
- (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+ (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
exp_named_subst
in
C.MutInd (uri,typeno,exp_named_subst')
| C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
let exp_named_subst' =
List.map
- (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+ (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
exp_named_subst
in
C.MutConstruct (uri,typeno,consno,exp_named_subst')
| t -> t
in
- match CicReduction.whd context te with
-(*
- C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
-*)
- C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
- | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> 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
- (subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | C.Prod (name,source,dest) ->
- does_not_occur context n nn
- (subst_inductive_type_with_dummy_mutind source)&&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | _ ->
- raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ (* 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) ->
+ List.for_all (does_not_occur context n nn) tl
+ | C.Sort C.Prop -> 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 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 &&
+ aux ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) dest
+ | _ ->
+ raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ in
+ aux context n nn (subst_inductive_type_with_dummy te)
(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
| (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
with
Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2)
| Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2)
- | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) ->
- CicUniv.add_ge u2 u1 ugraph
+ | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2)
| Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) ->
- CicUniv.add_gt u2 u1 ugraph
+ CicUniv.add_ge u2 u1 ugraph
| Cic.Sort _, Cic.Sort Cic.Prop
| Cic.Sort _, Cic.Sort Cic.CProp _
| Cic.Sort _, Cic.Sort Cic.Set
(are_all_occurrences_positive context uri indparamsno
(i+indparamsno) indparamsno (len+indparamsno) te)
then
- begin
- prerr_endline (UriManager.string_of_uri uri);
- prerr_endline (string_of_int (List.length tys));
raise
(TypeCheckerFailure
- (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end
+ (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
else
ugraph
) ugraph cl in
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
let ty',ugraph1 = type_of_aux ~logger context s ugraph in
let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+ R.are_convertible ~subst ~metasenv context ty' ty ugraph1
in
if not b then
raise
| (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
(* different from Coq manual!!! *)
t2',ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
(try
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
C.Sort (C.Type t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) ->
let t' = CicUniv.fresh() in
(try
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
C.Sort (C.CProp t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph
| (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph
| (C.Meta _, C.Sort _) -> t2',ugraph
check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
;;
-let typecheck uri =
+let typecheck ?(trust=true) uri =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let logger = new CicLogger.logger in
- match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
| CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
(* let's typecheck the uncooked object *)
let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
logger#log (`Type_checking_completed uri);
- match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
| CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| _ -> raise CicEnvironmentError
;;
projects / helm.git / blobdiff