X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=9c78c1aa777cba9b7f39b07a4d653ce9c332f9d0;hb=34fad691712f60b4cd11510b9f73c09d25eaf125;hp=a0dfb9f2889e2d7bb024a1e08b28c8d756616078;hpb=f0b23f17200a0b86a1f53cac172a333ddbd8181d;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a0dfb9f28..9c78c1aa7 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -42,6 +42,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,128 +74,20 @@ 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 = @@ -288,13 +204,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 +228,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 +273,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,47 +283,48 @@ and type_of_aux' metasenv context t ugraph = let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - (try - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - | _ -> raise (RefineFailure (lazy "Cast"))) + (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 + 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 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 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 -> - raise (RefineFailure (lazy "no coercion")) - | CoercGraph.NotHandled _ -> - raise (RefineFailure (lazy "not a sort in PI")) + | 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 -> - raise (Uncertain (lazy "Coercions on metas 1")) + 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) in @@ -412,7 +336,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 @@ -429,22 +352,29 @@ 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 - in - (match CicReduction.whd ~subst:subst' context sort1 with + type_of_aux subst metasenv context s ugraph in + let s',sort1 = + 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)))) - ) ; + | 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"))) + in 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 @@ -454,7 +384,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' @@ -476,15 +405,15 @@ 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 subst'' metasenv'' context + 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")) + | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context @@ -526,9 +455,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 = @@ -564,8 +493,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 @@ -611,6 +551,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 = @@ -743,6 +685,19 @@ and type_of_aux' metasenv context t ugraph = (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) + let tlbody_and_type,subst,metasenv,ugraph4 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + in + let _,_,subst,metasenv,ugraph4 = + eat_prods false subst metasenv context + outtypety tlbody_and_type ugraph4 + in let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 @@ -785,7 +740,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 @@ -827,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,_,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 @@ -853,6 +806,9 @@ 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 (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -918,7 +874,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 @@ -936,8 +892,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 @@ -1000,7 +956,9 @@ and type_of_aux' metasenv context t ugraph = (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2'')))) - and eat_prods subst metasenv context hetype tlbody_and_type ugraph = + and eat_prods + allow_coercions subst metasenv context hetype tlbody_and_type ugraph + = let rec mk_prod metasenv context = function [] -> @@ -1067,7 +1025,7 @@ and type_of_aux' metasenv context t ugraph = fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn -> + with exn when allow_coercions -> (* we search a coercion from hety to s *) let coer = let carr t subst context = @@ -1079,16 +1037,32 @@ and type_of_aux' metasenv context t ugraph = in 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 in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context - (* (CicMetaSubst.subst subst hete t) tl *) - (CicSubstitution.subst hete t) ugraph1 tl + (CicSubstitution.subst arg t) ugraph1 tl in arg::coerced_args,metasenv',subst',t',ugraph2 | _ -> assert false @@ -1147,9 +1121,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)) @@ -1177,7 +1151,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) -> @@ -1228,25 +1201,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 _ @@ -1271,7 +1250,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 = @@ -1285,7 +1266,7 @@ let typecheck metasenv uri obj = (fun (name,ty) (metasenv,ugraph,res) -> let ty = CicTypeChecker.debrujin_constructor 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,[]) @@ -1319,8 +1300,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