helm/ocaml/cic_notation/cicNotationFwd.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 module Ast = CicNotationPt
  29 module Env = CicNotationEnv
  30
  31 (* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
  32  * be removes as soon as we believe implementation are equivalent *)
  33 (* let meta_names_of term =
  34   let rec names = ref [] in
  35   let add_name n =
  36     if List.mem n !names then ()
  37     else names := n :: !names
  38   in
  39   let rec aux = function
  40     | AttributedTerm (_, term) -> aux term
  41     | Appl terms -> List.iter aux terms
  42     | Binder (_, _, body) -> aux body
  43     | Case (term, indty, outty_opt, patterns) ->
  44         aux term ;
  45         aux_opt outty_opt ;
  46         List.iter aux_branch patterns
  47     | LetIn (_, t1, t2) ->
  48         aux t1 ;
  49         aux t2
  50     | LetRec (_, definitions, body) ->
  51         List.iter aux_definition definitions ;
  52         aux body
  53     | Uri (_, Some substs) -> aux_substs substs
  54     | Ident (_, Some substs) -> aux_substs substs
  55     | Meta (_, substs) -> aux_meta_substs substs
  56
  57     | Implicit
  58     | Ident _
  59     | Num _
  60     | Sort _
  61     | Symbol _
  62     | Uri _
  63     | UserInput -> ()
  64
  65     | Magic magic -> aux_magic magic
  66     | Variable var -> aux_variable var
  67
  68     | _ -> assert false
  69   and aux_opt = function
  70     | Some term -> aux term
  71     | None -> ()
  72   and aux_capture_var (_, ty_opt) = aux_opt ty_opt
  73   and aux_branch (pattern, term) =
  74     aux_pattern pattern ;
  75     aux term
  76   and aux_pattern (head, vars) =
  77     List.iter aux_capture_var vars
  78   and aux_definition (var, term, i) =
  79     aux_capture_var var ;
  80     aux term
  81   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
  82   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
  83   and aux_variable = function
  84     | NumVar name -> add_name name
  85     | IdentVar name -> add_name name
  86     | TermVar name -> add_name name
  87     | FreshVar _ -> ()
  88     | Ascription _ -> assert false
  89   and aux_magic = function
  90     | Default (t1, t2)
  91     | Fold (_, t1, _, t2) ->
  92         aux t1 ;
  93         aux t2
  94     | _ -> assert false
  95   in
  96   aux term ;
  97   !names *)
  98
  99 let unopt_names names env =
 100   let rec aux acc = function
 101     | (name, (ty, v)) :: tl when List.mem name names ->
 102         (match ty, v with
 103         | Env.OptType ty, Env.OptValue (Some v) ->
 104             aux ((name, (ty, v)) :: acc) tl
 105         | _ -> assert false)
 106     | _ :: tl -> aux acc tl
 107       (* some pattern may contain only meta names, thus we trash all others *)
 108     | [] -> acc
 109   in
 110   aux [] env
 111
 112 let head_names names env =
 113   let rec aux acc = function
 114     | (name, (ty, v)) :: tl when List.mem name names ->
 115         (match ty, v with
 116         | Env.ListType ty, Env.ListValue (v :: _) ->
 117             aux ((name, (ty, v)) :: acc) tl
 118         | _ -> assert false)
 119     | _ :: tl -> aux acc tl
 120       (* base pattern may contain only meta names, thus we trash all others *)
 121     | [] -> acc
 122   in
 123   aux [] env
 124
 125 let tail_names names env =
 126   let rec aux acc = function
 127     | (name, (ty, v)) :: tl when List.mem name names ->
 128         (match ty, v with
 129         | Env.ListType ty, Env.ListValue (_ :: vtl) ->
 130             aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
 131         | _ -> assert false)
 132     | binding :: tl -> aux (binding :: acc) tl
 133     | [] -> acc
 134   in
 135   aux [] env
 136
 137 let instantiate_level2 env term =
 138   let fresh_env = ref [] in
 139   let lookup_fresh_name n =
 140     try
 141       List.assoc n !fresh_env
 142     with Not_found ->
 143       let new_name = CicNotationUtil.fresh_name () in
 144       fresh_env := (n, new_name) :: !fresh_env;
 145       new_name
 146   in
 147   let rec aux env term =
 148     match term with
 149     | Ast.AttributedTerm (_, term) -> aux env term
 150     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
 151     | Ast.Binder (binder, var, body) ->
 152         Ast.Binder (binder, aux_capture_var env var, aux env body)
 153     | Ast.Case (term, indty, outty_opt, patterns) ->
 154         Ast.Case (aux env term, indty, aux_opt env outty_opt,
 155           List.map (aux_branch env) patterns)
 156     | Ast.LetIn (var, t1, t2) ->
 157         Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
 158     | Ast.LetRec (kind, definitions, body) ->
 159         Ast.LetRec (kind, List.map (aux_definition env) definitions,
 160           aux env body)
 161     | Ast.Uri (name, None) -> Ast.Uri (name, None)
 162     | Ast.Uri (name, Some substs) ->
 163         Ast.Uri (name, Some (aux_substs env substs))
 164     | Ast.Ident (name, Some substs) ->
 165         Ast.Ident (name, Some (aux_substs env substs))
 166     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 167
 168     | Ast.Implicit
 169     | Ast.Ident _
 170     | Ast.Num _
 171     | Ast.Sort _
 172     | Ast.Symbol _
 173     | Ast.UserInput -> term
 174
 175     | Ast.Magic magic -> aux_magic env magic
 176     | Ast.Variable var -> aux_variable env var
 177
 178     | _ -> assert false
 179   and aux_opt env = function
 180     | Some term -> Some (aux env term)
 181     | None -> None
 182   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
 183   and aux_branch env (pattern, term) =
 184     (aux_pattern env pattern, aux env term)
 185   and aux_pattern env (head, vars) =
 186     (head, List.map (aux_capture_var env) vars)
 187   and aux_definition env (var, term, i) =
 188     (aux_capture_var env var, aux env term, i)
 189   and aux_substs env substs =
 190     List.map (fun (name, term) -> (name, aux env term)) substs
 191   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
 192   and aux_variable env = function
 193     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
 194     | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
 195     | Ast.TermVar name -> Env.lookup_term env name
 196     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
 197     | Ast.Ascription (term, name) -> assert false
 198   and aux_magic env = function
 199     | Ast.Default (some_pattern, none_pattern) ->
 200         (match CicNotationUtil.names_of_term some_pattern with
 201         | [] -> assert false (* some pattern must contain at least 1 name *)
 202         | (name :: _) as names ->
 203             (match Env.lookup_value env name with
 204             | Env.OptValue (Some _) ->
 205                 (* assumption: if "name" above is bound to Some _, then all
 206                  * names returned by "meta_names_of" are bound to Some _ as well
 207                  *)
 208                 aux (unopt_names names env) some_pattern
 209             | Env.OptValue None -> aux env none_pattern
 210             | _ -> assert false))
 211     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
 212         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 213         let meta_names =
 214           List.filter ((<>) acc_name)
 215             (CicNotationUtil.names_of_term rec_pattern)
 216         in
 217         (match meta_names with
 218         | [] -> assert false (* as above *)
 219         | (name :: _) as names ->
 220             let rec instantiate_fold_left acc env' =
 221               match Env.lookup_value env' name with
 222               | Env.ListValue (_ :: _) ->
 223                   instantiate_fold_left
 224                     (let acc_binding =
 225                       acc_name, (Env.TermType, Env.TermValue acc)
 226                      in
 227                      aux (acc_binding :: head_names names env') rec_pattern)
 228                     (tail_names names env')
 229               | Env.ListValue [] -> acc
 230               | _ -> assert false
 231             in
 232             instantiate_fold_left (aux env base_pattern) env)
 233     | Ast.Fold (`Right, base_pattern, names, rec_pattern) ->
 234         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 235         let meta_names =
 236           List.filter ((<>) acc_name)
 237             (CicNotationUtil.names_of_term rec_pattern)
 238         in
 239         (match meta_names with
 240         | [] -> assert false (* as above *)
 241         | (name :: _) as names ->
 242             let rec instantiate_fold_right env' =
 243               match Env.lookup_value env' name with
 244               | Env.ListValue (_ :: _) ->
 245                   let acc = instantiate_fold_right (tail_names names env') in
 246                   let acc_binding =
 247                     acc_name, (Env.TermType, Env.TermValue acc)
 248                   in
 249                   aux (acc_binding :: head_names names env') rec_pattern
 250               | Env.ListValue [] -> aux env base_pattern
 251               | _ -> assert false
 252             in
 253             instantiate_fold_right env)
 254     | Ast.If (_, p_true, p_false) as t ->
 255         aux env (CicNotationUtil.find_branch (Ast.Magic t))
 256     | Ast.Fail -> assert false
 257     | _ -> assert false
 258   in
 259   aux env term
 260
 261 let instantiate_appl_pattern env appl_pattern =
 262   let lookup name =
 263     try List.assoc name env
 264     with Not_found ->
 265       prerr_endline (sprintf "Name %s not found" name);
 266       assert false
 267   in
 268   let rec aux = function
 269     | Ast.UriPattern uri -> CicUtil.term_of_uri uri
 270     | Ast.ImplicitPattern -> Cic.Implicit None
 271     | Ast.VarPattern name -> lookup name
 272     | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
 273   in
 274   aux appl_pattern
 275