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 imp = Cic.Implicit None in
let dummyres = false,imp, imp,imp,imp in
match t with
- | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
+ | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
(match last_of tl with
- | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
let sib2,head = last_of tl2 in
true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
(c2::sib2@[imp])])
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 =
- match c with
- C.Appl l2 -> C.Appl (l2@[t])
- | _ -> C.Appl [c;t]
+ 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
in
try
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context coerced ugraph
- in
let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
+ avoid_double_coercion context subst metasenv ugraph coerced
+ coercion_tgt
in
Some (newt, tty, subst, metasenv, ugraph)
with
exn ->
enrich localization_tbl te'
~f:(fun _ ->
- lazy ("The term " ^
+ lazy ("(3)The term " ^
CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
| term ->
let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
let boh =
- CoercGraph.look_for_coercion coercion_src coercion_tgt
+ CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
in
(match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl t
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(4)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.NotMetaClosed ->
enrich localization_tbl t
(Uncertain
- (lazy ("The term " ^
+ (lazy ("(5)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (try_coercion
- t subst metasenv context ugraph coercion_tgt)
+ (try_coercion t subst context ugraph coercion_tgt)
candidates
in
match selected with
| None ->
enrich localization_tbl t
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(6)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv
subst t context ^
" is not a type since it has type " ^
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
let s',sort1,subst',metasenv',ugraph1 =
| coercion_src ->
let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
let boh =
- CoercGraph.look_for_coercion coercion_src coercion_tgt
+ CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
in
match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(7)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.NotMetaClosed ->
enrich localization_tbl s'
(Uncertain
- (lazy ("The term " ^
+ (lazy ("(8)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (try_coercion
- s' subst' metasenv' context ugraph1 coercion_tgt)
- candidates
+ (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 " ^
+ (lazy ("(9)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
expected_type' actual_type ugraph2
with
exn ->
+ prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
+ prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
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.
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
if b then
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
+ (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
with
| CoercGraph.SomeCoercion candidates ->
- let selected =
+ let selected =
HExtlib.list_findopt
- (function
+ (function (metasenv,last,c) ->
+ match c with
| c when not (CoercGraph.is_composite c) ->
debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
None
| c ->
- let newt =
- match c with
- | Cic.Appl l -> Cic.Appl (l @ [head])
- | _ -> Cic.Appl [c;head]
- in
- debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last head ugraph in
+ debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
(try
debug_print
(lazy
("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
+ type_of_aux subst metasenv context c ugraph in
debug_print (lazy "tipa...");
let subst, metasenv, ugraph =
(* COME MAI C'ERA UN IF su !pack_coercions ??? *)
he
in
let x,xty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context x ugraph
+ (*CSC: here unsharing is necessary to avoid an unwanted
+ relocalization. However, this also shows a great source of
+ inefficiency: "x" is refined twice (once now and once in the
+ subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
+ *)
+ type_of_aux subst metasenv context (Unshare.unshare x) ugraph
in
let carr_src =
CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
in
let carr_tgt = CoercDb.Fun 0 in
- match CoercGraph.look_for_coercion' carr_src carr_tgt with
+ match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
| CoercGraph.NoCoercion
| CoercGraph.NotMetaClosed
| CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
match
HExtlib.list_findopt
- (fun coerc ->
- let t = Cic.Appl [coerc;x] in
- debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t));
+ (fun (metasenv,last,coerc) ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last x ugraph in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
try
(* we want this to be available in the error handler fo the
* following (so it has its own try. *)
let t,tty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context t ugraph
+ type_of_aux subst metasenv context coerc ugraph
in
try
let metasenv, hetype' =
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
with Uncertain _ | RefineFailure _ -> None
- with Uncertain _ | RefineFailure _ -> None
- | exn -> assert false) (* ritornare None, e' un localized *)
+ with
+ Uncertain _
+ | RefineFailure _
+ | HExtlib.Localized (_,Uncertain _)
+ | HExtlib.Localized (_,RefineFailure _) -> None
+ | exn -> assert false) (* ritornare None, e' un localized *)
candidates
with
| Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
in
let c_hety = carr hety subst context in
let c_s = carr s subst context in
- CoercGraph.look_for_coercion c_hety c_s, c_s
+ CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
in
(match coer with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl hete exn
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(15)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| CoercGraph.NotMetaClosed ->
enrich localization_tbl hete exn
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(16)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (fun c ->
+ (fun (metasenv,last,c) ->
try
- let t = Cic.Appl[c;hete] in
+ 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
- t ugraph
+ c ugraph
in
let newt, newty, subst, metasenv, ugraph =
avoid_double_coercion context subst metasenv
| None ->
enrich localization_tbl hete
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(1)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| 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
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
| C.LetIn (name,so,dest) ->
let _,ty,metasenv,ugraph =
pack_coercions := false;
- type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+ type_of_aux' metasenv ctx so CicUniv.oblivion_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)
let b,_,_,_,_ = is_a_double_coercion t in
(* prerr_endline "CANDIDATO!!!!"; *)
if b then
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
let old_insert_coercions = !insert_coercions in
insert_coercions := false;
let newt, _, menv, _ =
projects / helm.git / blobdiff