X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=1caeb733db2a21253b996e91893f77df8a0d4878;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;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..1caeb733d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -23,12 +23,16 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf 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 +94,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 +310,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 +376,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 +452,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 +851,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]) ]) 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 *) @@ -959,22 +1013,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t and eat_prods allow_coercions subst metasenv context hetype tlbody_and_type ugraph = - let rec mk_prod metasenv context = + let rec mk_prod metasenv context' = function [] -> let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context + CicMkImplicit.mk_implicit_type metasenv subst context' in let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context + CicMkImplicit.identity_relocation_list_for_metavariable context' in metasenv,Cic.Meta (idx, irl) | (_,argty)::tl -> let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context + CicMkImplicit.mk_implicit_type metasenv subst context' in let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context + CicMkImplicit.identity_relocation_list_for_metavariable context' in let meta = Cic.Meta (idx,irl) in let name = @@ -982,7 +1036,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* Nevertheless, argty is well-typed only in context. *) (* Thus I generate a name (name_hint) in context and *) (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in (context'@context). *) + (* --- that is fresh in context'. *) let name_hint = (* Cic.Name "pippo" *) FreshNamesGenerator.mk_fresh_name ~subst metasenv @@ -993,10 +1047,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name ~subst - [] context name_hint ~typ:(Cic.Sort Cic.Prop) + [] context' name_hint ~typ:(Cic.Sort Cic.Prop) in let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl + mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl in metasenv,Cic.Prod (name,meta,target) in @@ -1025,17 +1079,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 +1112,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 +1333,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