-let eval_coercion status coercion =
- let coer_uri,coer_ty =
- match coercion with
- | Cic.Const (uri,_)
- | Cic.Var (uri,_) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- (match o with
- | Cic.Constant (_,_,ty,_,_)
- | Cic.Variable (_,_,ty,_,_) ->
- uri,ty
- | _ -> assert false)
- | Cic.MutConstruct (uri,t,c,_) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- (match o with
- | Cic.InductiveDefinition (l,_,_,_) ->
- let (_,_,_,cl) = List.nth l t in
- let (_,cty) = List.nth cl c in
- uri,cty
- | _ -> assert false)
- | _ -> assert false
- 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 context = [] 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 =
- CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
- let status =
- List.fold_left (fun s (uri,o,_) ->
- let status = MatitaSync.add_obj uri o status in
- {status with coercions = uri :: status.coercions})
- status new_coercions in
- let status = {status with coercions = coer_uri :: status.coercions} in
- let statement_of name =
- GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
- (CicNotationPt.Ident (name, None)))
- in
- let moo_content =
- statement_of (UriManager.name_of_uri coer_uri) ::
- (List.map
- (fun (uri, _, _) ->
- statement_of (UriManager.name_of_uri uri))
- new_coercions)
- in
- let status = add_moo_content moo_content status in
- { status with proof_status = No_proof }