]> matita.cs.unibo.it Git - helm.git/commitdiff
- ProofEngineHelpers: namer_of moved to GrafiteEngine
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 13 Nov 2007 16:28:34 +0000 (16:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 13 Nov 2007 16:28:34 +0000 (16:28 +0000)
- DestructTactic: unexported destruct_tac now uses lazy terms

helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/tactics/destructTactic.ml
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli

index 0d2fb682ed78b98ec293f6e26b6ce94353a7c1e2..afcbf7f26709a0ea6ddd875852b07a5e6a157b06 100644 (file)
@@ -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)
index ea871a0d4aff09e491194cf03d1dbf33ad0650b2..8164fc5f68a2165029697fc74b4fbff6e31060c9 100644 (file)
@@ -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
index 246751b32785f52b49cad40cff47f7172fffe469..b38512273081907ab6cff86c16cd56f35be304a1 100644 (file)
@@ -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
index cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2..39fb69b0d1067370a408c62be07cc495331516c1 100644 (file)
@@ -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