<keyword>split</keyword>
<keyword>to</keyword>
<keyword>transitivity</keyword>
+ <keyword>unfold</keyword>
<keyword>whd</keyword>
</keyword-list>
| `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
| `Reduce -> ProofEngineReduction.reduce
| `Simpl -> ProofEngineReduction.simpl
+ | `Unfold what -> ProofEngineReduction.unfold ?what
| `Whd -> CicReduction.whd ~delta:false ~subst:[]
in
Tactics.fold ~reduction ~term ~pattern
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
+ | `Unfold what -> Tactics.unfold ~pattern ?what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
status, Some wanted
in
status, (wanted, hyp_paths ,goal_path)
+
+let disambiguate_reduction_kind status = function
+ | `Unfold (Some t) ->
+ let status, t = disambiguate_term status t in
+ status, `Unfold (Some t)
+ | `Normalize
+ | `Reduce
+ | `Simpl
+ | `Unfold None
+ | `Whd as kind -> status, kind
let disambiguate_tactic status = function
| GrafiteAst.Apply (loc, term) ->
status, GrafiteAst.ElimType (loc, what, None, depth, idents)
| GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
| GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
- | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
+ | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
let status, pattern = disambiguate_pattern status pattern in
let status, term = disambiguate_term status term in
- status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
+ let status, red_kind = disambiguate_reduction_kind status red_kind in
+ status, GrafiteAst.Fold (loc,red_kind, term, pattern)
| GrafiteAst.FwdSimpl (loc, hyp, names) ->
status, GrafiteAst.FwdSimpl (loc, hyp, names)
| GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
| GrafiteAst.LetIn (loc, term, name) ->
let status, term = disambiguate_term status term in
status, GrafiteAst.LetIn (loc,term,name)
- | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
+ | GrafiteAst.Reduce (loc, red_kind, pattern) ->
let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
+ let status, red_kind = disambiguate_reduction_kind status red_kind in
+ status, GrafiteAst.Reduce(loc, red_kind, pattern)
| GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
| GrafiteAst.Replace (loc, pattern, with_what) ->
let status, pattern = disambiguate_pattern status pattern in
*)
type direction = [ `LeftToRight | `RightToLeft ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+type 'term reduction_kind =
+ [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
type loc = CicNotationPt.location
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
| Generalize of loc * ('term, 'ident) pattern * 'ident option
| LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
- | Reduce of loc * reduction_kind * ('term, 'ident) pattern
+ | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern
| Reflexivity of loc
| Replace of loc * ('term, 'ident) pattern * 'term
| Rewrite of loc * direction * 'term * ('term, 'ident) pattern
let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
let pp_reduction_kind = function
+ | `Normalize -> "normalize"
| `Reduce -> "reduce"
| `Simpl -> "simplify"
+ | `Unfold (Some t) -> "unfold " ^ pp_term_ast t
+ | `Unfold None -> "unfold"
| `Whd -> "whd"
- | `Normalize -> "normalize"
let pp_pattern (t, hyp, goal) =
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "reduce" -> `Reduce
+ [ IDENT "normalize" -> `Normalize
+ | IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
- | IDENT "whd" -> `Whd
- | IDENT "normalize" -> `Normalize ]
+ | IDENT "unfold"; t = OPT term -> `Unfold t
+ | IDENT "whd" -> `Whd ]
];
sequent_pattern_spec: [
[ hyp_paths =
tactics.cmi: proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
-proofEngineReduction.cmo: proofEngineReduction.cmi
-proofEngineReduction.cmx: proofEngineReduction.cmi
+proofEngineReduction.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi
+proofEngineReduction.cmx: proofEngineHelpers.cmx proofEngineReduction.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi
tacticals.cmo: proofEngineTypes.cmi tacticals.cmi
INTERFACE_FILES = \
proofEngineTypes.mli \
- proofEngineReduction.mli proofEngineHelpers.mli \
+ proofEngineHelpers.mli proofEngineReduction.mli \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
variousTactics.mli autoTactic.mli \
in
subst,metasenv,ugraph,context_terms, ty_terms
-(** locate_in_term what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_term what ~where context =
+exception TermNotFound
+exception TermFoundMultipleTimes
+
+(** 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]
+* [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 (@@) (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
+ (Some (name, entry)) :: context in
let rec aux context where =
- if what == where then context
+ if equality what where then context,[where]
else
match where with
| Cic.Implicit _
| 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) ->
- 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) ->
- 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) ->
- 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
- List.concat
+ list_concat
(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
- List.concat
+ list_concat
(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 *)
- List.concat (List.map (fun t -> aux context t) tl)
+ list_concat (List.map (fun t -> aux context t) tl)
in
- aux context where
+ match aux context where with
+ context,[] -> raise TermNotFound
+ | context,[t] -> context,t
+ | context,_ -> raise TermFoundMultipleTimes
-(** locate_in_conjecture what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_conjecture what (_,context,ty) =
+(** locate_in_term equality what where
+* [what] must be a subterm of [where] according to [equality]
+* It returns the context of [what] in [where]
+* [equality] defaults to physical equality
+* It may raise TermNotFound or TermFoundMultipleTimes
+*)
+let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
+ let (@@) (l1,l2) (l1',t) = l1 @ l1', l2 @ [t] in
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 ~equality what ~where:ty context in
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 ~equality what ~where:bo context in
let res =
match ty with
None -> res
- | Some ty -> res @ locate_in_term what ~where:ty context in
+ | Some ty ->
+ res @@ locate_in_term ~equality what ~where:ty context in
let context' = entry::context in
context',res
- ) context ([],[])
+ ) context ([],([],[]))
in
- res @ locate_in_term what ~where:ty context
-
+ let res = res @@ locate_in_term ~equality what ~where:ty context in
+ match res with
+ context,[] -> raise TermNotFound
+ | context,[_] -> context
+ | context,_ -> raise TermFoundMultipleTimes
(* 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
-(** locate_in_conjecture what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-val locate_in_conjecture: Cic.term -> Cic.conjecture -> Cic.context
+exception TermNotFound
+exception TermFoundMultipleTimes
+
+(** 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]
+* [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 ->
+ Cic.context -> Cic.context * Cic.term
+
+(** locate_in_conjecture equality what where
+* [what] must match a subterm of [where] according to [equality]
+* It returns the context of [what] in [where]
+* [equality] defaults to physical equality
+* It may raise TermNotFound or TermFoundMultipleTimes
+*)
+val locate_in_conjecture:
+ ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture ->
+ Cic.context
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
in
reduceaux context []
;;
+
+let unfold ?what context where =
+ let first_is_the_expandable_head_of_second t1 t2 =
+ match t1,t2 with
+ Cic.Const (uri,_), Cic.Const (uri',_)
+ | Cic.Var (uri,_), Cic.Var (uri',_)
+ | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
+ | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
+ | Cic.Const _, _
+ | Cic.Var _, _ -> false
+ | _,_ ->
+ raise
+ (ProofEngineTypes.Fail
+ "The term to unfold is neither a constant nor a variable")
+ in
+ let appl he tl =
+ if tl = [] then he else Cic.Appl (he::tl) in
+ let cannot_delta_expand t =
+ raise
+ (ProofEngineTypes.Fail
+ ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
+ let rec hd_delta_beta context tl =
+ function
+ Cic.Rel n as t ->
+ (try
+ match List.nth context (n-1) with
+ Some (_,Cic.Decl _) -> cannot_delta_expand t
+ | Some (_,Cic.Def (bo,_)) ->
+ CicReduction.head_beta_reduce
+ (appl (CicSubstitution.lift n bo) tl)
+ | None -> raise RelToHiddenHypothesis
+ with
+ Failure _ -> assert false)
+ | Cic.Const (uri,exp_named_subst) as t ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match o with
+ Cic.Constant (_,Some body,_,_,_) ->
+ CicReduction.head_beta_reduce
+ (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+ | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
+ | Cic.Variable _ -> raise ReferenceToVariable
+ | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | Cic.Var (uri,exp_named_subst) as t ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match o with
+ Cic.Constant _ -> raise ReferenceToConstant
+ | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | Cic.Variable (_,Some body,_,_,_) ->
+ CicReduction.head_beta_reduce
+ (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+ | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
+ )
+ | Cic.Appl [] -> assert false
+ | Cic.Appl (he::tl) -> hd_delta_beta context tl he
+ | t -> cannot_delta_expand t
+ in
+ let context, where =
+ match what with
+ None -> context, where
+ | Some what ->
+ try
+ 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))
+ in
+ hd_delta_beta context [] where
+;;
what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
val reduce : Cic.context -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term
+val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term
(curi,metasenv',pbo,pty), [metano]
;;
-let simpl_tac ~pattern =
+let simpl_tac ~pattern =
mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
-let reduce_tac ~pattern =
+let reduce_tac ~pattern =
mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
+
+let unfold_tac ?what ~pattern =
+ mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
+ ~pattern);;
-let whd_tac ~pattern =
+let whd_tac ~pattern =
mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
-let normalize_tac ~pattern =
+let normalize_tac ~pattern =
mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
exception NotConvertible
val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
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
val change_tac:
pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
+let unfold = ReductionTactics.unfold_tac
let whd = ReductionTactics.whd_tac
val split : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
+val unfold :
+ ?what:Cic.term ->
+ pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
projects / helm.git / commitdiff