Semantic selection back again (but no semantic cut&paste yet).

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 826238d1c0b7b85b79a8e72dd53a55124dd6049a..be731ba924fa9c1a2df699b0973568a1d11018de 100644 (file)
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -35,8 +35,6 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 (*
 type interpretation_id = int
 
-let idref id t = Ast.AttributedTerm (`IdRef id, t)
-
 type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, UriManager.uri) Hashtbl.t;
@@ -49,27 +47,34 @@ let get_types uri =
       | _ -> assert false
 *)
 
+let idref () =
+ let id = ref 0 in
+  function t ->
+   incr id;
+   Ast.AttributedTerm (`IdRef ("i" ^ string_of_int !id), t)
+;;
+
 (* CODICE c&p da NCicPp *)
-let nast_of_cic ~output_type ~subst ~context =
+let nast_of_cic ~idref ~output_type ~subst ~context =
   let rec k ctx = function
     | NCic.Rel n ->
        (try 
          let name,_ = List.nth ctx (n-1) in
          let name = if name = "_" then "__"^string_of_int n else name in
-          Ast.Ident (name,None)
+          idref (Ast.Ident (name,None))
         with Failure "nth" | Invalid_argument "List.nth" -> 
-          Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None))
-    | NCic.Const r -> Ast.Ident (NCicPp.r2s false r, None)
+          idref (Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None)))
+    | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s false r, None))
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ctx (NCicSubstitution.subst_meta lc t)
     | NCic.Meta (n,(s,l)) ->
        (* CSC: qua non dovremmo espandere *)
        let l = NCicUtils.expand_local_context l in
-        Ast.Meta
-         (n, List.map (fun x -> Some (k ctx (NCicSubstitution.lift s x))) l)
-    | NCic.Sort NCic.Prop -> Ast.Sort `Prop
-    | NCic.Sort NCic.Type _ -> Ast.Sort `Set
+        idref (Ast.Meta
+         (n, List.map (fun x -> Some (k ctx (NCicSubstitution.lift s x))) l))
+    | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
+    | NCic.Sort NCic.Type _ -> idref (Ast.Sort `Set)
     (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0"
     | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
     | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
@@ -80,18 +85,18 @@ let nast_of_cic ~output_type ~subst ~context =
         (List.tl l);
        F.fprintf f ")"*)
     (* CSC: qua siamo grezzi *)
-    | NCic.Implicit `Hole -> Ast.UserInput
-    | NCic.Implicit _ -> Ast.Implicit
+    | NCic.Implicit `Hole -> idref (Ast.UserInput)
+    | NCic.Implicit _ -> idref (Ast.Implicit)
     | NCic.Prod (n,s,t) ->
         let binder_kind = `Forall in
-         Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)),
-          k ((n,NCic.Decl s)::ctx) t)
+         idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)),
+          k ((n,NCic.Decl s)::ctx) t))
     | NCic.Lambda (n,s,t) ->
-        Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ctx s)),
-         k ((n,NCic.Decl s)::ctx) t)
+        idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ctx s)),
+         k ((n,NCic.Decl s)::ctx) t))
     | NCic.LetIn (n,s,ty,t) ->
-        Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s,
-         k ((n,NCic.Decl s)::ctx) t)
+        idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s,
+         k ((n,NCic.Decl s)::ctx) t))
     | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> 
        let _,_,t,_ = List.assoc n subst in
        let hd = NCicSubstitution.subst_meta lc t in
@@ -100,7 +105,7 @@ let nast_of_cic ~output_type ~subst ~context =
            (match hd with
            | NCic.Appl l -> NCic.Appl (l@args)
            | _ -> NCic.Appl (hd :: args)))
-    | NCic.Appl args -> Ast.Appl (List.map (k ctx) args)
+    | NCic.Appl args -> idref (Ast.Appl (List.map (k ctx) args))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
         let name = NUri.name_of_uri uri in
 (* CSC
@@ -147,13 +152,14 @@ let nast_of_cic ~output_type ~subst ~context =
             `Pattern -> None
           | `Term -> Some case_indty
         in
-         Ast.Case (k ctx te, indty, Some (k ctx outty), patterns)
+         idref (Ast.Case (k ctx te, indty, Some (k ctx outty), patterns))
   in
    k context
 ;;
 
 let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
  let module K = Content in
+ let nast_of_cic = nast_of_cic ~idref:(idref ()) ~output_type:`Term ~subst in
  let context',_ =
   List.fold_right
    (fun item (res,context) ->
@@ -167,7 +173,7 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
               K.dec_id = "-1"; 
               K.dec_inductive = false;
               K.dec_aref = "-1";
-              K.dec_type = nast_of_cic ~output_type:`Term ~subst ~context t
+              K.dec_type = nast_of_cic ~context t
             })::res,item::context
       | name,NCic.Def (t,ty) ->
          Some
@@ -177,12 +183,12 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
              { K.def_name = (Some name);
                K.def_id = "-1"; 
                K.def_aref = "-1";
-               K.def_term = nast_of_cic ~output_type:`Term ~subst ~context t;
-               K.def_type = nast_of_cic ~output_type:`Term ~subst ~context ty
+               K.def_term = nast_of_cic ~context t;
+               K.def_type = nast_of_cic ~context ty
              })::res,item::context
    ) context ([],[])
  in
-  "-1",i,context',nast_of_cic ~output_type:`Term ~subst ~context ty
+  "-1",i,context',nast_of_cic ~context ty
 ;;
 
 (*