| SYMBOL "<" -> `RightToLeft ]
];
int: [ [ num = NUMBER -> int_of_string num ] ];
+ intros_names: [
+ [ idents = OPT ident_list0 ->
+ match idents with None -> [] | Some idents -> idents
+ ]
+ ];
intros_spec: [
[ OPT [ IDENT "names" ];
num = OPT [ num = int -> num ];
- idents = OPT ident_list0 ->
- let idents = match idents with None -> [] | Some idents -> idents in
+ idents = intros_names ->
num, idents
]
];
GrafiteAst.Assumption loc
| IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
+ | IDENT "cases"; what = tactic_term;
+ (num, idents) = intros_spec ->
+ GrafiteAst.Cases (loc, what, idents)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
mk_tactic (elim_tac ~term)
;;
+let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+ let cases_tac ~term (proof, goal) =
+ let module T = CicTypeChecker in
+ let module U = UriManager in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (curi,metasenv,proofbo,proofty) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
+ let (termty,metasenv',arguments,fresh_meta) =
+ TermUtil.saturate_term
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+ let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+ let uri,exp_named_subst,typeno,args =
+ match termty with
+ C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
+ | _ -> raise NotAnInductiveTypeToEliminate
+ in
+ let paramsno,patterns =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ C.InductiveDefinition (tys,_,paramsno,_),_ ->
+ let _,_,_,cl = List.nth tys typeno in
+ let rec aux n context t =
+ match n,CicReduction.whd context t with
+ 0,C.Prod (name,source,target) ->
+ let fresh_name =
+ mk_fresh_name_callback metasenv' context name
+ (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
+ ~typ:source
+ in
+ C.Lambda (fresh_name,C.Implicit None,
+ aux 0 (Some (fresh_name,C.Decl source)::context) target)
+ | n,C.Prod (name,source,target) ->
+ let fresh_name =
+ mk_fresh_name_callback metasenv' context name
+ (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
+ ~typ:source
+ in
+ aux (n-1) (Some (fresh_name,C.Decl source)::context) target
+ | 0,_ -> C.Implicit None
+ | _,_ -> assert false
+ in
+ paramsno,
+ List.map (function (_,cty) -> aux paramsno context cty) cl
+ | _ -> assert false
+ in
+ let outtype =
+ let target =
+ C.Lambda (C.Name "fixme",C.Implicit None,
+ ProofEngineReduction.replace_lifting
+ ~equality:(ProofEngineReduction.alpha_equivalence)
+ ~what:[CicSubstitution.lift (paramsno+1) term]
+ ~with_what:[C.Rel (paramsno+1)]
+ ~where:(CicSubstitution.lift (paramsno+1) ty))
+ in
+ let rec add_lambdas =
+ function
+ 0 -> target
+ | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
+ in
+ add_lambdas paramsno
+ in
+ let term_to_refine =
+ C.MutCase (uri,typeno,outtype,term,patterns)
+ in
+prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
+ let refined_term,_,metasenv'',_ =
+ CicRefine.type_of_aux' metasenv' context term_to_refine
+ CicUniv.empty_ugraph
+ in
+ let new_goals =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ in
+ let proof' = curi,metasenv'',proofbo,proofty in
+ let proof'', new_goals' =
+ apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+ in
+ (* The apply_tactic can have closed some of the new_goals *)
+ let patched_new_goals =
+ let (_,metasenv''',_,_) = proof'' in
+ List.filter
+ (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
+ ) new_goals @ new_goals'
+ in
+ proof'', patched_new_goals
+ in
+ mk_tactic (cases_tac ~term)
+;;
+
+
let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
?depth ?using what =
Tacticals.then_ ~start:(elim_tac ~term:what)
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 28 11:13:28 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Dec 20 23:48:06 CET 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
val auto :
params:(string * string) list ->
dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
+val cases_intros :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ Cic.term -> ProofEngineTypes.tactic
val change :
pattern:ProofEngineTypes.lazy_pattern ->
Cic.lazy_term -> ProofEngineTypes.tactic
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?user_types:(UriManager.uri * int option) list ->
?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate : dbd:HMysql.dbd ->
- universe:Universe.universe -> ProofEngineTypes.tactic
+val demodulate :
+ dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
val destruct : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
projects / helm.git / commitdiff