| hd :: tl -> aux ([sep; hd] @ acc) tl
in
aux []
+
+let rec list_findopt f l =
+ let rec aux = function
+ | [] -> None
+ | x::tl ->
+ (match f x with
+ | None -> aux tl
+ | Some _ as rc -> rc)
+ in
+ aux l
(** {2 File predicates} *)
?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on lists *)
val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *)
val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*)
+val list_findopt: ('a -> 'b option) -> 'a list -> 'b option
(** {2 Debugging & Profiling} *)
}
type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit }
+
+let coercion_moo_statement_of uri =
+ GrafiteAst.Coercion
+ (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false)
let eval_coercion status ~add_composites coercion =
let uri = CicUtil.uri_of_term coercion in
- let status = MatitaSync.add_coercion status ~add_composites uri in
+ let basedir = Helm_registry.get "matita.basedir" in
+ let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
+ let moo_content = coercion_moo_statement_of uri in
+ let status = GrafiteTypes.add_moo_content [moo_content] status in
+ let status = MatitaSync.add_coercion status uri compounds in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
let eval_tactical ~disambiguate_tactic status tac =
let eval_comment status c = status
+(* since the record syntax allows to declare coercions, we have to put this
+ * information inside the moo *)
+let add_coercions_of_record_to_moo obj lemmas status =
+ let attributes = CicUtil.attributes_of_obj obj in
+ let is_record = function `Class (`Record att) -> Some att | _-> None in
+ match HExtlib.list_findopt is_record attributes with
+ | None -> status
+ | Some fields ->
+ let is_a_coercion uri =
+ try
+ let obj,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let attrs = CicUtil.attributes_of_obj obj in
+ List.mem (`Class `Projection) attrs
+ with Not_found -> assert false
+ in
+ (* looking at the fields we can know the 'wanted' coercions, but not the
+ * actually generated ones. So, only the intersection between the wanted
+ * and the actual should be in the moo as coercion, while everithing in
+ * lemmas should go as aliases *)
+ let wanted_coercions =
+ HExtlib.filter_map
+ (function
+ | (name,true) ->
+ Some
+ (UriManager.uri_of_string
+ (GrafiteTypes.qualify status name ^ ".con"))
+ | _ -> None)
+ fields
+ in
+ prerr_endline "wanted coercions:";
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ wanted_coercions;
+ let coercions, moo_content =
+ List.split
+ (HExtlib.filter_map
+ (fun uri ->
+ let is_a_wanted_coercion =
+ List.exists (UriManager.eq uri) wanted_coercions in
+ if is_a_coercion uri && is_a_wanted_coercion then
+ Some (uri, coercion_moo_statement_of uri)
+ else
+ None)
+ lemmas)
+ in
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ coercions;
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ List.fold_left
+ (fun status uri ->
+ MatitaSync.add_coercion status uri [])
+ status coercions
+
+let add_obj uri obj status =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = LibrarySync.add_obj uri obj basedir in
+ let status =
+ {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects} in
+ let status = MatitaSync.add_obj uri obj lemmas status in
+ status, lemmas
+
let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd ->
let status,cmd = disambiguate_command status cmd in
let cmd,notation_ids' = CicNotation.process_notation cmd in
"Proof not completed! metasenv is not empty!");
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some bo,ty,[],[]) in
- MatitaSync.add_obj uri obj
+ let status, _lemmas = add_obj uri obj status in
+ (* should we assert lemmas = [] ? *)
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
| GrafiteAst.Coercion (loc, coercion, add_composites) ->
eval_coercion status ~add_composites coercion
raise (GrafiteTypes.Command_error (
"metasenv not empty while giving a definition with body: " ^
CicMetaSubst.ppmetasenv [] metasenv));
- MatitaSync.add_obj uri obj
+ let status, lemmas = add_obj uri obj status in
+ let status = add_coercions_of_record_to_moo obj lemmas status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex ->
| Cic.Variable _
| Cic.CurrentProof _ -> assert false
-let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let lemmas = LibrarySync.add_obj uri obj basedir in
- let status = {status with objects = uri::status.objects} in
+let add_obj uri obj lemmas status =
List.fold_left add_alias_for_constant
(add_aliases_for_object status uri obj) lemmas
let profiler = HExtlib.profile "add_obj" in
fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
-let add_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
- let compounds = CoercGraph.add_coercion uri in
- let status =
- if add_composites then
- (List.iter (fun (u,_) ->
- prerr_endline (UriManager.string_of_uri u)) compounds;
- List.fold_left (fun s (uri,o) -> add_obj uri o s) status compounds )
- else
- status
- in
- let status =
- {status with coercions = uri :: List.map fst compounds @ status.coercions}
- in
- let statement_of name =
- GrafiteAst.Coercion
- (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in
- let moo_content = [statement_of (UriManager.name_of_uri uri)] in
- let status = GrafiteTypes.add_moo_content moo_content status in
- List.fold_left add_alias_for_constant status (List.map fst compounds)
+let add_coercion status uri compounds =
+ let status = {status with coercions = uri :: status.coercions} in
+ List.fold_left add_alias_for_constant status compounds
module OrderedUri =
struct
in
let debug_list = ref [] in
List.iter
- (fun uri -> CoercGraph.remove_coercion uri)
+ (fun uri -> LibrarySync.remove_coercion uri)
coercions_to_remove;
List.iter LibrarySync.remove_obj objs_to_remove;
List.iter CicNotation.remove_notation notation_to_remove
let init () =
- CoercGraph.remove_all ();
+ LibrarySync.remove_all_coercions ();
LibraryObjects.reset_defaults ();
{
aliases = DisambiguateTypes.Environment.empty;
*)
val add_obj:
- UriManager.uri -> Cic.obj ->
+ UriManager.uri -> Cic.obj -> UriManager.uri list ->
GrafiteTypes.status -> GrafiteTypes.status
val add_coercion:
- GrafiteTypes.status -> add_composites:bool -> UriManager.uri ->
+ GrafiteTypes.status -> UriManager.uri -> UriManager.uri list ->
GrafiteTypes.status
val time_travel:
+cicCoercion.cmi: coercDb.cmi
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
cicRecord.cmo: cicRecord.cmi
libraryDb.cmx: libraryDb.cmi
coercDb.cmo: coercDb.cmi
coercDb.cmx: coercDb.cmi
+cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
coercGraph.cmo: coercDb.cmi coercGraph.cmi
coercGraph.cmx: coercDb.cmx coercGraph.cmi
-librarySync.cmo: libraryDb.cmi coercGraph.cmi cicRecord.cmi cicElim.cmi \
- librarySync.cmi
-librarySync.cmx: libraryDb.cmx coercGraph.cmx cicRecord.cmx cicElim.cmx \
- librarySync.cmi
+librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \
+ cicElim.cmi cicCoercion.cmi librarySync.cmi
+librarySync.cmx: libraryDb.cmx coercGraph.cmx coercDb.cmx cicRecord.cmx \
+ cicElim.cmx cicCoercion.cmx librarySync.cmi
libraryNoDb.cmo: libraryNoDb.cmi
libraryNoDb.cmx: libraryNoDb.cmi
libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
libraryMisc.mli \
libraryDb.mli \
coercDb.mli \
+ cicCoercion.mli \
coercGraph.mli \
librarySync.mli \
libraryNoDb.mli \
--- /dev/null
+(* Copyright (C) 2005, 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 debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+(* given the new coercion uri from src to tgt returns the list
+ * of new coercions to create. hte list elements are
+ * (source, list of coercions to follow, target)
+ *)
+let get_closure_coercions src tgt uri coercions =
+ let eq_carr s t =
+ try
+ CoercDb.eq_carr s t
+ with
+ | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+ in
+ match src,tgt with
+ | CoercDb.Uri _, CoercDb.Uri _ ->
+ let c_from_tgt =
+ List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
+ in
+ let c_to_src =
+ List.filter (fun (_,t,_) -> eq_carr t src) coercions
+ in
+ (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
+ (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
+ (List.fold_left (
+ fun l (s,_,u1) ->
+ ((List.map (fun (_,t,u2) ->
+ (s,[u1;uri;u2],t)
+ )c_from_tgt)@l) )
+ [] c_to_src)
+ | _ -> [] (* do not close in case source or target is not an indty ?? *)
+;;
+
+let obj_attrs = [`Class `Coercion; `Generated]
+
+(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
+let generate_composite_closure c1 c2 univ =
+ let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
+ let rec mk_rels n =
+ match n with
+ | 0 -> []
+ | _ -> (Cic.Rel n) :: (mk_rels (n-1))
+ in
+ let rec compose k =
+ function
+ | Cic.Prod (name,src,tgt) ->
+ let name =
+ match name with
+ | Cic.Anonymous -> Cic.Name "x"
+ | _ -> name
+ in
+ Cic.Lambda (name,src,compose (k+1) tgt)
+ | Cic.Appl (he::tl) ->
+ Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
+ | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
+ in
+ let c = compose 0 c1_ty in
+ let c_ty,univ =
+ try
+ CicTypeChecker.type_of_aux' [] [] c univ
+ with CicTypeChecker.TypeCheckerFailure s as exn ->
+ debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s"
+ (CicPp.ppterm c) (Lazy.force s)));
+ raise exn
+ in
+ let cleaned_ty =
+ FreshNamesGenerator.clean_dummy_dependent_types c_ty
+ in
+ let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
+ obj,univ
+;;
+
+(* removes from l the coercions that are in !coercions *)
+let filter_duplicates l coercions =
+ List.filter (
+ fun (src,_,tgt) ->
+ not (List.exists (fun (s,t,u) ->
+ CoercDb.eq_carr s src &&
+ CoercDb.eq_carr t tgt)
+ coercions))
+ l
+
+(* given a new coercion uri from src to tgt returns
+ * a list of (new coercion uri, coercion obj, universe graph)
+ *)
+let close_coercion_graph src tgt uri =
+ (* check if the coercion already exists *)
+ let coercions = CoercDb.to_list () in
+ let todo_list = get_closure_coercions src tgt uri coercions in
+ let todo_list = filter_duplicates todo_list coercions in
+ let new_coercions =
+ List.map (
+ fun (src, l , tgt) ->
+ match l with
+ | [] -> assert false
+ | he :: tl ->
+ let first_step =
+ Cic.Constant ("",
+ Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+ Cic.Sort Cic.Prop, [], obj_attrs)
+ in
+ let o,_ =
+ List.fold_left (fun (o,univ) coer ->
+ match o with
+ | Cic.Constant (_,Some c,_,[],_) ->
+ generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri
+ coer)) univ
+ | _ -> assert false
+ ) (first_step, CicUniv.empty_ugraph) tl
+ in
+ let name_src = CoercDb.name_of_carr src in
+ let name_tgt = CoercDb.name_of_carr tgt in
+ let name = name_tgt ^ "_of_" ^ name_src in
+ let buri = UriManager.buri_of_uri uri in
+ let c_uri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+ in
+ let named_obj =
+ match o with
+ | Cic.Constant (_,bo,ty,vl,attrs) ->
+ Cic.Constant (name,bo,ty,vl,attrs)
+ | _ -> assert false
+ in
+ ((src,tgt,c_uri,named_obj))
+ ) todo_list
+ in
+ new_coercions
+;;
+
--- /dev/null
+(* Copyright (C) 2005, 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/
+ *)
+
+(* This module implements the Coercions transitive closure *)
+
+val close_coercion_graph:
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+
src, tgt
with Not_found -> assert false (* uri must be a coercion *)
+let term_of_carr = function
+ | Uri u -> CicUtil.term_of_uri u
+ | Sort s -> Cic.Sort s
+ | Term _ -> assert false
+
+
+
*)
- (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **)
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
+ *
+ * and may be merged with CicCoercion...
+ *
+ * **)
(** XXX WARNING: non-reentrant *)
val is_a_coercion: UriManager.uri -> bool
val get_carr: UriManager.uri -> coerc_carr * coerc_carr
-
+val term_of_carr: coerc_carr -> Cic.term
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-
(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion src tgt =
try
let tgt_uri = CoercDb.coerc_carr_of_term tgt in
look_for_coercion src_uri tgt_uri
-(* given the new coercion uri from src to tgt returns the list
- * of new coercions to create. hte list elements are
- * (source, list of coercions to follow, target)
- *)
-let get_closure_coercions src tgt uri coercions =
- let eq_carr s t =
- try
- CoercDb.eq_carr s t
- with
- | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
- in
- match src,tgt with
- | CoercDb.Uri _, CoercDb.Uri _ ->
- let c_from_tgt =
- List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
- in
- let c_to_src =
- List.filter (fun (_,t,_) -> eq_carr t src) coercions
- in
- (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
- (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
- (List.fold_left (
- fun l (s,_,u1) ->
- ((List.map (fun (_,t,u2) ->
- (s,[u1;uri;u2],t)
- )c_from_tgt)@l) )
- [] c_to_src)
- | _ -> [] (* do not close in case source or target is not an indty ?? *)
-;;
-
-let obj_attrs = [`Class `Coercion; `Generated]
-
-(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure c1 c2 univ =
- let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
- let rec mk_rels n =
- match n with
- | 0 -> []
- | _ -> (Cic.Rel n) :: (mk_rels (n-1))
- in
- let rec compose k =
- function
- | Cic.Prod (name,src,tgt) ->
- let name =
- match name with
- | Cic.Anonymous -> Cic.Name "x"
- | _ -> name
- in
- Cic.Lambda (name,src,compose (k+1) tgt)
- | Cic.Appl (he::tl) ->
- Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
- | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
- in
- let c = compose 0 c1_ty in
- let c_ty,univ =
- try
- CicTypeChecker.type_of_aux' [] [] c univ
- with CicTypeChecker.TypeCheckerFailure s as exn ->
- debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s"
- (CicPp.ppterm c) (Lazy.force s)));
- raise exn
- in
- let cleaned_ty =
- FreshNamesGenerator.clean_dummy_dependent_types c_ty
- in
- let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
- obj,univ
-;;
-
-(* removes from l the coercions that are in !coercions *)
-let filter_duplicates l coercions =
- List.filter (
- fun (src,_,tgt) ->
- not (List.exists (fun (s,t,u) ->
- CoercDb.eq_carr s src &&
- CoercDb.eq_carr t tgt)
- coercions))
- l
-
-let term_of_carr = function
- | CoercDb.Uri u -> CicUtil.term_of_uri u
- | CoercDb.Sort s -> Cic.Sort s
- | CoercDb.Term _ -> assert false
-
-(* given a new coercion uri from src to tgt returns
- * a list of (new coercion uri, coercion obj, universe graph)
- *)
-let close_coercion_graph src tgt uri =
- (* check if the coercion already exists *)
- let coercions = CoercDb.to_list () in
- let todo_list = get_closure_coercions src tgt uri coercions in
- let todo_list = filter_duplicates todo_list coercions in
- let new_coercions =
- List.map (
- fun (src, l , tgt) ->
- match l with
- | [] -> assert false
- | he :: tl ->
- let first_step =
- Cic.Constant ("",
- Some (term_of_carr (CoercDb.Uri he)),
- Cic.Sort Cic.Prop, [], obj_attrs)
- in
- let o,_ =
- List.fold_left (fun (o,univ) coer ->
- match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (term_of_carr (CoercDb.Uri
- coer)) univ
- | _ -> assert false
- ) (first_step, CicUniv.empty_ugraph) tl
- in
- let name_src = CoercDb.name_of_carr src in
- let name_tgt = CoercDb.name_of_carr tgt in
- let name = name_tgt ^ "_of_" ^ name_src in
- let buri = UriManager.buri_of_uri uri in
- let c_uri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- let named_obj =
- match o with
- | Cic.Constant (_,bo,ty,vl,attrs) ->
- Cic.Constant (name,bo,ty,vl,attrs)
- | _ -> assert false
- in
- ((src,tgt,c_uri,named_obj))
- ) todo_list
- in
- new_coercions
-;;
-
-let coercion_hashtbl = UriManager.UriHashtbl.create 3
-
-let add_coercion uri =
- let coer_ty,_ =
- CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
- CicUniv.empty_ugraph
- in
- (* we have to get the source and the tgt type uri
- * in Coq syntax we have already their names, but
- * since we don't support Funclass and similar I think
- * all the coercion should be of the form
- * (A:?)(B:?)T1->T2
- * So we should be able to extract them from the coercion type
- *)
- let extract_last_two_p ty =
- let rec aux = function
- | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
- | Cic.Prod( _, src, tgt) -> src, tgt
- | _ -> assert false
- in
- aux ty
- in
- let ty_src,ty_tgt = extract_last_two_p coer_ty in
- let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
- let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions = close_coercion_graph src_uri tgt_uri uri in
- UriManager.UriHashtbl.add coercion_hashtbl uri
- (List.map (fun (_,_,uri,_) -> uri) new_coercions);
- CoercDb.add_coercion (src_uri,tgt_uri,uri);
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- List.map (fun (_,_,uri,o) -> uri,o) new_coercions
-
-
-let remove_coercion uri =
- try
- let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
- UriManager.UriHashtbl.remove coercion_hashtbl uri;
- CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
- List.iter
- (fun u ->
- CoercDb.remove_coercion
- (fun (_,_,u1) -> UriManager.eq u u1))
- res;
- with
- Not_found -> ()
-
-let remove_all () =
- CoercDb.remove_coercion (fun (_,_,u1) -> true)
-
let is_a_coercion t =
try
let uri = CicUtil.uri_of_term t in
let source_of t =
try
let uri = CicUtil.uri_of_term t in
- term_of_carr (fst (CoercDb.get_carr uri))
+ CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
let target_of t =
try
let uri = CicUtil.uri_of_term t in
- term_of_carr (snd (CoercDb.get_carr uri))
+ CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
(* EOF *)
* http://cs.unibo.it/helm/.
*)
+(* This module implements the Query interface to the Coercion Graph *)
+
type coercion_search_result =
| SomeCoercion of Cic.term
| NoCoercion
val look_for_coercion :
Cic.term -> Cic.term -> coercion_search_result
-(* it returns the list of composite coercions *)
-(* composite coercions are always declared as such; they are added to the *)
-(* CoercDb adding them to the library is left to the caller *)
-val add_coercion:
- UriManager.uri ->
- (UriManager.uri * Cic.obj) list
-
-val remove_coercion: UriManager.uri -> unit
-
val is_a_coercion: Cic.term -> bool
val source_of: Cic.term -> Cic.term
val target_of: Cic.term -> Cic.term
-val remove_all: unit -> unit
let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
+(* uri |--> (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
+ *
+ * in case of remove_coercion uri, the first component is removed from the
+ * coercion DB, while the second is passed to remove_obj (and is not [] only if
+ * add_coercion is called with add_composites
+ * *)
+let coercion_hashtbl = UriManager.UriHashtbl.create 3
+
let merge_coercions obj =
let module C = Cic in
let rec aux2 = (fun (u,t) -> u,aux t)
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
ignore (LibraryDb.remove_uri uri);
- CoercGraph.remove_coercion uri;
+ (*CoercGraph.remove_coercion uri;*)
CicEnvironment.remove_obj uri)
to_remove
List.iter remove_single_obj !uris;
raise exn
+(* COERICONS ***********************************************************)
+
+let remove_all_coercions () =
+ UriManager.UriHashtbl.clear coercion_hashtbl;
+ CoercDb.remove_coercion (fun (_,_,u1) -> true)
+
+let add_coercion ~basedir ~add_composites uri =
+ let coer_ty,_ =
+ let coer = CicUtil.term_of_uri uri in
+ CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
+ in
+ (* we have to get the source and the tgt type uri
+ * in Coq syntax we have already their names, but
+ * since we don't support Funclass and similar I think
+ * all the coercion should be of the form
+ * (A:?)(B:?)T1->T2
+ * So we should be able to extract them from the coercion type
+ *
+ * Currently only (_:T1)T2 is supported.
+ * should we saturate it with metas in case we insert it?
+ *
+ *)
+ let extract_last_two_p ty =
+ let rec aux = function
+ | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) ->
+ assert false
+ (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
+ | Cic.Prod( _, src, tgt) -> src, tgt
+ | _ -> assert false
+ in
+ aux ty
+ in
+ let ty_src, ty_tgt = extract_last_two_p coer_ty in
+ let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+ let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+ let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
+ let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+ (* update the DB *)
+ List.iter
+ (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
+ new_coercions;
+ CoercDb.add_coercion (src_uri, tgt_uri, uri);
+ (* add the composites obj and they eventual lemmas *)
+ let lemmas =
+ if add_composites then
+ List.fold_left
+ (fun acc (_,_,uri,obj) ->
+ add_single_obj ~basedir uri obj;
+ uri::acc)
+ composite_uris new_coercions
+ else
+ []
+ in
+ (* store that composite_uris are related to uri. the first component is the
+ * stuff in the DB while the second is stuff for remove_obj *)
+ UriManager.UriHashtbl.add coercion_hashtbl uri
+ (composite_uris,if add_composites then composite_uris else []);
+ lemmas
+
+let remove_coercion uri =
+ try
+ let (composites_in_db, composites_in_lib) =
+ UriManager.UriHashtbl.find coercion_hashtbl uri
+ in
+ UriManager.UriHashtbl.remove coercion_hashtbl uri;
+ CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+ (* remove from the DB *)
+ List.iter
+ (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
+ composites_in_db;
+ (* remove composites from the lib *)
+ List.iter remove_single_obj composites_in_lib
+ with
+ Not_found -> () (* mhh..... *)
+
+
let generate_projections ~basedir uri fields =
let uris = ref [] in
let projections = CicRecord.projections_of uri (List.map fst fields) in
add_single_obj ~basedir uri obj;
let composites =
- if coercion then
- (* this is _NOT_ the place for THIS!!! *)
- (* MOO HANDLING IS MISSING *)
- let toadd = CoercGraph.add_coercion uri in
- List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd;
- List.map fst toadd
+ if coercion then
+ add_coercion ~basedir ~add_composites:true uri
else
[]
in
Not_found -> [] (*assert false*)
in
List.iter remove_single_obj (uri::uris)
+
(* Warning: it does not remove the dependencies on the object and on its *)
(* auxiliary lemmas! *)
val remove_obj: UriManager.uri -> unit
+
+(* Informs the library that [uri] is a coercion. *)
+(* This can generate some composite coercions that, if [add_composites] *)
+(* is true are added to the library. *)
+(* The list of added objects is returned. *)
+val add_coercion:
+ basedir:string -> add_composites:bool -> UriManager.uri ->
+ UriManager.uri list
+
+(* inverse of add_coercion, removes both the eventually created composite *)
+(* coercions and the information that [uri] and the composites are coercion *)
+val remove_coercion: UriManager.uri -> unit
+
+(* mh... *)
+val remove_all_coercions: unit -> unit
+
projects / helm.git / commitdiff