]> matita.cs.unibo.it Git - helm.git/commitdiff
elim tactic: it needs two arguments, a term as well as a pattern
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 16 Mar 2007 18:39:27 +0000 (18:39 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 16 Mar 2007 18:39:27 +0000 (18:39 +0000)
CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce
Procedural: refactoring

28 files changed:
helm/software/components/acic_procedural/.depend
helm/software/components/acic_procedural/.depend.opt
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralClassify.ml
helm/software/components/acic_procedural/proceduralMode.ml
helm/software/components/acic_procedural/proceduralMode.mli
helm/software/components/acic_procedural/proceduralPreprocess.ml
helm/software/components/acic_procedural/proceduralPreprocess.mli
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/cic_proof_checking/cicReduction.ml
helm/software/components/cic_proof_checking/cicReduction.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/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/components/tactics/proofEngineReduction.ml
helm/software/components/tactics/proofEngineReduction.mli
helm/software/components/tactics/reductionTactics.ml
helm/software/components/tactics/reductionTactics.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/matitaGui.ml

index 8cb9645ae7d90c02134a090f652ab83181419547..3bb617fbda4d8834a3e6e0fbada711cd69798fa0 100644 (file)
@@ -2,12 +2,10 @@ proceduralPreprocess.cmo: proceduralPreprocess.cmi
 proceduralPreprocess.cmx: proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
-proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi 
-proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \
-    proceduralMode.cmi 
-proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \
-    proceduralMode.cmi 
+proceduralClassify.cmo: proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralClassify.cmi 
+proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
+proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
     proceduralMode.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
index 8cb9645ae7d90c02134a090f652ab83181419547..3bb617fbda4d8834a3e6e0fbada711cd69798fa0 100644 (file)
@@ -2,12 +2,10 @@ proceduralPreprocess.cmo: proceduralPreprocess.cmi
 proceduralPreprocess.cmx: proceduralPreprocess.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
-proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi 
-proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi 
-proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \
-    proceduralMode.cmi 
-proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \
-    proceduralMode.cmi 
+proceduralClassify.cmo: proceduralClassify.cmi 
+proceduralClassify.cmx: proceduralClassify.cmi 
+proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi 
+proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi 
 proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \
     proceduralMode.cmi proceduralConversion.cmi 
 proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \
index dbdfb979209b146c32ee303f89dbe1f599adb096..d6638b3f07f5f294d227150f2ad908aca997e38e 100644 (file)
@@ -35,6 +35,7 @@ module HObj = HelmLibraryObjects
 module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
+module PEH  = ProofEngineHelpers
 module PER  = ProofEngineReduction
 
 module P    = ProceduralPreprocess
@@ -275,7 +276,7 @@ and mk_proof st = function
       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 premises, _ = PEH.split_with_whd (st.context, ty) in
         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
index 2fd2d979d7053abecb185562b9567858df3e6b8c..d21c14601f5108502d27de3c34f1511e3b89c3ab 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module C = Cic
-module D = Deannotate
-module I = CicInspect
-
-module P = ProceduralPreprocess
+module C   = Cic
+module D   = Deannotate
+module I   = CicInspect
+module PEH = ProofEngineHelpers
 
 type conclusion = (int * int) option
 
@@ -57,15 +56,15 @@ let out_table b =
 let id x = x
 
 let classify_conclusion = function
-   | C.Rel i                -> Some (i, 0)
-   | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
-   | _                      -> None
+   | _, C.Rel i                -> Some (i, 0)
+   | _, C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
+   | _                         -> None
 
 let classify c t =
 try   
-   let vs, h = P.split c t in
+   let vs, h = PEH.split_with_whd (c, t) in
    let rc = classify_conclusion (List.hd vs) in
-   let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
+   let map (b, h) (_, v) = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =
index 2b233a4bf358e4fc18d9f2de8bc6cb265b0b42e8..d2ddc6c9847c37d0c25dba76cc9a4dde0c9de096 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module C  = Cic
+module C   = Cic
+module PEH = ProofEngineHelpers
 
-module P = ProceduralPreprocess
 module Cl = ProceduralClassify
 
 let is_eliminator = function
-   | _ :: C.MutInd _ :: _               -> true
-   | _ :: C.Appl (C.MutInd _ :: _) :: _ -> true
-   | _                                  -> false
+   | _ :: (_, C.MutInd _) :: _               -> true
+   | _ :: (_, C.Appl (C.MutInd _ :: _)) :: _ -> true
+   | _                                       -> false
 
 let is_const = function
    | C.Sort _
@@ -49,9 +49,9 @@ let rec is_appl b = function
 
 let bkd c t =
    let classes, rc = Cl.classify c t in
-   let premises, _ = P.split c t in
+   let premises, _ = PEH.split_with_whd (c, t) in
    match rc with
       | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true
       | _ ->
-         let ts, _ = P.split c t in
-         is_appl true (List.hd ts)
+         let _, conclusion = List.hd premises in
+         is_appl true conclusion
index 2f0e7e9f49d292390458f3e3afdb947f640100c1..b55188600b80e6f433aef57e5ce5c852bee991c0 100644 (file)
@@ -23,6 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val is_eliminator: Cic.term list -> bool
+val is_eliminator: (Cic.context * Cic.term) list -> bool
 
 val bkd: Cic.context -> Cic.term -> bool
index dcd4cb58b20588734b9a40c5ee5ca27d2db0a1ba..d3e655da70ea6ee20f54674c8782bb5f0deed028 100644 (file)
@@ -30,26 +30,17 @@ module Un   = CicUniv
 module I    = CicInspect
 module E    = CicEnvironment
 module S    = CicSubstitution
-module Rd   = CicReduction
 module TC   = CicTypeChecker 
 module Rf   = CicRefine
 module DTI  = DoubleTypeInference
 module HEL  = HExtlib
+module PEH  = ProofEngineHelpers
 
 (* helper functions *********************************************************)
 
 let identity x = x
 
 let comp f g x = f (g x)
-   
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (Rd.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
 
 let get_type c t =
    try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
@@ -67,9 +58,9 @@ let refine c t =
       raise e
 
 let get_tail c t =
-   match split c t with
-      | hd :: _, _ -> hd
-      | _          -> assert false
+   match PEH.split_with_whd (c, t) with
+      | (_, hd) :: _, _ -> hd
+      | _               -> assert false
 
 let is_proof c t =
    match get_tail c (get_type c (get_type c t)) with
@@ -159,8 +150,8 @@ let eta_expand g tys t =
    let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
    let arg i = C.Rel (succ i) in
    let rec aux i f a = function
-      | []       -> f, a 
-      | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
+      | []            -> f, a 
+      | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl
    in
    let n = List.length tys in
    let absts, args = aux 0 identity [] tys in
@@ -174,7 +165,7 @@ let get_tys c decurry =
    let rec aux n = function
 (*      | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *)
       | t                 ->
-         let tys, _ = split c (get_type c t) in
+         let tys, _ = PEH.split_with_whd (c, get_type c t) in
          let _, tys = HEL.split_nth n (List.rev tys) in
         let tys, _ = HEL.split_nth decurry tys in
          tys
@@ -251,7 +242,7 @@ and pp_appl g ht es c t = function
       pp_proof g ht es c x
 
 and pp_atomic g ht es c t =
-   let _, premsno = split c (get_type c t) in
+   let _, premsno = PEH.split_with_whd (c, get_type c t) in
    g t true premsno
 
 and pp_mutcase g ht es c uri tyno outty arg cases =
@@ -265,14 +256,14 @@ and pp_mutcase g ht es c uri tyno outty arg cases =
       I.S.mem tyno (I.get_mutinds_of_uri uri t) 
    in
    let map2 case (_, cty) = 
-      let map (h, case, k) premise = 
+      let map (h, case, k) (_, premise) = 
          if h > 0 then pred h, case, k else
         if is_recursive premise then 
            0, add_abst k case, k + 2 
         else
            0, case, succ k
       in
-      let premises, _ = split c cty in
+      let premises, _ = PEH.split_with_whd (c, cty) in
       let _, lifted_case, _ =
          List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
       in
index 7bd55f4e221fd09b0dd5f9187fb41b56f875188a..6d66bf23732b2e83575826dd8f929cb10383a443 100644 (file)
@@ -23,6 +23,4 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val split: Cic.context -> Cic.term -> Cic.term list * int
-
 val pp_obj: Cic.obj -> Cic.obj
index 3ef27ea4020392e83173ee70dbc0d8af52247f69..b4d88169af438c267948b0c382114856ad2b9c05 100644 (file)
@@ -138,8 +138,8 @@ let mk_rewrite direction what where pattern =
    mk_tactic tactic
 
 let mk_elim what using pattern =
-   let pattern = Some what, [], Some pattern in
-   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
+   let pattern = None, [], Some pattern in
+   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =
index f4880e426de66ffd74b78808eea763cb4b761a71..6e963a274d06befaf6e6e897009e88aad9a9473c 100644 (file)
@@ -1120,46 +1120,50 @@ let normalize ?delta ?subst ctx term =
   
   
 (* performs an head beta/cast reduction *)
-let rec head_beta_reduce ?(delta=false) =
- function
-    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-      let he'' = CicSubstitution.subst he' t in
-       if tl' = [] then
-        he''
-       else
-        let he''' =
-         match he'' with
-            Cic.Appl l -> Cic.Appl (l@tl')
-          | _ -> Cic.Appl (he''::tl')
+let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
+ HLog.warn (Printf.sprintf "inside head_beta_reduce %i %s" upto (CicPp.ppterm t));
+ match upto with
+    0 -> t
+  | n ->
+    match t with
+       (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+         let he'' = CicSubstitution.subst he' t in
+          if tl' = [] then
+           he''
+          else
+           let he''' =
+            match he'' with
+               Cic.Appl l -> Cic.Appl (l@tl')
+             | _ -> Cic.Appl (he''::tl')
+           in
+            head_beta_reduce ~delta ~upto:(upto - 1) he'''
+     | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
+     | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         in
-         head_beta_reduce ~delta he'''
-  | Cic.Cast (te,_) -> head_beta_reduce ~delta te
-  | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce
-            ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
-  | Cic.Const (uri,ens) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo))
-  | t -> t
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~upto
+               ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+     | Cic.Const (uri,ens) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        in
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+     | t -> t
 
 (*
 let are_convertible ?subst ?metasenv context t1 t2 ugraph =
index bee4607d509d240e0e8453c8e243f51ffa209dcf..82be7fd3f5f43eface9449152ca330d64757c84e 100644 (file)
@@ -38,6 +38,7 @@ val are_convertible :
 val normalize:
   ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
  
-(* performs an head beta/cast reduction; the default is to not perform
-   delta reduction *)
-val head_beta_reduce: ?delta:bool -> Cic.term -> Cic.term
+(* performs head beta/(delta)/cast reduction; the default is to not perform
+   delta reduction; if provided, ~upto is the maximum number of beta redexes
+   reduced *)
+val head_beta_reduce: ?delta:bool -> ?upto:int -> Cic.term -> Cic.term
index b5e75712fb7ea6a6e7c467eb0f3b3f0029efe3b3..e8811830380cef794daf7f38c68348ae8a959dd8 100644 (file)
@@ -55,8 +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, 'lazy_term, 'ident) pattern * 'term option * 
-            int option * 'ident list
+  | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
+           int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
   | Exact of loc * 'term
   | Exists of loc
index e8fd2fe022b9c2a72b54f67ba16375c1d41f9586..d7ed16efd103aa6cdea44040794c135c4fac44ef 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 (_, pattern, using, num, idents) ->
-      sprintf "elim %s%s%s" 
-      (pp_tactic_pattern pattern)
+  | Elim (_, what, using, pattern, num, idents) ->
+      sprintf "elim %s%s %s%s" 
+      (term_pp what)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
+      (pp_tactic_pattern pattern)
       (pp_intros_specs (num, idents)) 
   | ElimType (_, term, using, num, idents) ->
       sprintf "elim type " ^ term_pp term ^
index 4c177fee76d3c6245ec47091af00f15427c733a7..51b86fa5e092db484f01737a5113db82087f8adc 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 (_, pattern, using, depth, names) ->
+  | GrafiteAst.Elim (_, what, using, pattern, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
-        pattern
+        ~pattern what
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
index 97f0d5e85892df5b5933cf706d5b5e69d9ec2144..5748f0bbb0a6178bd1f87463d851fc3d992f8060 100644 (file)
@@ -158,13 +158,15 @@ let disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
-       let pattern = disambiguate_pattern pattern in
+    | GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents) ->
+       let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
-        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)
+        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents)
+    | GrafiteAst.Elim (loc, what, None, pattern, depth, idents) ->
+       let metasenv,what = disambiguate_term context metasenv what in
+       let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Elim (loc, what, None, pattern, 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 dac05d7bdd056d83d146bbef82e03d886efc6742..3eb64d458fe2892a44f32af5bb1ce5e0af0db1fb 100644 (file)
@@ -163,13 +163,14 @@ EXTEND
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
-    | IDENT "elim"; what = tactic_term; using = using;
+    | IDENT "elim"; what = tactic_term; using = using; 
+       pattern = OPT pattern_spec;
        (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, pattern, using, num, idents)    
+       let pattern = match pattern with
+          | None         -> None, [], Some Ast.UserInput
+          | Some pattern -> pattern   
+       in
+       GrafiteAst.Elim (loc, what, using, pattern, num, idents)
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
        GrafiteAst.ElimType (loc, what, using, num, idents)
index 189cd9079b4fd429a330948cbb535b720a3a8593..6c37acaa4fdfa1ae224ef2d5ae7945570a6e0cac 100644 (file)
@@ -127,12 +127,11 @@ 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 pattern 
+     [ Tactics.elim_intros (Cic.Rel 1)
         ~mk_fresh_name_callback:
           (let i = ref 0 in
             fun _ _ _  ~typ ->
@@ -147,7 +146,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
 ;;
 
 let andelim t id1 t1 id2 t2 = 
- Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
+ Tactics.elim_intros t
       ~mk_fresh_name_callback:
         (let i = ref 0 in
           fun _ _ _  ~typ ->
@@ -251,8 +250,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- let pattern = Some (fun c m u -> t, m, u), [], Some pat in
- Tactics.elim_intros ~depth:0 pattern
+ let pattern = None, [], Some pat in
+ Tactics.elim_intros ~depth:0 ~pattern t
 ;;
 
 let case id ~params =
index 85eade2d08e0291ac53b7a5cab724f47b4831e26..f18d2b333b68b322523b656db7db9527816c7324 100644 (file)
@@ -34,24 +34,11 @@ module T    = Tacticals
 module PESR = ProofEngineStructuralRules
 module F    = FreshNamesGenerator
 module PET  = ProofEngineTypes
-module H    = ProofEngineHelpers
 module RT   = ReductionTactics
 module E    = CicEnvironment
 module R    = CicReduction
 module Un   = CicUniv
-
-(* from ProceduralClasify ***************************************************)
-
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (R.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
-
-(****************************************************************************)
+module PEH  = ProofEngineHelpers
 
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
@@ -64,9 +51,9 @@ let get_inductive_def uri =
 let is_not_recursive uri tyno tys = 
    let map mutinds (_, ty) = 
 (* FG: we can do much better here *)      
-      let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
+      let map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
 (**********************************)      
-      let premises, _ = split [] ty in
+      let premises, _ = PEH.split_with_whd ([], ty) in
       List.fold_left map mutinds (List.tl premises)
    in
    let msg = "recursiveness check non implemented for mutually inductive types" in
@@ -80,14 +67,14 @@ let rec check_type sorts metasenv context t =
       | C.MutInd (uri, tyno, _) as t -> 
          let lpsno, tys = get_inductive_def uri in
          let _, inductive, arity, _ = List.nth tys tyno in
-         let _, psno = split [] arity in
+         let _, psno = PEH.split_with_whd ([], arity) in
          let not_relation = (lpsno = psno) in
          let not_recursive = is_not_recursive uri tyno tys in
          let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
-         let sort = match split context ty_ty with
-            | C.Sort sort ::_ , _ -> CicPp.ppsort sort
-           | C.Meta _ :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
-           | _                   -> assert false
+         let sort = match PEH.split_with_whd (context, ty_ty) with
+            | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
+           | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
+           | _                        -> assert false
          in
          let right_sort = List.mem sort sorts in
          if not_relation && inductive && not_recursive && right_sort then
@@ -108,7 +95,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
-         match H.get_name context index with 
+         match PEH.get_name context index with 
            | _ when index <= 0 -> (proof, [goal])
            | None              -> aux (pred index)
            | Some what         -> 
@@ -126,11 +113,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let (proof, goal) = status in
       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 index, ty = PEH.lookup_type metasenv context what 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 pattern)
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
                    ~continuation:(PESR.clear [what])
         else 
            let msg = "unexported elim_clear: not an decomposable type" in
@@ -149,9 +135,8 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
     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 pattern; T.id_tac]
+      T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
     in
     PET.apply_tactic tac status
   in
index 2c22aa5ec2c10307dc308f44882367817db9a621..6646157240d93ab648ed54386908b03b51da1a28 100644 (file)
@@ -30,6 +30,7 @@ open ProofEngineTypes
 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
 exception NotAnInductiveTypeToEliminate
 exception WrongUriToVariable of string
+exception NotAnEliminator
 
 (* lambda_abstract newmeta ty *)
 (* returns a triple [bo],[context],[ty'] where              *)
@@ -477,21 +478,33 @@ let exact_tac ~term =
   mk_tactic (exact_tac ~term)
 
 (* not really "primitive" tactics .... *)
-let elim_tac ?using pattern = 
+  
+module TC  = CicTypeChecker
+module U   = UriManager
+module R   = CicReduction
+module C   = Cic
+module PET = ProofEngineTypes
+module PEH = ProofEngineHelpers
+module PER = ProofEngineReduction
+module MS  = CicMetaSubst 
+module S   = CicSubstitution 
+module T   = Tacticals
+module RT  = ReductionTactics
+
+let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = 
  let elim_tac (proof, goal) =
-  let module T = CicTypeChecker in
-  let module U = UriManager in
-  let module R = CicReduction in
-  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
+   let ugraph = CicUniv.empty_ugraph in
+   let curi, metasenv, proofbo, proofty, attrs = proof in
+   let conjecture = CicUtil.lookup_meta goal metasenv in
+   let metano, context, ty = conjecture in
+(*    let (term, metasenv, _ugraph), cpatt = match pattern with 
+       | Some f, [], Some cpatt -> f context metasenv ugraph, cpatt
+       | _                      -> assert false
     in
-    let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+*)    
+    let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
     let termty = CicReduction.whd context termty in
-    let (termty,metasenv',arguments,fresh_meta) =
+    let (termty,metasenv',arguments,_fresh_meta) =
      TermUtil.saturate_term
       (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
     let term = if arguments = [] then term else Cic.Appl (term::arguments) in
@@ -505,14 +518,14 @@ let elim_tac ?using pattern =
      let eliminator_uri =
       let buri = U.buri_of_uri uri in
       let name = 
-        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        let o,_ugraph = CicEnvironment.get_obj ugraph uri in
        match o with
           C.InductiveDefinition (tys,_,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in
             name
         | _ -> assert false
       in
-      let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in
+      let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in
       let ext =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
@@ -528,47 +541,75 @@ let elim_tac ?using pattern =
          | None   -> C.Const (eliminator_uri,exp_named_subst)
          | Some t -> t 
        in
-       let ety,_ = 
-         T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
-        let rec find_args_no =
-         function
-            C.Prod (_,_,t) -> 1 + find_args_no t
-          | C.Cast (s,_) -> find_args_no s
-          | C.LetIn (_,_,t) -> 0 + find_args_no t
-          | _ -> 0
-        in
-         let args_no = find_args_no ety in
-(* we find the predicate for the eliminator as in the rewrite tactic ********)
+       let ety,_ugraph = 
+         TC.type_of_aux' metasenv' context eliminator_ref ugraph in
+(* FG: ADDED PART ***********************************************************)
+(* FG: we can not assume eliminator is the default eliminator ***************)
+   let add_lambdas n t =
+      let rec aux n t =
+         if n <= 0 then t 
+        else C.Lambda (C.Anonymous, C.Implicit None, aux (pred n) t)
+      in
+      aux n (S.lift n t)
+   in
+   let rec args_init n f =
+      if n <= 0 then [] else f n :: args_init (pred n) f
+   in
+   let splits, args_no = PEH.split_with_whd (context, ety) in
+   let pred_pos = match List.hd splits with
+      | _, C.Rel i when i > 1 && i <= args_no -> i
+      | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
+      | _ -> raise NotAnEliminator
+   in
+   let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
+   let termty_ty =
+      let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
+      CicReduction.whd context termty_ty
+   in
 (*   
-   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 metasenv', term, pred, upto = match cpatt, termty_ty with
+      | C.Implicit (Some `Hole), _ 
+      | _, C.Sort C.Prop when lambdas = 0 -> metasenv', term, C.Implicit None, 0
+      | _                                 ->
+(* FG: 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 lazy_term c m u =  
+            let distance  = List.length c - List.length context in
+            S.lift distance term, m, u
+         in
+         let pattern = Some lazy_term, [], Some cpatt in
+         let subst, metasenv', _ugraph, _conjecture, selected_terms =
+            ProofEngineHelpers.select
+            ~metasenv:metasenv' ~ugraph ~conjecture ~pattern
+         in
+         let metasenv' = MS.apply_subst_metasenv subst metasenv' in  
+         let map (_context_of_t, t) l = t :: l in
+         let what = List.fold_right map selected_terms [] in
+         let ty = MS.apply_subst subst ty in
+         let term = MS.apply_subst subst term in
+         let termty = MS.apply_subst subst termty in
+         let abstr_ty = PER.replace_with_rel_1_from ~equality:(==) ~what 1 ty in
+         let abstr_ty = MS.apply_subst subst abstr_ty in
+         let pred_body = C.Lambda (fresh_name, termty, abstr_ty) in
+        metasenv', term, add_lambdas (pred lambdas) pred_body, lambdas 
+   in
+(* FG: END OF ADDED PART ****************************************************)
 *)
-(****************************************************************************)
+         let pred, upto = C.Implicit None, 0 in
+        
         let term_to_refine =
-          let rec make_tl base_case =
-           function
-              0 -> [base_case]
-            | n -> (C.Implicit None)::(make_tl base_case (n - 1))
-          in
-           C.Appl (eliminator_ref :: make_tl term (args_no - 1))
+          let f n =
+          if n = pred_pos then pred else
+          if n = 1 then term else C.Implicit None
+         in
+           C.Appl (eliminator_ref :: args_init args_no f)
          in
-          let refined_term,_,metasenv'',_ = 
+          let refined_term,_refined_termty,metasenv'',_ugraph = 
            CicRefine.type_of_aux' metasenv' context term_to_refine
-             CicUniv.empty_ugraph
+             ugraph
           in
            let new_goals =
             ProofEngineHelpers.compare_metasenvs
@@ -576,7 +617,7 @@ let elim_tac ?using pattern =
            in
            let proof' = curi,metasenv'',proofbo,proofty, attrs in
             let proof'', new_goals' =
-             apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+            apply_tactic (apply_tac ~term:refined_term) (proof',goal)
             in
              (* The apply_tactic can have closed some of the new_goals *)
              let patched_new_goals =
@@ -585,20 +626,30 @@ let elim_tac ?using pattern =
                 (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
                 ) new_goals @ new_goals'
              in
-              proof'', patched_new_goals
+              let res = proof'', patched_new_goals in
+               if upto = 0 then res else 
+               let pattern = PET.conclusion_pattern None in
+               let continuation =
+                RT.simpl_tac ~pattern
+                (* RT.head_beta_reduce_tac ~delta:false ~upto ~pattern *)
+               in
+                let dummy_status = proof,goal in
+                 PET.apply_tactic
+                  (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)
+                   dummy_status
  in
   mk_tactic elim_tac
 ;;
 
 let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cases_tac ~term (proof, goal) =
-  let module T = CicTypeChecker in
+  let module TC = CicTypeChecker in
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
    let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
     let (termty,metasenv',arguments,fresh_meta) =
      TermUtil.saturate_term
@@ -684,15 +735,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 pattern =
- Tacticals.then_ ~start:(elim_tac ?using pattern)
+                    ?depth ?using ?pattern what =
+ Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
   ~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 pattern =
- Tacticals.then_ ~start:(elim_tac ?using pattern)
+                          ?depth ?using ?pattern what =
+ Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
   ~continuation:
    (Tacticals.thens
      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
@@ -703,8 +754,6 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
 
 (* FG: insetrts a "hole" in the context (derived from letin_tac) *)
 
-module C = Cic
-
 let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
index 2700fc27f4066c586a33b3ca5b7514f30343ca64..863df5eeea2872ef08d48c01348c2c25974072f0 100644 (file)
@@ -73,12 +73,12 @@ val letin_tac:
 val elim_intros_simpl_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> 
-  ProofEngineTypes.lazy_pattern ->
+  ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term ->
   ProofEngineTypes.tactic 
 val elim_intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> 
-  ProofEngineTypes.lazy_pattern ->
+  ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term ->
   ProofEngineTypes.tactic 
 
 val cases_intros_tac:
index c2d0d15e171586b339f2fa32cd695cac1d063c54..177471c7403a4d9eb2da538289f76e5e718f0681 100644 (file)
@@ -639,3 +639,12 @@ let get_rel context name =
       | _ :: tl                                 -> aux (succ i) tl
    in
    aux 1 context
+
+let split_with_whd (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux whd a n c = function
+      | Cic.Prod (s, v, t)  -> aux false ((c, v) :: a) (succ n) (add s v c) t
+      | v when whd          -> (c, v) :: a, n
+      | v                   -> aux true a n c (CicReduction.whd c v)
+    in
+    aux false [] 0 c t
index f0b2c87f12fc14a2b8f8ac3d477c7654a023cc9f..1ac3ee707f17c7ef3eca3f7ec284885c9d5107a8 100644 (file)
@@ -111,3 +111,12 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 val get_name: Cic.context -> int -> string option
 
 val get_rel: Cic.context -> string -> Cic.term option
+
+(* split_with_whd (c, t) takes a type t typed in the context c and returns
+   [(c_0, t_0); (c_1, t_1); ...; (c_n, t_n)], n where t_0 is the conclusion of
+   t and t_i is the premise of t accessed by Rel i in t_0. 
+   Performes a whd on the conclusion before giving up.
+   Each t_i is returned with a context c_i in wich it is typed
+*)
+val split_with_whd: Cic.context * Cic.term -> 
+                    (Cic.context * Cic.term) list * int
index dbc98f722313e250ed0327c427c2aaaaffa9b280..1b5922d1d28f8f0af33c462f55ea1d07d21faa18 100644 (file)
@@ -383,8 +383,9 @@ 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 =
+(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
+   up to the fact that the index to start from can be specified *)
+let replace_with_rel_1_from ~equality ~what =
    let rec find_image t = function
       | []       -> false
       | hd :: tl -> equality t hd || find_image t tl 
@@ -392,7 +393,7 @@ let subst_inv ~equality ~what =
    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.Rel i -> if i < k then C.Rel i else C.Rel (succ i)
       | C.Sort _ as t -> t
       | C.Implicit _ as t -> t
       | C.Var (uri, enss) ->
index 39beb84aa8d8fc55913989f2a97a475ba07f563e..78f4b7f4c4e8024550fa91dd05a8ae91db2356a6 100644 (file)
@@ -65,7 +65,9 @@ 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 :
+(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
+   up to the fact that the index to start from can be specified *)
+val replace_with_rel_1_from :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> int -> Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
index 754b2c0c5b49cca403f94a8e3bde1ee86f2c9798..5afc672695733cada18b7335705e1d360bec515b 100644 (file)
@@ -118,6 +118,17 @@ let normalize_tac ~pattern =
  mk_tactic (reduction_tac
   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
+let head_beta_reduce_tac ?delta ?upto ~pattern =
+ begin match upto with
+    | Some upto -> 
+         HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto)
+    | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none")
+ end;
+ mk_tactic (reduction_tac
+  ~reduction:
+    (const_lazy_reduction
+      (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern)
+
 exception NotConvertible
 
 (* Note: this code is almost identical to reduction_tac and
index 16e2bc23c475694e8b70a0a2d73dd02e0c0a61d3..62200df69a0cfc3d6e843fae3ad0acc114d7fe4e 100644 (file)
@@ -27,6 +27,7 @@ val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 
 (* The default of term is the thesis of the goal to be prooved *)
 val unfold_tac:
index 8cca5aee014a39dae9cde8d7bfd9d9748bea3ada..4f2908706dee2625edb6fe47c527f6b9d83a7a8a 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 12 13:47:11 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Mar 16 19:03:48 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -33,11 +33,15 @@ val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int ->
-  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+  ?using:Cic.term ->
+  ?pattern:ProofEngineTypes.lazy_pattern ->
+  Cic.term -> ProofEngineTypes.tactic
 val elim_intros_simpl :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int ->
-  ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+  ?using:Cic.term ->
+  ?pattern:ProofEngineTypes.lazy_pattern ->
+  Cic.term -> ProofEngineTypes.tactic
 val elim_type :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
index 83fee2e1565628013e8ad8ee60fefc2bfacedaae..684e1fa2f3d40f9dc182326175f6db07fd0d5bc7 100644 (file)
@@ -990,7 +990,8 @@ 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, (Some hole, [], Some CicNotationPt.UserInput), None, None, [])));
+        (let pattern = None, [], Some CicNotationPt.UserInput in
+       A.Elim (loc, hole, None, pattern, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));