X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=620f66f1831a4ec598178645201dd7686c47c7d7;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=37d89bf1f300c279d39e36eea0dd9f15c2d7b83d;hpb=d7eb6fad3e5afc0fc786c9a91ef64733120dfb43;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 37d89bf1f..620f66f18 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" @@ -42,6 +46,30 @@ in profiler.HExtlib.profile foo () (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; + +let enrich localization_tbl t ?(f = fun msg -> msg) exn = + let exn' = + match exn with + RefineFailure msg -> RefineFailure (f msg) + | Uncertain msg -> Uncertain (f msg) + | _ -> assert false in + let loc = + try + Cic.CicHash.find localization_tbl t + with Not_found -> + prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + assert false + in + raise (HExtlib.Localized (loc,exn')) + +let relocalize localization_tbl oldt newt = + try + let infos = Cic.CicHash.find localization_tbl oldt in + Cic.CicHash.remove localization_tbl oldt; + Cic.CicHash.add localization_tbl newt infos; + with + Not_found -> () +;; let rec split l n = match (l,n) with @@ -50,130 +78,23 @@ let rec split l n = | (_,_) -> raise (AssertFailure (lazy "split: list too short")) ;; -let exp_impl metasenv subst context term = - let rec aux metasenv context = function - | (Cic.Rel _) as t -> metasenv, t - | (Cic.Sort _) as t -> metasenv, t - | Cic.Const (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Const (uri, subst') - | Cic.Var (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Var (uri, subst') - | Cic.MutInd (uri, i, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutInd (uri, i, subst') - | Cic.MutConstruct (uri, i, j, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutConstruct (uri, i, j, subst') - | Cic.Meta (n,l) -> - let metasenv', l' = do_local_context metasenv context l in - metasenv', Cic.Meta (n, l') - | Cic.Implicit (Some `Type) -> +let exp_impl metasenv subst context = + function + | Some `Type -> let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv', Cic.Meta (idx, irl) - | Cic.Implicit (Some `Closed) -> + | Some `Closed -> let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in metasenv', Cic.Meta (idx, []) - | Cic.Implicit None -> + | None -> let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv', Cic.Meta (idx, irl) - | Cic.Implicit _ -> assert false - | Cic.Cast (te, ty) -> - let metasenv', ty' = aux metasenv context ty in - let metasenv'', te' = aux metasenv' context te in - metasenv'', Cic.Cast (te', ty') - | Cic.Prod (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.Prod (name, s', t) - | Cic.Lambda (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.Lambda (name, s', t) - | Cic.LetIn (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.LetIn (name, s', t) - | Cic.Appl l when List.length l > 1 -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - l (metasenv, []) - in - metasenv', Cic.Appl l' - | Cic.Appl _ -> assert false - | Cic.MutCase (uri, i, outtype, term, patterns) -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - (outtype :: term :: patterns) (metasenv, []) - in - let outtype', term', patterns' = - match l' with - | outtype' :: term' :: patterns' -> outtype', term', patterns' - | _ -> assert false - in - metasenv', Cic.MutCase (uri, i, outtype', term', patterns') - | Cic.Fix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, _, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in - let rec combine = function - | ((name, index, _, body) :: funs_tl), - ((_, typ) :: typ_tl) -> - (name, index, typ, body) :: combine (funs_tl, typ_tl) - | [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types) in - metasenv', Cic.Fix (i, funs') - | Cic.CoFix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in - let rec combine = function - | ((name, _, body) :: funs_tl), - ((_, typ) :: typ_tl) -> - (name, typ, body) :: combine (funs_tl, typ_tl) - | [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types) in - metasenv', Cic.CoFix (i, funs') - and do_subst metasenv context subst = - List.fold_right - (fun (uri, term) (metasenv, substs) -> - let metasenv', term' = aux metasenv context term in - (metasenv', (uri, term') :: substs)) - subst (metasenv, []) - and do_local_context metasenv context local_context = - List.fold_right - (fun term (metasenv, local_context) -> - let metasenv', term' = - match term with - | None -> metasenv, None - | Some term -> - let metasenv', term' = aux metasenv context term in - metasenv', Some term' - in - metasenv', term' :: local_context) - local_context (metasenv, []) - in - aux metasenv context term + | _ -> assert false ;; + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -288,13 +209,14 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' metasenv context t ugraph = - let metasenv, t = exp_impl metasenv [] context t in +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 module C = Cic in let module S = CicSubstitution in let module U = UriManager in - (* this stops on binders, so we have to call it every time *) + let (t',_,_,_,_) as res = match t with (* function *) C.Rel n -> @@ -311,9 +233,13 @@ and type_of_aux' metasenv context t ugraph = (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph - | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) + | None -> + enrich localization_tbl t + (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure (lazy "Not a close term"))) + _ -> + enrich localization_tbl t + (RefineFailure (lazy "Not a close term"))) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst @@ -352,7 +278,9 @@ and type_of_aux' metasenv context t ugraph = t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Implicit infos -> + let metasenv',t' = exp_impl metasenv subst context infos in + type_of_aux subst metasenv' context t' ugraph | C.Cast (te,ty) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph @@ -360,46 +288,68 @@ and type_of_aux' metasenv context t ugraph = let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty' ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + (try + let subst''',metasenv''',ugraph3 = + fo_unif_subst subst'' context metasenv'' + inferredty ty' ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + with + exn -> + enrich localization_tbl te' + ~f:(fun _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst'' te' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst'' inferredty + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst'' ty' context)) exn + ) | C.Prod (name,s,t) -> let carr t subst context = CicMetaSubst.apply_subst subst t in - let coerce_to_sort - in_source tgt_sort t type_to_coerce subst ctx metasenv uragph + let coerce_to_sort in_source tgt_sort t type_to_coerce + subst context metasenv uragph = - let coercion_src = carr type_to_coerce subst ctx in - match coercion_src with - | Cic.Sort _ -> - t,type_to_coerce,subst,metasenv,ugraph -(* - | Cic.Meta _ as meta when not in_source -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in - let subst, metasenv, ugraph = - fo_unif_subst - subst ctx metasenv meta coercion_tgt ugraph - in - t, Cic.Sort tgt_sort, 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 ctx in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - (match boh with - | CoercGraph.NoCoercion -> - raise (RefineFailure (lazy "no coercion")) - | CoercGraph.NotHandled _ -> - raise (RefineFailure (lazy "not a sort in PI")) - | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on metas 1")) - | 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 @@ -409,7 +359,6 @@ and type_of_aux' metasenv context t ugraph = s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (name,(C.Decl s')))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',sort2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context_for_t t ugraph1 @@ -426,22 +375,46 @@ and type_of_aux' metasenv context t ugraph = | C.Lambda (n,s,t) -> let s',sort1,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph + type_of_aux subst metasenv context s ugraph in + 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 - (match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> () - | _ -> - raise (RefineFailure (lazy (sprintf - "Not well-typed lambda-abstraction: the source %s should be a type; - instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1)))) - ) ; let context_for_t = ((Some (n,(C.Decl s')))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',type2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - context_for_t t ugraph1 + type_of_aux subst' metasenv' context_for_t t ugraph1 in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 @@ -451,7 +424,6 @@ and type_of_aux' metasenv context t ugraph = type_of_aux subst metasenv context s ugraph in let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' @@ -473,15 +445,16 @@ and type_of_aux' metasenv context t ugraph = let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in - (x', ty)::res,subst',metasenv',ugraph1 + (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in let tl',applty,subst''',metasenv''',ugraph3 = eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 in - C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) + 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 = check_exp_named_subst subst metasenv context @@ -523,9 +496,9 @@ and type_of_aux' metasenv context t ugraph = C.InductiveDefinition (l,expl_params,parsno,_) -> List.nth l i , expl_params, parsno, u | _ -> - raise - (RefineFailure - (lazy ("Unkown mutual inductive definition " ^ + enrich localization_tbl t + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in let rec count_prod t = @@ -561,8 +534,19 @@ and type_of_aux' metasenv context t ugraph = in let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv,ugraph3 = + try fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 + with + exn -> + enrich localization_tbl term' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst term' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst expected_type' context)) in let rec instantiate_prod t = function @@ -608,6 +592,8 @@ and type_of_aux' metasenv context t ugraph = its instances *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 in (match outtype with | C.Meta (n,l) -> (let candidate,ugraph5,metasenv,subst = @@ -740,9 +726,6 @@ and type_of_aux' metasenv context t ugraph = (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) - let outtype,outtypety, subst, metasenv,ugraph4 = - type_of_aux subst metasenv context outtype ugraph4 - in let tlbody_and_type,subst,metasenv,ugraph4 = List.fold_right (fun x (res,subst,metasenv,ugraph) -> @@ -798,7 +781,6 @@ and type_of_aux' metasenv context t ugraph = let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> - let metasenv, bo = exp_impl metasenv subst context' bo in let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in @@ -840,7 +822,6 @@ and type_of_aux' metasenv context t ugraph = let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> - let metasenv, bo = exp_impl metasenv subst context' bo in let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in @@ -866,6 +847,22 @@ and type_of_aux' metasenv context t ugraph = fl_ty' fl_bo' fl in C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 + in + 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 - @@ -931,7 +928,7 @@ and type_of_aux' metasenv context t ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = match tl with [] -> [],metasubst,metasenv,ugraph - | ((uri,t) as subst)::tl -> + | (uri,t)::tl -> let ty_uri,ugraph1 = type_of_variable uri ugraph in let typeofvar = CicSubstitution.subst_vars substs ty_uri in @@ -949,8 +946,8 @@ and type_of_aux' metasenv context t ugraph = ) ; *) let t',typeoft,metasubst',metasenv',ugraph2 = - type_of_aux metasubst metasenv context t ugraph1 - in + type_of_aux metasubst metasenv context t ugraph1 in + let subst = uri,t' in let metasubst'',metasenv'',ugraph3 = try fo_unif_subst @@ -1016,22 +1013,22 @@ and type_of_aux' metasenv context t ugraph = 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 = @@ -1039,7 +1036,7 @@ and type_of_aux' metasenv context t ugraph = (* 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 @@ -1050,10 +1047,10 @@ and type_of_aux' metasenv context t ugraph = 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 @@ -1082,23 +1079,71 @@ and type_of_aux' metasenv context t ugraph = 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 _ -> raise exn + | CoercGraph.NotHandled _ -> + enrich localization_tbl hete + (RefineFailure + (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*)))) | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on meta")) + enrich localization_tbl hete + (Uncertain + (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*)))) | 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 + try + let newty,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety s ugraph + in + newt, subst, metasenv, ugraph + with 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) + | 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 @@ -1161,9 +1206,9 @@ and type_of_aux' metasenv context t ugraph = (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; -let type_of_aux' metasenv context term ugraph = +let type_of_aux' ?localization_tbl metasenv context term ugraph = try - type_of_aux' metasenv context term ugraph + type_of_aux' ?localization_tbl metasenv context term ugraph with CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) @@ -1191,7 +1236,6 @@ let map_first_n n start f g l = (*CSC: this is a very rough approximation; to be finished *) let are_all_occurrences_positive metasenv ugraph uri tys leftno = - let number_of_types = List.length tys in let subst,metasenv,ugraph,tys = List.fold_right (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) -> @@ -1242,25 +1286,31 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno = in metasenv,ugraph,substituted_tys -let typecheck metasenv uri obj = +let typecheck metasenv uri obj ~localization_tbl = let ugraph = CicUniv.empty_ugraph in match obj with Cic.Constant (name,Some bo,ty,args,attrs) -> - let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let bo',boty,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph in let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in let bo' = CicMetaSubst.apply_subst subst bo' in let ty' = CicMetaSubst.apply_subst subst ty' in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph | Cic.Constant (name,None,ty,args,attrs) -> - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph + in Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> assert (metasenv' = metasenv); (* Here we do not check the metasenv for correctness *) - let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in - let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let bo',boty,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] bo ugraph in + let ty',sort,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph in begin match sort with Cic.Sort _ @@ -1285,7 +1335,9 @@ let typecheck metasenv uri obj = let metasenv,ugraph,tys = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph + in metasenv,ugraph,(name,b,ty',cl)::res ) tys (metasenv,ugraph,[]) in let con_context = @@ -1297,9 +1349,11 @@ let typecheck metasenv uri obj = 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' metasenv con_context ty ugraph in + type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in metasenv,ugraph,(name,ty')::res ) cl (metasenv,ugraph,[]) @@ -1333,8 +1387,9 @@ let type_of_aux' metasenv context term = let profiler2 = HExtlib.profile "CicRefine" -let type_of_aux' metasenv context term ugraph = - profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph +let type_of_aux' ?localization_tbl metasenv context term ugraph = + profiler2.HExtlib.profile + (type_of_aux' ?localization_tbl metasenv context term) ugraph -let typecheck metasenv uri obj = - profiler2.HExtlib.profile (typecheck metasenv uri) obj +let typecheck ~localization_tbl metasenv uri obj = + profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj