From f85e6f52232af229b80a8447492cfae80f95d832 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Jun 2005 10:42:27 +0000 Subject: [PATCH] 1) moved select and pattern_of from cicUtil to proofEngineHelpers 2) select now returns a couple (context, term) so that we can build the right context from each returned term --- helm/ocaml/cic/cicUtil.ml | 82 -------------------- helm/ocaml/cic/cicUtil.mli | 16 ---- helm/ocaml/cic_proof_checking/.depend | 12 +-- helm/ocaml/tactics/.depend | 16 ++-- helm/ocaml/tactics/equalityTactics.ml | 4 +- helm/ocaml/tactics/proofEngineHelpers.ml | 94 +++++++++++++++++++++++ helm/ocaml/tactics/proofEngineHelpers.mli | 20 +++++ helm/ocaml/tactics/reductionTactics.ml | 17 ++-- helm/ocaml/tactics/variousTactics.ml | 2 +- 9 files changed, 140 insertions(+), 123 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 405b183cf..d3fcffd80 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -173,88 +173,6 @@ let uri_of_term = function (tyno + 1) consno) | _ -> raise (Invalid_argument "uri_of_term") -let select ~term ~context = - (* i is the number of binder traversed *) - let rec aux i context term = - match (context, term) with - | Cic.Implicit (Some `Hole), t -> [i,t] - | Cic.Implicit (Some `Type), t -> [] - | Cic.Implicit None,_ -> [] - | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> - List.concat - (List.map2 - (fun t1 t2 -> - (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> [])) - ctxt1 ctxt2) - | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2 - | Cic.Prod (_, s1, t1), Cic.Prod (_, s2, t2) - | Cic.Lambda (_, s1, t1), Cic.Lambda (_, s2, t2) - | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> - aux i s1 s2 @ aux (i+1) t1 t2 - | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2 - | Cic.Var (_, subst1), Cic.Var (_, subst2) - | Cic.Const (_, subst1), Cic.Const (_, subst2) - | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2) - | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) -> - auxs i (List.map snd subst1) (List.map snd subst2) - | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> - aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2 - | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> - List.concat - (List.map2 - (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> - aux i ty1 ty2 @ aux i bo1 bo2) - funs1 funs2) - | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> - List.concat - (List.map2 - (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2) - funs1 funs2) - | _ -> assert false (* maybe an Implicit annotation ? *) - and auxs i terms1 terms2 = (* as aux for list of terms *) - List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2) - in - aux 0 context term - -let context_of ?(equality=(==)) ~term terms = - let (===) x y = equality x y in - let rec aux t = - match t with - | t when List.exists (fun t' -> t === t') terms -> Cic.Implicit (Some `Hole) - | Cic.Var (uri, subst) -> Cic.Var (uri, aux_subst subst) - | Cic.Meta (i, ctxt) -> - let ctxt = - List.map (function None -> None | Some t -> Some (aux t)) ctxt - in - Cic.Meta (i, ctxt) - | Cic.Cast (t, ty) -> Cic.Cast (aux t, aux ty) - | Cic.Prod (name, s, t) -> Cic.Prod (name, aux s, aux t) - | Cic.Lambda (name, s, t) -> Cic.Lambda (name, aux s, aux t) - | Cic.LetIn (name, s, t) -> Cic.LetIn (name, aux s, aux t) - | Cic.Appl terms -> Cic.Appl (List.map aux terms) - | Cic.Const (uri, subst) -> Cic.Const (uri, aux_subst subst) - | Cic.MutInd (uri, tyno, subst) -> Cic.MutInd (uri, tyno, aux_subst subst) - | Cic.MutConstruct (uri, tyno, consno, subst) -> - Cic.MutConstruct (uri, tyno, consno, aux_subst subst) - | Cic.MutCase (uri, tyno, outty, t, pat) -> - Cic.MutCase (uri, tyno, aux outty, aux t, List.map aux pat) - | Cic.Fix (funno, funs) -> - let funs = - List.map (fun (name, i, ty, bo) -> (name, i, aux ty, aux bo)) funs - in - Cic.Fix (funno, funs) - | Cic.CoFix (funno, funs) -> - let funs = - List.map (fun (name, ty, bo) -> (name, aux ty, aux bo)) funs - in - Cic.CoFix (funno, funs) - | Cic.Rel _ - | Cic.Sort _ - | Cic.Implicit _ -> t - and aux_subst subst = - List.map (fun (uri, t) -> (uri, aux t)) subst - in - aux term (* let pack terms = diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 39316586e..31c7e4dee 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -55,22 +55,6 @@ val unpack: Cic.term -> Cic.term list val params_of_obj: Cic.obj -> UriManager.uri list val attributes_of_obj: Cic.obj -> Cic.attribute list -(** {2 Contexts} - * A context is a Cic term in which Cic.Implicit terms annotated with `Hole - * appears *) - -(** create a context from a term and a list of subterm. -* @param equality equality function used while walking the term. Defaults to -* physical equality (==) *) -val context_of: - ?equality:(Cic.term -> Cic.term -> bool) -> term:Cic.term -> Cic.term list -> - Cic.term - -(** select all subterms of a given term matching a given context (i.e. subtrees -* rooted at context's holes. The first component is the number of binder the -* term is below *) -val select: term:Cic.term -> context:Cic.term -> (int * Cic.term) list - (** mk_rels [howmany] [from] * creates a list of [howmany] rels starting from [from] in decreasing order *) val mk_rels : int -> int -> Cic.term list diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 105cfe4d9..e99b1253d 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -14,13 +14,13 @@ cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \ cicReduction.cmi cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \ cicReduction.cmi -cicTypeChecker.cmo: cicSubstitution.cmi cicReduction.cmi cicPp.cmi \ - cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi -cicTypeChecker.cmx: cicSubstitution.cmx cicReduction.cmx cicPp.cmx \ - cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi +cicTypeChecker.cmo: cicUnivUtils.cmi cicSubstitution.cmi cicReduction.cmi \ + cicPp.cmi cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi +cicTypeChecker.cmx: cicUnivUtils.cmx cicSubstitution.cmx cicReduction.cmx \ + cicPp.cmx cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \ cicPp.cmi cicEnvironment.cmi cicElim.cmi cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \ cicPp.cmx cicEnvironment.cmx cicElim.cmi -cicRecord.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicRecord.cmi -cicRecord.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicRecord.cmi +cicRecord.cmo: cicSubstitution.cmi cicEnvironment.cmi cicRecord.cmi +cicRecord.cmx: cicSubstitution.cmx cicEnvironment.cmx cicRecord.cmi diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 02467679c..9efaac2b9 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -25,9 +25,9 @@ proofEngineHelpers.cmx: proofEngineHelpers.cmi tacticals.cmo: proofEngineTypes.cmi tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ - reductionTactics.cmi + proofEngineHelpers.cmi reductionTactics.cmi reductionTactics.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ - reductionTactics.cmi + proofEngineHelpers.cmx reductionTactics.cmi proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ @@ -43,9 +43,11 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi primitiveTactics.cmi variousTactics.cmi + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + variousTactics.cmi variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx primitiveTactics.cmx variousTactics.cmi + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + variousTactics.cmi autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ primitiveTactics.cmi metadataQuery.cmi autoTactic.cmi autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ @@ -90,8 +92,10 @@ fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ fourier.cmx equalityTactics.cmx fourierR.cmi -fwdSimplTactic.cmo: proofEngineTypes.cmi metadataQuery.cmi fwdSimplTactic.cmi -fwdSimplTactic.cmx: proofEngineTypes.cmx metadataQuery.cmx fwdSimplTactic.cmi +fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi +fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi history.cmo: history.cmi history.cmx: history.cmi statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index dd2c42f1c..8cbfed96b 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -66,11 +66,11 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = match goal_path with | None -> assert false (* (==), [t1'] *) | Some path -> - let roots = CicUtil.select ~term:gty' ~context:path in + let roots = ProofEngineHelpers.select ~term:gty' ~pattern:path in let subterms = List.fold_left ( fun acc (i, r) -> - let wanted = CicSubstitution.lift i t1' in + let wanted = CicSubstitution.lift (List.length i) t1' in PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc ) [] roots in diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 61d46e24a..3382c4c98 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +exception Bad_pattern of string + let new_meta_of_proof ~proof:(_, metasenv, _, _) = CicMkImplicit.new_meta metasenv [] @@ -150,3 +152,95 @@ let find_subterms ~eq ~wanted t = ) [] funl in find wanted t + +let select ~term ~pattern = + let add_ctx i name entry = + (Some (name, entry)) :: i + in + (* i is the number of binder traversed *) + let rec aux i pattern term = + match (pattern, term) with + | Cic.Implicit (Some `Hole), t -> [i,t] + | Cic.Implicit (Some `Type), t -> [] + | Cic.Implicit None,_ -> [] + | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> + List.concat + (List.map2 + (fun t1 t2 -> + (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> [])) + ctxt1 ctxt2) + | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2 + | Cic.Prod (_, s1, t1), Cic.Prod (name, s2, t2) + | Cic.Lambda (_, s1, t1), Cic.Lambda (name, s2, t2) -> + aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2 + | Cic.LetIn (_, s1, t1), Cic.LetIn (name, s2, t2) -> + aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2 + | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2 + | Cic.Var (_, subst1), Cic.Var (_, subst2) + | Cic.Const (_, subst1), Cic.Const (_, subst2) + | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2) + | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) -> + auxs i (List.map snd subst1) (List.map snd subst2) + | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> + aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2 + | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> + List.concat + (List.map2 + (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> + aux i ty1 ty2 @ aux i bo1 bo2) + funs1 funs2) + | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> + List.concat + (List.map2 + (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2) + funs1 funs2) + | x,y -> + raise (Bad_pattern + (Printf.sprintf "Pattern %s versus term %s" + (CicPp.ppterm x) + (CicPp.ppterm y))) + and auxs i terms1 terms2 = (* as aux for list of terms *) + List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2) + in + aux [] pattern term + +let pattern_of ?(equality=(==)) ~term terms = + let (===) x y = equality x y in + let rec aux t = + match t with + | t when List.exists (fun t' -> t === t') terms -> Cic.Implicit (Some `Hole) + | Cic.Var (uri, subst) -> Cic.Var (uri, aux_subst subst) + | Cic.Meta (i, ctxt) -> + let ctxt = + List.map (function None -> None | Some t -> Some (aux t)) ctxt + in + Cic.Meta (i, ctxt) + | Cic.Cast (t, ty) -> Cic.Cast (aux t, aux ty) + | Cic.Prod (name, s, t) -> Cic.Prod (name, aux s, aux t) + | Cic.Lambda (name, s, t) -> Cic.Lambda (name, aux s, aux t) + | Cic.LetIn (name, s, t) -> Cic.LetIn (name, aux s, aux t) + | Cic.Appl terms -> Cic.Appl (List.map aux terms) + | Cic.Const (uri, subst) -> Cic.Const (uri, aux_subst subst) + | Cic.MutInd (uri, tyno, subst) -> Cic.MutInd (uri, tyno, aux_subst subst) + | Cic.MutConstruct (uri, tyno, consno, subst) -> + Cic.MutConstruct (uri, tyno, consno, aux_subst subst) + | Cic.MutCase (uri, tyno, outty, t, pat) -> + Cic.MutCase (uri, tyno, aux outty, aux t, List.map aux pat) + | Cic.Fix (funno, funs) -> + let funs = + List.map (fun (name, i, ty, bo) -> (name, i, aux ty, aux bo)) funs + in + Cic.Fix (funno, funs) + | Cic.CoFix (funno, funs) -> + let funs = + List.map (fun (name, ty, bo) -> (name, aux ty, aux bo)) funs + in + Cic.CoFix (funno, funs) + | Cic.Rel _ + | Cic.Sort _ + | Cic.Implicit _ -> t + and aux_subst subst = + List.map (fun (uri, t) -> (uri, aux t)) subst + in + aux term + diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 5cf58999c..c2f8c640a 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +exception Bad_pattern of string + (* Returns the first meta whose number is above the *) (* number of the higher meta. *) val new_meta_of_proof : proof:ProofEngineTypes.proof -> int @@ -41,6 +43,24 @@ val subst_meta_and_metasenv_in_proof : val compare_metasenvs : oldmetasenv:Cic.metasenv -> newmetasenv:Cic.metasenv -> int list + +(** { Patterns } + * A pattern is a Cic term in which Cic.Implicit terms annotated with `Hole + * appears *) + +(** create a pattern from a term and a list of subterm. +* @param equality equality function used while walking the term. Defaults to +* physical equality (==) *) +val pattern_of: + ?equality:(Cic.term -> Cic.term -> bool) -> term:Cic.term -> Cic.term list -> + Cic.term + +(** select all subterms of a given term matching a given pattern (i.e. subtrees +* rooted at pattern's holes. The first component is the context the term lives +* in). raise Bad_pattern (pattern_entry, term_entry) *) +val select: term:Cic.term -> pattern:Cic.term -> (Cic.context * Cic.term) list + + (** Finds the _pointers_ to subterms that are alpha-equivalent to wanted in t. * wanted is properly lifted when binders are crossed *) val find_subterms : diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index c641cbf65..430414b78 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -58,12 +58,9 @@ let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = try let terms, terms' = List.split - (List.map - (fun i, t -> t, - (let x, _, _ = CicMetaSubst.delift_rels [] metasenv i t in - let t' = reduction context x in - CicSubstitution.lift i t')) - terms) + (List.map + (fun i, t -> t, reduction (i @ context) t) + terms) in ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' ~where:where @@ -76,9 +73,9 @@ let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = in let ty' = match goal_pattern with - | None -> replace context ty [0,ty] + | None -> replace context ty [[],ty] | Some pat -> - let terms = CicUtil.select ~term:ty ~context:pat in + let terms = ProofEngineHelpers.select ~term:ty ~pattern:pat in replace context ty terms in let context' = @@ -90,7 +87,7 @@ let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = CicUtil.select ~term ~context:pat in + let terms = ProofEngineHelpers.select ~term ~pattern:pat in let where = replace context term terms in let entry = Some (name,Cic.Decl where) in entry::context) @@ -98,7 +95,7 @@ let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = CicUtil.select ~term ~context:pat in + let terms = ProofEngineHelpers.select ~term ~pattern:pat in let where = replace context term terms in let entry = Some (name,Cic.Def (where,None)) in entry::context) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 233cc321f..9fcbb966f 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -88,7 +88,7 @@ let generalize_tac match concl_pat with None -> Cic.Implicit (Some `Hole) | Some path -> path in - let roots = CicUtil.select ~term:ty ~context:path in + let roots = ProofEngineHelpers.select ~term:ty ~pattern:path in List.fold_left (fun acc (i, r) -> ProofEngineHelpers.find_subterms -- 2.39.2