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