let debug_print = fun _ -> ()
+let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
+
+let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
+ try
+let foo () =
+ CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods2.HExtlib.profile foo ()
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
+let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
+
+let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
+ try
+let foo () =
+ CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods.HExtlib.profile foo ()
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
let profiler = HExtlib.profile "CicRefine.fo_unif"
let fo_unif_subst subst context metasenv t1 t2 ugraph =
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
+ let try_coercion t subst metasenv context ugraph coercion_tgt c =
+ let coerced = Cic.Appl[c;t] 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
+ in
+ Some (newt, tty, subst, metasenv, ugraph)
+ with
+ | RefineFailure _ | Uncertain _ -> None
+ in
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context
subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion c ->
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context (Cic.Appl[c;t])
- ugraph in
- let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph
- newt coercion_tgt
- in
- newt, tty, subst, metasenv, ugraph)
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (try_coercion
+ t subst metasenv 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
+ subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^
+ " that is not a sort"))))
in
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
CoercGraph.look_for_coercion coercion_src coercion_tgt
in
match boh with
- | CoercGraph.SomeCoercion c ->
- let newt,_,subst',metasenv',ugraph1 =
- type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
- ugraph1 in
- let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion context subst' metasenv'
- ugraph1 newt coercion_tgt
- in
- newt, tty, subst', metasenv', ugraph1
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context
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
+ in
+ match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl s'
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^
+ " that is not a sort")))
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
in
let tl',applty,subst''',metasenv''',ugraph3 =
eat_prods true subst'' metasenv'' context
- he hetype tlbody_and_type ugraph2
+ he' hetype tlbody_and_type ugraph2
in
avoid_double_coercion context
subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
let tgt_carr = CicMetaSubst.apply_subst subst ty in
(match CoercGraph.look_for_coercion source_carr tgt_carr
with
- | CoercGraph.SomeCoercion c ->
- let newt =
- match c with
- Cic.Appl l -> Cic.Appl (l @ [head])
- | _ -> Cic.Appl [c;head]
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ let newt =
+ match c with
+ | Cic.Appl l -> Cic.Appl (l @ [head])
+ | _ -> Cic.Appl [c;head]
+ in
+ (try
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ Some (newt, ty, subst, metasenv, ugraph)
+ with RefineFailure _ | Uncertain _ -> None))
+ candidates
in
- (try
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv newt t ugraph
- in
- debug_print
- (lazy
- ("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
- newt, ty, subst, metasenv, ugraph
- with
- RefineFailure _ ->
- prerr_endline ("#### Coercion not packed (Refine_failure): " ^
- CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
- assert false
- | Uncertain _ ->
- prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
- CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+ (match selected with
+ | Some x -> x
+ | None ->
+ prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
assert false)
| _ -> assert false) (* the composite coercion must exist *)
else
in
metasenv,Cic.Prod (name,meta,target)
in
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv,ugraph1) =
- try
- fo_unif_subst subst context metasenv hetype hetype' ugraph
- with exn ->
- enrich localization_tbl he
- ~f:(fun _ ->
- (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"
- (* "\nReason: " ^ Lazy.force exn*)))) exn
+ let ((subst,metasenv,ugraph1),hetype') =
+ if CicUtil.is_meta_closed hetype then
+ (subst,metasenv,ugraph),hetype
+ else
+ let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+ try
+ fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
+ with exn ->
+ enrich localization_tbl he
+ ~f:(fun _ ->
+ (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"
+ (* "\nReason: " ^ Lazy.force exn*)))) exn
in
let rec eat_prods metasenv subst context hetype ugraph =
function
| [] -> [],metasenv,subst,hetype,ugraph
| (hete, hety)::tl ->
- (match hetype with
+ (match (CicReduction.whd ~subst context hetype) with
Cic.Prod (n,s,t) ->
let arg,subst,metasenv,ugraph1 =
try
let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv hety s ugraph
+ fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
with exn when allow_coercions && !insert_coercions ->
(* we search a coercion from hety to s *)
let coer, tgt_carr =
let carr t subst context =
- CicMetaSubst.apply_subst subst t
+ 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
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion c ->
- try
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- (Cic.Appl[c;hete]) ugraph in
- let newt, _, 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
- newt, subst, metasenv, ugraph
- with _ ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("The term " ^
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ try
+ let t = Cic.Appl[c;hete] in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ t ugraph
+ in
+ let newt, _, 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, 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 subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn)
+ (* "\nReason: " ^ Lazy.force e*)))) exn))
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
(CicSubstitution.subst arg t) ugraph1 tl
in
arg::coerced_args,metasenv',subst',t',ugraph2
- | _ -> assert false
- )
+ | _ ->
+ raise (RefineFailure
+ (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
let coerced_args,metasenv,subst,t,ugraph2 =
eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
-let type_of_aux' ?localization_tbl metasenv context term ugraph =
- try
- type_of_aux' ?localization_tbl metasenv context term ugraph
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
-
let undebrujin uri typesno tys t =
snd
(List.fold_right
| C.LetIn (name,so,dest) ->
let ctx' = Some (name,(C.Def (so,None)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.Appl l as t ->
+ | C.Appl l ->
+ 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!!!!"; *)
- let newt =
- if b then
- let ugraph = CicUniv.empty_ugraph in
- let old_insert_coercions = !insert_coercions in
- insert_coercions := false;
- let newt, _, menv, _ =
- 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;
- if metasenv <> [] || menv = [] then
- newt
- else
- (prerr_endline "PUO' SUCCEDERE!!!!!";t)
- else
- t
- in
- (match newt with
- | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
- | _ -> assert false)
+ if b then
+ let ugraph = CicUniv.empty_ugraph in
+ let old_insert_coercions = !insert_coercions in
+ insert_coercions := false;
+ let newt, _, menv, _ =
+ 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;
+ if metasenv <> [] || menv = [] then
+ newt
+ else
+ (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+ else
+ t
| C.Var (uri,exp_named_subst) ->
let exp_named_subst = List.map aux exp_named_subst in
C.Var (uri, exp_named_subst)
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
projects / helm.git / blobdiff