helm/ocaml/cic_notation/cicNotationRew.ml

   1 (* Copyright (C) 2004-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 open Printf
  27
  28 type pattern_id = int
  29 type interpretation_id = pattern_id
  30 type pretty_printer_id = pattern_id
  31
  32 type term_info =
  33   { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
  34     uri: (Cic.id, string) Hashtbl.t;
  35   }
  36
  37 let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
  38
  39 (* module Pattern32 =
  40   struct
  41   type pattern_t = CicNotationPt.cic_appl_pattern
  42   let compatible ap1 ap2 =
  43     match ap1, ap2 with
  44     | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _
  45     | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _
  46     | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true
  47     | _ -> false
  48   end
  49
  50 module Patterns32 = Patterns (Pattern32) *)
  51
  52   (* acic -> ast auxiliary function s *)
  53
  54 let get_types uri =
  55   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
  56     match o with
  57       | Cic.InductiveDefinition (l,_,_,_) -> l
  58       | _ -> assert false
  59
  60 let name_of_inductive_type uri i =
  61   let types = get_types uri in
  62   let (name, _, _, _) = try List.nth types i with Not_found -> assert false in
  63   name
  64
  65   (* returns <name, type> pairs *)
  66 let constructors_of_inductive_type uri i =
  67   let types = get_types uri in
  68   let (_, _, _, constructors) =
  69     try List.nth types i with Not_found -> assert false
  70   in
  71   constructors
  72
  73   (* returns name only *)
  74 let constructor_of_inductive_type uri i j =
  75   (try
  76     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
  77   with Not_found -> assert false)
  78
  79 module Ast = CicNotationPt
  80
  81 let string_of_name = function
  82   | Cic.Name s -> s
  83   | Cic.Anonymous -> "_"
  84
  85 let ident_of_name n = Ast.Ident (string_of_name n, None)
  86
  87 let idref id t = Ast.AttributedTerm (`IdRef id, t)
  88
  89 let pp_ast0 t k =
  90   prerr_endline "pp_ast0";
  91   let rec aux t = CicNotationUtil.visit_ast ~special_k k t
  92   and special_k = function
  93     | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
  94     | _ -> assert false
  95   in
  96   aux t
  97
  98 let ast_of_acic0 term_info acic k =
  99 (*   prerr_endline "ast_of_acic0"; *)
 100   let k = k term_info in
 101   let register_uri id uri = Hashtbl.add term_info.uri id uri in
 102   let sort_of_id id =
 103     try
 104       Hashtbl.find term_info.sort id
 105     with Not_found -> assert false
 106   in
 107   let aux_substs substs =
 108     Some
 109       (List.map
 110         (fun (uri, annterm) -> (UriManager.name_of_uri uri, k annterm))
 111         substs)
 112   in
 113   let aux_context context =
 114     List.map
 115       (function
 116         | None -> None
 117         | Some annterm -> Some (k annterm))
 118       context
 119   in
 120   let aux = function
 121     | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
 122     | Cic.AVar (id,uri,substs) ->
 123         register_uri id (UriManager.string_of_uri uri);
 124         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
 125     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
 126     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
 127     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
 128     | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
 129     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
 130     | Cic.AImplicit _ -> assert false
 131     | Cic.AProd (id,n,s,t) ->
 132         let binder_kind =
 133           match sort_of_id id with
 134           | `Set | `Type -> `Pi
 135           | `Prop | `CProp -> `Forall
 136         in
 137         idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t))
 138     | Cic.ACast (id,v,t) ->
 139         idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t])
 140     | Cic.ALambda (id,n,s,t) ->
 141         idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t))
 142     | Cic.ALetIn (id,n,s,t) ->
 143         idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
 144     | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
 145     | Cic.AConst (id,uri,substs) ->
 146         register_uri id (UriManager.string_of_uri uri);
 147         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
 148     | Cic.AMutInd (id,uri,i,substs) as t ->
 149         let name = name_of_inductive_type uri i in
 150         let uri_str = UriManager.string_of_uri uri in
 151         let puri_str =
 152           uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")"
 153         in
 154         register_uri id puri_str;
 155         idref id (Ast.Ident (name, aux_substs substs))
 156     | Cic.AMutConstruct (id,uri,i,j,substs) ->
 157         let name = constructor_of_inductive_type uri i j in
 158         let uri_str = UriManager.string_of_uri uri in
 159         let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
 160         register_uri id puri_str;
 161         idref id (Ast.Ident (name, aux_substs substs))
 162     | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
 163         let name = name_of_inductive_type uri typeno in
 164         let constructors = constructors_of_inductive_type uri typeno in
 165         let rec eat_branch ty pat =
 166           match (ty, pat) with
 167           | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
 168               let (cv, rhs) = eat_branch t t' in
 169               (ident_of_name name, Some (k s)) :: cv, rhs
 170           | _, _ -> [], k pat
 171         in
 172         let patterns =
 173           List.map2
 174             (fun (name, ty) pat ->
 175               let (capture_variables, rhs) = eat_branch ty pat in
 176               ((name, capture_variables), rhs))
 177             constructors patterns
 178         in
 179         idref id (Ast.Case (k te, Some name, Some (k ty), patterns))
 180     | Cic.AFix (id, no, funs) ->
 181         let defs =
 182           List.map
 183             (fun (_, n, decr_idx, ty, bo) ->
 184               ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
 185             funs
 186         in
 187         let name =
 188           try
 189             (match List.nth defs no with
 190             | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
 191             | _ -> assert false)
 192           with Not_found -> assert false
 193         in
 194         idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
 195     | Cic.ACoFix (id, no, funs) ->
 196         let defs =
 197           List.map
 198             (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
 199             funs
 200         in
 201         let name =
 202           try
 203             (match List.nth defs no with
 204             | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
 205             | _ -> assert false)
 206           with Not_found -> assert false
 207         in
 208         idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
 209   in
 210   aux acic
 211
 212   (* persistent state *)
 213
 214 let level1_patterns21 = Hashtbl.create 211
 215 (* let level2_patterns32 = Hashtbl.create 211 *)
 216
 217 let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * pattern_id) option)
 218 option ref) =
 219   ref None
 220 (* let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
 221   ref None *)
 222
 223 let pattern21_matrix = ref []
 224 (* let pattern32_matrix = ref Patterns32.empty *)
 225
 226 let get_compiled21 () =
 227   match !compiled21 with
 228   | None -> assert false
 229   | Some f -> f
 230 (* let get_compiled32 () =
 231   match !compiled32 with
 232   | None -> assert false
 233   | Some f -> f *)
 234
 235 let set_compiled21 f = compiled21 := Some f
 236 (* let set_compiled32 f = compiled32 := Some f *)
 237
 238   (* "envl" is a list of triples:
 239    *   <name environment, term environment, pattern id>, where
 240    *   name environment: (string * string) list
 241    *   term environment: (string * Cic.annterm) list *)
 242 let return_closure success_k =
 243   (fun term_info terms envl ->
 244 (*     prerr_endline "return_closure"; *)
 245     match terms with
 246     | [] ->
 247         (try
 248           success_k term_info (List.hd envl)
 249         with Failure _ -> assert false)
 250     | _ -> assert false)
 251
 252 let variable_closure names k =
 253   (fun term_info terms envl ->
 254 (*     prerr_endline "variable_closure"; *)
 255     match terms with
 256     | hd :: tl ->
 257         let envl' =
 258           List.map2
 259             (fun arg (name_env, term_env, pid) ->
 260               let rec aux name_env term_env pid arg term =
 261                 match arg, term with
 262                   Ast.IdentArg name, _ ->
 263                     (name_env, (name, term) :: term_env, pid)
 264                 | Ast.EtaArg (Some name, arg'),
 265                   Cic.ALambda (id, name', ty, body) ->
 266                     aux
 267                       ((name, (string_of_name name', Some (ty, id))) :: name_env)
 268                       term_env pid arg' body
 269                 | Ast.EtaArg (Some name, arg'), _ ->
 270                     let name' = CicNotationUtil.fresh_name () in
 271                     aux ((name, (name', None)) :: name_env)
 272                       term_env pid arg' term
 273                 | Ast.EtaArg (None, arg'), Cic.ALambda (id, name, ty, body) ->
 274                     assert false
 275                 | Ast.EtaArg (None, arg'), _ ->
 276                     assert false
 277               in
 278                 aux name_env term_env pid arg hd)
 279             names envl
 280         in
 281         k term_info tl envl'
 282     | _ -> assert false)
 283
 284 let appl_closure ks k =
 285   (fun term_info terms envl ->
 286 (*     prerr_endline "appl_closure"; *)
 287     (match terms with
 288     | Cic.AAppl (_, args) :: tl ->
 289         (try
 290           let k' = List.assoc (List.length args) ks in
 291           k' term_info (args @ tl) envl
 292         with Not_found -> k term_info terms envl)
 293     | [] -> assert false
 294     | _ -> k term_info terms envl))
 295
 296 let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
 297
 298 let uri_closure ks k =
 299   (fun term_info terms envl ->
 300 (*     prerr_endline "uri_closure"; *)
 301     (match terms with
 302     | [] -> assert false
 303     | hd :: tl ->
 304 (*         prerr_endline (sprintf "uri_of_term = %s" (uri_of_term hd)); *)
 305         begin
 306           try
 307             let k' = List.assoc (uri_of_term hd) ks in
 308             k' term_info tl envl
 309           with
 310           | Invalid_argument _  (* raised by uri_of_term *)
 311           | Not_found -> k term_info terms envl
 312         end))
 313
 314   (* compiler from level 3 to level 2 *)
 315 (* let compiler32 (t: Patterns32.t) success_k fail_k =
 316   let rec aux t k = |+ k is a continuation +|
 317     if t = [] then
 318       k
 319     else if Patterns32.are_empty t then begin
 320       (match t with
 321       | _::_::_ ->
 322           |+ XXX optimization possible here: throw away all except one of the
 323            * rules which lead to ambiguity +|
 324           warning "ambiguous interpretation"
 325       | _ -> ());
 326       return_closure success_k
 327     end else
 328       match Patterns32.horizontal_split t with
 329       | t', [] ->
 330           (match t' with
 331           | []
 332           | ([], _) :: _ -> assert false
 333           | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _
 334           | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ ->
 335               let first_column, t'' = Patterns32.vertical_split t' in
 336               let names =
 337                 List.map
 338                   (function
 339                     | Ast.ArgPattern arg -> arg
 340                     | _ -> assert false)
 341                   first_column
 342               in
 343               variable_closure names (aux t'' k)
 344           | (Ast.ApplPattern _ :: _, _) :: _ ->
 345               let pidl =
 346                 List.map
 347                   (function
 348                     | (Ast.ApplPattern args) :: _, _ -> List.length args
 349                     | _ -> assert false)
 350                   t'
 351               in
 352                 |+ arity partitioning +|
 353               let clusters = Patterns32.partition t' pidl in
 354               let ks =  |+ k continuation list +|
 355                 List.map
 356                   (fun (len, cluster) ->
 357                     let cluster' =
 358                       List.map  |+ add args as patterns heads +|
 359                         (function
 360                           | (Ast.ApplPattern args) :: tl, pid ->
 361                               |+ let's throw away "teste di cluster" +|
 362                               args @ tl, pid
 363                           | _ -> assert false)
 364                         cluster
 365                     in
 366                     len, aux cluster' k)
 367                   clusters
 368               in
 369               appl_closure ks k
 370           | (Ast.UriPattern _ :: _, _) :: _ ->
 371               let uidmap, pidl =
 372                 let urimap = ref [] in
 373                 let uidmap = ref [] in
 374                 let get_uri_id uri =
 375                   try
 376                     List.assoc uri !urimap
 377                   with
 378                     Not_found ->
 379                       let uid = List.length !urimap in
 380                       urimap := (uri, uid) :: !urimap ;
 381                       uidmap := (uid, uri) :: !uidmap ;
 382                       uid
 383                 in
 384                 let uidl =
 385                   List.map
 386                     (function
 387                       | (Ast.UriPattern uri) :: _, _ -> get_uri_id uri
 388                       | _ -> assert false)
 389                     t'
 390                 in
 391                   !uidmap, uidl
 392               in
 393               let clusters = Patterns32.partition t' pidl in
 394               let ks =
 395                 List.map
 396                   (fun (uid, cluster) ->
 397                     let cluster' =
 398                       List.map
 399                         (function
 400                         | (Ast.UriPattern uri) :: tl, pid -> tl, pid
 401                         | _ -> assert false)
 402                       cluster
 403                     in
 404                     List.assoc uid uidmap, aux cluster' k)
 405                   clusters
 406               in
 407               uri_closure ks k)
 408       | t', tl -> aux t' (aux tl k)
 409   in
 410   let matcher = aux t (fun _ _ -> raise No_match) in
 411   (fun term_info annterm ->
 412     try
 413       matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t)
 414     with No_match -> fail_k term_info annterm)
 415
 416 let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm *)
 417
 418 let instantiate21 env pid =
 419   prerr_endline "instantiate21";
 420   let precedence, associativity, l1 =
 421     try
 422       Hashtbl.find level1_patterns21 pid
 423     with Not_found -> assert false
 424   in
 425   let rec subst = function
 426     | Ast.AttributedTerm (_, t) -> subst t
 427     | Ast.Variable var ->
 428         let name, expected_ty = CicNotationEnv.declaration_of_var var in
 429         let ty, value =
 430           try
 431             List.assoc name env
 432           with Not_found -> assert false
 433         in
 434         assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
 435         (* following assertion should be a conditional that makes this
 436          * instantiation fail *)
 437         assert (CicNotationEnv.well_typed expected_ty value);
 438         CicNotationEnv.term_of_value value
 439     | Ast.Magic _ -> assert false (* TO BE IMPLEMENTED *)
 440     | Ast.Literal _ as t -> t
 441     | Ast.Layout l -> Ast.Layout (subst_layout l)
 442     | t -> CicNotationUtil.visit_ast subst t
 443   and subst_layout l = CicNotationUtil.visit_layout subst l in
 444   subst l1
 445
 446 let rec pp_ast1 term =
 447   let rec pp_value = function
 448     | CicNotationEnv.NumValue _ as v -> v
 449     | CicNotationEnv.StringValue _ as v -> v
 450     | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
 451     | CicNotationEnv.OptValue None as v -> v
 452     | CicNotationEnv.OptValue (Some v) ->
 453         CicNotationEnv.OptValue (Some (pp_value v))
 454     | CicNotationEnv.ListValue vl ->
 455         CicNotationEnv.ListValue (List.map pp_value vl)
 456   in
 457   let ast_env_of_env env =
 458     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
 459   in
 460   match (get_compiled21 ()) term with
 461   | None -> pp_ast0 term pp_ast1
 462   | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid
 463
 464 (* let instantiate32 term_info name_env term_env pid =
 465   let symbol, args =
 466     try
 467       Hashtbl.find level2_patterns32 pid
 468     with Not_found -> assert false
 469   in
 470   let rec instantiate_arg = function
 471     | Ast.IdentArg name ->
 472         (try List.assoc name term_env with Not_found -> assert false)
 473     | Ast.EtaArg (None, _) -> assert false  |+ TODO +|
 474     | Ast.EtaArg (Some name, arg) ->
 475         let (name', ty_opt) =
 476           try List.assoc name name_env with Not_found -> assert false
 477         in
 478         let body = instantiate_arg arg in
 479         let name' = Ast.Ident (name', None) in
 480         match ty_opt with
 481         | None -> Ast.Binder (`Lambda, (name', None), body)
 482         | Some (ty, id) ->
 483             idref id (Ast.Binder (`Lambda, (name', Some ty), body))
 484   in
 485   let args' = List.map instantiate_arg args in
 486   Ast.Appl (Ast.Symbol (symbol, 0) :: args')
 487
 488 let load_patterns32 t =
 489   let ast_env_of_name_env term_info name_env =
 490     List.map
 491       (fun (name, (name', ty_opt)) ->
 492         let ast_ty_opt =
 493           match ty_opt with
 494           | None -> None
 495           | Some (annterm, id) -> Some (ast_of_acic1 term_info annterm, id)
 496         in
 497         (name, (name', ast_ty_opt)))
 498       name_env
 499   in
 500   let ast_env_of_term_env term_info =
 501     List.map (fun (name, term) -> (name, ast_of_acic1 term_info term))
 502   in
 503   let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in
 504   let success_k term_info (name_env, term_env, pid) =
 505     instantiate32
 506       term_info
 507       (ast_env_of_name_env term_info name_env)
 508       (ast_env_of_term_env term_info term_env)
 509       pid
 510   in
 511   let compiled32 = compiler32 t success_k fail_k in
 512   set_compiled32 compiled32 *)
 513
 514 let load_patterns21 t =
 515   set_compiled21 (CicNotationMatcher.T21.compiler t)
 516
 517 (* let ast_of_acic id_to_sort annterm =
 518   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
 519   let ast = ast_of_acic1 term_info annterm in
 520   ast, term_info.uri *)
 521
 522 let pp_ast term = pp_ast1 term
 523
 524 let fresh_id =
 525   let counter = ref ~-1 in
 526   fun () ->
 527     incr counter;
 528     !counter
 529
 530 (* let add_interpretation (symbol, args) appl_pattern =
 531   let id = fresh_id () in
 532   Hashtbl.add level2_patterns32 id (symbol, args);
 533   pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix;
 534   load_patterns32 !pattern32_matrix;
 535   id *)
 536
 537 let add_pretty_printer ?precedence ?associativity l2 l1 =
 538   let id = fresh_id () in
 539   let l2' = CicNotationUtil.strip_attributes l2 in
 540   Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
 541   pattern21_matrix := (l2', id) :: !pattern21_matrix;
 542   load_patterns21 !pattern21_matrix;
 543   id
 544
 545 exception Interpretation_not_found
 546 exception Pretty_printer_not_found
 547
 548 (* let remove_interpretation id =
 549   (try
 550     Hashtbl.remove level2_patterns32 id;
 551   with Not_found -> raise Interpretation_not_found);
 552   pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;
 553   load_patterns32 !pattern32_matrix *)
 554
 555 let remove_pretty_printer id =
 556   (try
 557     Hashtbl.remove level1_patterns21 id;
 558   with Not_found -> raise Pretty_printer_not_found);
 559   pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
 560   load_patterns21 !pattern21_matrix
 561
 562 let _ =
 563   load_patterns21 [];
 564 (*   load_patterns32 [] *)
 565