+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 =
+ 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 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,ugraph) -> MatitaSync.add_obj uri o status)
+ status new_coercions in
+ {status with proof_status = No_proof}
+
+let generate_elimination_principles uri status =
+ let elim sort status =
+ try
+ let uri,obj = CicElim.elim_of ~sort uri 0 in
+ MatitaSync.add_obj uri obj status
+ with CicElim.Can_t_eliminate -> status
+ in
+ List.fold_left (fun status sort -> elim sort status) status
+ [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
+
+let generate_projections uri fields status =
+ let projections = CicRecord.projections_of uri fields in
+ List.fold_left
+ (fun status (uri, name, bo) ->
+ try
+ let ty, ugraph =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let bo = Unshare.unshare bo in
+ let ty = Unshare.unshare ty in
+ let attrs = [`Class `Projection; `Generated] in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ MatitaSync.add_obj uri obj status
+ with
+ CicTypeChecker.TypeCheckerFailure s ->
+ MatitaLog.message
+ ("Unable to create projection " ^ name ^ " cause: " ^ s);
+ status
+ | CicEnvironment.Object_not_found uri ->
+ let depend = UriManager.name_of_uri uri in
+ MatitaLog.message
+ ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
+ status
+ ) status projections
+