X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=95e6c7ba6d213ef308592031b32e4e550666d29a;hb=f4f050696e66b8604d9f0ff8173afe03addf74d6;hp=9c78c1aa777cba9b7f39b07a4d653ce9c332f9d0;hpb=34fad691712f60b4cd11510b9f73c09d25eaf125;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 9c78c1aa7..95e6c7ba6 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -29,6 +29,8 @@ exception RefineFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let insert_coercions = ref true + let debug_print = fun _ -> () let profiler = HExtlib.profile "CicRefine.fo_unif" @@ -90,6 +92,7 @@ let exp_impl metasenv subst context = | _ -> assert false ;; + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -305,28 +308,46 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let coerce_to_sort in_source tgt_sort t type_to_coerce subst context metasenv uragph = - 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 search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - (match boh with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - 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"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl t - (Uncertain (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"))) - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) + 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 search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + (match boh with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + 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"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl t + (Uncertain + (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"))) + | CoercGraph.SomeCoercion c -> + let newt, tty, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;t]) coercion_tgt + in + newt, tty, subst, metasenv, ugraph) in let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -353,24 +374,41 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let s',sort1 = - match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> s',sort1 - | coercion_src -> - let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - match boh with - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;s'], coercion_tgt - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - 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"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl s' - (Uncertain (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"))) + 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 search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + match boh with + | CoercGraph.SomeCoercion c -> + let newt, tty, subst', metasenv', ugraph1 = + avoid_double_coercion + subst' metasenv' ugraph1 + (Cic.Appl[c;s']) coercion_tgt + in + newt, tty, subst', metasenv', ugraph1 + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + 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"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl s' + (Uncertain + (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 = @@ -412,7 +450,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 in - C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 + avoid_double_coercion + subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -810,6 +849,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t relocalize localization_tbl t t'; res + and avoid_double_coercion subst metasenv ugraph t ty = + match t with + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> + 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 + with + | CoercGraph.SomeCoercion c -> + Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph + | _ -> assert false) (* the composite coercion must exist *) + | _ -> t, ty, subst, metasenv, ugraph + (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) @@ -1025,17 +1077,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn when allow_coercions -> + with exn when allow_coercions && !insert_coercions -> (* we search a coercion from hety to s *) - let coer = + let coer, tgt_carr = let carr t subst 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 c_hety c_s + CoercGraph.look_for_coercion c_hety c_s, c_s in - match coer with + (match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl hete @@ -1058,7 +1110,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> - (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph + let newt, _, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;hete]) tgt_carr + in + newt, subst, metasenv, ugraph) + | exn -> + 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 in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context @@ -1264,7 +1331,9 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv,ugraph,cl' = List.fold_right (fun (name,ty) (metasenv,ugraph,res) -> - let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty = + CicTypeChecker.debrujin_constructor + ~cb:(relocalize localization_tbl) uri typesno ty in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in