From 45586ab88c026e6a21927654387b6df266a44700 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Feb 2004 15:56:35 +0000 Subject: [PATCH] added a lot of notation: arithmetic operators, relational operators, ... --- .../ocaml/cic_disambiguation/arit_notation.ml | 96 +++++++++++++++---- .../cic_disambiguation/cicTextualParser2.ml | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 13 ++- .../cic_disambiguation/disambiguateChoices.ml | 28 ++++++ .../disambiguateChoices.mli | 14 ++- .../cic_disambiguation/logic_notation.ml | 27 +++++- 6 files changed, 155 insertions(+), 25 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index 53de39449..b24942775 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -39,7 +39,7 @@ EXTEND [ t1 = term; SYMBOL "*"; t2 = term -> return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2]) | t1 = term; SYMBOL "/"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("div", 0); t1; t2]) + return_term loc (CicAst.Appl [CicAst.Symbol ("divide", 0); t1; t2]) ] ]; term: LEVEL "inv" @@ -48,31 +48,89 @@ EXTEND return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t]) ] ]; + term: LEVEL "relop" + [ + [ t1 = term; SYMBOL <:unicode> (* ≤ *); t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("leq", 0); t1; t2]) + | t1 = term; SYMBOL <:unicode> (* ≥ *); t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("geq", 0); t1; t2]) + | t1 = term; SYMBOL "<"; t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("lt", 0); t1; t2]) + | t1 = term; SYMBOL ">"; t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("gt", 0); t1; t2]) + | t1 = term; SYMBOL <:unicode> (* ≠ *); t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("neq", 0); t1; t2]) + ] + ]; END let _ = + let uri s = UriManager.uri_of_string s in + let const s = Cic.Const (uri s, []) in + let mutind s = Cic.MutInd (uri s, 0, []) in + DisambiguateChoices.add_num_choice ("natural number", (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); DisambiguateChoices.add_num_choice ("real number", (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); - DisambiguateChoices.add_symbol_choice "plus" - ("natural plus", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ HelmLibraryObjects.Peano.plus; t1; t2 ])); - DisambiguateChoices.add_symbol_choice "plus" - ("real plus", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ HelmLibraryObjects.Reals.rplus; t1; t2 ])); + + DisambiguateChoices.add_binary_op "plus" "natural plus" + HelmLibraryObjects.Peano.plus; + DisambiguateChoices.add_binary_op "plus" "real plus" + HelmLibraryObjects.Reals.rplus; + DisambiguateChoices.add_binary_op "minus" "natural minus" + (const "cic:/Coq/Arith/Minus/minus.con"); + DisambiguateChoices.add_binary_op "minus" "real minus" + (const "cic:/Coq/Reals/Rdefinitions/Rminus.con"); + DisambiguateChoices.add_binary_op "times" "natural times" + (const "cic:/Coq/Init/Peano/mult.con"); + DisambiguateChoices.add_binary_op "times" "real times" + (const "cic:/Coq/Reals/Rdefinitions/Rmult.con"); + DisambiguateChoices.add_binary_op "divide" "real divide" + (const "cic:/Coq/Reals/Rdefinitions/Rdiv.con"); + DisambiguateChoices.add_unary_op "uminus" "real unary minus" + (const "cic:/Coq/Reals/Rdefinitions/Ropp.con"); + + DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'" + (mutind "cic:/Coq/Init/Peano/le.ind"); + DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'" + (const "cic:/Coq/Reals/Rdefinitions/Rle.con"); + DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'" + (const "cic:/Coq/Init/Peano/ge.con"); + DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'" + (const "cic:/Coq/Reals/Rdefinitions/Rge.con"); + DisambiguateChoices.add_binary_op "lt" "natural 'less than'" + (const "cic:/Coq/Init/Peano/lt.con"); + DisambiguateChoices.add_binary_op "lt" "real 'less than'" + (const "cic:/Coq/Reals/Rdefinitions/Rlt.con"); + DisambiguateChoices.add_binary_op "gt" "natural 'greater than'" + (const "cic:/Coq/Init/Peano/gt.con"); + DisambiguateChoices.add_binary_op "gt" "real 'greater than'" + (const "cic:/Coq/Reals/Rdefinitions/Rgt.con"); + DisambiguateChoices.add_symbol_choice "neq" + ("not equal to (leibnitz)", + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise DisambiguateChoices.Invalid_choice + in + Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; + Cic.Appl [ + Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + Cic.Implicit (Some `Type); t1; t2 ] ])); + DisambiguateChoices.add_symbol_choice "neq" + ("not equal to (sort Type)", + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise DisambiguateChoices.Invalid_choice + in + Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; + Cic.Appl [ + Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); + Cic.Implicit (Some `Type); t1; t2 ] ])); diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index efe959de8..26fc36c78 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -162,7 +162,7 @@ EXTEND return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] - | "eq" LEFTA + | "relop" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) ] diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 06f18080d..ca5f1449c 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -63,7 +63,9 @@ let refine metasenv context term = Ko let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = - snd (Environment.find item env) env num args + try + snd (Environment.find item env) env num args + with Not_found -> assert false (* TODO move it to Cic *) let find_in_environment name context = @@ -274,10 +276,15 @@ let domain_of_term ~context ast = | CicAst.AttributedTerm (_, term) -> aux loc context term | CicAst.Appl terms -> List.fold_left (fun dom term -> aux loc context term @ dom) [] terms - | CicAst.Binder (_, (var, typ), body) -> + | CicAst.Binder (kind, (var, typ), body) -> + let kind_dom = + match kind with + | `Exists -> [ Symbol ("exists", 0) ] + | _ -> [] + in let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in - body_dom @ type_dom + body_dom @ type_dom @ kind_dom | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index aa203f8be..c74566f20 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -41,6 +41,24 @@ let add_symbol_choice symbol codomain_item = in Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices) +let add_binary_op symbol dsc appl_head = + add_symbol_choice symbol + (dsc, + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Invalid_choice + in + Cic.Appl [ appl_head; t1; t2 ])) + +let add_unary_op symbol dsc appl_head = + add_symbol_choice symbol + (dsc, + (fun env _ args -> + let t = match args with [t] -> t | _ -> raise Invalid_choice in + Cic.Appl [ appl_head; t ])) + let add_num_choice choice = num_choices := choice :: !num_choices let lookup_symbol_choices symbol = @@ -63,3 +81,13 @@ let lookup_num_by_dsc dsc = List.find (has_description dsc) !num_choices with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc)) + (** initial table contents *) + +let _ = + let uri s = UriManager.uri_of_string s in + let const s = Cic.Const (uri s, []) in + let mutind s = Cic.MutInd (uri s, 0, []) in + add_binary_op "exists" "exists" (mutind "cic:/Coq/Init/Logic/ex.ind"); + add_binary_op "exists" "exists over terms with sort Type" + (mutind "cic:/Coq/Init/Logic_Type/exT.ind"); + diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli index 3a6e92f55..87d731e27 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli @@ -25,7 +25,7 @@ open DisambiguateTypes -(** {2 Choice registration interface} *) +(** {2 Choice registration low-level interface} *) (** to be raised when a choice is invalid due to some given parameter (e.g. * wrong number of Cic.term arguments received) *) @@ -40,6 +40,18 @@ val add_symbol_choice: string -> codomain_item -> unit (** register a new number choice *) val add_num_choice: codomain_item -> unit +(** {2 Choice registration high-level interface} *) + + (** @param symbol + * @param description + * @param term cic application head *) +val add_binary_op: string -> string -> Cic.term -> unit + + (** @param symbol + * @param description + * @param term cic application head *) +val add_unary_op: string -> string -> Cic.term -> unit + (** {2 Choices lookup} * for user defined aliases *) diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 1d47711da..fdbc75bf1 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -46,7 +46,14 @@ EXTEND ]; END +(* TODO a lot of hard coded URIs, move them in HelmLibraryObjects *) + let _ = + (* TODO cut-and-pasted code: here, in arit_notation.ml and + * disambiguateChoices.ml *) + let uri s = UriManager.uri_of_string s in + let const s = Cic.Const (uri s, []) in + let mutind s = Cic.MutInd (uri s, 0, []) in DisambiguateChoices.add_symbol_choice "eq" ("leibnitz's equality", (fun interp _ args -> @@ -58,5 +65,23 @@ let _ = Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 - ])) + ])); + DisambiguateChoices.add_symbol_choice "eq" + ("equality over objects with sort Type", + (fun interp _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise DisambiguateChoices.Invalid_choice + in + Cic.Appl [ + Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); + Cic.Implicit (Some `Type); t1; t2 + ])); + DisambiguateChoices.add_binary_op "and" "logical and" + (mutind "cic:/Coq/Init/Logic/and.ind"); + DisambiguateChoices.add_binary_op "or" "logical or" + (mutind "cic:/Coq/Init/Logic/or.ind"); + DisambiguateChoices.add_unary_op "not" "logical not" + (const "cic:/Coq/Init/Logic/not.con"); -- 2.39.2