From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 14:01:46 +0000 (+0000) Subject: New command default "foo" uri1 ... urin X-Git-Tag: PRE_GETTER_STORAGE~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9af753c66a80cb4f50f32e63272f3830cba306c;p=helm.git New command default "foo" uri1 ... urin to set uri1 ... urin as the default foo. Actually it can be used to set the current equality, true, false and absurd like this: default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri. default "true" trueuri. default "false" falseuri. default "absurd" absurduri. --- diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 74dff2733..45305130d 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -17,9 +17,5 @@ cicUtil.cmo: cic.cmo cicUtil.cmi cicUtil.cmx: cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi -matitaLibraryObjects.cmo: matitaLibraryObjects.cmi -matitaLibraryObjects.cmx: matitaLibraryObjects.cmi -libraryObjects.cmo: matitaLibraryObjects.cmi helmLibraryObjects.cmi \ - libraryObjects.cmi -libraryObjects.cmx: matitaLibraryObjects.cmx helmLibraryObjects.cmx \ - libraryObjects.cmi +libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi +libraryObjects.cmx: helmLibraryObjects.cmx libraryObjects.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 9a3d05383..d73177b45 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -9,7 +9,6 @@ INTERFACE_FILES = \ cicParser.mli \ cicUtil.mli \ helmLibraryObjects.mli \ - matitaLibraryObjects.mli \ libraryObjects.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml index f7613fe19..6a1e8a122 100644 --- a/helm/ocaml/cic/libraryObjects.ml +++ b/helm/ocaml/cic/libraryObjects.ml @@ -23,41 +23,75 @@ * http://helm.cs.unibo.it/ *) -(*CSC: how can we choose between the two libraries? *) -let eq_URI = - MatitaLibraryObjects.Equality.eq_URI +(**** TABLES ****) + +(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *) +let eq_URIs_ref = + ref [HelmLibraryObjects.Logic.eq_URI, + HelmLibraryObjects.Logic.sym_eq_URI, + HelmLibraryObjects.Logic.trans_eq_URI, + HelmLibraryObjects.Logic.eq_ind_URI, + HelmLibraryObjects.Logic.eq_ind_r_URI];; + +let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI] +let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI] +let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI] + + +(**** SET_DEFAULT ****) + +exception NotRecognized;; + +(* insert an element in front of the list, removing from the list all the + previous elements with the same key associated *) +let insert_unique e extract l = + let uri = extract e in + let l' = + List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l + in + e :: l' + +let set_default what l = + match what,l with + "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] -> + eq_URIs_ref := + insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI) + (fun x,_,_,_,_ -> x) !eq_URIs_ref + | "true",[true_URI] -> + true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref + | "false",[false_URI] -> + true_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref + | "absurd",[absurd_URI] -> + absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref + | _,_ -> raise NotRecognized + +(**** LOOKUP FUNCTIONS ****) + +let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq let is_eq_URI uri = - UriManager.eq uri HelmLibraryObjects.Logic.eq_URI || - UriManager.eq uri MatitaLibraryObjects.Equality.eq_URI - -exception Not_recognized;; - -let something_URI coq matita ~eq = - if UriManager.eq eq HelmLibraryObjects.Logic.eq_URI then coq - else if UriManager.eq eq MatitaLibraryObjects.Equality.eq_URI then matita - else raise Not_found - -let eq_ind_URI = - something_URI - HelmLibraryObjects.Logic.eq_ind_URI - MatitaLibraryObjects.Equality.eq_ind_URI - -let eq_ind_r_URI = - something_URI - HelmLibraryObjects.Logic.eq_ind_r_URI - MatitaLibraryObjects.Equality.eq_ind_r_URI - -let sym_eq_URI = - something_URI - HelmLibraryObjects.Logic.sym_eq_URI - MatitaLibraryObjects.Equality.sym_eq_URI - -let trans_eq_URI = - something_URI - HelmLibraryObjects.Logic.trans_eq_URI - MatitaLibraryObjects.Equality.trans_eq_URI - -let true_URI = MatitaLibraryObjects.Logic.true_URI -let false_URI = MatitaLibraryObjects.Logic.false_URI -let absurd_URI = MatitaLibraryObjects.Logic.absurd_URI + List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref + +let sym_eq_URI ~eq:uri = + try + let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise NotRecognized + +let trans_eq_URI ~eq:uri = + try + let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise NotRecognized + +let eq_ind_URI ~eq:uri = + try + let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise NotRecognized + +let eq_ind_r_URI ~eq:uri = + try + let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise NotRecognized + +let true_URI () = List.hd !true_URIs_ref +let false_URI () = List.hd !false_URIs_ref +let absurd_URI () = List.hd !absurd_URIs_ref diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli index 859b4e732..3ca7e7292 100644 --- a/helm/ocaml/cic/libraryObjects.mli +++ b/helm/ocaml/cic/libraryObjects.mli @@ -23,12 +23,13 @@ * http://helm.cs.unibo.it/ *) -(*CSC: how can we choose between the two libraries? *) -val eq_URI : UriManager.uri +val set_default : string -> UriManager.uri list -> unit + +val eq_URI : unit -> UriManager.uri val is_eq_URI : UriManager.uri -> bool -exception Not_recognized;; +exception NotRecognized;; val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri @@ -36,6 +37,6 @@ val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri -val false_URI : UriManager.uri -val true_URI : UriManager.uri -val absurd_URI : UriManager.uri +val false_URI : unit -> UriManager.uri +val true_URI : unit -> UriManager.uri +val absurd_URI : unit -> UriManager.uri diff --git a/helm/ocaml/cic/matitaLibraryObjects.ml b/helm/ocaml/cic/matitaLibraryObjects.ml deleted file mode 100644 index 0a4b4f11e..000000000 --- a/helm/ocaml/cic/matitaLibraryObjects.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let uri = UriManager.uri_of_string;; - -module Equality = - struct - let eq_URI = uri "cic:/matita/equality/eq.ind" - let eq_ind_URI = uri "cic:/matita/equality/eq_ind.con" - let eq_ind_r_URI = uri "cic:/matita/equality/eq_ind_r.con" - let sym_eq_URI = uri "cic:/matita/equality/sym_eq.con" - let trans_eq_URI = uri "cic:/matita/equality/trans_eq.con" - end - -module Logic = - struct - let true_URI = uri "cic:/matita/logic/True.ind" - let false_URI = uri "cic:/matita/logic/False.ind" - let absurd_URI = uri "cic:/matita/logic/absurd.ind" - end diff --git a/helm/ocaml/cic/matitaLibraryObjects.mli b/helm/ocaml/cic/matitaLibraryObjects.mli deleted file mode 100644 index 57311fde7..000000000 --- a/helm/ocaml/cic/matitaLibraryObjects.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -module Equality : - sig - val eq_URI : UriManager.uri - val eq_ind_URI : UriManager.uri - val eq_ind_r_URI : UriManager.uri - val sym_eq_URI : UriManager.uri - val trans_eq_URI : UriManager.uri - end - -module Logic : - sig - val true_URI : UriManager.uri - val false_URI : UriManager.uri - val absurd_URI : UriManager.uri - end diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 760b34a42..59bb1bc81 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -645,6 +645,9 @@ EXTEND TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) | IDENT "include" ; path = QSTRING -> TacticAst.Include (loc,path) + | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> + let uris = List.map UriManager.uri_of_string uris in + TacticAst.Default (loc,what,uris) ]]; executable: [ diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index a051c2af6..0dfb48aed 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -126,6 +126,7 @@ type obj = (string * CicAst.term) list type ('term,'obj) command = + | Default of loc * string * UriManager.uri list | Include of loc * string | Set of loc * string * string | Drop of loc diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 7802e582e..21bf33a0a 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -227,6 +227,9 @@ let pp_command = function | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term) | Alias (_,s) -> pp_alias s | Obj (_,obj) -> pp_obj obj + | Default (_,what,uris) -> + sprintf "default \"%s\" %s" what + (String.concat " " (List.map UriManager.string_of_uri uris)) let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac @@ -265,4 +268,5 @@ let pp_cic_command = function | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term) | Set (_, _, _) | Alias (_,_) + | Default (_,_,_) | Obj (_,_) -> assert false (* not implemented *) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 21fc2b33c..0f06351b4 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -276,8 +276,8 @@ let discriminate'_tac ~term = C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(LibraryObjects.false_URI,0,[])) - else (C.MutInd(LibraryObjects.true_URI,0,[])) + then (C.MutInd(LibraryObjects.false_URI (),0,[])) + else (C.MutInd(LibraryObjects.true_URI (),0,[])) in aux red_ty 1 ) constructor_list @@ -287,7 +287,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(LibraryObjects.false_URI,0,[]))) + ~term:(C.MutInd(LibraryObjects.false_URI (),0,[]))) status in (match goals' with diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 3d54fd18b..e4520292d 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -175,7 +175,7 @@ let replace_tac ~pattern ~with_what = ~start:( P.cut_tac (C.Appl [ - (C.MutInd (LibraryObjects.eq_URI, 0, [])) ; + (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ; ty_of_with_what ; what ; with_what])) diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index b86cf43d6..ee76921b2 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -37,7 +37,7 @@ let absurd_tac ~term = then ProofEngineTypes.apply_tactic (P.apply_tac ~term:( - C.Appl [(C.Const (LibraryObjects.absurd_URI , [] )) ; + C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; term ; ty]) ) status @@ -61,7 +61,7 @@ let contradiction_tac = ~start: (EliminationTactics.elim_type_tac ~term: - (C.MutInd (LibraryObjects.false_URI, 0, []))) + (C.MutInd (LibraryObjects.false_URI (), 0, []))) ~continuation: VariousTactics.assumption_tac)) status with