helm/ocaml/cic_notation/cicNotationUtil.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 CicNotationPt
  27
  28 (* let meta_names_of term = *)
  29 (*   let rec names = ref [] in *)
  30 (*   let add_name n = *)
  31 (*     if List.mem n !names then () *)
  32 (*     else names := n :: !names *)
  33 (*   in *)
  34 (*   let rec aux = function *)
  35 (*     | AttributedTerm (_, term) -> aux term *)
  36 (*     | Appl terms -> List.iter aux terms *)
  37 (*     | Binder (_, _, body) -> aux body *)
  38 (*     | Case (term, indty, outty_opt, patterns) -> *)
  39 (*         aux term ; *)
  40 (*         aux_opt outty_opt ; *)
  41 (*         List.iter aux_branch patterns *)
  42 (*     | LetIn (_, t1, t2) -> *)
  43 (*         aux t1 ; *)
  44 (*         aux t2 *)
  45 (*     | LetRec (_, definitions, body) -> *)
  46 (*         List.iter aux_definition definitions ; *)
  47 (*         aux body *)
  48 (*     | Uri (_, Some substs) -> aux_substs substs *)
  49 (*     | Ident (_, Some substs) -> aux_substs substs *)
  50 (*     | Meta (_, substs) -> aux_meta_substs substs *)
  51
  52 (*     | Implicit *)
  53 (*     | Ident _ *)
  54 (*     | Num _ *)
  55 (*     | Sort _ *)
  56 (*     | Symbol _ *)
  57 (*     | Uri _ *)
  58 (*     | UserInput -> () *)
  59
  60 (*     | Magic magic -> aux_magic magic *)
  61 (*     | Variable var -> aux_variable var *)
  62
  63 (*     | _ -> assert false *)
  64 (*   and aux_opt = function *)
  65 (*     | Some term -> aux term *)
  66 (*     | None -> () *)
  67 (*   and aux_capture_var (_, ty_opt) = aux_opt ty_opt *)
  68 (*   and aux_branch (pattern, term) = *)
  69 (*     aux_pattern pattern ; *)
  70 (*     aux term *)
  71 (*   and aux_pattern (head, vars) =  *)
  72 (*     List.iter aux_capture_var vars *)
  73 (*   and aux_definition (var, term, i) = *)
  74 (*     aux_capture_var var ; *)
  75 (*     aux term *)
  76 (*   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs *)
  77 (*   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs *)
  78 (*   and aux_variable = function *)
  79 (*     | NumVar name -> add_name name *)
  80 (*     | IdentVar name -> add_name name *)
  81 (*     | TermVar name -> add_name name *)
  82 (*     | FreshVar _ -> () *)
  83 (*     | Ascription _ -> assert false *)
  84 (*   and aux_magic = function *)
  85 (*     | Default (t1, t2) *)
  86 (*     | Fold (_, t1, _, t2) -> *)
  87 (*         aux t1 ; *)
  88 (*         aux t2 *)
  89 (*     | _ -> assert false *)
  90 (*   in *)
  91 (*   aux term ; *)
  92 (*   !names *)
  93
  94 let visit_ast ?(special_k = fun _ -> assert false) k =
  95   let rec aux = function
  96     | Appl terms -> Appl (List.map k terms)
  97     | Binder (kind, var, body) ->
  98         Binder (kind, aux_capture_variable var, k body)
  99     | Case (term, indtype, typ, patterns) ->
 100         Case (k term, indtype, aux_opt typ, aux_patterns patterns)
 101     | Cast (t1, t2) -> Cast (k t1, k t2)
 102     | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
 103     | LetRec (kind, definitions, term) ->
 104         let definitions =
 105           List.map
 106             (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
 107             definitions
 108         in
 109         LetRec (kind, definitions, k term)
 110     | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
 111     | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
 112     | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
 113     | (AttributedTerm _
 114       | Layout _
 115       | Literal _
 116       | Magic _
 117       | Variable _) as t -> special_k t
 118     | (Ident _
 119       | Implicit
 120       | Num _
 121       | Sort _
 122       | Symbol _
 123       | Uri _
 124       | UserInput) as t -> t
 125   and aux_opt = function
 126     | None -> None
 127     | Some term -> Some (k term)
 128   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
 129   and aux_patterns patterns = List.map aux_pattern patterns
 130   and aux_pattern ((head, vars), term) =
 131     ((head, List.map aux_capture_variable vars), k term)
 132   and aux_subst (name, term) = (name, k term)
 133   and aux_substs substs = List.map aux_subst substs
 134   in
 135   aux
 136
 137 let visit_layout k = function
 138   | Sub (t1, t2) -> Sub (k t1, k t2)
 139   | Sup (t1, t2) -> Sup (k t1, k t2)
 140   | Below (t1, t2) -> Below (k t1, k t2)
 141   | Above (t1, t2) -> Above (k t1, k t2)
 142   | Over (t1, t2) -> Over (k t1, k t2)
 143   | Atop (t1, t2) -> Atop (k t1, k t2)
 144   | Frac (t1, t2) -> Frac (k t1, k t2)
 145   | Sqrt t -> Sqrt (k t)
 146   | Root (arg, index) -> Root (k arg, k index)
 147   | Break -> Break
 148   | Box (kind, terms) -> Box (kind, List.map k terms)
 149   | Group terms -> Group (List.map k terms)
 150
 151 let visit_magic k = function
 152   | List0 (t, l) -> List0 (k t, l)
 153   | List1 (t, l) -> List1 (k t, l)
 154   | Opt t -> Opt (k t)
 155   | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
 156   | Default (t1, t2) -> Default (k t1, k t2)
 157   | If (t1, t2, t3) -> If (k t1, k t2, k t3)
 158   | Fail -> Fail
 159
 160 let variables_of_term t =
 161   let rec vars = ref [] in
 162   let add_variable v =
 163     if List.mem v !vars then ()
 164     else vars := v :: !vars
 165   in
 166   let rec aux = function
 167     | Magic m -> Magic (visit_magic aux m)
 168     | Layout l -> Layout (visit_layout aux l)
 169     | Variable v -> Variable (aux_variable v)
 170     | Literal _ as t -> t
 171     | AttributedTerm (_, t) -> aux t
 172     | t -> visit_ast aux t
 173   and aux_variable = function
 174     | (NumVar _
 175       | IdentVar _
 176       | TermVar _) as t ->
 177         add_variable t ;
 178         t
 179     | FreshVar _ as t -> t
 180     | Ascription _ -> assert false
 181   in
 182     ignore (aux t) ;
 183     !vars
 184
 185 let names_of_term t =
 186   let aux = function
 187     | NumVar s
 188     | IdentVar s
 189     | TermVar s -> s
 190     | _ -> assert false
 191   in
 192     List.map aux (variables_of_term t)
 193
 194 let keywords_of_term t =
 195   let rec keywords = ref [] in
 196   let add_keyword k = keywords := k :: !keywords in
 197   let rec aux = function
 198     | AttributedTerm (_, t) -> aux t
 199     | Layout l -> Layout (visit_layout aux l)
 200     | Literal (`Keyword k) as t ->
 201         add_keyword k;
 202         t
 203     | Literal _ as t -> t
 204     | Magic m -> Magic (visit_magic aux m)
 205     | Variable _ as v -> v
 206     | t -> visit_ast aux t
 207   in
 208     ignore (aux t) ;
 209     !keywords
 210
 211 let rec strip_attributes t =
 212   let special_k = function
 213     | AttributedTerm (_, term) -> strip_attributes term
 214     | Magic m -> Magic (visit_magic strip_attributes m)
 215     | Variable _ as t -> t
 216     | t -> assert false
 217   in
 218   visit_ast ~special_k strip_attributes t
 219
 220 let meta_names_of_term term =
 221   let rec names = ref [] in
 222   let add_name n =
 223     if List.mem n !names then ()
 224     else names := n :: !names
 225   in
 226   let rec aux = function
 227     | AttributedTerm (_, term) -> aux term
 228     | Appl terms -> List.iter aux terms
 229     | Binder (_, _, body) -> aux body
 230     | Case (term, indty, outty_opt, patterns) ->
 231         aux term ;
 232         aux_opt outty_opt ;
 233         List.iter aux_branch patterns
 234     | LetIn (_, t1, t2) ->
 235         aux t1 ;
 236         aux t2
 237     | LetRec (_, definitions, body) ->
 238         List.iter aux_definition definitions ;
 239         aux body
 240     | Uri (_, Some substs) -> aux_substs substs
 241     | Ident (_, Some substs) -> aux_substs substs
 242     | Meta (_, substs) -> aux_meta_substs substs
 243
 244     | Implicit
 245     | Ident _
 246     | Num _
 247     | Sort _
 248     | Symbol _
 249     | Uri _
 250     | UserInput -> ()
 251
 252     | Magic magic -> aux_magic magic
 253     | Variable var -> aux_variable var
 254
 255     | _ -> assert false
 256   and aux_opt = function
 257     | Some term -> aux term
 258     | None -> ()
 259   and aux_capture_var (_, ty_opt) = aux_opt ty_opt
 260   and aux_branch (pattern, term) =
 261     aux_pattern pattern ;
 262     aux term
 263   and aux_pattern (head, vars) =
 264     List.iter aux_capture_var vars
 265   and aux_definition (var, term, i) =
 266     aux_capture_var var ;
 267     aux term
 268   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
 269   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
 270   and aux_variable = function
 271     | NumVar name -> add_name name
 272     | IdentVar name -> add_name name
 273     | TermVar name -> add_name name
 274     | FreshVar _ -> ()
 275     | Ascription _ -> assert false
 276   and aux_magic = function
 277     | Default (t1, t2)
 278     | Fold (_, t1, _, t2) ->
 279         aux t1 ;
 280         aux t2
 281     | If (t1, t2, t3) ->
 282         aux t1 ;
 283         aux t2 ;
 284         aux t3
 285     | Fail -> ()
 286     | _ -> assert false
 287   in
 288   aux term ;
 289   !names
 290
 291 let rectangular matrix =
 292   let columns = Array.length matrix.(0) in
 293   try
 294     Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix;
 295     true
 296   with Exit -> false
 297
 298 let ncombine ll =
 299   let matrix = Array.of_list (List.map Array.of_list ll) in
 300   assert (rectangular matrix);
 301   let rows = Array.length matrix in
 302   let columns = Array.length matrix.(0) in
 303   let lists = ref [] in
 304   for j = 0 to columns - 1 do
 305     let l = ref [] in
 306     for i = 0 to rows - 1 do
 307       l := matrix.(i).(j) :: !l
 308     done;
 309     lists := List.rev !l :: !lists
 310   done;
 311   List.rev !lists
 312
 313 let string_of_literal = function
 314   | `Symbol s
 315   | `Keyword s
 316   | `Number s -> s
 317
 318 let boxify = function
 319   | [ a ] -> a
 320   | l -> Layout (Box ((H, false, false), l))
 321
 322 let unboxify = function
 323   | Layout (Box ((H, false, false), [ a ])) -> a
 324   | l -> l
 325
 326 let group = function
 327   | [ a ] -> a
 328   | l -> Layout (Group l)
 329
 330 let ungroup =
 331   let rec aux acc =
 332     function
 333         [] -> List.rev acc
 334       | Layout (Group terms) :: terms' -> aux acc (terms @ terms')
 335       | term :: terms -> aux (term :: acc) terms
 336   in
 337     aux []
 338
 339 let dress sauce =
 340   let rec aux =
 341     function
 342       | [] -> []
 343       | [hd] -> [hd]
 344       | hd :: tl -> hd :: sauce :: aux tl
 345   in
 346     aux
 347
 348 let find_appl_pattern_uris ap =
 349   let rec aux acc =
 350     function
 351     | UriPattern uri ->
 352         (try
 353           ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
 354           acc
 355         with Not_found -> uri :: acc)
 356     | ImplicitPattern
 357     | VarPattern _ -> acc
 358     | ApplPattern apl -> List.fold_left aux acc apl
 359   in
 360   aux [] ap
 361
 362 let rec find_branch =
 363   function
 364       Magic (If (_, Magic Fail, t)) -> find_branch t
 365     | Magic (If (_, t, _)) -> find_branch t
 366     | t -> t
 367
 368 let cic_name_of_name = function
 369   | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
 370   | CicNotationPt.Ident (name, None) -> Cic.Name name
 371   | _ -> assert false
 372
 373 let name_of_cic_name = function
 374   | Cic.Name s -> CicNotationPt.Ident (s, None)
 375   | Cic.Anonymous -> CicNotationPt.Ident ("_", None)
 376
 377 let fresh_index = ref ~-1
 378
 379 type notation_id = int
 380
 381 let fresh_id () =
 382   incr fresh_index;
 383   !fresh_index
 384
 385   (* TODO ensure that names generated by fresh_var do not clash with user's *)
 386 let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
 387