From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 2 Mar 2004 15:53:19 +0000 (+0000)
Subject: added cast concrete syntax
X-Git-Tag: v0_0_4~57
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4649be7680244c896149f9a70dd893353577a4fe;p=helm.git

added cast concrete syntax
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2474191fe..7c8261fae 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -209,6 +209,8 @@ EXTEND
         PAREN "]" ->
           return_term loc
             (CicAst.Case (t, indty_ident, outtyp, patterns))
+      | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" ->
+          return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2])
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index 9caf77aab..368bc2f45 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -85,4 +85,14 @@ let lookup_num_by_dsc dsc =
 
 let _ =
   add_binary_op "exists" "exists"
-   (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []))
+    (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []));
+  add_symbol_choice "cast"
+    ("type cast",
+      (fun env _ args ->
+        let t1, t2 =
+          match args with 
+          | [t1; t2] -> t1, t2
+          | _ -> raise Invalid_choice
+        in
+        Cic.Cast (t1, t2)));
+