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])])
| _ -> dummyres
let more_args_than_expected
- localization_tbl subst he context hetype' tlbody_and_type exn
+ localization_tbl metasenv 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 ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
+ " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
" arguments that are more than expected")
in
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
enrich localization_tbl te'
~f:(fun _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst'' te'
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst'' inferredty
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
+ 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
| 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
enrich localization_tbl t
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst t context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ 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 subst t context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ 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 metasenv context ugraph coercion_tgt)
+ (try_coercion t subst context ugraph coercion_tgt)
candidates
in
match selected with
enrich localization_tbl t
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^
" that is not a sort"))))
in
| 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
enrich localization_tbl s'
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ 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 subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ 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' metasenv' context ugraph1 coercion_tgt)
- candidates
+ (try_coercion s' subst' context ugraph1 coercion_tgt)
+ candidates
in
match selected with
| Some x -> x
enrich localization_tbl s'
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^
" that is not a sort")))
in
enrich localization_tbl term' exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst term'
+ CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst actual_type
+ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_type' context))
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
in
let rec instantiate_prod t =
function
enrich localization_tbl p exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst p
+ CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst instance'
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance'
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst instance
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance
context)))
(subst,metasenv,ugraph5) pl' outtypeinstances
in
enrich localization_tbl bo exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst ty_of_bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_ty
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
context))
in
fl @ [bo'] , subst',metasenv',ugraph'
enrich localization_tbl bo exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst ty_of_bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_ty
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
context))
in
fl @ [bo'],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))))))
+ 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
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
(try
fo_unif_subst
subst' context metasenv' inferredty ct ugraph1
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t'], subst'',metasenv'',ugraph2
| None, Some _ ->
- raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
+ raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
with
Invalid_argument _ ->
raise
(RefineFailure
(lazy (sprintf
"Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext subst canonical_context))))
+ (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
and check_exp_named_subst metasubst metasenv context tl ugraph =
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
with _ ->
raise (RefineFailure (lazy
("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasubst' typeoft ^
+ CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
" not unifiable with " ^
- CicMetaSubst.ppterm metasubst' typeofvar)))
+ CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
in
(* FIXME: no mere tail recursive! *)
let exp_name_subst, metasubst''', metasenv''', ugraph4 =
(lazy
(sprintf
"%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context subst t context)
- (CicMetaSubst.ppterm_in_context subst t2 context))))
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
| _,_ ->
enrich localization_tbl t
(RefineFailure
(lazy
(sprintf
"%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context subst s context)
- (CicMetaSubst.ppterm_in_context subst t1 context))))
+ (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
and avoid_double_coercion context subst metasenv ugraph t ty =
if not !pack_coercions then
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 ??? *)
(* {{{ we search a coercion of the head (saturated) to funclass *)
let metasenv = pristinemenv in
debug_print (lazy
- ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
- " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype'
+ ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
+ " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
(* ^ " cause: " ^ Lazy.force s *)));
let how_many_args_are_needed =
let rec aux n = function
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.SomeCoercion candidates ->
match
HExtlib.list_findopt
- (fun coerc ->
- let t = Cic.Appl [coerc;x] in
- debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm 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' =
mk_prod_of_metas metasenv context subst remainder
in
debug_print (lazy
- (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
- CicMetaSubst.ppterm subst hetype'));
+ (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
+ CicMetaSubst.ppterm ~metasenv subst hetype'));
let subst,metasenv,ugraph =
fo_unif_subst_eat_prods
subst context metasenv tty hetype' ugraph
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
with Uncertain _ | RefineFailure _ -> None
- with Uncertain _ | RefineFailure _ -> None)
+ 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)->
subst,metasenv,ugraph,hetype',he,args_bo_and_ty
| None ->
- more_args_than_expected localization_tbl
+ more_args_than_expected localization_tbl metasenv
subst he context hetype args_bo_and_ty exn
(* }}} end coercion to funclass stuff *)
(* }}} end fix_arity *)
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
enrich localization_tbl hete exn
~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ 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 subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Lazy.force e*))))
| 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
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Lazy.force e*)))) exn))
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Printexc.to_string exn*)))) exn
(* }}} end coercion stuff *)
in
metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
with RefineFailure _ | Uncertain _ as exn ->
(* unable to fix arity *)
- more_args_than_expected localization_tbl
+ more_args_than_expected localization_tbl metasenv
subst he context hetype args_bo_and_ty exn
(* }}} *)
in
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
+ more_args_than_expected localization_tbl metasenv
subst he context hetype args_bo_and_ty exn
in
let coerced_args,subst,metasenv,he,t,ugraph =
projects / helm.git / blobdiff