helm/ocaml/cic_unification/cicMkImplicit.ml

   1 (* Copyright (C) 2004, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 (* identity_relocation_list_for_metavariable i canonical_context         *)
  27 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
  28 (* where n = List.length [canonical_context]                             *)
  29 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
  30 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
  31   let rec aux =
  32    function
  33       (_,[]) -> []
  34     | (n,None::tl) -> None::(aux ((n+1),tl))
  35     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
  36   in
  37    aux (start,canonical_context)
  38
  39 (* Returns the first meta whose number is above the *)
  40 (* number of the higher meta.                       *)
  41 let new_meta metasenv subst =
  42   let rec aux =
  43    function
  44       None, [] -> 1
  45     | Some n, [] -> n
  46     | None, n::tl -> aux (Some n,tl)
  47     | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  48   in
  49   let indexes =
  50     (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst)
  51   in
  52   1 + aux (None, indexes)
  53
  54 let mk_implicit metasenv subst context =
  55   let newmeta = new_meta metasenv subst in
  56   let newuniv = CicUniv.fresh () in
  57   let irl = identity_relocation_list_for_metavariable context in
  58     (* in the following mk_* functions we apply substitution to canonical
  59     * context since we have the invariant that the metasenv has already been
  60     * instantiated with subst *)
  61   let context = CicMetaSubst.apply_subst_context subst context in
  62   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
  63     (* TASSI: ?? *)
  64     newmeta + 1, context, Cic.Meta (newmeta, []);
  65     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
  66    newmeta + 2)
  67
  68 let mk_implicit_type metasenv subst context =
  69   let newmeta = new_meta metasenv subst in
  70   let newuniv = CicUniv.fresh () in
  71   let context = CicMetaSubst.apply_subst_context subst context in
  72   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
  73     (* TASSI: ?? *)
  74     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
  75    newmeta + 1)
  76
  77 let mk_implicit_sort metasenv subst =
  78   let newmeta = new_meta metasenv subst in
  79   let newuniv = CicUniv.fresh () in
  80   ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
  81   (* TASSI: ?? *)
  82
  83 let n_fresh_metas metasenv subst context n =
  84   if n = 0 then metasenv, []
  85   else
  86     let irl = identity_relocation_list_for_metavariable context in
  87     let context = CicMetaSubst.apply_subst_context subst context in
  88     let newmeta = new_meta metasenv subst in
  89     let newuniv = CicUniv.fresh () in
  90     let rec aux newmeta n =
  91       if n = 0 then metasenv, []
  92       else
  93         let metasenv', l = aux (newmeta + 3) (n-1) in
  94         (* TASSI: ?? *)
  95         (newmeta, context, Cic.Sort (Cic.Type newuniv))::
  96         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
  97         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
  98         Cic.Meta(newmeta+2,irl)::l in
  99     aux newmeta n
 100
 101 let fresh_subst metasenv subst context uris =
 102   let irl = identity_relocation_list_for_metavariable context in
 103   let context = CicMetaSubst.apply_subst_context subst context in
 104   let newmeta = new_meta metasenv subst in
 105   let newuniv = CicUniv.fresh () in
 106   let rec aux newmeta = function
 107       [] -> metasenv, []
 108     | uri::tl ->
 109        let metasenv', l = aux (newmeta + 3) tl in
 110          (* TASSI: ?? *)
 111          (newmeta, context, Cic.Sort (Cic.Type newuniv))::
 112          (newmeta + 1, context, Cic.Meta (newmeta, irl))::
 113          (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
 114           (uri,Cic.Meta(newmeta+2,irl))::l in
 115     aux newmeta uris
 116
 117 let expand_implicits metasenv subst context term =
 118   let rec aux metasenv context = function
 119     | (Cic.Rel _) as t -> metasenv, t
 120     | (Cic.Sort _) as t -> metasenv, t
 121     | Cic.Const (uri, subst) ->
 122         let metasenv', subst' = do_subst metasenv context subst in
 123         metasenv', Cic.Const (uri, subst')
 124     | Cic.Var (uri, subst) ->
 125         let metasenv', subst' = do_subst metasenv context subst in
 126         metasenv', Cic.Var (uri, subst')
 127     | Cic.MutInd (uri, i, subst) ->
 128         let metasenv', subst' = do_subst metasenv context subst in
 129         metasenv', Cic.MutInd (uri, i, subst')
 130     | Cic.MutConstruct (uri, i, j, subst) ->
 131         let metasenv', subst' = do_subst metasenv context subst in
 132         metasenv', Cic.MutConstruct (uri, i, j, subst')
 133     | Cic.Meta (n,l) ->
 134         let metasenv', l' = do_local_context metasenv context l in
 135         metasenv', Cic.Meta (n, l')
 136     | Cic.Implicit (Some `Type) ->
 137         let (metasenv', idx) = mk_implicit_type metasenv subst context in
 138         let irl = identity_relocation_list_for_metavariable context in
 139         metasenv', Cic.Meta (idx, irl)
 140     | Cic.Implicit (Some `Closed) ->
 141         let (metasenv', idx) = mk_implicit metasenv subst [] in
 142         metasenv', Cic.Meta (idx, [])
 143     | Cic.Implicit None ->
 144         let (metasenv', idx) = mk_implicit metasenv subst context in
 145         let irl = identity_relocation_list_for_metavariable context in
 146         metasenv', Cic.Meta (idx, irl)
 147     | Cic.Cast (te, ty) ->
 148         let metasenv', ty' = aux metasenv context ty in
 149         let metasenv'', te' = aux metasenv' context te in
 150         metasenv'', Cic.Cast (te', ty')
 151     | Cic.Prod (name, s, t) ->
 152         let metasenv', s' = aux metasenv context s in
 153         let metasenv'', t' =
 154           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 155         in
 156         metasenv'', Cic.Prod (name, s', t')
 157     | Cic.Lambda (name, s, t) ->
 158         let metasenv', s' = aux metasenv context s in
 159         let metasenv'', t' =
 160           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 161         in
 162         metasenv'', Cic.Lambda (name, s', t')
 163     | Cic.LetIn (name, s, t) ->
 164         let metasenv', s' = aux metasenv context s in
 165         let metasenv'', t' =
 166           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
 167         in
 168         metasenv'', Cic.LetIn (name, s', t')
 169     | Cic.Appl l when List.length l > 1 ->
 170         let metasenv', l' =
 171           List.fold_right
 172             (fun term (metasenv, terms) ->
 173               let new_metasenv, term = aux metasenv context term in
 174               new_metasenv, term :: terms)
 175             l (metasenv, [])
 176         in
 177         metasenv', Cic.Appl l'
 178     | Cic.Appl _ -> assert false
 179     | Cic.MutCase (uri, i, outtype, term, patterns) ->
 180         let metasenv', l' =
 181           List.fold_right
 182             (fun term (metasenv, terms) ->
 183               let new_metasenv, term = aux metasenv context term in
 184               new_metasenv, term :: terms)
 185             (outtype :: term :: patterns) (metasenv, [])
 186         in
 187         let outtype', term', patterns' =
 188           match l' with
 189           | outtype' :: term' :: patterns' -> outtype', term', patterns'
 190           | _ -> assert false
 191         in
 192         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
 193     | Cic.Fix (i, funs) ->
 194         let metasenv', types =
 195           List.fold_right
 196             (fun (name, _, typ, _) (metasenv, types) ->
 197               let new_metasenv, new_type = aux metasenv context typ in
 198               (new_metasenv, (name, new_type) :: types))
 199             funs (metasenv, [])
 200         in
 201         let context' =
 202           (List.rev_map
 203             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 204             types)
 205           @ context
 206         in
 207         let metasenv'', bodies =
 208           List.fold_right
 209             (fun (_, _, _, body) (metasenv, bodies) ->
 210               let new_metasenv, new_body = aux metasenv context' body in
 211               (new_metasenv, new_body :: bodies))
 212             funs (metasenv', [])
 213         in
 214         let rec combine = function
 215           | ((name, index, _, _) :: funs_tl),
 216             ((_, typ) :: typ_tl),
 217             (body :: body_tl) ->
 218               (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 219           | [], [], [] -> []
 220           | _ -> assert false
 221         in
 222         let funs' = combine (funs, types, bodies) in
 223         metasenv'', Cic.Fix (i, funs')
 224     | Cic.CoFix (i, funs) ->
 225         let metasenv', types =
 226           List.fold_right
 227             (fun (name, typ, _) (metasenv, types) ->
 228               let new_metasenv, new_type = aux metasenv context typ in
 229               (new_metasenv, (name, new_type) :: types))
 230             funs (metasenv, [])
 231         in
 232         let context' =
 233           (List.rev_map
 234             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 235             types)
 236           @ context
 237         in
 238         let metasenv'', bodies =
 239           List.fold_right
 240             (fun (_, _, body) (metasenv, bodies) ->
 241               let new_metasenv, new_body = aux metasenv context' body in
 242               (new_metasenv, new_body :: bodies))
 243             funs (metasenv', [])
 244         in
 245         let rec combine = function
 246           | ((name, _, _) :: funs_tl),
 247             ((_, typ) :: typ_tl),
 248             (body :: body_tl) ->
 249               (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 250           | [], [], [] -> []
 251           | _ -> assert false
 252         in
 253         let funs' = combine (funs, types, bodies) in
 254         metasenv'', Cic.CoFix (i, funs')
 255   and do_subst metasenv context subst =
 256     List.fold_right
 257       (fun (uri, term) (metasenv, substs) ->
 258         let metasenv', term' = aux metasenv context term in
 259         (metasenv', (uri, term') :: substs))
 260       subst (metasenv, [])
 261   and do_local_context metasenv context local_context =
 262     List.fold_right
 263       (fun term (metasenv, local_context) ->
 264         let metasenv', term' =
 265           match term with
 266           | None -> metasenv, None
 267           | Some term ->
 268               let metasenv', term' = aux metasenv context term in
 269               metasenv', Some term'
 270         in
 271         metasenv', term' :: local_context)
 272       local_context (metasenv, [])
 273   in
 274   aux metasenv context term
 275