decompose tactic: user provided premise and types removed.
The decomposable types are now the non-recursive inductive
types without right parameters and are auto-detected
[T.Branch (qs, ""); p2; p1]
and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
+ | C.AAppl (_, hd :: tl) as v ->
if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
[T.LetIn (name, v, dtext ^ text)]
end
- | v ->
- [T.LetIn (name, v, dtext)]
+ | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
+ begin match Cn.mk_ind st.context id uri tyno outty arg cases with
+ | None -> [T.LetIn (name, v, dtext)]
+ | Some v -> mk_fwd_proof st dtext name v
+ end
+ | v ->
+ [T.LetIn (name, v, dtext)]
and mk_proof st = function
- | C.ALambda (_, name, v, t) as what ->
+ | C.ALambda (_, name, v, t) as what ->
let entry = Some (name, C.Decl (cic v)) in
let intro = get_intro name t in
let ety = match get_inner_types st what with
| None -> None
in
mk_proof (add st entry intro ety) t
- | C.ALetIn (_, name, v, t) as what ->
+ | C.ALetIn (_, name, v, t) as what ->
let proceed, dtext = test_depth st in
let script = if proceed then
let entry = Some (name, C.Def (cic v, None)) in
[T.Apply (what, dtext)]
in
mk_intros st script
- | C.ARel _ as what ->
+ | C.ARel _ as what ->
let _, dtext = test_depth st in
let text = "assumption" in
let script = [T.Apply (what, dtext ^ text)] in
mk_intros st script
- | C.AMutConstruct _ as what ->
+ | C.AMutConstruct _ as what ->
let _, dtext = test_depth st in
let script = [T.Apply (what, dtext)] in
mk_intros st script
- | C.AAppl (_, hd :: tl) as t ->
+ | C.AAppl (_, hd :: tl) as t ->
let proceed, dtext = test_depth st in
let script = if proceed then
let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
[T.Apply (t, dtext)]
in
mk_intros st script
- | t ->
+ | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
+ begin match Cn.mk_ind st.context id uri tyno outty arg cases with
+ | None ->
+ let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
+ let script = [T.Note text] in
+ mk_intros st script
+ | Some t -> mk_proof st t
+ end
+ | t ->
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
let script = [T.Note text] in
mk_intros st script
* http://cs.unibo.it/helm/.
*)
-module C = Cic
+module C = Cic
+module E = CicEnvironment
+module Un = CicUniv
+module TC = CicTypeChecker
+module D = Deannotate
+module UM = UriManager
+
+module T = ProceduralTypes
+
+(* helpers ******************************************************************)
+
+let cic = D.deannotate_term
+
+let get_ind_type uri tyno =
+ match E.get_obj Un.empty_ugraph uri with
+ | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
+ | _ -> assert false
+
+let get_default_eliminator context uri tyno ty =
+ let _, (name, _, _, _) = get_ind_type uri tyno in
+ let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
+ let ext = match sort with
+ | C.Sort C.Prop -> "_ind"
+ | C.Sort C.Set -> "_rec"
+ | C.Sort C.CProp -> "_rec"
+ | C.Sort (C.Type _) -> "_rect"
+ | C.Meta (_,_) -> assert false
+ | _ -> assert false
+ in
+ let buri = UM.buri_of_uri uri in
+ let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
+ C.Const (uri, [])
+
+(* proof construction *******************************************************)
let rec need_whd i = function
| C.ACast (_, t, _) -> need_whd i t
| C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
in
lift_term k
+
+let fake_annotate c =
+ let get_binder c m =
+ try match List.nth c (pred m) with
+ | Some (C.Name s, _) -> s
+ | _ -> assert false
+ with
+ | Invalid_argument _ -> assert false
+ in
+ let mk_decl n v = Some (n, C.Decl v) in
+ let mk_def n v = Some (n, C.Def (v, None)) in
+ let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
+ let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
+ let rec ann_xns c (uri, t) = uri, ann_term c t
+ and ann_ms c = function
+ | None -> None
+ | Some t -> Some (ann_term c t)
+ and ann_fix newc c (name, i, ty, bo) =
+ "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
+ and ann_cofix newc c (name, ty, bo) =
+ "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
+ and ann_term c = function
+ | C.Sort sort -> C.ASort ("", sort)
+ | C.Implicit ann -> C.AImplicit ("", ann)
+ | C.Rel m -> C.ARel ("", "", m, get_binder c m)
+ | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
+ | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
+ | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
+ | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
+ | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
+ | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
+ | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
+ | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
+ | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
+ | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
+ | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
+ | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
+ | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
+ in
+ ann_term c
+
+let rec add_abst n t =
+ if n <= 0 then t else
+ let t = C.ALambda ("", C.Anonymous, C.AImplicit ("", None), lift 0 1 t) in
+ add_abst (pred n) t
+
+let mk_ind context id uri tyno outty arg cases =
+ let lpsno, (_, _, arity, constructors) = get_ind_type uri tyno in
+ let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
+ let ps = match inty with
+ | C.MutInd _ -> []
+ | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
+ | _ -> assert false
+ in
+ let lps, rps = T.list_split lpsno ps in
+ let eliminator = get_default_eliminator context uri tyno inty in
+ let arg_ref = T.mk_arel 0 "" in
+ let body = C.AMutCase (id, uri, tyno, outty, arg_ref, cases) in
+ let predicate = add_abst (succ (List.length rps)) body in
+ None
val need_whd: int -> Cic.annterm -> bool
val lift: int -> int -> Cic.annterm -> Cic.annterm
+
+val mk_ind:
+ Cic.context -> Cic.id -> UriManager.uri -> int ->
+ Cic.annterm -> Cic.annterm -> Cic.annterm list ->
+ Cic.annterm option
type ('term, 'lazy_term, 'ident) pattern =
'lazy_term option * ('ident * 'term) list * 'term option
-type ('term, 'ident) type_spec =
- | Ident of 'ident
- | Type of UriManager.uri * int
-
type 'lazy_term reduction =
[ `Normalize
| `Reduce
| Constructor of loc * int
| Contradiction of loc
| Cut of loc * 'ident option * 'term
- | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
+ | Decompose of loc * 'ident list
| Demodulate of loc
| Destruct of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| Cut (_, ident, term) ->
"cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
- | Decompose (_, [], what, names) ->
- sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names))
- | Decompose (_, types, what, names) ->
- let to_ident = function
- | Ident id -> id
- | Type _ -> assert false
- in
- let types = List.rev_map to_ident types in
- sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
+ | Decompose (_, names) ->
+ sprintf "decompose%s" (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
| Destruct (_, term) -> "destruct " ^ term_pp term
| Elim (_, term, using, num, idents) ->
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.Decompose (_, types, what, names) ->
- let to_type = function
- | GrafiteAst.Type (uri, typeno) -> uri, Some typeno
- | GrafiteAst.Ident _ -> assert false
- in
- let user_types = List.rev_map to_type types in
- let dbd = LibraryDb.instance () in
+ | GrafiteAst.Decompose (_, names) ->
let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+ Tactics.decompose ~mk_fresh_name_callback ()
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Cut (loc, ident, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate (metasenv,types) = function
- | GrafiteAst.Type _ -> assert false
- | GrafiteAst.Ident id ->
- (match
- disambiguate_term context metasenv
- (CicNotationPt.Ident(id, None))
- with
- | metasenv,Cic.MutInd (uri, tyno, _) ->
- metasenv,(GrafiteAst.Type (uri, tyno) :: types)
- | _ ->
- raise (GrafiteDisambiguator.DisambiguationError
- (0,[[[],[],None,lazy "Decompose works only on inductive types",true]])))
- in
- let metasenv,types =
- List.fold_left disambiguate (metasenv,[]) types
- in
- metasenv,GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Decompose (loc, names) ->
+ metasenv,GrafiteAst.Decompose (loc, names)
| GrafiteAst.Demodulate loc ->
metasenv,GrafiteAst.Demodulate loc
| GrafiteAst.Destruct (loc,term) ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
- idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
- let types = match types with None -> [] | Some types -> types in
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
- let to_spec id = GrafiteAst.Ident id in
- GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+ GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
(* $Id$ *)
-module C = Cic
-module P = PrimitiveTactics
-module T = Tacticals
-module S = ProofEngineStructuralRules
-module F = FreshNamesGenerator
-module E = ProofEngineTypes
-module H = ProofEngineHelpers
-module R = ReductionTactics
-
-(*
-(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
-let search_inductive_types ty =
- let rec aux types = function
- | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) ->
- (uri, typeno) :: types
- | C.Appl applist -> List.fold_left aux types applist
- | _ -> types
- in
- aux [] ty
-(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *)
-*)
+module C = Cic
+module P = PrimitiveTactics
+module T = Tacticals
+module S = ProofEngineStructuralRules
+module F = FreshNamesGenerator
+module PET = ProofEngineTypes
+module H = ProofEngineHelpers
+module RT = ReductionTactics
+module E = CicEnvironment
+module R = CicReduction
+module Un = CicUniv
+
+(* from ProceduralClasify ***************************************************)
+
+let split c t =
+ let add s v c = Some (s, C.Decl v) :: c in
+ let rec aux whd a n c = function
+ | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
+ | v when whd -> v :: a, n
+ | v -> aux true a n c (R.whd ~delta:true c v)
+ in
+ aux false [] 0 c t
-(* unexported tactics *******************************************************)
+(****************************************************************************)
type type_class = Other
| Ind
let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
+let get_inductive_type uri tyno =
+ match E.get_obj Un.empty_ugraph uri with
+ | C.InductiveDefinition (tys, _, lpsno, _), _ ->
+ let _, inductive, arity, _ = List.nth tys tyno in
+ lpsno, inductive, arity
+ | _ -> assert false
+
+let rec check_type = function
+ | C.MutInd (uri, tyno, _) ->
+ let lpsno, inductive, arity = get_inductive_type uri tyno in
+ let _, psno = split [] arity in
+ if lpsno <> psno && inductive then Other else Ind
+(* | C.Const (uri, _) as t ->
+ if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other
+*) | C.Appl (hd :: tl) -> check_type hd
+ | _ -> Other
+
+(* unexported tactics *******************************************************)
+
let rec scan_tac ~old_context_length ~index ~tactic =
let scan_tac status =
let (proof, goal) = status in
let tac = T.then_ ~start:(tactic ~what)
~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic)
in
- try E.apply_tactic tac status
- with E.Fail _ -> aux (pred index)
+ try PET.apply_tactic tac status
+ with PET.Fail _ -> aux (pred index)
in aux (index + context_length - old_context_length)
in
- E.mk_tactic scan_tac
-
-let rec check_types types = function
- | C.MutInd (uri, typeno, _) ->
- if List.mem (uri, Some typeno) types then Ind else Other
- | C.Const (uri, _) as t ->
- if List.mem (uri, None) types then Con (E.const_lazy_term t) else Other
- | C.Appl (hd :: tl) -> check_types types hd
- | _ -> Other
+ PET.mk_tactic scan_tac
-let elim_clear_unfold_tac ~mk_fresh_name_callback ~types ~what =
+let elim_clear_unfold_tac ~mk_fresh_name_callback ~what =
let elim_clear_unfold_tac status =
let (proof, goal) = status in
let _, metasenv, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = H.lookup_type metasenv context what in
- match check_types types ty with
- | Ind ->
- let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
- ~continuation:(S.clear [what])
- in
- E.apply_tactic tac status
- | Con t ->
- let tac = R.unfold_tac (Some t) ~pattern:(premise_pattern what) in
- E.apply_tactic tac status
+ let tac = match check_type ty with
+ | Ind -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+ ~continuation:(S.clear [what])
+ | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what)
| Other ->
- raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
+ let msg = "unexported elim_clear: not an decomposable type" in
+ raise (PET.Fail (lazy msg))
+ in
+ PET.apply_tactic tac status
in
- E.mk_tactic elim_clear_unfold_tac
+ PET.mk_tactic elim_clear_unfold_tac
(* elim type ****************************************************************)
let tac =
T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
in
- E.apply_tactic tac status
+ PET.apply_tactic tac status
in
- E.mk_tactic elim_type_tac
+ PET.mk_tactic elim_type_tac
(* decompose ****************************************************************)
(* roba seria ------------------------------------------------------------- *)
-let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
- ?(user_types=[]) ?what ~dbd =
+let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in
let _, metasenv,_,_, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
- let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback ~types in
+ let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in
let old_context_length = List.length context in
- let tac = match what with
- | Some what ->
- T.then_ ~start:(tactic ~what)
- ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
- | None ->
- scan_tac ~old_context_length ~index:old_context_length ~tactic
+ let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
in
- E.apply_tactic tac status
+ PET.apply_tactic tac status
in
- E.mk_tactic decompose_tac
+ PET.mk_tactic decompose_tac
val decompose_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?user_types:((UriManager.uri * int option) list) ->
- ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ unit -> ProofEngineTypes.tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jan 24 20:31:34 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Feb 21 14:36:23 CET 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
Cic.term -> ProofEngineTypes.tactic
val decompose :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?user_types:(UriManager.uri * int option) list ->
- ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ unit -> ProofEngineTypes.tactic
val demodulate :
dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
val destruct : term:Cic.term -> ProofEngineTypes.tactic
<title>decompose</title>
<titleabbrev>decompose</titleabbrev>
<para><userinput>
- decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>)
- H as H<subscript>1</subscript> ... H<subscript>m</subscript>
+ decompose as H<subscript>1</subscript> ... H<subscript>m</subscript>
</userinput></para>
<para>
<variablelist>
<listitem>
<para>
<emphasis role="bold">decompose</emphasis>
- [<emphasis role="bold">(</emphasis>
- &id;…
- <emphasis role="bold">)</emphasis>]
- [&id;]
[<emphasis role="bold">as</emphasis> &id;…]
</para>
</listitem>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>
- <command>H</command> must inhabit one inductive type among
- <command>
- T<subscript>1</subscript> ... T<subscript>n</subscript>
- </command>
- and the types of a predefined list.
- </para>
+ <para>None.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
<para>
- Runs <command>
- elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
- </command>, clears <command>H</command> and tries to run itself
- recursively on each new identifier introduced by
+ For each each premise <command>H</command>
+ of type <command>T</command> in the current context
+ where <command>T</command> is a non-recursive inductive type
+ withour right parameters, the tactic runs
+ <command>
+ elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command>, clears <command>H</command> and runs itself
+ recursively on each new premise introduced by
<command>elim</command> in the opened sequents.
- If <command>H</command> is not provided tries this operation on
- each premise in the current context.
</para>
</listitem>
</varlistentry>
projects / helm.git / commitdiff