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 let unopt_names names env =
  32   let rec aux acc = function
  33     | (name, (ty, v)) :: tl when List.mem name names ->
  34         (match ty, v with
  35         | Env.OptType ty, Env.OptValue (Some v) ->
  36             aux ((name, (ty, v)) :: acc) tl
  37         | _ -> assert false)
  38     | _ :: tl -> aux acc tl
  39       (* some pattern may contain only meta names, thus we trash all others *)
  40     | [] -> acc
  41   in
  42   aux [] env
  43
  44 let head_names names env =
  45   let rec aux acc = function
  46     | (name, (ty, v)) :: tl when List.mem name names ->
  47         (match ty, v with
  48         | Env.ListType ty, Env.ListValue (v :: _) ->
  49             aux ((name, (ty, v)) :: acc) tl
  50         | _ -> assert false)
  51     | _ :: tl -> aux acc tl
  52       (* base pattern may contain only meta names, thus we trash all others *)
  53     | [] -> acc
  54   in
  55   aux [] env
  56
  57 let tail_names names env =
  58   let rec aux acc = function
  59     | (name, (ty, v)) :: tl when List.mem name names ->
  60         (match ty, v with
  61         | Env.ListType ty, Env.ListValue (_ :: vtl) ->
  62             aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
  63         | _ -> assert false)
  64     | binding :: tl -> aux (binding :: acc) tl
  65     | [] -> acc
  66   in
  67   aux [] env
  68
  69 let instantiate_level2 env term =
  70   let fresh_env = ref [] in
  71   let lookup_fresh_name n =
  72     try
  73       List.assoc n !fresh_env
  74     with Not_found ->
  75       let new_name = CicNotationUtil.fresh_name () in
  76       fresh_env := (n, new_name) :: !fresh_env;
  77       new_name
  78   in
  79   let rec aux env term =
  80     match term with
  81     | Ast.AttributedTerm (_, term) -> aux env term
  82     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
  83     | Ast.Binder (binder, var, body) ->
  84         Ast.Binder (binder, aux_capture_var env var, aux env body)
  85     | Ast.Case (term, indty, outty_opt, patterns) ->
  86         Ast.Case (aux env term, indty, aux_opt env outty_opt,
  87           List.map (aux_branch env) patterns)
  88     | Ast.LetIn (var, t1, t2) ->
  89         Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
  90     | Ast.LetRec (kind, definitions, body) ->
  91         Ast.LetRec (kind, List.map (aux_definition env) definitions,
  92           aux env body)
  93     | Ast.Uri (name, None) -> Ast.Uri (name, None)
  94     | Ast.Uri (name, Some substs) ->
  95         Ast.Uri (name, Some (aux_substs env substs))
  96     | Ast.Ident (name, Some substs) ->
  97         Ast.Ident (name, Some (aux_substs env substs))
  98     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
  99
 100     | Ast.Implicit
 101     | Ast.Ident _
 102     | Ast.Num _
 103     | Ast.Sort _
 104     | Ast.Symbol _
 105     | Ast.UserInput -> term
 106
 107     | Ast.Magic magic -> aux_magic env magic
 108     | Ast.Variable var -> aux_variable env var
 109
 110     | _ -> assert false
 111   and aux_opt env = function
 112     | Some term -> Some (aux env term)
 113     | None -> None
 114   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
 115   and aux_branch env (pattern, term) =
 116     (aux_pattern env pattern, aux env term)
 117   and aux_pattern env (head, hrefs, vars) =
 118     (head, hrefs, List.map (aux_capture_var env) vars)
 119   and aux_definition env (var, term, i) =
 120     (aux_capture_var env var, aux env term, i)
 121   and aux_substs env substs =
 122     List.map (fun (name, term) -> (name, aux env term)) substs
 123   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
 124   and aux_variable env = function
 125     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
 126     | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
 127     | Ast.TermVar name -> Env.lookup_term env name
 128     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
 129     | Ast.Ascription (term, name) -> assert false
 130   and aux_magic env = function
 131     | Ast.Default (some_pattern, none_pattern) ->
 132         (match CicNotationUtil.names_of_term some_pattern with
 133         | [] -> assert false (* some pattern must contain at least 1 name *)
 134         | (name :: _) as names ->
 135             (match Env.lookup_value env name with
 136             | Env.OptValue (Some _) ->
 137                 (* assumption: if "name" above is bound to Some _, then all
 138                  * names returned by "meta_names_of" are bound to Some _ as well
 139                  *)
 140                 aux (unopt_names names env) some_pattern
 141             | Env.OptValue None -> aux env none_pattern
 142             | _ -> assert false))
 143     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
 144         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 145         let meta_names =
 146           List.filter ((<>) acc_name)
 147             (CicNotationUtil.names_of_term rec_pattern)
 148         in
 149         (match meta_names with
 150         | [] -> assert false (* as above *)
 151         | (name :: _) as names ->
 152             let rec instantiate_fold_left acc env' =
 153               match Env.lookup_value env' name with
 154               | Env.ListValue (_ :: _) ->
 155                   instantiate_fold_left
 156                     (let acc_binding =
 157                       acc_name, (Env.TermType, Env.TermValue acc)
 158                      in
 159                      aux (acc_binding :: head_names names env') rec_pattern)
 160                     (tail_names names env')
 161               | Env.ListValue [] -> acc
 162               | _ -> assert false
 163             in
 164             instantiate_fold_left (aux env base_pattern) env)
 165     | Ast.Fold (`Right, base_pattern, names, rec_pattern) ->
 166         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 167         let meta_names =
 168           List.filter ((<>) acc_name)
 169             (CicNotationUtil.names_of_term rec_pattern)
 170         in
 171         (match meta_names with
 172         | [] -> assert false (* as above *)
 173         | (name :: _) as names ->
 174             let rec instantiate_fold_right env' =
 175               match Env.lookup_value env' name with
 176               | Env.ListValue (_ :: _) ->
 177                   let acc = instantiate_fold_right (tail_names names env') in
 178                   let acc_binding =
 179                     acc_name, (Env.TermType, Env.TermValue acc)
 180                   in
 181                   aux (acc_binding :: head_names names env') rec_pattern
 182               | Env.ListValue [] -> aux env base_pattern
 183               | _ -> assert false
 184             in
 185             instantiate_fold_right env)
 186     | Ast.If (_, p_true, p_false) as t ->
 187         aux env (CicNotationUtil.find_branch (Ast.Magic t))
 188     | Ast.Fail -> assert false
 189     | _ -> assert false
 190   in
 191   aux env term
 192
 193 let instantiate_appl_pattern env appl_pattern =
 194   let lookup name =
 195     try List.assoc name env
 196     with Not_found ->
 197       prerr_endline (sprintf "Name %s not found" name);
 198       assert false
 199   in
 200   let rec aux = function
 201     | Ast.UriPattern uri -> CicUtil.term_of_uri uri
 202     | Ast.ImplicitPattern -> Cic.Implicit None
 203     | Ast.VarPattern name -> lookup name
 204     | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
 205   in
 206   aux appl_pattern
 207