From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Jul 2005 12:38:38 +0000 (+0000)
Subject: Missing case (Cast) implemented.
X-Git-Tag: V_0_7_2~172
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d6486664169e87c0f2123f4923ab0aa3e544ebb;p=helm.git

Missing case (Cast) implemented.
---

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 5c1ea95d7..0e7a01306 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -66,6 +66,8 @@ and countterm current_size t =
              let size3 =
                List.fold_left countvar (c+String.length constr) vars in
              countterm size3 action) size2 pl 
+    | A.Cast (bo,ty) ->
+       countterm (countterm (current_size + 3) bo) ty
     | A.LetIn (var,s,t) ->
         let size1 = countvar current_size var in
         let size2 = countterm size1 s in
@@ -265,6 +267,10 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                         Box.smallskip;
                         Box.Text([],"with")]);
                  Box.indent plbox])
+    | A.Cast (bo,ty) ->
+        Box.V(make_attributes [Some "helm","xref"] [xref],
+              [Box.H([],[Box.Text([],"("); ast2box ~tail:[] bo]);
+               Box.H([],[Box.Text([],":"); ast2box ~tail ty;Box.Text([],")")])])
     | A.LetIn (var, s, t) ->
         Box.V(make_attributes [Some "helm","xref"] [xref],
               (make_def "let" var s "in")@[ast2box ~tail t])
@@ -486,6 +492,10 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
         | `None ->
             P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
             [m_close_fence]))
+    | A.Cast (bo,ty) ->
+       let attr = make_attributes [Some "helm","xref"] [xref] in
+        P.Mrow (attr,
+         [m_open_fence; aux bo; P.Mo ([],":"); aux ty; m_close_fence])
     | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
     | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index 8076e0062..2479fe24a 100644
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -49,6 +49,7 @@ let rec pp_term = function
       sprintf "%smatch %s with %s"
         (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
         (pp_term term) (pp_patterns patterns)
+  | CicAst.Cast (t1,t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
   | CicAst.LetIn (var, t1, t2) ->
       sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
         (pp_term t2)