From: Claudio Sacerdoti Coen Date: Mon, 18 May 2009 11:57:50 +0000 (+0000) Subject: 1) new tactic normalize (low-level function implemented in X-Git-Tag: make_still_working~3966 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4080c4f65aa9f69af505530dfbbe94ffede8052e;p=helm.git 1) new tactic normalize (low-level function implemented in nCicTacReduction) 2) the select tactic used to generate fresh metavariables by unifying the "wanted" part of the pattern in a root where "wanted" did not occur. Those metavariables are now removed in that case --- diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index 3ee5156f9..139f27288 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -1,6 +1,7 @@ PACKAGE = ng_tactics INTERFACE_FILES = \ + nCicTacReduction.mli \ nTacStatus.mli \ nTactics.mli \ nCicElim.mli diff --git a/helm/software/components/ng_tactics/nCicTacReduction.ml b/helm/software/components/ng_tactics/nCicTacReduction.ml new file mode 100644 index 000000000..3236956fd --- /dev/null +++ b/helm/software/components/ng_tactics/nCicTacReduction.ml @@ -0,0 +1,24 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +let rec normalize ?(delta=0) ~subst ctx t = + let aux = normalize ~delta ~subst in + match NCicReduction.whd ~delta ~subst ctx t with + NCic.Meta (n,(s,lc)) -> + let l = NCicUtils.expand_local_context lc in + let l' = List.map (aux ctx) l in + if l = l' then t + else + NCic.Meta (n,(s,NCic.Ctx l)) + | t -> NCicUtils.map (fun h ctx -> h::ctx) ctx aux t +;; diff --git a/helm/software/components/ng_tactics/nCicTacReduction.mli b/helm/software/components/ng_tactics/nCicTacReduction.mli new file mode 100644 index 000000000..51b7851a7 --- /dev/null +++ b/helm/software/components/ng_tactics/nCicTacReduction.mli @@ -0,0 +1,15 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val normalize: + ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 323b1e6fc..413afbef0 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -135,6 +135,13 @@ let whd status ?delta ctx t = status, (name, ctx, t) ;; +let normalize status ?delta ctx t = + let status, (name,_,t) = relocate status ctx t in + let _,_,_,subst,_ = status.pstatus in + let t = NCicTacReduction.normalize ~subst ?delta ctx t in + status, (name, ctx, t) +;; + let unify status ctx a b = let status, (_,_,a) = relocate status ctx a in let status, (_,_,b) = relocate status ctx b in @@ -231,22 +238,23 @@ let select_term | NCicUnification.Uncertain _ -> false, status in let match_term status ctx (wanted : cic_term) t = - let rec aux ctx status t = + let rec aux ctx (status,already_found) t = let b, status = is_found status ctx t wanted in if b then let status , (_,_,t) = found status (None, ctx, t) in - status, t + (status,true),t else let _,_,_,subst,_ = status.pstatus in match t with | NCic.Meta (i,lc) when List.mem_assoc i subst -> let _,_,t,_ = NCicUtils.lookup_subst i subst in - aux ctx status t - | NCic.Meta _ -> status, t - | _ -> - NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t + aux ctx (status,already_found) t + | NCic.Meta _ -> (status,already_found),t + | _ -> + NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux + (status,already_found) t in - aux ctx status t + aux ctx (status,false) t in let _,_,_,subst,_ = low_status.pstatus in let rec select status ctx pat cic = @@ -296,9 +304,12 @@ let select_term | NCic.Implicit `Hole, t -> (match wanted with | Some wanted -> - let status, wanted = disambiguate status wanted None ctx in - match_term status ctx wanted t - | None -> match_term status ctx (None,ctx,t) t) + let status', wanted = disambiguate status wanted None ctx in + let (status',found), t' = match_term status' ctx wanted t in + if found then status',t' else status,t + | None -> + let (status,_),t = match_term status ctx (None,ctx,t) t in + status,t) | NCic.Implicit _, t -> status, t | _,t -> fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[] diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 0653223af..c04df8d37 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -50,6 +50,9 @@ val ppterm: lowtac_status -> cic_term -> string val whd: lowtac_status -> ?delta:int -> NCic.context -> cic_term -> lowtac_status * cic_term +val normalize: + lowtac_status -> ?delta:int -> NCic.context -> cic_term -> + lowtac_status * cic_term val typeof: lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term val unify: