and does_not_occur ?(subst=[]) context n nn te =
let module C = Cic in
- (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
- (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
- (*CSC: universi *)
- match CicReduction.whd ~subst context te with
+ match te with
C.Rel m when m > n && m <= nn -> false
- | C.Rel _
+ | C.Rel m ->
+ (try
+ (match List.nth context (m-1) with
+ Some (_,C.Def (bo,_)) ->
+ does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
+ | _ -> true)
+ with
+ Failure _ -> assert false)
| C.Sort _
| C.Implicit _ -> true
| C.Meta (_,l) ->
(fun x i ->
match x with
None -> i
- | Some x -> i && does_not_occur ~subst context n nn x) l true
+ | Some x -> i && does_not_occur ~subst context n nn x) l true &&
+ (try
+ let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+ does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
+ with
+ CicUtil.Subst_not_found _ -> true)
| C.Cast (te,ty) ->
does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
| C.Prod (name,so,dest) ->
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonymous,so,type_of_branch ~subst
+ C.Prod (name,so,type_of_branch ~subst
((Some (name,(C.Decl so)))::context) argsno need_dummy
(CicSubstitution.lift 1 outtype) term' de)
- | _ -> raise (AssertFailure (lazy "20"))
+ | _ -> raise (AssertFailure (lazy "20"))
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
| None -> raise
(TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
with
- _ ->
+ Failure _ ->
raise (TypeCheckerFailure (lazy "unbound variable"))
)
| C.Var (uri,exp_named_subst) ->
type_of_aux ~logger
((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
in
- (CicSubstitution.subst s ty1),ugraph2
+ (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
let tlbody_and_type,ugraph2 =
R.are_convertible
~subst ~metasenv context ty_p ty_branch ugraph3
in
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
if not b1 then
debug_print (lazy
("#### " ^ CicPp.ppterm ty_p ^
begin
CicReduction.fdebug := -1 ;
eat_prods ~subst context
- (CicSubstitution.subst hete t) tl ugraph1
+ (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+ tl ugraph1
(*TASSI: not sure *)
end
else
(** wrappers which instantiate fresh loggers *)
+let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
+
let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
- type_of_aux' ~logger ~subst metasenv context t ugraph
+ profiler.HExtlib.profile
+ (type_of_aux' ~logger ~subst metasenv context t) ugraph
let typecheck_obj uri obj =
let logger = new CicLogger.logger in