matita/components/ng_cic_content/nTermCicContent.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *)
  27
  28 open Printf
  29
  30 module Ast = CicNotationPt
  31
  32 let debug = false
  33 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  34
  35 type id = string
  36
  37 let hide_coercions = ref true;;
  38
  39 (*
  40 type interpretation_id = int
  41
  42 type term_info =
  43   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
  44     uri: (Cic.id, UriManager.uri) Hashtbl.t;
  45   }
  46
  47 let get_types uri =
  48   let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
  49     match o with
  50       | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno
  51       | _ -> assert false
  52 *)
  53
  54 let idref register_ref =
  55  let id = ref 0 in
  56   fun ?reference t ->
  57    incr id;
  58    let id = "i" ^ string_of_int !id in
  59     (match reference with None -> () | Some r -> register_ref id r);
  60     Ast.AttributedTerm (`IdRef id, t)
  61 ;;
  62
  63 let level_of_uri u =
  64   let name = NUri.name_of_uri u in
  65   assert(String.length name > String.length "Type");
  66   String.sub name 4 (String.length name - 4)
  67 ;;
  68
  69 let destroy_nat =
  70   let is_nat_URI = NUri.eq (NUri.uri_of_string
  71   "cic:/matita/ng/arithmetics/nat/nat.ind") in
  72   let is_zero = function
  73     | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when
  74        is_nat_URI uri -> true
  75     | _ -> false
  76   in
  77   let is_succ = function
  78     | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when
  79        is_nat_URI uri -> true
  80     | _ -> false
  81   in
  82   let rec aux acc = function
  83     | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl
  84     | t when is_zero t -> Some acc
  85     | _ -> None
  86   in
  87    aux 0
  88
  89 (* CODICE c&p da NCicPp *)
  90 let nast_of_cic0 status
  91  ~(idref:
  92     ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
  93  ~output_type ~metasenv ~subst k ~context =
  94   function
  95     | NCic.Rel n ->
  96        (try
  97          let name,_ = List.nth context (n-1) in
  98          let name = if name = "_" then "__"^string_of_int n else name in
  99           idref (Ast.Ident (name,None))
 100         with Failure "nth" | Invalid_argument "List.nth" ->
 101          idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
 102     | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None))
 103     | NCic.Meta (n,lc) when List.mem_assoc n subst ->
 104         let _,_,t,_ = List.assoc n subst in
 105          k ~context (NCicSubstitution.subst_meta lc t)
 106     | NCic.Meta (n,(s,l)) ->
 107        (* CSC: qua non dovremmo espandere *)
 108        let l = NCicUtils.expand_local_context l in
 109         idref (Ast.Meta
 110          (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l))
 111     | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
 112     | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set)
 113     | NCic.Sort NCic.Type ((`Type,u)::_) ->
 114               idref(Ast.Sort (`NType (level_of_uri u)))
 115     | NCic.Sort NCic.Type ((`CProp,u)::_) ->
 116               idref(Ast.Sort (`NCProp (level_of_uri u)))
 117     | NCic.Sort NCic.Type ((`Succ,u)::_) ->
 118               idref(Ast.Sort (`NType (level_of_uri u ^ "+1")))
 119     | NCic.Implicit `Hole -> idref (Ast.UserInput)
 120     | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
 121     | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
 122     | NCic.Prod (n,s,t) ->
 123         let n = if n.[0] = '_' then "_" else n in
 124         let binder_kind = `Forall in
 125          idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)),
 126           k ~context:((n,NCic.Decl s)::context) t))
 127     | NCic.Lambda (n,s,t) ->
 128         idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
 129          k ~context:((n,NCic.Decl s)::context) t))
 130     | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
 131         idref (Ast.Cast (k ~context ty, k ~context s))
 132     | NCic.LetIn (n,s,ty,t) ->
 133         idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
 134           ty, k ~context:((n,NCic.Decl s)::context) t))
 135     | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
 136        let _,_,t,_ = List.assoc n subst in
 137        let hd = NCicSubstitution.subst_meta lc t in
 138         k ~context
 139          (NCicReduction.head_beta_reduce ~upto:(List.length args)
 140            (match hd with
 141            | NCic.Appl l -> NCic.Appl (l@args)
 142            | _ -> NCic.Appl (hd :: args)))
 143     | NCic.Appl args as t ->
 144        (match destroy_nat t with
 145          | Some n -> idref (Ast.Num (string_of_int n, -1))
 146          | None ->
 147             let args =
 148              if not !hide_coercions then args
 149              else
 150               match
 151                NCicCoercion.match_coercion status ~metasenv ~context ~subst t
 152               with
 153                | None -> args
 154                | Some (_,sats,cpos) ->
 155 (* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di
 156    argomenti da saltare, come prima! *)
 157                   if cpos < List.length args - 1 then
 158                    List.nth args (cpos + 1) ::
 159                     try snd (HExtlib.split_nth (cpos+sats+2) args)
 160                     with Failure _->[]
 161                   else
 162                    args
 163             in
 164              (match args with
 165                  [arg] -> idref (k ~context arg)
 166                | _ -> idref (Ast.Appl (List.map (k ~context) args))))
 167     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
 168         let name = NUri.name_of_uri uri in
 169 (* CSC
 170         let uri_str = UriManager.string_of_uri uri in
 171         let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
 172         let ctor_puri j =
 173           UriManager.uri_of_string
 174             (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
 175         in
 176 *)
 177         let case_indty =
 178          name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in
 179         let constructors, leftno =
 180          let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in
 181          let _,_,_,cl  = List.nth tys n in
 182           cl,leftno
 183         in
 184         let rec eat_branch n ctx ty pat =
 185           match (ty, pat) with
 186           | NCic.Prod (name, s, t), _ when n > 0 ->
 187              eat_branch (pred n) ctx t pat
 188           | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
 189               let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
 190               (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs
 191           | _, _ -> [], k ~context:ctx pat
 192         in
 193         let j = ref 0 in
 194         let patterns =
 195           try
 196             List.map2
 197               (fun (_, name, ty) pat ->
 198                 incr j;
 199                 let name,(capture_variables,rhs) =
 200                  match output_type with
 201                     `Term -> name, eat_branch leftno context ty pat
 202                   | `Pattern -> "_", ([], k ~context pat)
 203                 in
 204                  Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs
 205               ) constructors patterns
 206           with Invalid_argument _ -> assert false
 207         in
 208         let indty =
 209          match output_type with
 210             `Pattern -> None
 211           | `Term -> Some case_indty
 212         in
 213          idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
 214 ;;
 215
 216   (* persistent state *)
 217
 218 (*
 219 let initial_level2_patterns32 () = Hashtbl.create 211
 220 let initial_interpretations () = Hashtbl.create 211
 221
 222 let level2_patterns32 = ref (initial_level2_patterns32 ())
 223 (* symb -> id list ref *)
 224 let interpretations = ref (initial_interpretations ())
 225 *)
 226 let compiled32 = ref None
 227 (*
 228 let pattern32_matrix = ref []
 229 let counter = ref ~-1
 230
 231 let stack = ref []
 232
 233 let push () =
 234  stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
 235  counter := ~-1;
 236  level2_patterns32 := initial_level2_patterns32 ();
 237  interpretations := initial_interpretations ();
 238  compiled32 := None;
 239  pattern32_matrix := []
 240 ;;
 241
 242 let pop () =
 243  match !stack with
 244     [] -> assert false
 245   | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
 246    stack := old;
 247    counter := ocounter;
 248    level2_patterns32 := olevel2_patterns32;
 249    interpretations := ointerpretations;
 250    compiled32 := ocompiled32;
 251    pattern32_matrix := opattern32_matrix
 252 ;;
 253 *)
 254
 255 let get_compiled32 () =
 256   match !compiled32 with
 257   | None -> assert false
 258   | Some f -> Lazy.force f
 259
 260 let set_compiled32 f = compiled32 := Some f
 261
 262 let add_idrefs =
 263   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
 264
 265 let instantiate32 idrefs env symbol args =
 266   let rec instantiate_arg = function
 267     | Ast.IdentArg (n, name) ->
 268         let t =
 269           try List.assoc name env
 270           with Not_found -> prerr_endline ("name not found in env: "^name);
 271                             assert false
 272         in
 273         let rec count_lambda = function
 274           | Ast.AttributedTerm (_, t) -> count_lambda t
 275           | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
 276           | _ -> 0
 277         in
 278         let rec add_lambda t n =
 279           if n > 0 then
 280             let name = CicNotationUtil.fresh_name () in
 281             Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
 282               Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
 283           else
 284             t
 285         in
 286         add_lambda t (n - count_lambda t)
 287   in
 288   let head =
 289     let symbol = Ast.Symbol (symbol, 0) in
 290     add_idrefs idrefs symbol
 291   in
 292   if args = [] then head
 293   else Ast.Appl (head :: List.map instantiate_arg args)
 294
 295 let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
 296   match (get_compiled32 ()) term with
 297   | None ->
 298      nast_of_cic0 status ~idref ~output_type ~metasenv ~subst
 299       (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term
 300   | Some (env, ctors, pid) ->
 301       let idrefs =
 302        List.map
 303         (fun term ->
 304           let attrterm =
 305            idref
 306             ~reference:
 307               (match term with NCic.Const nref -> nref | _ -> assert false)
 308            (CicNotationPt.Ident ("dummy",None))
 309           in
 310            match attrterm with
 311               Ast.AttributedTerm (`IdRef id, _) -> id
 312             | _ -> assert false
 313         ) ctors
 314       in
 315       let env =
 316        List.map
 317         (fun (name, term) ->
 318           name,
 319            nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context
 320             term
 321         ) env
 322       in
 323       let _, symbol, args, _ =
 324         try
 325           Interpretations.find_level2_patterns32 pid
 326         with Not_found -> assert false
 327       in
 328       let ast = instantiate32 idrefs env symbol args in
 329       idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*)
 330 ;;
 331
 332 let load_patterns32 t =
 333  let t =
 334   HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
 335  in
 336   set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
 337 in
 338  Interpretations.add_load_patterns32 load_patterns32;
 339  Interpretations.init ()
 340 ;;
 341
 342 (*
 343 let ast_of_acic ~output_type id_to_sort annterm =
 344   debug_print (lazy ("ast_of_acic <- "
 345     ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
 346   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
 347   let ast = ast_of_acic1 ~output_type term_info annterm in
 348   debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
 349   ast, term_info.uri
 350
 351 let fresh_id =
 352   fun () ->
 353     incr counter;
 354     !counter
 355
 356 let add_interpretation dsc (symbol, args) appl_pattern =
 357   let id = fresh_id () in
 358   Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
 359   pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
 360   load_patterns32 !pattern32_matrix;
 361   (try
 362     let ids = Hashtbl.find !interpretations symbol in
 363     ids := id :: !ids
 364   with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
 365   id
 366
 367 let get_all_interpretations () =
 368   List.map
 369     (function (_, _, id) ->
 370       let (dsc, _, _, _) =
 371         try
 372           Hashtbl.find !level2_patterns32 id
 373         with Not_found -> assert false
 374       in
 375       (id, dsc))
 376     !pattern32_matrix
 377
 378 let get_active_interpretations () =
 379   HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
 380     !pattern32_matrix
 381
 382 let set_active_interpretations ids =
 383   let pattern32_matrix' =
 384     List.map
 385       (function
 386         | (_, ap, id) when List.mem id ids -> (true, ap, id)
 387         | (_, ap, id) -> (false, ap, id))
 388       !pattern32_matrix
 389   in
 390   pattern32_matrix := pattern32_matrix';
 391   load_patterns32 !pattern32_matrix
 392
 393 exception Interpretation_not_found
 394
 395 let lookup_interpretations symbol =
 396   try
 397    HExtlib.list_uniq
 398     (List.sort Pervasives.compare
 399      (List.map
 400       (fun id ->
 401         let (dsc, _, args, appl_pattern) =
 402           try
 403             Hashtbl.find !level2_patterns32 id
 404           with Not_found -> assert false
 405         in
 406         dsc, args, appl_pattern)
 407       !(Hashtbl.find !interpretations symbol)))
 408   with Not_found -> raise Interpretation_not_found
 409
 410 let remove_interpretation id =
 411   (try
 412     let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
 413     let ids = Hashtbl.find !interpretations symbol in
 414     ids := List.filter ((<>) id) !ids;
 415     Hashtbl.remove !level2_patterns32 id;
 416   with Not_found -> raise Interpretation_not_found);
 417   pattern32_matrix :=
 418     List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
 419   load_patterns32 !pattern32_matrix
 420
 421 let _ = load_patterns32 []
 422
 423 let instantiate_appl_pattern
 424   ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
 425 =
 426   let lookup name =
 427     try List.assoc name env
 428     with Not_found ->
 429       prerr_endline (sprintf "Name %s not found" name);
 430       assert false
 431   in
 432   let rec aux = function
 433     | Ast.UriPattern uri -> term_of_uri uri
 434     | Ast.ImplicitPattern -> mk_implicit false
 435     | Ast.VarPattern name -> lookup name
 436     | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
 437   in
 438   aux appl_pattern
 439 *)
 440
 441 let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
 442  let module K = Content in
 443  let nast_of_cic =
 444   nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
 445  let context',_ =
 446   List.fold_right
 447    (fun item (res,context) ->
 448      match item with
 449       | name,NCic.Decl t ->
 450          Some
 451           (* We should call build_decl_item, but we have not computed *)
 452           (* the inner-types ==> we always produce a declaration      *)
 453           (`Declaration
 454             { K.dec_name = (Some name);
 455               K.dec_id = "-1";
 456               K.dec_inductive = false;
 457               K.dec_aref = "-1";
 458               K.dec_type = nast_of_cic ~context t
 459             })::res,item::context
 460       | name,NCic.Def (t,ty) ->
 461          Some
 462           (* We should call build_def_item, but we have not computed *)
 463           (* the inner-types ==> we always produce a declaration     *)
 464           (`Definition
 465              { K.def_name = (Some name);
 466                K.def_id = "-1";
 467                K.def_aref = "-1";
 468                K.def_term = nast_of_cic ~context t;
 469                K.def_type = nast_of_cic ~context ty
 470              })::res,item::context
 471    ) context ([],[])
 472  in
 473   ("-1",i,context',nast_of_cic ~context ty)
 474 ;;
 475
 476 let nmap_sequent status ~metasenv ~subst conjecture =
 477  let module K = Content in
 478  let ids_to_refs = Hashtbl.create 211 in
 479  let register_ref = Hashtbl.add ids_to_refs in
 480   nmap_sequent0 status ~idref:(idref register_ref) ~metasenv ~subst conjecture,
 481   ids_to_refs
 482 ;;
 483
 484 let object_prefix = "obj:";;
 485 let declaration_prefix = "decl:";;
 486 let definition_prefix = "def:";;
 487 let inductive_prefix = "ind:";;
 488 let joint_prefix = "joint:";;
 489
 490 let get_id =
 491  function
 492     Ast.AttributedTerm (`IdRef id, _) -> id
 493   | _ -> assert false
 494 ;;
 495
 496 let gen_id prefix seed =
 497  let res = prefix ^ string_of_int !seed in
 498   incr seed ;
 499   res
 500 ;;
 501
 502 let build_def_item seed context metasenv id n t ty =
 503  let module K = Content in
 504 (*
 505   try
 506    let sort = Hashtbl.find ids_to_inner_sorts id in
 507    if sort = `Prop then
 508        (let p =
 509         (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
 510        in
 511         `Proof p;)
 512    else
 513 *)
 514       `Definition
 515         { K.def_name = Some n;
 516           K.def_id = gen_id definition_prefix seed;
 517           K.def_aref = id;
 518           K.def_term = t;
 519           K.def_type = ty
 520         }
 521 (*
 522   with
 523    Not_found -> assert false
 524 *)
 525
 526 let build_decl_item seed id n s =
 527  let module K = Content in
 528 (*
 529  let sort =
 530    try
 531     Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
 532    with Not_found -> None
 533  in
 534  match sort with
 535  | Some `Prop ->
 536     `Hypothesis
 537       { K.dec_name = name_of n;
 538         K.dec_id = gen_id declaration_prefix seed;
 539         K.dec_inductive = false;
 540         K.dec_aref = id;
 541         K.dec_type = s
 542       }
 543  | _ ->
 544 *)
 545     `Declaration
 546       { K.dec_name = Some n;
 547         K.dec_id = gen_id declaration_prefix seed;
 548         K.dec_inductive = false;
 549         K.dec_aref = id;
 550         K.dec_type = s
 551       }
 552 ;;
 553
 554 let nmap_obj status (uri,_,metasenv,subst,kind) =
 555   let module K = Content in
 556   let ids_to_refs = Hashtbl.create 211 in
 557   let register_ref = Hashtbl.add ids_to_refs in
 558   let idref = idref register_ref in
 559   let nast_of_cic =
 560    nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
 561   let seed = ref 0 in
 562   let conjectures =
 563    match metasenv with
 564       [] -> None
 565     | _ -> (*Some (List.map (map_conjectures seed) metasenv)*)
 566       (*CSC: used to be the previous line, that uses seed *)
 567       Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv)
 568   in
 569 let  build_constructors seed l =
 570       List.map
 571        (fun (_,n,ty) ->
 572            let ty = nast_of_cic ~context:[] ty in
 573            { K.dec_name = Some n;
 574              K.dec_id = gen_id declaration_prefix seed;
 575              K.dec_inductive = false;
 576              K.dec_aref = "";
 577              K.dec_type = ty
 578            }) l
 579 in
 580 let build_inductive b seed =
 581       fun (_,n,ty,cl) ->
 582         let ty = nast_of_cic ~context:[] ty in
 583         `Inductive
 584           { K.inductive_id = gen_id inductive_prefix seed;
 585             K.inductive_name = n;
 586             K.inductive_kind = b;
 587             K.inductive_type = ty;
 588             K.inductive_constructors = build_constructors seed cl
 589            }
 590 in
 591 let build_fixpoint b seed =
 592       fun (_,n,_,ty,t) ->
 593         let t = nast_of_cic ~context:[] t in
 594         let ty = nast_of_cic ~context:[] ty in
 595         `Definition
 596           { K.def_id = gen_id inductive_prefix seed;
 597             K.def_name = Some n;
 598             K.def_aref = "";
 599             K.def_type = ty;
 600             K.def_term = t;
 601            }
 602 in
 603   let res =
 604    match kind with
 605     | NCic.Fixpoint (is_rec, ifl, _) ->
 606          (gen_id object_prefix seed, [], conjectures,
 607             `Joint
 608               { K.joint_id = gen_id joint_prefix seed;
 609                 K.joint_kind =
 610                    if is_rec then
 611                         `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
 612                    else `CoRecursive;
 613                 K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
 614               })
 615     | NCic.Inductive (is_ind, lno, itl, _) ->
 616          (gen_id object_prefix seed, [], conjectures,
 617             `Joint
 618               { K.joint_id = gen_id joint_prefix seed;
 619                 K.joint_kind =
 620                    if is_ind then `Inductive lno else `CoInductive lno;
 621                 K.joint_defs = List.map (build_inductive is_ind seed) itl
 622               })
 623     | NCic.Constant (_,_,Some bo,ty,_) ->
 624        let ty = nast_of_cic ~context:[] ty in
 625        let bo = nast_of_cic ~context:[] bo in
 626         (gen_id object_prefix seed, [], conjectures,
 627           `Def (K.Const,ty,
 628             build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
 629     | NCic.Constant (_,_,None,ty,_) ->
 630        let ty = nast_of_cic ~context:[] ty in
 631          (gen_id object_prefix seed, [], conjectures,
 632            `Decl (K.Const,
 633              (*CSC: ??? get_id ty here used to be the id of the axiom! *)
 634              build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
 635  in
 636   res,ids_to_refs
 637 ;;