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     | hd :: tl -> aux (hd :: acc) tl
  39     | [] -> acc
  40   in
  41   aux [] env
  42
  43 let head_names names env =
  44   let rec aux acc = function
  45     | (name, (ty, v)) :: tl when List.mem name names ->
  46         (match ty, v with
  47         | Env.ListType ty, Env.ListValue (v :: _) ->
  48             aux ((name, (ty, v)) :: acc) tl
  49         | _ -> assert false)
  50     | _ :: tl -> aux acc tl
  51       (* base pattern may contain only meta names, thus we trash all others *)
  52     | [] -> acc
  53   in
  54   aux [] env
  55
  56 let tail_names names env =
  57   let rec aux acc = function
  58     | (name, (ty, v)) :: tl when List.mem name names ->
  59         (match ty, v with
  60         | Env.ListType ty, Env.ListValue (_ :: vtl) ->
  61             aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
  62         | _ -> assert false)
  63     | binding :: tl -> aux (binding :: acc) tl
  64     | [] -> acc
  65   in
  66   aux [] env
  67
  68 let instantiate_level2 env term =
  69   let fresh_env = ref [] in
  70   let lookup_fresh_name n =
  71     try
  72       List.assoc n !fresh_env
  73     with Not_found ->
  74       let new_name = CicNotationUtil.fresh_name () in
  75       fresh_env := (n, new_name) :: !fresh_env;
  76       new_name
  77   in
  78   let rec aux env term =
  79 (*     prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
  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         let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
 133         let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
 134         let opt_names =
 135           List.filter
 136             (fun name -> not (List.mem name none_pattern_names))
 137             some_pattern_names
 138         in
 139         (match opt_names with
 140         | [] -> assert false (* some pattern must contain at least 1 name *)
 141         | (name :: _) as names ->
 142             (match Env.lookup_value env name with
 143             | Env.OptValue (Some _) ->
 144                 (* assumption: if "name" above is bound to Some _, then all
 145                  * names returned by "meta_names_of" are bound to Some _ as well
 146                  *)
 147                 aux (unopt_names names env) some_pattern
 148             | Env.OptValue None -> aux env none_pattern
 149             | _ ->
 150                 prerr_endline (sprintf
 151                   "lookup of %s in env %s did not return an optional value"
 152                   name (CicNotationPp.pp_env env));
 153                 assert false))
 154     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
 155         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 156         let meta_names =
 157           List.filter ((<>) acc_name)
 158             (CicNotationUtil.names_of_term rec_pattern)
 159         in
 160         (match meta_names with
 161         | [] -> assert false (* as above *)
 162         | (name :: _) as names ->
 163             let rec instantiate_fold_left acc env' =
 164               match Env.lookup_value env' name with
 165               | Env.ListValue (_ :: _) ->
 166                   instantiate_fold_left
 167                     (let acc_binding =
 168                       acc_name, (Env.TermType, Env.TermValue acc)
 169                      in
 170                      aux (acc_binding :: head_names names env') rec_pattern)
 171                     (tail_names names env')
 172               | Env.ListValue [] -> acc
 173               | _ -> assert false
 174             in
 175             instantiate_fold_left (aux env base_pattern) env)
 176     | Ast.Fold (`Right, base_pattern, names, rec_pattern) ->
 177         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
 178         let meta_names =
 179           List.filter ((<>) acc_name)
 180             (CicNotationUtil.names_of_term rec_pattern)
 181         in
 182         (match meta_names with
 183         | [] -> assert false (* as above *)
 184         | (name :: _) as names ->
 185             let rec instantiate_fold_right env' =
 186               match Env.lookup_value env' name with
 187               | Env.ListValue (_ :: _) ->
 188                   let acc = instantiate_fold_right (tail_names names env') in
 189                   let acc_binding =
 190                     acc_name, (Env.TermType, Env.TermValue acc)
 191                   in
 192                   aux (acc_binding :: head_names names env') rec_pattern
 193               | Env.ListValue [] -> aux env base_pattern
 194               | _ -> assert false
 195             in
 196             instantiate_fold_right env)
 197     | Ast.If (_, p_true, p_false) as t ->
 198         aux env (CicNotationUtil.find_branch (Ast.Magic t))
 199     | Ast.Fail -> assert false
 200     | _ -> assert false
 201   in
 202   aux env term
 203
 204 let instantiate_appl_pattern env appl_pattern =
 205   let lookup name =
 206     try List.assoc name env
 207     with Not_found ->
 208       prerr_endline (sprintf "Name %s not found" name);
 209       assert false
 210   in
 211   let rec aux = function
 212     | Ast.UriPattern uri -> CicUtil.term_of_uri uri
 213     | Ast.ImplicitPattern -> Cic.Implicit None
 214     | Ast.VarPattern name -> lookup name
 215     | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
 216   in
 217   aux appl_pattern
 218