| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
| SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
+ | NotHandled
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let saturate_coercion ul metasenv subst context =
- let cl = List.map CicUtil.term_of_uri ul in
- let funclass_arityl =
- let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
- List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+ let cl =
+ List.map
+ (fun u,saturations ->
+ let t = CicUtil.term_of_uri u in
+ let arity =
+ match CoercDb.is_a_coercion t with
+ | Some (_,CoercDb.Fun i,_,_,_) -> i
+ | _ -> 0
+ in
+ arity,t,saturations) ul
in
let freshmeta = CicMkImplicit.new_meta metasenv subst in
- List.map2
- (fun arity c ->
+ List.map
+ (fun (arity,c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let _,metasenv,args,lastmeta =
- TermUtil.saturate_term freshmeta metasenv context ty arity in
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
- metasenv, Cic.Meta (lastmeta-1,irl),
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
match args with
[] -> c
| _ -> Cic.Appl (c::args)
- ) funclass_arityl cl
+ ) cl
;;
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
+ let is_dead = function CoercDb.Dead -> true | _ -> false in
let pp_l s l =
match l with
| [] ->
debug_print
(lazy
(sprintf ":-( coercion non trovata[%s] da %s a %s" s
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
| _::_ ->
debug_print (lazy (
sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
(List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
in
- try
+ if is_dead src || is_dead tgt then NotHandled
+ else
let l =
CoercDb.find_coercion
(fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
pp_l "approx" l;
(match l with
| [] -> NoCoercion
- | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+ | ul ->
+ SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
| ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
- with
- | CoercDb.EqCarrNotImplemented s -> NotHandled s
- | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
+;;
+
+let rec count_pi c s t =
+ match CicReduction.whd ~delta:false ~subst:s c t with
+ | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+ | _ -> 0
;;
let look_for_coercion metasenv subst context 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' metasenv subst context src_uri tgt_uri
+ let src_arity = count_pi context subst src in
+ let tgt_arity = count_pi context subst tgt in
+ let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+ let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+ look_for_coercion_carr metasenv subst context src_carr tgt_carr
let source_of t =
- try
- let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
+ match CoercDb.is_a_coercion t with
+ | None -> assert false
+ | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
+ | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
+ | Some _ -> assert false (* t must be a coercion not to funclass *)
+;;
let generate_dot_file () =
let module Pp = GraphvizPp.Dot in
~edge_attrs:["fontsize", "10"] fmt;
let l = CoercDb.to_list () in
let pp_description carr =
- match CoercDb.uri_of_carr carr with
- | None -> ()
- | Some uri ->
- Pp.node (CoercDb.name_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ match carr with
+ | CoercDb.Uri uri ->
+ Pp.node (CoercDb.string_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt
+ | _ -> ()
+ in
List.iter
- (fun (src, tgt, cl) ->
- let src_name = CoercDb.name_of_carr src in
- let tgt_name = CoercDb.name_of_carr tgt in
+ (fun (src, tgt, ul) ->
+ let src_name = CoercDb.string_of_carr src in
+ let tgt_name = CoercDb.string_of_carr tgt in
pp_description src;
pp_description tgt;
List.iter
- (fun c ->
+ (fun (u,saturations,_) ->
Pp.edge src_name tgt_name
- ~attrs:[ "label", UriManager.name_of_uri c;
- "href", UriManager.string_of_uri c ]
+ ~attrs:[ "label",
+ (UriManager.name_of_uri u ^
+ if saturations = 0 then
+ ""
+ else
+ "(" ^ string_of_int saturations ^ ")");
+ "href", UriManager.string_of_uri u ]
fmt)
- cl)
+ ul)
l;
Pp.trailer fmt;
Buffer.contents buf
| Cic.Appl (he::_) -> CicUtil.uri_of_term he
| _ -> CicUtil.uri_of_term t
in
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.Constant (_,_, _, _, attrs),_ ->
List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
| _ -> false
let coerced_arg l =
match l with
- | [] | [_] -> assert false
- | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+ | [] | [_] -> None
| c::tl ->
- let arity =
- match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
- in
- (* decide a decent structure for coercion carriers so that all this stuff is
- * useless *)
- let pi =
- (* this calculation is not complete, since we have strange carriers *)
- let rec count_pi = function
- | Cic.Prod(_,_,t) -> 1+ (count_pi t)
- | _ -> 0
- in
- let uri = CicUtil.uri_of_term c in
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- | Cic.Constant (_, _, ty, _, _) -> count_pi ty
- | _ -> assert false
- in
- try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+ match CoercDb.is_a_coercion c with
+ | None -> None
+ | Some (_,_,_,_,cpos) ->
+ if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
;;
(************************* meet calculation stuff ********************)
let eq_uri_opt u1 u2 =
match u1,u2 with
- | Some u1, Some u2 -> UriManager.eq u1 u2
+ | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
| None,Some _ | Some _, None -> false
| None, None -> true
;;
let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
-let splat e l = List.map (fun x -> e, Some x) l;;
+let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_to carr =
| [] -> acc
;;
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
let saturate metasenv uo =
match uo with
| None -> metasenv, None
in
List.map
(fun (c,uo1,uo2) ->
- let metasenv, uo1 = saturate metasenv uo1 in
- let metasenv, uo2 = saturate metasenv uo2 in
+ let metasenv, uo1 =
+ if grow_left then saturate metasenv uo1 else metasenv, None in
+ let metasenv, uo2 =
+ if grow_right then saturate metasenv uo2 else metasenv, None in
c,metasenv, uo1, uo2)
(min [] (intersect (grow left) (grow right)))
;;
projects / helm.git / blobdiff