-/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-./tlt_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo
-/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma
-./terms_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-./lref_map_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo
+/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+./lref_map_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo
+/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma /home/tassi/helm/matita/coq.moo
+./terms_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+./tlt_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo
+!! TOTAL TIME SPENT IN disambiguate_thing: 0.
+!! TOTAL TIME SPENT IN disambiguate_thing.refine_thing: 0.
+!! TOTAL TIME SPENT IN add_obj: 0.
+!! TOTAL TIME SPENT IN add_obj.index_obj: 0.
+!! TOTAL TIME SPENT IN add_obj.typecheck_obj: 0.
+!! TOTAL TIME SPENT IN alias_diff (conteggiato anche in include): 0.
+!! TOTAL TIME SPENT IN disambiguate_thing.refine_thing: 0.
+!! TOTAL TIME SPENT IN CicRefine: 0.
+!! TOTAL TIME SPENT IN CicRefine.fo_unif: 0.
+!! TOTAL TIME SPENT IN clean_and_fill: 0.
+!! TOTAL TIME SPENT IN mysql: 0.
+!! TOTAL TIME SPENT IN Xml.pp: 0.
(fun (s,t,u) ->
MatitaLog.debug
(UriManager.name_of_uri u ^ ":"
- ^ UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
+ ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
(CoercDb.to_list ()));
addDebugItem "print top-level grammar entries"
CicNotationParser.print_l2_pattern;
in
let ty_src,ty_tgt = extract_last_two_p coer_ty in
let context = [] in
- let src_uri =
- let ty_src = CicReduction.whd context ty_src in
- CicUtil.uri_of_term ty_src
- in
- let tgt_uri =
- let ty_tgt = CicReduction.whd context ty_tgt in
- CicUtil.uri_of_term ty_tgt
- in
+ let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_src) in
+ let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_tgt) in
let new_coercions =
- (* also adds them to the Db *)
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
let status =
List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
elim a.
clear a.left.left.
reflexivity.
-clear H.clear H1.clear a.right.
- exists.exact s.exists.exact s1.reflexivity.
clear H.clear a.left.right.
exists.exact s.reflexivity.
+clear H.clear H1.clear a.right.
+ exists.exact s.exists.exact s1.reflexivity.
qed.
theorem t: 0=0 \to stupidtype.
(\lambda a,b,K. y=a \to O=b \to
match K with [ (k a b p) \Rightarrow a ] = x)
? ? ? H).
+ goal 16.
simplify. intros.
generalize in match H1.
rewrite < H2; rewrite < H3.intro.
(CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
-
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
type_of_aux subst' metasenv'
((Some (name,(C.Decl s')))::context) t ugraph1
in
- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
- in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ (try
+ let sop,subst''',metasenv''',ugraph3 =
+ sort_of_prod subst'' metasenv''
+ context (name,s') (sort1,sort2) ugraph2
+ in
+ C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ with
+ | RefineFailure _ as exn ->
+ (* given [t] of type [type_to_coerce] returns
+ * a term that has type [tgt_sort] eventually
+ * derived from (coercion [t]) *)
+ let refined_target = t' in
+ let sort_of_refined_target = sort2 in
+ let carr t subst context = CicMetaSubst.apply_subst subst t in
+ let coerce_to_sort tgt_sort t type_to_coerce subst ctx =
+ match type_to_coerce with
+ | Cic.Sort _ -> t
+ | term ->
+ let coercion_src = carr type_to_coerce subst ctx in
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let search = CoercGraph.look_for_coercion in
+ (match search coercion_src coercion_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain "Coercions on metas")
+ | CoercGraph.SomeCoercion c -> Cic.Appl [c;t])
+ in
+ (* this is probably not the best... *)
+ let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in
+ let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in
+ let new_src =
+ coerce_to_sort tgt_sort_for_pi_source s sort1 subst context
+ in
+ let context_with_new_src =
+ ((Some (name,(C.Decl new_src)))::context)
+ in
+ let new_tgt =
+ coerce_to_sort
+ tgt_sort_for_pi_target
+ refined_target sort_of_refined_target
+ subst context_with_new_src
+ in
+ let newprod = C.Prod (name,new_src,new_tgt) in
+ let _,sort_of_refined_prod,subst,metasenv,ugraph3 =
+ type_of_aux subst metasenv context newprod ugraph2
+ in
+ (* this if for a coercion on the tail of the arrow *)
+ let new_target =
+ match sort_of_refined_target with
+ | Cic.Sort _ -> refined_target
+ | _ -> new_tgt
+ in
+ C.Prod(name,new_src,new_target),
+ sort_of_refined_prod,subst,metasenv,ugraph3)
| C.Lambda (n,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ (* different than Coq manual!!! *)
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
C.Sort (C.Type t'),subst,metasenv,ugraph2
| (C.Sort _,C.Sort (C.Type t1)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
C.Sort (C.Type t1),subst,metasenv,ugraph
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
| (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
* brake the invariant that refine produce only well typed terms *)
- (* TODO if we check the non meta term and if it is a sort then we are
- * likely to know the exact value of the result e.g. if the rhs is a
- * Sort (Prop | Set | CProp) then the result is the rhs *)
+ (* TODO if we check the non meta term and if it is a sort then we
+ * are likely to know the exact value of the result e.g. if the rhs
+ * is a Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv,ugraph1) =
- fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
+ fo_unif_subst subst context_for_t2 metasenv
+ (C.Meta (idx,[])) t2'' ugraph
in
t2'',subst,metasenv,ugraph1
- | (_,_) ->
- raise (RefineFailure (Reason (sprintf
- "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
- (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
- (CicPp.ppterm t2''))))
+ | _,_ ->
+ raise
+ (RefineFailure
+ (Reason
+ (sprintf
+ ("Two sorts were expected, found %s " ^^
+ "(that reduces to %s) and %s (that reduces to %s)")
+ (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
+ (CicPp.ppterm t2''))))
and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
let rec mk_prod metasenv context =
hete,subst,metasenv,ugraph1
with exn ->
(* we search a coercion from hety to s *)
- let coer = CoercGraph.look_for_coercion
- (CicMetaSubst.apply_subst subst hety)
- (CicMetaSubst.apply_subst subst s)
+ let coer =
+ let carr t subst context =
+ CicMetaSubst.apply_subst subst t
+ in
+ let c_hety = carr hety subst context in
+ let c_s = carr s subst context in
+ CoercGraph.look_for_coercion c_hety c_s
in
match coer with
- | None -> raise exn
- | Some c ->
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain "Coercions on meta")
+ | CoercGraph.SomeCoercion c ->
(Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
in
let coerced_args,metasenv',subst',t',ugraph2 =
* http://helm.cs.unibo.it/
*)
+type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+exception EqCarrNotImplemented of string
+exception EqCarrOnNonMetaClosed
+
let db = ref []
let use_coercions = ref true
+let coerc_carr_of_term t =
+ try
+ Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+ match t with
+ | Cic.Sort s -> Sort s
+ | t -> Term t
+;;
+
+let eq_carr src tgt =
+ match src, tgt with
+ | Uri src, Uri tgt -> UriManager.eq src tgt
+ | Sort (Cic.Type _), Sort (Cic.Type _) -> true
+ | Sort src, Sort tgt when src = tgt -> true
+ | Term t1, Term t2 when
+ CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 ->
+ raise
+ (EqCarrNotImplemented
+ ("Unsupported carr for coercions: " ^
+ CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))
+ | _ -> raise EqCarrOnNonMetaClosed
+
+let name_of_carr = function
+ | Uri u -> UriManager.name_of_uri u
+ | Sort s -> CicPp.ppsort s
+ | Term _ -> assert false
+
+
let to_list () =
!db
*)
(** XXX WARNING: non-reentrant *)
+type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+exception EqCarrNotImplemented of string
+exception EqCarrOnNonMetaClosed
+val eq_carr: coerc_carr -> coerc_carr -> bool
+val coerc_carr_of_term: Cic.term -> coerc_carr
+val name_of_carr: coerc_carr -> string
val use_coercions: bool ref (** initial status is true *)
val to_list:
unit ->
- (UriManager.uri * UriManager.uri * UriManager.uri) list
+ (coerc_carr * coerc_carr * UriManager.uri) list
val add_coercion:
- UriManager.uri * UriManager.uri * UriManager.uri -> unit
+ coerc_carr * coerc_carr * UriManager.uri -> unit
val remove_coercion:
- (UriManager.uri * UriManager.uri * UriManager.uri -> bool) -> unit
+ (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
val find_coercion:
- (UriManager.uri * UriManager.uri -> bool) -> UriManager.uri list
+ (coerc_carr * coerc_carr -> bool) -> UriManager.uri list
open Printf;;
+type coercion_search_result =
+ | SomeCoercion of Cic.term
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string
+
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 src = CicUtil.uri_of_term src in
- let tgt = CicUtil.uri_of_term tgt in
- let l =
- CoercDb.find_coercion
- (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt)
- in
- match l with
- | [] -> debug_print (lazy ":( coercion non trovata"); None
- | u::_ ->
- debug_print (lazy (
- sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
- (List.length l)
- (UriManager.name_of_uri src)
- (UriManager.name_of_uri tgt)
- (UriManager.name_of_uri u)));
- Some (CicUtil.term_of_uri u)
- with Invalid_argument s ->
- debug_print (lazy (":( coercion non trovata (fallita la uri_of_term): " ^ s));
- None
+ try
+ let l =
+ CoercDb.find_coercion
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ in
+ match l with
+ | [] -> debug_print (lazy ":( coercion non trovata"); NoCoercion
+ | u::_ ->
+ debug_print (lazy (
+ sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ SomeCoercion (CicUtil.term_of_uri u)
+ with
+ | CoercDb.EqCarrNotImplemented s -> NotHandled s
+ | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
;;
+let look_for_coercion src tgt =
+ let src_uri = CoercDb.coerc_carr_of_term src in
+ 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 c_from_tgt = List.filter (fun (f,_,_) -> UriManager.eq f tgt) coercions in
- let c_to_src = List.filter (fun (_,t,_) -> UriManager.eq 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)
+ match src,tgt with
+ | CoercDb.Uri _, CoercDb.Uri _ ->
+ let c_from_tgt =
+ List.filter (fun (f,_,_) -> CoercDb.eq_carr f tgt) coercions
+ in
+ let c_to_src =
+ List.filter (fun (_,t,_) -> CoercDb.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]
List.filter (
fun (src,_,tgt) ->
not (List.exists (fun (s,t,u) ->
- UriManager.eq s src &&
- UriManager.eq t tgt)
+ 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 _ -> assert false
+ | CoercDb.Term _ -> assert false
+
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
match l with
| [] -> assert false
| he :: tl ->
- let term_of_uri' uri = CicUtil.term_of_uri uri in
let first_step =
- Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
- obj_attrs)
+ Cic.Constant ("",
+ Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
in
let o,u =
- List.fold_left (fun (o,u) coer ->
+ List.fold_left (fun (o,univ) coer ->
match o with
| Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (term_of_uri' coer) u
+ generate_composite_closure c (term_of_carr (CoercDb.Uri
+ coer)) univ
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl
in
- let name_src = UriManager.name_of_uri src in
- let name_tgt = UriManager.name_of_uri tgt 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 =
* http://cs.unibo.it/helm/.
*)
+type coercion_search_result =
+ | SomeCoercion of Cic.term
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string
+
val look_for_coercion :
- Cic.term -> Cic.term -> Cic.term option
+ Cic.term -> Cic.term -> coercion_search_result
(* also adds them to the Db *)
val close_coercion_graph:
- UriManager.uri -> UriManager.uri -> UriManager.uri ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
(UriManager.uri * Cic.obj * CicUniv.universe_graph) list
projects / helm.git / commitdiff