| [ IDENT "normalize" ] -> `Normalize ]
];
pattern_spec: [
- [ "in";
- hyp_paths =
- LIST0
- [ id = IDENT ;
- path = OPT [SYMBOL ":" ; path = term -> path ] ->
- (id,match path with Some p -> p | None -> CicAst.UserInput) ]
- SEP SYMBOL ";";
- goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
- (hyp_paths, goal_path) ]
+ [ wanted = OPT term;
+ hyp_paths_and_goal_path =
+ OPT [
+ "in";
+ hyp_paths =
+ LIST0
+ [ id = IDENT ;
+ path = OPT [SYMBOL ":" ; path = term -> path ] ->
+ (id,match path with Some p -> p | None -> CicAst.UserInput) ]
+ SEP SYMBOL ";";
+ goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
+ let goal_path =
+ match goal_path with
+ None -> CicAst.UserInput
+ | Some goal_path -> goal_path
+ in
+ hyp_paths,goal_path
+ ] ->
+ let hyp_paths,goal_path =
+ match hyp_paths_and_goal_path with
+ None -> [], CicAst.UserInput
+ | Some (hyp_paths,goal_path) -> hyp_paths,goal_path
+ in
+ wanted, hyp_paths, goal_path ]
];
direction: [
[ IDENT "left" -> `Left
TacticAst.Clear (loc,id)
| IDENT "clearbody"; id = IDENT ->
TacticAst.ClearBody (loc,id)
- | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; "in";
- where = pattern_spec ->
- TacticAst.Change (loc, t1, t2, where)
+ | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
+ TacticAst.Change (loc, what, t)
| IDENT "compare"; t = tactic_term ->
TacticAst.Compare (loc,t)
| IDENT "constructor"; n = NUM ->
| IDENT "exists" ->
TacticAst.Exists loc
| IDENT "fail" -> TacticAst.Fail loc
- | IDENT "fold"; kind = reduction_kind; t = tactic_term;
- p = OPT [ pattern_spec ] ->
- let p = match p with None -> [], None | Some p -> p in
- TacticAst.Fold (loc, kind, t, p)
+ | IDENT "fold"; kind = reduction_kind; p = pattern_spec ->
+ TacticAst.Fold (loc, kind, p)
| IDENT "fourier" ->
TacticAst.Fourier loc
| IDENT "fwd"; t = term ->
TacticAst.FwdSimpl (loc, t)
- | IDENT "generalize"; t = tactic_term;
- id = OPT [ "as" ; id = IDENT -> id ];
- p = OPT [ pattern_spec ] ->
- let p = match p with None -> [], None | Some p -> p in
- TacticAst.Generalize (loc,t,id,p)
+ | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
+ TacticAst.Generalize (loc,p,id)
| IDENT "goal"; n = NUM ->
TacticAst.Goal (loc, int_of_string n)
| IDENT "id" -> TacticAst.IdTac loc
| IDENT "left" -> TacticAst.Left loc
| IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
- | kind = reduction_kind; p = OPT [ pattern_spec ] ->
- let p = match p with None -> [], None | Some p -> p in
+ | kind = reduction_kind; p = pattern_spec ->
TacticAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
TacticAst.Reflexivity loc
- | IDENT "replace"; p = OPT [ pattern_spec ]; "with"; t = tactic_term ->
- let p = match p with None -> [], None | Some p -> p in
+ | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
TacticAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] ->
- let p = match p with None -> [], None | Some p -> p in
- TacticAst.Rewrite (loc, d, t, p)
+ | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec ->
+ let (pt,_,_) = p in
+ if pt <> None then
+ raise
+ (Parse_error
+ (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))
+ else
+ TacticAst.Rewrite (loc, d, t, p)
| IDENT "right" ->
TacticAst.Right loc
| IDENT "ring" ->
sequentPp.cmo: cic2Xml.cmi sequentPp.cmi
sequentPp.cmx: cic2Xml.cmx sequentPp.cmi
applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \
- content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi
+ domMisc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi
applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \
- content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi
+ domMisc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi
tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi
tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi
boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi
let rec pp_term = function
| CicAst.AttributedTerm (_, term) -> pp_term term
-
| CicAst.Appl terms ->
sprintf "(%s)" (String.concat " " (List.map pp_term terms))
| CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
| CicAst.Sort `Type -> "Type"
| CicAst.Sort `CProp -> "CProp"
| CicAst.Symbol (name, _) -> name
-
- | CicAst.UserInput -> ""
+ | CicAst.UserInput -> "%"
and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
and pp_substs substs = String.concat "; " (List.map pp_subst substs)
type loc = CicAst.location
-type ('term, 'ident) pattern =
- ('ident * 'term) list * 'term option
+type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Assumption of loc
| Auto of loc * int option * int option (* depth, width *)
- | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
+ | Change of loc * ('term,'ident) pattern * 'term
| Clear of loc * 'ident
| ClearBody of loc * 'ident
| Compare of loc * 'term
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * reduction_kind * ('term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * 'term
- | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
+ | Generalize of loc * ('term, 'ident) pattern * 'ident option
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
| IdTac of loc
| Injection of loc * 'term
| `Normalize -> "normalize"
-let pp_pattern (hyp, goal) =
+let pp_pattern (t, hyp, goal) =
let pp_hyp_pattern l =
String.concat "; "
- (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l)
+ (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in
+ let pp_t t =
+ match t with
+ None -> ""
+ | Some t -> pp_term_ast t
in
- let pp_goal_pattern p =
- match p with
- | None -> ""
- | Some p -> pp_term_ast p
- in
- let separator =
- if hyp <> [] then " \\vdash " else " "
- in
- "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal
+ pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
let rec pp_tactic = function
| Absurd (_, term) -> "absurd" ^ pp_term_ast term
| Apply (_, term) -> "apply " ^ pp_term_ast term
| Auto _ -> "auto"
| Assumption _ -> "assumption"
- | Change (_, t1, t2, where) ->
- sprintf "change %s with %s %s" (pp_term_ast t1) (pp_term_ast t2)
- (pp_pattern where)
+ | Change (_, where, with_what) ->
+ sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what)
| Clear (_,id) -> sprintf "clear %s" id
| ClearBody (_,id) -> sprintf "clearbody %s" id
| Compare (_,term) -> "compare " ^ pp_term_ast term
| ElimType (_, term) -> "elim type " ^ pp_term_ast term
| Exact (_, term) -> "exact " ^ pp_term_ast term
| Exists _ -> "exists"
- | Fold (_, kind, term, pattern) ->
- sprintf "fold %s %s %s" (pp_reduction_kind kind) (pp_term_ast term)
- (pp_pattern pattern)
- | Generalize (_, term, ident, pattern) ->
- sprintf "generalize %s%s %s" (pp_term_ast term)
+ | Fold (_, kind, pattern) ->
+ sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+ | Generalize (_, pattern, ident) ->
+ sprintf "generalize %s%s" (pp_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
- (pp_pattern pattern)
| Goal (_, n) -> "goal " ^ string_of_int n
| Fail _ -> "fail"
| Fourier _ -> "fourier"
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineReduction.cmo: proofEngineReduction.cmi
proofEngineReduction.cmx: proofEngineReduction.cmi
-proofEngineHelpers.cmo: proofEngineHelpers.cmi
-proofEngineHelpers.cmx: proofEngineHelpers.cmi
+proofEngineHelpers.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi
+proofEngineHelpers.cmx: proofEngineReduction.cmx proofEngineHelpers.cmi
tacticals.cmo: proofEngineTypes.cmi tacticals.cmi
tacticals.cmx: proofEngineTypes.cmx tacticals.cmi
reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \
primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi
equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
- introductionTactics.cmi equalityTactics.cmi
+ primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi
equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
- introductionTactics.cmx equalityTactics.cmi
+ primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmi
discriminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
eliminationTactics.cmi discriminationTactics.cmi
in
ProofEngineTypes.apply_tactic
(P.change_tac
- ~what:new_t1'
- ~pattern:([],None)
- ~with_what:
- (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda (
- (C.Name "x"),
- (S.lift 1 tty),
- (S.lift 2 tty'))),
- (C.Rel 1), pattern
- )
- );
- t1]
- ))
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
+ (C.Appl [
+ C.Lambda (
+ C.Name "x", tty,
+ C.MutCase (
+ turi, typeno,
+ (C.Lambda (
+ (C.Name "x"),
+ (S.lift 1 tty),
+ (S.lift 2 tty'))),
+ (C.Rel 1), pattern
+ )
+ );
+ t1]
+ ))
status
))
~continuation:
(T.then_
~start:
(P.change_tac
- ~what:gty'
- ~pattern:([],None)
- ~with_what:
- (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
- (C.Rel 1), pattern
- )
- );
- t2]
- )
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
+ (C.Appl [
+ C.Lambda (
+ C.Name "x", tty,
+ C.MutCase (
+ turi, typeno,
+ (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
+ (C.Rel 1), pattern
+ )
+ );
+ t2]
+ )
)
~continuation:
(
let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
+(*
let module C = Cic in
let module U = UriManager in
let module PET = ProofEngineTypes in
in
assert (List.length goals = 0) ;
(proof',[fresh_meta])
+*) assert false
let rewrite_tac ?where ~term () =
(Tacticals.then_
~start:(rewrite_tac ?where ~term ())
~continuation:
- (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)))
status
in
ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
(Tacticals.then_
~start:(rewrite_back_tac ?where ~term ())
~continuation:
- (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)))
status
in
ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
(Tacticals.then_
~start:
(ReductionTactics.fold_tac ~reduction:CicReduction.whd
- ~pattern:([],None)
- ~term:
- (Cic.Appl
- [_Rle ; _R0 ;
- Cic.Appl
- [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
- ]
- )
+ ~pattern:
+ (ProofEngineTypes.conclusion_pattern
+ (Some
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ )))
)
~continuation:
(Tacticals.then_
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
- ~with_what:(Cic.Appl [ _not; ineq]))
+ (PrimitiveTactics.change_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+ (Cic.Appl [ _not; ineq]))
status))
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
- ~with_what:w1) status in
+ (PrimitiveTactics.change_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+ w1) status
+ in
debug("fine MY_CHNGE\n");
r))
~continuation:(*PORTINGTacticals.id_tac*)tac2]))
(Tacticals.thens
~start:(intros_tac ())
~continuations:
- [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
+ [ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)])
;;
exception NotConvertible
(*CSC: while [what] can have a richer context (because of binders) *)
(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
(*CSC: Is that evident? Is that right? Or should it be changed? *)
-let change_tac ~what ~with_what ~pattern =
+let change_tac ~pattern with_what =
(*
let change_tac ~what ~with_what ~pattern (proof, goal) =
let curi,metasenv,pbo,pty = proof in
term: Cic.term -> ProofEngineTypes.tactic
val change_tac:
- what: Cic.term -> with_what: Cic.term -> pattern:ProofEngineTypes.pattern ->
- ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
;;
(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
-let find_subterms ~eq ~wanted t =
- let rec find w t =
- if eq w t then
- [t]
+let find_subterms ~wanted ~context t =
+ let rec find context w t =
+ if ProofEngineReduction.alpha_equivalence w t then
+ [context,t]
else
match t with
| Cic.Sort _
fun acc e ->
match e with
| None -> acc
- | Some t -> find w t @ acc
+ | Some t -> find context w t @ acc
) [] ctx
- | Cic.Lambda (_, t1, t2)
- | Cic.Prod (_, t1, t2)
- | Cic.LetIn (_, t1, t2) ->
- find w t1 @ find (CicSubstitution.lift 1 w) t2
+ | Cic.Lambda (name, t1, t2)
+ | Cic.Prod (name, t1, t2) ->
+ find context w t1 @
+ find (Some (name, Cic.Decl t1)::context)
+ (CicSubstitution.lift 1 w) t2
+ | Cic.LetIn (name, t1, t2) ->
+ find context w t1 @
+ find (Some (name, Cic.Def (t1,None))::context)
+ (CicSubstitution.lift 1 w) t2
| Cic.Appl l ->
- List.fold_left (fun acc t -> find w t @ acc) [] l
- | Cic.Cast (t, ty) -> find w t @ find w ty
+ List.fold_left (fun acc t -> find context w t @ acc) [] l
+ | Cic.Cast (t, ty) -> find context w t @ find context w ty
| Cic.Implicit _ -> assert false
| Cic.Const (_, esubst)
| Cic.Var (_, esubst)
| Cic.MutInd (_, _, esubst)
| Cic.MutConstruct (_, _, _, esubst) ->
- List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst
+ List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst
| Cic.MutCase (_, _, outty, indterm, patterns) ->
- find w outty @ find w indterm @
- List.fold_left (fun acc p -> find w p @ acc) [] patterns
+ find context w outty @ find context w indterm @
+ List.fold_left (fun acc p -> find context w p @ acc) [] patterns
| Cic.Fix (_, funl) ->
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
+ in
List.fold_left (
- fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc
+ fun acc (_, _, ty, bo) ->
+ find context w ty @ find (tys @ context) w bo @ acc
) [] funl
| Cic.CoFix (_, funl) ->
+ let tys =
+ List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
+ in
List.fold_left (
- fun acc (_, ty, bo) -> find w ty @ find w bo @ acc
+ fun acc (_, ty, bo) ->
+ find context w ty @ find (tys @ context) w bo @ acc
) [] funl
in
- find wanted t
+ find context wanted t
-let select ~term ~pattern =
- let add_ctx i name entry =
- (Some (name, entry)) :: i
+let select ~context ~term ~pattern:(wanted,where) =
+ let add_ctx context name entry =
+ (Some (name, entry)) :: context
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]
+ let rec aux context where term =
+ match (where, term) with
+ | Cic.Implicit (Some `Hole), t -> [context,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 | _ -> []))
+ (match (t1, t2) with
+ Some t1, Some t2 -> aux context t1 t2
+ | _ -> []))
ctxt1 ctxt2)
- | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2
+ | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) ->
+ aux context te1 te2 @ aux context ty1 ty2
| Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
| Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
- aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
+ aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
| Cic.Prod (Cic.Name n1, s1, t1),
Cic.Prod ((Cic.Name n2) as name , s2, t2)
| Cic.Lambda (Cic.Name n1, s1, t1),
Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
+ aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
| Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
| Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
| Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
- aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
+ aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
| Cic.LetIn (Cic.Name n1, s1, t1),
Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
+ aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
| Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
- | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2
+ | Cic.Appl terms1, Cic.Appl terms2 -> auxs context 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)
+ auxs context (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
+ aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
| Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+ in
List.concat
(List.map2
(fun (_, _, ty1, bo1) (_, _, ty2, bo2) ->
- aux i ty1 ty2 @ aux i bo1 bo2)
+ aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
funs1 funs2)
| Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
+ let tys =
+ List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+ in
List.concat
(List.map2
- (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2)
+ (fun (_, ty1, bo1) (_, ty2, bo2) ->
+ aux context ty1 ty2 @ aux (tys @ context) 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)
+ and auxs context terms1 terms2 = (* as aux for list of terms *)
+ List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2)
in
- aux [] pattern term
+ let roots = aux context where term in
+ match wanted with
+ None -> roots
+ | Some wanted ->
+ let rec find_in_roots =
+ function
+ [] -> []
+ | (context,where)::tl ->
+ let tl' = find_in_roots tl in
+ let found =
+ let wanted = CicSubstitution.lift (List.length context) wanted in
+ find_subterms ~wanted ~context where
+ in
+ found @ tl'
+ in
+ find_in_roots roots
let pattern_of ?(equality=(==)) ~term terms =
let (===) x y = equality x y in
?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 :
- eq:(Cic.term -> Cic.term -> bool) ->
- wanted:Cic.term -> Cic.term ->
- Cic.term list
-
+(** select context term (what,where)
+* select all subterms of [term] matching [what] in positions rooted at the holes
+* of the pattern [where]. [context] is the context of [term]. It returns
+* the list of the matched terms (that can be compared using physical equality)
+* together with their contexts. *)
+val select:
+ context:Cic.context -> term:Cic.term -> pattern:(Cic.term option * Cic.term) ->
+ (Cic.context * Cic.term) list
(** creates an opaque tactic from a status->proof*goal list function *)
let mk_tactic t = t
-type pattern = (string * Cic.term) list * Cic.term option
-let goal_pattern = [],None
+ (** what, hypothesis patterns, conclusion pattern *)
+type pattern = Cic.term option * (string * Cic.term) list * Cic.term
+let conclusion_pattern t = t,[],Cic.Implicit (Some `Hole)
(** tactic failure *)
exception Fail of string
type tactic
val mk_tactic: (status -> proof * goal list) -> tactic
-(** the type of a tactic application domain
- * [ hypothesis_name * path ] * goal_path
- *)
-type pattern = (string * Cic.term) list * Cic.term option
+ (** what, hypothesis patterns, conclusion pattern *)
+type pattern = Cic.term option * (string * Cic.term) list * Cic.term
-(** the pattern for the whole goal *)
-val goal_pattern : pattern
+ (** conclusion_pattern [t] returns the pattern (t,[],%) *)
+val conclusion_pattern : Cic.term option -> pattern
(** tactic failure *)
exception Fail of string
open ProofEngineTypes
-(*
-let reduction_tac ~reduction (proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let new_ty = reduction context ty in
- let new_metasenv =
- List.map
- (function
- (n,_,_) when n = metano -> (metano,context,new_ty)
- | _ as t -> t
- ) metasenv
- in
- (curi,new_metasenv,pbo,pty), [metano]
-;;
-*)
-
(* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) =
+let reduction_tac ~reduction ~pattern:(what,hyp_patterns,goal_pattern)
+ (proof,goal)
+=
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- (* We don't know if [term] is a subterm of [ty] or a subterm of *)
- (* the type of one metavariable. So we replace it everywhere. *)
- (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
- (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
- (*CSC: e' meglio prima cercare il termine e scoprirne il *)
- (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
- let replace context where terms =
- (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
- (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
- (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
- try
- let terms, terms' =
- List.split
- (List.map
- (fun i, t -> t, reduction (i @ context) t)
- terms)
- in
- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where
- (* FIXME this is a catch ALL... bad thing *)
- with exc -> (*prerr_endline (Printexc.to_string exc);*) where
- in
+ let replace where terms =
+ let terms, terms' =
+ List.split (List.map (fun (context, t) -> t, reduction context t) terms)
+ in
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where in
let find_pattern_for name =
try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
- with Not_found -> None
- in
+ with Not_found -> None in
let ty' =
- match goal_pattern with
- | None -> replace context ty [[],ty]
- | Some pat ->
- let terms = ProofEngineHelpers.select ~term:ty ~pattern:pat in
- replace context ty terms
- in
+ let terms =
+ ProofEngineHelpers.select ~context ~term:ty ~pattern:(what,goal_pattern)
+ in
+ replace ty terms in
+ let context_len = List.length context in
let context' =
if hyp_patterns <> [] then
List.fold_right
(fun entry context ->
match entry with
+ None -> None::context
| Some (name,Cic.Decl term) ->
(match find_pattern_for name with
| None -> entry::context
| Some pat ->
- 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)
- | Some (name,Cic.Def (term, None)) ->
+ try
+ let what =
+ match what with
+ None -> None
+ | Some what ->
+ let what,subst',metasenv' =
+ CicMetaSubst.delift_rels [] metasenv
+ (context_len - List.length context) what
+ in
+ assert (subst' = []);
+ assert (metasenv' = metasenv);
+ Some what in
+ let terms =
+ ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in
+ let term' = replace term terms in
+ Some (name,Cic.Decl term') :: context
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ raise
+ (ProofEngineTypes.Fail
+ ("The term the user wants to convert is not closed " ^
+ "in the context of the position of the substitution.")))
+ | Some (name,Cic.Def (term, ty)) ->
(match find_pattern_for name with
| None -> entry::context
| Some pat ->
- 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)
- | _ -> entry::context
+ try
+ let what =
+ match what with
+ None -> None
+ | Some what ->
+ let what,subst',metasenv' =
+ CicMetaSubst.delift_rels [] metasenv
+ (context_len - List.length context) what
+ in
+ assert (subst' = []);
+ assert (metasenv' = metasenv);
+ Some what in
+ let terms =
+ ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in
+ let term' = replace term terms in
+ let ty' =
+ match ty with
+ None -> None
+ | Some ty ->
+ let terms =
+ ProofEngineHelpers.select
+ ~context ~term:ty ~pattern:(what,pat)
+ in
+ Some (replace ty terms)
+ in
+ Some (name,Cic.Def (term',ty')) :: context
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ raise
+ (ProofEngineTypes.Fail
+ ("The term the user wants to convert is not closed " ^
+ "in the context of the position of the substitution.")))
) context []
else
context
let normalize_tac ~pattern =
mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
-let fold_tac ~reduction ~pattern ~term =
+let fold_tac ~reduction ~pattern =
(*
let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
=
val fold_tac:
reduction:(Cic.context -> Cic.term -> Cic.term) ->
- pattern:ProofEngineTypes.pattern -> term:Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
?depth:int ->
?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
val change :
- what:Cic.term ->
- with_what:Cic.term ->
- pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val clear : hyp:string -> ProofEngineTypes.tactic
val clearbody : hyp:string -> ProofEngineTypes.tactic
val compare : term:Cic.term -> ProofEngineTypes.tactic
val fail : ProofEngineTypes.tactic
val fold :
reduction:(Cic.context -> Cic.term -> Cic.term) ->
- pattern:ProofEngineTypes.pattern ->
- term:Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val fourier : ProofEngineTypes.tactic
val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+ ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val id : ProofEngineTypes.tactic
val injection : term:Cic.term -> ProofEngineTypes.tactic
val intros :
(* ANCORA DA DEBUGGARE *)
+exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
+exception TheSelectedTermsMustLiveInTheGoalContext
exception AllSelectedTermsMustBeConvertible;;
exception CannotGeneralizeInHypotheses;;
let generalize_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ~term pattern
+ pattern
=
let module PET = ProofEngineTypes in
- let generalize_tac mk_fresh_name_callback ~term (hyps_pat,concl_pat) status =
+ let generalize_tac mk_fresh_name_callback
+ ~pattern:(term,hyps_pat,concl_pat) status
+ =
if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ;
let (proof, goal) = status in
let module C = Cic in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let terms =
- let path =
- match concl_pat with
- None -> Cic.Implicit (Some `Hole)
- | Some path -> path in
- let roots = ProofEngineHelpers.select ~term:ty ~pattern:path in
- List.fold_left
- (fun acc (i, r) ->
- ProofEngineHelpers.find_subterms
- ~eq:ProofEngineReduction.alpha_equivalence ~wanted:term r @ acc
- ) [] roots
- in
- let typ =
- let typ,u =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- (* We need to check that all the convertibility of all the terms *)
- ignore (
- (* TASSI: FIXME *)
- List.fold_left
- (fun u t ->
- let b,u1 = CicReduction.are_convertible context term t u in
- if not b then
- raise AllSelectedTermsMustBeConvertible
- else
- u1
- ) u terms) ;
- typ
- in
- PET.apply_tactic
- (T.thens
+ let terms_with_context =
+ ProofEngineHelpers.select ~context ~term:ty ~pattern:(term,concl_pat) in
+ let typ,term =
+ match terms_with_context, term with
+ [], None ->
+ raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+ | _, Some term
+ | (_,term)::_, None ->
+ fst
+ (CicTypeChecker.type_of_aux' metasenv context term
+ CicUniv.empty_ugraph),
+ term in
+ (* We need to check:
+ 1. whether they live in the context of the goal;
+ if they do they are also well-typed since they are closed subterms
+ of a well-typed term in the well-typed context of the well-typed
+ term
+ 2. whether they are convertible
+ *)
+ ignore (
+ (* TASSI: FIXME *)
+ List.fold_left
+ (fun u (context_of_t,t) ->
+ (* 1 *)
+ begin
+ try
+ ignore
+ (CicMetaSubst.delift_rels [] metasenv
+ (List.length context_of_t - List.length context) t)
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ raise TheSelectedTermsMustLiveInTheGoalContext
+ end;
+ (* 2 *)
+ let b,u1 = CicReduction.are_convertible context term t u in
+ if not b then
+ raise AllSelectedTermsMustBeConvertible
+ else
+ u1
+ ) CicUniv.empty_ugraph terms_with_context) ;
+ PET.apply_tactic
+ (T.thens
~start:
(P.cut_tac
(C.Prod(
typ,
(ProofEngineReduction.replace_lifting_csc 1
~equality:(==)
- ~what:terms
- ~with_what:(List.map (function _ -> C.Rel 1) terms)
+ ~what:(List.map snd terms_with_context)
+ ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
~where:ty)
)))
~continuations:
T.id_tac])
status
in
- PET.mk_tactic (generalize_tac mk_fresh_name_callback ~term pattern)
+ PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
;;
val generalize_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- term:Cic.term -> ProofEngineTypes.pattern ->
+ ProofEngineTypes.pattern ->
ProofEngineTypes.tactic
projects / helm.git / commitdiff