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
| sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
let sib2,head = last_of tl2 in
true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
- (c2::sib2@[Cic.Implicit None])])
+ (c2::sib2@[imp])])
| _ -> dummyres)
| _ -> dummyres
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module U = UriManager in
let try_coercion t subst metasenv context ugraph coercion_tgt c =
- let coerced = Cic.Appl[c;t] in
+ let coerced = C.Appl[c;t] in
try
let newt,_,subst,metasenv,ugraph =
type_of_aux subst metasenv context coerced ugraph
with
| RefineFailure _ | Uncertain _ -> None
in
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
let (t',_,_,_,_) as res =
match t with
(* function *)
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
| Some t,Some (_,C.Def (ct,_)) ->
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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
(CicPp.ppterm t2''))))
and avoid_double_coercion context subst metasenv ugraph t ty =
+ if not !pack_coercions then
+ t,ty,subst,metasenv,ugraph
+ else
let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
if b then
let source_carr = CoercGraph.source_of c2 in
| RefineFailure s | Uncertain s ->
debug_print s;debug_print (lazy "goon\n");
try
+ let old_pack_coercions = !pack_coercions in
pack_coercions := false; (* to avoid diverging *)
let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
type_of_aux subst metasenv context c1_c2_implicit ugraph
in
- pack_coercions := true;
+ pack_coercions := old_pack_coercions;
let b, _, _, _, _ =
is_a_double_coercion refined_c1_c2_implicit
in
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context ^
- "\nReason: " ^ Printexc.to_string exn))) exn
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Printexc.to_string exn*)))) exn
(* }}} end coercion stuff *)
in
eat_prods_and_args pristinemenv metasenv subst context pristinehe he
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
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 =
+ pack_coercions := false;
+ type_of_aux' metasenv ctx so CicUniv.empty_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.Appl l ->
let l = List.map (merge_coercions ctx) l in
try
type_of_aux' metasenv ctx t ugraph
with RefineFailure _ | Uncertain _ ->
- prerr_endline (CicPp.ppterm t);
t, t, [], ugraph
in
insert_coercions := old_insert_coercions;