From d174e54c365ab9df38367de9336c213a03be3c27 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2009 15:43:14 +0000 Subject: [PATCH] unification: - the case (? args) v.s. ?(tag:OUT_SCOPE) is considered as a pattern-driven delifting. - the case ? args v.s. t is reduced to ?[args] v.s. t - eta-contraction reimplemented - beta-expand no longer used delift: - handle out/in scope tag ntactics: - elim sets the out_scope tag for 1 entry --- .../components/ng_refiner/nCicMetaSubst.ml | 83 +++++++--- .../components/ng_refiner/nCicMetaSubst.mli | 6 + .../components/ng_refiner/nCicUnification.ml | 156 +++++++++++++----- .../components/ng_tactics/nTacStatus.ml | 8 +- .../components/ng_tactics/nTacStatus.mli | 2 - .../components/ng_tactics/nTactics.ml | 8 +- .../components/syntax_extensions/.depend | 3 + 7 files changed, 190 insertions(+), 76 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 5062353cd..1a2b5471b 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -21,17 +21,19 @@ let newmeta = 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 = @@ -193,25 +195,53 @@ and restrict metasenv subst i restrictions = | 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 @@ -220,13 +250,13 @@ let delift ~unify metasenv subst context n l t = (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 ( @@ -237,8 +267,13 @@ let delift ~unify metasenv subst context n l t = | 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 @@ -307,7 +342,7 @@ let delift ~unify metasenv subst context n l t = | 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 @@ -330,9 +365,11 @@ let delift ~unify metasenv subst context n l t = 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 *) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 293e3a01f..1ed2fcee3 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -67,3 +67,9 @@ val saturate: NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list +val flexible: NCic.substitution -> NCic.term list -> bool + +val in_scope_tag : string +val out_scope_tag : int -> string +val is_out_scope_tag : string -> bool +val int_of_out_scope_tag : string -> int diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index f23116b63..d64fb005f 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -36,36 +36,45 @@ let mk_appl ~upto hd tl = | _ -> 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;; @@ -98,13 +107,24 @@ let fix_sorts swap metasenv subst context meta t = 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 @@ -159,12 +179,18 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap = 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)); @@ -275,6 +301,34 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = 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 @@ -316,29 +370,45 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = 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)) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 3d81ca53c..f0d12aa8e 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -158,9 +158,6 @@ let mk_meta status ?name ctx bo_or_ty = status, (None,ctx,instance) ;; -let in_scope_tag = "tag:in_scope" ;; -let out_scope_tag = "tag:out_scope" ;; - let select_term low_status (name,context,term) (wanted,path) = let found status ctx t wanted = (* we could lift wanted step-by-step *) @@ -174,7 +171,8 @@ let select_term low_status (name,context,term) (wanted,path) = let b, status = found status ctx t wanted in if b then let status, (_,_,t) = - mk_meta status ~name:in_scope_tag ctx (`Def (None, ctx, t)) + mk_meta status ~name:NCicMetaSubst.in_scope_tag + ctx (`Def (None, ctx, t)) in status, t else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t @@ -232,7 +230,7 @@ let select_term low_status (name,context,term) (wanted,path) = in let status, term = select low_status context path term in let term = (name, context, term) in - mk_meta status ~name:out_scope_tag context (`Def term) + mk_meta status ~name:(NCicMetaSubst.out_scope_tag 1) context (`Def term) ;; let analyse_indty status ty = diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 1feac415b..ce3fd33b0 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -59,8 +59,6 @@ val mk_meta: lowtac_status * cic_term val instantiate: lowtac_status -> int -> cic_term -> lowtac_status -val in_scope_tag: string -val out_scope_tag: string val select_term: lowtac_status -> cic_term -> ast_term option * NCic.term -> lowtac_status * cic_term diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 7fa2b48d8..f45aa656b 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -240,13 +240,15 @@ let reopen status = let subst, newm = List.partition (function (_,(Some tag,_,_,_)) -> - tag <> in_scope_tag && tag <> out_scope_tag + tag <> NCicMetaSubst.in_scope_tag && + not (NCicMetaSubst.is_out_scope_tag tag) | _ -> true) subst in let in_m, out_m = List.partition - (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false) + (function (_,(Some tag,_,_,_)) -> + tag = NCicMetaSubst.in_scope_tag | _ -> assert false) newm in let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in @@ -288,11 +290,11 @@ let elim_tac ~what ~where status = [ select_tac ~where; distribute_tac (fun status goal -> let goalty = get_goalty status goal in + let _,_,w = what in let status, what = disambiguate status what None (ctx_of goalty) in let _ty_what = typeof status (ctx_of what) what in (* check inductive... find eliminator *) - let w = (*astify what *) CicNotationPt.Ident ("m",None) in let holes = [ CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit] in diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2