helm/ocaml/cic_unification/cicMkImplicit.ml

   1
   2 (* identity_relocation_list_for_metavariable i canonical_context         *)
   3 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
   4 (* where n = List.length [canonical_context]                             *)
   5 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
   6 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
   7  let canonical_context_length = List.length canonical_context in
   8   let rec aux =
   9    function
  10       (_,[]) -> []
  11     | (n,None::tl) -> None::(aux ((n+1),tl))
  12     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
  13   in
  14    aux (start,canonical_context)
  15
  16 (* Returns the first meta whose number is above the *)
  17 (* number of the higher meta.                       *)
  18 let new_meta metasenv =
  19   let rec aux =
  20    function
  21       None,[] -> 1
  22     | Some n,[] -> n
  23     | None,(n,_,_)::tl -> aux (Some n,tl)
  24     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  25   in
  26    1 + aux (None,metasenv)
  27
  28 let mk_implicit metasenv context =
  29   let newmeta = new_meta metasenv in
  30   let irl = identity_relocation_list_for_metavariable context in
  31   ([ newmeta, context, Cic.Sort Cic.Type ;
  32     newmeta + 1, context, Cic.Meta (newmeta, irl);
  33     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
  34    newmeta + 2)
  35
  36 let n_fresh_metas metasenv context n =
  37   if n = 0 then metasenv, []
  38   else
  39     let irl = identity_relocation_list_for_metavariable context in
  40     let newmeta = new_meta metasenv in
  41     let rec aux newmeta n =
  42       if n = 0 then metasenv, []
  43       else
  44         let metasenv', l = aux (newmeta + 3) (n-1) in
  45         (newmeta, context, Cic.Sort Cic.Type)::
  46         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
  47         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
  48         Cic.Meta(newmeta+2,irl)::l in
  49     aux newmeta n
  50
  51 let fresh_subst metasenv context uris =
  52   let irl = identity_relocation_list_for_metavariable context in
  53   let newmeta = new_meta metasenv in
  54   let rec aux newmeta = function
  55       [] -> metasenv, []
  56     | uri::tl ->
  57        let metasenv', l = aux (newmeta + 3) tl in
  58          (newmeta, context, Cic.Sort Cic.Type)::
  59          (newmeta + 1, context, Cic.Meta (newmeta, irl))::
  60          (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
  61           (uri,Cic.Meta(newmeta+2,irl))::l in
  62     aux newmeta uris
  63
  64 let mk_implicit' metasenv context =
  65   let (metasenv, index) = mk_implicit metasenv context in
  66   (metasenv, index - 1, index)
  67
  68 let mk_implicit_type metasenv context =
  69   let newmeta = new_meta metasenv in
  70   let irl = identity_relocation_list_for_metavariable context in
  71   ([ newmeta, context, Cic.Sort Cic.Type ;
  72     newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
  73    newmeta + 1)
  74
  75 let expand_implicits metasenv context term =
  76   let rec aux metasenv context = function
  77     | (Cic.Rel _) as t -> metasenv, t
  78     | (Cic.Sort _) as t -> metasenv, t
  79     | Cic.Const (uri, subst) ->
  80         let metasenv', subst' = do_subst metasenv context subst in
  81         metasenv', Cic.Const (uri, subst')
  82     | Cic.Var (uri, subst) ->
  83         let metasenv', subst' = do_subst metasenv context subst in
  84         metasenv', Cic.Var (uri, subst')
  85     | Cic.MutInd (uri, i, subst) ->
  86         let metasenv', subst' = do_subst metasenv context subst in
  87         metasenv', Cic.MutInd (uri, i, subst')
  88     | Cic.MutConstruct (uri, i, j, subst) ->
  89         let metasenv', subst' = do_subst metasenv context subst in
  90         metasenv', Cic.MutConstruct (uri, i, j, subst')
  91     | Cic.Meta (n,l) ->
  92         let metasenv', l' = do_local_context metasenv context l in
  93         metasenv', Cic.Meta (n, l')
  94     | Cic.Implicit ->
  95         let (metasenv', type_index, _) = mk_implicit' metasenv context in
  96         let irl = identity_relocation_list_for_metavariable context in
  97         metasenv', Cic.Meta (type_index, irl)
  98     | Cic.Cast (te, ty) ->
  99         let metasenv', ty' = aux metasenv context ty in
 100         let metasenv'', te' = aux metasenv' context te in
 101         metasenv'', Cic.Cast (te', ty')
 102     | Cic.Prod (name, s, t) ->
 103         let metasenv', s' = aux metasenv context s in
 104         let metasenv'', t' =
 105           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 106         in
 107         metasenv'', Cic.Prod (name, s', t')
 108     | Cic.Lambda (name, s, t) ->
 109         let metasenv', s' = aux metasenv context s in
 110         let metasenv'', t' =
 111           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 112         in
 113         metasenv'', Cic.Lambda (name, s', t')
 114     | Cic.LetIn (name, s, t) ->
 115         let metasenv', s' = aux metasenv context s in
 116         let metasenv'', t' =
 117           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
 118         in
 119         metasenv'', Cic.LetIn (name, s', t')
 120     | Cic.Appl l when List.length l > 1 ->
 121         let metasenv', l' =
 122           List.fold_right
 123             (fun term (metasenv, terms) ->
 124               let new_metasenv, term = aux metasenv context term in
 125               new_metasenv, term :: terms)
 126             l (metasenv, [])
 127         in
 128         metasenv', Cic.Appl l'
 129     | Cic.Appl _ -> assert false
 130     | Cic.MutCase (uri, i, outtype, term, patterns) ->
 131         let metasenv', l' =
 132           List.fold_right
 133             (fun term (metasenv, terms) ->
 134               let new_metasenv, term = aux metasenv context term in
 135               new_metasenv, term :: terms)
 136             (outtype :: term :: patterns) (metasenv, [])
 137         in
 138         let outtype', term', patterns' =
 139           match l' with
 140           | outtype' :: term' :: patterns' -> outtype', term', patterns'
 141           | _ -> assert false
 142         in
 143         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
 144     | Cic.Fix (i, funs) ->
 145         let metasenv', types =
 146           List.fold_right
 147             (fun (name, _, typ, _) (metasenv, types) ->
 148               let new_metasenv, new_type = aux metasenv context typ in
 149               (new_metasenv, (name, new_type) :: types))
 150             funs (metasenv, [])
 151         in
 152         let context' =
 153           (List.rev_map
 154             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 155             types)
 156           @ context
 157         in
 158         let metasenv'', bodies =
 159           List.fold_right
 160             (fun (_, _, _, body) (metasenv, bodies) ->
 161               let new_metasenv, new_body = aux metasenv context' body in
 162               (new_metasenv, new_body :: bodies))
 163             funs (metasenv', [])
 164         in
 165         let rec combine = function
 166           | ((name, index, _, _) :: funs_tl),
 167             ((_, typ) :: typ_tl),
 168             (body :: body_tl) ->
 169               (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 170           | [], [], [] -> []
 171           | _ -> assert false
 172         in
 173         let funs' = combine (funs, types, bodies) in
 174         metasenv'', Cic.Fix (i, funs')
 175     | Cic.CoFix (i, funs) ->
 176         let metasenv', types =
 177           List.fold_right
 178             (fun (name, typ, _) (metasenv, types) ->
 179               let new_metasenv, new_type = aux metasenv context typ in
 180               (new_metasenv, (name, new_type) :: types))
 181             funs (metasenv, [])
 182         in
 183         let context' =
 184           (List.rev_map
 185             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 186             types)
 187           @ context
 188         in
 189         let metasenv'', bodies =
 190           List.fold_right
 191             (fun (_, _, body) (metasenv, bodies) ->
 192               let new_metasenv, new_body = aux metasenv context' body in
 193               (new_metasenv, new_body :: bodies))
 194             funs (metasenv', [])
 195         in
 196         let rec combine = function
 197           | ((name, _, _) :: funs_tl),
 198             ((_, typ) :: typ_tl),
 199             (body :: body_tl) ->
 200               (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 201           | [], [], [] -> []
 202           | _ -> assert false
 203         in
 204         let funs' = combine (funs, types, bodies) in
 205         metasenv'', Cic.CoFix (i, funs')
 206   and do_subst metasenv context subst =
 207     List.fold_right
 208       (fun (uri, term) (metasenv, substs) ->
 209         let metasenv', term' = aux metasenv context term in
 210         (metasenv', (uri, term') :: substs))
 211       subst (metasenv, [])
 212   and do_local_context metasenv context local_context =
 213     List.fold_right
 214       (fun term (metasenv, local_context) ->
 215         let metasenv', term' =
 216           match term with
 217           | None -> metasenv, None
 218           | Some term ->
 219               let metasenv', term' = aux metasenv context term in
 220               metasenv', Some term'
 221         in
 222         metasenv', term' :: local_context)
 223       local_context (metasenv, [])
 224   in
 225   aux metasenv context term
 226