From 10be6b9fb25a5bcd8721f707beba4b8a125591b5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 21 Jan 2005 11:49:03 +0000 Subject: [PATCH] - Changed ApplyTransformation API to return both the mathml and acic, plus all the related tables - Added the "Coercion" keyword to CicTextualParser2 --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 6 +++++- helm/ocaml/cic_disambiguation/disambiguateTypes.mli | 2 +- helm/ocaml/cic_transformations/applyTransformation.ml | 8 +++++--- helm/ocaml/cic_transformations/applyTransformation.mli | 9 +++++++-- helm/ocaml/cic_transformations/tacticAst.ml | 1 + helm/ocaml/cic_unification/cicRefine.ml | 2 +- 6 files changed, 20 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 00b4c4418..478e97d39 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -392,7 +392,7 @@ EXTEND tl = OPT [ "with"; types = LIST1 [ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; - OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> (name, true, typ, constructors) ] SEP "with" -> types ] -> let params = @@ -427,6 +427,10 @@ EXTEND ind_types in return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT -> + return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some []))) + | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI -> + return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some []))) | [ IDENT "goal" | IDENT "Goal" ]; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index c21084966..6146a082d 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -47,7 +47,7 @@ module type Callbacks = ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list - val interactive_interpretation_choice : + val interactive_interpretation_choice : (string * string) list list -> int list (** @param title gtk window title for user prompting diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 784ab89d7..4d1a65069 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -46,7 +46,8 @@ let mml_of_cic_sequent metasenv sequent = (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in let xmlpres = mpres_document pres_sequent in Xml2Gdome.document_of_xml Misc.domImpl xmlpres, - (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + (asequent, + (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) ;; let mml_of_cic_object uri obj = @@ -61,6 +62,7 @@ let mml_of_cic_object uri obj = let pres = Content2pres.content2pres ~ids_to_inner_sorts content in let xmlpres = mpres_document pres in let mathml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in - (mathml, - (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses)) + (mathml,(annobj, + (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, + ids_to_inner_sorts,ids_to_inner_types))) diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli index 1b646aa6e..f7d3d2da2 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.mli +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -37,16 +37,21 @@ val mml_of_cic_sequent : Cic.metasenv -> (* metasenv *) Cic.conjecture -> (* sequent *) Gdome.document * (* Math ML *) + (Cic.annconjecture * (* annsequent *) ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) - (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *) val mml_of_cic_object : UriManager.uri -> (* object uri *) Cic.obj -> (* uri *) Gdome.document * (* Math ML *) + (Cic.annobj * (* annobj *) ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *) - (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic2acic.anntypes) Hashtbl.t))(* ids_to_inner_types *) diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 8c678de93..1b4e906e0 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -111,6 +111,7 @@ type 'term command = * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) + | Coercion of 'term | Redo of int option | Undo of int option diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index fe70f250a..d8b822d82 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -52,7 +52,7 @@ let look_for_coercion src tgt = then begin prerr_endline "TROVATA coercion"; - Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con") + Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con") end else begin -- 2.39.2