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