From 61d82f6f49845fe5111969156945accf21fb5a70 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 13 Nov 2007 16:28:34 +0000 Subject: [PATCH] - ProofEngineHelpers: namer_of moved to GrafiteEngine - DestructTactic: unexported destruct_tac now uses lazy terms --- .../grafite_engine/grafiteEngine.ml | 42 +++-- .../components/tactics/destructTactic.ml | 168 +++++++----------- .../components/tactics/proofEngineHelpers.ml | 17 -- .../components/tactics/proofEngineHelpers.mli | 5 - 4 files changed, 96 insertions(+), 136 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 0d2fb682e..afcbf7f26 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -42,6 +42,23 @@ type options = { clean_baseuri: bool } +(** create a ProofEngineTypes.mk_fresh_name_type function which uses given + * names as long as they are available, then it fallbacks to name generation + * using FreshNamesGenerator module *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = match List.nth names !count with + | Some s -> Cic.Name s + | None -> Cic.Anonymous + in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ + let rec tactic_of_ast status ast = let module PET = ProofEngineTypes in match ast with @@ -75,7 +92,7 @@ let rec tactic_of_ast status ast = Tactics.auto ~params ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Cases (_, what, (howmany, names)) -> - Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names) what | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what @@ -83,24 +100,24 @@ let rec tactic_of_ast status ast = | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> Tactics.compose times t1 t2 ?howmany - ~mk_fresh_name_callback:(PEH.namer_of names) + ~mk_fresh_name_callback:(namer_of names) | GrafiteAst.Contradiction _ -> Tactics.contradiction | GrafiteAst.Constructor (_, n) -> Tactics.constructor n | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.cut ~mk_fresh_name_callback:(PEH.namer_of names) term + Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | GrafiteAst.Decompose (_, names) -> - let mk_fresh_name_callback = PEH.namer_of names in + let mk_fresh_name_callback = namer_of names in Tactics.decompose ~mk_fresh_name_callback () | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) ~pattern what | GrafiteAst.ElimType (_, what, using, (depth, names)) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what | GrafiteAst.Exact (_, term) -> Tactics.exact term | GrafiteAst.Exists _ -> Tactics.exists @@ -125,24 +142,24 @@ let rec tactic_of_ast status ast = Tactics.fold ~reduction ~term ~pattern | GrafiteAst.Fourier _ -> Tactics.fourier | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(LibraryDb.instance ()) hyp | GrafiteAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.generalize ~mk_fresh_name_callback:(PEH.namer_of names) pattern + Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern | GrafiteAst.IdTac _ -> Tactics.id | GrafiteAst.Intros (_, (howmany, names)) -> PrimitiveTactics.intros_tac ?howmany - ~mk_fresh_name_callback:(PEH.namer_of names) () + ~mk_fresh_name_callback:(namer_of names) () | GrafiteAst.Inversion (_, term) -> Tactics.inversion term | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.lapply ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ~linear ?how_many ~to_what what | GrafiteAst.Left _ -> Tactics.left | GrafiteAst.LetIn (loc,term,name) -> - Tactics.letin term ~mk_fresh_name_callback:(PEH.namer_of [Some name]) + Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name]) | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with | `Normalize -> Tactics.normalize ~pattern @@ -155,7 +172,7 @@ let rec tactic_of_ast status ast = Tactics.replace ~pattern ~with_what | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> EqualityTactics.rewrite_tac ~direction ~pattern t -(* to be replaced with ~mk_fresh_name_callback:(PEH.namer_of names) *) +(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *) (List.map (function Some s -> s | None -> assert false) names) | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring @@ -204,7 +221,6 @@ let classify_tactic tactic = | _ -> false let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= - let module PEH = ProofEngineHelpers in (* let print_m name metasenv = prerr_endline (">>>>> " ^ name); prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index ea871a0d4..8164fc5f6 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/components/tactics/destructTactic.ml @@ -39,7 +39,6 @@ module RT = ReductionTactics module PEH = ProofEngineHelpers module ET = EqualityTactics module DTI = DoubleTypeInference -module FNG = FreshNamesGenerator let debug = false let debug_print = @@ -244,40 +243,25 @@ let clear_term first_time lterm = in PET.mk_tactic clear_term -let simpl_in_term context = function - | Cic.Rel i -> - let name = match List.nth context (pred i) with - | Some (Cic.Name s, Cic.Def _) -> s - | Some (Cic.Name s, Cic.Decl _) -> s - | _ -> assert false - in - RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) - | _ -> T.id_tac - -let mk_fresh_name metasenv context name typ = - let name = C.Name name in - match FNG.mk_fresh_name ~subst:[] metasenv context name ~typ with - | C.Name s -> s - | C.Anonymous -> assert false - let exists context = function | C.Rel i -> List.nth context (pred i) <> None | _ -> true -let rec recur_on_child_tac name = +let rec recur_on_child_tac ~before = let recur_on_child status = let (proof, goal) = status in let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - debug_print (lazy ("\nrecur_on_child su: " ^ name)); + debug_print (lazy ("\nrecur_on_child")); debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - let rec search_name i = function - | [] -> T.id_tac - | Some (Cic.Name n, _) :: _ when n = name -> - destruct ~first_time:false (Cic.Rel i) - | _ :: tl -> search_name (succ i) tl + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug in - PET.apply_tactic (search_name 1 context) status + let lterm = mk_lterm (Cic.Rel 1) in + let continuation = destruct ~first_time:false lterm in + let tactic = T.then_ ~start:before ~continuation in + PET.apply_tactic tactic status in PET.mk_tactic recur_on_child @@ -442,13 +426,10 @@ and injection_tac ~lterm ~i ~continuation = PET.mk_tactic fill_cut in debug_print (lazy ("CUT: " ^ pp context cutted)); - let name = mk_fresh_name metasenv context "Hcut" cutted in - let mk_fresh_name_callback = PEH.namer_of [Some name] in - debug_print (lazy ("figlio: " ^ name)); let tactic = - T.thens ~start: (P.cut_tac ~mk_fresh_name_callback cutted) + T.thens ~start: (P.cut_tac cutted) ~continuations:[ - T.seq ~tactics:[continuation; recur_on_child_tac name]; + recur_on_child_tac continuation; fill_cut_tac term ] in @@ -474,17 +455,14 @@ 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 = - T.seq ~tactics:[continuation; recur_on_child_tac name] - in - debug_print (lazy ("figlio: " ^ name)); + let ok_tactic = recur_on_child_tac continuation 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 term = +and destruct ~first_time lterm = let are_convertible hd1 hd2 metasenv context = fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph) in @@ -492,38 +470,38 @@ and destruct ~first_time term = let (proof, goal) = status in let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - debug_print (lazy ("\ndestruct di: " ^ pp context term)); - debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - let termty,_ = - CTC.type_of_aux' metasenv context term CU.empty_ugraph - in - debug_print (lazy ("\ndestruct su: " ^ pp context termty)); - let mk_lterm term c m ug = - let distance = List.length c - List.length context in - S.lift distance term, m, ug - in - let lterm = mk_lterm term in - let mk_subst_chain direction index with_what what = - let k = match term with C.Rel i -> i | _ -> -1 in - let rec traverse_context first_time j = function - | [] -> - let continuation = - T.seq ~tactics:[ - clear_term first_time lterm; - clear_term false (mk_lterm what); - clear_term false (mk_lterm with_what) - ] - in - subst_tac ~direction ~lterm ~where:None ~continuation - | 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) - ~continuation:(traverse_context false (succ j) tl) - | _ :: tl -> traverse_context first_time (succ j) tl + let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let tactic = if not (first_time || exists context term) then T.id_tac else begin + debug_print (lazy ("\ndestruct di: " ^ pp context term)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); + let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in + debug_print (lazy ("\ndestruct su: " ^ pp context termty)); + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug in - traverse_context first_time 1 context - in - let tac = match termty with + let lterm = mk_lterm term in + let mk_subst_chain direction index with_what what = + let k = match term with C.Rel i -> i | _ -> -1 in + let rec traverse_context first_time j = function + | [] -> + let continuation = + T.seq ~tactics:[ + clear_term first_time lterm; + clear_term false (mk_lterm what); + clear_term false (mk_lterm with_what) + ] + in + subst_tac ~direction ~lterm ~where:None ~continuation + | 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) + ~continuation:(traverse_context false (succ j) tl) + | _ :: tl -> traverse_context first_time (succ j) tl + in + traverse_context first_time 1 context + in + match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] when LibraryObjects.is_eq_URI equri -> begin match t1,t2 with @@ -579,46 +557,34 @@ and destruct ~first_time term = end | _ when first_time -> raise exn_nothingtodo | _ (* when not first time *) -> T.id_tac - in - PET.apply_tactic tac status + end in + PET.apply_tactic tactic status in PET.mk_tactic destruct -let lazy_destruct_tac ~first_time ~lterm = - let lazy_destruct status = +(* destruct performs either injection or discriminate or subst *) +let destruct_tac xterm = + let destruct status = let (proof, goal) = status in let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, _, _ = lterm context metasenv CU.empty_ugraph in - let tactic = - if exists context term then destruct ~first_time term else T.id_tac + let mk_lterm term c m ug = + let distance = List.length c - List.length context in + S.lift distance term, m, ug in - PET.apply_tactic tactic status - in - PET.mk_tactic lazy_destruct - -(* destruct performs either injection or discriminate *) -(* equivalent to Coq's "analyze equality" *) -let destruct_tac = function - | Some term -> destruct ~first_time:true term - | None -> - let destruct_all status = - let (proof, goal) = status in - let _,metasenv,_subst,_,_, _ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let mk_lterm term c m ug = - let distance = List.length c - List.length context in - S.lift distance term, m, ug - in - let rec mk_tactics first_time i tacs = function - | [] -> List.rev tacs - | Some _ :: tl -> - let lterm = mk_lterm (C.Rel i) in - let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in - mk_tactics false (succ i) tacs tl - | _ :: tl -> mk_tactics first_time (succ i) tacs tl - in - let tactics = mk_tactics false 1 [] context in - PET.apply_tactic (T.seq ~tactics) status + let tactics = match xterm with + | Some term -> [destruct ~first_time:true (mk_lterm term)] + | None -> + let rec mk_tactics first_time i tacs = function + | [] -> List.rev tacs + | Some _ :: tl -> + let lterm = mk_lterm (C.Rel i) in + let tacs = destruct ~first_time lterm :: tacs in + mk_tactics false (succ i) tacs tl + | _ :: tl -> mk_tactics first_time (succ i) tacs tl + in + mk_tactics false 1 [] context in - PET.mk_tactic destruct_all + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic destruct diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index 246751b32..b38512273 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -706,20 +706,3 @@ let relations_of_menv m c = let sort_metasenv (m : Cic.metasenv) = (MS.topological_sort m (relations_of_menv m) : Cic.metasenv) ;; - -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = match List.nth names !count with - | Some s -> Cic.Name s - | None -> Cic.Anonymous - in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index cc13d1ad7..39fb69b0d 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -128,8 +128,3 @@ val split_with_whd: Cic.context * Cic.term -> (Cic.context * Cic.term) list * int val split_with_normalize: Cic.context * Cic.term -> (Cic.context * Cic.term) list * int - -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type -- 2.39.2