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