X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=8dac90f26bde2c20a7d9e0a5ebee5adcc986960e;hb=50afaf262195266d156f594cff7e92a6e8898b3e;hp=b81a7c3dead0ebe02105c854bf45706e133b91bc;hpb=94c0dace142ca00a1b5e1a63d83f65d86e3a1c8d;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index b81a7c3de..8dac90f26 100644
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -76,6 +76,7 @@ type count    = int
 type note     = string
 type where    = (name * name) option
 type inferred = Cic.annterm
+type pattern  = Cic.annterm
 
 type step = Note of note 
           | Theorem of name * what * note
@@ -84,11 +85,10 @@ type step = Note of note
 	  | Intros of count option * name list * note
 	  | Cut of name * what * note
 	  | LetIn of name * what * note
-	  | Rewrite of how * what * where * note
-	  | Elim of what * using option * note
+	  | Rewrite of how * what * where * pattern * note
+	  | Elim of what * using option * pattern * note
 	  | Apply of what * note
-	  | Whd of count * note
-	  | Change of inferred * what * where * note 
+	  | Change of inferred * what * where * pattern * note 
 	  | ClearBody of name * note
 	  | Branch of step list list * note
 
@@ -98,10 +98,9 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 (* grafite ast constructors *************************************************)
 
+(*
 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 = 
@@ -130,32 +129,28 @@ let mk_letin name what =
    let tactic = G.LetIn (floc, what, name) in
    mk_tactic tactic
 
-let mk_rewrite direction what where =
+let mk_rewrite direction what where pattern =
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
-      | None                 -> (None, [], Some hole), []
-      | Some (premise, name) -> (None, [premise, hole], None), [name] 
+      | None                 -> (None, [], Some pattern), []
+      | Some (premise, name) -> (None, [premise, pattern], None), [name] 
    in
    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 = None, [], Some pattern in
+   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
    mk_tactic tactic
 
 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_change t where =
+let mk_change t where pattern =
    let pattern = match where with
-      | None              -> None, [], Some hole
-      | Some (premise, _) -> None, [premise, hole], None
+      | None              -> None, [], Some pattern
+      | Some (premise, _) -> None, [premise, pattern], None
    in
    let tactic = G.Change (floc, pattern, t) in
    mk_tactic tactic
@@ -177,22 +172,21 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
 (* rendering ****************************************************************)
 
 let rec render_step sep a = function
-   | Note s               -> mk_note s :: a
-   | Theorem (n, t, s)    -> mk_note s :: mk_theorem n t :: a 
-   | Qed s                -> (* mk_note s :: *) mk_qed :: a
-   | Id s                 -> mk_note s :: cont sep (mk_id :: a)
-   | Intros (c, ns, s)    -> mk_note s :: cont sep (mk_intros c ns :: a)
-   | 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, 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)
-   | Change (t, _, w, s)  -> mk_note s :: cont sep (mk_change t w :: a)
-   | ClearBody (n, s)     -> mk_note s :: cont sep (mk_clearbody n :: a)
-   | Branch ([], s)       -> a
-   | Branch ([ps], s)     -> render_steps sep a ps
-   | Branch (pss, s)      ->
+   | Note s                  -> mk_note s :: a
+   | Theorem (n, t, s)       -> mk_note s :: mk_theorem n t :: a 
+   | Qed s                   -> (* mk_note s :: *) mk_qed :: a
+   | Id s                    -> mk_note s :: cont sep (mk_id :: a)
+   | Intros (c, ns, s)       -> mk_note s :: cont sep (mk_intros c ns :: a)
+   | 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, 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)
+   | Branch ([], s)          -> a
+   | 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 None) mk_vb a pss in
       mk_note s :: cont sep body
@@ -208,6 +202,8 @@ and render_steps sep a = function
       render_steps sep (render_step (Some mk_dot) a p) ps
 
 let render_steps a = render_steps None a
+*)
+let render_steps sep a = assert false
 
 (* counting *****************************************************************)