]> matita.cs.unibo.it Git - helm.git/commitdiff
matitaGui: some missing cases during disambiguation now treated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 24 Jan 2007 19:28:15 +0000 (19:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 24 Jan 2007 19:28:15 +0000 (19:28 +0000)
grafiteAst: rename tactic removed
procedural: some improvements

18 files changed:
components/content_pres/acic2Procedural.ml
components/content_pres/acic2Procedural.mli
components/content_pres/cicClassify.ml
components/content_pres/cicClassify.mli
components/content_pres/objPp.ml
components/content_pres/objPp.mli
components/content_pres/proceduralConversion.ml
components/content_pres/proceduralConversion.mli
components/content_pres/proceduralTypes.ml
components/content_pres/proceduralTypes.mli
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/tactics.ml
components/tactics/tactics.mli
matita/matitaGui.ml

index c92d108e5500f3ed4bb0c159a04399fdc68d4fa3..adfe4b05cdf8d647f26e68359332737e4c0097fc 100644 (file)
@@ -45,13 +45,17 @@ type status = {
    prefix: string;
    max_depth: int option;
    depth: int;
-   entries: C.context;
+   context: C.context;
    intros: string list;
    ety: C.annterm option
 }
 
 (* helpers ******************************************************************)
 
+let id x = x
+
+let comp f g x = f (g x)
+
 let cic = D.deannotate_term
 
 let split2_last l1 l2 =
@@ -80,22 +84,23 @@ let string_of_head = function
    | C.AMeta _         -> "meta"
    | C.AImplicit _     -> "implict"
 
-let next st = {st with depth = succ st.depth; intros = []; ety = None}
+let clear st = {st with intros = []; ety = None}
+
+let next st = {(clear st) with depth = succ st.depth}
 
 let set_ety st ety =
    if st.ety = None then {st with ety = ety} else st
 
 let add st entry intro ety = 
    let st = set_ety st ety in
-   {st with entries = entry :: st.entries; intros = intro :: st.intros}
+   {st with context = entry :: st.context; intros = intro :: st.intros}
 
 let test_depth st =
 try   
    let msg = Printf.sprintf "Depth %u: " st.depth in
    match st.max_depth with
       | None   -> true, "" 
-      | Some d -> 
-         if st.depth < d then true, msg else false, "DEPTH EXCEDED"
+      | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
 with Invalid_argument _ -> failwith "A2P.test_depth"
 
 let is_rewrite_right = function
@@ -146,6 +151,27 @@ let defined_premise = "DEFINED"
 
 let assumed_premise = "ASSUMED"
 
+let expanded_premise = "EXPANDED"
+
+let eta_expand n t =
+   let ty = C.AImplicit ("", None) in
+   let name i = Printf.sprintf "%s%u" expanded_premise i in 
+   let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in
+   let arg i n = T.mk_arel (n - i) (name i) 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 id [] 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 ("", C.AAppl (id, before) :: after)
+   | _                -> assert false
+
 let get_intro name t = 
 try
 match name with 
@@ -164,17 +190,17 @@ try
       | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
       | _                                   -> p1 :: script
 with Invalid_argument _ -> failwith "A2P.mk_intros"
-(*
-let rec mk_premise st dtext = function
-   | C.ARel (_, _, _, binder)  -> [], binder
-   | where                     -> 
-      let name = contracted_premise in
-      mk_fwd_proof st dtext name where, name
-*)
-let rec mk_fwd_rewrite st dtext name tl direction =
+
+let rec mk_atomic st dtext what =
+   if T.is_atomic what then [], what else
+   let name = defined_premise in
+   mk_fwd_proof st dtext name what, T.mk_arel 0 name
+
+and mk_fwd_rewrite st dtext name tl direction =
    let what, where = List.nth tl 5, List.nth tl 3 in
    let rewrite premise =
-      [T.Rewrite (direction, what, Some (premise, name), dtext)]
+      let script, what = mk_atomic st dtext what in
+      T.Rewrite (direction, what, Some (premise, name), dtext) :: script
    in
    match where with
       | C.ARel (_, _, _, binder) -> rewrite binder
@@ -200,8 +226,8 @@ and mk_fwd_proof st dtext name = function
            let qs = [[T.Id ""]; mk_proof (next st) v] in
            [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
          | None          ->
-            let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
-            let (classes, rc) as h = Cl.classify ty in
+            let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+            let (classes, rc) as h = Cl.classify st.context ty in
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
             [T.LetIn (name, v, dtext ^ text)]
       end
@@ -217,7 +243,7 @@ and mk_proof st = function
         | None          -> None
       in
       mk_proof (add st entry intro ety) 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
@@ -228,42 +254,51 @@ 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, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
-         let (classes, rc) as h = Cl.classify ty in
-         let synth = Cl.S.singleton 0 in
+         let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+         let (classes, rc) as h = Cl.classify st.context ty in
+         let decurry = List.length classes - List.length tl in
+         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
+        let synth = Cl.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
-            | Some (i, j) when i > 1 ->
+            | Some (i, j) when i > 1 && i <= List.length classes ->
               let classes, tl, _, what = split2_last classes tl in
+              let script, what = mk_atomic st dtext what in
               let synth = Cl.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
-                 [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
+                 List.rev script @ 
+                 [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
               else if is_rewrite_left hd then 
-                 [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
+                 List.rev script @
+                 [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
               else   
                  let using = Some hd in
+                 List.rev script @
                  [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
-           | _                                             ->
+           | _                                                  ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
-               [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+              let script, hd = mk_atomic st dtext hd in               
+              List.rev script @               
+              [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
       else
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | t ->
+   | t                                 ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
@@ -276,9 +311,6 @@ try
       if Cl.S.is_empty inv then Some (mk_proof st v) else
       Some [T.Apply (v, dtext ^ "dependent")]
    in
-   let l1, l2 = List.length classes, List.length ts in
-   if l1 > l2 then failwith "partial application" else
-   if l1 < l2 then failwith "too many arguments" else
    T.list_map2_filter aux classes ts
 with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
 
@@ -299,14 +331,14 @@ let mk_obj st = function
 
 (* interface functions ******************************************************)
 
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj = 
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = 
    let st = {
       sorts     = ids_to_inner_sorts;
       types     = ids_to_inner_types;
       prefix    = prefix;
-      max_depth = None;
+      max_depth = depth;
       depth     = 0;
-      entries   = [];
+      context   = [];
       intros    = [];
       ety       = None
    } in
index 50fb60898b6c3560ebaf70f620db044e3cbae624..d1ff6a0c20e18695ed4b5b504e96fde40a85888f 100644 (file)
@@ -26,7 +26,7 @@
 val acic2procedural:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
-   string -> Cic.annobj ->
+   ?depth:int -> string -> Cic.annobj ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list
index 0c464c7d94d4c8d7500aca63028a2fa4c228934f..4cfd47e5abcac8309337f7f808b87c37f750bd50 100644 (file)
@@ -24,7 +24,7 @@
  *)
 
 module C = Cic
-module CS = CicSubstitution
+module R = CicReduction
 module D = Deannotate
 module Int = struct
    type t = int
@@ -57,6 +57,8 @@ let out_table b =
    
 (****************************************************************************)
 
+let id x = x
+
 let rec list_fold_left g map = function
   | []       -> g
   | hd :: tl -> map (list_fold_left g map tl) hd
@@ -98,28 +100,29 @@ let get_rels h t =
    let g a = a in
    aux 1 g t S.empty
 
-let split t =
-   let rec aux a n = function
-      | C.Prod (_, v, t)  -> aux (v :: a) (succ n) t
-      | C.Cast (t, v)     -> aux a n t
-      | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
-      | v                 -> v :: a, n
+let split 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 [] 0 t
+    aux false [] 0 c t
 
 let classify_conclusion = function
    | C.Rel i                -> Some (i, 0)
    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
    | _                      -> None
 
-let classify t =
-   let vs, h = split t in
+let classify c t =
+try   
+   let vs, h = split c t in
    let rc = classify_conclusion (List.hd vs) in
    let map (b, h) v = (get_rels h v, 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 =
-      let map j = S.union (fst b.(j)) in 
+      let map j = if j < h then S.union (fst b.(j)) else id in 
       for i = pred h downto 0 do
          let direct, unused = b.(i) in
         b.(i) <- S.fold map direct direct, unused 
@@ -129,16 +132,17 @@ let classify t =
    let rec mk_inverse i direct =
       if S.is_empty direct then () else
       let j = S.choose direct in
-      let unused, inverse = b.(j) in 
-      b.(j) <- unused, S.add i inverse;
-      mk_inverse i (S.remove j direct)
+      if j < h then
+         let unused, inverse = b.(j) in 
+         b.(j) <- unused, S.add i inverse
+       else ();
+       mk_inverse i (S.remove j direct)
    in
    let map i (direct, _) = mk_inverse i direct in
    Array.iteri map b;
 (*   out_table b; *)
    List.rev_map snd (List.tl (Array.to_list b)), rc
-
-let aclassify t = classify (D.deannotate_term t)
+with Invalid_argument _ -> failwith "Classify.classify"
 
 let overlaps s1 s2 =
    let predicate x = S.mem x s1 in
index c35ba1b5c65dd4d5b129af9ec613fbd0bed3a345..3d92134df6a18ee97a5a799acbb2df791c54340f 100644 (file)
@@ -27,9 +27,7 @@ module S : Set.S with type elt = int
 
 type conclusion = (int * int) option
 
-val classify: Cic.term -> S.t list * conclusion
-
-val aclassify: Cic.annterm -> S.t list * conclusion
+val classify: Cic.context -> Cic.term -> S.t list * conclusion
 
 val to_string: S.t list * conclusion -> string
 
index 3cdad5528a56dac0b13021fa9f743b74d95ee02b..f83b18635e6198fd33f4bdb237ed2a3c76f0bfd7 100644 (file)
@@ -49,17 +49,17 @@ let obj_to_string n style prefix obj =
        failwith msg
   in
   match style with
-     | GrafiteAst.Declarative ->
+     | GrafiteAst.Declarative      ->
         let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
         let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
         remove_closed_substs ("\n\n" ^
           BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
        )
-     | GrafiteAst.Procedural ->
+     | GrafiteAst.Procedural depth ->
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
         let obj_pp = CicNotationPp.pp_obj term_pp in
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
         let script = Acic2Procedural.acic2procedural 
-          ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj in
+          ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
        "\n\n" ^ String.concat "" (List.map aux script)
index 9367661ec4c782ad2baca66b9579ef6c74f13aff..de320bf14d9fb85f19bef203c590368924fa506a 100644 (file)
@@ -24,4 +24,5 @@
  *)
 
 (* columns, rendering style, name prefix, object *)
-val obj_to_string: int -> GrafiteAst.style -> string -> Cic.obj -> string
+val obj_to_string: 
+   int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string
index e506a8f6eec7581614291cfd1abbf71003def272..abd6fd62a8f897f7df4e2b884258706db50804bf 100644 (file)
@@ -30,3 +30,32 @@ let rec need_whd i = function
    | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
    | _                    when i > 0 -> true
    | _                               -> false
+
+let lift k n =
+   let rec lift_xns k (uri, t) = uri, lift_term k t
+   and lift_ms k = function
+      | None   -> None
+      | Some t -> Some (lift_term k t)
+   and lift_fix len k (id, name, i, ty, bo) =
+      id, name, i, lift_term k ty, lift_term (k + len) bo
+   and lift_cofix len k (id, name, ty, bo) =
+      id, name, lift_term k ty, lift_term (k + len) bo
+   and lift_term k = function
+      | C.ASort _ as t -> t
+      | C.AImplicit _ as t -> t
+      | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
+      | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
+      | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
+      | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
+      | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
+      | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
+      | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
+      | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
+      | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
+      | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
+      | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
+      | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+      | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
+      | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
+   in
+   lift_term k
index 448112cdb03c30ba2bfc8478d37759a8eb6fd1f8..d5ad4fd1c9634e7620bc4f8d9f53195792ceeeb4 100644 (file)
@@ -24,3 +24,5 @@
  *)
 
 val need_whd: int -> Cic.annterm -> bool
+
+val lift: int -> int -> Cic.annterm -> Cic.annterm
index b7f6d3c6b68b2baf49909f448e86c5aa2f83e3e4..95fdc6e562d6c8e281c937509dd8b57d57431ab9 100644 (file)
@@ -55,6 +55,17 @@ let list_rev_map_concat map sep a l =
    in
    aux a l
 
+let is_atomic = function
+   | C.ASort _
+   | C.AConst _
+   | C.AMutInd _
+   | C.AMutConstruct _
+   | C.AVar _
+   | C.ARel _
+   | C.AMeta _
+   | C.AImplicit _     -> true
+   | _                 -> false
+
 (****************************************************************************)
 
 type name  = string
index b06acd1049b1938e815ae4a37c37136fd4150dbb..dfd82df12ff1d2b0504a07e04309bea6fd0d91f3 100644 (file)
@@ -31,6 +31,8 @@ val list_split: int -> 'a list -> 'a list * 'a list
 
 val mk_arel: int -> string -> Cic.annterm
 
+val is_atomic:Cic.annterm -> bool 
+
 (****************************************************************************)
 
 type name  = string
index e75e53867aa88306d06dedfe5ee1fff9f2b9efe8..10d7b6bccad33d454a73385686ea9c085e1944fe 100644 (file)
@@ -77,7 +77,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | LetIn of loc * 'term * 'ident
   | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern 
   | Reflexivity of loc
-  | Rename of loc * 'ident list * 'ident list
   | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Rewrite of loc * direction * 'term *
       ('term, 'lazy_term, 'ident) pattern * 'ident list
@@ -109,8 +108,8 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
 type print_kind = [ `Env | `Coer ]
 
-type style = Declarative
-           | Procedural
+type presentation_style = Declarative
+                        | Procedural of int option
 
 type 'term macro = 
   (* Whelp's stuff *)
@@ -122,7 +121,8 @@ type 'term macro =
   (* real macros *)
   | Check of loc * 'term 
   | Hint of loc
-  | Inline of loc * style * string * string (* URI or base-uri, name prefix *) 
+  | Inline of loc * presentation_style * string * string 
+     (* URI or base-uri, name prefix *) 
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
index ce9ea017b2c1565d6b82302e75f8d1582188a9b4..183fc5ec464ca725ccd4b6b54b591ad326478d70 100644 (file)
@@ -148,8 +148,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Reduce (_, kind, pat) ->
       sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
-  | Rename (_, froms, tos) -> 
-     sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos)
   | Replace (_, pattern, t) ->
       sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
   | Rewrite (_, pos, t, pattern, names) -> 
@@ -202,8 +200,9 @@ let pp_arg ~term_pp arg =
 let pp_macro ~term_pp = 
   let term_pp = pp_arg ~term_pp in
   let style_pp = function
-     | Declarative -> ""
-     | Procedural -> "procedural "
+     | Declarative         -> ""
+     | Procedural None     -> "procedural "
+     | Procedural (Some i) -> sprintf "procedural %u " i
   in
   let prefix_pp prefix = 
      if prefix = "" then "" else sprintf " \"%s\"" prefix
index 09ceecebc5d8eceefecda4d254fb7c8db863da47..ab98132210238daf670872dacbb356cf6817c9df 100644 (file)
@@ -151,7 +151,6 @@ let tactic_of_ast status ast =
         | `Unfold what -> Tactics.unfold ~pattern what
         | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
-  | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos
   | GrafiteAst.Replace (_, pattern, with_what) ->
      Tactics.replace ~pattern ~with_what
   | GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
index e7f5eb1fd4077190f7d6d3f4b58be49699e9cd2b..7d110e2df6a5e4844d894d4ab96f2afb5ee92691 100644 (file)
@@ -232,8 +232,6 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
     | GrafiteAst.Reflexivity loc ->
         metasenv,GrafiteAst.Reflexivity loc
-    | GrafiteAst.Rename (loc, froms, tos) ->
-        metasenv,GrafiteAst.Rename (loc, froms, tos)
     | GrafiteAst.Replace (loc, pattern, with_what) -> 
         let pattern = disambiguate_pattern pattern in
         let with_what = disambiguate_lazy_term with_what in
index 586cca004a50f1563bca7e6a3857d160a025082b..2d37892217407440aac8957ee8c9029ff1bc9613 100644 (file)
@@ -218,8 +218,6 @@ EXTEND
         GrafiteAst.Reduce (loc, kind, p)
     | IDENT "reflexivity" ->
         GrafiteAst.Reflexivity loc
-    | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 ->
-       GrafiteAst.Rename (loc, froms, tos)
     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Replace (loc, p, t)
     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
@@ -428,11 +426,11 @@ EXTEND
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "inline"]; 
-        style = OPT [ IDENT "procedural" ];
+        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
        suri = QSTRING; prefix = OPT QSTRING ->
          let style = match style with 
-           | None   -> GrafiteAst.Declarative
-           | Some _ -> GrafiteAst.Procedural
+           | None       -> GrafiteAst.Declarative
+           | Some depth -> GrafiteAst.Procedural depth
         in
         let prefix = match prefix with None -> "" | Some prefix -> prefix in
         GrafiteAst.Inline (loc,style,suri,prefix)
index 130ad7100e833bf9a1521aab76bcd79789afc4bc..82c343085a0c0b4ec38e35693db54acfebd4a8b5 100644 (file)
@@ -59,7 +59,6 @@ let letin = PrimitiveTactics.letin_tac
 let normalize = ReductionTactics.normalize_tac
 let reduce = ReductionTactics.reduce_tac
 let reflexivity = Setoids.setoid_reflexivity_tac
-let rename = ProofEngineStructuralRules.rename 
 let replace = EqualityTactics.replace_tac
 let rewrite = EqualityTactics.rewrite_tac
 let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
index 71265bc7a026959a28b3c761cb8dbedd91ae16db..eb290ff053a414dc42843316134c4e54066e9040 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 14:56:56 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jan 14 12:32:17 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -72,7 +72,6 @@ val normalize :
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val reflexivity : ProofEngineTypes.tactic
-val rename : froms:string list -> tos:string list -> ProofEngineTypes.tactic
 val replace :
   pattern:ProofEngineTypes.lazy_pattern ->
   with_what:Cic.lazy_term -> ProofEngineTypes.tactic
index e2a5588dc178dc2f6eb00394c5658f2e9013f621..ed39ac6525e642912bef5288e35317400032fc0b 100644 (file)
@@ -234,16 +234,40 @@ class interpErrorModel =
 
 let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
 = 
+  assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
    if all_passes then errorll else
      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
     (* We remove passes 1,2 and 5,6 *)
-     []::[]
-     ::(remove_non_significant (safe_list_nth errorll 2))
-     ::(remove_non_significant (safe_list_nth errorll 3))
-     ::[]::[]
+     let res =
+      []::[]
+      ::(remove_non_significant (safe_list_nth errorll 2))
+      ::(remove_non_significant (safe_list_nth errorll 3))
+      ::[]::[]
+     in
+      if List.flatten res <> [] then res
+      else
+       (* all errors (if any) are not significant: we keep them *)
+       let res =
+        []::[]
+        ::(safe_list_nth errorll 2)
+        ::(safe_list_nth errorll 3)
+        ::[]::[]
+       in
+        if List.flatten res <> [] then
+        begin
+          HLog.warn
+          "All disambiguation errors are not significant. Showing them anyway." ;
+         res
+        end
+       else
+         begin
+          HLog.warn
+          "No errors in phases 2 and 3. Showing all errors in all phases" ;
+          errorll
+         end
    in
   let choices =
    let pass = ref 0 in