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
-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 =
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
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
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 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 =
+ 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;
projects / helm.git / blobdiff