From: Ferruccio Guidi Date: Wed, 14 Nov 2007 20:28:58 +0000 (+0000) Subject: now destruct takes an optional list of term rather than a sigle optional term X-Git-Tag: 0.4.95@7852~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=42f2dc48b4fef5b404f406bf512d6a0cde35c067;p=helm.git now destruct takes an optional list of term rather than a sigle optional term --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 3e87ffba5..2b0f4db5f 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -71,7 +71,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | 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 diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index eb1a18e5a..cf9106ea3 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -68,13 +68,14 @@ let pp_intros_specs s = function | 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 = @@ -127,7 +128,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (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) @@ -159,7 +160,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = (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) -> diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index afcbf7f26..e8e3171a0 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -112,7 +112,7 @@ let rec tactic_of_ast status ast = | 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 diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 2fe6b9aae..53142e252 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -216,9 +216,13 @@ let rec disambiguate_tactic 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) -> @@ -264,12 +268,12 @@ let rec disambiguate_tactic 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 diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 83e9d10d8..a0fd33358 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -170,8 +170,8 @@ EXTEND 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 -> diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml index 8164fc5f6..a8bfc007d 100644 --- a/components/tactics/destructTactic.ml +++ b/components/tactics/destructTactic.ml @@ -247,7 +247,7 @@ let exists context = function | 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 @@ -259,13 +259,12 @@ let rec recur_on_child_tac ~before = 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) @@ -429,7 +428,7 @@ and injection_tac ~lterm ~i ~continuation = 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 @@ -438,7 +437,7 @@ and injection_tac ~lterm ~i ~continuation = 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 @@ -455,17 +454,18 @@ and subst_tac ~lterm ~direction ~where ~continuation = 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 @@ -492,10 +492,10 @@ and destruct ~first_time lterm = 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 @@ -519,7 +519,7 @@ and destruct ~first_time lterm = 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, @@ -563,7 +563,7 @@ and destruct ~first_time lterm = 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 @@ -572,9 +572,11 @@ let destruct_tac xterm = 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 -> diff --git a/components/tactics/destructTactic.mli b/components/tactics/destructTactic.mli index 0ecccdab0..cc3f0d5cf 100644 --- a/components/tactics/destructTactic.mli +++ b/components/tactics/destructTactic.mli @@ -27,4 +27,4 @@ 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 diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 45bfa7e3b..8c97039fb 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* 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 : @@ -32,7 +32,7 @@ val decompose : 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 ->