From 18d9e31c73e22d03371d33b7b0a56418abf9b156 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Nov 2005 14:43:32 +0000
Subject: [PATCH] moved coercions away (work in progress)

---
 helm/matita/matitaEngine.ml | 72 +++++--------------------------------
 helm/matita/matitaSync.ml   | 13 ++++++-
 helm/matita/matitaSync.mli  |  4 +++
 3 files changed, 24 insertions(+), 65 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 8f417485a..fc8e19621 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -571,67 +571,10 @@ let eval_tactical status tac =
   in
   status
 
-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 }
+let eval_coercion status ~add_composites coercion =
+ let uri = CicUtil.uri_of_term coercion in
+ let status = MatitaSync.add_coercion status ~add_composites uri in
+  {status with proof_status = No_proof}
 
 (* to avoid a long list of recursive functions *)
 let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
@@ -674,10 +617,10 @@ let disambiguate_command status =
   | GrafiteAst.Render _
   | GrafiteAst.Set _ as cmd ->
       status,cmd
-  | GrafiteAst.Coercion (loc, term) ->
+  | GrafiteAst.Coercion (loc, term, add_composites) ->
       let status_ref = ref status in
       let term = disambiguate_term ~context:[] status_ref ~-1 term in
-      !status_ref, GrafiteAst.Coercion (loc,term)
+      !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
   | GrafiteAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
       status, GrafiteAst.Obj (loc,obj)
@@ -757,7 +700,8 @@ let eval_command opts status cmd =
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj {status with proof_status = No_proof}
-  | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion
+  | GrafiteAst.Coercion (loc, coercion, add_composites) ->
+     eval_coercion status ~add_composites coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
       (*CSC: Warning: this code should be factorized with the corresponding
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 66e3528bf..b06aedf30 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -124,7 +124,18 @@ let add_obj uri obj status =
 let add_obj =
  let profiler = HExtlib.profile "add_obj" in
   fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
-   
+
+let add_coercion status ~add_composites uri =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in
+ let status = {status with coercions = uri :: status.coercions} in
+ let statement_of name =
+   GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
+     (CicNotationPt.Ident (name, None)), false) in
+ let moo_content = [statement_of (UriManager.name_of_uri uri)] in
+ let status = MatitaTypes.add_moo_content moo_content status in
+  List.fold_left add_alias_for_constant status lemmas
+ 
 module OrderedUri =
 struct
   type t = UriManager.uri * string
diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index 1a2d8445c..13023a854 100644
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -27,6 +27,10 @@ val add_obj:
   UriManager.uri -> Cic.obj -> 
     MatitaTypes.status -> MatitaTypes.status
 
+val add_coercion:
+ MatitaTypes.status -> add_composites:bool -> UriManager.uri ->
+  MatitaTypes.status
+
 val time_travel: 
   present:MatitaTypes.status -> past:MatitaTypes.status -> unit
 
-- 
2.39.2