X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=48ae522f4c9b4b170111a2dabff110e93388d863;hb=b934a94a5d005f9d8e668ef49ec83487090a787b;hp=e99ce5cd70285fe94680b80fdab6a20442b860c7;hpb=bba18e224460b5140bf50ef5750e3993e4a32a01;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index e99ce5cd7..48ae522f4 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -261,6 +261,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -392,15 +405,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " 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 @@ -439,15 +462,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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' @@ -465,6 +479,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " 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 = @@ -1100,31 +1132,33 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1197,7 +1231,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1238,29 +1272,40 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 _ ->