diff options
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 69 |
1 files changed, 52 insertions, 17 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 88e1bce9..0a90e0db 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -24,6 +24,7 @@ open Pretype_errors open Evarutil open Unification open Misctypes +open Sigma.Notations (* Abbreviations *) @@ -71,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause let clenv_push_prod cl = - let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match kind_of_term typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> @@ -108,7 +109,7 @@ let clenv_environments evd bound t = | (n, Cast (t,_,_)) -> clrec (e,metas) n t | (n, Prod (na,t1,t2)) -> let mv = new_meta () in - let dep = dependent (mkRel 1) t2 in + let dep = not (noccurn 1 t2) in let na' = if dep then na else Anonymous in let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) @@ -119,7 +120,7 @@ let clenv_environments evd bound t = clrec (evd,[]) bound t let mk_clenv_from_env env sigma n (c,cty) = - let evd = create_goal_evar_defs sigma in + let evd = clear_metas sigma in let (evd,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; @@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs = else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in + let evd = Sigma.Unsafe.of_evar_map clenv.evd in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs (******************************************************************) -let connect_clenv gls clenv = - let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in - { clenv with - evd = evd ; - env = Goal.V82.env evd (sig_it gls) } - -(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *) -(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *) - (* [clenv_fchain mv clenv clenv'] * * Resolves the value of "mv" (which must be undefined) in clenv to be @@ -432,6 +426,44 @@ let check_bindings bl = str " occurs more than once in binding list.") | [] -> () +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then out_name na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) in + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum pr_id mvl ++ str")."))) + +let meta_with_name evd id = + let na = Name id in + let fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in + match mvnodef, mvl with + | _,[] -> + explain_no_such_bound_variable evd id + | ([n],_|_,[n]) -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + strbrk "\" occurs more than once in clause.") + let meta_of_binder clause loc mvs = function | NamedHyp s -> meta_with_name clause.evd s | AnonHyp n -> @@ -459,7 +491,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c @@ -576,7 +609,9 @@ let make_evar_clause env sigma ?len t = | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in - let sigma, ev = new_evar ~store env sigma t1 in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let sigma = Sigma.to_evar_map sigma in let dep = dependent (mkRel 1) t2 in let hole = { hole_evar = ev; @@ -628,7 +663,7 @@ let evar_of_binder holes = function try let h = List.nth holes (pred n) in h.hole_evar - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "" (str "No such binder.") let define_with_type sigma env ev c = |