]> matita.cs.unibo.it Git - helm.git/commitdiff
elim tactic: now takes a pattern instead of just a term
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 13 Mar 2007 13:21:56 +0000 (13:21 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 13 Mar 2007 13:21:56 +0000 (13:21 +0000)
             works as before for now. the pattern wil be activated soon
Procedural:  cleaning up
ProofEngineReduction: new subst_inv function exactly inverts subst

18 files changed:
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralConversion.ml
helm/software/components/acic_procedural/proceduralConversion.mli
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/proofEngineReduction.ml
helm/software/components/tactics/proofEngineReduction.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/matitaGui.ml

index e3545f62a7c0f3e4b831f9e0141ef1a9052d8ae9..dbdfb979209b146c32ee303f89dbe1f599adb096 100644 (file)
@@ -55,10 +55,6 @@ type status = {
 
 (* helpers ******************************************************************)
 
-let identity x = x
-
-let comp f g x = f (g x)
-
 let cic = D.deannotate_term
 
 let split2_last l1 l2 =
@@ -166,39 +162,17 @@ let unused_premise = "UNUSED"
 
 let defined_premise = "DEFINED"
 
-let expanded_premise = "EXPANDED"
-
 let convert st ?name v = 
    match get_inner_types st v with
       | None          -> []
       | Some (st, et) ->
          let cst, cet = cic st, cic et in
         if PER.alpha_equivalence cst cet then [] else 
-        let e = Cn.mk_pattern [] (T.mk_arel 1 "") in
+        let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
         match name with
            | None    -> [T.Change (st, et, None, e, "")]
            | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
 
-let eta_expand n t =
-   let id = Ut.id_of_annterm t in
-   let ty = C.AImplicit ("", None) in
-   let name i = Printf.sprintf "%s%u" expanded_premise i in 
-   let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
-   let arg i n = T.mk_arel ((* n - *) succ i) (name (n - i - 1)) in
-   let rec aux i f a =
-      if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
-   in
-   let absts, args = aux 0 identity [] in
-   match Cn.lift 1 n t with
-      | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
-      | t                -> absts (C.AAppl ("", t :: args))  
-
-let appl_expand n = function
-   | C.AAppl (id, ts) -> 
-      let before, after = T.list_split (List.length ts + n) ts in
-      C.AAppl (id, C.AAppl ("", before) :: after)
-   | _                -> assert false
-
 let get_intro name t = 
 try
 match name with 
@@ -226,9 +200,8 @@ let rec mk_atomic st dtext what =
 
 and mk_fwd_rewrite st dtext name tl direction =   
    assert (List.length tl = 6);
-   let what, where = List.nth tl 5, List.nth tl 3 in
-   let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-   let e = Cn.mk_pattern rps predicate in
+   let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
    match where with
       | C.ARel (_, _, _, premise) ->
          let script, what = mk_atomic st dtext what in
@@ -237,19 +210,19 @@ and mk_fwd_rewrite st dtext name tl direction =
 
 and mk_rewrite st dtext script t what qs tl direction = 
    assert (List.length tl = 5);
-   let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-   let e = Cn.mk_pattern rps predicate in
+   let predicate = List.nth tl 2 in
+   let e = Cn.mk_pattern 1 predicate in
    List.rev script @ convert st t @
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 and mk_fwd_proof st dtext name = function
-   | C.ALetIn (_, n, v, t)                           ->
+   | C.ALetIn (_, n, v, t)      ->
       let entry = Some (n, C.Def (cic v, None)) in
       let intro = get_intro n t in
       let qt = mk_fwd_proof (add st entry intro) dtext name t in
       let qv = mk_fwd_proof st "" intro v in
       List.append qt qv
-   | C.AAppl (_, hd :: tl) as v                         -> 
+   | C.AAppl (_, hd :: tl) as v -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
       if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
       let ty = get_type "TC1" st hd in
@@ -262,14 +235,9 @@ and mk_fwd_proof st dtext name = function
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
            [T.LetIn (name, v, dtext ^ text)]
       end
-(*   | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
-      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
-         | None   -> [T.LetIn (name, v, dtext)] 
-         | Some v -> mk_fwd_proof st dtext name v
-      end
-*)   | C.ACast (_, v, _)                                  ->
-      mk_fwd_proof st dtext name v
-   | v                                                  ->
+   | C.AMutCase _               -> assert false
+   | C.ACast _                  -> assert false 
+   | v                          ->
       match get_inner_types st v with
          | Some (ity, _) ->
            let qs = [[T.Id ""]; mk_proof (next st) v] in
@@ -278,11 +246,11 @@ and mk_fwd_proof st dtext name = function
             [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t)                     ->
+   | C.ALambda (_, name, v, t)        ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
       mk_proof (add st entry intro) t
-   | C.ALetIn (_, name, v, t) as what              ->
+   | C.ALetIn (_, name, v, t) as what ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
@@ -293,27 +261,22 @@ and mk_proof st = function
         [T.Apply (what, dtext)]
       in
       mk_intros st script
-   | C.ARel _ as what                              ->
+   | C.ARel _ as what                 ->
       let _, dtext = test_depth st in
       let text = "assumption" in
       let script = [T.Apply (what, dtext ^ text)] in 
       mk_intros st script
-   | C.AMutConstruct _ as what                     ->
+   | C.AMutConstruct _ as what        ->
       let _, dtext = test_depth st in
       let script = [T.Apply (what, dtext)] in 
       mk_intros st script   
-   | C.AAppl (_, hd :: tl) as t                    ->
+   | C.AAppl (_, hd :: tl) as t       ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
          let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
          let premises, _ = P.split st.context ty in
-        let decurry = List.length classes - List.length tl in
-         if decurry <> 0 then
-           Printf.eprintf "DECURRY: %u %s\n" decurry (CicPp.ppterm (cic t));
-        assert (decurry = 0);
-        if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
-         if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
+        assert (List.length classes - List.length tl = 0);
         let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
@@ -327,9 +290,12 @@ and mk_proof st = function
               else if is_rewrite_left hd then 
                  mk_rewrite st dtext script t what qs tl true
               else   
-                 let using = Some hd in
+                  let l = succ (List.length tl) in
+                 let predicate = List.nth tl (l - i) in
+                  let e = Cn.mk_pattern j predicate in
+                 let using = Some hd in
                  List.rev script @ convert st t @
-                 [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
+                 [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")]
            | _                                                  ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
               let script, hd = mk_atomic st dtext hd in               
@@ -339,17 +305,9 @@ and mk_proof st = function
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | C.AMutCase (id, uri, tyno, outty, arg, cases) as t ->
-      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
-         | _ (* None *)  -> 
-            let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
-            let script = [T.Note text] in
-            mk_intros st script
-(*         | Some t -> mk_proof st t *)
-      end
-   | C.ACast (_, t, _)                             ->
-      mk_proof st t
-   | t                                             ->
+   | C.AMutCase _                     -> assert false
+   | C.ACast _                        -> assert false
+   | t                                ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
index d2d305ed4cffc959e107a274479389d42cfb8f64..5f705053a1a3e405903fa06d2a081f278c057ffb 100644 (file)
@@ -39,26 +39,6 @@ module M    = ProceduralMode
 
 let cic = D.deannotate_term
 
-let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
-      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
-      | _                                           -> assert false
-
-let get_default_eliminator context uri tyno ty =
-   let _, (name, _, _, _) = get_ind_type uri tyno in
-   let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
-   let ext = match sort with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
-      | C.Sort (C.Type _) -> "_rect" 
-      | C.Meta (_,_)      -> assert false
-      | _                 -> assert false
-   in
-   let buri = UM.buri_of_uri uri in
-   let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
-   C.Const (uri, [])
-
 let rec list_sub start length = function
    | _  :: tl when start  > 0 -> list_sub (pred start) length tl
    | hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl
@@ -98,46 +78,6 @@ let lift k n =
    in
    lift_term k
 
-let fake_annotate c =
-   let get_binder c m =
-      try match List.nth c (pred m) with
-        | Some (C.Name s, _) -> s
-        | _                  -> assert false
-      with
-         | Invalid_argument _ -> assert false 
-   in
-   let mk_decl n v = Some (n, C.Decl v) in
-   let mk_def n v = Some (n, C.Def (v, None)) in
-   let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
-   let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
-   let rec ann_xns c (uri, t) = uri, ann_term c t
-   and ann_ms c = function
-      | None   -> None
-      | Some t -> Some (ann_term c t)
-   and ann_fix newc c (name, i, ty, bo) =
-      "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_cofix newc c (name, ty, bo) =
-      "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
-   and ann_term c = function
-      | C.Sort sort -> C.ASort ("", sort)
-      | C.Implicit ann -> C.AImplicit ("", ann)
-      | C.Rel m -> C.ARel ("", "", m, get_binder c m)
-      | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
-      | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
-      | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
-      | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
-      | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
-      | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
-      | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
-      | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)      
-      | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
-      | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
-      | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
-      | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
-   in
-   ann_term c
-
 let clear_absts m =
    let rec aux k n = function
       | C.AImplicit (_, None) as t         -> t
@@ -152,42 +92,6 @@ let clear_absts m =
    in 
    aux m
 
-let mk_ind context id uri tyno outty arg cases =
-try
-   let sort_disp = 0 in
-   let is_recursive = function
-      | C.MutInd (u, no, _) -> UM.eq u uri && no = tyno
-      | _                   -> false
-   in
-   let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
-   let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
-   let ps = match Rd.whd ~delta:true context inty with
-      | C.MutInd _                  -> []
-      | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
-      | _                           -> assert false
-   in
-   let lps, rps = T.list_split lpsno ps in
-   let rpsno = List.length rps in
-   let eliminator = get_default_eliminator context uri tyno inty in
-   let eliminator = fake_annotate context eliminator in
-   let predicate = clear_absts rpsno (1 - sort_disp) outty in   
-   let map2 case (_, cty) = 
-      let map (h, case, k) premise = 
-         if h > 0 then pred h, lift k 1 case, k else
-        if is_recursive premise then 0, lift (succ k) 1 case, succ k else
-        0, case, succ k
-      in
-      let premises, _ = P.split context cty in
-      let _, lifted_case, _ =
-         List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
-      in
-      lifted_case
-   in
-   let lifted_cases = List.map2 map2 cases constructors in
-   let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   Some (C.AAppl (id, args))
-with Invalid_argument _ -> failwith "PCn.mk_ind"
-
 let hole id = C.AImplicit (id, Some `Hole)
 
 let meta id = C.AImplicit (id, None)
@@ -239,8 +143,6 @@ let generalize n =
    in
    gen_term 0
 
-let mk_pattern rps predicate =
-   let sort_disp = 0 in
-   let rpsno = List.length rps in
-   let body = generalize (rpsno + sort_disp) predicate in
-   clear_absts 0 (rpsno + sort_disp) body
+let mk_pattern rpsno predicate =
+   let body = generalize rpsno predicate in
+   clear_absts 0 rpsno body
index 3b65200144a1e9f40eee72bf0a094fdb9d76d39d..5cbb75da26efc3d86b70fd5142f1e37c1adc6f29 100644 (file)
@@ -25,9 +25,4 @@
 
 val lift: int -> int -> Cic.annterm -> Cic.annterm
 
-val mk_ind: 
-   Cic.context -> Cic.id -> UriManager.uri -> int -> 
-   Cic.annterm -> Cic.annterm -> Cic.annterm list ->
-   Cic.annterm option
-
-val mk_pattern: Cic.annterm list -> Cic.annterm -> Cic.annterm
+val mk_pattern: int -> Cic.annterm -> Cic.annterm
index 91f2408b94ba6ea9c15d5e6fee582381a6536a5d..3ef27ea4020392e83173ee70dbc0d8af52247f69 100644 (file)
@@ -86,7 +86,7 @@ type step = Note of note
          | Cut of name * what * note
          | LetIn of name * what * note
          | Rewrite of how * what * where * pattern * note
-         | Elim of what * using option * note
+         | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note 
          | ClearBody of name * note
@@ -137,8 +137,9 @@ let mk_rewrite direction what where pattern =
    let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
    mk_tactic tactic
 
-let mk_elim what using =
-   let tactic = G.Elim (floc, what, using, Some 0, []) in
+let mk_elim what using pattern =
+   let pattern = Some what, [], Some pattern in
+   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =
@@ -178,7 +179,7 @@ let rec render_step sep a = function
    | Cut (n, t, s)           -> mk_note s :: cont sep (mk_cut n t :: a)
    | LetIn (n, t, s)         -> mk_note s :: cont sep (mk_letin n t :: a)
    | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a)
-   | Elim (t, xu, s)         -> mk_note s :: cont sep (mk_elim t xu :: a)
+   | Elim (t, xu, e, s)      -> mk_note s :: cont sep (mk_elim t xu e :: a)
    | Apply (t, s)            -> mk_note s :: cont sep (mk_apply t :: a)
    | Change (t, _, w, e, s)  -> mk_note s :: cont sep (mk_change t w e :: a)
    | ClearBody (n, s)        -> mk_note s :: cont sep (mk_clearbody n :: a)
index 33a7e9c05c51e16a8f23b97407678daeb4a2e5fe..97ca7fdbb98bd21518673169db3d2d97fcd4f2f0 100644 (file)
@@ -53,7 +53,7 @@ type step = Note of note
           | Cut of name * what * note
           | LetIn of name * what * note
          | Rewrite of how * what * where * pattern * note
-         | Elim of what * using option * note
+         | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note
          | ClearBody of name * note
index 1ec71be92481e826763b18e81f4c6cb7bd244ad6..b5e75712fb7ea6a6e7c467eb0f3b3f0029efe3b3 100644 (file)
@@ -55,7 +55,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Decompose of loc * 'ident list
   | Demodulate of loc
   | Destruct of loc * 'term
-  | Elim of loc * 'term * 'term option * int option * 'ident list
+  | Elim of loc * ('term, 'lazy_term, 'ident) pattern * 'term option * 
+            int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
   | Exists of loc
index e433c9b7b73cf0aa4b261020e8a9287fbe6422af..e8fd2fe022b9c2a72b54f67ba16375c1d41f9586 100644 (file)
@@ -99,10 +99,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "decompose%s" (pp_intros_specs (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
-  | Elim (_, term, using, num, idents) ->
-      sprintf "elim " ^ term_pp term ^
+  | Elim (_, pattern, using, num, idents) ->
+      sprintf "elim %s%s%s" 
+      (pp_tactic_pattern pattern)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
-      ^ pp_intros_specs (num, idents
+      (pp_intros_specs (num, idents)
   | ElimType (_, term, using, num, idents) ->
       sprintf "elim type " ^ term_pp term ^
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
index db08a6038f86bcf08c23f6fc33ec3994ef79010e..4c177fee76d3c6245ec47091af00f15427c733a7 100644 (file)
@@ -87,9 +87,9 @@ let tactic_of_ast status ast =
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
-  | GrafiteAst.Elim (_, what, using, depth, names) ->
+  | GrafiteAst.Elim (_, pattern, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
-        what
+        pattern
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
index cc8360c28f51d0728996cdb37c7851e11cd69965..97f0d5e85892df5b5933cf706d5b5e69d9ec2144 100644 (file)
@@ -158,13 +158,13 @@ let disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
+    | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
+       let pattern = disambiguate_pattern pattern in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents)
+    | GrafiteAst.Elim (loc, pattern, None, depth, idents) ->
+       let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents)
     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
index 3653c46069adc15ff3a2be2aa7edc7ca9693ea1f..dac05d7bdd056d83d146bbef82e03d886efc6742 100644 (file)
@@ -164,8 +164,12 @@ EXTEND
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;
+       (num, idents) = intros_spec ->
+       let pattern = Some what, [], Some Ast.UserInput in
+       GrafiteAst.Elim (loc, pattern, using, num, idents)
+    | IDENT "elim"; pattern = pattern_spec; using = using;
       (num, idents) = intros_spec ->
-       GrafiteAst.Elim (loc, what, using, num, idents)
+       GrafiteAst.Elim (loc, pattern, using, num, idents)    
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
        GrafiteAst.ElimType (loc, what, using, num, idents)
index 110f72fb1fb4c5fb511be332f50ff552e858c539..189cd9079b4fd429a330948cbb535b720a3a8593 100644 (file)
@@ -127,11 +127,12 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
   let proof' = (n,metasenv,bo,ty,attrs) in
+   let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
    ProofEngineTypes.apply_tactic (
    Tacticals.thens
     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
     ~continuations:
-     [ Tactics.elim_intros (Cic.Rel 1)
+     [ Tactics.elim_intros pattern 
         ~mk_fresh_name_callback:
           (let i = ref 0 in
             fun _ _ _  ~typ ->
@@ -146,7 +147,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
 ;;
 
 let andelim t id1 t1 id2 t2 = 
- Tactics.elim_intros t
+ Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
       ~mk_fresh_name_callback:
         (let i = ref 0 in
           fun _ _ _  ~typ ->
@@ -250,8 +251,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- (*BUG here: pat unused *)
- Tactics.elim_intros ~depth:0 t
+ let pattern = Some (fun c m u -> t, m, u), [], Some pat in
+ Tactics.elim_intros ~depth:0 pattern
 ;;
 
 let case id ~params =
index e74886e95e1146235ef0114fd3b350d4360a5e13..85eade2d08e0291ac53b7a5cab724f47b4831e26 100644 (file)
@@ -127,9 +127,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
+      let pattern = PET.conclusion_pattern (Some (C.Rel index)) in
       let tac = 
          if check_type sorts metasenv context (S.lift index ty) then 
-            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern)
                    ~continuation:(PESR.clear [what])
         else 
            let msg = "unexported elim_clear: not an decomposable type" in
@@ -144,12 +145,13 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
 let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
   ?using what
 =
-  let elim what =
-    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+  let elim =
+    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
   in
   let elim_type_tac status =
+    let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in
     let tac =
-      T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+      T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac]
     in
     PET.apply_tactic tac status
   in
index 60eb4dc5b54579611febe23bee2fdff84449c437..2c22aa5ec2c10307dc308f44882367817db9a621 100644 (file)
@@ -477,7 +477,7 @@ let exact_tac ~term =
   mk_tactic (exact_tac ~term)
 
 (* not really "primitive" tactics .... *)
-let elim_tac ?using ~term = 
+let elim_tac ?using pattern = 
  let elim_tac (proof, goal) =
   let module T = CicTypeChecker in
   let module U = UriManager in
@@ -485,6 +485,10 @@ let elim_tac ?using ~term =
   let module C = Cic in
    let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let term, metasenv, _ = match pattern with 
+       | Some f, [], Some _ -> f context metasenv CicUniv.empty_ugraph
+       | _                  -> assert false
+    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) =
@@ -534,7 +538,27 @@ let elim_tac ?using ~term =
           | _ -> 0
         in
          let args_no = find_args_no ety in
-         let term_to_refine =
+(* we find the predicate for the eliminator as in the rewrite tactic ********)
+(*   
+   let fresh_name = 
+       FreshNamesGenerator.mk_fresh_name 
+       ~subst:[] metasenv' context C.Anonymous ~typ:termty in
+  let lifted_gty = S.lift 1 ty in
+  let lifted_conjecture =
+    metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in
+  let lifted_t1 = S.lift 1 t1x in
+  let lifted_pattern =
+    let lifted_concl_pat =
+      match concl_pat with
+      | None -> None
+      | Some term -> Some (S.lift 1 term) in
+    Some (fun c m u -> 
+       let distance  = pred (List.length c - List.length context) in
+       S.lift distance lifted_t1, m, u),[],lifted_concl_pat
+  in
+*)
+(****************************************************************************)
+        let term_to_refine =
           let rec make_tl base_case =
            function
               0 -> [base_case]
@@ -660,15 +684,15 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
 
 
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-                    ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                    ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 ;;
 
 (* The simplification is performed only on the conclusion *)
 let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-                          ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                          ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:
    (Tacticals.thens
      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
index 3e7a4858128fd2c26cf5625659603bcc14104d19..2700fc27f4066c586a33b3ca5b7514f30343ca64 100644 (file)
@@ -72,10 +72,14 @@ val letin_tac:
 
 val elim_intros_simpl_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
+  ?depth:int -> ?using:Cic.term -> 
+  ProofEngineTypes.lazy_pattern ->
+  ProofEngineTypes.tactic 
 val elim_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic 
+  ?depth:int -> ?using:Cic.term -> 
+  ProofEngineTypes.lazy_pattern ->
+  ProofEngineTypes.tactic 
 
 val cases_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
index 6d198d4d133e721539c30e77d86196787ff6c1b5..c359313dd1e87e1ec88d1ef8684c46d6e48e3098 100644 (file)
@@ -46,8 +46,10 @@ exception WrongUriToInductiveDefinition;;
 exception WrongUriToConstant;;
 exception RelToHiddenHypothesis;;
 
+module C = Cic
+module S = CicSubstitution
+
 let alpha_equivalence =
- let module C = Cic in
   let rec aux t t' =
    if t = t' then true
    else
@@ -122,7 +124,6 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 (* "textual" replacement of several subterms with other ones *)
 let replace ~equality ~what ~with_what ~where =
- let module C = Cic in
   let find_image t =
    let rec find_image_aux =
     function
@@ -184,8 +185,6 @@ let replace ~equality ~what ~with_what ~where =
 (* replaces in a term a term with another one. *)
 (* Lifting are performed as usual.             *)
 let replace_lifting ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image what t =
    let rec find_image_aux =
     function
@@ -282,8 +281,6 @@ let replace_lifting ~equality ~what ~with_what ~where =
 (* replaces in a term a list of terms with other ones. *)
 (* Lifting are performed as usual.                     *)
 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image t =
    let rec find_image_aux =
     function
@@ -373,12 +370,72 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
   substaux 1 where
 ;;
 
+(* This is the inverse of the subst function. *)
+let subst_inv ~equality ~what =
+   let rec find_image t = function
+      | []       -> false
+      | hd :: tl -> equality t hd || find_image t tl 
+   in
+   let rec subst_term k t =
+      if find_image t what then C.Rel k else inspect_term k t
+   and inspect_term k = function
+      | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
+      | C.Sort _ as t -> t
+      | C.Implicit _ as t -> t
+      | C.Var (uri, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Var (uri, enss)
+      | C.Const (uri ,enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Const (uri, enss)
+     | C.MutInd (uri, tyno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutInd (uri, tyno, enss)
+     | C.MutConstruct (uri, tyno, consno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutConstruct (uri, tyno, consno, enss)
+     | C.Meta (i, mss) -> 
+         let mss = List.map (subst_ms k) mss in
+         C.Meta(i, mss)
+     | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
+     | C.Appl ts ->      
+         let ts = List.map (subst_term k) ts in
+         C.Appl ts
+     | C.MutCase (uri, tyno, outty, t, cases) ->
+         let cases = List.map (subst_term k) cases in
+        C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
+     | C.Prod (n, v, t) ->
+        C.Prod (n, subst_term k v, subst_term (succ k) t)
+     | C.Lambda (n, v, t) ->
+        C.Lambda (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, t) ->
+        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.Fix (i, fixes) ->
+        let fixesno = List.length fixes in
+        let fixes = List.map (subst_fix fixesno k) fixes in
+        C.Fix (i, fixes)
+     | C.CoFix (i, cofixes) ->
+        let cofixesno = List.length cofixes in
+        let cofixes = List.map (subst_cofix cofixesno k) cofixes in
+         C.CoFix (i, cofixes)
+   and subst_ens k (uri, t) = uri, subst_term k t   
+   and subst_ms k = function
+      | None   -> None
+      | Some t -> Some (subst_term k t)
+   and subst_fix fixesno k (n, ind, ty, bo) =
+      n, ind, subst_term k ty, subst_term (k + fixesno) bo
+   and subst_cofix cofixesno k (n, ty, bo) =
+      n, subst_term k ty, subst_term (k + cofixesno) bo
+in
+subst_term
+   
+
+
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (match List.nth context (n-1) with
@@ -595,8 +652,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let module C = Cic in
- let module S = CicSubstitution in
  (* a simplified term is active if it can create a redex when used as an *)
  (* actual parameter                                                     *)
  let rec is_active =
@@ -805,8 +860,6 @@ let simpl context =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
  and try_delta_expansion context l term body =
-  let module C = Cic in
-  let module S = CicSubstitution in
    try
     let res,constant_args =
      let rec aux rev_constant_args l =
index 67247876aaa2e62f12a2bc5608f6c18f89d71487..c0318bdfeb53be8562604f7595fabc77f8d136f5 100644 (file)
@@ -44,6 +44,9 @@ val replace_lifting :
 val replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
+val subst_inv :
+  equality:(Cic.term -> Cic.term -> bool) ->
+  what:Cic.term list -> int -> Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
 val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term
index deaf84aa612cb0f979d7c0345af027d863eb4c33..8cca5aee014a39dae9cde8d7bfd9d9748bea3ada 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar  1 10:25:04 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 12 13:47:11 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -32,10 +32,12 @@ val demodulate :
 val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  ?depth:int ->
+  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val elim_intros_simpl :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  ?depth:int ->
+  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val elim_type :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
index a9faa592e8de974b5ce3192a81eacf22f556ac0c..83fee2e1565628013e8ad8ee60fefc2bfacedaae 100644 (file)
@@ -990,7 +990,7 @@ class gui () =
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
       connect_button tbar#elimButton (tac_w_term
-        (A.Elim (loc, hole, None, None, [])));
+        (A.Elim (loc, (Some hole, [], Some CicNotationPt.UserInput), None, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));