match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
+ | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
| Sys.Break -> raise exn
- | _ -> assert false in
+ | _ -> prerr_endline (Printexc.to_string exn); assert false
+ in
let loc =
try
Cic.CicHash.find localization_tbl t
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
+(*
let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv last t ugraph
with
| RefineFailure _ | Uncertain _ -> None
in
+*)
let (t',_,_,_,_) as res =
match t with
(* function *)
inferredty ty' ugraph2
in
C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- exn ->
- enrich localization_tbl te'
- ~f:(fun _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
- )
- | C.Prod (name,s,t) ->
- let carr t subst context = CicMetaSubst.apply_subst subst t in
- let coerce_to_sort in_source tgt_sort t type_to_coerce
- subst context metasenv uragph
- =
- if not !insert_coercions then
- t,type_to_coerce,subst,metasenv,ugraph
- else
- let coercion_src = carr type_to_coerce subst context in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- t, cast, subst, metasenv, ugraph
- | term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
- let boh =
- CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
+ with
+ | Uncertain _ | RefineFailure _ ->
+ let exn =
+ RefineFailure (lazy ("(3)The term " ^
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context metasenv''
+ subst'' inferredty context ^
+ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context
+ metasenv'' subst'' ty' context))
+ in
+ try
+ let (te, ty), subst, metasenv, ugraph =
+ coerce_to_something te' inferredty ty'
+ subst'' metasenv'' context exn ugraph2
in
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl t
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (try_coercion t subst context ugraph coercion_tgt)
- candidates
- in
- match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^
- " that is not a sort"))))
- in
+ C.Cast (te, ty'), ty', subst, metasenv, ugraph
+ with exn -> enrich localization_tbl te' exn)
+ | C.Prod (name,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
in
C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
-
let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
+ type_of_aux subst metasenv context s ugraph
+ in
let s',sort1,subst',metasenv',ugraph1 =
- if not !insert_coercions then
- s',sort1, subst', metasenv', ugraph1
- else
- match CicReduction.whd ~subst:subst' context sort1 with
- | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
- | coercion_src ->
- let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- let boh =
- CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
- in
- match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl s'
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl s'
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (try_coercion s' subst' context ugraph1 coercion_tgt)
- candidates
- in
- match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl s'
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^
- " that is not a sort")))
+ coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(10)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
(* TODO: check if the sort elimination
* is allowed: [(I q1 ... qr)|B] *)
let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- List.fold_left
- (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+ List.fold_right
+ (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
let constructor =
if left_args = [] then
(C.MutConstruct (uri,i,j,exp_named_subst))
type_of_aux subst metasenv context constructor ugraph1
in
let outtypeinstance,subst,metasenv,ugraph3 =
- check_branch 0 context metasenv subst no_left_params
- actual_type constructor' expected_type ugraph2
+ try
+ check_branch 0 context metasenv subst
+ no_left_params actual_type constructor' expected_type
+ ugraph2
+ with
+ exn ->
+ enrich localization_tbl constructor'
+ ~f:(fun _ ->
+ lazy ("(11)The term " ^
+ CicMetaSubst.ppterm_in_context metasenv subst p'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context metasenv subst actual_type
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context metasenv subst expected_type
+ context)) exn
in
- (pl @ [p'],j+1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- ([],1,[],subst,metasenv,ugraph3) pl
+ (p'::pl,j-1,
+ outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+ pl ([],List.length pl,[],subst,metasenv,ugraph3)
in
(* we are left to check that the outype matches his instances.
candidate_oty,ugraph,metasenv,subst
with
CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | RefineFailure _ | Uncertain _ ->
None,ugraph,metasenv,subst
) (Some instance',ugraph4,metasenv,subst) tl
in
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(12)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
(C.Appl(outtype::right_args@[term]))),
subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1,len =
List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+ (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
in
fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl ty')) :: types, ugraph
- ) ([],subst,metasenv,[],ugraph) fl
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
+ :: types, ugraph, len+1
+ ) ([],subst,metasenv,[],ugraph,0) fl
in
- let len = List.length types in
let context' = types@context in
let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(13)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
in
C.Fix (i,fl''),ty,subst,metasenv,ugraph2
| C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1,len =
List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+ (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
in
fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl ty')) :: types, ugraph1
- ) ([],subst,metasenv,[],ugraph) fl
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
+ types, ugraph1, len+1
+ ) ([],subst,metasenv,[],ugraph,0) fl
in
- let len = List.length types in
let context' = types@context in
let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(14)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
| CoercGraph.NoCoercion
| CoercGraph.NotMetaClosed
| CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
match
HExtlib.list_findopt
debug_print (lazy " success!");
Some (subst,metasenv,ugraph,tty,t,remainder)
with
- | Uncertain _ | RefineFailure _
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | Uncertain _ | RefineFailure _ ->
try
let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
fix_arity
match (CicReduction.whd ~subst context hetype) with
| Cic.Prod (n,s,t) ->
let arg,subst,metasenv,ugraph1 =
- try
+ try
+ (try
let subst,metasenv,ugraph1 =
fo_unif_subst_eat_prods2
subst context metasenv hety s ugraph
in
(hete,hety),subst,metasenv,ugraph1
- (* {{{ we search a coercion from hety to s if fails *)
with RefineFailure _ | Uncertain _ as exn
when allow_coercions && !insert_coercions ->
- let coer, tgt_carr =
- let carr t subst context =
- CicReduction.whd ~delta:false
- context (CicMetaSubst.apply_subst subst t )
- in
- let c_hety = carr hety subst context in
- let c_s = carr s subst context in
- CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
- in
- (match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl hete exn
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete exn
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (fun (metasenv,last,c) ->
- try
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last hete
- ugraph in
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- c ugraph
- in
- let newt, newty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv
- ugraph newt tgt_carr
- in
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- Some ((newt,newty), subst, metasenv, ugraph)
- with Uncertain _ | RefineFailure _ -> None)
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn))
- | exn ->
+ coerce_to_something
+ hete hety s subst metasenv context exn ugraph)
+ with exn ->
enrich localization_tbl hete
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(2)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s context
+ CicMetaSubst.ppterm_in_context
+ ~metasenv subst s context
(* "\nReason: " ^ Printexc.to_string exn*)))) exn
- (* }}} end coercion stuff *)
in
eat_prods_and_args pristinemenv metasenv subst context pristinehe he
(CicSubstitution.subst (fst arg) t)
metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
in
he,(List.map fst coerced_args),t,subst,metasenv,ugraph
+
+ and coerce_to_something t infty expty subst metasenv context exn ugraph =
+ if not !insert_coercions then
+ raise exn
+ else
+ let clean t subst context =
+ CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
+ in
+ let infty = clean infty subst context in
+ let expty = clean expty subst context in
+ match infty, expty with
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
+ (* covariant part *)
+ let name_con = Cic.Name "name_con" in
+ let name_t, ty_s_bo, bo =
+ match t with
+ | Cic.Lambda (name, src, bo) -> name, src, bo
+ | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
+ in
+ let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+ let (bo, _), subst, metasenv, ugraph =
+ coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
+ in
+ (* contravariant part *)
+ let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
+ (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn
+ ugraph
+ in
+ let coerced =
+ Cic.Lambda (name_t,src2,
+ CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+ in
+ (coerced, expty), subst, metasenv, ugraph
+ | _ ->
+ coerce_atom_to_something t infty expty subst metasenv context exn ugraph
+
+ and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
+ let coer =
+ CoercGraph.look_for_coercion metasenv subst context infty expty
+ in
+ match coer with
+ | CoercGraph.NotMetaClosed ->
+ (match exn with
+ | RefineFailure s -> raise (Uncertain s)
+ | HExtlib.Localized _ -> assert false
+ | _ -> raise exn)
+ | CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
+ | CoercGraph.NotHandled _ ->
+ raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun (metasenv,last,c) ->
+ try
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last t
+ ugraph in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ c ugraph
+ in
+ let newt, newty, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv
+ ugraph newt expty
+ in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety expty ugraph
+ in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None -> raise exn
+
+ and coerce_to_sort
+ in_source tgt_sort t type_to_coerce subst context metasenv uragph =
+ match CicReduction.whd ~subst:subst context type_to_coerce with
+ | Cic.Meta _ | Cic.Sort _ ->
+ t,type_to_coerce, subst, metasenv, ugraph
+ | src ->
+ let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ let exn =
+ RefineFailure (lazy ("(7)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context
+ ^ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst src context
+ ^ " that is not a sort"))
+ in
+ try
+ let (t, ty_t), subst, metasenv, ugraph =
+ coerce_to_something t src tgt
+ subst metasenv context exn ugraph
+ in
+ t, ty_t, subst, metasenv, ugraph
+ with exn -> enrich localization_tbl t exn
in
(* eat prods ends here! *)
let con_context =
List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
(* second phase: we fix only the constructors *)
+ let saved_menv = metasenv in
let metasenv,ugraph,tys =
List.fold_right
(fun (name,b,ty,cl) (metasenv,ugraph,res) ->
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
- metasenv,ugraph,(name,ty')::res
+ metasenv@saved_menv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in
metasenv,ugraph,(name,b,ty,cl')::res
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
let b,_,_,_,_ = is_a_double_coercion t in
- (* prerr_endline "CANDIDATO!!!!"; *)
if b then
let ugraph = CicUniv.oblivion_ugraph in
let old_insert_coercions = !insert_coercions in