generalized to return the list of matched terms
2. unfold generalized to unfold several occurrences at once
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
- | `Unfold what -> Tactics.unfold ~pattern ?what
+ | `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
match term with
| `Term t ->
let context' =
match term with
| `Term t ->
let context' =
ProofEngineHelpers.locate_in_conjecture t
(dummy_goal, context, conclusion)
ProofEngineHelpers.locate_in_conjecture t
(dummy_goal, context, conclusion)
+ with
+ [context,_] -> context
+ | _ -> assert false (* since it uses physical equality *)
in
dummy_goal, context', t
| `Hyp context -> dummy_goal, context, Cic.Rel 1
in
dummy_goal, context', t
| `Hyp context -> dummy_goal, context, Cic.Rel 1
-theorem trivial: \forall n. S (myplus n n) = (S n) + n.
- unfold myplus.
+theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
+ unfold myplus in \vdash \forall _.(? ? ? %).
rewrite > lem.
reflexivity.
qed.
\ No newline at end of file
rewrite > lem.
reflexivity.
qed.
\ No newline at end of file
in
subst,metasenv,ugraph,context_terms, ty_terms
in
subst,metasenv,ugraph,context_terms, ty_terms
-exception TermNotFound
-exception TermFoundMultipleTimes
-
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
-* It returns the matched term together with its context in [where]
+* It returns the matched terms together with their contexts in [where]
* [equality] defaults to physical equality
* [context] must be the context of [where]
* [equality] defaults to physical equality
* [context] must be the context of [where]
-* It may raise TermNotFound or TermFoundMultipleTimes
*)
let locate_in_term ?(equality=(==))what ~where context =
*)
let locate_in_term ?(equality=(==))what ~where context =
- let (@@) (l1,l2) (l1',l2') = l1 @ l1', l2 @ l2' in
- let list_concat l = List.fold_right (@@) l ([],[]) in
let add_ctx context name entry =
(Some (name, entry)) :: context in
let rec aux context where =
let add_ctx context name entry =
(Some (name, entry)) :: context in
let rec aux context where =
- if equality what where then context,[where]
+ if equality what where then [context,where]
else
match where with
| Cic.Implicit _
else
match where with
| Cic.Implicit _
| Cic.Var _
| Cic.Const _
| Cic.MutInd _
| Cic.Var _
| Cic.Const _
| Cic.MutInd _
- | Cic.MutConstruct _ -> [],[]
- | Cic.Cast (te, ty) -> aux context te @@ aux context ty
+ | Cic.MutConstruct _ -> []
+ | Cic.Cast (te, ty) -> aux context te @ aux context ty
| Cic.Prod (name, s, t)
| Cic.Lambda (name, s, t) ->
| Cic.Prod (name, s, t)
| Cic.Lambda (name, s, t) ->
- aux context s @@ aux (add_ctx context name (Cic.Decl s)) t
+ aux context s @ aux (add_ctx context name (Cic.Decl s)) t
| Cic.LetIn (name, s, t) ->
| Cic.LetIn (name, s, t) ->
- aux context s @@ aux (add_ctx context name (Cic.Def (s,None))) t
+ aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
| Cic.Appl tl -> auxs context tl
| Cic.MutCase (_, _, out, t, pat) ->
| Cic.Appl tl -> auxs context tl
| Cic.MutCase (_, _, out, t, pat) ->
- aux context out @@ aux context t @@ auxs context pat
+ aux context out @ aux context t @ auxs context pat
| Cic.Fix (_, funs) ->
let tys =
List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
| Cic.Fix (_, funs) ->
let tys =
List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
(List.map
(fun (_, _, ty, bo) ->
(List.map
(fun (_, _, ty, bo) ->
- aux context ty @@ aux (tys @ context) bo)
+ aux context ty @ aux (tys @ context) bo)
funs)
| Cic.CoFix (_, funs) ->
let tys =
List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
funs)
| Cic.CoFix (_, funs) ->
let tys =
List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
(List.map
(fun (_, ty, bo) ->
(List.map
(fun (_, ty, bo) ->
- aux context ty @@ aux (tys @ context) bo)
+ aux context ty @ aux (tys @ context) bo)
funs)
and auxs context tl = (* as aux for list of terms *)
funs)
and auxs context tl = (* as aux for list of terms *)
- list_concat (List.map (fun t -> aux context t) tl)
+ List.concat (List.map (fun t -> aux context t) tl)
- match aux context where with
- context,[] -> raise TermNotFound
- | context,[t] -> context,t
- | context,_ -> raise TermFoundMultipleTimes
-(** locate_in_term equality what where
-* [what] must be a subterm of [where] according to [equality]
-* It returns the context of [what] in [where]
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
* [equality] defaults to physical equality
* [equality] defaults to physical equality
-* It may raise TermNotFound or TermFoundMultipleTimes
+* [context] must be the context of [where]
*)
let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
*)
let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
- let (@@) (l1,l2) =
- function
- None -> l1,l2
- | Some (l1',t) -> l1 @ l1', l2 @ [t] in
- let locate_in_term what ~where context =
- try
- Some (locate_in_term ~equality what ~where context)
- with
- TermNotFound -> None in
let context,res =
List.fold_right
(fun entry (context,res) ->
match entry with
None -> entry::context, res
| Some (_, Cic.Decl ty) ->
let context,res =
List.fold_right
(fun entry (context,res) ->
match entry with
None -> entry::context, res
| Some (_, Cic.Decl ty) ->
- let res = res @@ locate_in_term what ~where:ty context in
+ let res = res @ locate_in_term what ~where:ty context in
let context' = entry::context in
context',res
| Some (_, Cic.Def (bo,ty)) ->
let context' = entry::context in
context',res
| Some (_, Cic.Def (bo,ty)) ->
- let res = res @@ locate_in_term what ~where:bo context in
+ let res = res @ locate_in_term what ~where:bo context in
let res =
match ty with
None -> res
| Some ty ->
let res =
match ty with
None -> res
| Some ty ->
- res @@ locate_in_term what ~where:ty context in
+ res @ locate_in_term what ~where:ty context in
let context' = entry::context in
context',res
let context' = entry::context in
context',res
- let res = res @@ locate_in_term what ~where:ty context in
- match res with
- context,[] -> raise TermNotFound
- | context,[_] -> context
- | context,_ -> raise TermFoundMultipleTimes
+ res @ locate_in_term what ~where:ty context
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
] option list *
(Cic.context * Cic.term) list
] option list *
(Cic.context * Cic.term) list
-exception TermNotFound
-exception TermFoundMultipleTimes
-
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
-* It returns the matched term together with its context in [where]
+* It returns the matched terms together with their contexts in [where]
* [equality] defaults to physical equality
* [context] must be the context of [where]
* [equality] defaults to physical equality
* [context] must be the context of [where]
-* It may raise TermNotFound or TermFoundMultipleTimes
*)
val locate_in_term:
?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term ->
*)
val locate_in_term:
?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term ->
- Cic.context -> Cic.context * Cic.term
+ Cic.context -> (Cic.context * Cic.term) list
-(** locate_in_conjecture equality what where
+(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
* [what] must match a subterm of [where] according to [equality]
-* It returns the context of [what] in [where]
+* It returns the matched terms together with their contexts in [where]
* [equality] defaults to physical equality
* [equality] defaults to physical equality
-* It may raise TermNotFound or TermFoundMultipleTimes
+* [context] must be the context of [where]
*)
val locate_in_conjecture:
?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture ->
*)
val locate_in_conjecture:
?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture ->
+ (Cic.context * Cic.term) list
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
| Cic.Appl (he::tl) -> hd_delta_beta context tl he
| t -> cannot_delta_expand t
in
| Cic.Appl (he::tl) -> hd_delta_beta context tl he
| t -> cannot_delta_expand t
in
+ let context_and_matched_term_list =
+ None -> [context, where]
ProofEngineHelpers.locate_in_term
~equality:first_is_the_expandable_head_of_second
what ~where context
ProofEngineHelpers.locate_in_term
~equality:first_is_the_expandable_head_of_second
what ~where context
- with
- ProofEngineHelpers.TermNotFound ->
raise
(ProofEngineTypes.Fail
("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
raise
(ProofEngineTypes.Fail
("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
- let reduced_term = hd_delta_beta context [] where' in
- match what with
- None -> reduced_term
- | Some what ->
- replace ~equality:first_is_the_expandable_head_of_second
- ~what:[what] ~with_what:[reduced_term] ~where
+ let reduced_terms =
+ List.map
+ (function (context,where) -> hd_delta_beta context [] where)
+ context_and_matched_term_list in
+ let whats = List.map snd context_and_matched_term_list in
+ replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
let reduce_tac ~pattern =
mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
let reduce_tac ~pattern =
mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
-let unfold_tac ?what ~pattern =
+let unfold_tac what ~pattern =
mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
~pattern);;
mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
~pattern);;
val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val unfold_tac:
val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val unfold_tac:
- ?what:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+ Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val change_tac:
pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val change_tac:
pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
val unfold :
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
val unfold :
pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic