From 4649be7680244c896149f9a70dd893353577a4fe Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 2 Mar 2004 15:53:19 +0000 Subject: [PATCH] added cast concrete syntax --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 2 ++ helm/ocaml/cic_disambiguation/disambiguateChoices.ml | 12 +++++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) 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))); + -- 2.39.2