try
Cic.CicHash.find localization_tbl t
with Not_found ->
- prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
raise exn'
in
raise (HExtlib.Localized (loc,exn'))
enrich localization_tbl he ~f:(fun _-> msg) exn
;;
-let mk_prod_of_metas metasenv context' subst args =
+let mk_prod_of_metas metasenv context subst args =
let rec mk_prod metasenv context' = function
| [] ->
let (metasenv, idx) =
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in context'. *)
let name_hint =
- (* Cic.Name "pippo" *)
FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context')
+ (CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
~typ:(CicMetaSubst.apply_subst subst argty)
in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name ~subst
[] context' name_hint ~typ:(Cic.Sort Cic.Prop)
in
in
metasenv,Cic.Prod (name,meta,target)
in
- mk_prod metasenv context' args
+ mk_prod metasenv context args
;;
let rec type_of_constant uri ugraph =
(lazy ("Unkown mutual inductive definition " ^
U.string_of_uri uri)))
in
+ if List.length constructors <> List.length pl then
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy "Wrong number of cases")) ;
let rec count_prod t =
match CicReduction.whd ~subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("(10)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
exn ->
enrich localization_tbl constructor'
~f:(fun _ ->
- lazy ("(11)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context metasenv subst p'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv subst actual_type
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("(12)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(13)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(14)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
| 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.");
+(*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))))))
in
(* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
" <==> " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
+ "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+ context));
debug_print (lazy ("FO_UNIF_SUBST: " ^
CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv infty expty ugraph
in
(t, expty), subst, metasenv, ugraph
- with Uncertain _ | RefineFailure _ as exn ->
- if not allow_coercions || not !insert_coercions then
- enrich localization_tbl t exn
- else
+ with (Uncertain _ | RefineFailure _ as exn)
+ when allow_coercions && !insert_coercions ->
let whd = CicReduction.whd ~delta:false in
let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
let infty = clean infty subst context in