exception NotInTheList;;
-let position n (shift, lc) =
+let position to_skip n (shift, lc) =
match lc with
+ | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *)
| NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
| NCic.Irl _ -> n - shift
| NCic.Ctx tl ->
- let rec aux k = function
+ let rec aux to_skip k = function
| [] -> raise NotInTheList
+ | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl
| (NCic.Rel m)::_ when m + shift = n -> k
- | _::tl -> aux (k+1) tl
+ | _::tl -> aux to_skip (k+1) tl
in
- aux 1 tl
+ aux to_skip 1 tl
;;
let pack_lc orig =
| NCicUtils.Meta_not_found _ -> assert false
;;
+let rec flexible_arg subst = function
+ | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)->
+ (try
+ let _,_,t,_ = List.assoc i subst in
+ flexible_arg subst t
+ with Not_found -> true)
+ | _ -> false
+;;
+
+let flexible subst l = List.exists (flexible_arg subst) l;;
+
+let in_scope_tag = "tag:in_scope" ;;
+let out_scope_tag_prefix = "tag:out_scope:"
+let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;;
+let is_out_scope_tag tag =
+ String.length tag > String.length out_scope_tag_prefix &&
+ String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix
+;;
+let int_of_out_scope_tag tag =
+ int_of_string
+ (String.sub tag (String.length out_scope_tag_prefix)
+ (String.length tag - (String.length out_scope_tag_prefix)))
+;;
+
+
(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
otherwise the occur check does not make sense in case of unification
of ?n with ?n *)
let delift ~unify metasenv subst context n l t =
- let unify_list =
+ let unify_list in_scope =
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
- HExtlib.list_findopt
- (fun li i ->
- let li = NCicSubstitution.lift (k+shift) li in
- match unify metasenv subst context li t with
- | Some (metasenv,subst) ->
- Some ((metasenv, subst), NCic.Rel (i+1+k))
- | None -> None)
- l
+ if flexible_arg subst t then None else
+ let lb = List.map (fun t -> t, flexible_arg subst t) l in
+ HExtlib.list_findopt
+ (fun (li,flexible) i ->
+ if flexible || i < in_scope then None else
+ let li = NCicSubstitution.lift (k+shift) li in
+ match unify metasenv subst context li t with
+ | Some (metasenv,subst) ->
+ Some ((metasenv, subst), NCic.Rel (i+1+k))
+ | None -> None)
+ lb
in
- let rec aux k (metasenv, subst as ms) t =
- match unify_list metasenv subst context k t with
+ let rec aux (context,k,in_scope) (metasenv, subst as ms) t =
+ match unify_list in_scope metasenv subst context k t with
| Some x -> x
| None ->
match t with
(try
match List.nth context (n-k-1) with
| _,NCic.Def (bo,_) ->
- (try ms, NCic.Rel ((position (n-k) l) + k)
+ (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
with NotInTheList ->
(* CSC: This bit of reduction hurts performances since it is
* possible to have an exponential explosion of the size of the
* proof. required for nat/nth_prime.ma *)
- aux k ms (NCicSubstitution.lift n bo))
- | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k)
+ aux (context,k,in_scope) ms (NCicSubstitution.lift n bo))
+ | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k)
with Failure _ -> assert false) (*Unbound variable found in delift*)
| NCic.Meta (i,_) when i=n ->
raise (MetaSubstFailure (lazy (Printf.sprintf (
| NCic.Meta (i,l1) as orig ->
(try
let tag,_,t,_ = NCicUtils.lookup_subst i subst in
- (match tag with None -> () | Some tag -> prerr_endline tag);
- aux k ms (NCicSubstitution.subst_meta l1 t)
+ let in_scope =
+ match tag with
+ | Some tag when tag = in_scope_tag -> 0
+ | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
+ | _ -> in_scope
+ in
+ aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
with NCicUtils.Subst_not_found _ ->
if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
else
| t::tl ->
let ms, tbr, tl = deliftl tbr (j+1) ms tl in
try
- let ms, t = aux k ms t in
+ let ms, t = aux (context,k,in_scope) ms t in
ms, tbr, t::tl
with
| NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
restrict metasenv subst i to_be_r in
(metasenv, subst), NCic.Meta(newmeta,l1))
- | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
+ | t ->
+ NCicUntrusted.map_term_fold_a
+ (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
in
- try aux 0 (metasenv,subst) t
+ try aux (context,0,0) (metasenv,subst) t
with NotInTheList ->
(* This is the case where we fail even first order unification. *)
(* The reason is that our delift function is weaker than first *)
| _ -> NCic.Appl (hd :: tl))
;;
-let flexible l =
- List.exists
- (function
- | NCic.Meta _
- | NCic.Appl (NCic.Meta _::_) -> true
- | _ -> false) l
-;;
-
exception WrongShape;;
-let eta_reduce =
- let delift_if_not_occur body orig =
+let eta_reduce subst t =
+ let delift_if_not_occur body =
try
- NCicSubstitution.psubst ~avoid_beta_redexes:true
- (fun () -> raise WrongShape) [()] body
- with WrongShape -> orig
+ Some (NCicSubstitution.psubst ~avoid_beta_redexes:true
+ (fun () -> raise WrongShape) [()] body)
+ with WrongShape -> None
+ in
+ let rec eat_lambdas ctx = function
+ | NCic.Lambda (name, src, tgt) ->
+ eat_lambdas ((name, src) :: ctx) tgt
+ | NCic.Meta (i,lc) as t->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta lc t in
+ eat_lambdas ctx t
+ with Not_found -> ctx, t)
+ | t -> ctx, t
in
- function
- | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
- delift_if_not_occur hd orig
- | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
- when HExtlib.list_last l = NCic.Rel 1 ->
- let body =
- let args, _ = HExtlib.split_nth (List.length l - 1) l in
- NCic.Appl (hd::args)
- in
- delift_if_not_occur body orig
- | t -> t
+ let context_body = eat_lambdas [] t in
+ let rec aux = function
+ | [],body -> body
+ | (name, src)::ctx, (NCic.Appl (hd::[NCic.Rel 1]) as bo) ->
+ (match delift_if_not_occur hd with
+ | None -> aux (ctx,NCic.Lambda(name,src, bo))
+ | Some bo -> aux (ctx,bo))
+ | (name, src)::ctx, (NCic.Appl args as bo)
+ when HExtlib.list_last args = NCic.Rel 1 ->
+ let args, _ = HExtlib.split_nth (List.length args - 1) args in
+ (match delift_if_not_occur (NCic.Appl args) with
+ | None -> aux (ctx,NCic.Lambda(name,src, bo))
+ | Some bo -> aux (ctx,bo))
+ | (name, src) :: ctx, t ->
+ aux (ctx,NCic.Lambda(name,src, t))
+ in
+ aux context_body
;;
-
+
module C = NCic;;
module Ref = NReference;;
aux () t
;;
-let rec beta_expand_many metasenv subst context t args =
+let is_locked n subst =
+ try
+ match NCicUtils.lookup_subst n subst with
+ | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
+ | _ -> false
+ with NCicUtils.Subst_not_found _ -> false
+;;
+
+
+let rec lambda_intros metasenv subst context t args =
let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in
let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in
let rec mk_lambda context n = function
| [] ->
let metasenv, _, bo, _ =
- NCicMetaSubst.mk_meta metasenv context (`WithType tty) in
+ NCicMetaSubst.mk_meta metasenv context
+ (`WithType (NCicSubstitution.lift n tty))
+ in
metasenv, bo
| ty::tail ->
let name = "HBeta"^string_of_int n in
pp msg; assert false
in
let lty = NCicSubstitution.subst_meta lc ty in
- pp (lazy ("On the types: " ^
- NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
- NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
- ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
- let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
- metasenv, subst, t
+ match ty_t with
+ | NCic.Implicit _ ->
+ raise (UnificationFailure
+ (lazy "trying to unify a term with a type"))
+ | ty_t ->
+ pp (lazy ("On the types: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
+ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+ ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
+ let metasenv,subst =
+ unify test_eq_only metasenv subst context lty ty_t in
+ metasenv, subst, t
in
pp (lazy(string_of_int n ^ " := 111 = "^
NCicPp.ppterm ~metasenv ~subst ~context t));
let term2 = NCicSubstitution.subst_meta lc2 term in
unify hdb test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+ | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when
+ not (NCicMetaSubst.flexible subst args) &&
+ is_locked n subst &&
+ not (List.mem_assoc i subst)
+ ->
+ (* we verify that none of the args is a Meta,
+ since beta expanding w.r.t a metavariable makes no sense *)
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args
+ in
+ let metasenv, subst =
+ unify hdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj
+ in
+ let t1 = NCicReduction.whd ~subst context t1 in
+ let i, l =
+ match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+ in
+ let metasenv, subst =
+ instantiate hdb test_eq_only metasenv subst context i l t2 true
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false)
| C.Meta (n,lc), t ->
(try
with Invalid_argument _ ->
raise (fail_exc metasenv subst context t1 t2))
- | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
+ | NCic.Appl (NCic.Meta (i,l)::args), _ when
+ not (NCicMetaSubst.flexible subst args) ->
(* we verify that none of the args is a Meta,
since beta expanding w.r.t a metavariable makes no sense *)
- let metasenv, beta_expanded =
- beta_expand_many metasenv subst context t2 args
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args
in
let metasenv, subst =
unify hdb test_eq_only metasenv subst context
- (C.Meta (i,l)) beta_expanded
+ (C.Meta (i,l)) lambda_Mj
in
-
- (* .... eta_reduce ?i ... *)
+ let metasenv, subst =
unify hdb test_eq_only metasenv subst context t1 t2
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false)
- | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
- let metasenv, beta_expanded =
- beta_expand_many metasenv subst context t1 args
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when
+ not(NCicMetaSubst.flexible subst args) ->
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t2 args
in
let metasenv, subst =
unify hdb test_eq_only metasenv subst context
- beta_expanded (C.Meta (i,l))
+ lambda_Mj (C.Meta (i,l))
in
+ let metasenv, subst =
unify hdb test_eq_only metasenv subst context t1 t2
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false)
(* processing this case here we avoid a useless small delta step *)
| (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
projects / helm.git / commitdiff