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