match List.nth context (n - 1) with
Some (_,C.Decl ty) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) ->
+ | Some (_,C.Def (_,ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (bo,None)) ->
- let ty,ugraph =
- (* if it is in the context it must be already well-typed*)
- CicTypeChecker.type_of_aux' ~subst metasenv context
- (S.lift n bo) ugraph
- in
- t,ty,subst,metasenv,ugraph
| None ->
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
- | C.LetIn (n,s,t) ->
- (* only to check if s is well-typed *)
- let s',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+ | C.LetIn (n,s,ty,t) ->
+ (* only to check if s is well-typed *)
+ let s',ty',subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph in
+ let ty,_,subst',metasenv',ugraph1 =
+ type_of_aux subst' metasenv' context ty ugraph1 in
+ let subst',metasenv',ugraph1 =
+ try
+ fo_unif_subst subst' context metasenv'
+ ty ty' ugraph1
+ with
+ exn ->
+ enrich localization_tbl s' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
+ context))
+ in
+ let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
let t',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),
+ C.LetIn (n,s',ty,t'),
CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,
- C.Def ((S.subst_meta l (S.lift i t)),
- Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some
+ (n,
+ C.Def
+ (S.subst_meta l (S.lift i t),
+ S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
_,None ->
l @ [None],subst,metasenv,ugraph
| Some t,Some (_,C.Def (ct,_)) ->
+ (*CSC: the following optimization is to avoid a possibly
+ expensive reduction that can be easily avoided and
+ that is quite frequent. However, this is better
+ handled using levels to control reduction *)
+ let optimized_t =
+ match t with
+ Cic.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Def (te,_)) -> S.lift n te
+ | _ -> t
+ with
+ Failure _ -> t)
+ | _ -> t
+ in
let subst',metasenv',ugraph' =
(try
(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
* il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
- fo_unif_subst subst context metasenv t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ fo_unif_subst subst context metasenv optimized_t ct ugraph
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
| Some (n, Cic.Def (bo,ty)) ->
let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' =
- match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
in
Some (n, Cic.Def (bo',ty'))
) context
(* CSC: ugly code. Here I need to retrieve in advance the loc of bo
since type_of_aux' destroys localization information (which are
preserved by type_of_aux *)
- let loc =
+ let loc exn' =
try
Cic.CicHash.find localization_tbl bo
- with Not_found -> assert false in
+ with Not_found ->
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
+ raise exn' in
let bo',boty,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] bo ugraph in
let ty',_,metasenv,ugraph =
" but is here used with type " ^
CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
in
- match exn with
- RefineFailure _ -> raise (HExtlib.Localized (loc,RefineFailure msg))
- | Uncertain _ -> raise (HExtlib.Localized (loc,Uncertain msg))
- | _ -> assert false
+ let exn' =
+ match exn with
+ RefineFailure _ -> RefineFailure msg
+ | Uncertain _ -> Uncertain msg
+ | _ -> assert false
+ in
+ raise (HExtlib.Localized (loc exn',exn'))
in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
| C.Lambda (name,so,dest) ->
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,dest) ->
- let _,ty,metasenv,ugraph =
- pack_coercions := false;
- type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
- pack_coercions := true;
- let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
- C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,ty,dest) ->
+ let ctx' = Some (name,(C.Def (so,ty)))::ctx in
+ C.LetIn
+ (name, merge_coercions ctx so, merge_coercions ctx ty,
+ merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
projects / helm.git / blobdiff