let premise_prefix = "prem:";;
let lemma_prefix = "lemma:";;
+let hide_coercions = ref true;;
+
(* e se mettessi la conversione di BY nell'apply_context ? *)
(* sarebbe carino avere l'invariante che la proof2pres
generasse sempre prove con contesto vuoto *)
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
else raise Not_a_proof
| C.AAppl (id,li) ->
- (try rewrite
+ (try coercion
+ seed li ~ids_to_inner_types ~ids_to_inner_sorts
+ with NotApplicable ->
+ try rewrite
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try inductive
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
- try transitivity
+ try transitivity
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
let subproofs, args =
}
| _ -> raise NotApplicable
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+ match li with
+ | ((Cic.AConst _) as he)::tl
+ | ((Cic.AMutInd _) as he)::tl
+ | ((Cic.AMutConstruct _) as he)::tl when
+ CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+ !hide_coercions ->
+ let rec last =
+ function
+ [] -> assert false
+ | [t] -> t
+ | _::tl -> last tl
+ in
+ acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ | _ -> raise NotApplicable
+
and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
let module C2A = Cic2acic in
val map_sequent :
Cic.annconjecture -> Cic.annterm Content.conjecture
+
+val hide_coercions: bool ref
+
fst (List.nth (constructors_of_inductive_type uri i) (j-1))
with Not_found -> assert false)
-let hide_coercions = ref true;;
let ast_of_acic0 term_info acic k =
let k = k term_info in
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
- !hide_coercions
+ !Acic2content.hide_coercions
then
let rec last =
function
* http://helm.cs.unibo.it/
*)
-val hide_coercions: bool ref
(** {2 Persistant state handling} *)
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
+ let try_coercion t subst metasenv context ugraph coercion_tgt c =
+ let coerced = Cic.Appl[c;t] in
+ try
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context coerced ugraph
+ in
+ let newt, tty, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
+ in
+ Some (newt, tty, subst, metasenv, ugraph)
+ with
+ | RefineFailure _ | Uncertain _ -> None
+ in
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context
subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion c ->
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context (Cic.Appl[c;t])
- ugraph in
- let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph
- newt coercion_tgt
- in
- newt, tty, subst, metasenv, ugraph)
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (try_coercion
+ t subst metasenv context ugraph coercion_tgt)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context
+ subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^
+ " that is not a sort"))))
in
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
CoercGraph.look_for_coercion coercion_src coercion_tgt
in
match boh with
- | CoercGraph.SomeCoercion c ->
- let newt,_,subst',metasenv',ugraph1 =
- type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
- ugraph1 in
- let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion context subst' metasenv'
- ugraph1 newt coercion_tgt
- in
- newt, tty, subst', metasenv', ugraph1
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context
subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (try_coercion
+ s' subst' metasenv' context ugraph1 coercion_tgt)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl s'
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^
+ " that is not a sort")))
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
let tgt_carr = CicMetaSubst.apply_subst subst ty in
(match CoercGraph.look_for_coercion source_carr tgt_carr
with
- | CoercGraph.SomeCoercion c ->
- let newt =
- match c with
- Cic.Appl l -> Cic.Appl (l @ [head])
- | _ -> Cic.Appl [c;head]
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ let newt =
+ match c with
+ | Cic.Appl l -> Cic.Appl (l @ [head])
+ | _ -> Cic.Appl [c;head]
+ in
+ (try
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ Some (newt, ty, subst, metasenv, ugraph)
+ with RefineFailure _ | Uncertain _ -> None))
+ candidates
in
- (try
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv newt t ugraph
- in
- debug_print
- (lazy
- ("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
- newt, ty, subst, metasenv, ugraph
- with
- RefineFailure _ ->
- prerr_endline ("#### Coercion not packed (Refine_failure): " ^
- CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
- assert false
- | Uncertain _ ->
- prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
- CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+ (match selected with
+ | Some x -> x
+ | None ->
+ prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
assert false)
| _ -> assert false) (* the composite coercion must exist *)
else
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion c ->
- try
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- (Cic.Appl[c;hete]) ugraph in
- let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv
- ugraph newt tgt_carr in
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- newt, subst, metasenv, ugraph
- with _ ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("The term " ^
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ try
+ let t = Cic.Appl[c;hete] in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ t ugraph
+ in
+ let newt, _, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv
+ ugraph newt tgt_carr
+ in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety s ugraph
+ in
+ Some (newt, subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ (match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn)
+ (* "\nReason: " ^ Lazy.force e*)))) exn))
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
cicNotationPres.cmx box.cmx content2pres.cmi
+objPp.cmo: content2pres.cmi boxPp.cmi objPp.cmi
+objPp.cmx: content2pres.cmx boxPp.cmx objPp.cmi
sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
box.cmi sequent2pres.cmi
sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
cicNotationPres.mli \
boxPp.mli \
content2pres.mli \
+ objPp.mli \
sequent2pres.mli \
$(NULL)
IMPLEMENTATION_FILES = \
let s_len = String.length s in
(fun _ -> s_len, [s])
-let render_to_strings size markup =
+let render_to_strings choose_action size markup =
let max_size = max_int in
let rec aux_box =
function
| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false
- | Box.Action (_, hd :: _) -> aux_box hd
+ | Box.Action (_, l) -> aux_box (choose_action l)
| Box.Object (_, o) -> aux_mpres o
| Box.H (attrs, children) ->
let spacing = want_spacing attrs in
in
snd (aux_mpres markup size)
-let render_to_string size markup =
- String.concat "\n" (render_to_strings size markup)
+let render_to_string choose_action size markup =
+ String.concat "\n" (render_to_strings choose_action size markup)
*)
(** @return rows list of rows *)
-val render_to_strings: int -> CicNotationPres.markup -> string list
+val render_to_strings:
+ (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) ->
+ int -> CicNotationPres.markup -> string list
(** helper function
* @return s, concatenation of the return value of render_to_strings above
* with newlines as separators *)
-val render_to_string: int -> CicNotationPres.markup -> string
+val render_to_string:
+ (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) ->
+ int -> CicNotationPres.markup -> string
("<>", <:unicode<neq>>); (":=", <:unicode<def>>);
]
-let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
let regexp uri =
("cic:/" | "theory:/") (* schema *)
--- /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 obj_to_string n obj =
+ let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
+ let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
+ let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
+ BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
--- /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/
+ *)
+
+val obj_to_string: int -> Cic.obj -> string
+
let eval_coercion status ~add_composites uri =
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
- let moo_content = coercion_moo_statement_of uri in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
+ let moo_content =
+ List.map coercion_moo_statement_of (uri::compounds)
+ in
+ let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
compounds
let obj,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
- List.mem (`Class `Projection) attrs
+ List.mem (`Class `Coercion) attrs
with Not_found -> assert false
in
(* looking at the fields we can know the 'wanted' coercions, but not the
| _ -> None)
fields
in
- (*
- prerr_endline "wanted coercions:";
+ (*prerr_endline "wanted coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
wanted_coercions; *)
(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
+ 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
- (* prerr_endline "actual coercions:";
+ (*prerr_endline "actual coercions:";
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ coercions;
+ prerr_endline "lemmas was:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions; *)
+ lemmas; *)
let status = GrafiteTypes.add_moo_content moo_content status in
{status with
GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
match src,tgt with
| CoercDb.Uri _, CoercDb.Uri _ ->
let c_from_tgt =
- List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
+ List.filter
+ (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src))
+ coercions
in
let c_to_src =
- List.filter (fun (_,t,_) -> eq_carr t src) coercions
+ List.filter
+ (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt))
+ 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)
+ (HExtlib.flatten_map
+ (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+ (HExtlib.flatten_map
+ (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+ (HExtlib.flatten_map
+ (fun (s,_,u1l) ->
+ HExtlib.flatten_map
+ (fun (_,t,u2l) ->
+ HExtlib.flatten_map
+ (fun u1 ->
+ List.map
+ (fun u2 -> (s,[u1;uri;u2],t))
+ u2l)
+ u1l)
+ c_from_tgt)
+ c_to_src)
| _ -> [] (* do not close in case source or target is not an indty ?? *)
;;
(* 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) ->
+ fun (src,l1,tgt) ->
+ not (List.exists (fun (s,t,l2) ->
CoercDb.eq_carr s src &&
- CoercDb.eq_carr t tgt)
+ CoercDb.eq_carr t tgt &&
+ try
+ List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+ with
+ | Invalid_argument "List.for_all2" -> false)
coercions))
l
+let mangle s t l =
+ (*List.fold_left
+ (fun s x -> s ^ "_" ^ x)
+ (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*)
+ s ^ "_OF_" ^ t
+;;
+
+exception ManglingFailed of string
+
+let number_if_already_defined buri name =
+ let rec aux n =
+ let suffix = if n > 0 then string_of_int n else "" in
+ let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in
+ try
+ let _ = Http_getter.resolve ~writable:true uri in
+ if Http_getter.exists uri then
+ begin
+ HLog.warn ("Uri " ^ uri ^ " already exists.");
+ if n < 10 then aux (n+1) else
+ raise
+ (ManglingFailed
+ ("Unable to give an altenative name to " ^
+ buri ^ "/" ^ name ^ ".con"))
+ end
+ else
+ UriManager.uri_of_string uri
+ with
+ | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri
+ | Http_getter_types.Unresolvable_URI _ -> assert false
+ in
+ aux 0
+;;
+
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
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 =
- HExtlib.filter_map (
- fun (src, l , tgt) ->
- try
- (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 rt c
- (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+ try
+ let new_coercions =
+ HExtlib.filter_map (
+ fun (src, l , tgt) ->
+ try
+ (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 rt 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 by = List.map UriManager.name_of_uri l in
+ let name = mangle name_tgt name_src by in
+ let buri = UriManager.buri_of_uri uri in
+ let c_uri = number_if_already_defined buri name in
+ let named_obj =
+ match o with
+ | Cic.Constant (_,bo,ty,vl,attrs) ->
+ Cic.Constant (name,bo,ty,vl,attrs)
| _ -> 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
- Some ((src,tgt,c_uri,named_obj)))
- with UnableToCompose -> None
- ) todo_list
- in
- new_coercions
+ in
+ Some ((src,tgt,c_uri,named_obj)))
+ with UnableToCompose -> None
+ ) todo_list
+ in
+ new_coercions
+ with ManglingFailed s -> HLog.error s; []
;;
let to_list () =
!db
-let add_coercion c =
- db := c :: !db
-
-let remove_coercion p =
- db := List.filter (fun u -> not(p u)) !db
+let rec myfilter p = function
+ | [] -> []
+ | (s,t,l)::tl ->
+ let l = List.filter (fun u -> not (p (s,t,u))) l in
+ if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
+;;
+
+let remove_coercion p = db := myfilter p !db;;
let find_coercion f =
- List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+ List.flatten
+ (List.map
+ (fun (_,_,x) -> x)
+ (List.filter (fun (s,t,_) -> f (s,t)) !db))
+;;
-let is_a_coercion u =
- List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+let is_a_coercion u =
+ List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
+;;
let get_carr uri =
try
- let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+ let src, tgt, _ =
+ List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db
+ in
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
+;;
+let add_coercion (src,tgt,u) =
+ let f s t = eq_carr s src && eq_carr t tgt in
+ let where = List.filter (fun (s,t,_) -> f s t) !db in
+ let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
+ match where with
+ | [] -> db := (src,tgt,[u]) :: !db
+ | (src,tgt,l)::tl ->
+ assert (tl = []); (* not sure, this may be a feature *)
+ db := (src,tgt,u::l)::tl @ rest
+;;
+
val to_list:
unit ->
- (coerc_carr * coerc_carr * UriManager.uri) list
+ (coerc_carr * coerc_carr * UriManager.uri list) list
val add_coercion:
coerc_carr * coerc_carr * UriManager.uri -> unit
open Printf;;
type coercion_search_result =
- | SomeCoercion of Cic.term
+ | SomeCoercion of Cic.term list
| NoCoercion
| NotMetaClosed
| NotHandled of string Lazy.t
(CoercDb.name_of_carr src)
(CoercDb.name_of_carr tgt)));
None
- | [u] ->
+ | _::_ ->
debug_print (lazy (
- sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- Some u
- | u::_ ->
- debug_print (lazy (
- sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ sprintf ":-) TROVATE %d coercion(s) da %s a %s"
(List.length l)
(CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- Some u
+ (CoercDb.name_of_carr tgt)));
+ Some l
in
(match uri with
None -> NoCoercion
- | Some u ->
- let c = CicUtil.term_of_uri u in
- let arity = arity_of c in
- let args = mk_implicits (arity - 1) in
- let newt =
- match args with
- [] -> c
- | _ -> Cic.Appl (c::args)
+ | Some ul ->
+ let cl = List.map CicUtil.term_of_uri ul in
+ let arityl = List.map arity_of cl in
+ let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+ let newtl =
+ List.map2
+ (fun args c ->
+ match args with
+ | [] -> c
+ | _ -> Cic.Appl (c::args))
+ argsl cl
in
- SomeCoercion newt)
+ SomeCoercion newtl)
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
in
let conclusion = " } \n" in
let data = List.fold_left
- (fun acc (src,tgt,c) ->
- acc ^ CoercDb.name_of_carr src ^ " -> " ^
- CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
- "\"];\n") "" l
+ (fun acc (src,tgt,cl) ->
+ List.fold_left
+ (fun acc c ->
+ acc ^ CoercDb.name_of_carr src ^ " -> " ^
+ CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
+ "\"];\n")
+ acc cl)
+ "" l
in
preamble ^ data ^ conclusion
(* This module implements the Query interface to the Coercion Graph *)
type coercion_search_result =
- | SomeCoercion of Cic.term
+ | SomeCoercion of Cic.term list
| NoCoercion
| NotMetaClosed
| NotHandled of string Lazy.t
in
aux ty
in
+ let already_in =
+ List.exists
+ (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (CoercDb.to_list ())
+ in
let ty_src, ty_tgt = extract_last_two_p coer_ty in
let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr 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;
- if
- List.exists
- (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr)
- (CoercDb.to_list ())
- then
- begin
- assert (new_coercions = []);
- []
- end
+ if not add_composites then
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
- begin
- CoercDb.add_coercion (src_carr, tgt_carr, 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 uri obj refinement_toolkit;
- 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 *)
- (*
- prerr_endline ("adding: " ^
- string_of_bool add_composites ^ UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composite_uris;
- *)
- UriManager.UriHashtbl.add coercion_hashtbl uri
- (composite_uris,if add_composites then composite_uris else []);
- lemmas
- end
+ let new_coercions =
+ CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ in
+ let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+ if already_in then
+ (* this if starts here just to be sure the closure function works fine *)
+ begin
+ assert (new_coercions = []);
+ HLog.warn
+ (UriManager.string_of_uri uri ^
+ " is already declared as a coercion! skipping...");
+ []
+ end
+ else
+ begin
+ (* update the DB *)
+ List.iter
+ (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
+ new_coercions;
+ CoercDb.add_coercion (src_carr, tgt_carr, 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 uri obj refinement_toolkit;
+ uri::acc)
+ [] 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 *)
+ (*
+ prerr_endline ("adding: " ^
+ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
+ *)
+ UriManager.UriHashtbl.add coercion_hashtbl uri
+ (composite_uris,if add_composites then composite_uris else []);
+ (*
+ prerr_endline ("lemmas:");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ lemmas;
+ prerr_endline ("lemmas END");*)
+ lemmas
+ end
+;;
let remove_coercion uri =
try
let (composites_in_db, composites_in_lib) =
UriManager.UriHashtbl.find coercion_hashtbl uri
in
- prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+ (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composites_in_db;
+ composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
(* remove from the DB *)
add_single_obj uri obj refinement_toolkit;
let composites =
if coercion then
- add_coercion ~add_composites:true refinement_toolkit uri
+ begin
+ prerr_endline ("composite for " ^ UriManager.string_of_uri uri);
+ let x = add_coercion ~add_composites:true refinement_toolkit uri
+ in
+ prerr_endline ("are: ");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+ prerr_endline "---";
+ x
+ end
else
[]
in
| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None
projects / helm.git / commitdiff