(CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
+
+let enrich localization_tbl t f 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 =
| _ -> 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 ->
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 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.NoCoercion
| CoercGraph.NotHandled _ ->
- raise (RefineFailure (lazy "not a sort in PI"))
+ raise
+ (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
| CoercGraph.NotMetaClosed ->
- raise (Uncertain (lazy "Coercions on metas 1"))
+ 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)
in
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
"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))))
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 =
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
(* 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
in
match coer with
| CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotHandled _ ->
+ let msg e =
+ 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*))
+ in
+ enrich localization_tbl hete msg exn
| CoercGraph.NotMetaClosed ->
raise (Uncertain (lazy "Coercions on meta"))
| CoercGraph.SomeCoercion c ->
(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 =
(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,[])
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