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? *)
- non_informative &&
- does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
- (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph
+ non_informative, ugraph
else
false,ugraph
| _ ->
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
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
;;