| Cut of loc * 'ident option * 'term
| Decompose of loc * 'ident option list
| Demodulate of loc
- | Destruct of loc * 'term option
+ | Destruct of loc * 'term list option
| Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
'ident intros_spec
| ElimType of loc * 'term * 'term option * 'ident intros_spec
| None, idents -> Printf.sprintf " %s%s" s (pp_idents idents)
| Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents)
-let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms)
let opt_string_pp = function
| None -> ""
| Some what -> what ^ " "
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
+ let pp_terms = pp_terms ~term_pp in
let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
let pp_reduction_kind = pp_reduction_kind ~term_pp in
let pp_tactic_pattern =
(pp_intros_specs "names " (None, names))
| Demodulate _ -> "demodulate"
| Destruct (_, None) -> "destruct"
- | Destruct (_, Some term) -> "destruct " ^ term_pp term
+ | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
| Elim (_, what, using, pattern, specs) ->
Printf.sprintf "elim %s%s %s%s"
(term_pp what)
(if linear then " linear " else "")
(match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
(term_pp term)
- (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
+ (match terms with [] -> "" | _ -> " to " ^ pp_terms terms)
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
| Left _ -> "left"
| LetIn (_, term, ident) ->
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
- | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm
+ | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
~pattern what
metasenv,GrafiteAst.Decompose (loc, names)
| GrafiteAst.Demodulate loc ->
metasenv,GrafiteAst.Demodulate loc
- | GrafiteAst.Destruct (loc, Some term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Destruct(loc, Some term)
+ | GrafiteAst.Destruct (loc, Some terms) ->
+ let map term (metasenv, terms) =
+ let metasenv, term = disambiguate_term context metasenv term in
+ metasenv, term :: terms
+ in
+ let metasenv, terms = List.fold_right map terms (metasenv, []) in
+ metasenv, GrafiteAst.Destruct(loc, Some terms)
| GrafiteAst.Destruct (loc, None) ->
metasenv,GrafiteAst.Destruct(loc,None)
| GrafiteAst.Exact (loc, term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Inversion (loc, term)
| GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
- let f term to_what =
- let metasenv,term = disambiguate_term context metasenv term in
- term :: to_what
+ let f term (metasenv, to_what) =
+ let metasenv, term = disambiguate_term context metasenv term in
+ metasenv, term :: to_what
in
- let to_what = List.fold_right f to_what [] in
- let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
+ let metasenv, what = disambiguate_term context metasenv what in
metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
| GrafiteAst.Left loc ->
metasenv,GrafiteAst.Left loc
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] ->
- GrafiteAst.Destruct (loc, xt)
+ | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+ GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
| C.Rel i -> List.nth context (pred i) <> None
| _ -> true
-let rec recur_on_child_tac ~before =
+let recur_on_child_tac ~before ~after =
let recur_on_child status =
let (proof, goal) = status in
let _, metasenv, _subst, _, _, _ = proof in
S.lift distance term, m, ug
in
let lterm = mk_lterm (Cic.Rel 1) in
- let continuation = destruct ~first_time:false lterm in
- let tactic = T.then_ ~start:before ~continuation in
+ let tactic = T.then_ ~start:before ~continuation:(after lterm) in
PET.apply_tactic tactic status
in
PET.mk_tactic recur_on_child
-and injection_tac ~lterm ~i ~continuation =
+let injection_tac ~lterm ~i ~continuation ~recur =
let give_name seed = function
| C.Name _ as name -> name
| C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
let tactic =
T.thens ~start: (P.cut_tac cutted)
~continuations:[
- recur_on_child_tac continuation;
+ recur_on_child_tac continuation recur;
fill_cut_tac term
]
in
in
PET.mk_tactic injection_tac
-and subst_tac ~lterm ~direction ~where ~continuation =
+let subst_tac ~lterm ~direction ~where ~continuation ~recur =
let subst_tac status =
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
debug_print (lazy ("nella premessa: " ^ name));
let pattern = None, [name, PET.hole], None in
let start = ET.rewrite_tac ~direction ~pattern term [] in
- let ok_tactic = recur_on_child_tac continuation in
+ let ok_tactic = recur_on_child_tac continuation recur in
T.if_ ~start ~continuation:ok_tactic ~fail:continuation
in
PET.apply_tactic tactic status
in
PET.mk_tactic subst_tac
-and destruct ~first_time lterm =
+let rec destruct ~first_time lterm =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
in
+ let recur = destruct ~first_time:false in
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
clear_term false (mk_lterm with_what)
]
in
- subst_tac ~direction ~lterm ~where:None ~continuation
+ subst_tac ~direction ~lterm ~where:None ~continuation ~recur
| Some (C.Name name, _) :: tl when j < index && j <> k ->
debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
- subst_tac ~direction ~lterm ~where:(Some name)
+ subst_tac ~direction ~lterm ~where:(Some name) ~recur
~continuation:(traverse_context false (succ j) tl)
| _ :: tl -> traverse_context first_time (succ j) tl
in
if are_convertible hd1 hd2 metasenv context then
traverse_list first_time (succ i) tl1 tl2
else
- injection_tac ~i ~lterm ~continuation:
+ injection_tac ~i ~lterm ~recur ~continuation:
(traverse_list false (succ i) tl1 tl2)
| _ -> assert false
(* i 2 termini hanno in testa lo stesso costruttore,
PET.mk_tactic destruct
(* destruct performs either injection or discriminate or subst *)
-let destruct_tac xterm =
+let destruct_tac xterms =
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let distance = List.length c - List.length context in
S.lift distance term, m, ug
in
- let tactics = match xterm with
- | Some term -> [destruct ~first_time:true (mk_lterm term)]
- | None ->
+ let tactics = match xterms with
+ | Some terms ->
+ let map term = destruct ~first_time:false (mk_lterm term) in
+ List.map map terms
+ | None ->
let rec mk_tactics first_time i tacs = function
| [] -> List.rev tacs
| Some _ :: tl ->
looking for constructors. If the two sides differ on two constructors,
it closes the current goal. If they differ by other two terms it introduces
an equality. *)
-val destruct_tac: Cic.term option -> ProofEngineTypes.tactic
+val destruct_tac: Cic.term list option -> ProofEngineTypes.tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Nov 7 13:24:27 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Nov 14 12:07:32 CET 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
unit -> ProofEngineTypes.tactic
val demodulate :
dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
-val destruct : Cic.term option -> ProofEngineTypes.tactic
+val destruct : Cic.term list option -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?depth:int ->
projects / helm.git / commitdiff