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, [], Cic.Sort Cic.Type ;
  32     newmeta + 1, context, Cic.Meta (newmeta, []);
  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_type metasenv context =
  65   let newmeta = new_meta metasenv in
  66   ([ newmeta, [], Cic.Sort Cic.Type ;
  67     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
  68    newmeta + 1)
  69
  70 let expand_implicits metasenv context term =
  71   let rec aux metasenv context = function
  72     | (Cic.Rel _) as t -> metasenv, t
  73     | (Cic.Sort _) as t -> metasenv, t
  74     | Cic.Const (uri, subst) ->
  75         let metasenv', subst' = do_subst metasenv context subst in
  76         metasenv', Cic.Const (uri, subst')
  77     | Cic.Var (uri, subst) ->
  78         let metasenv', subst' = do_subst metasenv context subst in
  79         metasenv', Cic.Var (uri, subst')
  80     | Cic.MutInd (uri, i, subst) ->
  81         let metasenv', subst' = do_subst metasenv context subst in
  82         metasenv', Cic.MutInd (uri, i, subst')
  83     | Cic.MutConstruct (uri, i, j, subst) ->
  84         let metasenv', subst' = do_subst metasenv context subst in
  85         metasenv', Cic.MutConstruct (uri, i, j, subst')
  86     | Cic.Meta (n,l) ->
  87         let metasenv', l' = do_local_context metasenv context l in
  88         metasenv', Cic.Meta (n, l')
  89     | Cic.Implicit (Some `Type) ->
  90         let (metasenv', idx) = mk_implicit_type metasenv context in
  91         let irl = identity_relocation_list_for_metavariable context in
  92         metasenv', Cic.Meta (idx, irl)
  93     | Cic.Implicit (Some `Closed) ->
  94         let (metasenv', idx) = mk_implicit metasenv [] in
  95         metasenv', Cic.Meta (idx, [])
  96     | Cic.Implicit None ->
  97         let (metasenv', idx) = mk_implicit metasenv context in
  98         let irl = identity_relocation_list_for_metavariable context in
  99         metasenv', Cic.Meta (idx, irl)
 100     | Cic.Cast (te, ty) ->
 101         let metasenv', ty' = aux metasenv context ty in
 102         let metasenv'', te' = aux metasenv' context te in
 103         metasenv'', Cic.Cast (te', ty')
 104     | Cic.Prod (name, s, t) ->
 105         let metasenv', s' = aux metasenv context s in
 106         let metasenv'', t' =
 107           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 108         in
 109         metasenv'', Cic.Prod (name, s', t')
 110     | Cic.Lambda (name, s, t) ->
 111         let metasenv', s' = aux metasenv context s in
 112         let metasenv'', t' =
 113           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 114         in
 115         metasenv'', Cic.Lambda (name, s', t')
 116     | Cic.LetIn (name, s, t) ->
 117         let metasenv', s' = aux metasenv context s in
 118         let metasenv'', t' =
 119           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
 120         in
 121         metasenv'', Cic.LetIn (name, s', t')
 122     | Cic.Appl l when List.length l > 1 ->
 123         let metasenv', l' =
 124           List.fold_right
 125             (fun term (metasenv, terms) ->
 126               let new_metasenv, term = aux metasenv context term in
 127               new_metasenv, term :: terms)
 128             l (metasenv, [])
 129         in
 130         metasenv', Cic.Appl l'
 131     | Cic.Appl _ -> assert false
 132     | Cic.MutCase (uri, i, outtype, term, patterns) ->
 133         let metasenv', l' =
 134           List.fold_right
 135             (fun term (metasenv, terms) ->
 136               let new_metasenv, term = aux metasenv context term in
 137               new_metasenv, term :: terms)
 138             (outtype :: term :: patterns) (metasenv, [])
 139         in
 140         let outtype', term', patterns' =
 141           match l' with
 142           | outtype' :: term' :: patterns' -> outtype', term', patterns'
 143           | _ -> assert false
 144         in
 145         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
 146     | Cic.Fix (i, funs) ->
 147         let metasenv', types =
 148           List.fold_right
 149             (fun (name, _, typ, _) (metasenv, types) ->
 150               let new_metasenv, new_type = aux metasenv context typ in
 151               (new_metasenv, (name, new_type) :: types))
 152             funs (metasenv, [])
 153         in
 154         let context' =
 155           (List.rev_map
 156             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 157             types)
 158           @ context
 159         in
 160         let metasenv'', bodies =
 161           List.fold_right
 162             (fun (_, _, _, body) (metasenv, bodies) ->
 163               let new_metasenv, new_body = aux metasenv context' body in
 164               (new_metasenv, new_body :: bodies))
 165             funs (metasenv', [])
 166         in
 167         let rec combine = function
 168           | ((name, index, _, _) :: funs_tl),
 169             ((_, typ) :: typ_tl),
 170             (body :: body_tl) ->
 171               (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 172           | [], [], [] -> []
 173           | _ -> assert false
 174         in
 175         let funs' = combine (funs, types, bodies) in
 176         metasenv'', Cic.Fix (i, funs')
 177     | Cic.CoFix (i, funs) ->
 178         let metasenv', types =
 179           List.fold_right
 180             (fun (name, typ, _) (metasenv, types) ->
 181               let new_metasenv, new_type = aux metasenv context typ in
 182               (new_metasenv, (name, new_type) :: types))
 183             funs (metasenv, [])
 184         in
 185         let context' =
 186           (List.rev_map
 187             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 188             types)
 189           @ context
 190         in
 191         let metasenv'', bodies =
 192           List.fold_right
 193             (fun (_, _, body) (metasenv, bodies) ->
 194               let new_metasenv, new_body = aux metasenv context' body in
 195               (new_metasenv, new_body :: bodies))
 196             funs (metasenv', [])
 197         in
 198         let rec combine = function
 199           | ((name, _, _) :: funs_tl),
 200             ((_, typ) :: typ_tl),
 201             (body :: body_tl) ->
 202               (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 203           | [], [], [] -> []
 204           | _ -> assert false
 205         in
 206         let funs' = combine (funs, types, bodies) in
 207         metasenv'', Cic.CoFix (i, funs')
 208   and do_subst metasenv context subst =
 209     List.fold_right
 210       (fun (uri, term) (metasenv, substs) ->
 211         let metasenv', term' = aux metasenv context term in
 212         (metasenv', (uri, term') :: substs))
 213       subst (metasenv, [])
 214   and do_local_context metasenv context local_context =
 215     List.fold_right
 216       (fun term (metasenv, local_context) ->
 217         let metasenv', term' =
 218           match term with
 219           | None -> metasenv, None
 220           | Some term ->
 221               let metasenv', term' = aux metasenv context term in
 222               metasenv', Some term'
 223         in
 224         metasenv', term' :: local_context)
 225       local_context (metasenv, [])
 226   in
 227   aux metasenv context term
 228