let insert_coercions = ref true
let pack_coercions = ref true
-let debug_print = fun _ -> ()
-(* let debug_print x = prerr_endline (Lazy.force x);; *)
+let debug_print = fun _ -> ();;
+(*let debug_print x = prerr_endline (Lazy.force x);;*)
let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
+ | Sys.Break -> raise exn
| _ -> assert false in
let loc =
try
| _ -> dummyres)
| _ -> dummyres
-let more_args_than_expected subst he context hetype' tlbody_and_type =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he context ^
- " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
- ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected")
+let more_args_than_expected
+ localization_tbl subst he context hetype' tlbody_and_type exn
+=
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst he context ^
+ " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^
+ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected")
+ in
+ enrich localization_tbl he ~f:(fun _-> msg) exn
;;
let mk_prod_of_metas metasenv context' subst args =
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ ->
+ Failure _ ->
enrich localization_tbl t
- (RefineFailure (lazy "Not a close term")))
+ (RefineFailure (lazy "Not a closed term")))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst'',metasenv'',ugraph2
+ C.LetIn (n,s',t'),
+ CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
debug_print
(lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
t, ty, subst, metasenv, ugraph)
- | _ -> assert false) (* the composite coercion must exist *)
+ | _ -> t, ty, subst, metasenv, ugraph)
else
t, ty, subst, metasenv, ugraph
let metasenv = pristinemenv in
debug_print (lazy
("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
- " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^
- " cause: " ^ Lazy.force s));
+ " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype'
+ (* ^ " cause: " ^ Lazy.force s *)));
let how_many_args_are_needed =
let rec aux n = function
| Cic.Prod(_,_,t) -> aux (n+1) t
metasenv context subst t tty remainder ugraph
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
- with exn -> None
- with exn -> None)
+ with Uncertain _ | RefineFailure _ -> None
+ with Uncertain _ | RefineFailure _ -> None)
candidates
with
| Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
subst,metasenv,ugraph,hetype',he,args_bo_and_ty
| None ->
- enrich localization_tbl he
- ~f:(fun _-> more_args_than_expected subst he context hetype
- args_bo_and_ty) exn
+ more_args_than_expected localization_tbl
+ subst he context hetype args_bo_and_ty exn
(* }}} end coercion to funclass stuff *)
(* }}} end fix_arity *)
in
(* aux function to process the type of the head and the args in parallel *)
let rec eat_prods_and_args
- pristinemenv metasenv subst context he hetype ugraph newargs
+ pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
=
(* {{{ body *)
function
"\nReason: " ^ Printexc.to_string exn))) exn
(* }}} end coercion stuff *)
in
- eat_prods_and_args pristinemenv metasenv subst context he
+ eat_prods_and_args pristinemenv metasenv subst context pristinehe he
(CicSubstitution.subst (fst arg) t)
ugraph1 (newargs@[arg]) tl
| _ ->
(newargs@[hete,hety]@tl) ugraph
in
eat_prods_and_args metasenv
- metasenv subst context he hetype' ugraph [] args_bo_and_ty
- with RefineFailure s | Uncertain s ->
+ metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+ with RefineFailure _ | Uncertain _ as exn ->
(* unable to fix arity *)
- let msg =
- more_args_than_expected
- subst he context hetype args_bo_and_ty
- in
- raise (RefineFailure msg)
+ more_args_than_expected localization_tbl
+ subst he context hetype args_bo_and_ty exn
(* }}} *)
in
(* first we check if we are in the simple case of a meta closed term *)
subst,metasenv,ugraph,hetype,he,args_bo_and_ty
else
(* this (says CSC) is also useful to infer dependent types *)
- fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ try
+ fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ with RefineFailure _ | Uncertain _ as exn ->
+ (* unable to fix arity *)
+ more_args_than_expected localization_tbl
+ subst he context hetype args_bo_and_ty exn
in
let coerced_args,subst,metasenv,he,t,ugraph =
eat_prods_and_args
- metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
+ metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
in
he,(List.map fst coerced_args),t,subst,metasenv,ugraph
in
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 ctx' = Some (name,(C.Def (so,None)))::ctx in
+ let _,ty,metasenv,ugraph =
+ type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+ let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in