Huge commit with several changes:

[helm.git] / helm / software / components / ng_cic_content / nTermCicContent.ml

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 2022797a2dea9e251b2d0b47dc5e4a6897956d7a..da8061fde197d56c3d482c071d75276ffa74cae1 100644 (file)
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -32,6 +32,8 @@ module Ast = CicNotationPt
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
+type id = string
+
 (*
 type interpretation_id = int
 
@@ -47,15 +49,20 @@ let get_types uri =
       | _ -> assert false
 *)
 
-let idref () =
+let idref register_ref =
  let id = ref 0 in
-  function t ->
+  fun ?reference t ->
    incr id;
-   Ast.AttributedTerm (`IdRef ("i" ^ string_of_int !id), t)
+   let id = "i" ^ string_of_int !id in
+    (match reference with None -> () | Some r -> register_ref id r);
+    Ast.AttributedTerm (`IdRef id, t)
 ;;
 
 (* CODICE c&p da NCicPp *)
-let nast_of_cic0 ~idref ~output_type ~subst k ~context =
+let nast_of_cic0
+ ~(idref:
+    ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+ ~output_type ~subst k ~context =
   function
     | NCic.Rel n ->
        (try 
@@ -64,7 +71,7 @@ let nast_of_cic0 ~idref ~output_type ~subst k ~context =
           idref (Ast.Ident (name,None))
         with Failure "nth" | Invalid_argument "List.nth" -> 
          idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
-    | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s true r, None))
+    | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None))
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ~context (NCicSubstitution.subst_meta lc t)
@@ -236,31 +243,31 @@ let instantiate32 idrefs env symbol args =
   else Ast.Appl (head :: List.map instantiate_arg args)
 
 let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = 
-(*
-  let register_uri id uri = assert false in
-*)
   match (get_compiled32 ()) term with
   | None ->
      nast_of_cic0 ~idref ~output_type ~subst
       (nast_of_cic1 ~idref ~output_type ~subst) ~context term 
   | Some (env, ctors, pid) -> 
       let idrefs =
-(*
-        List.map
-          (fun term ->
-            let idref = idref term in
-            (try
-              register_uri idref
-                (CicUtil.uri_of_term (Deannotate.deannotate_term term))
-            with Invalid_argument _ -> ());
-            idref)
-          ctors
-*) []
+       List.map
+        (fun term ->
+          let attrterm =
+           idref
+            ~reference:
+              (match term with NCic.Const nref -> nref | _ -> assert false)
+           (CicNotationPt.Ident ("dummy",None))
+          in
+           match attrterm with
+              Ast.AttributedTerm (`IdRef id, _) -> id
+            | _ -> assert false
+        ) ctors
       in
       let env =
        List.map
         (fun (name, term) ->
-          name, nast_of_cic1 ~idref ~output_type ~subst ~context term) env
+          name,
+           nast_of_cic1 ~idref ~output_type ~subst ~context term
+        ) env
       in
       let _, symbol, args, _ =
         try
@@ -382,7 +389,11 @@ let instantiate_appl_pattern
 
 let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
  let module K = Content in
- let nast_of_cic = nast_of_cic1 ~idref:(idref ()) ~output_type:`Term ~subst in
+ let ids_to_refs = Hashtbl.create 211 in
+ let register_ref = Hashtbl.add ids_to_refs in
+ let nast_of_cic =
+  nast_of_cic1 ~idref:(idref register_ref) ~output_type:`Term
+   ~subst in
  let context',_ =
   List.fold_right
    (fun item (res,context) ->
@@ -411,6 +422,6 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
              })::res,item::context
    ) context ([],[])
  in
-  "-1",i,context',nast_of_cic ~context ty
+  ("-1",i,context',nast_of_cic ~context ty), ids_to_refs
 ;;