| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
-let enrich f =
- function
- RefineFailure msg -> raise (RefineFailure (f msg))
- | Uncertain msg -> raise (Uncertain (f msg))
- | _ -> assert false
+let enrich loc f exn =
+ let exn' =
+ match exn with
+ RefineFailure msg -> RefineFailure (f msg)
+ | Uncertain msg -> Uncertain (f msg)
+ | _ -> assert false
+ in
+ match loc with
+ None -> raise exn'
+ | Some loc -> 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
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
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
+ relocalize localization_tbl x x';
+ (x', ty)::res,subst',metasenv',ugraph1
) tl ([],subst',metasenv',ugraph1)
in
let tl',applty,subst''',metasenv''',ugraph3 =
- try
eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
- with
- exn ->
- enrich
- (fun msg ->
- lazy ("The application " ^
- CicMetaSubst.ppterm_in_context subst'' t context ^
- " is not well typed:\n" ^ Lazy.force msg)) exn
in
C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
| C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
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
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))
in
- enrich msg exn
+ enrich
+ (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
+ 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))
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
projects / helm.git / blobdiff