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