* 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"
(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
| (_,_) -> 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
| _ -> 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 ->
(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
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
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
- | CoercGraph.NotHandled _ ->
- raise
- (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.NotMetaClosed ->
- raise
- (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to 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
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
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 _
- | CoercGraph.NotMetaClosed ->
- 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 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 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
in
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'
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
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 =
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
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 =
(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) ->
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
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
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 -
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
) ;
*)
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
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 =
(* 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
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
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
(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))
(*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) ->
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 _
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 =
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,[])
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
projects / helm.git / blobdiff