helm/software/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 (*
  38 type interpretation_id = int
  39
  40 type term_info =
  41   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
  42     uri: (Cic.id, UriManager.uri) Hashtbl.t;
  43   }
  44
  45 let get_types uri =
  46   let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
  47     match o with
  48       | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno
  49       | _ -> assert false
  50 *)
  51
  52 let freshid register_ref register_father_id =
  53  let id = ref 0 in
  54   fun ?reference father_id ->
  55    incr id;
  56    let id = "i" ^ string_of_int !id in
  57     (match reference with None -> () | Some r -> register_ref id r);
  58     register_father_id id father_id;
  59     Some id, fun t -> Ast.AttributedTerm (`IdRef id, t)
  60 ;;
  61
  62 (* CODICE c&p da NCicPp *)
  63 let nast_of_cic0
  64  ~(freshid:
  65     ?reference:NReference.reference -> id option ->
  66       id option * (CicNotationPt.term -> CicNotationPt.term))
  67  ~output_type ~subst k ~context father_id =
  68   function
  69     | NCic.Rel n ->
  70        let id, idref = freshid father_id in
  71         (try
  72           let name,_ = List.nth context (n-1) in
  73           let name = if name = "_" then "__"^string_of_int n else name in
  74            idref (Ast.Ident (name,None))
  75          with Failure "nth" | Invalid_argument "List.nth" ->
  76           idref (Ast.Ident ("-"^ string_of_int (n - List.length context),None)))
  77     | NCic.Const r ->
  78        let id, idref = freshid ~reference:r father_id in
  79         idref (Ast.Ident (NCicPp.r2s true r, None))
  80     | NCic.Meta (n,lc) when List.mem_assoc n subst ->
  81         let _,_,t,_ = List.assoc n subst in
  82          k ~context father_id (NCicSubstitution.subst_meta lc t)
  83     | NCic.Meta (n,(s,l)) ->
  84        let id, idref = freshid father_id in
  85        (* CSC: qua non dovremmo espandere *)
  86        let l = NCicUtils.expand_local_context l in
  87         idref (Ast.Meta
  88          (n,
  89            List.map (fun x->Some(k ~context id (NCicSubstitution.lift s x))) l))
  90     | NCic.Sort NCic.Prop ->
  91        let id, idref = freshid father_id in
  92         idref (Ast.Sort `Prop)
  93     | NCic.Sort NCic.Type _ ->
  94        let id, idref = freshid father_id in
  95         idref (Ast.Sort `Set)
  96     (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0"
  97     | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
  98     | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
  99     | C.Sort (C.Type l) ->
 100        F.fprintf f "Max(";
 101        aux ctx (C.Sort (C.Type [List.hd l]));
 102        List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
 103         (List.tl l);
 104        F.fprintf f ")"*)
 105     (* CSC: qua siamo grezzi *)
 106     | NCic.Implicit `Hole ->
 107        let id, idref = freshid father_id in
 108         idref (Ast.UserInput)
 109     | NCic.Implicit _ ->
 110        let id, idref = freshid father_id in
 111         idref (Ast.Implicit)
 112     | NCic.Prod (n,s,t) ->
 113        let id, idref = freshid father_id in
 114        let n = if n.[0] = '_' then "_" else n in
 115        let binder_kind = `Forall in
 116         idref
 117          (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context id s)),
 118          k ~context:((n,NCic.Decl s)::context) id t))
 119     | NCic.Lambda (n,s,t) ->
 120        let id, idref = freshid father_id in
 121         idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context id s)),
 122          k ~context:((n,NCic.Decl s)::context) id t))
 123     | NCic.LetIn (n,s,ty,t) ->
 124        let id, idref = freshid father_id in
 125         idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context id ty)),
 126          k ~context id s, k ~context:((n,NCic.Decl s)::context) id t))
 127     | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
 128        let _,_,t,_ = List.assoc n subst in
 129        let hd = NCicSubstitution.subst_meta lc t in
 130         k ~context father_id
 131          (NCicReduction.head_beta_reduce ~upto:(List.length args)
 132            (match hd with
 133            | NCic.Appl l -> NCic.Appl (l@args)
 134            | _ -> NCic.Appl (hd :: args)))
 135     | NCic.Appl args ->
 136        let id, idref = freshid father_id in
 137         idref (Ast.Appl (List.map (k ~context id) args))
 138     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
 139        let id, idref = freshid father_id in
 140         let name = NUri.name_of_uri uri in
 141 (* CSC
 142         let uri_str = UriManager.string_of_uri uri in
 143         let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
 144         let ctor_puri j =
 145           UriManager.uri_of_string
 146             (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
 147         in
 148 *)
 149         let case_indty =
 150          name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in
 151         let constructors, leftno =
 152          let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in
 153          let _,_,_,cl  = List.nth tys n in
 154           cl,leftno
 155         in
 156         let rec eat_branch n ctx ty pat =
 157           match (ty, pat) with
 158           | NCic.Prod (name, s, t), _ when n > 0 ->
 159              eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat
 160           | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
 161               let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
 162               (Ast.Ident (name,None), Some (k ~context id s)) :: cv, rhs
 163           | _, _ -> [], k ~context id pat
 164         in
 165         let j = ref 0 in
 166         let patterns =
 167           try
 168             List.map2
 169               (fun (_, name, ty) pat ->
 170                 incr j;
 171                 let name,(capture_variables,rhs) =
 172                  match output_type with
 173                     `Term -> name, eat_branch leftno context ty pat
 174                   | `Pattern -> "_", ([], k ~context id pat)
 175                 in
 176                  Ast.Pattern
 177                   (name, None(*CSC Some (ctor_puri !j)*), capture_variables),rhs
 178               ) constructors patterns
 179           with Invalid_argument _ -> assert false
 180         in
 181         let indty =
 182          match output_type with
 183             `Pattern -> None
 184           | `Term -> Some case_indty
 185         in
 186          idref
 187           (Ast.Case
 188            (k ~context id te, indty, Some (k ~context id outty), patterns))
 189 ;;
 190
 191   (* persistent state *)
 192
 193 (*
 194 let initial_level2_patterns32 () = Hashtbl.create 211
 195 let initial_interpretations () = Hashtbl.create 211
 196
 197 let level2_patterns32 = ref (initial_level2_patterns32 ())
 198 (* symb -> id list ref *)
 199 let interpretations = ref (initial_interpretations ())
 200 *)
 201 let compiled32 = ref None
 202 (*
 203 let pattern32_matrix = ref []
 204 let counter = ref ~-1
 205
 206 let stack = ref []
 207
 208 let push () =
 209  stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
 210  counter := ~-1;
 211  level2_patterns32 := initial_level2_patterns32 ();
 212  interpretations := initial_interpretations ();
 213  compiled32 := None;
 214  pattern32_matrix := []
 215 ;;
 216
 217 let pop () =
 218  match !stack with
 219     [] -> assert false
 220   | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
 221    stack := old;
 222    counter := ocounter;
 223    level2_patterns32 := olevel2_patterns32;
 224    interpretations := ointerpretations;
 225    compiled32 := ocompiled32;
 226    pattern32_matrix := opattern32_matrix
 227 ;;
 228 *)
 229
 230 let get_compiled32 () =
 231   match !compiled32 with
 232   | None -> assert false
 233   | Some f -> Lazy.force f
 234
 235 let set_compiled32 f = compiled32 := Some f
 236
 237 let add_idrefs =
 238   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
 239
 240 let instantiate32 idrefs env symbol args =
 241   let rec instantiate_arg = function
 242     | Ast.IdentArg (n, name) ->
 243         let t =
 244           try List.assoc name env
 245           with Not_found -> prerr_endline ("name not found in env: "^name);
 246                             assert false
 247         in
 248         let rec count_lambda = function
 249           | Ast.AttributedTerm (_, t) -> count_lambda t
 250           | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
 251           | _ -> 0
 252         in
 253         let rec add_lambda t n =
 254           if n > 0 then
 255             let name = CicNotationUtil.fresh_name () in
 256             Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
 257               Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
 258           else
 259             t
 260         in
 261         add_lambda t (n - count_lambda t)
 262   in
 263   let head =
 264     let symbol = Ast.Symbol (symbol, 0) in
 265     add_idrefs idrefs symbol
 266   in
 267   if args = [] then head
 268   else Ast.Appl (head :: List.map instantiate_arg args)
 269
 270 let rec nast_of_cic1 ~freshid ~output_type ~subst ~context father_id term =
 271   match (get_compiled32 ()) term with
 272   | None ->
 273      nast_of_cic0 ~freshid ~output_type ~subst
 274       (nast_of_cic1 ~freshid ~output_type ~subst) ~context father_id term
 275   | Some (env, ctors, pid) ->
 276      let id, idref = freshid father_id in
 277      let idrefs =
 278       List.map
 279        (fun term ->
 280          let id, _ =
 281           freshid
 282            ~reference:
 283              (match term with NCic.Const nref -> nref | _ -> assert false)
 284            father_id
 285          in
 286           match id with Some id -> id | None -> assert false
 287        ) ctors in
 288      let env =
 289       List.map
 290        (fun (name, term) ->
 291          name,nast_of_cic1 ~freshid ~output_type ~subst ~context id term
 292        ) env in
 293      let _, symbol, args, _ =
 294       try
 295        TermAcicContent.find_level2_patterns32 pid
 296       with Not_found -> assert false in
 297      let ast = instantiate32 idrefs env symbol args in
 298       idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*)
 299 ;;
 300
 301 let load_patterns32 t =
 302  let t =
 303   HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
 304  in
 305   set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
 306 in
 307  TermAcicContent.add_load_patterns32 load_patterns32;
 308  TermAcicContent.init ()
 309 ;;
 310
 311 (*
 312 let ast_of_acic ~output_type id_to_sort annterm =
 313   debug_print (lazy ("ast_of_acic <- "
 314     ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
 315   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
 316   let ast = ast_of_acic1 ~output_type term_info annterm in
 317   debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
 318   ast, term_info.uri
 319
 320 let fresh_id =
 321   fun () ->
 322     incr counter;
 323     !counter
 324
 325 let add_interpretation dsc (symbol, args) appl_pattern =
 326   let id = fresh_id () in
 327   Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
 328   pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
 329   load_patterns32 !pattern32_matrix;
 330   (try
 331     let ids = Hashtbl.find !interpretations symbol in
 332     ids := id :: !ids
 333   with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
 334   id
 335
 336 let get_all_interpretations () =
 337   List.map
 338     (function (_, _, id) ->
 339       let (dsc, _, _, _) =
 340         try
 341           Hashtbl.find !level2_patterns32 id
 342         with Not_found -> assert false
 343       in
 344       (id, dsc))
 345     !pattern32_matrix
 346
 347 let get_active_interpretations () =
 348   HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
 349     !pattern32_matrix
 350
 351 let set_active_interpretations ids =
 352   let pattern32_matrix' =
 353     List.map
 354       (function
 355         | (_, ap, id) when List.mem id ids -> (true, ap, id)
 356         | (_, ap, id) -> (false, ap, id))
 357       !pattern32_matrix
 358   in
 359   pattern32_matrix := pattern32_matrix';
 360   load_patterns32 !pattern32_matrix
 361
 362 exception Interpretation_not_found
 363
 364 let lookup_interpretations symbol =
 365   try
 366    HExtlib.list_uniq
 367     (List.sort Pervasives.compare
 368      (List.map
 369       (fun id ->
 370         let (dsc, _, args, appl_pattern) =
 371           try
 372             Hashtbl.find !level2_patterns32 id
 373           with Not_found -> assert false
 374         in
 375         dsc, args, appl_pattern)
 376       !(Hashtbl.find !interpretations symbol)))
 377   with Not_found -> raise Interpretation_not_found
 378
 379 let remove_interpretation id =
 380   (try
 381     let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
 382     let ids = Hashtbl.find !interpretations symbol in
 383     ids := List.filter ((<>) id) !ids;
 384     Hashtbl.remove !level2_patterns32 id;
 385   with Not_found -> raise Interpretation_not_found);
 386   pattern32_matrix :=
 387     List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
 388   load_patterns32 !pattern32_matrix
 389
 390 let _ = load_patterns32 []
 391
 392 let instantiate_appl_pattern
 393   ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
 394 =
 395   let lookup name =
 396     try List.assoc name env
 397     with Not_found ->
 398       prerr_endline (sprintf "Name %s not found" name);
 399       assert false
 400   in
 401   let rec aux = function
 402     | Ast.UriPattern uri -> term_of_uri uri
 403     | Ast.ImplicitPattern -> mk_implicit false
 404     | Ast.VarPattern name -> lookup name
 405     | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
 406   in
 407   aux appl_pattern
 408 *)
 409
 410 let nmap_sequent0 ~freshid ~subst (i,(n,context,ty):int * NCic.conjecture) =
 411  let module K = Content in
 412  let nast_of_cic ~context =
 413   nast_of_cic1 ~freshid ~output_type:`Term ~subst ~context None in
 414  let context',_ =
 415   List.fold_right
 416    (fun item (res,context) ->
 417      match item with
 418       | name,NCic.Decl t ->
 419          Some
 420           (* We should call build_decl_item, but we have not computed *)
 421           (* the inner-types ==> we always produce a declaration      *)
 422           (`Declaration
 423             { K.dec_name = (Some name);
 424               K.dec_id = "-1";
 425               K.dec_inductive = false;
 426               K.dec_aref = "-1";
 427               K.dec_type = nast_of_cic ~context t
 428             })::res,item::context
 429       | name,NCic.Def (t,ty) ->
 430          Some
 431           (* We should call build_def_item, but we have not computed *)
 432           (* the inner-types ==> we always produce a declaration     *)
 433           (`Definition
 434              { K.def_name = (Some name);
 435                K.def_id = "-1";
 436                K.def_aref = "-1";
 437                K.def_term = nast_of_cic ~context t;
 438                K.def_type = nast_of_cic ~context ty
 439              })::res,item::context
 440    ) context ([],[])
 441  in
 442   ("-1",i,context',nast_of_cic ~context ty)
 443 ;;
 444
 445 let nmap_sequent ~subst metasenv =
 446  let module K = Content in
 447  let ids_to_refs = Hashtbl.create 503 in
 448  let ids_to_father_ids = Hashtbl.create 503 in
 449  let register_ref = Hashtbl.add ids_to_refs in
 450  let register_father_id = Hashtbl.add ids_to_father_ids in
 451   nmap_sequent0 ~freshid:(freshid register_ref register_father_id) ~subst
 452    metasenv,ids_to_refs,ids_to_father_ids
 453 ;;
 454
 455 let object_prefix = "obj:";;
 456 let declaration_prefix = "decl:";;
 457 let definition_prefix = "def:";;
 458
 459 let get_id =
 460  function
 461     Ast.AttributedTerm (`IdRef id, _) -> id
 462   | _ -> assert false
 463 ;;
 464
 465 let gen_id prefix seed =
 466  let res = prefix ^ string_of_int !seed in
 467   incr seed ;
 468   res
 469 ;;
 470
 471 let build_def_item seed context metasenv id n t ty =
 472  let module K = Content in
 473 (*
 474   try
 475    let sort = Hashtbl.find ids_to_inner_sorts id in
 476    if sort = `Prop then
 477        (let p =
 478         (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
 479        in
 480         `Proof p;)
 481    else
 482 *)
 483       `Definition
 484         { K.def_name = Some n;
 485           K.def_id = gen_id definition_prefix seed;
 486           K.def_aref = id;
 487           K.def_term = t;
 488           K.def_type = ty
 489         }
 490 (*
 491   with
 492    Not_found -> assert false
 493 *)
 494
 495 let build_decl_item seed id n s =
 496  let module K = Content in
 497 (*
 498  let sort =
 499    try
 500     Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
 501    with Not_found -> None
 502  in
 503  match sort with
 504  | Some `Prop ->
 505     `Hypothesis
 506       { K.dec_name = name_of n;
 507         K.dec_id = gen_id declaration_prefix seed;
 508         K.dec_inductive = false;
 509         K.dec_aref = id;
 510         K.dec_type = s
 511       }
 512  | _ ->
 513 *)
 514     `Declaration
 515       { K.dec_name = Some n;
 516         K.dec_id = gen_id declaration_prefix seed;
 517         K.dec_inductive = false;
 518         K.dec_aref = id;
 519         K.dec_type = s
 520       }
 521 ;;
 522
 523 let nmap_obj (uri,_,metasenv,subst,kind) =
 524   let module K = Content in
 525   let ids_to_refs = Hashtbl.create 503 in
 526   let register_ref = Hashtbl.add ids_to_refs in
 527   let ids_to_father_ids = Hashtbl.create 503 in
 528   let register_father_id = Hashtbl.add ids_to_father_ids in
 529   let freshid = freshid register_ref register_father_id in
 530   let nast_of_cic ~context =
 531    nast_of_cic1 ~freshid ~output_type:`Term ~subst ~context None in
 532   let seed = ref 0 in
 533   let conjectures =
 534    match metasenv with
 535       [] -> None
 536     | _ -> (*Some (List.map (map_conjectures seed) metasenv)*)
 537       (*CSC: used to be the previous line, that uses seed *)
 538       Some (List.map (nmap_sequent0 ~freshid ~subst) metasenv)
 539   in
 540   let res =
 541    match kind with
 542       NCic.Constant (_,_,Some bo,ty,_) ->
 543        let ty = nast_of_cic ~context:[] ty in
 544        let bo = nast_of_cic ~context:[] bo in
 545         (gen_id object_prefix seed, [], conjectures,
 546           `Def (K.Const,ty,
 547             build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
 548     | NCic.Constant (_,_,None,ty,_) ->
 549        let ty = nast_of_cic ~context:[] ty in
 550          (gen_id object_prefix seed, [], conjectures,
 551            `Decl (K.Const,
 552              (*CSC: ??? get_id ty here used to be the id of the axiom! *)
 553              build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
 554 (*
 555     | C.AInductiveDefinition (id,l,params,nparams,_) ->
 556          (gen_id object_prefix seed, params, conjectures,
 557             `Joint
 558               { K.joint_id = gen_id joint_prefix seed;
 559                 K.joint_kind = `Inductive nparams;
 560                 K.joint_defs = List.map (build_inductive seed) l
 561               })
 562
 563 and
 564     build_inductive seed =
 565      let module K = Content in
 566       fun (_,n,b,ty,l) ->
 567         `Inductive
 568           { K.inductive_id = gen_id inductive_prefix seed;
 569             K.inductive_name = n;
 570             K.inductive_kind = b;
 571             K.inductive_type = ty;
 572             K.inductive_constructors = build_constructors seed l
 573            }
 574
 575 and
 576     build_constructors seed l =
 577      let module K = Content in
 578       List.map
 579        (fun (n,t) ->
 580            { K.dec_name = Some n;
 581              K.dec_id = gen_id declaration_prefix seed;
 582              K.dec_inductive = false;
 583              K.dec_aref = "";
 584              K.dec_type = t
 585            }) l
 586 *)
 587  in
 588   res,ids_to_refs,ids_to_father_ids
 589 ;;