2) select now returns a couple (context, term) so that we can build the right context from each returned term
(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 =
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
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
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 \
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 \
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 \
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
* http://cs.unibo.it/helm/.
*)
+exception Bad_pattern of string
+
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
CicMkImplicit.new_meta metasenv []
) [] 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
+
* 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
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 :
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
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' =
(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)
(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)
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
projects / helm.git / commitdiff