X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FproceduralTypes.ml;h=95fdc6e562d6c8e281c937509dd8b57d57431ab9;hb=46bde81a59b45bedd6d859450decfc2263d92d7e;hp=be1dbee73e7ff7ae18d0cf503b24b4a0b64cf20f;hpb=c1e0024285a65a7d3e31bbdf77ad5d12bcdde36c;p=helm.git

diff --git a/components/content_pres/proceduralTypes.ml b/components/content_pres/proceduralTypes.ml
index be1dbee73..95fdc6e56 100644
--- a/components/content_pres/proceduralTypes.ml
+++ b/components/content_pres/proceduralTypes.ml
@@ -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
@@ -75,6 +86,7 @@ type step = Note of note
 	  | Rewrite of how * what * where * note
 	  | Elim of what * using option * note
 	  | Apply of what * note
+	  | Whd of count * note
 	  | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -85,6 +97,8 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 let floc = H.dummy_floc
 
+let hole = C.AImplicit ("", Some `Hole)
+
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
 let mk_theorem name t = 
@@ -114,7 +128,6 @@ let mk_letin name what =
    mk_tactic tactic
 
 let mk_rewrite direction what where =
-   let hole = C.AImplicit ("", Some `Hole) in
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
       | None                 -> (None, [], Some hole), []
@@ -131,6 +144,11 @@ let mk_apply t =
    let tactic = G.Apply (floc, t) in
    mk_tactic tactic
 
+let mk_whd i =
+   let pattern = None, [], Some hole in
+   let tactic = G.Reduce (floc, `Whd, pattern) in
+   mk_tactic tactic
+
 let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
 
 let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
@@ -154,24 +172,25 @@ let rec render_step sep a = function
    | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
+   | Whd (c, s)           -> mk_note s :: cont sep (mk_whd c :: a)
    | Branch ([], s)       -> a
-   | Branch ([ps], s)     -> cont sep (render_steps a ps)
+   | Branch ([ps], s)     -> render_steps sep a ps
    | Branch (pss, s)      ->
       let a =  mk_ob :: a in
-      let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
+      let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in
       mk_note s :: cont sep body
 
-and render_steps a = function
+and render_steps sep a = function
    | []                                          -> a
-   | [p]                                         -> render_step None a p
-   | (Note _ | Theorem _ | Qed _ as p) :: ps     ->
-      render_steps (render_step None a p) ps 
-   | p :: ((Branch ([], _) :: _) as ps) ->
-      render_steps (render_step None a p) ps
+   | [p]                                         -> render_step sep a p
+   | p :: Branch ([], _) :: ps                   ->
+      render_steps sep a (p :: ps)
    | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
-      render_steps (render_step (Some mk_sc) a p) ps
+      render_steps sep (render_step (Some mk_sc) a p) ps
    | p :: ps                                     ->
-      render_steps (render_step (Some mk_dot) a p) ps
+      render_steps sep (render_step (Some mk_dot) a p) ps
+
+let render_steps a = render_steps None a
 
 (* counting *****************************************************************)