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.
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
cicParser.mli \
cicUtil.mli \
helmLibraryObjects.mli \
- matitaLibraryObjects.mli \
libraryObjects.mli
IMPLEMENTATION_FILES = \
cic.ml $(INTERFACE_FILES:%.mli=%.ml)
* 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
* 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
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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
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: [
(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
| 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
| Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
| Set (_, _, _)
| Alias (_,_)
+ | Default (_,_,_)
| Obj (_,_) -> assert false (* not implemented *)
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
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
~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]))
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
~start:
(EliminationTactics.elim_type_tac
~term:
- (C.MutInd (LibraryObjects.false_URI, 0, [])))
+ (C.MutInd (LibraryObjects.false_URI (), 0, [])))
~continuation: VariousTactics.assumption_tac))
status
with
projects / helm.git / commitdiff